From 564830ab3136919568237db830f57bd800cc97d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jun 2025 11:42:31 +0200 Subject: [PATCH] enable conditional euf-completion with (optional) solver This allows using z3 for limited E-saturation simplification. The tactic rewrites all assertions using the E-graph induced by the equalities and instantiated equality axioms. It does allow solving with conditionals, although this is a first inefficient cut. The following is a sample use case that rewrites to false. ``` (declare-fun prime () Int) (declare-fun add (Int Int) Int) (declare-fun mul (Int Int) Int) (declare-fun ^ (Int Int) Int) (declare-fun sub (Int Int) Int) (declare-fun i () Int) (declare-fun j () Int) (declare-fun base () Int) (declare-fun S () (Seq Int)) (declare-fun hash ((Seq Int) Int Int Int Int) Int) (assert (let ((a!1 (mul (seq.nth S i) (^ base (sub (sub j i) 1))))) (let ((a!2 (mod (add (hash S base prime (add i 1) j) a!1) prime))) (not (= (hash S base prime i j) a!2))))) (assert (forall ((x Int)) (! (= (mod (mod x prime) prime) (mod x prime)) :pattern ((mod (mod x prime) prime))))) (assert (forall ((x Int) (y Int)) (! (= (mod (mul x y) prime) (mod (mul (mod x prime) y) prime)) :pattern ((mod (mul x y) prime)) :pattern ((mod (mul (mod x prime) y) prime))))) (assert (forall ((x Int) (y Int)) (! (= (mod (mul x y) prime) (mod (mul x (mod y prime)) prime)) :pattern ((mod (mul x y) prime)) :pattern ((mod (mul x (mod y prime)) prime))))) (assert (forall ((x Int) (y Int)) (! (= (mod (add x y) prime) (mod (add x (mod y prime)) prime)) :pattern ((mod (add x y) prime)) :pattern ((mod (add x (mod y prime)) prime))))) (assert (forall ((x Int) (y Int)) (! (= (mod (add x y) prime) (mod (add (mod x prime) y) prime)) :pattern ((mod (add x y) prime)) :pattern ((mod (add (mod x prime) y) prime))))) (assert (forall ((x Int) (y Int)) (! (= (mul x (^ x y)) (^ x (add y 1))) :pattern ((mul x (^ x y)))))) (assert (forall ((x Int) (y Int)) (! (= (mul x y) (mul y x)) :pattern ((mul x y))))) (assert (forall ((x Int) (y Int)) (! (= (add x y) (add y x)) :pattern ((add x y))))) (assert (forall ((x Int) (y Int)) (! (= (mul x y) (mul y x)) :pattern ((mul x y))))) (assert (forall ((x Int) (y Int) (z Int)) (! (= (add x (add y z)) (add (add x y) z)) :pattern ((add x (add y z))) :pattern ((add (add x y) z))))) (assert (forall ((x Int) (y Int) (z Int)) (! (= (mul x (mul y z)) (mul (mul x y) z)) :pattern ((mul x (mul y z))) :pattern ((mul (mul x y) z))))) (assert (forall ((x Int) (y Int) (z Int)) (! (= (sub (sub x y) z) (sub (sub x z) y)) :pattern ((sub (sub x y) z))))) (assert (forall ((x Int) (y Int) (z Int)) (! (= (mul x (add y z)) (add (mul x y) (mul x z))) :pattern ((mul x (add y z)))))) (assert (forall ((x Int)) (! (= (sub (add x 1) 1) x) :pattern ((add x 1))))) (assert (forall ((x Int)) (! (= (add (sub x 1) 1) x) :pattern ((sub x 1))))) (assert (let ((a!1 (^ base (sub (sub (sub j 1) i) 1)))) (let ((a!2 (mod (add (hash S base prime (add i 1) (sub j 1)) (mul (seq.nth S i) a!1)) prime))) (= (hash S base prime i (sub j 1)) a!2)))) (assert (let ((a!1 (add (seq.nth S (- j 1)) (mul base (hash S base prime i (sub j 1)))))) (= (hash S base prime i j) (mod a!1 prime)))) (assert (let ((a!1 (add (seq.nth S (- j 1)) (mul base (hash S base prime (add i 1) (sub j 1)))))) (= (hash S base prime (add i 1) j) (mod a!1 prime)))) (apply euf-completion) ``` To use conditional rewriting you can ``` (assert (not (= 0 prime))) ``` and update axioms using modulus with prime to be of the form: ``` (=> (not (= 0 prime)) ) ``` --- src/ast/simplifiers/euf_completion.h | 29 ++++++- src/tactic/core/CMakeLists.txt | 2 - src/tactic/core/euf_completion_tactic.cpp | 24 ------ src/tactic/portfolio/CMakeLists.txt | 2 + .../portfolio/euf_completion_tactic.cpp | 79 +++++++++++++++++++ .../euf_completion_tactic.h | 0 6 files changed, 109 insertions(+), 27 deletions(-) delete mode 100644 src/tactic/core/euf_completion_tactic.cpp create mode 100644 src/tactic/portfolio/euf_completion_tactic.cpp rename src/tactic/{core => portfolio}/euf_completion_tactic.h (100%) diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index 4f07578ef..5e9f675cb 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -17,6 +17,7 @@ Author: #pragma once +#include "util/scoped_vector.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/euf/euf_egraph.h" #include "ast/euf/euf_mam.h" @@ -24,6 +25,13 @@ Author: namespace euf { + class side_condition_solver { + public: + virtual ~side_condition_solver() = default; + virtual void add_constraint(expr* f, expr_dependency* d) = 0; + virtual bool is_true(expr* f, expr_dependency*& d) = 0; + }; + class completion : public dependent_expr_simplifier, public on_binding_callback, public mam_solver { struct stats { @@ -32,6 +40,14 @@ namespace euf { void reset() { memset(this, 0, sizeof(*this)); } }; + struct ground_rule { + expr_ref_vector m_body; + expr_ref m_head; + expr_dependency* m_dep; + ground_rule(expr_ref_vector& b, expr_ref& h, expr_dependency* d) : + m_body(b), m_head(h), m_dep(d) {} + }; + egraph m_egraph; scoped_ptr m_mam; enode* m_tt, *m_ff; @@ -44,10 +60,11 @@ namespace euf { unsigned_vector m_epochs; th_rewriter m_rewriter; stats m_stats; + scoped_ptr m_side_condition_solver; + ptr_vector m_rules; bool m_has_new_eq = false; bool m_should_propagate = false; - enode* mk_enode(expr* e); bool is_new_eq(expr* a, expr* b); void update_has_new_eq(expr* g); @@ -65,9 +82,17 @@ namespace euf { expr_dependency* explain_conflict(); expr_dependency* get_dependency(quantifier* q) { return m_q2dep.contains(q) ? m_q2dep[q] : nullptr; } + lbool eval_cond(expr* f, expr_dependency*& d); + + lbool check_rule(ground_rule& rule); + void check_rules(); + void add_rule(expr* f, expr_dependency* d); + void reset_rules(); + bool is_gt(expr* a, expr* b) const; public: completion(ast_manager& m, dependent_expr_state& fmls); + ~completion() override; char const* name() const override { return "euf-reduce"; } void push() override { m_egraph.push(); dependent_expr_simplifier::push(); } void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); } @@ -84,5 +109,7 @@ namespace euf { void on_binding(quantifier* q, app* pat, enode* const* binding, unsigned mg, unsigned ming, unsigned mx) override; + void set_solver(side_condition_solver* s) { m_side_condition_solver = s; } + }; } diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 0827c12fb..a191b6251 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -8,7 +8,6 @@ z3_add_component(core_tactics der_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp - euf_completion_tactic.cpp injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp @@ -38,7 +37,6 @@ z3_add_component(core_tactics elim_uncnstr_tactic.h elim_uncnstr2_tactic.h eliminate_predicates_tactic.h - euf_completion_tactic.h injectivity_tactic.h nnf_tactic.h occf_tactic.h diff --git a/src/tactic/core/euf_completion_tactic.cpp b/src/tactic/core/euf_completion_tactic.cpp deleted file mode 100644 index af2ca9ed7..000000000 --- a/src/tactic/core/euf_completion_tactic.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/*++ -Copyright (c) 2022 Microsoft Corporation - -Module Name: - - euf_completion_tactic.cpp - -Abstract: - - Tactic for simplifying with equations. - -Author: - - Nikolaj Bjorner (nbjorner) 2022-10-30 - ---*/ - -#include "tactic/tactic.h" -#include "tactic/core/euf_completion_tactic.h" - -tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, - [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::completion, m, s); }); -} diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 6e954717f..bd927d4fc 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -1,5 +1,6 @@ z3_add_component(portfolio SOURCES + euf_completion_tactic.cpp default_tactic.cpp smt_strategic_solver.cpp solver2lookahead.cpp @@ -16,6 +17,7 @@ z3_add_component(portfolio ufbv_tactic fd_solver TACTIC_HEADERS + euf_completion_tactic.h default_tactic.h solver_subsumption_tactic.h diff --git a/src/tactic/portfolio/euf_completion_tactic.cpp b/src/tactic/portfolio/euf_completion_tactic.cpp new file mode 100644 index 000000000..b8784d8f5 --- /dev/null +++ b/src/tactic/portfolio/euf_completion_tactic.cpp @@ -0,0 +1,79 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + euf_completion_tactic.cpp + +Abstract: + + Tactic for simplifying with equations. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-10-30 + +--*/ + +#include "tactic/tactic.h" +#include "tactic/portfolio/euf_completion_tactic.h" +#include "solver/solver.h" + +class euf_side_condition_solver : public euf::side_condition_solver { + ast_manager& m; + params_ref m_params; + scoped_ptr m_solver; + expr_ref_vector m_deps; + obj_map m_e2d; + void init_solver() { + if (m_solver.get()) + return; + m_params.set_uint("smt.max_conflicts", 100); + scoped_ptr f = mk_smt_strategic_solver_factory(); + m_solver = (*f)(m, m_params, false, false, true, symbol::null); + } +public: + euf_side_condition_solver(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_deps(m) {} + + void add_constraint(expr* f, expr_dependency* d) override { + if (!is_ground(f)) + return; + init_solver(); + expr* e_dep = nullptr; + if (d) { + e_dep = m.mk_fresh_const("dep", m.mk_bool_sort()); + m_deps.push_back(e_dep); + m_e2d.insert(e_dep, d); + } + m_solver->assert_expr(f, e_dep); + } + + bool is_true(expr* f, expr_dependency*& d) override { + d = nullptr; + m_solver->push(); + expr_ref_vector fmls(m); + fmls.push_back(m.mk_not(f)); + expr_ref nf(m.mk_not(f), m); + lbool r = m_solver->check_sat(fmls); + if (r == l_false) { + expr_ref_vector core(m); + m_solver->get_unsat_core(core); + for (auto c : core) + d = m.mk_join(d, m_e2d[c]); + } + m_solver->pop(1); + return r == l_false; + } +}; + +static euf::completion* mk_completion(ast_manager& m, dependent_expr_state& s, params_ref const& p) { + auto r = alloc(euf::completion, m, s); + auto scs = alloc(euf_side_condition_solver, m, p); + r->set_solver(scs); + return r; +} + +tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::completion, m, s); }); +} diff --git a/src/tactic/core/euf_completion_tactic.h b/src/tactic/portfolio/euf_completion_tactic.h similarity index 100% rename from src/tactic/core/euf_completion_tactic.h rename to src/tactic/portfolio/euf_completion_tactic.h