mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

include nyis

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-12 18:00:43 -08:00
parent e49bfdb285
commit 9a933e29e3
3 changed files with 16 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -69,10 +69,11 @@ namespace polysat {
void undo() override { void undo() override {
auto& [sc, lit, val] = c.m_constraint_index.back(); auto& [sc, lit, val] = c.m_constraint_index.back();
auto& vars = sc.vars(); auto& vars = sc.vars();
IF_VERBOSE(10,
verbose_stream() << "undo add watch " << sc << " "; 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() > 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]] << ") "; if (vars.size() > 1) verbose_stream() << "(" << c.m_constraint_index.size() -1 << ": " << c.m_watch[vars[1]] << ") ";
verbose_stream() << "\n"; verbose_stream() << "\n");
SASSERT(vars.size() <= 0 || c.m_watch[vars[0]].back() == c.m_constraint_index.size() - 1); 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); SASSERT(vars.size() <= 1 || c.m_watch[vars[1]].back() == c.m_constraint_index.size() - 1);
if (vars.size() > 0) if (vars.size() > 0)
@ -141,10 +142,10 @@ namespace polysat {
add_watch(idx, vars[0]); add_watch(idx, vars[0]);
if (vars.size() > 1) if (vars.size() > 1)
add_watch(idx, vars[1]); add_watch(idx, vars[1]);
verbose_stream() << "add watch " << sc << " " << vars << " "; IF_VERBOSE(10, verbose_stream() << "add watch " << sc << " " << vars << " ";
if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") "; if (vars.size() > 0) verbose_stream() << "( " << idx << " : " << m_watch[vars[0]] << ") ";
if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") "; if (vars.size() > 1) verbose_stream() << "( " << idx << " : " << m_watch[vars[1]] << ") ";
verbose_stream() << "\n"; verbose_stream() << "\n");
s.trail().push(mk_add_watch(*this)); s.trail().push(mk_add_watch(*this));
return idx; return idx;
} }

9
src/sat/smt/polysat/op_constraint.cpp
View file

@ -42,6 +42,7 @@ namespace polysat {
break; break;
case code::inv_op: case code::inv_op:
SASSERT(q.is_zero()); SASSERT(q.is_zero());
break;
default: default:
break; break;
} }
@ -192,6 +193,9 @@ namespace polysat {
case code::lshr_op: case code::lshr_op:
propagate_lshr(c, dep); propagate_lshr(c, dep);
break; break;
case code::ashr_op:
propagate_ashr(c, dep);
break;
case code::shl_op: case code::shl_op:
propagate_shl(c, dep); propagate_shl(c, dep);
break; break;
@ -202,6 +206,7 @@ namespace polysat {
propagate_inv(c, dep); propagate_inv(c, dep);
break; break;
default: default:
verbose_stream() << "not implemented yet: " << *this << "\n";
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
} }
@ -311,6 +316,10 @@ namespace polysat {
} }
} }
void op_constraint::propagate_ashr(core& s, dependency const& dep) {
}
/** /**
* Enforce axioms for constraint: r == p << q * Enforce axioms for constraint: r == p << q

1
src/sat/smt/polysat/op_constraint.h
View file

@ -57,6 +57,7 @@ namespace polysat {
static lbool eval_inv(pdd const& p, pdd const& r); static lbool eval_inv(pdd const& p, pdd const& r);
void propagate_lshr(core& s, dependency const& dep); void propagate_lshr(core& s, dependency const& dep);
void propagate_ashr(core& s, dependency const& dep);
void propagate_shl(core& s, dependency const& dep); void propagate_shl(core& s, dependency const& dep);
void propagate_and(core& s, dependency const& dep); void propagate_and(core& s, dependency const& dep);
void propagate_inv(core& s, dependency const& dep); void propagate_inv(core& s, dependency const& dep);