mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-12 16:37:39 -08:00
parent c663d28201
commit e49bfdb285
4 changed files with 30 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/intblast_solver.h
View file

@ -95,7 +95,7 @@ namespace intblast {
void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
void set_translated(expr* e, expr* r) { m_translate.setx(e->get_id(), r); }
void set_translated(expr* e, expr* r) { SASSERT(r); m_translate.setx(e->get_id(), r); }
expr* arg(unsigned i) { return m_args.get(i); }
expr* umod(expr* bv_expr, unsigned i);

27
src/sat/smt/polysat/core.cpp
View file

@ -66,9 +66,15 @@ namespace polysat {
core& c;
public:
mk_add_watch(core& c) : c(c) {}
void undo() override {
void undo() override {
auto& [sc, lit, val] = c.m_constraint_index.back();
auto& vars = sc.vars();
verbose_stream() << "undo add watch " << sc << " ";
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)
c.m_watch[vars[0]].pop_back();
if (vars.size() > 1)
@ -135,6 +141,10 @@ namespace polysat {
add_watch(idx, vars[0]);
if (vars.size() > 1)
add_watch(idx, vars[1]);
verbose_stream() << "add watch " << sc << " " << vars << " ";
if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
verbose_stream() << "\n";
s.trail().push(mk_add_watch(*this));
return idx;
}
@ -213,6 +223,15 @@ namespace polysat {
m_assignment.push(v , value);
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
@ -226,15 +245,14 @@ namespace polysat {
bool swapped = false;
for (unsigned i = vars.size(); i-- > 2; ) {
if (!is_assigned(vars[i])) {
verbose_stream() << "watch instead " << idx << " " << vars[i] << "instead of " << vars[0] << "\n";
add_watch(idx, vars[i]);
std::swap(vars[i], vars[0]);
swapped = true;
break;
}
}
sc.propagate(*this, value, dep);
SASSERT(!swapped || vars.size() <= 1 || (!is_assigned(vars[0]) && !is_assigned(vars[1])));
if (swapped)
continue;
@ -249,6 +267,7 @@ namespace polysat {
m_viable.add_unitary(v1, idx);
}
m_watch[v].shrink(j);
verbose_stream() << "new watch " << v << ": " << m_watch[v] << "\n";
}
void core::propagate_value(prop_item const& dc) {

2
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -75,8 +75,6 @@ Useful lemmas:
#include "sat/smt/polysat/constraints.h"
#include "sat/smt/polysat/ule_constraint.h"
#define LOG(_msg_) verbose_stream() << _msg_ << "\n"
namespace polysat {
// Simplify lhs <= rhs.

7
src/sat/smt/polysat_solver.cpp
View file

@ -138,6 +138,10 @@ namespace polysat {
for (auto lit : lits)
level = std::max(level, s().lvl(lit));
auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
if (level == 0) {
ctx.set_conflict(ex);
return;
}
ctx.push(value_trail<bool>(m_has_lemma));
m_has_lemma = true;
m_lemma_level = level;
@ -165,7 +169,8 @@ namespace polysat {
if (!m_has_lemma)
return l_undef;
unsigned num_scopes = s().scope_lvl() - m_lemma_level;
SASSERT(m_lemma_level > 0);
unsigned num_scopes = s().scope_lvl() - m_lemma_level - 1;
NOT_IMPLEMENTED_YET();
// s().pop_reinit(num_scopes);