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

migrating interface

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-22 07:05:17 -08:00
parent 78aea59387
commit 1d1457f81a
12 changed files with 123 additions and 149 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/sat/smt/polysat/core.cpp
View file

@ -175,11 +175,11 @@ namespace polysat {
s.trail().push(mk_dqueue_var(m_var, *this));
switch (m_viable.find_viable(m_var, m_value)) {
case find_t::empty:
s.set_lemma(m_viable.get_core(), get_dependencies(m_viable.explain()));
s.set_conflict(m_viable.explain());
// propagate_unsat_core();
return sat::check_result::CR_CONTINUE;
case find_t::singleton:
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), get_dependencies(m_viable.explain()));
s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
return sat::check_result::CR_CONTINUE;
case find_t::multiple:
s.add_eq_literal(m_var, m_value);
@ -353,10 +353,10 @@ namespace polysat {
return;
switch (eval(sc)) {
case l_false:
s.propagate(d, true, get_dependencies(explain_eval(sc)));
s.propagate(d, true, explain_eval(sc));
break;
case l_true:
s.propagate(d, false, get_dependencies(explain_eval(sc)));
s.propagate(d, false, explain_eval(sc));
break;
default:
break;
@ -369,17 +369,10 @@ namespace polysat {
return value == l_false ? ~d : d;
}
dependency_vector core::get_dependencies(constraint_id_vector const& cc) {
dependency_vector core::get_dependencies(constraint_id_vector const& ids) const {
dependency_vector result;
for (auto idx : cc)
result.push_back(get_dependency(idx));
return result;
}
dependency_vector core::get_dependencies(std::initializer_list<constraint_id> const& cc) {
dependency_vector result;
for (auto idx : cc)
result.push_back(get_dependency(idx));
for (auto id : ids)
result.push_back(get_dependency(id));
return result;
}
@ -388,7 +381,7 @@ namespace polysat {
if (eval_value == l_undef)
sc.propagate(*this, value, d);
else if (value == l_undef)
s.propagate(d, eval_value != l_true, get_dependencies(explain_eval(sc)));
s.propagate(d, eval_value != l_true, explain_eval(sc));
else if (value != eval_value) {
m_unsat_core = explain_eval(sc);
m_unsat_core.push_back(id);
@ -411,8 +404,7 @@ namespace polysat {
void core::propagate_unsat_core() {
// default is to use unsat core:
// if core is based on viable, use s.set_lemma();
s.set_conflict(get_dependencies(m_unsat_core));
s.set_conflict(m_unsat_core);
}
void core::assign_eh(constraint_id index, bool sign, unsigned level) {
@ -451,6 +443,10 @@ namespace polysat {
return s.trail();
}
void core::add_axiom(char const* name, core_vector const& cs, bool is_redundant) {
s.add_axiom(name, cs, is_redundant);
}
std::ostream& core::display(std::ostream& out) const {
if (m_constraint_index.empty() && m_vars.empty())
return out;
@ -480,14 +476,6 @@ namespace polysat {
assign_eh(idx, false, 0);
}
bool core::add_clause(char const* name, core_vector const& cs, bool is_redundant) {
for (auto e : cs)
if (std::holds_alternative<signed_constraint>(e) && eval(*std::get_if<signed_constraint>(&e)) == l_true)
return false;
return s.add_polysat_clause(name, cs, is_redundant);
}
signed_constraint core::get_constraint(constraint_id idx) {
auto [sc, d, value] = m_constraint_index[idx.id];
SASSERT(value != l_undef);

13
src/sat/smt/polysat/core.h
View file

@ -89,10 +89,7 @@ namespace polysat {
void add_watch(unsigned idx, unsigned var);
lbool eval(signed_constraint const& sc);
constraint_id_vector explain_eval(signed_constraint const& sc);
dependency_vector get_dependencies(constraint_id_vector const& cc);
dependency_vector get_dependencies(std::initializer_list<constraint_id> const& cc);
sat::check_result final_check();
constraint_id find_conflicting_constraint();
@ -138,7 +135,7 @@ namespace polysat {
* In other words, the clause represents the formula /\ d_i -> \/ sc_j
* Where d_i are logical interpretations of dependencies and sc_j are signed constraints.
*/
bool add_clause(char const* name, core_vector const& cs, bool is_redundant);
void add_axiom(char const* name, core_vector const& cs, bool is_redundant);
pvar add_var(unsigned sz);
pdd var(pvar p) { return m_vars[p]; }
@ -156,9 +153,11 @@ namespace polysat {
constraint_id_vector const& unsat_core() const { return m_unsat_core; }
constraint_id_vector const& assigned_constraints() const { return m_prop_queue; }
dependency get_dependency(constraint_id idx) const;
dependency_vector get_dependencies(constraint_id_vector const& ids) const;
lbool eval(constraint_id id);
bool propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, get_dependencies(ids)); }
bool propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& ids) { return s.propagate(sc, get_dependencies(ids)); }
bool propagate(signed_constraint const& sc, constraint_id_vector const& ids) { return s.propagate(sc, ids); }
lbool eval(signed_constraint const& sc);
constraint_id_vector explain_eval(signed_constraint const& sc);
/*
* Constraints

98
src/sat/smt/polysat/op_constraint.cpp
View file

@ -272,25 +272,25 @@ namespace polysat {
auto& C = c.cs();
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
c.add_clause("lshr 1", { C.ule(r, p) }, false);
c.add_axiom("lshr 1", { C.ule(r, p) }, false);
else if (qv.is_val() && qv.val() >= N && rv.is_val() && !rv.is_zero())
// TODO: instead of rv.is_val() && !rv.is_zero(), we should use !is_forced_zero(r) which checks whether eval(r) = 0 or bvalue(r=0) = true; see saturation.cpp
c.add_clause("q >= N -> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
c.add_axiom("q >= N -> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv)
c.add_clause("q = 0 -> p = r", { ~C.eq(q), C.eq(p, r) } , true);
c.add_axiom("q = 0 -> p = r", { ~C.eq(q), C.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())
c.add_clause("q != 0 & p > 0 -> r < p", { C.eq(q), C.ule(p, 0), C.ult(r, p) }, true);
c.add_axiom("q != 0 & p > 0 -> r < p", { C.eq(q), C.ule(p, 0), C.ult(r, p) }, true);
else if (qv.is_val() && !qv.is_zero() && qv.val() < N && rv.is_val() && rv.val() > rational::power_of_two(N - qv.val().get_unsigned()) - 1)
c.add_clause("q >= k -> r <= 2^{N-k} - 1", { ~C.ule(qv.val(), q), C.ule(r, rational::power_of_two(N - qv.val().get_unsigned()) - 1)}, true);
c.add_axiom("q >= k -> r <= 2^{N-k} - 1", { ~C.ule(qv.val(), q), C.ule(r, rational::power_of_two(N - qv.val().get_unsigned()) - 1)}, true);
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
unsigned k = qv.val().get_unsigned();
for (unsigned i = 0; i < N - k; ++i) {
if (rv.val().get_bit(i) && !pv.val().get_bit(i + k))
c.add_clause("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i), C.bit(p, i + k) }, true);
c.add_axiom("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i), C.bit(p, i + k) }, true);
if (!rv.val().get_bit(i) && pv.val().get_bit(i + k))
c.add_clause("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i), ~C.bit(p, i + k) }, true);
c.add_axiom("q = k -> r[i] = p[i+k] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i), ~C.bit(p, i + k) }, true);
}
}
else {
@ -301,12 +301,12 @@ namespace polysat {
rational const& q_val = qv.val();
if (q_val >= N)
// q >= N ==> r = 0
c.add_clause("q >= N ==> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
c.add_axiom("q >= N ==> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
else if (pv.is_val()) {
SASSERT(q_val.is_unsigned());
//
rational const r_val = machine_div2k(pv.val(), q_val.get_unsigned());
c.add_clause("p = p_val & q = q_val ==> r = p_val / 2^q_val", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, r_val) }, true);
c.add_axiom("p = p_val & q = q_val ==> r = p_val / 2^q_val", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, r_val) }, true);
}
}
}
@ -316,9 +316,9 @@ namespace polysat {
auto& m = p.manager();
unsigned const N = m.power_of_2();
auto& C = c.cs();
c.add_clause("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, false);
c.add_clause("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, false);
c.add_clause("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, false);
c.add_axiom("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, false);
c.add_axiom("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, false);
c.add_axiom("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, false);
}
@ -326,8 +326,8 @@ namespace polysat {
auto x = p, y = q;
auto& C = c.cs();
c.add_clause("band-mask p&q <= p", { C.ule(r, p) }, false);
c.add_clause("band-mask p&q <= q", { C.ule(r, q) }, false);
c.add_axiom("band-mask p&q <= p", { C.ule(r, p) }, false);
c.add_axiom("band-mask p&q <= q", { C.ule(r, q) }, false);
if (x.is_val())
std::swap(x, y);
@ -338,15 +338,15 @@ namespace polysat {
if (!(yv + 1).is_power_of_two())
return;
if (yv == m.max_value())
c.add_clause("band-mask-true", { C.eq(x, r) }, false);
c.add_axiom("band-mask-true", { C.eq(x, r) }, false);
else if (yv == 0)
c.add_clause("band-mask-false", { C.eq(r) }, false);
c.add_axiom("band-mask-false", { C.eq(r) }, false);
else {
unsigned N = m.power_of_2();
unsigned k = yv.get_num_bits();
SASSERT(k < N);
rational exp = rational::power_of_two(N - k);
c.add_clause("band-mask 1", { C.eq(x * exp, r * exp) }, false);
c.add_axiom("band-mask 1", { C.eq(x * exp, r * exp) }, false);
}
}
@ -384,9 +384,9 @@ namespace polysat {
rational twoK = rational::power_of_two(k);
rational twoNk = rational::power_of_two(N - k);
auto eqK = C.eq(q, k);
c.add_clause("q = k -> r*2^k + p < 2^k", { ~eqK, C.ult(p - r * twoK, twoK) }, true);
c.add_clause("q = k & p >= 0 -> r < 2^{N-k}", { ~eqK, ~C.ule(0, p), C.ult(r, twoNk) }, true);
c.add_clause("q = k & p < 0 -> r >= 2^N - 2^{N-k}", { ~eqK, ~C.slt(p, 0), C.uge(r, twoN - twoNk) }, true);
c.add_axiom("q = k -> r*2^k + p < 2^k", { ~eqK, C.ult(p - r * twoK, twoK) }, true);
c.add_axiom("q = k & p >= 0 -> r < 2^{N-k}", { ~eqK, ~C.ule(0, p), C.ult(r, twoNk) }, true);
c.add_axiom("q = k & p < 0 -> r >= 2^N - 2^{N-k}", { ~eqK, ~C.slt(p, 0), C.uge(r, twoN - twoNk) }, true);
}
}
@ -409,24 +409,24 @@ namespace polysat {
auto& C = c.cs();
if (qv.is_val() && qv.val() >= N && rv.is_val() && !rv.is_zero())
c.add_clause("q >= N -> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
c.add_axiom("q >= N -> r = 0", { ~C.ule(N, q), C.eq(r) }, true);
else if (qv.is_zero() && pv.is_val() && rv.is_val() && rv != pv)
//
c.add_clause("q = 0 -> r = p", { ~C.eq(q), C.eq(r, p) }, true);
c.add_axiom("q = 0 -> r = p", { ~C.eq(q), C.eq(r, p) }, true);
else if (qv.is_val() && !qv.is_zero() && qv.val() < N && 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)
c.add_clause("q >= k -> r - 1 >= 2^k - 1", { ~C.ule(qv.val(), q), C.ule(rational::power_of_two(qv.val().get_unsigned()) - 1, r - 1) }, true);
c.add_axiom("q >= k -> r - 1 >= 2^k - 1", { ~C.ule(qv.val(), q), C.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 k = qv.val().get_unsigned();
// q = k -> r[i+k] = p[i] for 0 <= i < N - k
for (unsigned i = 0; i < N - k; ++i) {
if (rv.val().get_bit(i + k) && !pv.val().get_bit(i)) {
c.add_clause("q = k -> r[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true);
c.add_axiom("q = k -> r[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), ~C.bit(r, i + k), C.bit(p, i) }, true);
}
if (!rv.val().get_bit(i + k) && pv.val().get_bit(i)) {
c.add_clause("q = k -> r[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true);
c.add_axiom("q = k -> r[i+k] = p[i] for 0 <= i < N - k", { ~C.eq(q, k), C.bit(r, i + k), ~C.bit(p, i) }, true);
}
}
}
@ -438,12 +438,12 @@ namespace polysat {
rational const& q_val = qv.val();
if (q_val >= N)
// q >= N ==> r = 0
c.add_clause("shl forward 1", {~C.ule(N, q), C.eq(r)}, true);
c.add_axiom("shl forward 1", {~C.ule(N, q), C.eq(r)}, true);
if (pv.is_val()) {
SASSERT(q_val.is_unsigned());
// p = p_val & q = q_val ==> r = p_val * 2^q_val
rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned());
c.add_clause("shl forward 2", {~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, r_val)}, true);
c.add_axiom("shl forward 2", {~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, r_val)}, true);
}
}
}
@ -470,31 +470,31 @@ namespace polysat {
auto& C = c.cs();
if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
c.add_clause("p&q <= p", { C.ule(r, p) }, true);
c.add_axiom("p&q <= p", { C.ule(r, p) }, true);
else if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
c.add_clause("p&q <= q", { C.ule(r, q) }, true);
c.add_axiom("p&q <= q", { C.ule(r, q) }, true);
else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
c.add_clause("p = q => r = p", { ~C.eq(p, q), C.eq(r, p) }, true);
c.add_axiom("p = q => r = p", { ~C.eq(p, q), C.eq(r, p) }, true);
else if (pv.is_val() && qv.is_val() && rv.is_val()) {
if (pv.is_max() && qv != rv)
c.add_clause("p = -1 => r = q", { ~C.eq(p, m.max_value()), C.eq(q, r) }, true);
c.add_axiom("p = -1 => r = q", { ~C.eq(p, m.max_value()), C.eq(q, r) }, true);
if (qv.is_max() && pv != rv)
c.add_clause("q = -1 => r = p", { ~C.eq(q, m.max_value()), C.eq(p, r) }, true);
c.add_axiom("q = -1 => r = p", { ~C.eq(q, m.max_value()), C.eq(p, r) }, true);
unsigned const N = m.power_of_2();
unsigned pow;
if ((pv.val() + 1).is_power_of_two(pow)) {
if (rv.is_zero() && !qv.is_zero() && qv.val() <= pv.val())
c.add_clause("p = 2^k - 1 && r = 0 && q != 0 => q >= 2^k", { ~C.eq(p, pv), ~C.eq(r), C.eq(q), C.ule(pv + 1, q) }, true);
c.add_axiom("p = 2^k - 1 && r = 0 && q != 0 => q >= 2^k", { ~C.eq(p, pv), ~C.eq(r), C.eq(q), C.ule(pv + 1, q) }, true);
if (rv != qv)
c.add_clause("p = 2^k - 1 ==> r*2^{N - k} = q*2^{N - k}", { ~C.eq(p, pv), C.eq(r * rational::power_of_two(N - pow), q * rational::power_of_two(N - pow)) }, true);
c.add_axiom("p = 2^k - 1 ==> r*2^{N - k} = q*2^{N - k}", { ~C.eq(p, pv), C.eq(r * rational::power_of_two(N - pow), q * rational::power_of_two(N - pow)) }, true);
}
if ((qv.val() + 1).is_power_of_two(pow)) {
if (rv.is_zero() && !pv.is_zero() && pv.val() <= qv.val())
c.add_clause("q = 2^k - 1 && r = 0 && p != 0 ==> p >= 2^k", { ~C.eq(q, qv), ~C.eq(r), C.eq(p), C.ule(qv + 1, p) }, true);
c.add_axiom("q = 2^k - 1 && r = 0 && p != 0 ==> p >= 2^k", { ~C.eq(q, qv), ~C.eq(r), C.eq(p), C.ule(qv + 1, p) }, true);
//
if (rv != pv)
c.add_clause("q = 2^k - 1 ==> r*2^{N - k} = p*2^{N - k}", { ~C.eq(q, qv), C.eq(r * rational::power_of_two(N - pow), p * rational::power_of_two(N - pow)) }, true);
c.add_axiom("q = 2^k - 1 ==> r*2^{N - k} = p*2^{N - k}", { ~C.eq(q, qv), C.eq(r * rational::power_of_two(N - pow), p * rational::power_of_two(N - pow)) }, true);
}
for (unsigned i = 0; i < N; ++i) {
@ -504,11 +504,11 @@ namespace polysat {
if (rb == (pb && qb))
continue;
if (pb && qb && !rb)
c.add_clause("p&q[i] = p[i]&q[i]", { ~C.bit(p, i), ~C.bit(q, i), C.bit(r, i) }, true);
c.add_axiom("p&q[i] = p[i]&q[i]", { ~C.bit(p, i), ~C.bit(q, i), C.bit(r, i) }, true);
else if (!pb && rb)
c.add_clause("p&q[i] = p[i]&q[i]", { C.bit(p, i), ~C.bit(r, i) }, true);
c.add_axiom("p&q[i] = p[i]&q[i]", { C.bit(p, i), ~C.bit(r, i) }, true);
else if (!qb && rb)
c.add_clause("p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) }, true);
c.add_axiom("p&q[i] = p[i]&q[i]", { C.bit(q, i), ~C.bit(r, i) }, true);
else
UNREACHABLE();
}
@ -517,14 +517,14 @@ namespace polysat {
// Propagate r if p or q are 0
else if (pv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
c.add_clause("p = 0 -> p&q = 0", { C.ule(r, p) }, true);
c.add_axiom("p = 0 -> p&q = 0", { C.ule(r, p) }, true);
else if (qv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
c.add_clause("q = 0 -> p&q = 0", { C.ule(r, q) }, true);
c.add_axiom("q = 0 -> p&q = 0", { C.ule(r, q) }, true);
// p = a && q = b ==> r = a & b
else if (pv.is_val() && qv.is_val() && !rv.is_val()) {
// Just assign by this very weak justification. It will be strengthened in saturation in case of a conflict
LOG(p << " = " << pv << " and " << q << " = " << qv << " yields [band] " << r << " = " << bitwise_and(pv.val(), qv.val()));
c.add_clause("p = a & q = b => r = a&b", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, bitwise_and(pv.val(), qv.val())) }, true);
c.add_axiom("p = a & q = b => r = a&b", { ~C.eq(p, pv), ~C.eq(q, qv), C.eq(r, bitwise_and(pv.val(), qv.val())) }, true);
}
}
@ -569,15 +569,15 @@ namespace polysat {
// p = 0 ==> r = 0
if (pv.is_zero())
c.add_clause(~invc, ~C.eq(p), C.eq(r), true);
c.add_axiom(~invc, ~C.eq(p), C.eq(r), true);
// r = 0 ==> p = 0
if (rv.is_zero())
c.add_clause(~invc, ~C.eq(r), C.eq(p), true);
c.add_axiom(~invc, ~C.eq(r), C.eq(p), true);
// forward propagation: p assigned ==> r = pseudo_inverse(eval(p))
// TODO: (later) this should be propagated instead of adding a clause
/*if (pv.is_val() && !rv.is_val())
c.add_clause(~invc, ~C.eq(p, pv), C.eq(r, pv.val().pseudo_inverse(m.power_of_2())), true);*/
c.add_axiom(~invc, ~C.eq(p, pv), C.eq(r, pv.val().pseudo_inverse(m.power_of_2())), true);*/
if (!pv.is_val() || !rv.is_val())
return {};
@ -590,7 +590,7 @@ namespace polysat {
// p != 0 ==> odd(r)
if (parity_rv != 0)
c.add_clause("r = inv p & p != 0 ==> odd(r)", {~invc, C.eq(p), s.odd(r)}, true);
c.add_axiom("r = inv p & p != 0 ==> odd(r)", {~invc, C.eq(p), s.odd(r)}, true);
pdd prod = p * r;
rational prodv = (pv * rv).val();
@ -606,12 +606,12 @@ namespace polysat {
LOG("Its in [" << lower << "; " << upper << ")");
// parity(p) >= k ==> p * r >= 2^k
if (prodv < rational::power_of_two(middle))
c.add_clause("r = inv p & parity(p) >= k ==> p*r >= 2^k",
c.add_axiom("r = inv p & parity(p) >= k ==> p*r >= 2^k",
{~invc, ~s.parity_at_least(p, middle), s.uge(prod, rational::power_of_two(middle))}, false);
// parity(p) >= k ==> r <= 2^(N - k) - 1 (because r is the smallest pseudo-inverse)
rational const max_rv = rational::power_of_two(m.power_of_2() - middle) - 1;
if (rv.val() > max_rv)
c.add_clause("r = inv p & parity(p) >= k ==> r <= 2^(N - k) - 1",
c.add_axiom("r = inv p & parity(p) >= k ==> r <= 2^(N - k) - 1",
{~invc, ~s.parity_at_least(p, middle), C.ule(r, max_rv)}, false);
}
else { // parity less than middle
@ -620,7 +620,7 @@ namespace polysat {
LOG("Its in [" << lower << "; " << upper << ")");
// parity(p) < k ==> p * r <= 2^k - 1
if (prodv > rational::power_of_two(middle))
c.add_clause("r = inv p & parity(p) < k ==> p*r <= 2^k - 1",
c.add_axiom("r = inv p & parity(p) < k ==> p*r <= 2^k - 1",
{~invc, s.parity_at_least(p, middle), C.ule(prod, rational::power_of_two(middle) - 1)}, false);
}
}

31
src/sat/smt/polysat/saturation.cpp
View file

@ -34,11 +34,6 @@ namespace polysat {
saturation::saturation(core& c) : c(c), C(c.cs()) {}
void saturation::propagate(pvar v) {
for (auto id : c.unsat_core())
propagate(v, id);
}
bool saturation::propagate(pvar v, constraint_id id) {
if (c.eval(id) == l_true)
return false;
@ -62,13 +57,27 @@ namespace polysat {
}
void saturation::propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises) {
if (c.propagate(sc, premises))
if (c.propagate(sc, constraint_id_vector(premises)))
m_propagated = true;
}
void saturation::add_clause(char const* name, core_vector const& cs, bool is_redundant) {
if (c.add_clause(name, cs, is_redundant))
m_propagated = true;
void saturation::add_clause(char const* name, clause const& cs, bool is_redundant) {
vector<std::variant<constraint_id, dependency>> core;
for (auto const& e : cs) {
if (std::holds_alternative<constraint_id>(e)) {
core.push_back(*std::get_if<constraint_id>(&e));
continue;
}
auto sc = *std::get_if<signed_constraint>(&e);
if (c.eval(sc) != l_false)
return;
c.propagate(~sc, c.explain_eval(sc));
// retrieve dep/id from propagated ~sc
// add to id to ids or ~dep to deps
}
// TODO
//
// c.add_axiom(name, core_vector(core.begin(), core.end()), is_redundant);
}
bool saturation::match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id_out) {
@ -128,9 +137,9 @@ namespace polysat {
auto ovfl = C.umul_ovfl(x, y);
if (i.is_strict())
add_clause("[x] yx < zx ==> Ω*(x,y) \\/ y < z", { i.dep(), ovfl, C.ult(y, z)}, false);
add_clause("[x] yx < zx ==> Ω*(x,y) \\/ y < z", { i.id(), ovfl, C.ult(y, z)}, false);
else
add_clause("[x] yx <= zx ==> Ω*(x,y) \\/ y <= z \\/ x = 0", { i.dep(), ovfl, C.eq(x), C.ule(y, z) }, false);
add_clause("[x] yx <= zx ==> Ω*(x,y) \\/ y <= z \\/ x = 0", { i.id(), ovfl, C.eq(x), C.ule(y, z) }, false);
}
/**

3
src/sat/smt/polysat/saturation.h
View file

@ -23,6 +23,7 @@ namespace polysat {
*/
class saturation {
using clause = std::initializer_list<std::variant<constraint_id, signed_constraint>>;
core& c;
constraints& C;
char const* m_rule = nullptr;
@ -30,7 +31,7 @@ namespace polysat {
void set_rule(char const* r) { m_rule = r; }
void propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises);
void add_clause(char const* name, core_vector const& cs, bool is_redundant);
void add_clause(char const* name, clause const& cs, bool is_redundant);
bool match_core(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);
bool match_constraints(std::function<bool(signed_constraint const& sc)> const& p, constraint_id& id);

10
src/sat/smt/polysat/types.h
View file

@ -84,6 +84,7 @@ namespace polysat {
using core_vector = std::initializer_list<std::variant<signed_constraint, dependency>>;
using constraint_id_vector = svector<constraint_id>;
using constraint_ids = std::initializer_list<constraint_id>;
//
@ -94,11 +95,10 @@ namespace polysat {
public:
virtual ~solver_interface() {}
virtual void add_eq_literal(pvar v, rational const& val) = 0;
virtual void set_conflict(dependency_vector const& core) = 0;
virtual void set_lemma(core_vector const& aux_core, dependency_vector const& core) = 0;
virtual bool add_polysat_clause(char const* name, core_vector cs, bool redundant) = 0;
virtual bool propagate(signed_constraint sc, dependency_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;
virtual bool add_axiom(char const* name, core_vector const& core, bool redundant) = 0;
virtual void set_conflict(constraint_id_vector const& core) = 0;
virtual bool propagate(signed_constraint sc, constraint_id_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;
virtual trail_stack& trail() = 0;
virtual bool inconsistent() const = 0;
virtual void get_bitvector_suffixes(pvar v, pvar_vector& out) = 0;

4
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -346,8 +346,8 @@ namespace polysat {
auto q = c.subst(rhs());
auto& C = c.cs();
if (sign && !lhs().is_val() && !rhs().is_val()) {
c.add_clause("lhs > rhs ==> -1 > rhs", { d, C.ult(rhs(), -1) }, false);
c.add_clause("lhs > rhs ==> lhs > 0", { d, C.ult(0, lhs()) }, false);
c.add_axiom("lhs > rhs ==> -1 > rhs", { d, C.ult(rhs(), -1) }, false);
c.add_axiom("lhs > rhs ==> lhs > 0", { d, C.ult(0, lhs()) }, false);
}
}

4
src/sat/smt/polysat/umul_ovfl_constraint.cpp
View file

@ -138,7 +138,7 @@ namespace polysat {
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_clause("~Ovfl(p, q) & p <= p_bound ==> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, false);
c.add_axiom("~Ovfl(p, q) & p <= p_bound ==> q < q_bound", { d, ~C.ule(p0, p_bound), C.ule(q_bound, q0) }, false);
}
else {
// Find lowest bound for p such that q_bound is still correct.
@ -148,7 +148,7 @@ namespace polysat {
SASSERT(p_bound * q_bound >= M);
SASSERT(p_bound * (q_bound - 1) < M);
// LOG("p_bound: " << p.manager().mk_val(p_bound));
c.add_clause("~Ovfl(p, q) & p >= p_bound ==> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, false);
c.add_axiom("~Ovfl(p, q) & p >= p_bound ==> q < q_bound", { d, ~C.ule(p_bound, p0), C.ult(q0, q_bound) }, false);
}
return true;
}

10
src/sat/smt/polysat_internalize.cpp
View file

@ -519,18 +519,18 @@ namespace polysat {
// b = 0 ==> q = -1
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
// Maybe we need something like an op_constraint for better propagation.
add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false);
add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false);
add_axiom("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false);
add_axiom("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false);
// r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1
add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false);
add_axiom("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false);
auto c_eq = m_core.eq(b);
if (!c_eq.is_always_true())
add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false);
add_axiom("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false);
if (!c_eq.is_always_false())
add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
add_axiom("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
}
void solver::internalize_sign_extend(app* e) {

46
src/sat/smt/polysat_solver.cpp
View file

@ -105,8 +105,10 @@ namespace polysat {
m_core.assign_eh(a->m_index, l.sign(), s().lvl(l));
}
void solver::set_conflict(dependency_vector const& core) {
auto [lits, eqs] = explain_deps(core);
// TBD: add also lemma
void solver::set_conflict(constraint_id_vector const& core) {
auto deps = m_core.get_dependencies(core);
auto [lits, eqs] = explain_deps(deps);
auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
ctx.set_conflict(ex);
}
@ -142,38 +144,6 @@ namespace polysat {
return { core, eqs };
}
void solver::set_lemma(core_vector const& aux_core, dependency_vector const& core) {
auto [lits, eqs] = explain_deps(core);
unsigned level = 0;
for (auto const& [n1, n2] : eqs)
ctx.get_eq_antecedents(n1, n2, lits);
for (auto lit : lits)
level = std::max(level, s().lvl(lit));
auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
if (level == 0) {
ctx.set_conflict(ex);
return;
}
ctx.push(value_trail<bool>(m_has_lemma));
m_has_lemma = true;
m_lemma_level = level;
m_lemma.reset();
for (auto sc : aux_core) {
if (std::holds_alternative<dependency>(sc)) {
auto d = *std::get_if<dependency>(&sc);
if (d.is_literal())
m_lemma.push_back(ctx.literal2expr(d.literal()));
else {
auto [v1, v2] = d.eq();
m_lemma.push_back(ctx.mk_eq(var2enode(v1), var2enode(v2)));
}
}
else if (std::holds_alternative<signed_constraint>(sc))
m_lemma.push_back(constraint2expr(*std::get_if<signed_constraint>(&sc)));
}
ctx.set_conflict(ex);
}
// If an MCSat lemma is added, then backjump based on the lemma level and
// add the lemma to the solver with potentially fresh literals.
// return l_false to signal sat::solver that backjumping has been taken care of internally.
@ -238,17 +208,19 @@ namespace polysat {
// Core uses the propagate callback to add unit propagations to the trail.
// The polysat::solver takes care of translating signed constraints into expressions, which translate into literals.
// Everything goes over expressions/literals. polysat::core is not responsible for replaying expressions.
bool solver::propagate(signed_constraint sc, dependency_vector const& deps) {
bool solver::propagate(signed_constraint sc, constraint_id_vector const& cs) {
sat::literal lit = ctx.mk_literal(constraint2expr(sc));
if (s().value(lit) == l_true)
return false;
auto deps = m_core.get_dependencies(cs);
auto [core, eqs] = explain_deps(deps);
auto ex = euf::th_explain::propagate(*this, core, eqs, lit, nullptr);
ctx.propagate(lit, ex);
return true;
}
void solver::propagate(dependency const& d, bool sign, dependency_vector const& deps) {
void solver::propagate(dependency const& d, bool sign, constraint_id_vector const& cs) {
auto deps = m_core.get_dependencies(cs);
auto [core, eqs] = explain_deps(deps);
if (d.is_literal()) {
auto lit = d.literal();
@ -278,7 +250,7 @@ namespace polysat {
return ctx.get_trail_stack();
}
bool solver::add_polysat_clause(char const* name, core_vector cs, bool is_redundant) {
bool solver::add_axiom(char const* name, core_vector const& cs, bool is_redundant) {
sat::literal_vector lits;
for (auto e : cs) {
if (std::holds_alternative<dependency>(e)) {

9
src/sat/smt/polysat_solver.h
View file

@ -160,15 +160,14 @@ namespace polysat {
// callbacks from core
void add_eq_literal(pvar v, rational const& val) override;
void set_conflict(dependency_vector const& core) override;
void set_lemma(core_vector const& aux_core, dependency_vector const& core) override;
bool propagate(signed_constraint sc, dependency_vector const& deps) override;
void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
void set_conflict(constraint_id_vector const& core) override;
bool add_axiom(char const* name, core_vector const& core, bool redundant) override;
bool propagate(signed_constraint sc, constraint_id_vector const& deps) override;
void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
trail_stack& trail() override;
bool inconsistent() const override;
void get_bitvector_suffixes(pvar v, pvar_vector& out) override;
void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) override;
bool add_polysat_clause(char const* name, core_vector cs, bool redundant) override;
std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);