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

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-03-29 09:58:46 -07:00
commit 8cefa02b0d
11 changed files with 105 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/boolean.cpp
View file

@ -135,18 +135,22 @@ namespace polysat {
}
/**
* A literal may be watched if there is no unwatched literal that has been assigned later,
* where true and unassigned literals are considered at infinite level.
* We prefer true literals to unassigned literals.
* Priority for watching literals:
* 1. true literal, prefer lower search index to keep clause inactive for as long as possible.
* 2. unassigned literal
* 3. false literal, prefer higher search index (otherwise we might miss boolean propagations)
*/
uint64_t bool_var_manager::get_watch_level(sat::literal lit) const {
switch (value(lit)) {
case l_false:
return s.m_search.get_bool_index(lit);
case l_true:
return std::numeric_limits<uint64_t>::max();
case l_undef:
return std::numeric_limits<uint64_t>::max() - 1;
case l_true:
// 0xFFFF'FFFF'****'****
return 0xFFFF'FFFF'FFFF'FFFFull - s.m_search.get_bool_index(lit);
case l_undef:
// 0x0FFF'FFFF'FFFF'FFFF
return 0x0FFF'FFFF'FFFF'FFFFull;
case l_false:
// 0x0000'0000'****'****
return s.m_search.get_bool_index(lit);
}
UNREACHABLE();
return 0;

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

@ -276,9 +276,10 @@ namespace polysat {
SASSERT(!s.is_assigned(v));
m_level = s.m_level;
logger().begin_conflict(header_with_var("viable_interval v", v));
VERIFY(s.m_viable.resolve_interval(v, *this));
if (s.m_viable.resolve_interval(v, *this)) {
revert_pvar(v); // at this point, v is not assigned
}
SASSERT(!empty());
revert_pvar(v); // at this point, v is not assigned
}
void conflict::init_by_viable_fallback(pvar v, univariate_solver& us) {
@ -319,6 +320,7 @@ namespace polysat {
}
bool conflict::insert_or_replace(signed_constraint c) {
// TODO: what if we have already passed c in the trail in resolve_conflict? should check that. (probably restart the resolve_conflict loop with the new conflict?)
switch (c.bvalue(s)) {
case l_true:
// regular case

16
src/math/polysat/constraint_manager.cpp
View file

@ -397,12 +397,12 @@ namespace polysat {
// b = 0 ==> q = -1
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
// Maybe we need something like an op_constraint for better propagation.
s.add_clause(eq(b * q + r - a), false);
s.add_clause(~umul_ovfl(b, q), false);
s.add_clause("[axiom] quot_rem 1", { eq(b * q + r - a) }, false);
s.add_clause("[axiom] quot_rem 2", { ~umul_ovfl(b, q) }, false);
// r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1
s.add_clause(ule(b*q, -r-1), false);
s.add_clause("[axiom] quot_rem 3", { ule(b*q, -r-1) }, false);
#if 0
// b*q <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
@ -411,8 +411,8 @@ namespace polysat {
#endif
auto c_eq = eq(b);
s.add_clause(c_eq, ult(r, b), false);
s.add_clause(~c_eq, eq(q + 1), false);
s.add_clause("[axiom] quot_rem 4", { c_eq, ult(r, b) }, false);
s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1) }, false);
return {std::move(q), std::move(r)};
}
@ -523,9 +523,15 @@ namespace polysat {
}
pdd constraint_manager::bor(pdd const& p, pdd const& q) {
#if 1
// From "Hacker's Delight", section 2-2. Addition Combined with Logical Operations;
// found via Int-Blasting paper; see https://doi.org/10.1007/978-3-030-94583-1_24
return (p + q) - band(p, q);
#else
// Alternatively, de Morgan:
// (advantage: only one occurrence of p, q)
return bnot(band(bnot(p), bnot(q)));
#endif
}
pdd constraint_manager::bxor(pdd const& p, pdd const& q) {

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

@ -25,7 +25,7 @@ Other:
*/
/*
TODO: add "conditional" logs, i.e., the messages are held back and only printed when a non-conditional message is logged.
TODO: add deferred logs, i.e., the messages are held back and only printed when a non-conditional message is logged.
Purpose: reduce noise, e.g., when printing prerequisites for transformations that do not always apply.
*/

5
src/math/polysat/log.h
View file

@ -114,7 +114,10 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
inline void set_log_enabled(bool) {}
inline bool get_log_enabled() { return false; }
class scoped_set_log_enabled {};
class scoped_set_log_enabled {
public:
scoped_set_log_enabled(bool) {}
};
#define LOG_(vlvl, lvl, x) \
do { \

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

@ -45,6 +45,7 @@ namespace polysat {
default:
break;
}
VERIFY(r.is_var());
}
lbool op_constraint::eval() const {
@ -342,12 +343,12 @@ namespace polysat {
rational const& q_val = qv.val();
if (q_val >= N)
// q >= N ==> r = 0
return s.mk_clause(~shl, ~s.ule(N, q()), s.eq(r()), true);
return s.mk_clause("shl forward 1", {~shl, ~s.ule(N, q()), s.eq(r())}, true);
if (pv.is_val()) {
SASSERT(q_val.is_unsigned());
// p = p_val & q = q_val ==> r = p_val * 2^q_val
rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned());
return s.mk_clause(~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true);
return s.mk_clause("shl forward 2", {~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val)}, true);
}
}
}

12
src/math/polysat/op_constraint.h
View file

@ -27,21 +27,21 @@ namespace polysat {
class op_constraint final : public constraint {
public:
enum class code {
/// r is the logical right shift of p by q
/// r is the logical right shift of p by q.
lshr_op,
/// r is the arithmetic right shift of p by q
/// r is the arithmetic right shift of p by q.
ashr_op,
/// r is the left shift of p by q
/// r is the left shift of p by q.
shl_op,
/// r is the bit-wise 'and' of p and q
/// r is the bit-wise 'and' of p and q.
and_op,
/// r is the smallest multiplicative pseudo-inverse of p;
/// by definition we set r == 0 when p == 0.
/// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
inv_op,
// r is the quotient of dividing p by q
// r is the quotient of unsigned division of p by q.
udiv_op,
// r is the remainder of dividing p by q
// r is the remainder of unsigned division of p by q.
urem_op,
};
protected:

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

@ -934,9 +934,7 @@ namespace polysat {
unsigned lvl = 0;
for (signed_constraint c : m_viable.get_constraints(v)) {
LOG("due to: " << lit_pp(*this, c));
if (!m_bvars.is_assigned(c.blit())) // side condition, irrelevant because all vars are already in the main condition
continue;
SASSERT(m_bvars.is_assigned(c.blit()));
VERIFY(m_bvars.is_assigned(c.blit()));
lvl = std::max(lvl, m_bvars.level(c.blit()));
for (pvar w : c->vars())
if (is_assigned(w)) // TODO: question of which variables are relevant. e.g., v1 > v0 implies v1 > 0 without dependency on v0. maybe add a lemma v1 > v0 --> v1 > 0 on the top level to reduce false variable dependencies? instead of handling such special cases separately everywhere.
@ -1053,7 +1051,7 @@ namespace polysat {
unsigned max_level = 0; // highest level in lemma
unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma
unsigned snd_level = 0; // second-highest level in lemma
unsigned num_undef = 0; // whether there is an unassigned literal (at most one)
unsigned num_undef = 0; // number of unassigned literals
for (sat::literal lit : lemma) {
switch (m_bvars.value(lit)) {
case l_true:
@ -1061,6 +1059,8 @@ namespace polysat {
case l_false:
break;
default:
// TODO: Entering this case means we used clause_builder::insert at some point where it should have been clause_builder::insert_eval?
// Maybe we should just get rid of the insert/insert_eval distinction and evaluate everything here.
switch (lit2cnstr(lit).eval(*this)) {
case l_true:
return std::nullopt;
@ -1069,15 +1069,11 @@ namespace polysat {
break;
case l_undef:
++num_undef;
// NSB: we used to not return null here.
// Lemmas that were not false under evaluation are now skipped
// with this change.
if (num_undef > 1)
return std::nullopt;
continue;
}
}
unsigned const lit_level = m_bvars.level(lit);
if (lit_level > max_level) {
snd_level = max_level;
@ -1102,8 +1098,8 @@ namespace polysat {
// backjump to max_level so we can propagate
unsigned jump_level;
unsigned branching_factor = lits_at_max_level;
if (num_undef == 1)
jump_level = max_level, branching_factor = 1;
if (num_undef >= 1)
jump_level = max_level, branching_factor = num_undef;
else if (lits_at_max_level <= 1)
jump_level = snd_level;
else
@ -1315,12 +1311,6 @@ namespace polysat {
return lit;
}
/**
* Activate constraint immediately
* Activation and de-activation of constraints follows the scope controlled by push/pop.
* constraints activated within the linear solver are de-activated when the linear
* solver is popped.
*/
void solver::activate_constraint(signed_constraint c) {
SASSERT(c);
LOG("Activating constraint: " << c);
@ -1392,12 +1382,20 @@ namespace polysat {
enqueue_pwatch(lit2cnstr(lit).get());
}
void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_ref clause = mk_clause(n, cs, is_redundant);
void solver::add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_ref clause = mk_clause(name, n, cs, is_redundant);
if (clause)
add_clause(*clause);
}
void solver::add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant) {
add_clause(name, static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
}
void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
add_clause("", n, cs, is_redundant);
}
void solver::add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant) {
add_clause(static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
}

2
src/math/polysat/solver.h
View file

@ -327,6 +327,8 @@ namespace polysat {
void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
void add_clause(std::initializer_list<signed_constraint> cs, bool is_redundant);
void add_clause(unsigned n, signed_constraint const* cs, bool is_redundant);
void add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
void add_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant);
// Create a clause without adding it to the solver.
clause_ref mk_clause(signed_constraint c1, bool is_redundant);

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

@ -64,7 +64,9 @@ The following forms are equivalent:
Useful lemmas:
- p <= q ==> p == 0 || -q <= -p
p <= q && q+1 != 0 ==> p+1 <= q+1
p <= q && p != 0 ==> -q <= -p
--*/
@ -104,19 +106,6 @@ namespace {
return;
}
#if 0
// simple version that we had for a long time, subsumed by rule in #else
// p + 1 <= p --> p + 1 <= 0
// p <= p - 1 --> p <= 0
//
// p + k <= p --> p + k <= k - 1
// p <= p - k --> p <= k - 1
if ((lhs - rhs).is_val()) {
pdd k = lhs - rhs;
rhs = k - 1;
}
#else
// Try to reduce the number of variables on one side using one of these rules:
//
// p <= q --> p <= p - q - 1
@ -144,11 +133,11 @@ namespace {
// verbose_stream() << "OUT: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
}
}
#endif
#if 0
// TODO: maybe enable this later to make some constraints more "readable"
// TODO: maybe enable this later to make some constraints more readable
// p - k <= -k - 1 --> k <= p
// ALTERNATIVE: p > k-1 to keep the polynomial on the lhs? allows us to have boolean conflicts between x <= k and x > k ? (otherwise it is x <= k and k+1 <= x.)
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == (rhs + 1).val()) {
// verbose_stream() << "IN: " << ule_pp(to_lbool(is_positive), lhs, rhs) << "\n";
std::abort();
@ -172,16 +161,6 @@ namespace {
is_positive = !is_positive;
}
#if 0
// TODO: enabling this rule leads to unsoundness in 1041-minimized (but the rule itself is correct)
// k <= p --> p - k <= - k - 1
if (lhs.is_val()) {
pdd k = lhs;
lhs = rhs - k;
rhs = - k - 1;
}
#endif
// p > -2 --> p + 1 <= 0
// p <= -2 --> p + 1 > 0
if (rhs.is_val() && !rhs.is_zero() && (rhs + 2).is_zero()) {

58
src/math/polysat/viable.cpp
View file

@ -608,12 +608,12 @@ namespace {
do {
rational coeff_val = mod(e->coeff * val, mod_value);
if (e->interval.currently_contains(coeff_val)) {
IF_LOGGING(
verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
for (const auto& src : e->src)
verbose_stream() << lit_pp(s, src) << "\n";
);
LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
// IF_LOGGING(
// verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
// for (const auto& src : e->src)
// verbose_stream() << lit_pp(s, src) << "\n";
// );
// LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
if (mod(e->interval.hi_val() + 1, mod_value) == e->interval.lo_val()) {
// We have an equation: a * v == b
@ -735,11 +735,12 @@ namespace {
m_diseq_lin[v] = m_diseq_lin[v]->next();
do {
IF_LOGGING(
verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
for (const auto& src : e->src)
verbose_stream() << lit_pp(s, src) << "\n";
);
// IF_LOGGING(
// verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
// for (const auto& src : e->src)
// verbose_stream() << lit_pp(s, src) << "\n";
// );
// We compute an interval if the concrete value 'val' violates the constraint:
// p*val + q > r*val + s if e->src.is_positive()
// p*val + q >= r*val + s if e->src.is_negative()
@ -1907,8 +1908,7 @@ namespace {
bool viable::resolve_interval(pvar v, conflict& core) {
DEBUG_CODE( log(v); );
if (has_viable(v))
return false;
VERIFY(!has_viable(v)); // does a pass over interval refinement, making sure the intervals actually exist
#if 0
// Prefer bit information as justifications
@ -1980,10 +1980,15 @@ namespace {
n = n1;
}
// verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
lemma.insert_try_eval(~c);
// lemma.insert_try_eval(~c);
VERIFY(c.is_currently_true(s));
if (c.bvalue(s) == l_false) {
core.reset();
core.init(~c);
return false;
}
lemma.insert_eval(~c);
for (auto sc : e->side_cond)
lemma.insert_eval(~sc);
@ -1996,8 +2001,25 @@ namespace {
}
while (e != first);
// TODO: violated in bench27
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
// TODO: violated in 5133-min.smt2:
//
// viable lemma:
// 35: -31 <= -1*v17 + -1*v11*v0 + -1*v5*v2 + 32 [ b:l_true p:l_false bprop@0 idx:28 pwatched ]
// -22: v17 + v11*v0 + v6 + v5*v2 != 0 [ b:l_false p:l_undef assert@0 idx:8 pwatched dep:16 ]
// 36: v17 + v11*v0 + v5*v2 + 1 == 0 [ b:l_false p:l_false eval@39 idx:75 ]
// -7: -31 > v6 + 32 [ b:l_false p:l_undef assert@0 idx:17 pwatched dep:33 ]
// ASSERTION VIOLATION
// File: /Users/jakob/projects/z3/src/math/polysat/viable.cpp
// Line: 2036
// all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; })
//
// Reason: there is an eval/bool conflict that we didn't discover before,
// because not-yet-assigned variables are watched but the constraint already evaluates due to cancellation of some terms.
//
// verbose_stream() << "viable lemma:\n";
// for (auto lit : lemma)
// verbose_stream() << " " << lit_pp(s, lit) << "\n";
VERIFY(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v));