mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

register completion with solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-06 20:45:49 +02:00
parent 1cd162203d
commit 2897661bb3
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tactic/portfolio/euf_completion_tactic.cpp
View file

@ -35,6 +35,16 @@ class euf_side_condition_solver : public euf::side_condition_solver {
public: public:
euf_side_condition_solver(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_deps(m) {} euf_side_condition_solver(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_deps(m) {}
void push() override {
init_solver();
m_solver->push();
}
void pop(unsigned n) override {
SASSERT(m_solver.get());
m_solver->pop(n);
}
void add_constraint(expr* f, expr_dependency* d) override { void add_constraint(expr* f, expr_dependency* d) override {
if (!is_ground(f)) if (!is_ground(f))
return; return;
@ -66,7 +76,7 @@ public:
} }
}; };
static euf::completion* mk_completion(ast_manager& m, dependent_expr_state& s, params_ref const& p) { dependent_expr_simplifier* mk_euf_completion_simplifier(ast_manager& m, dependent_expr_state& s, params_ref const& p) {
auto r = alloc(euf::completion, m, s); auto r = alloc(euf::completion, m, s);
auto scs = alloc(euf_side_condition_solver, m, p); auto scs = alloc(euf_side_condition_solver, m, p);
r->set_solver(scs); r->set_solver(scs);
@ -75,5 +85,5 @@ static euf::completion* mk_completion(ast_manager& m, dependent_expr_state& s, p
tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) {
return alloc(dependent_expr_state_tactic, m, p, return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return mk_completion(m, s, p); }); [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return mk_euf_completion_simplifier(m, s, p); });
} }

3
src/tactic/portfolio/euf_completion_tactic.h
View file

@ -40,10 +40,11 @@ class ast_manager;
class tactic; class tactic;
tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params_ref());
dependent_expr_simplifier* mk_euf_completion_simplifier(ast_manager& m, dependent_expr_state& s, params_ref const& p = params_ref());
/* /*
ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)") ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)")
ADD_SIMPLIFIER("euf-completion", "simplify modulo congruence closure.", "alloc(euf::completion, m, s)") ADD_SIMPLIFIER("euf-completion", "simplify modulo congruence closure.", "mk_euf_completion_simplifier(m, s, p)")
*/ */