mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

minor

Browse source
This commit is contained in:
Jakob Rath 2022-09-29 18:25:28 +02:00
parent 8242069ba6
commit 9b907d709f
4 changed files with 23 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/conflict.cpp
View file

@ -287,7 +287,7 @@ namespace polysat {
if (c.is_always_true())
return;
LOG("Inserting " << lit_pp(s, c));
SASSERT(c.bvalue(s) == l_true);
SASSERT_EQ(c.bvalue(s), l_true);
SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology
SASSERT(!c->vars().empty());
m_literals.insert(c.blit().index());

2
src/math/polysat/saturation.cpp
View file

@ -102,7 +102,7 @@ namespace polysat {
core.insert_eval(d);
if (c.bvalue(s) != l_false) // conflict is due to the evaluation of c, so it depends on the variable values
core.insert_vars(c);
core.insert(~c);
core.insert_eval(~c);
core.set_backjump();
core.logger().log(inf_name);
LOG("Core " << core);

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

@ -246,6 +246,7 @@ namespace polysat {
*/
void solver::propagate(sat::literal lit) {
LOG_H2("Propagate bool " << lit << "@" << m_bvars.level(lit) << " " << m_level << " qhead: " << m_qhead);
LOG("Literal " << lit_pp(*this, lit));
signed_constraint c = lit2cnstr(lit);
SASSERT(c);
// TODO: review active and activate_constraint
@ -471,6 +472,7 @@ namespace polysat {
case trail_instr_t::pwatch_i: {
constraint* c = m_pwatch_trail.back();
erase_pwatch(c);
c->set_active(false); // TODO: review meaning of "active"
m_pwatch_trail.pop_back();
break;
}
@ -789,7 +791,7 @@ namespace polysat {
*/
void solver::revert_decision(pvar v) {
rational val = m_value[v];
LOG_H3("Reverting decision: pvar " << v << " := " << val);
LOG_H2("Reverting decision: pvar " << v << " := " << val);
SASSERT(m_justification[v].is_decision());
clause_ref lemma = m_conflict.build_lemma();
@ -1015,6 +1017,10 @@ namespace polysat {
}
if (c->is_pwatched())
out << " pwatched";
if (c->is_active())
out << " active";
if (c->is_external())
out << " ext";
out << " ]";
return out;
}
@ -1087,8 +1093,8 @@ namespace polysat {
}
unsigned expected_watches = std::min(2u, c->vars().size());
if (num_watches != expected_watches)
LOG("wrong number of watches: " << sc.blit() << ": " << sc << " (vars: " << sc->vars() << ")");
SASSERT_EQ(num_watches, expected_watches);
LOG("Wrong number of watches: " << sc.blit() << ": " << sc << " (vars: " << sc->vars() << ")");
VERIFY_EQ(num_watches, expected_watches);
}
return true;
}

15
src/test/polysat.cpp
View file

@ -232,6 +232,14 @@ namespace polysat {
s.expect_sat({{a, 4}, {b, 4}});
}
static void test_l6() {
scoped_solver s(__func__);
auto x = s.var(s.add_var(6));
s.add_ule(29*x + 3, 29*x + 1);
s.check();
s.expect_sat();
}
/**
* This one is unsat because a*a*(a*a - 1)
* is 0 for all values of a.
@ -1404,7 +1412,7 @@ void tst_polysat() {
// test_polysat::test_add_conflicts(); // ok
// test_polysat::test_wlist(); // ok
// test_polysat::test_cjust(); // uses viable_fallback; weak lemmas
// test_polysat::test_subst(); // TODO: assert + resource limit
// test_polysat::test_subst(); // TODO: resource limit; needs polynomial superposition
// test_polysat::test_pop_conflict(); // ok now (had bad conflict/pop interaction)
// test_polysat::test_l1(); // ok
@ -1413,13 +1421,14 @@ void tst_polysat() {
// test_polysat::test_l4(); // ok now (had assertion failure in conflict::insert)
// test_polysat::test_l4b(); // ok
// test_polysat::test_l5(); // inefficient conflicts (needs equality reasoning)
// test_polysat::test_l6(); // ok (refine-equal-lin)
// test_polysat::test_p1(); // ok (conflict @0 by viable_fallback)
// test_polysat::test_p2(); // ok (viable_fallback finds the correct value)
// test_polysat::test_p3(); // TODO: resource limit
// test_polysat::test_ineq_basic1(); // ok
// test_polysat::test_ineq_basic2(); // TODO: assert / boolean conflict
// test_polysat::test_ineq_basic2(); // ok
// test_polysat::test_ineq_basic3(); // ok
// test_polysat::test_ineq_basic4(); // TODO: resource limit
// test_polysat::test_ineq_basic5(); // works, but only because variable order changes after the conflict
@ -1436,7 +1445,7 @@ void tst_polysat() {
// test_polysat::test_monot_bounds(2); // weak conflicts
// test_polysat::test_monot_bounds(8);
// test_polysat::test_monot_bounds(); // TODO: resource limit
// test_polysat::test_monot_bounds_full(); // TODO: triggers assertion in watchlist invariant
// test_polysat::test_monot_bounds_full(); // TODO: triggers assertion in watchlist invariant -- it's a problem with push/pop and that the "active" flag isn't maintained properly
// test_polysat::test_monot_bounds_simple(8); // undef
// test_polysat::test_fixed_point_arith_div_mul_inverse(); // undef