Searched refs:yices_get_model (Results 1 – 14 of 14) sorted by relevance
| /dports/math/yices/yices-2.6.2/examples/ |
| H A D | example2.c | 85 mdl = yices_get_model(ctx, true); in main()
|
| H A D | example1c.c | 114 model_t* model = yices_get_model(ctx, true); // get the model in simple_test()
|
| H A D | example1b.c | 120 model = yices_get_model(ctx, 1); // get the model in simple_test()
|
| H A D | example1.c | 109 model_t* model = yices_get_model(ctx, true); // get the model in simple_test()
|
| H A D | example_unsat_core.c | 75 model = yices_get_model(ctx, true); in check_and_get_core()
|
| H A D | example_mcsat.c | 139 mdl = yices_get_model(ctx, true); in test_mcsat()
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_mcsat.c | 139 mdl = yices_get_model(ctx, true); in test_mcsat()
|
| H A D | sudoku.c | 189 model_t *model = yices_get_model(ctx, 1); in get_solution()
|
| /dports/math/py-pysmt/pysmt-0.9.0/pysmt/solvers/ |
| H A D | yices.py | 214 self.model = yicespy.yices_get_model(self.yices, 1)
|
| /dports/math/yices/yices-2.6.2/src/exists_forall/ |
| H A D | efsolver.c | 401 mdl = yices_get_model(ctx, true); in satisfy_context()
|
| /dports/math/yices/yices-2.6.2/src/include/ |
| H A D | yices.h | 3319 __YICES_DLLSPEC__ extern model_t *yices_get_model(context_t *ctx, int32_t keep_subst);
|
| /dports/math/yices/yices-2.6.2/src/frontend/smt2/ |
| H A D | smt2_commands.c | 3403 mdl = yices_get_model(g->ctx, true); in get_model()
|
| /dports/math/yices/yices-2.6.2/src/api/ |
| H A D | yices_api.c | 9040 EXPORTED model_t *yices_get_model(context_t *ctx, int32_t keep_subst) { in yices_get_model() function
9588 model = yices_get_model(&context, true); in yices_do_check_formulas()
|
| /dports/math/yices/yices-2.6.2/doc/manual/ |
| H A D | manual.tex | 4379 model_t *model = yices_get_model(ctx, true); // get the model
|