From 4de4618f5b2fad16418612d82f011e8cc78144f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 08:17:21 -0800 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 1 + src/sat/smt/intblast_solver.h | 2 +- src/sat/smt/polysat/constraints.h | 5 +++++ src/sat/smt/polysat/core.cpp | 34 ++++++++++++++++--------------- 4 files changed, 25 insertions(+), 17 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 729ad81e8..d0dd0b1c1 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -23,6 +23,7 @@ Author: #include "sat/smt/bv_solver.h" #include "sat/smt/intblast_solver.h" #include "sat/smt/polysat_solver.h" +#include "sat/smt/intblast_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/array_solver.h" #include "sat/smt/arith_solver.h" diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index 74683d0bf..2c0ebda28 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -109,7 +109,7 @@ namespace intblast { void translate_quantifier(quantifier* q); void translate_var(var* v); - void ensure_args(app* e); + void ensure_translated(expr* e); void internalize_bv(app* e); unsigned m_vars_qhead = 0; diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index a9ec63165..47c9beb49 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -31,12 +31,15 @@ namespace polysat { class constraint { unsigned_vector m_vars; + unsigned m_num_watch = 0; public: virtual ~constraint() {} unsigned_vector& vars() { return m_vars; } unsigned_vector const& vars() const { return m_vars; } unsigned var(unsigned idx) const { return m_vars[idx]; } bool contains_var(pvar v) const { return m_vars.contains(v); } + unsigned num_watch() const { return m_num_watch; } + void set_num_watch(unsigned n) { SASSERT(n <= 2); m_num_watch = n; } virtual std::ostream& display(std::ostream& out, lbool status) const = 0; virtual std::ostream& display(std::ostream& out) const = 0; virtual lbool eval() const = 0; @@ -63,6 +66,8 @@ namespace polysat { unsigned_vector const& vars() const { return m_constraint->vars(); } unsigned var(unsigned idx) const { return m_constraint->var(idx); } bool contains_var(pvar v) const { return m_constraint->contains_var(v); } + unsigned num_watch() const { return m_constraint->num_watch(); } + void set_num_watch(unsigned n) { m_constraint->set_num_watch(n); } void activate(core& c, dependency const& d) { m_constraint->activate(c, m_sign, d); } void propagate(core& c, lbool value, dependency const& d) { m_constraint->propagate(c, value, d); } bool is_always_true() const { return eval() == l_true; } diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp index de2fedb5a..c0b56a3d8 100644 --- a/src/sat/smt/polysat/core.cpp +++ b/src/sat/smt/polysat/core.cpp @@ -74,11 +74,13 @@ namespace polysat { if (vars.size() > 0) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[0]] << ") "; if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") "; verbose_stream() << "\n"); - SASSERT(vars.size() <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1); - SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1); - if (vars.size() > 0) + unsigned n = sc.num_watch(); + SASSERT(n <= vars.size()); + SASSERT(n <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1); + SASSERT(n <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1); + if (n > 0) c.m_watch[vars[0]].pop_back(); - if (vars.size() > 1) + if (n > 1) c.m_watch[vars[1]].pop_back(); c.m_constraint_index.pop_back(); } @@ -138,9 +140,10 @@ namespace polysat { for (; i < sz && j < 2; ++i) if (!is_assigned(vars[i])) std::swap(vars[i], vars[j++]); - if (vars.size() > 0) + sc.set_num_watch(i); + if (i > 0) add_watch(idx, vars[0]); - if (vars.size() > 1) + if (i > 1) add_watch(idx, vars[1]); IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << " "; if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") "; @@ -225,19 +228,12 @@ namespace polysat { s.trail().push(mk_assign_var(v, *this)); return; - // to debug: - unsigned sz = m_watch[v].size(); - for (unsigned i = 0; i < sz; ++i) { - auto idx = m_watch[v][i]; - auto [sc, dep, value] = m_constraint_index[idx]; - sc.propagate(*this, value, dep); - } - // update the watch lists for pvars // remove constraints from m_watch[v] that have more than 2 free variables. // for entries where there is only one free variable left add to viable set - unsigned j = 0; - for (auto idx : m_watch[v]) { + unsigned j = 0, sz = m_watch[v].size(); + for (unsigned k = 0; k < sz; ++k) { + auto idx = m_watch[v][k]; auto [sc, dep, value] = m_constraint_index[idx]; auto& vars = sc.vars(); if (vars[0] != v) @@ -253,6 +249,11 @@ namespace polysat { break; } } + + // this can create fresh literals and update m_watch, but + // will not update m_watch[v] (other than copy constructor for m_watch) + // because v has been assigned a value. + sc.propagate(*this, value, dep); SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1]))); if (swapped) @@ -267,6 +268,7 @@ namespace polysat { // detect unitary, add to viable, detect conflict? m_viable.add_unitary(v1, idx); } + SASSERT(m_watch[v].size() == sz && "size of watch list was not changed"); m_watch[v].shrink(j); verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n"; }