mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +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-07 16:35:42 +01:00
commit 47cb83f578
34 changed files with 1540 additions and 888 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1629,26 +1629,26 @@ namespace dd {
std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) {
auto mons = to_monomials(b);
bool first = true;
for (auto& m : mons) {
for (auto& [a, vs] : mons) {
if (!first)
out << " ";
if (m.first.is_neg())
if (a.is_neg())
out << "- ";
else if (!first)
out << "+ ";
first = false;
rational c = abs(m.first);
m.second.reverse();
if (!c.is_one() || m.second.empty()) {
rational c = abs(a);
vs.reverse();
if (!c.is_one() || vs.empty()) {
if (m_semantics == mod2N_e)
out << normalize(c);
out << val_pp(*this, c, !vs.empty());
else
out << c;
if (!m.second.empty()) out << "*";
if (!vs.empty()) out << "*";
}
unsigned v_prev = UINT_MAX;
unsigned pow = 0;
for (unsigned v : m.second) {
for (unsigned v : vs) {
if (v == v_prev) {
pow++;
continue;
@ -1672,6 +1672,23 @@ namespace dd {
return out;
}
std::ostream& val_pp::display(std::ostream& out) const {
if (m.get_semantics() != pdd_manager::mod2N_e)
return out << val;
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);
}
bool pdd_manager::well_formed() {
bool ok = true;
for (unsigned n : m_free_nodes) {

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

@ -315,6 +315,11 @@ namespace dd {
pdd_manager(unsigned num_vars, semantics s = free_e, unsigned power_of_2 = 0);
~pdd_manager();
pdd_manager(pdd_manager const&) = delete;
pdd_manager(pdd_manager&&) = delete;
pdd_manager& operator=(pdd_manager const&) = delete;
pdd_manager& operator=(pdd_manager&&) = delete;
semantics get_semantics() const { return m_semantics; }
void reset(unsigned_vector const& level2var);
@ -416,8 +421,9 @@ namespace dd {
bool is_linear() const { return m.is_linear(root); }
bool is_var() const { return m.is_var(root); }
bool is_max() const { return m.is_max(root); }
/** Polynomial is of the form a * x + b for numerals a, b. */
/** Polynomial is of the form a * x + b for some numerals a, b. */
bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); }
/** Polynomial is of the form a * x for some numeral a. */
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); }
bool is_binary() const { return m.is_binary(root); }
@ -544,6 +550,16 @@ namespace dd {
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
};
class val_pp {
pdd_manager const& m;
rational const& val;
bool 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;
};
inline std::ostream& operator<<(std::ostream& out, val_pp const& v) { return v.display(out); }
}

13
src/math/polysat/assignment.cpp
View file

@ -31,6 +31,11 @@ namespace polysat {
return p.subst_val(m_subst);
}
bool substitution::contains(pvar var) const {
rational out_value;
return value(var, out_value);
}
bool substitution::value(pvar var, rational& out_value) const {
return m_subst.subst_get(var, out_value);
}
@ -49,6 +54,14 @@ namespace polysat {
return a;
}
bool assignment::contains(pvar var) const {
return subst(s().size(var)).contains(var);
}
bool assignment::value(pvar var, rational& out_value) const {
return subst(s().size(var)).value(var, out_value);
}
substitution& assignment::subst(unsigned sz) {
return const_cast<substitution&>(std::as_const(*this).subst(sz));
}

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

@ -56,6 +56,7 @@ namespace polysat {
substitution add(pvar var, rational const& value) const;
pdd apply_to(pdd const& p) const;
bool contains(pvar var) const;
bool value(pvar var, rational& out_value) const;
bool empty() const { return m_subst.is_one(); }
@ -96,6 +97,9 @@ namespace polysat {
pdd apply_to(pdd const& p) const;
bool contains(pvar var) const;
bool value(pvar var, rational& out_value) const;
rational value(pvar var) const { rational val; VERIFY(value(var, val)); return val; }
bool empty() const { return pairs().empty(); }
substitution const& subst(unsigned sz) const;
vector<assignment_item_t> const& pairs() const { return m_pairs; }

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

@ -20,10 +20,6 @@ namespace polysat {
class signed_constraint;
class simplify_clause;
class clause;
using clause_ref = ref<clause>;
using clause_ref_vector = sref_vector<clause>;
/// Disjunction of constraints represented by boolean literals
// NB code review:
// right, ref-count is unlikely the right mechanism.
@ -31,11 +27,14 @@ namespace polysat {
// and deleted when they exist the arena.
//
class clause {
public:
static inline const bool redundant_default = true;
private:
friend class constraint_manager;
friend class simplify_clause;
unsigned m_ref_count = 0; // TODO: remove refcount once we confirm it's not needed anymore
bool m_redundant = true;
bool m_redundant = redundant_default;
sat::literal_vector m_literals;

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

@ -29,6 +29,7 @@ namespace polysat {
void clause_builder::reset() {
m_literals.reset();
m_is_tautology = false;
m_redundant = clause::redundant_default;
SASSERT(empty());
}
@ -49,6 +50,9 @@ namespace polysat {
}
m_literals.shrink(j);
clause_ref cl = clause::from_literals(std::move(m_literals));
SASSERT(cl);
cl->set_redundant(m_redundant);
m_redundant = clause::redundant_default;
SASSERT(empty());
return cl;
}
@ -58,6 +62,8 @@ namespace polysat {
insert(m_solver->lit2cnstr(lit));
}
// TODO: in the final version, we may also skip assumptions (and even literals propagated at the base level),
// provided we correctly track external dependencies/level for the clause.
void clause_builder::insert(signed_constraint c) {
SASSERT(c);
if (c.is_always_false()) // filter out trivial constraints such as "4 < 2"

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

@ -28,6 +28,7 @@ namespace polysat {
/// True iff clause contains a literal that is always true
/// (only this specific case of tautology is covered by this flag)
bool m_is_tautology = false;
bool m_redundant = clause::redundant_default;
public:
clause_builder(solver& s);
@ -36,9 +37,11 @@ namespace polysat {
clause_builder& operator=(clause_builder const& s) = delete;
clause_builder& operator=(clause_builder&& s) = default;
bool empty() const { return m_literals.empty() && !m_is_tautology; }
bool empty() const { return m_literals.empty() && !m_is_tautology && m_redundant == clause::redundant_default; }
void reset();
void set_redundant(bool r) { m_redundant = r; }
/// Build the clause. This will reset the clause builder so it can be reused.
/// Returns nullptr if the clause is a tautology and should not be added to the solver.
clause_ref build();

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

@ -57,23 +57,28 @@ TODO:
namespace polysat {
class conflict_resolver {
inf_saturate m_saturate;
saturation m_saturation;
ex_polynomial_superposition m_poly_sup;
free_variable_elimination m_free_variable_elimination;
public:
conflict_resolver(solver& s)
: m_saturate(s)
: m_saturation(s)
, m_poly_sup(s)
, m_free_variable_elimination(s)
{}
bool try_resolve_value(pvar v, conflict& core) {
if (m_poly_sup.perform(v, core))
return true;
// if (m_saturate.perform(v, core))
// return true;
return false;
//
// 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;
}
// Analyse current conflict core to extract additional lemmas
@ -252,6 +257,8 @@ namespace polysat {
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());
}
@ -298,26 +305,27 @@ namespace polysat {
m_vars.insert(v);
}
void conflict::add_lemma(std::initializer_list<signed_constraint> cs) {
add_lemma(std::data(cs), cs.size());
void conflict::add_lemma(char const* name, std::initializer_list<signed_constraint> cs) {
add_lemma(name, std::data(cs), cs.size());
}
void conflict::add_lemma(signed_constraint const* cs, size_t cs_len) {
void conflict::add_lemma(char const* name, signed_constraint const* cs, size_t cs_len) {
clause_builder cb(s);
for (size_t i = 0; i < cs_len; ++i)
cb.insert_eval(cs[i]);
add_lemma(cb.build());
add_lemma(name, cb.build());
}
void conflict::add_lemma(clause_ref lemma) {
void conflict::add_lemma(char const* name, clause_ref lemma) {
LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
SASSERT(lemma);
lemma->set_redundant(true);
LOG_H3("Lemma: " << *lemma);
for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit));
SASSERT(s.m_bvars.value(lit) != l_true);
}
m_lemmas.push_back(std::move(lemma));
// TODO: pass to inference_logger (with name)
}
void conflict::remove(signed_constraint c) {
@ -391,7 +399,11 @@ namespace polysat {
logger().log(inf_resolve_with_assignment(s, lit, c));
}
bool conflict::resolve_value(pvar v) {
void conflict::revert_decision(pvar v) {
m_resolver->infer_lemmas_for_value(v, *this);
}
void conflict::resolve_value(pvar v) {
SASSERT(contains_pvar(v));
SASSERT(s.m_justification[v].is_propagation());
@ -405,11 +417,8 @@ namespace polysat {
insert(s.eq(i.hi(), i.hi_val()));
}
logger().log(inf_resolve_value(s, v));
if (m_resolver->try_resolve_value(v, *this))
return true;
return false;
revert_decision(v);
}
clause_ref conflict::build_lemma() {

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

@ -160,9 +160,9 @@ namespace polysat {
void insert_eval(signed_constraint c);
/** Add a side lemma to the conflict; to be learned in addition to the main lemma after conflict resolution finishes. */
void add_lemma(std::initializer_list<signed_constraint> cs);
void add_lemma(signed_constraint const* cs, size_t cs_len);
void add_lemma(clause_ref lemma);
void add_lemma(char const* name, std::initializer_list<signed_constraint> cs);
void add_lemma(char const* name, signed_constraint const* cs, size_t cs_len);
void add_lemma(char const* name, clause_ref lemma);
/** Remove c from core */
void remove(signed_constraint c);
@ -181,7 +181,10 @@ namespace polysat {
void resolve_with_assignment(sat::literal lit);
/** Perform resolution with "v = value <- ..." */
bool resolve_value(pvar v);
void resolve_value(pvar v);
/** Revert decision, add auxiliary lemmas for the decision variable **/
void revert_decision(pvar v);
/** Convert the core into a lemma to be learned. */
clause_ref build_lemma();

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

@ -37,8 +37,13 @@ namespace polysat {
return m_constraint->to_ule().lhs();
}
signed_constraint inequality::as_signed_constraint() const {
return signed_constraint(const_cast<constraint*>(src), !is_strict);
inequality inequality::from_ule(signed_constraint src)
{
ule_constraint& c = src->to_ule();
if (src.is_positive())
return inequality(c.lhs(), c.rhs(), src);
else
return inequality(c.rhs(), c.lhs(), src);
}
ule_constraint& constraint::to_ule() {

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

@ -34,19 +34,6 @@ namespace polysat {
using constraints = ptr_vector<constraint>;
using signed_constraints = vector<signed_constraint>;
/// Normalized inequality:
/// lhs <= rhs, if !is_strict
/// lhs < rhs, otherwise
struct inequality {
pdd lhs;
pdd rhs;
bool is_strict;
constraint const* src; // TODO: should be signed_constraint now
inequality(pdd const & lhs, pdd const & rhs, bool is_strict, constraint const* src):
lhs(lhs), rhs(rhs), is_strict(is_strict), src(src) {}
signed_constraint as_signed_constraint() const;
};
class constraint {
friend class constraint_manager;
friend class signed_constraint;
@ -97,7 +84,12 @@ namespace polysat {
bool is_currently_false(solver const& s, bool is_positive) const { return is_currently_true(s, !is_positive); }
virtual void narrow(solver& s, bool is_positive, bool first) = 0;
virtual inequality as_inequality(bool is_positive) const = 0;
/**
* If possible, produce a lemma that contradicts the given assignment.
* This method should not modify the solver's search state.
* TODO: don't pass the solver, but an interface that only allows creation of constraints
*/
virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) { return {}; }
ule_constraint& to_ule();
ule_constraint const& to_ule() const;
@ -167,7 +159,7 @@ namespace polysat {
bool is_currently_true(solver const& s) const { return get()->is_currently_true(s, is_positive()); }
lbool bvalue(solver& s) const;
void narrow(solver& s, bool first) { get()->narrow(s, is_positive(), first); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); }
clause_ref produce_lemma(solver& s, assignment const& a) { return get()->produce_lemma(s, a, is_positive()); }
void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep) const { get()->add_to_univariate_solver(s, us, dep, is_positive()); }
@ -196,7 +188,8 @@ namespace polysat {
return combine_hash(get_ptr_hash(get()), bool_hash()(is_positive()));
}
bool operator==(signed_constraint const& other) const {
return get() == other.get() && is_positive() == other.is_positive();
SASSERT_EQ(blit() == other.blit(), get() == other.get() && is_positive() == other.is_positive());
return blit() == other.blit();
}
bool operator!=(signed_constraint const& other) const { return !operator==(other); }
@ -212,6 +205,25 @@ namespace polysat {
return c.display(out);
}
/// Normalized inequality:
/// lhs <= rhs, if !is_strict
/// lhs < rhs, otherwise
class inequality {
pdd m_lhs;
pdd m_rhs;
signed_constraint m_src;
inequality(pdd lhs, pdd rhs, signed_constraint src):
m_lhs(std::move(lhs)), m_rhs(std::move(rhs)), m_src(std::move(src)) {}
public:
static inequality from_ule(signed_constraint src);
pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; }
bool is_strict() const { return m_src.is_negative(); }
signed_constraint as_signed_constraint() const { return m_src; }
};
class constraint_pp {
constraint const* c;
lbool status;

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

@ -275,6 +275,7 @@ namespace polysat {
return ult(a + shift, b + shift);
}
/** unsigned quotient/remainder */
std::pair<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) {
auto& m = a.manager();
unsigned sz = m.power_of_2();
@ -282,6 +283,9 @@ namespace polysat {
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
return {m.mk_val(m.max_value()), a};
}
if (b.is_one()) {
return {a, m.zero()};
}
if (a.is_val() && b.is_val()) {
rational const av = a.val();
rational const bv = b.val();
@ -296,7 +300,14 @@ namespace polysat {
SASSERT(r.val() < b.val());
return {std::move(q), std::move(r)};
}
constraint_dedup::quot_rem_args args({ a, b });
#if 0
unsigned pow;
if (b.is_val() && b.val().is_power_of_two(pow)) {
// TODO: q = a >> b.val()
// r = 0 \circ a[pow:] ???
}
#endif
constraint_dedup::quot_rem_args args({a, b});
auto it = m_dedup.quot_rem_expr.find_iterator(args);
if (it != m_dedup.quot_rem_expr.end())
return { m.mk_var(it->m_value.first), m.mk_var(it->m_value.second) };
@ -311,17 +322,17 @@ namespace polysat {
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
// b ≠ 0 ==> r < b
// b = 0 ==> q = -1
s.add_eq(a, b * q + r);
s.add_umul_noovfl(b, q);
s.add_clause(eq(b * q + r - a), false);
s.add_clause(~umul_ovfl(b, q), false);
// r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1
s.add_ule(b*q, -r-1);
s.add_clause(ule(b*q, -r-1), false);
#if 0
// b*q <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// r <= - b*q - 1
s.add_ule(r, -b*q-1); // redundant, but may help propagation
s.add_clause(ule(r, -b*q-1), false); // redundant, but may help propagation
#endif
auto c_eq = eq(b);

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

@ -127,6 +127,8 @@ namespace polysat {
return true;
}
static char* _last_function = "";
bool forbidden_intervals::get_interval_ule(signed_constraint const& c, pvar v, fi_record& fi) {
@ -135,6 +137,26 @@ namespace polysat {
fi.coeff = 1;
fi.src = c;
struct show {
forbidden_intervals& f;
signed_constraint const& c;
pvar v;
fi_record& fi;
backtrack& _backtrack;
show(forbidden_intervals& f,
signed_constraint const& c,
pvar v,
fi_record& fi,
backtrack& _backtrack):f(f), c(c), v(v), fi(fi), _backtrack(_backtrack) {}
~show() {
if (!_backtrack.released)
return;
IF_VERBOSE(0, verbose_stream() << _last_function << " " << v << " " << c << " " << fi.interval << " " << fi.side_cond << "\n");
}
};
// uncomment to trace intervals
// show _show(*this, c, v, fi, _backtrack);
// eval(lhs) = a1*v + eval(e1) = a1*v + b1
// eval(rhs) = a2*v + eval(e2) = a2*v + b2
// We keep the e1, e2 around in case we need side conditions such as e1=b1, e2=b2.
@ -261,12 +283,13 @@ namespace polysat {
/**
* Match e1 + t <= e2, with t = a1*y
* condition for empty/full: e2 == -1
* condition for empty/full: e2 == -1
*/
bool forbidden_intervals::match_linear1(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 (a2.is_zero() && !a1.is_zero()) {
SASSERT(!a1.is_zero());
bool is_trivial = (b2 + 1).is_zero();
@ -291,6 +314,7 @@ namespace polysat {
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 (a1.is_zero() && !a2.is_zero()) {
SASSERT(!a2.is_zero());
bool is_trivial = b1.is_zero();
@ -315,6 +339,7 @@ namespace polysat {
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 (a1 == a2 && !a1.is_zero()) {
bool is_trivial = b1.val() == b2.val();
push_eq(is_trivial, e1 - e2, fi.side_cond);
@ -337,6 +362,7 @@ namespace polysat {
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 (a1 != a2 && !a1.is_zero() && !a2.is_zero()) {
// NOTE: we don't have an interval here in the same sense as in the other cases.
// We use the interval to smuggle out the values a1,b1,a2,b2 without adding additional fields.
@ -368,6 +394,7 @@ namespace polysat {
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_positive() && a1.is_odd() && b1.is_zero() && a2.is_zero() && b2.is_zero()) {
auto& m = e1.manager();
rational lo_val(1);
@ -397,6 +424,7 @@ namespace polysat {
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
@ -435,6 +463,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi) {
_last_function = __func__;
if (a1.is_odd() && b1.is_zero() && c.is_negative()) {
auto& m = e1.manager();
rational lo_val(0);
@ -475,6 +504,7 @@ namespace polysat {
signed_constraint const& c,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
_last_function = __func__;
if (a2.is_one() && b2.is_val() && c.is_negative()) {
auto& m = e2.manager();
rational const& mod_value = m.two_to_N();

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

@ -24,12 +24,22 @@ Other:
- code diverges on coding conventions.
*/
/*
TODO: add "conditional" 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.
*/
char const* color_red() { return "\x1B[31m"; }
char const* color_yellow() { return "\x1B[33m"; }
char const* color_blue() { return "\x1B[34m"; }
char const* color_reset() { return "\x1B[0m"; }
#if POLYSAT_LOGGING_ENABLED
std::atomic<bool> g_log_enabled(true);
void set_log_enabled(bool log_enabled) {
g_log_enabled = log_enabled;
g_log_enabled = log_enabled;
}
bool get_log_enabled() {
@ -62,11 +72,6 @@ bool polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_f
return msg_level <= max_log_level;
}
char const* color_red() { return "\x1B[31m"; }
char const* color_yellow() { return "\x1B[33m"; }
char const* color_blue() { return "\x1B[34m"; }
char const* color_reset() { return "\x1B[0m"; }
static char const* level_color(LogLevel msg_level) {
switch (msg_level) {
case LogLevel::Heading1: return color_red();

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

@ -29,6 +29,18 @@ char const* color_reset();
void set_log_enabled(bool log_enabled);
bool get_log_enabled();
class scoped_set_log_enabled {
bool m_prev;
public:
scoped_set_log_enabled(bool enabled) {
m_prev = get_log_enabled();
set_log_enabled(enabled);
}
~scoped_set_log_enabled() {
set_log_enabled(m_prev);
}
};
class polysat_log_indent
{
int m_amount;
@ -96,6 +108,7 @@ 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 {};
#define LOG_(lvl, x) \
do { \

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

@ -37,18 +37,12 @@ namespace polysat {
switch (c) {
case code::and_op:
case code::or_op:
case code::xor_op:
if (p.index() > q.index())
std::swap(m_p, m_q);
break;
default:
break;
}
// The following can currently not be used as standalone constraints
SASSERT(c != code::or_op);
SASSERT(c != code::xor_op);
SASSERT(c != code::not_op);
}
lbool op_constraint::eval() const {
@ -74,9 +68,9 @@ namespace polysat {
std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
switch (status) {
case l_true: return display(out);
case l_false: return display(out << "~");
default: return display(out << "?");
case l_true: return display(out, "==");
case l_false: return display(out, "!=");
default: return display(out, "?=");
}
}
@ -90,10 +84,6 @@ namespace polysat {
return out << "<<";
case op_constraint::code::and_op:
return out << "&";
case op_constraint::code::or_op:
return out << "|";
case op_constraint::code::xor_op:
return out << "^";
default:
UNREACHABLE();
return out;
@ -102,41 +92,78 @@ namespace polysat {
}
std::ostream& op_constraint::display(std::ostream& out) const {
if (m_op == code::not_op)
return out << r() << " == ~" << p();
else
return out << r() << " == " << p() << " " << m_op << " " << q();
return display(out, l_true);
}
std::ostream& op_constraint::display(std::ostream& out, char const* eq) const {
return out << r() << " " << eq << " " << p() << " " << m_op << " " << q();
}
/**
* Propagate consequences or detect conflicts based on partial assignments.
*
* We can assume that op_constraint is only asserted positive.
*/
* Propagate consequences or detect conflicts based on partial assignments.
*
* We can assume that op_constraint is only asserted positive.
*/
void op_constraint::narrow(solver& s, bool is_positive, bool first) {
SASSERT(is_positive);
if (is_currently_true(s, is_positive))
return;
switch (m_op) {
case code::lshr_op:
narrow_lshr(s);
break;
case code::shl_op:
narrow_shl(s);
break;
case code::and_op:
narrow_and(s);
break;
default:
NOT_IMPLEMENTED_YET();
break;
}
if (first)
activate(s);
if (clause_ref lemma = produce_lemma(s, s.assignment()))
s.add_clause(*lemma);
if (!s.is_conflict() && is_currently_false(s, is_positive))
s.set_conflict(signed_constraint(this, is_positive));
}
/**
* Produce lemmas that contradict the given assignment.
*
* We can assume that op_constraint is only asserted positive.
*/
clause_ref op_constraint::produce_lemma(solver& s, assignment const& a, bool is_positive) {
SASSERT(is_positive);
if (is_currently_true(a, is_positive))
return {};
return produce_lemma(s, a);
}
clause_ref op_constraint::produce_lemma(solver& s, assignment const& a) {
switch (m_op) {
case code::lshr_op:
return lemma_lshr(s, a);
case code::shl_op:
return lemma_shl(s, a);
case code::and_op:
return lemma_and(s, a);
default:
NOT_IMPLEMENTED_YET();
return {};
}
}
void op_constraint::activate(solver& s) {
switch (m_op) {
case code::lshr_op:
break;
case code::shl_op:
// TODO: if shift amount is constant p << k, then add p << k == p*2^k
break;
case code::and_op:
// handle masking of high order bits
activate_and(s);
break;
default:
break;
}
}
unsigned op_constraint::hash() const {
return mk_mix(p().hash(), q().hash(), r().hash());
}
@ -169,47 +196,46 @@ namespace polysat {
* s.m_viable.max_viable()
* when r, q are variables.
*/
void op_constraint::narrow_lshr(solver& s) {
auto const pv = s.subst(p());
auto const qv = s.subst(q());
auto const rv = s.subst(r());
clause_ref op_constraint::lemma_lshr(solver& s, assignment const& a) {
auto const pv = a.apply_to(p());
auto const qv = a.apply_to(q());
auto const rv = a.apply_to(r());
unsigned const K = p().manager().power_of_2();
signed_constraint const lshr(this, true);
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
// r <= p
s.add_clause(~lshr, s.ule(r(), p()), true);
return s.mk_clause(~lshr, s.ule(r(), p()), true);
else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
// q >= K -> r = 0
s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
return s.mk_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv)
// q = 0 -> p = r
s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
return s.mk_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && rv.val() >= pv.val())
// q != 0 & p > 0 -> r < p
s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
return s.mk_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
rv.val() > rational::power_of_two(K - qv.val().get_unsigned()) - 1)
// q >= k -> r <= 2^{K-k} - 1
s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned()) - 1), true);
return s.mk_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned()) - 1), true);
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
unsigned const k = qv.val().get_unsigned();
// q = k -> r[i] = p[i+k] for 0 <= i < K - k
for (unsigned i = 0; i < K - k; ++i) {
if (rv.val().get_bit(i) && !pv.val().get_bit(i + k)) {
s.add_clause(~lshr, ~s.eq(q(), k), ~s.bit(r(), i), s.bit(p(), i + k), true);
return;
return s.mk_clause(~lshr, ~s.eq(q(), k), ~s.bit(r(), i), s.bit(p(), i + k), true);
}
if (!rv.val().get_bit(i) && pv.val().get_bit(i + k)) {
s.add_clause(~lshr, ~s.eq(q(), k), s.bit(r(), i), ~s.bit(p(), i + k), true);
return;
return s.mk_clause(~lshr, ~s.eq(q(), k), s.bit(r(), i), ~s.bit(p(), i + k), true);
}
}
}
else {
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
}
return {};
}
/** Evaluate constraint: r == p >> q */
@ -244,10 +270,10 @@ namespace polysat {
* r != 0 -> r >= p
* q = 0 -> r = p
*/
void op_constraint::narrow_shl(solver& s) {
auto const pv = s.subst(p());
auto const qv = s.subst(q());
auto const rv = s.subst(r());
clause_ref op_constraint::lemma_shl(solver& s, assignment const& a) {
auto const pv = a.apply_to(p());
auto const qv = a.apply_to(q());
auto const rv = a.apply_to(r());
unsigned const K = p().manager().power_of_2();
signed_constraint const shl(this, true);
@ -256,35 +282,34 @@ namespace polysat {
// r != 0 -> r >= p
// r = 0 \/ r >= p (equivalent)
// r-1 >= p-1 (equivalent unit constraint to better support narrowing)
s.add_clause(~shl, s.ule(p() - 1, r() - 1), true);
return s.mk_clause(~shl, s.ule(p() - 1, r() - 1), true);
else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
// q >= K -> r = 0
s.add_clause(~shl, ~s.ule(K, q()), s.eq(r()), true);
return s.mk_clause(~shl, ~s.ule(K, q()), s.eq(r()), true);
else if (qv.is_zero() && pv.is_val() && rv.is_val() && rv != pv)
// q = 0 -> r = p
s.add_clause(~shl, ~s.eq(q()), s.eq(r(), p()), true);
return s.mk_clause(~shl, ~s.eq(q()), s.eq(r(), p()), true);
else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
!rv.is_zero() && rv.val() < rational::power_of_two(qv.val().get_unsigned()))
// q >= k -> r = 0 \/ r >= 2^k (intuitive version)
// q >= k -> r - 1 >= 2^k - 1 (equivalent unit constraint to better support narrowing)
s.add_clause(~shl, ~s.ule(qv.val(), q()), s.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r() - 1), true);
return s.mk_clause(~shl, ~s.ule(qv.val(), q()), s.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r() - 1), true);
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
unsigned const k = qv.val().get_unsigned();
// q = k -> r[i+k] = p[i] for 0 <= i < K - k
for (unsigned i = 0; i < K - k; ++i) {
if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) {
s.add_clause(~shl, ~s.eq(q(), k), ~s.bit(r(), i + k), s.bit(p(), i), true);
return;
return s.mk_clause(~shl, ~s.eq(q(), k), ~s.bit(r(), i + k), s.bit(p(), i), true);
}
if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) {
s.add_clause(~shl, ~s.eq(q(), k), s.bit(r(), i + k), ~s.bit(p(), i), true);
return;
return s.mk_clause(~shl, ~s.eq(q(), k), s.bit(r(), i + k), ~s.bit(p(), i), true);
}
}
}
else {
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
}
return {};
}
/** Evaluate constraint: r == p << q */
@ -310,37 +335,83 @@ namespace polysat {
return l_undef;
}
/**
* Produce lemmas:
* p & q <= p
* p & q <= q
* p = q => p & q = r
* p = 0 => r = 0
* q = 0 => r = 0
* p[i] && q[i] = r[i]
*
* Possible other:
* p = max_value => q = r
* q = max_value => p = r
*/
void op_constraint::narrow_and(solver& s) {
auto pv = s.subst(p());
auto qv = s.subst(q());
auto rv = s.subst(r());
void op_constraint::activate_and(solver& s) {
auto x = p(), y = q();
if (x.is_val())
std::swap(x, y);
if (!y.is_val())
return;
auto& m = x.manager();
auto yv = y.val();
if (!(yv + 1).is_power_of_two())
return;
signed_constraint const andc(this, true);
if (yv == m.max_value())
s.add_clause(~andc, s.eq(x, r()), false);
else if (yv == 0)
s.add_clause(~andc, s.eq(r()), false);
else {
unsigned K = m.power_of_2();
unsigned k = yv.get_num_bits();
SASSERT(k < K);
rational exp = rational::power_of_two(K - k);
s.add_clause(~andc, s.eq(x * exp, r() * exp), false);
s.add_clause(~andc, s.ule(r(), y), false); // maybe always activate these constraints regardless?
}
}
signed_constraint andc(this, true);
/**
* Produce lemmas for constraint: r == p & q
* r <= p
* r <= q
* p = q => r = p
* p[i] && q[i] = r[i]
* p = 2^K - 1 => q = r
* q = 2^K - 1 => p = r
* p = 2^k - 1 => r*2^{K - k} = q*2^{K - k}
* q = 2^k - 1 => r*2^{K - k} = p*2^{K - k}
* r = 0 && q != 0 & p = 2^k - 1 => q >= 2^k
* r = 0 && p != 0 & q = 2^k - 1 => p >= 2^k
*/
clause_ref op_constraint::lemma_and(solver& s, assignment const& a) {
auto& m = p().manager();
auto pv = a.apply_to(p());
auto qv = a.apply_to(q());
auto rv = a.apply_to(r());
signed_constraint const andc(this, true);
// r <= p
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
s.add_clause(~andc, s.ule(r(), p()), true);
else if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
s.add_clause(~andc, s.ule(r(), q()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
s.add_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
else if (pv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(p()), s.eq(r()), true);
else if (qv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(q()), s.eq(r()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val()) {
unsigned K = p().manager().power_of_2();
return s.mk_clause(~andc, s.ule(r(), p()), true);
// r <= q
if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
return s.mk_clause(~andc, s.ule(r(), q()), true);
// p = q => r = p
if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
return s.mk_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
if (pv.is_val() && qv.is_val() && rv.is_val()) {
// p = -1 => r = q
if (pv.val() == m.max_value() && qv != rv)
return s.mk_clause(~andc, ~s.eq(p(), m.max_value()), s.eq(q(), r()), true);
// q = -1 => r = p
if (qv.val() == m.max_value() && pv != rv)
return s.mk_clause(~andc, ~s.eq(q(), m.max_value()), s.eq(p(), r()), true);
unsigned K = m.power_of_2();
// p = 2^k - 1 => r*2^{K - k} = q*2^{K - k}
// TODO
// if ((pv.val() + 1).is_power_of_two() ...)
// q = 2^k - 1 => r*2^{K - k} = p*2^{K - k}
// r = 0 && q != 0 & p = 2^k - 1 => q >= 2^k
if ((pv.val() + 1).is_power_of_two() && rv.val() > pv.val())
return s.mk_clause(~andc, ~s.eq(r()), ~s.eq(p(), pv.val()), s.eq(q()), s.ult(p(), q()), true);
// r = 0 && p != 0 & q = 2^k - 1 => p >= 2^k
if (rv.is_zero() && (qv.val() + 1).is_power_of_two() && pv.val() <= qv.val())
return s.mk_clause(~andc, ~s.eq(r()), ~s.eq(q(), qv.val()), s.eq(p()),s.ult(q(), p()), true);
for (unsigned i = 0; i < K; ++i) {
bool pb = pv.val().get_bit(i);
bool qb = qv.val().get_bit(i);
@ -348,16 +419,22 @@ namespace polysat {
if (rb == (pb && qb))
continue;
if (pb && qb && !rb)
s.add_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true);
return s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true);
else if (!pb && rb)
s.add_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true);
return s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true);
else if (!qb && rb)
s.add_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
return s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
else
UNREACHABLE();
return;
return {};
}
}
// Propagate r if p or q are 0
if (pv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
return s.mk_clause(~andc, s.ule(r(), p()), true);
if (qv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
return s.mk_clause(~andc, s.ule(r(), q()), true);
return {};
}
/** Evaluate constraint: r == p & q */
@ -379,6 +456,9 @@ namespace polysat {
case code::lshr_op:
us.add_lshr(p_coeff, q_coeff, r_coeff, !is_positive, dep);
break;
case code::shl_op:
us.add_shl(p_coeff, q_coeff, r_coeff, !is_positive, dep);
break;
case code::and_op:
us.add_and(p_coeff, q_coeff, r_coeff, !is_positive, dep);
break;

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

@ -9,9 +9,7 @@ Module Name:
ashr: r == p >>a q
lshl: r == p << q
and: r == p & q
or: r == p | q
not: r == ~p
xor: r == p ^ q
Author:
@ -28,7 +26,7 @@ namespace polysat {
class op_constraint final : public constraint {
public:
enum class code { lshr_op, ashr_op, shl_op, and_op, or_op, xor_op, not_op };
enum class code { lshr_op, ashr_op, shl_op, and_op };
protected:
friend class constraint_manager;
@ -39,16 +37,23 @@ namespace polysat {
op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r);
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
clause_ref produce_lemma(solver& s, assignment const& a);
void narrow_lshr(solver& s);
clause_ref lemma_lshr(solver& s, assignment const& a);
static lbool eval_lshr(pdd const& p, pdd const& q, pdd const& r);
void narrow_shl(solver& s);
clause_ref lemma_shl(solver& s, assignment const& a);
static lbool eval_shl(pdd const& p, pdd const& q, pdd const& r);
void narrow_and(solver& s);
clause_ref lemma_and(solver& s, assignment const& a);
static lbool eval_and(pdd const& p, pdd const& q, pdd const& r);
std::ostream& display(std::ostream& out, char const* eq) const;
void activate(solver& s);
void activate_and(solver& s);
public:
~op_constraint() override {}
pdd const& p() const { return m_p; }
@ -59,7 +64,7 @@ namespace polysat {
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }

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

File diff suppressed because it is too large Load diff

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

@ -12,38 +12,28 @@ Author:
--*/
#pragma once
#include "math/polysat/clause_builder.h"
#include "math/polysat/conflict.h"
namespace polysat {
class solver;
/**
* Introduce lemmas that derive new (simpler) constraints from the current conflict and partial model.
*/
class saturation {
class inference_engine {
friend class conflict;
protected:
solver& s;
public:
inference_engine(solver& s) :s(s) {}
virtual ~inference_engine() {}
/** Try to apply an inference rule.
* Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
* Returns true if a new constraint was added to the core.
*/
virtual bool perform(pvar v, conflict& core) = 0;
};
class inf_saturate : public inference_engine {
vector<signed_constraint> m_new_constraints;
clause_builder m_lemma;
char const* m_rule = nullptr;
void set_rule(char const* r) { m_rule = r; }
void set_rule(char const* r) { m_rule = r; }
void push_omega(pdd const& x, pdd const& y);
void push_omega_bisect(pdd const& x, rational x_max, pdd const& y, rational y_max);
bool is_non_overflow(pdd const& x, pdd const& y, signed_constraint& c);
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c);
bool propagate(char const* inf_name, conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs);
bool propagate(conflict& core, inequality const& crit1, signed_constraint c);
bool add_conflict(conflict& core, inequality const& crit1, signed_constraint c);
bool add_conflict(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint c);
bool try_ugt_x(pvar v, conflict& core, inequality const& c);
@ -52,14 +42,18 @@ namespace polysat {
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
bool try_ugt_z(pvar z, conflict& core, inequality const& c);
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_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
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);
// c := lhs ~ v
// where ~ is < or <=
// c := lhs ~ v
// where ~ is < or <=
bool is_l_v(pvar v, inequality const& c);
// c := v ~ rhs
@ -73,12 +67,25 @@ namespace polysat {
bool verify_Xy_l_XZ(pvar y, inequality const& c, pdd const& x, pdd const& z);
// c := Y ~ Ax
bool is_Y_l_Ax(pvar x, inequality const& d, pdd& a, pdd& y);
bool verify_Y_l_Ax(pvar x, inequality const& d, pdd const& a, pdd const& y);
bool is_Y_l_Ax(pvar x, inequality const& c, pdd& a, pdd& y);
bool verify_Y_l_Ax(pvar x, inequality const& c, pdd const& a, pdd const& y);
// c := Ax ~ Y
bool is_Ax_l_Y(pvar x, inequality const& c, pdd& a, pdd& y);
bool verify_Ax_l_Y(pvar x, inequality const& c, pdd const& a, pdd const& y);
// c := Ax + B ~ Y
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 := 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 := Y*X ~ z*X
bool is_YX_l_zX(pvar z, inequality const& c, pdd& x, pdd& y);
bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y);
bool verify_YX_l_zX(pvar z, inequality const& c, pdd const& x, pdd const& y);
// c := xY <= xZ
bool is_xY_l_xZ(pvar x, inequality const& c, pdd& y, pdd& z);
@ -92,11 +99,20 @@ namespace polysat {
// p := coeff*x*y where coeff_x = coeff*x, x a variable
bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
rational max_value(pdd const& x);
bool is_forced_eq(pdd const& p, rational const& val);
bool is_forced_eq(pdd const& p, int i) { return is_forced_eq(p, rational(i)); }
bool is_forced_diseq(pdd const& p, int i, signed_constraint& c);
bool is_forced_odd(pdd const& p, signed_constraint& c);
bool is_forced_false(signed_constraint const& sc);
bool is_forced_true(signed_constraint const& sc);
public:
inf_saturate(solver& s) : inference_engine(s) {}
bool perform(pvar v, conflict& core) override;
saturation(solver& s);
bool perform(pvar v, conflict& core);
};
/*

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

@ -38,7 +38,6 @@ namespace polysat {
lbool eval(assignment const& a) const override { return l_undef; } // TODO
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }

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

@ -62,6 +62,10 @@ namespace polysat {
}
lbool solver::check_sat() {
#ifndef NDEBUG
SASSERT(!m_is_solving);
flet<bool> save_(m_is_solving, true);
#endif
LOG("Starting");
while (should_search()) {
m_stats.m_num_iterations++;
@ -72,6 +76,7 @@ namespace polysat {
IF_LOGGING(m_viable.log());
if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
else if (is_conflict()) resolve_conflict();
else if (should_add_pwatch()) add_pwatch();
else if (can_propagate()) propagate();
else if (!can_decide()) { LOG_H2("SAT"); SASSERT(verify_sat()); return l_true; }
else if (m_constraints.should_gc()) m_constraints.gc();
@ -136,6 +141,8 @@ namespace polysat {
}
void solver::assign_eh(signed_constraint c, dependency dep) {
// This method is part of the external interface and should not be used to create internal constraints during solving.
SASSERT(!m_is_solving);
backjump(base_level());
SASSERT(at_base_level());
SASSERT(c);
@ -184,8 +191,8 @@ namespace polysat {
if (!can_propagate())
return;
#ifndef NDEBUG
SASSERT(!m_propagating);
flet<bool> save_(m_propagating, true);
SASSERT(!m_is_propagating);
flet<bool> save_(m_is_propagating, true);
#endif
push_qhead();
while (can_propagate()) {
@ -242,7 +249,8 @@ namespace polysat {
* Return true if a new watch was found; or false to keep the existing one.
*/
bool solver::propagate(pvar v, constraint* c) {
LOG_H3("Propagate " << m_vars[v] << " in " << constraint_pp(c, m_bvars.value(c->bvar())));
lbool const bvalue = m_bvars.value(c->bvar());
LOG_H3("Propagate " << m_vars[v] << " in " << constraint_pp(c, bvalue));
SASSERT(is_assigned(v));
SASSERT(!c->vars().empty());
unsigned idx = 0;
@ -259,9 +267,9 @@ namespace polysat {
}
}
// at most one pvar remains unassigned
if (m_bvars.is_assigned(c->bvar())) {
if (bvalue != l_undef) {
// constraint state: bool-propagated
signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
signed_constraint sc(c, bvalue == l_true);
if (c->vars().size() >= 2) {
unsigned other_v = c->var(1 - idx);
if (!is_assigned(other_v))
@ -328,6 +336,25 @@ namespace polysat {
#endif
}
/** Enqueue constraint c to perform add_pwatch(c) on the next solver iteration */
void solver::enqueue_pwatch(constraint* c) {
SASSERT(c);
if (c->is_pwatched())
return;
m_pwatch_queue.push_back(c);
}
bool solver::should_add_pwatch() const {
return !m_pwatch_queue.empty();
}
void solver::add_pwatch() {
for (constraint* c : m_pwatch_queue) {
add_pwatch(c);
}
m_pwatch_queue.reset();
}
void solver::add_pwatch(constraint* c) {
SASSERT(c);
if (c->is_pwatched())
@ -342,8 +369,10 @@ namespace polysat {
if (vars.size() > 1)
add_pwatch(c, vars[1]);
c->set_pwatched(true);
#if 0
m_pwatch_trail.push_back(c);
m_trail.push_back(trail_instr_t::pwatch_i);
#endif
}
void solver::add_pwatch(constraint* c, pvar v) {
@ -412,12 +441,15 @@ namespace polysat {
m_lemmas.pop_back();
break;
}
#if 0
// NOTE: erase_pwatch should be called when the constraint is deleted from the solver.
case trail_instr_t::pwatch_i: {
constraint* c = m_pwatch_trail.back();
erase_pwatch(c);
m_pwatch_trail.pop_back();
break;
}
#endif
case trail_instr_t::add_var_i: {
// NOTE: currently we cannot delete variables during solving,
// since lemmas may introduce new helper variables if they use operations like bitwise and or pseudo-inverse.
@ -626,15 +658,38 @@ namespace polysat {
/// Verify the value we're trying to assign against the univariate solver
void solver::assign_verify(pvar v, rational val, justification j) {
SASSERT(j.is_decision() || j.is_propagation());
// First, check evaluation of the currently-univariate constraints
// TODO: we should add a better way to test constraints under assignments, without modifying the solver state.
m_value[v] = val;
m_search.push_assignment(v, val);
m_justification[v] = j;
bool is_valid = m_viable_fallback.check_constraints(v);
m_search.pop();
m_justification[v] = justification::unassigned();
if (!is_valid) {
#ifndef NDEBUG
unsigned const old_size = m_search.size();
#endif
signed_constraint c;
clause_ref lemma;
{
// Fake the assignment v := val so we can check the constraints using the new value.
// NOTE: we modify the global state here because cloning the assignment is expensive.
m_search.push_assignment(v, val);
assignment_t const& a = m_search.assignment();
on_scope_exit _undo([&](){
m_search.pop();
});
// Check evaluation of the currently-univariate constraints.
c = m_viable_fallback.find_violated_constraint(a, v);
if (c) {
LOG("Violated constraint: " << c);
lemma = c.produce_lemma(*this, a);
LOG("Produced lemma: " << show_deref(lemma));
}
}
SASSERT(m_search.size() == old_size);
SASSERT(!m_search.assignment().contains(v));
if (lemma) {
add_clause(*lemma);
SASSERT(!is_conflict()); // if we have a conflict here, we could have produced this lemma already earlier
if (can_propagate())
return;
}
if (c) {
LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
++m_stats.m_num_viable_fallback;
// Try to find a valid replacement value
@ -675,7 +730,7 @@ namespace polysat {
// Decision should satisfy all univariate constraints.
// Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated.
// TODO: on the other hand, checking constraints here would have us discover some conflicts earlier.
SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(v));
SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(assignment(), v));
#if ENABLE_LINEAR_SOLVER
// TODO: convert justification into a format that can be tracked in a dependency core.
m_linear_solver.set_value(v, val, UINT_MAX);
@ -715,6 +770,7 @@ namespace polysat {
continue;
}
if (j.is_decision()) {
// NSB TODO - disabled m_conflict.revert_decision(v);
revert_decision(v);
return;
}
@ -740,7 +796,7 @@ namespace polysat {
}
continue;
}
SASSERT(!m_bvars.is_assumption(var));
SASSERT(!m_bvars.is_assumption(var)); // TODO: "assumption" is basically "propagated by unit clause" (or "at base level"); except we do not explicitly store the unit clause.
if (m_bvars.is_decision(var)) {
revert_bool_decision(lit);
return;
@ -758,119 +814,47 @@ namespace polysat {
report_unsat();
}
#if 0
/**
* Simple backjumping for lemmas:
* jump to the level where the lemma can be (bool-)propagated,
* even without reverting the last decision.
*/
void solver::backjump_lemma() {
clause_ref lemma = m_conflict.build_lemma();
LOG_H2("backjump_lemma: " << show_deref(lemma));
SASSERT(lemma);
// find second-highest level of the literals in the lemma
unsigned max_level = 0;
unsigned jump_level = 0;
for (auto lit : *lemma) {
if (!m_bvars.is_assigned(lit))
continue;
unsigned lit_level = m_bvars.level(lit);
if (lit_level > max_level) {
jump_level = max_level;
max_level = lit_level;
} else if (max_level > lit_level && lit_level > jump_level) {
jump_level = lit_level;
}
}
jump_level = std::max(jump_level, base_level());
backjump_and_learn(jump_level, *lemma);
}
#endif
/**
* Revert a decision that caused a conflict.
* Variable v was assigned by a decision at position i in the search stack.
*
* C & v = val is conflict.
*
* C => v != val
*
* l1 \/ l2 \/ ... \/ lk \/ v != val
*
*/
void solver::revert_decision(pvar v) {
#if 0
rational val = m_value[v];
LOG_H2("Reverting decision: pvar " << v << " := " << val);
SASSERT(m_justification[v].is_decision());
clause_ref lemma = m_conflict.build_lemma();
SASSERT(lemma);
if (lemma->empty()) {
report_unsat();
return;
}
unsigned jump_level = get_level(v) - 1;
backjump_and_learn(jump_level, *lemma);
#endif
unsigned max_jump_level = get_level(v) - 1;
backjump_and_learn(max_jump_level);
}
void solver::revert_bool_decision(sat::literal const lit) {
#if 0
LOG_H2("Reverting decision: " << lit_pp(*this, lit));
sat::bool_var const var = lit.var();
clause_ref lemma_ref = m_conflict.build_lemma();
SASSERT(lemma_ref);
clause& lemma = *lemma_ref;
SASSERT(!lemma.empty());
SASSERT(count(lemma, ~lit) > 0);
SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_false(lit1); }));
SASSERT(all_of(lemma, [this, var](sat::literal lit1) { return var == lit1.var() || m_bvars.level(lit1) < m_bvars.level(var); }));
unsigned jump_level = m_bvars.level(var) - 1;
backjump_and_learn(jump_level, lemma);
// At this point, the lemma is asserting for ~lit,
// and has been propagated by learn_lemma/add_clause.
SASSERT(all_of(lemma, [this](sat::literal lit1) { return m_bvars.is_assigned(lit1); }));
// so the regular propagation loop will propagate ~lit.
// Recall that lit comes from a non-asserting lemma.
// If there is more than one undef choice left in that lemma,
// then the next bdecide will take care of that (after all outstanding propagations).
SASSERT(can_bdecide());
#endif
unsigned max_jump_level = m_bvars.level(lit) - 1;
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 at_max_level = 0; // how many literals at the 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;
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)) {
SASSERT(!is_propagation);
is_propagation = true;
continue;
}
unsigned const lit_level = m_bvars.level(lit);
if (lit_level > max_level) {
snd_level = max_level;
max_level = lit_level;
at_max_level = 1;
} else if (lit_level == max_level) {
at_max_level++;
} else if (max_level > lit_level && lit_level > snd_level) {
snd_level = lit_level;
lits_at_max_level = 1;
}
else if (lit_level == max_level)
lits_at_max_level++;
else if (max_level > lit_level && lit_level > snd_level)
snd_level = lit_level;
}
SASSERT(lemma.empty() || at_max_level > 0);
SASSERT(lemma.empty() || lits_at_max_level > 0);
// The MCSAT paper distinguishes between "UIP clauses" and "semantic split clauses".
// It is the same as our distinction between "asserting" and "non-asserting" lemmas.
// - UIP clause: a single literal on the highest decision level in the lemma.
@ -879,11 +863,13 @@ namespace polysat {
// Backtrack to "highest level - 1" and split on the lemma there.
// For now, we follow the same convention for computing the jump levels.
unsigned jump_level;
if (at_max_level <= 1)
if (is_propagation)
jump_level = max_level;
if (lits_at_max_level <= 1)
jump_level = snd_level;
else
jump_level = (max_level == 0) ? 0 : (max_level - 1);
return {{jump_level, at_max_level}};
return {{jump_level, lits_at_max_level}};
}
void solver::backjump_and_learn(unsigned max_jump_level) {
@ -916,7 +902,7 @@ namespace polysat {
SASSERT(best_score < lemma_score::max());
SASSERT(best_lemma);
unsigned const jump_level = best_score.jump_level();
unsigned const jump_level = std::max(best_score.jump_level(), base_level());
SASSERT(jump_level <= max_jump_level);
m_conflict.reset();
@ -948,9 +934,10 @@ namespace polysat {
if (is_conflict()) {
// until this is fixed (if possible; and there may be other causes of conflict at this point),
// we just forget about the remaining lemmas and restart conflict analysis.
// TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
return;
}
SASSERT(!is_conflict()); // TODO: is this true in general? No lemma by itself should lead to a conflict here. But can there be conflicting asserting lemmas?
SASSERT(!is_conflict());
}
LOG("best_score: " << best_score);
@ -980,62 +967,6 @@ namespace polysat {
}
} // backjump_and_learn
#if 0
void solver::backjump_and_learn(unsigned jump_level, clause& lemma) {
clause_ref_vector lemmas = m_conflict.take_lemmas();
sat::literal_vector narrow_queue = m_conflict.take_narrow_queue();
m_conflict.reset();
backjump(jump_level);
for (sat::literal lit : narrow_queue) {
switch (m_bvars.value(lit)) {
case l_true:
lit2cnstr(lit).narrow(*this, false);
break;
case l_false:
lit2cnstr(~lit).narrow(*this, false);
break;
case l_undef:
/* do nothing */
break;
default:
UNREACHABLE();
}
}
for (clause* cl : lemmas) {
m_simplify_clause.apply(*cl);
add_clause(*cl);
}
learn_lemma(lemma);
}
#endif
#if 0
void solver::learn_lemma(clause& lemma) {
SASSERT(!lemma.empty());
m_simplify_clause.apply(lemma);
add_clause(lemma); // propagates undef literals, if possible
// At this point, all literals in lemma have been value- or bool-propated, if possible.
// So if the lemma is/was asserting, all its literals are now assigned.
bool is_asserting = all_of(lemma, [this](sat::literal lit) { return m_bvars.is_assigned(lit); });
if (!is_asserting) {
LOG("Lemma is not asserting!");
m_lemmas.push_back(&lemma);
m_trail.push_back(trail_instr_t::add_lemma_i);
// TODO: currently we forget non-asserting lemmas when backjumping over them.
// We surely don't want to keep them in m_lemmas because then we will start doing case splits
// even the lemma should instead be waiting for propagations.
// We could instead watch its pvars and re-insert into m_lemmas when all but one are assigned.
// The same could even be done in general for all lemmas, instead of distinguishing between
// asserting and non-asserting lemmas.
// (Note that the same lemma can be asserting in one branch of the search but non-asserting in another,
// depending on which pvars are assigned.)
SASSERT(can_bdecide());
}
}
#endif
unsigned solver::level(sat::literal lit0, clause const& cl) {
unsigned lvl = 0;
for (auto lit : cl) {
@ -1099,8 +1030,25 @@ namespace polysat {
LOG("Activating constraint: " << c);
SASSERT_EQ(m_bvars.value(c.blit()), l_true);
add_pwatch(c.get());
pvar v = null_var;
if (c->vars().size() == 1)
m_viable_fallback.push_constraint(c->var(0), c);
// If there is exactly one variable in c, then c is always univariate.
v = c->vars()[0];
else {
// Otherwise, check if exactly one variable in c remains unassigned.
for (pvar w : c->vars()) {
if (is_assigned(w))
continue;
if (v != null_var) {
// two or more unassigned vars; abort
v = null_var;
break;
}
v = w;
}
}
if (v != null_var)
m_viable_fallback.push_constraint(v, c);
c.narrow(*this, true);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c);
@ -1108,6 +1056,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);
pop_levels(m_level - new_level);
@ -1131,44 +1080,68 @@ namespace polysat {
SASSERT(!clause.empty());
m_constraints.store(&clause, true);
if (!clause.is_redundant()) {
// for (at least) non-redundant clauses, we also need to watch the constraints
// so we can discover when the clause should propagate
// TODO: check if we also need pwatch for redundant clauses
for (sat::literal lit : clause)
add_pwatch(m_constraints.lookup(lit.var()));
}
// Defer add_pwatch until the next solver iteration, because during propagation of a variable v the watchlist for v is locked.
// NOTE: for non-redundant clauses, pwatching its constraints is required for soundness.
for (sat::literal lit : clause)
enqueue_pwatch(lit2cnstr(lit).get());
}
void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) {
clause_builder cb(*this);
for (unsigned i = 0; i < n; ++i)
cb.insert(cs[i]);
clause_ref clause = cb.build();
if (clause) {
clause->set_redundant(is_redundant);
void solver::add_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_ref clause = mk_clause(n, cs, is_redundant);
if (clause)
add_clause(*clause);
}
}
void solver::add_clause(signed_constraint c, bool is_redundant) {
signed_constraint cs[1] = { c };
add_clause(1, 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);
}
void solver::add_clause(signed_constraint c1, bool is_redundant) {
add_clause({ c1 }, is_redundant);
}
void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
signed_constraint cs[2] = { c1, c2 };
add_clause(2, cs, is_redundant);
add_clause({ c1, c2 }, is_redundant);
}
void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) {
signed_constraint cs[3] = { c1, c2, c3 };
add_clause(3, cs, is_redundant);
add_clause({ c1, c2, c3 }, is_redundant);
}
void solver::add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant) {
signed_constraint cs[4] = { c1, c2, c3, c4 };
add_clause(4, cs, is_redundant);
add_clause({ c1, c2, c3, c4 }, is_redundant);
}
clause_ref solver::mk_clause(std::initializer_list<signed_constraint> cs, bool is_redundant) {
return mk_clause(static_cast<unsigned>(cs.size()), std::data(cs), is_redundant);
}
clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_builder cb(*this);
for (unsigned i = 0; i < n; ++i)
cb.insert(cs[i]);
cb.set_redundant(is_redundant);
return cb.build();
}
clause_ref solver::mk_clause(signed_constraint c1, bool is_redundant) {
return mk_clause({ c1 }, is_redundant);
}
clause_ref solver::mk_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
return mk_clause({ c1, c2 }, is_redundant);
}
clause_ref solver::mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant) {
return mk_clause({ c1, c2, c3 }, is_redundant);
}
clause_ref solver::mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant) {
return mk_clause({ c1, c2, c3, c4 }, is_redundant);
}
clause_ref solver::mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, signed_constraint c5, bool is_redundant) {
return mk_clause({ c1, c2, c3, c4, c5 }, is_redundant);
}
void solver::push() {

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

@ -133,7 +133,7 @@ namespace polysat {
friend class assignments_pp;
friend class ex_polynomial_superposition;
friend class free_variable_elimination;
friend class inf_saturate;
friend class saturation;
friend class constraint_manager;
friend class scoped_solverv;
friend class test_polysat;
@ -165,7 +165,8 @@ namespace polysat {
vector<constraints> m_pwatch; // watch list datastructure into constraints.
#ifndef NDEBUG
std::optional<pvar> m_locked_wlist; // restrict watch list modification while it is being propagated
bool m_propagating = false; // set to true during propagation
bool m_is_propagating = false; // set to true during propagation
bool m_is_solving = false; // set to true during solving
#endif
unsigned_vector m_activity;
@ -179,7 +180,10 @@ namespace polysat {
svector<trail_instr_t> m_trail;
unsigned_vector m_qhead_trail;
constraints m_pwatch_queue;
#if 0
constraints m_pwatch_trail;
#endif
ptr_vector<clause> m_lemmas; ///< the non-asserting lemmas
unsigned m_lemmas_qhead = 0;
@ -233,6 +237,9 @@ namespace polysat {
void propagate(pvar v);
bool propagate(pvar v, constraint* c);
bool propagate(sat::literal lit, clause& cl);
void enqueue_pwatch(constraint* c);
bool should_add_pwatch() const;
void add_pwatch();
void add_pwatch(constraint* c);
void add_pwatch(constraint* c, pvar v);
void erase_pwatch(pvar v, constraint* c);
@ -273,12 +280,23 @@ namespace polysat {
void report_unsat();
void learn_lemma(clause& lemma);
void backjump(unsigned new_level);
void add_clause(clause& clause);
void add_clause(signed_constraint c, bool is_redundant);
void add_clause(signed_constraint c1, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
void add_clause(unsigned n, signed_constraint* cs, 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);
// Create a clause without adding it to the solver.
clause_ref mk_clause(signed_constraint c1, bool is_redundant);
clause_ref mk_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
clause_ref mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant);
clause_ref mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
clause_ref mk_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, signed_constraint c5, bool is_redundant);
clause_ref mk_clause(std::initializer_list<signed_constraint> cs, bool is_redundant);
clause_ref mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant);
signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
@ -393,6 +411,9 @@ namespace polysat {
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
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)); }
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); }
@ -400,9 +421,13 @@ namespace polysat {
signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); }
signed_constraint ule(pdd const& p, int n) { return ule(p, rational(n)); }
signed_constraint ule(int n, pdd const& p) { return ule(rational(n), p); }
signed_constraint uge(pdd const& p, pdd const& q) { return ule(q, p); }
signed_constraint uge(pdd const& p, rational const& q) { return ule(q, p); }
signed_constraint ult(pdd const& p, pdd const& q) { return m_constraints.ult(p, q); }
signed_constraint ult(pdd const& p, rational const& q) { return ult(p, p.manager().mk_val(q)); }
signed_constraint ult(rational const& p, pdd const& q) { return ult(q.manager().mk_val(p), q); }
signed_constraint ult(int p, pdd const& q) { return ult(rational(p), q); }
signed_constraint ult(pdd const& p, int q) { return ult(p, rational(q)); }
signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
signed_constraint slt(pdd const& p, rational const& q) { return slt(p, p.manager().mk_val(q)); }
@ -418,7 +443,7 @@ namespace polysat {
signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
/** Create and activate polynomial constraints. */
/** Create and activate constraints */
void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); }
void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }
void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }

10
src/math/polysat/superposition.cpp
View file

@ -72,23 +72,19 @@ namespace polysat {
SASSERT(c1.is_currently_true(s));
SASSERT(c2.is_currently_false(s));
SASSERT_EQ(c1.bvalue(s), l_true);
SASSERT(c2.bvalue(s) != l_false);
SASSERT_EQ(c2.bvalue(s), l_true);
signed_constraint c = resolve1(v, c1, c2);
if (!c)
continue;
SASSERT(c.is_currently_false(s));
// char const* inf_name = "?";
switch (c.bvalue(s)) {
case l_false:
core.add_lemma({c, ~c1, ~c2});
// core.log_inference(inference_sup("l_false", v, c2, c1));
core.add_lemma("superposition l_false", {c, ~c1, ~c2});
return l_true;
case l_undef:
// inf_name = "l_undef";
core.add_lemma({c, ~c1, ~c2});
// core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
core.add_lemma("superposition l_undef", {c, ~c1, ~c2});
break;
case l_true:
break;

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

@ -20,7 +20,7 @@ namespace polysat {
qhead_i,
lemma_qhead_i,
add_lemma_i,
pwatch_i,
// pwatch_i,
add_var_i,
inc_level_i,
viable_add_i,

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

@ -28,6 +28,9 @@ namespace polysat {
class solver;
class clause;
using clause_ref = ref<clause>;
using clause_ref_vector = sref_vector<clause>;
typedef dd::pdd pdd;
typedef dd::bdd bdd;
typedef dd::bddv bddv;
@ -47,7 +50,10 @@ namespace polysat {
inline const dependency null_dependency = dependency(UINT_MAX);
typedef svector<dependency> dependency_vector;
inline bool operator<(dependency const& d1, dependency const& d2) { return d1.val() < d2.val(); }
inline bool operator< (dependency const& d1, dependency const& d2) { return d1.val() < d2.val(); }
inline bool operator<=(dependency const& d1, dependency const& d2) { return d1.val() <= d2.val(); }
inline bool operator> (dependency const& d1, dependency const& d2) { return d1.val() > d2.val(); }
inline bool operator>=(dependency const& d1, dependency const& d2) { return d1.val() >= d2.val(); }
inline bool operator==(dependency const& d1, dependency const& d2) { return d1.val() == d2.val(); }
inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); }

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

@ -87,12 +87,25 @@ namespace {
lhs = 0, rhs = 0, is_positive = !is_positive;
return;
}
#if 0
// !(k <= p) -> p <= k - 1
if (!is_positive && lhs.is_val() && lhs.val() > 0) {
pdd k = lhs;
lhs = rhs;
rhs = k - 1;
is_positive = true;
}
#endif
// k <= p --> p - k <= - k - 1
if (lhs.is_val()) {
pdd k = lhs;
lhs = rhs - k;
rhs = - k - 1;
}
// NSB: why this?
// p > -2 --> p + 1 <= 0
// p <= -2 --> p + 1 > 0
if (rhs.is_val() && (rhs + 2).is_zero()) {
@ -162,7 +175,7 @@ namespace polysat {
}
std::ostream& ule_constraint::display(std::ostream& out) const {
return out << m_lhs << (is_eq() ? " == " : " <= ") << m_rhs;
return display(out, l_true, m_lhs, m_rhs);
}
void ule_constraint::narrow(solver& s, bool is_positive, bool first) {
@ -187,6 +200,15 @@ namespace polysat {
}
s.m_viable.intersect(p, q, sc);
if (first && !is_positive) {
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);
}
}
// Evaluate lhs <= rhs
@ -215,13 +237,6 @@ namespace polysat {
return eval(a.apply_to(lhs()), a.apply_to(rhs()));
}
inequality ule_constraint::as_inequality(bool is_positive) const {
if (is_positive)
return inequality(lhs(), rhs(), false, this);
else
return inequality(rhs(), lhs(), true, this);
}
unsigned ule_constraint::hash() const {
return mk_mix(lhs().hash(), rhs().hash(), kind());
}

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

@ -41,7 +41,6 @@ namespace polysat {
lbool eval() const override;
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return m_rhs.is_zero(); }

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

@ -137,7 +137,6 @@ namespace polysat {
return s.m_viable.intersect(p0, q0, sc);
}
unsigned umul_ovfl_constraint::hash() const {
return mk_mix(p().hash(), q().hash(), kind());
}

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

@ -41,7 +41,6 @@ namespace polysat {
lbool eval(assignment const& a) const override;
void narrow(solver& s, bool is_positive, bool first) override;
inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const override { return false; }

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

@ -390,7 +390,7 @@ namespace polysat {
cb.insert(c_new);
ref<clause> c = cb.build();
if (c) // Can we get tautologies this way?
core.add_lemma(c);
core.add_lemma("variable elimination", cb.build());
}
}

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

@ -116,7 +116,7 @@ namespace polysat {
m_trail.pop_back();
}
bool viable::intersect(pdd const & p, pdd const & q, signed_constraint const& sc) {
bool viable::intersect(pdd const& p, pdd const& q, signed_constraint const& sc) {
pvar v = null_var;
bool first = true;
bool prop = false;
@ -205,7 +205,7 @@ namespace polysat {
}
bool viable::intersect(pvar v, entry* ne) {
SASSERT(!s.is_assigned(v));
// SASSERT(!s.is_assigned(v)); // TODO: do we get unsoundness if this condition is violated? (see comment on cyclic dependencies in solver::pop_levels)
entry* e = m_units[v];
if (e && e->interval.is_full()) {
m_alloc.push_back(ne);
@ -726,7 +726,7 @@ namespace polysat {
while (e != first);
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false; }));
core.add_lemma(lemma.build());
core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v));
return true;
}
@ -837,17 +837,17 @@ namespace polysat {
m_constraints[v].pop_back();
}
bool viable_fallback::check_constraints(pvar v) {
for (auto const& c : m_constraints[v]) {
signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar v) {
for (signed_constraint const c : m_constraints[v]) {
// for this check, all variables need to be assigned
DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
if (c.is_currently_false(s)) {
LOG(assignment_pp(s, v, s.get_value(v)) << " violates constraint " << lit_pp(s, c));
return false;
DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(a.contains(w)); });
if (c.is_currently_false(a)) {
LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c));
return c;
}
SASSERT(c.is_currently_true(s));
SASSERT(c.is_currently_true(a));
}
return true;
return {};
}
dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) {
@ -869,6 +869,7 @@ namespace polysat {
auto const& cs = m_constraints[v];
for (unsigned i = cs.size(); i-- > 0; ) {
LOG("Univariate constraint: " << cs[i]);
cs[i].add_to_univariate_solver(s, *us, i);
}

17
src/math/polysat/viable.h
View file

@ -85,7 +85,11 @@ namespace polysat {
*/
bool intersect(pvar v, signed_constraint const& c);
bool intersect(pdd const & p, pdd const & q, signed_constraint const& c);
/**
* Extract remaining variable v from p and q and try updating viable state for v.
* NOTE: does not require a particular constraint type (e.g., we call this for ule_constraint and umul_ovfl_constraint)
*/
bool intersect(pdd const& p, pdd const& q, signed_constraint const& c);
/**
* Check whether variable v has any viable values left according to m_viable.
@ -98,10 +102,9 @@ namespace polysat {
bool is_viable(pvar v, rational const& val);
/*
* Extract min and max viable values for v
*/
* Extract min and max viable values for v
*/
rational min_viable(pvar v);
rational max_viable(pvar v);
/**
@ -245,8 +248,10 @@ namespace polysat {
void push_constraint(pvar v, signed_constraint const& c);
void pop_constraint();
// Check whether all constraints for 'v' are satisfied.
bool check_constraints(pvar v);
// Check whether all constraints for 'v' are satisfied;
// or find an arbitrary violated constraint.
bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
signed_constraint find_violated_constraint(assignment const& a, pvar v);
dd::find_t find_viable(pvar v, rational& out_val);
signed_constraints unsat_core(pvar v);