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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-14 22:03:28 -07:00
parent 034132d245
commit 9a2b7677bf
3 changed files with 20 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/dd/dd_pdd.cpp
View file

@ -240,9 +240,8 @@ namespace dd {
break; break;
case pdd_subst_val_op: case pdd_subst_val_op:
while (!is_val(q) && !is_val(p)) { while (!is_val(q) && !is_val(p)) {
if (level(p) == level(q)) break;
if (level(p) < level(q)) q = lo(q); if (level(p) < level(q)) q = lo(q);
else p = lo(p); else break;
} }
if (is_val(p) || is_val(q)) return p; if (is_val(p) || is_val(q)) return p;
break; break;
@ -388,12 +387,19 @@ namespace dd {
case pdd_subst_val_op: case pdd_subst_val_op:
SASSERT(!is_val(p)); SASSERT(!is_val(p));
SASSERT(!is_val(q)); SASSERT(!is_val(q));
SASSERT(level_p == level_q); SASSERT(level_p >= level_q);
push(apply_rec(lo(p), q, pdd_subst_val_op)); // lo := subst(lo(p), s) push(apply_rec(lo(p), q, pdd_subst_val_op)); // lo := subst(lo(p), s)
push(apply_rec(hi(p), q, pdd_subst_val_op)); // hi := subst(hi(p), s) push(apply_rec(hi(p), q, pdd_subst_val_op)); // hi := subst(hi(p), s)
if (level_p > level_q) {
r = make_node(level_p, read(2), read(1));
npop = 2;
}
else {
push(apply_rec(lo(q), read(1), pdd_mul_op)); // hi := hi*s[var(p)] push(apply_rec(lo(q), read(1), pdd_mul_op)); // hi := hi*s[var(p)]
r = apply_rec(read(1), read(3), pdd_add_op); // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s) r = apply_rec(read(1), read(3), pdd_add_op); // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s)
npop = 3; npop = 3;
}
break; break;
default: default:
r = null_pdd; r = null_pdd;

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

@ -220,9 +220,9 @@ namespace polysat {
return false; return false;
} }
// one variable remains unassigned. // at most one variable remains unassigned.
auto other_var = vars[1 - idx]; auto other_var = vars[1 - idx];
SASSERT(!is_assigned(other_var)); // SASSERT(!is_assigned(other_var));
// Detect and apply unit propagation. // Detect and apply unit propagation.
@ -364,12 +364,14 @@ namespace polysat {
void solver::set_conflict(constraint& c) { void solver::set_conflict(constraint& c) {
SASSERT(m_conflict.empty()); SASSERT(m_conflict.empty());
TRACE("polysat", tout << "conflict " << c << "\n";);
m_conflict.push_back(&c); m_conflict.push_back(&c);
} }
void solver::set_conflict(pvar v) { void solver::set_conflict(pvar v) {
SASSERT(m_conflict.empty()); SASSERT(m_conflict.empty());
m_conflict.append(m_cjust[v]); m_conflict.append(m_cjust[v]);
TRACE("polysat", tout << "conflict "; for (auto* c : m_conflict) tout << *c << "\n";);
if (m_cjust[v].empty()) if (m_cjust[v].empty())
m_conflict.push_back(nullptr); m_conflict.push_back(nullptr);
} }

3
src/test/polysat.cpp
View file

@ -37,6 +37,9 @@ namespace polysat {
s.check(); s.check();
} }
// TBD: we get the wrong result / conflicts.
// it claims that v1 + 2*v0 + 1 with v0 replaced by 0 is 1.
// it should be v1 + 1
static void test_l2() { static void test_l2() {
scoped_solver s; scoped_solver s;
auto a = s.var(s.add_var(2)); auto a = s.var(s.add_var(2));