From ecddaeae66378180423d93928992dfe53bba25c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Sep 2020 07:15:13 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.h | 7 ++++++ src/sat/sat_solver.cpp | 45 -------------------------------------- src/sat/sat_solver.h | 31 +++++++++++++------------- src/sat/smt/euf_solver.cpp | 7 ++++++ src/sat/smt/sat_th.h | 4 +++- src/util/id_var_list.h | 1 + 6 files changed, 33 insertions(+), 62 deletions(-) diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 72313a88a..19bee4a06 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -39,6 +39,13 @@ namespace euf { r1(r1), n1(n1), r2_num_parents(r2_num_parents) {} }; + /*** + \brief store derived theory equalities. + Theory 'id' is notified with the equality of theory variables v1, v2 + that are merged into the common root of child and root (their roots may + have been updated since the equality was derived, but the explanation for + v1 == v2 is provided by explaining the equality child == root. + */ struct th_eq { theory_id m_id; theory_var m_v1; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a8c2bf482..6bd5a50ea 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1602,7 +1602,6 @@ namespace sat { } lbool solver::bounded_search() { -#if 1 lbool is_sat = l_undef; while (is_sat == l_undef && !should_cancel()) { if (inconsistent()) is_sat = resolve_conflict_core(); @@ -1614,26 +1613,6 @@ namespace sat { else if (!decide()) is_sat = final_check(); } return is_sat; -#else - while (true) { - checkpoint(); - bool done = false; - while (!done) { - lbool is_sat = propagate_and_backjump_step(done); - if (is_sat != l_true) return is_sat; - } - - SASSERT(!inconsistent()); - do_gc(); - - if (!decide()) { - lbool is_sat = final_check(); - if (is_sat != l_undef) { - return is_sat; - } - } - } -#endif } bool solver::should_propagate() const { @@ -1641,30 +1620,6 @@ namespace sat { } - lbool solver::propagate_and_backjump_step(bool& done) { - done = true; - propagate(true); - if (!inconsistent()) { - return should_restart() ? l_undef : l_true; - } - if (!resolve_conflict()) - return l_false; - if (reached_max_conflicts()) - return l_undef; - if (should_rephase()) - do_rephase(); - if (at_base_lvl()) { - do_cleanup(false); // cleaner may propagate frozen clauses - if (inconsistent()) { - TRACE("sat", tout << "conflict at level 0\n";); - return l_false; - } - do_gc(); - } - done = false; - return l_true; - } - lbool solver::final_check() { if (m_ext) { switch (m_ext->check()) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index fcbe2140c..07871d43c 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -459,29 +459,28 @@ namespace sat { protected: - unsigned m_conflicts_since_init; - unsigned m_restarts; - unsigned m_restart_next_out; - unsigned m_conflicts_since_restart; - bool m_force_conflict_analysis; - unsigned m_simplifications; - unsigned m_restart_threshold; - unsigned m_luby_idx; - unsigned m_conflicts_since_gc; - unsigned m_gc_threshold; - unsigned m_defrag_threshold; - unsigned m_num_checkpoints; - double m_min_d_tk; - unsigned m_next_simplify; + unsigned m_conflicts_since_init { 0 }; + unsigned m_restarts { 0 }; + unsigned m_restart_next_out { 0 }; + unsigned m_conflicts_since_restart { 0 }; + bool m_force_conflict_analysis { false }; + unsigned m_simplifications { 0 }; + unsigned m_restart_threshold { 0 }; + unsigned m_luby_idx { 0 }; + unsigned m_conflicts_since_gc { 0 }; + unsigned m_gc_threshold { 0 }; + unsigned m_defrag_threshold { 0 }; + unsigned m_num_checkpoints { 0 }; + double m_min_d_tk { 0 } ; + unsigned m_next_simplify { 0 }; bool decide(); bool_var next_var(); lbool bounded_search(); lbool final_check(); - lbool propagate_and_backjump_step(bool& done); void init_search(); literal_vector m_min_core; - bool m_min_core_valid; + bool m_min_core_valid { false }; void init_reason_unknown() { m_reason_unknown = "no reason given"; } void init_assumptions(unsigned num_lits, literal const* lits); void reassert_min_core(); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 7b4b9e8c4..0680ea612 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -190,6 +190,8 @@ namespace euf { if (s().value(lit) == l_true) continue; s().assign(literal(v, false), sat::justification::mk_ext_justification(lvl, eq_constraint().to_index())); + if (s().inconsistent()) + return; } for (euf::enode* p : m_egraph.new_lits()) { expr* e = p->get_owner(); @@ -203,6 +205,11 @@ namespace euf { if (s().value(lit) == l_false && m_ackerman) m_ackerman->cg_conflict_eh(p->get_owner(), p->get_root()->get_owner()); s().assign(lit, sat::justification::mk_ext_justification(lvl, lit_constraint().to_index())); + if (s().inconsistent()) + return; + } + for (euf::th_eq const& eq : m_egraph.new_th_eqs()) { + // m_id2solver[eq.m_id]->new_eq_eh(eq); } } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 50fb246dc..2f3bd56f2 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -18,7 +18,7 @@ Author: #include "util/top_sort.h" #include "sat/smt/sat_smt.h" -#include "ast/euf/euf_enode.h" +#include "ast/euf/euf_egraph.h" namespace sat { @@ -63,6 +63,8 @@ namespace sat { virtual ~th_solver() {} virtual th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) = 0; + + virtual void new_eq_eh(euf::th_eq const& eq) {} }; diff --git a/src/util/id_var_list.h b/src/util/id_var_list.h index 6a795c616..4fe4ed091 100644 --- a/src/util/id_var_list.h +++ b/src/util/id_var_list.h @@ -21,6 +21,7 @@ Revision History: #pragma once #include "util/region.h" +#include "util/debug.h" template class id_var_list {