| /dports/math/z3/z3-z3-4.8.13/src/tactic/smtlogics/ |
| H A D | qfidl_tactic.cpp | 79 tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m), in mk_qfidl_tactic() local
93 bv_solver); in mk_qfidl_tactic()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/smtlogics/ |
| H A D | qfidl_tactic.cpp | 79 tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m),
93 bv_solver);
|
| /dports/math/yices/yices-2.6.2/src/context/ |
| H A D | context.c | 149 u = ctx->bv.eterm_of_var(ctx->bv_solver, x); in translate_bvvar_to_eterm()
650 x = ctx->bv.create_const(ctx->bv_solver, c); in map_bvconst_to_eterm()
2381 y = ctx->bv.create_zero(ctx->bv_solver, n); in map_bveq0_to_literal()
4391 y = ctx->bv.create_zero(ctx->bv_solver, n); in assert_toplevel_bveq0()
5292 ctx->bv_solver = solver; in create_bv_solver()
5334 ctx->bv_solver = NULL; in init_solvers()
5485 ctx->bv_solver = NULL; in init_context()
5594 if (ctx->bv_solver != NULL) { in delete_context()
5595 delete_bv_solver(ctx->bv_solver); in delete_context()
5596 safe_free(ctx->bv_solver); in delete_context()
[all …]
|
| H A D | dump_context.c | 152 dump_bv_solver(f, context->bv_solver); in dump_context()
|
| H A D | context_solver.c | 899 if (ctx->bv.value_in_model(ctx->bv_solver, x, b)) { in bv_value()
1045 ctx->bv.build_model(ctx->bv_solver); in context_build_model()
1081 ctx->bv.free_model(ctx->bv_solver); in context_build_model()
|
| H A D | context_types.h | 653 void *bv_solver; member
|
| H A D | context_statistics.c | 221 show_bvsolver_stats(f, ctx->bv_solver); in yices_show_statistics()
|
| H A D | context_utils.h | 648 return ctx->bv_solver != NULL; in context_has_bv_solver()
|
| /dports/math/z3/z3-z3-4.8.13/examples/python/tutorial/jupyter/ |
| H A D | strategies.ipynb | 71 …bv_solver = Then('simplify', \n 'solve-eqs', \n 'bit-blast', \n …
78 …"source": "In the example above, the tactic bv_solver implements a basic bit-vector solver using e…
85 …bv_solver = Then(With('simplify', mul2concat=True),\n 'solve-eqs', \n …
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/python/tutorial/jupyter/ |
| H A D | strategies.ipynb | 71 …bv_solver = Then('simplify', \n 'solve-eqs', \n 'bit-blast', \n …
78 …"source": "In the example above, the tactic bv_solver implements a basic bit-vector solver using e…
85 …bv_solver = Then(With('simplify', mul2concat=True),\n 'solve-eqs', \n …
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_smt_internalizer.c | 336 dump_bv_solver(f, ctx->bv_solver); in dump_context()
473 if (bv_solver_bitblast(context.bv_solver)) { in test_internalization()
|
| H A D | test_smt_blaster.c | 322 if (bv_solver_bitblast(context.bv_solver)) { in test_blaster()
|
| /dports/math/yices/yices-2.6.2/src/solvers/bv/ |
| H A D | dimacs_printer.c | 309 dimacs_print_bvvar(f, ctx->bv_solver, x); in dimacs_print_bv_code()
|
| /dports/math/yices/yices-2.6.2/src/frontend/ |
| H A D | yices_smt.c | 1244 show_bvsolver_stats(context.bv_solver); in print_results()
1593 bv = context->bv_solver; in dump_the_context()
|
| H A D | yices_smtcomp.c | 725 show_bvsolver_stats(context.bv_solver); in print_results()
|
| /dports/math/yices/yices-2.6.2/src/frontend/smt2/ |
| H A D | smt2_commands.c | 197 dump_bv_solver(f, ctx->bv_solver); in dump_context()
1665 show_bvsolver_stats(fd, b, ctx->bv_solver); in show_ctx_stats()
|
| /dports/math/yices/yices-2.6.2/doc/ |
| H A D | NOTES | 608 in bv_solver)
|
| /dports/math/yices/yices-2.6.2/src/frontend/yices/ |
| H A D | yices_reval.c | 2031 show_bvsolver_stats(context->bv_solver); in yices_showstats_cmd()
|