From ffd43235735b1731ff272250723b078dbf8c2d85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Jun 2023 22:24:55 +0200 Subject: [PATCH] experiment with delayed disequalities Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 2 +- src/sat/smt/q_solver.cpp | 34 ++++++++++++++++++++++- src/sat/smt/q_solver.h | 2 ++ src/smt/theory_arith_core.h | 1 - src/smt/theory_lra.cpp | 54 ++++++++++++++++++++++++++++++++++--- 5 files changed, 86 insertions(+), 7 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 0ae56beb3..0180fcc60 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -172,7 +172,7 @@ namespace euf { IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n"); } - void solver::init_search() { + void solver::init_search() { TRACE("before_search", s().display(tout);); m_reason_unknown.clear(); for (auto* s : m_solvers) diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index fff11898c..f49611660 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -45,10 +45,15 @@ namespace q { quantifier* q = to_quantifier(e); if (l.sign() == is_forall(e)) { + if (m_quantifiers_are_positive && is_forall(e)) + return; sat::literal lit = skolemize(q); add_clause(~l, lit); return; } + if (m_quantifiers_are_positive && is_exists(e)) + return; + quantifier* q_flat = nullptr; if (!m_flat.find(q, q_flat)) { if (expand(q)) { @@ -141,10 +146,37 @@ namespace q { return mk_literal(body); } + class insert_skolem : public trail { + obj_map& sk; + quantifier* q; + public: + insert_skolem(obj_map& sk, quantifier* q): + sk(sk), + q(q) + {} + void undo() override { + dealloc(sk[q]); + sk.remove(q); + } + }; + sat::literal solver::skolemize(quantifier* q) { + expr_ref_vector* sk = nullptr; std::function mk_var = [&](quantifier* q, unsigned i) { - return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i)); + expr * t = nullptr; + if (sk->size() <= i) { + t = m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i)); + sk->push_back(t); + } + else + t = sk->get(i); + return t; }; + if (!m_skolems.find(q, sk)) { + sk = alloc(expr_ref_vector, m); + m_skolems.insert(q, sk); + ctx.push(insert_skolem(m_skolems, q)); + } return instantiate(q, is_forall(q), mk_var); } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index d0581f852..2433955db 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -68,6 +68,8 @@ namespace q { obj_map m_unit_table; expr_ref_vector m_expanded; der_rewriter m_der; + bool m_quantifiers_are_positive = false; + obj_map m_skolems; sat::literal instantiate(quantifier* q, bool negate, std::function& mk_var); sat::literal skolemize(quantifier* q); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 6f0820ca7..2e111fa99 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1466,7 +1466,6 @@ namespace smt { template void theory_arith::restart_eh() { - return; m_arith_eq_adapter.restart_eh(); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bdb396916..3b7494cba 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1304,17 +1304,60 @@ public: TRACE("arith", tout << "eq " << v1 << " == " << v2 << "\n";); if (!is_int(v1) && !is_real(v1)) return; - m_arith_eq_adapter.new_eq_eh(v1, v2); + + if (true) { + enode* n1 = get_enode(v1); + enode* n2 = get_enode(v2); + lpvar w1 = register_theory_var_in_lar_solver(v1); + lpvar w2 = register_theory_var_in_lar_solver(v2); + auto cs = lp().add_equality(w1, w2); + add_eq_constraint(cs.first, n1, n2); + add_eq_constraint(cs.second, n1, n2); + } + else { + m_arith_eq_adapter.new_eq_eh(v1, v2); + } } bool use_diseqs() const { return true; } + svector> m_diseqs; + unsigned m_diseqs_qhead = 0; + void new_diseq_eh(theory_var v1, theory_var v2) { TRACE("arith", tout << "v" << v1 << " != " << "v" << v2 << "\n";); ++m_stats.m_assert_diseq; - m_arith_eq_adapter.new_diseq_eh(v1, v2); + if (false) { + if (is_eq(v1, v2)) { + m_arith_eq_adapter.new_diseq_eh(v1, v2); + } + else { + m_diseqs.push_back({v1, v2}); + ctx().push_trail(push_back_vector(m_diseqs)); + } + } + else + m_arith_eq_adapter.new_diseq_eh(v1, v2); + } + + bool delayed_diseqs() { + if (m_diseqs_qhead == m_diseqs.size()) + return false; + verbose_stream() << m_diseqs_qhead << " out of " << m_diseqs.size() << "\n"; + ctx().push_trail(value_trail(m_diseqs_qhead)); + bool has_eq = false; + while (m_diseqs_qhead < m_diseqs.size()) { + auto [v1,v2] = m_diseqs[m_diseqs_qhead]; + if (is_eq(v1, v2)) { + verbose_stream() << "bad diseq " << m_diseqs_qhead << "\n"; + m_arith_eq_adapter.new_diseq_eh(v1, v2); + has_eq = true; + } + ++m_diseqs_qhead; + } + return has_eq; } void apply_sort_cnstr(enode* n, sort*) { @@ -1361,7 +1404,6 @@ public: } void restart_eh() { - return; m_arith_eq_adapter.restart_eh(); } @@ -1800,6 +1842,10 @@ public: TRACE("arith", display(tout);); random_update(); m_model_eqs.reset(); + + if (delayed_diseqs()) + return true; + theory_var sz = static_cast(th.get_num_vars()); unsigned old_sz = m_assume_eq_candidates.size(); @@ -1943,7 +1989,7 @@ public: final_check_status final_check_eh() { - // verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n"; + // verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n"; //ctx().display(verbose_stream()); //exit(0);