mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-14 10:39:15 +01:00
commit dc95179ae5
23 changed files with 797 additions and 325 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -165,6 +165,47 @@ namespace dd {
return true;
}
unsigned pdd_manager::min_parity(PDD p) {
if (m_semantics != mod2N_e)
return 0;
if (is_val(p)) {
rational v = val(p);
if (v.is_zero())
return m_power_of_2 + 1;
unsigned r = 0;
while (v.is_even() && v > 0)
r++, v /= 2;
return r;
}
init_mark();
PDD q = p;
m_todo.push_back(hi(q));
while (!is_val(q)) {
q = lo(q);
m_todo.push_back(hi(q));
}
unsigned p2 = val(q).trailing_zeros();
init_mark();
while (p2 != 0 && !m_todo.empty()) {
PDD r = m_todo.back();
m_todo.pop_back();
if (is_marked(r))
continue;
set_mark(r);
if (!is_val(r)) {
m_todo.push_back(lo(r));
m_todo.push_back(hi(r));
}
else if (val(r).is_zero())
continue;
else if (val(r).trailing_zeros() < p2)
p2 = val(r).trailing_zeros();
}
m_todo.reset();
return p2;
}
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
}
@ -1678,15 +1719,15 @@ namespace dd {
unsigned pow;
if (val.is_power_of_two(pow) && pow > 10)
return out << "2^" << pow;
else if (val < m.max_value() && (val + 1).is_power_of_two(pow) && pow > 10) {
if (require_parens)
out << "(";
out << "2^" << pow << "-1";
if (require_parens)
out << ")";
return out;
} else
return out << m.normalize(val);
for (int offset : {-1, 1})
if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10)
return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen();
rational neg_val = mod(-val, m.two_to_N());
if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise
if (neg_val.is_power_of_two(pow) && pow > 10)
return out << "-2^" << pow;
}
return out << m.normalize(val);
}
bool pdd_manager::well_formed() {

4
src/math/dd/dd_pdd.h
View file

@ -255,6 +255,7 @@ namespace dd {
inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); }
inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); }
bool is_never_zero(PDD p);
unsigned min_parity(PDD p);
inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
@ -432,6 +433,7 @@ namespace dd {
void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
bool is_never_zero() const { return m.is_never_zero(root); }
unsigned min_parity() const { return m.min_parity(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
pdd operator-() const { return m.minus(*this); }
@ -554,6 +556,8 @@ namespace dd {
pdd_manager const& m;
rational const& val;
bool require_parens;
char const* lparen() const { return require_parens ? "(" : ""; }
char const* rparen() const { return require_parens ? ")" : ""; }
public:
val_pp(pdd_manager const& m, rational const& val, bool require_parens): m(m), val(val), require_parens(require_parens) {}
std::ostream& display(std::ostream& out) const;

14
src/math/polysat/clause.cpp
View file

@ -28,20 +28,6 @@ namespace polysat {
return alloc(clause, std::move(literals));
}
bool clause::is_always_false(solver& s) const {
return all_of(m_literals, [&s](sat::literal lit) {
signed_constraint c = s.m_constraints.lookup(lit);
return c.is_always_false();
});
}
bool clause::is_currently_false(solver& s) const {
return all_of(m_literals, [&s](sat::literal lit) {
signed_constraint c = s.m_constraints.lookup(lit);
return c.is_currently_false(s);
});
}
std::ostream& clause::display(std::ostream& out) const {
bool first = true;
for (auto lit : *this) {

4
src/math/polysat/clause.h
View file

@ -68,10 +68,6 @@ namespace polysat {
const_iterator begin() const { return m_literals.begin(); }
const_iterator end() const { return m_literals.end(); }
// evaluates under pvar assignment
bool is_always_false(solver& s) const;
bool is_currently_false(solver& s) const;
std::ostream& display(std::ostream& out) const;
void set_redundant(bool r) { m_redundant = r; }

9
src/math/polysat/clause_builder.cpp
View file

@ -75,13 +75,14 @@ namespace polysat {
m_literals.push_back(c.blit());
}
void clause_builder::insert_eval(sat::literal lit) {
insert_eval(m_solver->lit2cnstr(lit));
void clause_builder::insert_eval(sat::literal lit, bool status) {
insert_eval(m_solver->lit2cnstr(lit), status);
}
void clause_builder::insert_eval(signed_constraint c) {
void clause_builder::insert_eval(signed_constraint c, bool status) {
if (c.bvalue(*m_solver) == l_undef) {
m_solver->assign_eval(~c.blit());
sat::literal lit = c.blit();
m_solver->assign_eval(status ? lit : ~lit);
}
insert(c);
}

16
src/math/polysat/clause_builder.h
View file

@ -51,11 +51,17 @@ namespace polysat {
void insert(signed_constraint c);
void insert(inequality const& i) { insert(i.as_signed_constraint()); }
/// Inserting constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to false.
/// \pre Constraint must be false in the current assignment.
void insert_eval(sat::literal lit);
void insert_eval(signed_constraint c);
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to the given status.
/// \pre Constraint must evaluate to true or false according to the given status in the current assignment.
void insert_eval(sat::literal lit, bool status);
void insert_eval(signed_constraint c, bool status);
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to \b false.
/// \pre Constraint must be \b false in the current assignment.
void insert_eval(sat::literal lit) { insert_eval(lit, false); }
void insert_eval(signed_constraint c) { insert_eval(c, false); }
void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); }
using const_iterator = decltype(m_literals)::const_iterator;

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

@ -68,17 +68,13 @@ namespace polysat {
, m_free_variable_elimination(s)
{}
//
// NSB review: the plugins need not be mutually exclusive
// Shouldn't saturation and superposition be allowed independently?
// If they create propagations or conflict lemmas we select the
// tightest propagation as part of backjumping.
//
void infer_lemmas_for_value(pvar v, conflict& core) {
if (m_poly_sup.perform(v, core))
return;
if (m_saturation.perform(v, core))
return;
(void)m_poly_sup.perform(v, core);
(void)m_saturation.perform(v, core);
}
void infer_lemmas_for_value(pvar v, signed_constraint const& c, conflict& core) {
(void)m_saturation.perform(v, c, core);
}
// Analyse current conflict core to extract additional lemmas
@ -104,11 +100,11 @@ namespace polysat {
}
};
struct inf_resolve_with_assignment : public inference {
struct inf_resolve_evaluated : public inference {
solver& s;
sat::literal lit;
signed_constraint c;
inf_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
inf_resolve_evaluated(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
std::ostream& display(std::ostream& out) const override {
out << "Resolve upon " << lit << " with assignment:";
for (pvar v : c->vars())
@ -189,6 +185,7 @@ namespace polysat {
}
void conflict::init(signed_constraint c) {
LOG("Conflict: constraint " << lit_pp(s, c));
SASSERT(empty());
m_level = s.m_level;
m_narrow_queue.push_back(c.blit()); // if the conflict is only due to a missed propagation of c
@ -221,6 +218,7 @@ namespace polysat {
}
void conflict::init(clause const& cl) {
LOG("Conflict: clause " << cl);
SASSERT(empty());
m_level = s.m_level;
for (auto lit : cl) {
@ -233,6 +231,7 @@ namespace polysat {
}
void conflict::init(pvar v, bool by_viable_fallback) {
LOG("Conflict: viable v" << v);
SASSERT(empty());
m_level = s.m_level;
if (by_viable_fallback) {
@ -251,15 +250,13 @@ namespace polysat {
insert_vars(c);
}
SASSERT(!m_vars.contains(v));
// TODO: apply conflict resolution plugins here too?
}
else {
logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
VERIFY(s.m_viable.resolve(v, *this));
}
// NSB TODO - disabled: revert_decision(v);
SASSERT(!empty());
revert_pvar(v); // at this point, v is not assigned
}
bool conflict::contains(sat::literal lit) const {
@ -301,7 +298,7 @@ namespace polysat {
void conflict::insert_vars(signed_constraint c) {
for (pvar v : c->vars())
if (s.is_assigned(v))
if (s.is_assigned(v))
m_vars.insert(v);
}
@ -322,7 +319,11 @@ namespace polysat {
lemma->set_redundant(true);
for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit));
SASSERT(s.m_bvars.value(lit) != l_true);
// NOTE: it can happen that the literal's bvalue is l_true at this point.
// E.g., lit has been assigned to true on the search stack but not yet propagated.
// A propagation before lit will cause a conflict, and by chance the viable conflict will contain lit.
// (in that case, the evaluation of lit in the current assignment must be false, and it would have caused a conflict by itself when propagated.)
SASSERT(s.m_bvars.value(lit) != l_true || !s.lit2cnstr(lit).is_currently_true(s));
}
m_lemmas.push_back(std::move(lemma));
// TODO: pass to inference_logger (with name)
@ -364,7 +365,7 @@ namespace polysat {
logger().log(inf_resolve_bool(lit, cl));
}
void conflict::resolve_with_assignment(sat::literal lit) {
void conflict::resolve_evaluated(sat::literal lit) {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
@ -387,19 +388,24 @@ namespace polysat {
#endif
if (!has_decision) {
for (pvar v : c->vars()) {
if (s.is_assigned(v) && s.get_level(v) <= lvl) {
m_vars.insert(v);
// TODO - figure out what to do with constraints from conflict lemma that disappear here.
// if (s.m_bvars.is_false(lit))
// m_resolver->infer_lemmas_for_value(v, ~c, *this);
}
}
remove(c);
for (pvar v : c->vars())
if (s.is_assigned(v) && s.get_level(v) <= lvl)
m_vars.insert(v);
}
SASSERT(!contains(lit));
SASSERT(!contains(~lit));
logger().log(inf_resolve_with_assignment(s, lit, c));
logger().log(inf_resolve_evaluated(s, lit, c));
}
void conflict::revert_decision(pvar v) {
void conflict::revert_pvar(pvar v) {
m_resolver->infer_lemmas_for_value(v, *this);
}
@ -418,7 +424,7 @@ namespace polysat {
}
logger().log(inf_resolve_value(s, v));
revert_decision(v);
revert_pvar(v);
}
clause_ref conflict::build_lemma() {

8
src/math/polysat/conflict.h
View file

@ -177,14 +177,14 @@ namespace polysat {
/** Perform boolean resolution with the clause upon the given literal. */
void resolve_bool(sat::literal lit, clause const& cl);
/** lit was fully evaluated under the assignment. */
void resolve_with_assignment(sat::literal lit);
/** lit was evaluated under the assignment. */
void resolve_evaluated(sat::literal lit);
/** Perform resolution with "v = value <- ..." */
void resolve_value(pvar v);
/** Revert decision, add auxiliary lemmas for the decision variable **/
void revert_decision(pvar v);
/** Revert variable assignment, add auxiliary lemmas for the reverted variable */
void revert_pvar(pvar v);
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma();

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

@ -234,4 +234,6 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, constraint_pp const& p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return out << i.as_signed_constraint(); }
}

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

@ -85,42 +85,125 @@ namespace polysat {
}
}
// find literals that are not propagated to false
// if clause is unsat then assign arbitrary
// solver handles unsat clauses by creating a conflict.
// solver also can propagate, but need to check that it does indeed.
/**
* Move literals to be watched to the front of the clause.
*/
void constraint_manager::normalize_watch(clause& cl) {
SASSERT(cl.size() > 1);
// A literal may be watched if there is no unwatched literal at higher level,
// where true and unassigned literals are considered at infinite level.
// We prefer true literals to unassigned literals.
auto get_watch_level = [&](sat::literal lit) -> unsigned {
switch (s.m_bvars.value(lit)) {
case l_false:
return s.m_bvars.level(lit);
case l_true:
return UINT_MAX;
case l_undef:
return UINT_MAX - 1;
}
UNREACHABLE();
return 0;
};
unsigned lvl0 = get_watch_level(cl[0]);
unsigned lvl1 = get_watch_level(cl[1]);
if (lvl0 < lvl1) {
std::swap(lvl0, lvl1);
std::swap(cl[0], cl[1]);
}
SASSERT(lvl0 >= lvl1);
for (unsigned i = 2; i < cl.size(); ++i) {
sat::literal const lit = cl[i];
unsigned const lvl = get_watch_level(lit);
if (lvl > lvl0) {
cl[i] = cl[1];
cl[1] = cl[0];
lvl1 = lvl0;
cl[0] = lit;
lvl0 = lvl;
}
else if (lvl > lvl1) {
cl[i] = cl[1];
cl[1] = lit;
lvl1 = lvl;
}
SASSERT_EQ(lvl0, get_watch_level(cl[0]));
SASSERT_EQ(lvl1, get_watch_level(cl[1]));
SASSERT(lvl0 >= lvl1 && lvl1 >= get_watch_level(cl[i]));
}
SASSERT(all_of(cl, [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[0]); }));
SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); }));
}
void constraint_manager::watch(clause& cl, bool value_propagate) {
if (cl.empty())
return;
bool first = true;
for (unsigned i = 0; i < cl.size(); ++i) {
if (s.m_bvars.is_false(cl[i]))
continue;
signed_constraint sc = s.lit2cnstr(cl[i]);
if (value_propagate && sc.is_currently_false(s)) {
if (s.m_bvars.is_true(cl[i])) {
s.set_conflict(sc);
return;
if (value_propagate) {
#if 1
// First, try to bool-propagate.
// Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
// With this, we will get a constraint-conflict instead.
// TODO: maybe it makes sense to choose bool vs. eval depending on which has the lower level?
sat::literal undef_lit = sat::null_literal;
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;
if (s.m_bvars.is_true(lit)) {
undef_lit = sat::null_literal;
break;
}
SASSERT(!s.m_bvars.is_assigned(lit));
if (undef_lit == sat::null_literal)
undef_lit = lit;
else {
undef_lit = sat::null_literal;
break;
}
s.assign_eval(~cl[i]);
continue;
}
if (undef_lit != sat::null_literal)
s.assign_propagate(undef_lit, cl);
s.m_bvars.watch(cl[i]).push_back(&cl);
std::swap(cl[!first], cl[i]);
if (!first)
return;
first = false;
// this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?)
// (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval)
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;
signed_constraint sc = s.lit2cnstr(lit);
if (sc.is_currently_false(s)) {
if (s.m_bvars.is_true(lit)) {
s.set_conflict(sc);
return;
}
s.assign_eval(~lit);
}
}
#endif
}
if (first)
s.m_bvars.watch(cl[0]).push_back(&cl);
if (cl.size() > 1)
s.m_bvars.watch(cl[1]).push_back(&cl);
if (cl.size() == 1) {
if (s.m_bvars.is_false(cl[0]))
s.set_conflict(cl);
else if (!s.m_bvars.is_assigned(cl[0]))
s.assign_propagate(cl[0], cl);
return;
}
normalize_watch(cl);
s.m_bvars.watch(cl[0]).push_back(&cl);
s.m_bvars.watch(cl[1]).push_back(&cl);
if (s.m_bvars.is_true(cl[0]))
return;
if (first)
SASSERT(!s.m_bvars.is_true(cl[1]));
if (!s.m_bvars.is_false(cl[1])) {
SASSERT(!s.m_bvars.is_assigned(cl[0]) && !s.m_bvars.is_assigned(cl[1]));
return;
}
if (s.m_bvars.is_false(cl[0]))
s.set_conflict(cl);
else
s.assign_propagate(cl[0], cl);

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

@ -74,6 +74,7 @@ namespace polysat {
void gc_constraints();
void gc_clauses();
void normalize_watch(clause& cl);
void watch(clause& cl, bool value_propagate);
void unwatch(clause& cl);

70
src/math/polysat/forbidden_intervals.cpp
View file

@ -128,7 +128,7 @@ namespace polysat {
return true;
}
static char* _last_function = "";
static char const* _last_function = "";
bool forbidden_intervals::get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi) {
@ -180,12 +180,11 @@ namespace polysat {
SASSERT(b1.is_val());
SASSERT(b2.is_val());
// a*v <= 0, a odd
// a*v + b <= 0, a odd
// a*v + b > 0, a odd
if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// a*v + b > 0, a odd
if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@ -385,9 +384,12 @@ namespace polysat {
* a*v <= 0, a odd
* forbidden interval for v is [1,0[
*
* a*v + b <= 0, a odd
* forbidden interval for v is [n+1,n[ where n = -b * a^-1
*
* TODO: extend to
* 2^k*a*v <= 0, a odd
* (using periodic intervals?)
* (using intervals for the lower bits of v)
*/
bool forbidden_intervals::match_zero(
signed_constraint const& c,
@ -395,53 +397,27 @@ namespace polysat {
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (c.is_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) {
auto& m = e1.manager();
rational lo_val(1);
auto lo = m.one();
rational hi_val(0);
auto hi = m.zero();
fi.coeff = 1;
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
if (b1 != e1)
fi.side_cond.push_back(s.eq(b1, e1));
if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2));
return true;
}
return false;
}
/**
* a*v + b > 0, a odd
*
* TODO: extend to
* 2^k*a*v + b > 0, a odd
* (using periodic intervals?)
*/
bool forbidden_intervals::match_non_zero_linear(
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) {
// a*v + b > 0
// <=> a*v + b != 0
// <=> v + a^-1 * b != 0
// <=> v != - a^-1 * b
if (a1.is_odd() && a2.is_zero() && b2.is_zero()) {
auto& m = e1.manager();
rational const& mod_value = m.two_to_N();
rational a1_inv;
VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
rational lo_val(mod(-b1.val() * a1_inv, mod_value));
auto lo = -e1 * a1_inv;
rational hi_val(mod(lo_val + 1, mod_value));
auto hi = lo + 1;
// interval for a*v + b > 0 is [n,n+1[ where n = -b * a^-1
rational lo_val = mod(-b1.val() * a1_inv, mod_value);
pdd lo = -e1 * a1_inv;
rational hi_val = mod(lo_val + 1, mod_value);
pdd hi = lo + 1;
// interval for a*v + b <= 0 is the complement
if (c.is_positive()) {
std::swap(lo_val, hi_val);
std::swap(lo, hi);
}
fi.coeff = 1;
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
if (b1 != e1)
fi.side_cond.push_back(s.eq(b1, e1));
// RHS == 0 is a precondition because we can only multiply with a^-1 in equations, not inequalities
if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2));
return true;

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

@ -73,11 +73,6 @@ namespace polysat {
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi);
bool match_non_zero_linear(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi);
bool match_non_zero(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi);

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

@ -32,32 +32,41 @@ namespace polysat {
saturation::saturation(solver& s) : s(s), m_lemma(s) {}
bool saturation::perform(pvar v, conflict& core) {
for (auto c : core) {
if (!c->is_ule())
continue;
if (c.is_currently_true(s))
continue;
auto i = inequality::from_ule(c);
#if 0
if (try_mul_bounds(v, core, i))
return true;
#endif
#if 0
if (try_parity(v, core, i))
return true;
#endif
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))
return true;
if (try_ugt_z(v, core, i))
return true;
if (try_y_l_ax_and_x_l_z(v, core, i))
return true;
if (try_tangent(v, core, i))
return true;
}
void saturation::perform(pvar v, conflict& core) {
for (auto c : core)
if (perform(v, c, core)) {
IF_VERBOSE(0, auto const& cl = core.lemmas().back();
verbose_stream() << m_rule << " v" << v << " ";
for (auto lit : *cl) verbose_stream() << s.lit2cnstr(lit) << " ";
verbose_stream() << "\n");
return;
}
}
bool saturation::perform(pvar v, signed_constraint const& c, conflict& core) {
if (!c->is_ule())
return false;
if (c.is_currently_true(s))
return false;
auto i = inequality::from_ule(c);
if (try_mul_bounds(v, core, i))
return true;
if (try_parity(v, core, i))
return true;
if (try_parity_diseq(v, core, i))
return true;
if (try_factor_equality(v, core, i))
return true;
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))
return true;
if (try_ugt_z(v, core, i))
return true;
if (try_y_l_ax_and_x_l_z(v, core, i))
return true;
if (false && try_tangent(v, core, i))
return true;
return false;
}
@ -68,7 +77,6 @@ namespace polysat {
return s.ule(lhs, rhs);
}
bool saturation::propagate(conflict& core, inequality const& crit, signed_constraint c) {
if (is_forced_true(c))
return false;
@ -96,8 +104,7 @@ namespace polysat {
SASSERT(all_of(m_lemma, [this](sat::literal lit) { return is_forced_false(s.lit2cnstr(lit)); }));
// NSB review question: insert_eval: Is this right?
m_lemma.insert_eval(c);
m_lemma.insert(c);
core.add_lemma(m_rule, m_lemma.build());
return true;
}
@ -122,10 +129,9 @@ namespace polysat {
if (!is_forced_false(c))
return false;
// TODO: ??? this means that c is already on the search stack, so presumably the lemma won't help. Should check whether this case occurs.
// if (c.bvalue(s) == l_true)
// return false;
SASSERT(c.bvalue(s) != l_true);
// Constraint c is already on the search stack, so the lemma will not derive anything new.
if (c.bvalue(s) == l_true)
return false;
m_lemma.insert_eval(c);
core.add_lemma(m_rule, m_lemma.build());
@ -223,6 +229,18 @@ namespace polysat {
return i.rhs() == y && i.lhs() == a * s.var(x) + b;
}
bool saturation::is_Y_l_AxB(pvar x, inequality const& i, pdd& y, pdd& a, pdd& b) {
y = i.lhs();
pdd aa = a, bb = b;
return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, aa, bb), aa == a && bb == b);
}
bool saturation::verify_Y_l_AxB(pvar x, inequality const& i, pdd const& y, pdd const& a, pdd& b) {
return i.lhs() == y && i.rhs() == a * s.var(x) + b;
}
/**
* Match [x] a*x + b <= y, val(y) = 0
*/
@ -238,6 +256,16 @@ namespace polysat {
return y.is_val() && y.val() == 0 && i.rhs() == y && i.lhs() == a * s.var(x) + b;
}
bool saturation::is_AxB_diseq_0(pvar x, inequality const& i, pdd& a, pdd& b, pdd& y) {
if (!i.is_strict())
return false;
y = i.lhs();
rational y_val;
if (!s.try_eval(y, y_val) || y_val != 0)
return false;
return i.rhs().degree(x) == 1 && (i.rhs().factor(x, 1, a, b), true);
}
/**
* Match [coeff*x] coeff*x*Y where x is a variable
*/
@ -350,12 +378,12 @@ namespace polysat {
if (!is_xY_l_xZ(v, xy_l_xz, y, z))
return false;
if (!xy_l_xz.is_strict() && s.get_value(v).is_zero())
if (!xy_l_xz.is_strict() && s.is_assigned(v) && s.get_value(v).is_zero())
return false;
if (!is_non_overflow(x, y, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
if (!xy_l_xz.is_strict())
m_lemma.insert_eval(s.eq(x));
return add_conflict(core, xy_l_xz, ineq(xy_l_xz.is_strict(), y, z));
@ -398,7 +426,7 @@ namespace polysat {
return false;
pdd const& z_prime = l_y.lhs();
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x));
}
@ -438,7 +466,7 @@ namespace polysat {
if (!is_non_overflow(x, y_prime, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, yx_l_zx, z_l_y, ineq(z_l_y.is_strict() || yx_l_zx.is_strict(), y * x, y_prime * x));
}
@ -479,7 +507,7 @@ namespace polysat {
if (!is_non_overflow(a, z, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~non_ovfl);
return add_conflict(core, y_l_ax, x_l_z, ineq(x_l_z.is_strict() || y_l_ax.is_strict(), y, a * z));
}
@ -514,20 +542,20 @@ namespace polysat {
auto prop1 = [&](signed_constraint c) {
m_lemma.reset();
m_lemma.insert(~s.eq(b));
m_lemma.insert(~s.eq(y));
m_lemma.insert(x_eq_0);
m_lemma.insert(a_eq_0);
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(x_eq_0);
m_lemma.insert_eval(a_eq_0);
return propagate(core, axb_l_y, c);
};
auto prop2 = [&](signed_constraint ante, signed_constraint c) {
m_lemma.reset();
m_lemma.insert(~s.eq(b));
m_lemma.insert(~s.eq(y));
m_lemma.insert(x_eq_0);
m_lemma.insert(a_eq_0);
m_lemma.insert(~ante);
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(x_eq_0);
m_lemma.insert_eval(a_eq_0);
m_lemma.insert_eval(~ante);
return propagate(core, axb_l_y, c);
};
@ -561,7 +589,7 @@ namespace polysat {
//
// NSB review: should we handle cases where k_val >= 2^{K-1}, but exploit that x*y = 0 iff -x*y = 0?
//
IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y.as_signed_constraint() << " " << u_l_k.as_signed_constraint() << " \n");
// IF_VERBOSE(0, verbose_stream() << "mult-bounds2 " << Y << " " << axb_l_y << " " << u_l_k<< " \n");
rational bound = ceil(rational::power_of_two(m.power_of_2()) / k_val);
if (prop2(d, s.uge(Y, bound)))
return true;
@ -569,8 +597,8 @@ namespace polysat {
return true;
}
IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y.as_signed_constraint() << " \n");
IF_VERBOSE(0, verbose_stream() << core << "\n");
// IF_VERBOSE(0, verbose_stream() << "mult-bounds1 " << a << " " << axb_l_y << " \n");
// IF_VERBOSE(0, verbose_stream() << core << "\n");
if (prop1(s.umul_ovfl(a, X)))
return true;
if (prop1(s.umul_ovfl(a, -X)))
@ -603,9 +631,9 @@ namespace polysat {
if (!is_non_overflow(a, X, non_ovfl))
return false;
m_lemma.reset();
m_lemma.insert(~s.eq(b, rational(-1)));
m_lemma.insert(~s.eq(y));
m_lemma.insert(~non_ovfl);
m_lemma.insert_eval(~s.eq(b, rational(-1)));
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~non_ovfl);
if (propagate(core, axb_l_y, s.eq(X, 1)))
return true;
if (propagate(core, axb_l_y, s.eq(a, 1)))
@ -639,41 +667,135 @@ namespace polysat {
bool saturation::try_parity(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] a*x + b = 0 => (odd(a) & odd(x) <=> odd(b))");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero();
pdd a = m.zero();
pdd b = m.zero();
pdd X = s.var(x);
if (!is_AxB_eq_0(x, axb_l_y, a, b, y))
return false;
if (a.is_max() && b.is_var()) // x == y, we propagate values in each direction and don't need a lemma
return false;
if (a.is_one() && (-b).is_var()) // y == x
return false;
if (a.is_one())
return false;
signed_constraint b_is_odd = s.odd(b);
signed_constraint a_is_odd = s.odd(a);
signed_constraint x_is_odd = s.odd(X);
if (!b_is_odd.is_currently_true(s)) {
if (!a_is_odd.is_currently_true(s))
return false;
if (!x_is_odd.is_currently_true(s))
return false;
auto propagate1 = [&](signed_constraint premise, signed_constraint conseq) {
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~a_is_odd);
m_lemma.insert(~x_is_odd);
if (propagate(core, axb_l_y, b_is_odd))
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~premise);
return propagate(core, axb_l_y, conseq);
};
auto propagate2 = [&](signed_constraint premise1, signed_constraint premise2, signed_constraint conseq) {
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~premise1);
m_lemma.insert_eval(~premise2);
return propagate(core, axb_l_y, conseq);
};
#if 0
LOG_H1("try_parity: " << X << " on: " << lit_pp(s, axb_l_y.as_signed_constraint()));
LOG("y: " << y << " a: " << a << " b: " << b);
LOG("b_is_odd: " << lit_pp(s, b_is_odd));
LOG("a_is_odd: " << lit_pp(s, a_is_odd));
LOG("x_is_odd: " << lit_pp(s, x_is_odd));
#endif
if (a_is_odd.is_currently_true(s) &&
x_is_odd.is_currently_true(s) &&
propagate2(a_is_odd, x_is_odd, b_is_odd))
return true;
if (b_is_odd.is_currently_true(s)) {
if (propagate1(b_is_odd, a_is_odd))
return true;
if (propagate1(b_is_odd, x_is_odd))
return true;
return false;
}
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~b_is_odd);
if (propagate(core, axb_l_y, a_is_odd))
return true;
m_lemma.reset();
m_lemma.insert(~s.eq(y));
m_lemma.insert(~b_is_odd);
if (propagate(core, axb_l_y, x_is_odd))
return true;
// a is divisibly by 4,
// max divisor of x is k
// -> b has parity k + 4
unsigned a_parity = a_is_odd.is_currently_false(s) ? 1 : 0;
unsigned x_parity = x_is_odd.is_currently_false(s) ? 1 : 0;
if ((a_parity > 0 || x_parity > 0) && !is_forced_eq(a, 0) && !is_forced_eq(X, 0)) {
while (a_parity < N && s.parity(a, a_parity+1).is_currently_true(s))
++a_parity;
while (x_parity < N && s.parity(X, x_parity+1).is_currently_true(s))
++x_parity;
unsigned b_parity = std::min(N, a_parity + x_parity);
if (a_parity > 0 && x_parity > 0 && propagate2(s.parity(a, a_parity), s.parity(X, x_parity), s.parity(b, b_parity)))
return true;
if (a_parity > 0 && x_parity == 0 && propagate1(s.parity(a, a_parity), s.parity(b, b_parity)))
return true;
if (a_parity == 0 && x_parity > 0 && propagate1(s.parity(X, x_parity), s.parity(b, b_parity)))
return true;
}
//
// if b has at most b_parity, then a*x has at most b_parity
//
else if (!is_forced_eq(b, 0)) {
unsigned b_parity = 1;
bool found = false;
for (; b_parity < N; ++b_parity) {
if (s.parity(b, b_parity).is_currently_false(s)) {
found = true;
break;
}
}
if (found) {
if (propagate1(~s.parity(b, b_parity), ~s.parity(a, b_parity)))
return true;
if (propagate1(~s.parity(b, b_parity), ~s.parity(a, b_parity)))
return true;
for (unsigned i = 1; i < N; ++i) {
if (s.parity(a, i).is_currently_true(s) &&
propagate2(~s.parity(b, b_parity), s.parity(a, i), ~s.parity(X, b_parity - i)))
return true;
if (s.parity(X, i).is_currently_true(s) &&
propagate2(~s.parity(b, b_parity), s.parity(X, i), ~s.parity(a, b_parity - i)))
return true;
}
}
}
return false;
}
/**
* 2^{K-1}*x*y != 0 => odd(x) & odd(y)
* 2^k*x != 0 => parity(x) < K - k
* 2^k*x*y != 0 => parity(x) + parity(y) < K - k
*/
bool saturation::try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] 2^k*x*y != 0 => parity(x) + parity(y) < K - k");
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y = m.zero();
pdd a = y, b = y, X = y;
if (!is_AxB_diseq_0(x, axb_l_y, a, b, y))
return false;
if (!is_forced_eq(b, 0))
return false;
auto coeff = a.leading_coefficient();
if (coeff.is_odd())
return false;
SASSERT(coeff != 0);
unsigned k = coeff.trailing_zeros();
m_lemma.reset();
m_lemma.insert_eval(~s.eq(y));
m_lemma.insert_eval(~s.eq(b));
return propagate(core, axb_l_y, ~s.parity(X, N - k));
}
/**
* a*x = 0 => a = 0 or even(x)
* a*x = 0 => a = 0 or x = 0 or even(a)
@ -693,19 +815,82 @@ namespace polysat {
if (!is_forced_diseq(a, 0, a_eq_0))
return false;
m_lemma.reset();
m_lemma.insert(s.eq(y));
m_lemma.insert(~s.eq(b));
m_lemma.insert(a_eq_0);
m_lemma.insert_eval(s.eq(y));
m_lemma.insert_eval(~s.eq(b));
m_lemma.insert_eval(a_eq_0);
if (propagate(core, axb_l_y, s.even(X)))
return true;
if (!is_forced_diseq(X, 0, x_eq_0))
return false;
m_lemma.insert(x_eq_0);
m_lemma.insert_eval(x_eq_0);
if (propagate(core, axb_l_y, s.even(a)))
return true;
return false;
}
/**
* [x] ax + p <= q, ax + r = 0 => -r + p <= q
* [x] p <= ax + q, ax + r = 0 => p <= -r + q
* generalizations
* [x] abx + p <= q, ax + r = 0 => -rb + p <= q
* [x] p <= abx + q, ax + r = 0 => p <= -rb + q
*/
bool saturation::try_factor_equality(pvar x, conflict& core, inequality const& a_l_b) {
auto& m = s.var2pdd(x);
unsigned N = m.power_of_2();
pdd y1 = m.zero();
pdd a1 = m.zero();
pdd b1 = m.zero();
pdd a2 = a1, b2 = b1, y2 = y1, a3 = a2, b3 = b2, y3 = y2;
bool is_axb_l_y = is_AxB_l_Y(x, a_l_b, a1, b1, y1);
bool is_y_l_axb = is_Y_l_AxB(x, a_l_b, y2, a2, b2);
if (!a_l_b.is_strict() && a_l_b.rhs().is_zero())
return false;
if (!is_axb_l_y && !is_y_l_axb)
return false;
if (a1.is_val() && a2.is_val())
return false;
for (auto c : core) {
if (!c->is_ule())
continue;
auto i = inequality::from_ule(c);
if (i.is_strict())
continue;
if (!is_AxB_eq_0(x, i, a3, b3, y3))
continue;
if (c == a_l_b.as_signed_constraint())
continue;
pdd lhs = i.lhs();
pdd rhs = i.rhs();
bool change = false;
if (is_axb_l_y && a1 == a3) {
change = true;
lhs = b3 - b1;
}
if (is_y_l_axb && a2 == a3) {
change = true;
rhs = b3 - b2;
}
if (!change) {
IF_VERBOSE(0, verbose_stream() << "missed factor equality " << c << " " << a_l_b << "\n");
continue;
}
signed_constraint conseq = i.is_strict() ? s.ult(lhs, rhs) : s.ule(lhs, rhs);
m_lemma.reset();
m_lemma.insert(~s.eq(y3));
m_lemma.insert(~c);
IF_VERBOSE(0, verbose_stream() << "factor equality " << a_l_b << "\n");
if (propagate(core, a_l_b, conseq))
return true;
}
return false;
}
/*
* TODO
*

11
src/math/polysat/saturation.h
View file

@ -47,7 +47,9 @@ namespace polysat {
bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
bool try_parity(pvar x, conflict& core, inequality const& axb_l_y);
bool try_parity_diseq(pvar x, conflict& core, inequality const& axb_l_y);
bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b);
bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y);
bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y);
bool try_tangent(pvar v, conflict& core, inequality const& c);
@ -78,10 +80,16 @@ namespace polysat {
bool is_AxB_l_Y(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
bool verify_AxB_l_Y(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y);
// c := Y ~ Ax + B
bool is_Y_l_AxB(pvar x, inequality const& c, pdd& y, pdd& a, pdd& b);
bool verify_Y_l_AxB(pvar x, inequality const& c, pdd const& y, pdd const& a, pdd& b);
// c := Ax + B ~ Y, val(Y) = 0
bool is_AxB_eq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
bool verify_AxB_eq_0(pvar x, inequality const& c, pdd const& a, pdd const& b, pdd const& y);
// c := Ax + B != Y, val(Y) = 0
bool is_AxB_diseq_0(pvar x, inequality const& c, pdd& a, pdd& b, pdd& y);
// c := Y*X ~ z*X
bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);
@ -112,7 +120,8 @@ namespace polysat {
public:
saturation(solver& s);
bool perform(pvar v, conflict& core);
void perform(pvar v, conflict& core);
bool perform(pvar v, signed_constraint const& sc, conflict& core);
};
/*

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

@ -205,6 +205,7 @@ namespace polysat {
if (!is_conflict())
linear_propagate();
SASSERT(wlist_invariant());
SASSERT(bool_watch_invariant());
SASSERT(assignment_invariant());
}
@ -217,6 +218,7 @@ namespace polysat {
signed_constraint c = lit2cnstr(lit);
activate_constraint(c);
auto& wlist = m_bvars.watch(~lit);
LOG("wlist[" << ~lit << "]: " << wlist);
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
if (!propagate(lit, *wlist[i]))
@ -278,6 +280,7 @@ namespace polysat {
sc.narrow(*this, false);
} else {
// constraint state: active but unassigned (bvalue undef, but pwatch is set; e.g., new constraints generated for lemmas)
#if 1
if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx);
// Wait for the remaining variable to be assigned
@ -293,6 +296,19 @@ namespace polysat {
SASSERT(sc.is_currently_false(*this));
assign_eval(~sc.blit());
}
#else
signed_constraint sc(c, true);
switch (sc.eval(*this)) {
case l_true:
assign_eval(sc.blit());
break;
case l_false:
assign_eval(~sc.blit());
break;
default:
break;
}
#endif
}
return false;
}
@ -517,13 +533,15 @@ namespace polysat {
using T = std::decay_t<decltype(arg)>;
if constexpr (std::is_same_v<T, sat::literal>) {
sat::literal lit = arg;
m_search.push_boolean(arg);
m_search.push_boolean(lit);
m_trail.push_back(trail_instr_t::assign_bool_i);
LOG("Replay: " << lit);
}
else if constexpr (std::is_same_v<T, pvar>) {
pvar v = arg;
m_search.push_assignment(v, m_value[v]);
m_trail.push_back(trail_instr_t::assign_i);
LOG("Replay: " << assignment_pp(*this, v, m_value[v]));
// TODO: are the viable sets propagated properly?
// when substituting polynomials, it will now take into account the replayed variables, which may itself depend on previous propagations.
// will we get into trouble with cyclic dependencies?
@ -537,6 +555,12 @@ namespace polysat {
// then we get an assignment up to that dependency level.
// each literal can only depend on entries with lower dependency level
// (that is the invariant that propagations are justified by a prefix of the search stack.)
// Actually, cyclic dependencies probably don't happen:
// - viable restrictions only occur when all-but-one variable is set (or some vars are irrelevant... those might introduce additional fake dependencies)
// - we only replay propagations... so all new variable assignments are propagations (that depend on earlier decisions)
// - but now the replayed constraints may evaluate to true already and thus not give the forbidden intervals from before anymore...
// so maybe we miss some dependencies this way? a variable was propagated because of a constraint, but after replay the constraint evaluates to true and thus does not add an interval anymore.
// TODO: work out example to explain and test this
}
else
static_assert(always_false<T>::value, "non-exhaustive visitor");
@ -559,6 +583,22 @@ namespace polysat {
void solver::decide() {
LOG_H2("Decide");
SASSERT(can_decide());
#if 1
// Simple hack to try deciding the boolean skeleton first
if (!can_bdecide()) {
// enqueue all not-yet-true clauses
for (auto const& cls : m_constraints.clauses()) {
for (auto const& cl : cls) {
bool is_true = any_of(*cl, [&](sat::literal lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t undefs = count_if(*cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); });
if (undefs >= 2)
m_lemmas.push_back(cl.get());
}
}
}
#endif
if (can_bdecide())
bdecide();
else
@ -770,7 +810,7 @@ namespace polysat {
continue;
}
if (j.is_decision()) {
// NSB TODO - disabled m_conflict.revert_decision(v);
m_conflict.revert_pvar(v);
revert_decision(v);
return;
}
@ -806,7 +846,7 @@ namespace polysat {
// do we really want to resolve these eagerly?
m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
else
m_conflict.resolve_with_assignment(lit);
m_conflict.resolve_evaluated(lit);
}
}
LOG("End of resolve_conflict loop");
@ -824,17 +864,12 @@ namespace polysat {
backjump_and_learn(max_jump_level);
}
//
// NSB review: this code assumes that these lemmas are false.
// It does not allow saturation to add unit propagation into freshly created literals.
//
std::optional<lemma_score> solver::compute_lemma_score(clause const& lemma) {
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
bool is_propagation = false;
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
bool is_propagation = false; // whether there is an unassigned literal (at most one)
for (sat::literal lit : lemma) {
SASSERT(m_bvars.is_assigned(lit)); // any new constraints should have been assign_eval'd
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma
return std::nullopt;
if (!m_bvars.is_assigned(lit)) {
@ -861,15 +896,19 @@ namespace polysat {
// Do the standard backjumping known from SAT solving (back to second-highest level in the lemma, propagate it there).
// - Semantic split clause: multiple literals on the highest level in the lemma.
// Backtrack to "highest level - 1" and split on the lemma there.
// For now, we follow the same convention for computing the jump levels.
// For now, we follow the same convention for computing the jump levels,
// but we support an additional type of clause:
// - Propagation clause: a single literal is unassigned and should be propagated after backjumping.
// backjump to max_level so we can propagate
unsigned jump_level;
unsigned branching_factor = lits_at_max_level;
if (is_propagation)
jump_level = max_level;
if (lits_at_max_level <= 1)
jump_level = max_level, branching_factor = 1;
else if (lits_at_max_level <= 1)
jump_level = snd_level;
else
jump_level = (max_level == 0) ? 0 : (max_level - 1);
return {{jump_level, lits_at_max_level}};
return {{jump_level, branching_factor}};
}
void solver::backjump_and_learn(unsigned max_jump_level) {
@ -886,6 +925,10 @@ namespace polysat {
auto appraise_lemma = [&](clause* lemma) {
m_simplify_clause.apply(*lemma);
auto score = compute_lemma_score(*lemma);
if (score)
LOG(" score: " << *score);
else
LOG(" score: <none>");
if (score && *score < best_score) {
best_score = *score;
best_lemma = lemma;
@ -905,6 +948,9 @@ namespace polysat {
unsigned const jump_level = std::max(best_score.jump_level(), base_level());
SASSERT(jump_level <= max_jump_level);
LOG("best_score: " << best_score);
LOG("best_lemma: " << *best_lemma);
m_conflict.reset();
backjump(jump_level);
@ -923,6 +969,11 @@ namespace polysat {
default:
UNREACHABLE();
}
if (is_conflict()) {
// TODO: the remainder of the narrow_queue as well as the lemmas are forgotten.
// should we just insert them into the new conflict to carry them along?
return;
}
}
for (clause* lemma : lemmas) {
@ -937,13 +988,9 @@ namespace polysat {
// TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
return;
}
SASSERT(!is_conflict());
}
LOG("best_score: " << best_score);
LOG("best_lemma: " << *best_lemma);
if (best_score.literals_at_max_level() > 1) {
if (best_score.branching_factor() > 1) {
// NOTE: at this point it is possible that the best_lemma is non-asserting.
// We need to double-check, because the backjump level may not be exact (see comment on checking is_conflict above).
bool const is_asserting = all_of(*best_lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
@ -1049,6 +1096,10 @@ namespace polysat {
}
if (v != null_var)
m_viable_fallback.push_constraint(v, c);
// TODO: we use narrow with first=true to add axioms about the constraint to the solver.
// However, constraints can be activated multiple times (e.g., if it comes from a lemma and is propagated at a non-base level).
// So the same axioms may be added multiple times.
// Maybe separate narrow/activate? And keep a flag in m_bvars to remember whether constraint has already been activated.
c.narrow(*this, true);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c);
@ -1058,7 +1109,7 @@ namespace polysat {
void solver::backjump(unsigned new_level) {
SASSERT(new_level >= base_level());
if (m_level != new_level) {
LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
LOG_H3("Backjumping to level " << new_level << " from level " << m_level << " (base_level: " << base_level() << ")");
pop_levels(m_level - new_level);
}
}
@ -1269,7 +1320,8 @@ namespace polysat {
out << lpad(4, lit) << ": " << rpad(30, c);
if (!c)
return out;
out << " [ " << s.m_bvars.value(lit);
out << " [ b:" << rpad(7, s.m_bvars.value(lit));
out << " p:" << rpad(7, c.eval(s));
if (s.m_bvars.is_assigned(lit)) {
out << ' ';
if (s.m_bvars.is_assumption(lit))
@ -1291,12 +1343,7 @@ namespace polysat {
}
std::ostream& num_pp::display(std::ostream& out) const {
rational const& p = rational::power_of_two(s.size(var));
if (val > mod(-val, p))
out << -mod(-val, p);
else
out << val;
return out;
return out << dd::val_pp(s.var2pdd(var), val, require_parens);
}
void solver::collect_statistics(statistics& st) const {
@ -1322,7 +1369,7 @@ namespace polysat {
/**
* Check that two variables of each constraint are watched.
*/
bool solver::wlist_invariant() {
bool solver::wlist_invariant() const {
#if 0
for (pvar v = 0; v < m_value.size(); ++v) {
std::stringstream s;
@ -1336,6 +1383,7 @@ namespace polysat {
for (unsigned i = m_qhead; i < m_search.size(); ++i)
if (m_search[i].is_boolean())
skip.insert(m_search[i].lit().var());
SASSERT(is_conflict() || skip.empty()); // after propagation we either finished the queue or we are in a conflict
for (auto c : m_constraints) {
if (skip.contains(c->bvar()))
continue;
@ -1361,6 +1409,33 @@ namespace polysat {
return true;
}
bool solver::bool_watch_invariant() const {
if (is_conflict()) // propagation may be unfinished if a conflict was discovered
return true;
// Check for missed boolean propagations:
// - no clause should have exactly one unassigned literal, unless it is already true.
// - no clause should be false
for (auto const& cls : m_constraints.clauses()) {
for (auto const& clref : cls) {
clause const& cl = *clref;
bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); });
if (is_true)
continue;
size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); });
if (undefs == 1) {
LOG("Missed boolean propagation of clause: " << cl);
for (sat::literal lit : cl) {
LOG(" " << lit_pp(*this, lit));
}
}
SASSERT(undefs != 1);
bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); });
SASSERT(!is_false);
}
}
return true;
}
pdd solver::subst(pdd const& p) const {
return assignment().apply_to(p);
}

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

@ -52,20 +52,19 @@ namespace polysat {
*
* Comparison criterion:
* - Lowest jump level has priority, because otherwise, some of the accumulated lemmas may still be false after backjumping.
* - To break ties on jump level, choose clause with the fewest literals at its highest decision level;
* to limit case splits.
* - To break ties on jump level, choose clause with the lowest branching factor.
*/
class lemma_score {
unsigned m_jump_level;
unsigned m_literals_at_max_level;
unsigned m_branching_factor; // how many literals will be unassigned after backjumping to jump_level
public:
lemma_score(unsigned jump_level, unsigned at_max_level)
: m_jump_level(jump_level), m_literals_at_max_level(at_max_level)
lemma_score(unsigned jump_level, unsigned bf)
: m_jump_level(jump_level), m_branching_factor(bf)
{ }
unsigned jump_level() const { return m_jump_level; }
unsigned literals_at_max_level() const { return m_literals_at_max_level; }
unsigned branching_factor() const { return m_branching_factor; }
static lemma_score max() {
return {UINT_MAX, UINT_MAX};
@ -73,20 +72,20 @@ namespace polysat {
bool operator==(lemma_score const& other) const {
return m_jump_level == other.m_jump_level
&& m_literals_at_max_level == other.m_literals_at_max_level;
&& m_branching_factor == other.m_branching_factor;
}
bool operator!=(lemma_score const& other) const { return !operator==(other); }
bool operator<(lemma_score const& other) const {
return m_jump_level < other.m_jump_level
|| (m_jump_level == other.m_jump_level && m_literals_at_max_level < other.m_literals_at_max_level);
|| (m_jump_level == other.m_jump_level && m_branching_factor < other.m_branching_factor);
}
bool operator>(lemma_score const& other) const { return other.operator<(*this); }
bool operator<=(lemma_score const& other) const { return operator==(other) || operator<(other); }
bool operator>=(lemma_score const& other) const { return operator==(other) || operator>(other); }
std::ostream& display(std::ostream& out) const {
return out << "jump_level=" << m_jump_level << " at_max_level=" << m_literals_at_max_level;
return out << "jump_level=" << m_jump_level << " branching_factor=" << m_branching_factor;
}
};
@ -138,7 +137,7 @@ namespace polysat {
friend class scoped_solverv;
friend class test_polysat;
friend class test_fi;
friend struct inf_resolve_with_assignment;
friend struct inf_resolve_evaluated;
reslimit& m_lim;
params_ref m_params;
@ -212,7 +211,7 @@ namespace polysat {
dd::pdd_manager& sz2pdd(unsigned sz) const;
dd::pdd_manager& var2pdd(pvar v) const;
assignment const& assignment() const { return m_search.assignment(); }
assignment_t const& assignment() const { return m_search.assignment(); }
void push_level();
void pop_levels(unsigned num_levels);
@ -304,7 +303,8 @@ namespace polysat {
bool invariant();
static bool invariant(signed_constraints const& cs);
bool wlist_invariant();
bool wlist_invariant() const;
bool bool_watch_invariant() const;
bool assignment_invariant();
bool verify_sat();
@ -413,7 +413,16 @@ namespace polysat {
signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); }
signed_constraint odd(pdd const& p) { return ~even(p); }
signed_constraint even(pdd const& p) { return parity(p, 1); }
signed_constraint parity(pdd const& p, unsigned k) { return eq(p*rational::power_of_two(p.manager().power_of_2() - k)); }
/** parity(p) >= k (<=> p * 2^(K-k) == 0) */
signed_constraint parity(pdd const& p, unsigned k) {
unsigned N = p.manager().power_of_2();
if (k >= N)
return eq(p);
else if (k == 0)
return odd(p);
else
return eq(p*rational::power_of_two(N - k));
}
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); }
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
@ -533,8 +542,9 @@ namespace polysat {
solver const& s;
pvar var;
rational const& val;
bool require_parens;
public:
num_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {}
num_pp(solver const& s, pvar var, rational const& val, bool require_parens = false): s(s), var(var), val(val), require_parens(require_parens) {}
std::ostream& display(std::ostream& out) const;
};

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

@ -202,12 +202,12 @@ namespace polysat {
s.m_viable.intersect(p, q, sc);
if (first && !is_positive) {
if (!p.is_val())
if (!p.is_val())
// -1 > q
s.add_clause(~sc, s.ult(q, -1), false);
if (!q.is_val())
// p > 0
s.add_clause(~sc, s.ult(0, q), false);
s.add_clause(~sc, s.ult(0, p), false);
}
}

17
src/math/polysat/umul_ovfl_constraint.cpp
View file

@ -80,6 +80,9 @@ namespace polysat {
if (is_always_true(is_positive, p1, q1))
return;
if (first)
activate(s, is_positive);
if (try_viable(s, is_positive, p(), q(), p1, q1))
return;
@ -91,6 +94,16 @@ namespace polysat {
}
void umul_ovfl_constraint::activate(solver& s, bool is_positive) {
// TODO - remove to enable
return;
if (!is_positive) {
signed_constraint sc(this, is_positive);
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false);
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false);
}
}
/**
* if p constant, q, propagate inequality
*/
@ -120,8 +133,8 @@ namespace polysat {
SASSERT(bound * p.val() > max);
SASSERT((bound - 1) * p.val() <= max);
clause_builder cb(s);
cb.insert(~sc);
cb.insert(~premise);
cb.insert_eval(~sc);
cb.insert_eval(~premise);
cb.insert(conseq);
clause_ref just = cb.build();
SASSERT(just);

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

@ -30,6 +30,7 @@ namespace polysat {
static lbool eval(pdd const& p, pdd const& q);
bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
void activate(solver& s, bool is_positive);
public:
~umul_ovfl_constraint() override {}

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

@ -376,7 +376,7 @@ namespace polysat {
lo = val - lambda_l;
increase_hi(hi);
}
LOG("forbidden interval v" << v << " " << val << " " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "[");
LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval << " [" << num_pp(s, v, lo) << ", " << num_pp(s, v, hi) << "[");
SASSERT(hi <= mod_value);
bool full = (lo == 0 && hi == mod_value);
if (hi == mod_value)
@ -707,6 +707,8 @@ namespace polysat {
n = n1;
}
// verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
if (!e->interval.is_full()) {
auto const& hi = e->interval.hi();
auto const& next_lo = n->interval.lo();
@ -725,7 +727,8 @@ namespace polysat {
}
while (e != first);
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); }));
core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v));
return true;

183
src/test/polysat.cpp
View file

@ -204,7 +204,7 @@ namespace polysat {
for (test_record const* r : m_records) {
if (!r->m_finished)
continue;
r->display(out, max_name_len);
r->display(out, static_cast<unsigned>(max_name_len));
out << std::endl;
if (r->m_result == test_result::ok && r->m_answer == l_true)
n_sat++;
@ -241,10 +241,9 @@ namespace polysat {
public:
scoped_solver(std::string name): solver(lim), m_name(name) {
if (collect_test_records) {
std::cout << m_name << ":";
std::cout.flush();
} else {
if (collect_test_records)
std::cout << m_name << std::flush;
else {
std::cout << std::string(78, '#') << "\n\n";
std::cout << "START: " << m_name << "\n";
}
@ -266,10 +265,8 @@ namespace polysat {
}
void check() {
if (collect_test_records) {
std::cout << " ...";
std::cout.flush();
}
if (collect_test_records)
std::cout << " ..." << std::flush;
auto* rec = test_records.active_or_new_record();
m_last_finished = nullptr;
SASSERT(rec->m_answer == l_undef);
@ -287,7 +284,7 @@ namespace polysat {
rec->m_finished = true;
m_last_finished = rec;
if (collect_test_records)
std::cout << " " << m_last_result;
std::cout << " " << m_last_result << std::flush;
else
std::cout << "DONE: " << m_name << ": " << m_last_result << "\n";
statistics st;
@ -327,7 +324,7 @@ namespace polysat {
for (auto const& p : expected_assignment) {
auto const& v_pdd = p.first;
auto const expected_value = p.second;
SASSERT(v_pdd.is_monomial() && !v_pdd.is_val());
SASSERT(v_pdd.is_var());
auto const v = v_pdd.var();
if (get_value(v) != expected_value) {
rec->m_result = test_result::wrong_model;
@ -632,6 +629,66 @@ namespace polysat {
SASSERT(cl->size() == 2);
}
// 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat
static void test_parity1() {
scoped_solver s(__func__);
auto x = s.var(s.add_var(8));
auto y = s.var(s.add_var(8));
auto z = s.var(s.add_var(8));
s.add_clause({s.eq(x * y + z), s.eq(x * y + 5)}, false);
s.add_eq(y, 8);
s.add_eq(z, 3);
s.check();
s.expect_unsat();
}
// 8 * u * x + 3 == 0 or 8 * u * x + 5 == 0 is unsat
static void test_parity1b() {
scoped_solver s(__func__);
auto u = s.var(s.add_var(8));
auto x = s.var(s.add_var(8));
auto y = s.var(s.add_var(8));
auto z = s.var(s.add_var(8));
s.add_clause({s.eq(u * x * y + z), s.eq(u * x * y + 5)}, false);
s.add_eq(y, 8);
s.add_eq(z, 3);
s.check();
s.expect_unsat();
}
// 8 * x + 2 == 0 or 8 * x + 4 == 0 is unsat
static void test_parity2() {
scoped_solver s(__func__);
auto x = s.var(s.add_var(8));
auto y = s.var(s.add_var(8));
s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false);
s.add_eq(y, 8);
s.check();
s.expect_unsat();
}
// (x * y + 4 == 0 or x * y + 2 == 0) & 16 divides y is unsat
static void test_parity3() {
scoped_solver s(__func__);
auto x = s.var(s.add_var(8));
auto y = s.var(s.add_var(8));
s.add_clause({ s.eq(x * y + 2), s.eq(x * y + 4) }, false);
s.add_eq(16 * y);
s.check();
s.expect_unsat();
}
// x*y + 2 == 0
// parity(y) >= 4 || parity(y) >= 8
static void test_parity4(unsigned bw = 8) {
scoped_solver s(concat(__func__, " bw=", bw));
pdd x = s.var(s.add_var(bw));
pdd y = s.var(s.add_var(bw));
s.add_eq(x * y + 2);
s.add_clause({ s.parity(y, 4), s.parity(y, 8) }, false);
s.check();
s.expect_unsat();
}
/**
* Check unsat of:
@ -654,9 +711,10 @@ namespace polysat {
/**
* Check unsat of:
* n*q1 = a - b
* n*q2 + r2 = c*a - c*b
* n > r2 > 0
* n*q1 = a - b 3*1 == 3 - 0
* n*q2 + r2 = c*a - c*b 3*0 + 1 == 11*3 - 11*0 (= 33 = 1 mod 32)
* n > r2 > 0 3 > 1 > 0
* It is actually satisfiable, e.g.: { {n, 3}, {q1, 1}, {a, 3}, {b, 0}, {c, 11}, {q2, 0}, {r2, 1} } (not a unique solution)
*/
static void test_ineq2() {
scoped_solver s(__func__);
@ -672,10 +730,9 @@ namespace polysat {
s.add_ult(r2, n);
s.add_diseq(r2);
s.check();
s.expect_unsat();
s.expect_sat();
}
/**
* Monotonicity example from certora
*
@ -1188,7 +1245,7 @@ namespace polysat {
// x*y <= b & a <= x & !Omega(x*y) => a*y <= b
static void test_ineq_non_axiom4(unsigned bw, unsigned i) {
auto const bound = rational::power_of_two(bw - 1);
scoped_solver s(std::string(__func__) + " perm=" + std::to_string(i));
scoped_solver s(concat(__func__, " bw=", bw, " perm=", i));
LOG("permutation: " << i);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
@ -1258,7 +1315,6 @@ namespace polysat {
static void test_quot_rem_incomplete() {
unsigned bw = 4;
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto quot = s.var(s.add_var(bw));
auto rem = s.var(s.add_var(bw));
auto a = s.value(rational(2), bw);
@ -1278,7 +1334,6 @@ namespace polysat {
static void test_quot_rem_fixed() {
unsigned bw = 4;
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto a = s.value(rational(2), bw);
auto b = s.value(rational(5), bw);
auto [quot, rem] = s.quot_rem(a, b);
@ -1289,24 +1344,22 @@ namespace polysat {
static void test_quot_rem(unsigned bw = 32) {
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto a = s.var(s.add_var(bw));
auto quot = s.var(s.add_var(bw));
auto rem = s.var(s.add_var(bw));
auto x = a * 123;
auto y = 123;
// quot = udiv(a*123, 123)
s.add_eq(quot * y + rem - x);
s.add_diseq(a - quot);
s.add_umul_noovfl(quot, y);
s.add_ult(rem, x);
s.add_eq(x, quot * y + rem); // 123*a = q*123 + r
s.add_diseq(a, quot); // a != quot
s.add_umul_noovfl(quot, y); // 123*quot < 2^K
s.add_ult(rem, x); // r < 123*a ???
s.check();
s.expect_sat();
s.expect_sat(); // dubious
}
static void test_quot_rem2(unsigned bw = 32) {
scoped_solver s(__func__);
s.set_max_conflicts(5);
auto q = s.var(s.add_var(bw));
auto r = s.var(s.add_var(bw));
auto idx = s.var(s.add_var(bw));
@ -1459,6 +1512,17 @@ namespace polysat {
s.expect_sat({{a, 5}});
}
static void test_bench6_viable() {
scoped_solver s(__func__);
rational coeff("12737129816104781496592808350955669863859698313220462044340334240870444260393");
auto a = s.var(s.add_var(256));
auto b = s.var(s.add_var(256));
s.add_eq(4 * b - coeff * a);
s.add_eq(b - 1);
// s.add_eq(a - 100);
s.check();
}
}; // class test_polysat
@ -1590,28 +1654,26 @@ static void STD_CALL polysat_on_ctrl_c(int) {
void tst_polysat() {
using namespace polysat;
#if 0 // Enable this block to run a single unit test with detailed output.
#if 1 // Enable this block to run a single unit test with detailed output.
collect_test_records = false;
test_max_conflicts = 50;
test_polysat::test_band5();
// test_polysat::test_band5_clause();
// test_polysat::test_ineq_axiom1(32, 1);
// test_polysat::test_pop_conflict();
// test_polysat::test_l2();
// test_polysat::test_ineq1();
// test_polysat::test_quot_rem();
// test_polysat::test_ineq_non_axiom1(32, 3);
// test_polysat::test_monot_bounds_full();
// test_polysat::test_band2();
// test_polysat::test_quot_rem_incomplete();
// test_polysat::test_monot();
// test_polysat::test_fixed_point_arith_div_mul_inverse();
// test_polysat::test_parity1();
// test_polysat::test_parity1b();
// test_polysat::test_parity2();
// test_polysat::test_parity3();
test_polysat::test_parity4();
test_polysat::test_parity4(256);
// test_polysat::test_ineq2();
// test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop
// test_polysat::test_ineq_non_axiom4(32, 4); // stuck in viable refinement loop
// test_polysat::test_band1();
// test_polysat::test_bench6_viable();
return;
#endif
// If non-empty, only run tests whose name contains the run_filter
run_filter = "";
test_max_conflicts = 10;
test_max_conflicts = 20;
collect_test_records = true;
@ -1621,6 +1683,12 @@ void tst_polysat() {
set_log_enabled(false);
}
RUN(test_polysat::test_parity1());
RUN(test_polysat::test_parity1b());
RUN(test_polysat::test_parity2());
RUN(test_polysat::test_parity3());
RUN(test_polysat::test_parity4());
RUN(test_polysat::test_clause_simplify1());
RUN(test_polysat::test_add_conflicts());
@ -1662,6 +1730,24 @@ void tst_polysat() {
RUN(test_polysat::test_fixed_point_arith_mul_div_inverse());
RUN(test_polysat::test_fixed_point_arith_div_mul_inverse());
RUN(test_polysat::test_quot_rem_incomplete());
RUN(test_polysat::test_quot_rem_fixed());
RUN(test_polysat::test_quot_rem());
RUN(test_polysat::test_quot_rem2());
RUN(test_polysat::test_band1());
RUN(test_polysat::test_band2());
RUN(test_polysat::test_band3());
RUN(test_polysat::test_band4());
RUN(test_polysat::test_band5());
RUN(test_polysat::test_band5_clause());
RUN(test_polysat::test_fi_zero());
RUN(test_polysat::test_fi_nonzero());
RUN(test_polysat::test_fi_nonmax());
RUN(test_polysat::test_fi_disequal_mild());
RUN(test_polysat::test_bench6_viable());
RUN(test_polysat::test_ineq_axiom1());
RUN(test_polysat::test_ineq_axiom2());
RUN(test_polysat::test_ineq_axiom3());
@ -1671,21 +1757,6 @@ void tst_polysat() {
RUN(test_polysat::test_ineq_non_axiom1());
RUN(test_polysat::test_ineq_non_axiom4());
RUN(test_polysat::test_quot_rem_incomplete());
RUN(test_polysat::test_quot_rem_fixed());
RUN(test_polysat::test_band1());
RUN(test_polysat::test_band2());
RUN(test_polysat::test_band3());
RUN(test_polysat::test_band4());
RUN(test_polysat::test_band5());
RUN(test_polysat::test_band5_clause());
RUN(test_polysat::test_quot_rem());
RUN(test_polysat::test_fi_zero());
RUN(test_polysat::test_fi_nonzero());
RUN(test_polysat::test_fi_nonmax());
RUN(test_polysat::test_fi_disequal_mild());
// test_fi::exhaustive();
// test_fi::randomized();

8
src/util/util.h
View file

@ -385,6 +385,14 @@ bool all_of(Container const& c, Predicate p)
return std::all_of(begin(c), end(c), std::forward<Predicate>(p));
}
/** Compact version of std::any_of */
template <typename Container, typename Predicate>
bool any_of(Container const& c, Predicate p)
{
using std::begin, std::end; // allows begin(c) to also find c.begin()
return std::any_of(begin(c), end(c), std::forward<Predicate>(p));
}
/** Compact version of std::count */
template <typename Container, typename Item>
std::size_t count(Container const& c, Item x)