Home
last modified time | relevance | path

Searched refs:th_solver (Results 1 – 25 of 53) sorted by relevance

123

/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Deuf_solver.h97 th_solver* m_qsolver { nullptr };
105 scoped_ptr_vector<th_solver> m_solvers;
106 ptr_vector<th_solver> m_id2solver;
132 th_solver* get_solver(family_id fid, func_decl* f);
133 th_solver* sort2solver(sort* s) { return get_solver(s->get_family_id(), nullptr); } in sort2solver()
134 th_solver* func_decl2solver(func_decl* f) { return get_solver(f->get_family_id(), f); } in func_decl2solver()
135 th_solver* quantifier2solver();
136 th_solver* expr2solver(expr* e);
137 th_solver* bool_var2solver(sat::bool_var v);
138 void add_solver(th_solver* th);
[all …]
H A Dsat_th.h100 …class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_i…
104 … th_solver(ast_manager& m, symbol const& name, euf::theory_id id) : extension(name, id), m(m) {} in th_solver() function
106 virtual th_solver* clone(euf::solver& ctx) = 0;
123 class th_euf_solver : public th_solver {
H A Deuf_solver.cpp62 th_solver* solver::bool_var2solver(sat::bool_var v) { in bool_var2solver()
71 th_solver* solver::expr2solver(expr* e) { in expr2solver()
79 th_solver* solver::quantifier2solver() { in quantifier2solver()
90 th_solver* solver::get_solver(family_id fid, func_decl* f) { in get_solver()
126 void solver::add_solver(th_solver* th) { in add_solver()
H A Dq_solver.h68 euf::th_solver* clone(euf::solver& ctx) override;
H A Dfpa_solver.h74 euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } in clone()
H A Dba_solver.h49 class ba_solver : public euf::th_solver, public ba::solver_interface {
154 …euf::th_solver* clone_aux(ast_manager& m, sat::solver& s, sat::sat_internalizer& si, euf::theory_i…
437 euf::th_solver* clone(euf::solver& ctx) override;
H A Duser_solver.h126 euf::th_solver* clone(euf::solver& ctx) override;
H A Duser_solver.cpp149 euf::th_solver* solver::clone(euf::solver& dst_ctx) { in clone()
H A Ddt_solver.h144 euf::th_solver* clone(euf::solver& ctx) override;
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Deuf_solver.h104 th_solver* m_qsolver = nullptr;
113 scoped_ptr_vector<th_solver> m_solvers;
114 ptr_vector<th_solver> m_id2solver;
142 th_solver* get_solver(family_id fid, func_decl* f);
143 th_solver* sort2solver(sort* s) { return get_solver(s->get_family_id(), nullptr); } in sort2solver()
144 th_solver* func_decl2solver(func_decl* f) { return get_solver(f->get_family_id(), f); } in func_decl2solver()
145 th_solver* quantifier2solver();
146 th_solver* expr2solver(expr* e);
147 th_solver* bool_var2solver(sat::bool_var v);
148 void add_solver(th_solver* th);
[all …]
H A Dsat_th.h100 …class th_solver : public sat::extension, public th_model_builder, public th_decompile, public th_i…
104 … th_solver(ast_manager& m, symbol const& name, euf::theory_id id) : extension(name, id), m(m) {} in th_solver() function
106 virtual th_solver* clone(euf::solver& ctx) = 0;
123 class th_euf_solver : public th_solver {
H A Deuf_solver.cpp69 th_solver* solver::bool_var2solver(sat::bool_var v) { in bool_var2solver()
78 th_solver* solver::expr2solver(expr* e) { in expr2solver()
86 th_solver* solver::quantifier2solver() { in quantifier2solver()
97 th_solver* solver::get_solver(family_id fid, func_decl* f) { in get_solver()
136 void solver::add_solver(th_solver* th) { in add_solver()
466 auto apply_solver = [&](th_solver* e) { in check()
H A Dfpa_solver.h77 euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } in clone()
H A Dq_solver.h78 euf::th_solver* clone(euf::solver& ctx) override;
H A Dpb_solver.h43 class solver : public euf::th_solver, public pb::solver_interface {
148 …euf::th_solver* clone_aux(ast_manager& m, sat::solver& s, sat::sat_internalizer& si, euf::theory_i…
407 euf::th_solver* clone(euf::solver& ctx) override;
H A Duser_solver.h128 euf::th_solver* clone(euf::solver& ctx) override;
H A Drecfun_solver.h102 euf::th_solver* clone(euf::solver& ctx) override;
H A Duser_solver.cpp163 euf::th_solver* solver::clone(euf::solver& dst_ctx) { in clone()
H A Ddt_solver.h148 euf::th_solver* clone(euf::solver& ctx) override;
/dports/math/py-z3-solver/z3-z3-4.8.10/src/cmd_context/
H A Dsimplify_cmd.cpp75 th_solver solver(ctx); in execute()
76 s.set_solver(alloc(th_solver, ctx)); in execute()
H A Deval_cmd.cpp76 ev.set_solver(alloc(th_solver, ctx)); in execute()
/dports/math/z3/z3-z3-4.8.13/src/cmd_context/
H A Dsimplify_cmd.cpp75 th_solver solver(ctx); in execute()
76 s.set_solver(alloc(th_solver, ctx)); in execute()
H A Deval_cmd.cpp76 ev.set_solver(alloc(th_solver, ctx)); in execute()
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/
H A Dsmt_core.c1461 s->th_solver = th; in init_smt_core()
1604 s->th_solver = th; in smt_core_reset_thsolver()
1747 s->th_ctrl.reset(s->th_solver); in reset_smt_core()
2070 s->th_ctrl.increase_decision_level(s->th_solver); in decide_literal()
5107 s->th_ctrl.push(s->th_solver); in smt_push()
5337 s->th_ctrl.pop(s->th_solver); in smt_pop()
5399 s->th_ctrl.clear(s->th_solver); in smt_clear()
5726 s->th_smt.end_atom_deletion(s->th_solver); in delete_irrelevant_variables()
5806 s->th_ctrl.start_internalization(s->th_solver); in internalization_start()
5897 s->th_ctrl.start_search(s->th_solver); in start_search()
[all …]
/dports/math/yices/yices-2.6.2/src/context/
H A Dcontext_solver.c334 l = core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l); in theory_branch()
342 return core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l); in theory_or_neg_branch()
350 return core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l); in theory_or_pos_branch()

123