mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

some fixes

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 15:09:50 +02:00
parent cf80225fee
commit e5289f84a0
5 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/conflict_core.cpp
View file

@ -149,6 +149,7 @@ namespace polysat {
if (c->contains_var(v)) if (c->contains_var(v))
unset_mark(c); unset_mark(c);
} }
m_vars.remove(v);
} }
void conflict_core::set_bailout() { void conflict_core::set_bailout() {
@ -366,6 +367,10 @@ namespace polysat {
return m_bvar2mark.get(b, false); return m_bvar2mark.get(b, false);
} }
bool conflict_core::contains_literal(sat::literal lit) const {
return m_literals.contains(lit.to_uint());
}
void conflict_core::insert_literal(sat::literal lit) { void conflict_core::insert_literal(sat::literal lit) {
m_literals.insert(lit.to_uint()); m_literals.insert(lit.to_uint());
} }

1
src/math/polysat/conflict_core.h
View file

@ -45,6 +45,7 @@ namespace polysat {
void set_mark(signed_constraint c); void set_mark(signed_constraint c);
void unset_mark(signed_constraint c); void unset_mark(signed_constraint c);
bool contains_literal(sat::literal lit) const;
void insert_literal(sat::literal lit); void insert_literal(sat::literal lit);
void remove_literal(sat::literal lit); void remove_literal(sat::literal lit);

4
src/math/polysat/search_state.cpp
View file

@ -19,9 +19,9 @@ namespace polysat {
std::ostream& search_item::display(std::ostream& out) const { std::ostream& search_item::display(std::ostream& out) const {
switch (kind()) { switch (kind()) {
case search_item_k::assignment: case search_item_k::assignment:
return out << "assignment(v" << var() << ")"; return out << "v" << var() << "=?";
case search_item_k::boolean: case search_item_k::boolean:
return out << "boolean(" << lit() << ")"; return out << lit();
} }
UNREACHABLE(); UNREACHABLE();
return out; return out;

4
src/math/polysat/solver.cpp
View file

@ -210,14 +210,14 @@ namespace polysat {
} }
void solver::propagate(sat::literal lit) { void solver::propagate(sat::literal lit) {
LOG_H2("Propagate boolean literal " << lit); LOG_H2("Propagate bool " << lit);
signed_constraint c = m_constraints.lookup(lit); signed_constraint c = m_constraints.lookup(lit);
SASSERT(c); SASSERT(c);
activate_constraint(c); activate_constraint(c);
} }
void solver::propagate(pvar v) { void solver::propagate(pvar v) {
LOG_H2("Propagate pvar " << v); LOG_H2("Propagate v" << v);
auto& wlist = m_watch[v]; auto& wlist = m_watch[v];
unsigned i = 0, j = 0, sz = wlist.size(); unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i) for (; i < sz && !is_conflict(); ++i)

7
src/math/polysat/ule_constraint.cpp
View file

@ -50,14 +50,13 @@ namespace polysat {
// p <= 0, e.g., p == 0 // p <= 0, e.g., p == 0
if (q.is_zero() && p.is_unilinear()) { if (q.is_zero() && p.is_unilinear()) {
// a*x + b == 0 // a*x + b == 0
pvar v = q.var(); pvar v = p.var();
s.push_cjust(v, { this, is_positive }); s.push_cjust(v, { this, is_positive });
rational a = q.hi().val(); rational a = p.hi().val();
rational b = q.lo().val(); rational b = p.lo().val();
s.m_viable.intersect_eq(a, v, b, is_positive); s.m_viable.intersect_eq(a, v, b, is_positive);
rational val; rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton) if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, { this, is_positive }); s.propagate(v, val, { this, is_positive });