mirror of
https://github.com/Z3Prover/z3
synced 2025-06-26 15:53:41 +00:00
fixes, updates
This commit is contained in:
parent
57324e953e
commit
10d56d9af9
5 changed files with 62 additions and 72 deletions
|
@ -374,6 +374,11 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (v == null_var && weak_eval(sc) == l_false) {
|
else if (v == null_var && weak_eval(sc) == l_false) {
|
||||||
|
saturation sat(*this);
|
||||||
|
if (sat(idx) == l_false) {
|
||||||
|
verbose_stream() << "Saturated conflict " << ~sc << "\n";
|
||||||
|
return;
|
||||||
|
}
|
||||||
auto ex = explain_weak_eval(sc);
|
auto ex = explain_weak_eval(sc);
|
||||||
ex.push_back(dep);
|
ex.push_back(dep);
|
||||||
verbose_stream() << "infeasible propagation " << ~sc << " <- " << ex << "\n";
|
verbose_stream() << "infeasible propagation " << ~sc << " <- " << ex << "\n";
|
||||||
|
|
|
@ -61,21 +61,17 @@ namespace polysat {
|
||||||
shuffle(m_to_refine.size(), m_to_refine.data(), c.rand());
|
shuffle(m_to_refine.size(), m_to_refine.data(), c.rand());
|
||||||
if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return prefix_overflow(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
|
|
||||||
if (any_of(m_to_refine, [&](auto i) { return mul0(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return mul0(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return mul1(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
if (any_of(m_to_refine, [&](auto i) { return mul_parametric_inverse(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return mul_parametric_inverse(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
|
|
||||||
if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
|
|
||||||
return l_false;
|
|
||||||
if (any_of(m_to_refine, [&](auto i) { return mul0_inverse(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return mul0_inverse(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
if (false && any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
if (false && any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return mul1_inverse(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); }))
|
if (any_of(m_to_refine, [&](auto i) { return non_overflow_monotone(m_monomials[i]); }))
|
||||||
return l_false;
|
return l_false;
|
||||||
|
@ -172,7 +168,6 @@ namespace polysat {
|
||||||
}
|
}
|
||||||
|
|
||||||
// p * q = p => parity(q - 1) + parity(p) >= N
|
// p * q = p => parity(q - 1) + parity(p) >= N
|
||||||
// p * q = p & ~Ovfl(p,q) => q = 1 or p = 0
|
|
||||||
bool monomials::mul_parametric_inverse(monomial const& mon) {
|
bool monomials::mul_parametric_inverse(monomial const& mon) {
|
||||||
for (unsigned j = mon.size(); j-- > 0; ) {
|
for (unsigned j = mon.size(); j-- > 0; ) {
|
||||||
auto const& arg_val = mon.arg_vals[j];
|
auto const& arg_val = mon.arg_vals[j];
|
||||||
|
@ -197,16 +192,16 @@ namespace polysat {
|
||||||
if (c.add_axiom("p * q = p => parity(q - 1) + parity(p) >= N", { ~C.eq(mon.var, p), ~C.parity_at_most(p, pb), C.parity_at_least(qs - 1, N - pb) }, true))
|
if (c.add_axiom("p * q = p => parity(q - 1) + parity(p) >= N", { ~C.eq(mon.var, p), ~C.parity_at_most(p, pb), C.parity_at_least(qs - 1, N - pb) }, true))
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
if (c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true))
|
|
||||||
return true;
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
// parity p >= i => parity p * q >= i
|
// parity p * q = min(N, parity(p) + parity(q))
|
||||||
bool monomials::parity(monomial const& mon) {
|
bool monomials::parity(monomial const& mon) {
|
||||||
unsigned parity_val = get_parity(mon.val, mon.num_bits());
|
unsigned parity_val = get_parity(mon.val, mon.num_bits());
|
||||||
|
unsigned sum_parities = 0;
|
||||||
|
unsigned N = mon.var.manager().power_of_2();
|
||||||
for (unsigned j = 0; j < mon.args.size(); ++j) {
|
for (unsigned j = 0; j < mon.args.size(); ++j) {
|
||||||
unsigned k = get_parity(mon.arg_vals[j], mon.num_bits());
|
unsigned k = get_parity(mon.arg_vals[j], mon.num_bits());
|
||||||
if (k > parity_val) {
|
if (k > parity_val) {
|
||||||
|
@ -214,8 +209,25 @@ namespace polysat {
|
||||||
if (c.add_axiom("parity p >= i => parity p * q >= i", { ~C.parity_at_least(p, k), C.parity_at_least(mon.var, k) }, true))
|
if (c.add_axiom("parity p >= i => parity p * q >= i", { ~C.parity_at_least(p, k), C.parity_at_least(mon.var, k) }, true))
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
sum_parities += k;
|
||||||
}
|
}
|
||||||
return false;
|
if (sum_parities == parity_val)
|
||||||
|
return false;
|
||||||
|
if (sum_parities >= N && N == parity_val)
|
||||||
|
return false;
|
||||||
|
if (sum_parities > parity_val) {
|
||||||
|
constraint_or_dependency_vector clause;
|
||||||
|
for (unsigned j = 0; j < mon.args.size(); ++j)
|
||||||
|
clause.push_back(~C.parity_at_least(mon.args[j], get_parity(mon.arg_vals[j], mon.num_bits())));
|
||||||
|
clause.push_back(C.parity_at_least(mon.var, sum_parities));
|
||||||
|
return c.add_axiom("N >= pp + qp, pp >= parity(p), qq >= parity(q) => parity p * q >= pp + qp)", clause, true);
|
||||||
|
}
|
||||||
|
// sum_parities < parity_val
|
||||||
|
constraint_or_dependency_vector clause;
|
||||||
|
clause.push_back(~C.parity_at_least(mon.var, sum_parities));
|
||||||
|
for (unsigned j = 0; j < mon.args.size(); ++j)
|
||||||
|
clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], mon.num_bits())));
|
||||||
|
return c.add_axiom("parity(p * q) > pp + qp => pp < parity(p) or qp < parity(q))", clause, true);
|
||||||
}
|
}
|
||||||
|
|
||||||
// ~ovfl*(p,q) & q != 0 => p <= p*q
|
// ~ovfl*(p,q) & q != 0 => p <= p*q
|
||||||
|
@ -247,21 +259,8 @@ namespace polysat {
|
||||||
return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
|
return c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
|
||||||
}
|
}
|
||||||
|
|
||||||
// p * q = 1 => parity(p) = 0 (instance of parity(p*q) >= min(N, parity(p) + parity(q))
|
|
||||||
// ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1
|
// ~ovfl*(p,q) & p*q = 1 => p = 1, q = 1
|
||||||
bool monomials::mul1_inverse(monomial const& mon) {
|
bool monomials::mul1_inverse(monomial const& mon) {
|
||||||
if (!mon.val.is_odd())
|
|
||||||
return false;
|
|
||||||
|
|
||||||
unsigned j = 0;
|
|
||||||
for (auto const& val : mon.arg_vals) {
|
|
||||||
if (val.is_even()) {
|
|
||||||
if (c.add_axiom("odd(p*q) => odd(p)",
|
|
||||||
{~C.parity_at_most(mon.var, 0), C.parity_at_most(mon.args[j], 0) }, true))
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
++j;
|
|
||||||
}
|
|
||||||
if (mon.val != 1)
|
if (mon.val != 1)
|
||||||
return false;
|
return false;
|
||||||
rational product(1);
|
rational product(1);
|
||||||
|
@ -288,43 +287,22 @@ namespace polysat {
|
||||||
|
|
||||||
|
|
||||||
// p*q = 0 => parity(p) + parity(q) >= N
|
// p*q = 0 => parity(p) + parity(q) >= N
|
||||||
// TODO: update to use parity instead of overflow
|
|
||||||
// ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0
|
|
||||||
bool monomials::mul0_inverse(monomial const& mon) {
|
bool monomials::mul0_inverse(monomial const& mon) {
|
||||||
if (mon.val != 0)
|
if (mon.val != 0)
|
||||||
return false;
|
return false;
|
||||||
for (auto const& val : mon.arg_vals)
|
|
||||||
if (val == 0)
|
unsigned sum_parities = 0;
|
||||||
return false;
|
unsigned N = mon.var.manager().power_of_2();
|
||||||
rational product(1);
|
for (unsigned j = 0; j < mon.args.size(); ++j)
|
||||||
for (auto const& val : mon.arg_vals)
|
sum_parities += get_parity(mon.arg_vals[j], mon.num_bits());
|
||||||
product *= val;
|
if (sum_parities >= N)
|
||||||
if (product > mon.var.manager().max_value())
|
|
||||||
return false;
|
return false;
|
||||||
constraint_or_dependency_vector clause;
|
constraint_or_dependency_vector clause;
|
||||||
clause.push_back(~C.eq(mon.var));
|
clause.push_back(~C.eq(mon.var));
|
||||||
pdd p = mon.args[0];
|
for (unsigned j = 0; j < mon.args.size(); ++j)
|
||||||
for (unsigned i = 1; i < mon.args.size(); ++i) {
|
clause.push_back(C.parity_at_least(mon.args[j], 1 + get_parity(mon.arg_vals[j], mon.num_bits())));
|
||||||
clause.push_back(C.umul_ovfl(p, mon.args[i]));
|
|
||||||
p *= mon.args[i];
|
|
||||||
}
|
|
||||||
for (auto const& q : mon.args)
|
|
||||||
clause.push_back(C.eq(q));
|
|
||||||
|
|
||||||
return c.add_axiom("~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0", clause, true);
|
return c.add_axiom("p*q = 0 & pp + qq < N => parity(p) > pp or parity(q) > qp", clause, true);
|
||||||
}
|
|
||||||
|
|
||||||
// parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0
|
|
||||||
bool monomials::parity0(monomial const& mon) {
|
|
||||||
if (mon.val.is_odd())
|
|
||||||
return false;
|
|
||||||
if (!all_of(mon.arg_vals, [&](auto const& v) { return v.is_odd(); }))
|
|
||||||
return false;
|
|
||||||
constraint_or_dependency_vector clause;
|
|
||||||
clause.push_back(~C.parity_at_least(mon.var, 1));
|
|
||||||
for (auto const& p : mon.args)
|
|
||||||
clause.push_back(C.parity_at_least(p, 1));
|
|
||||||
return c.add_axiom("parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0", clause, true);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// 0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k
|
// 0p * 0q >= 2^k => ovfl(p,q), where |p| = |q| = k
|
||||||
|
|
|
@ -55,7 +55,6 @@ namespace polysat {
|
||||||
bool non_overflow_monotone(monomial const& mon);
|
bool non_overflow_monotone(monomial const& mon);
|
||||||
bool mul1_inverse(monomial const& mon);
|
bool mul1_inverse(monomial const& mon);
|
||||||
bool mul0_inverse(monomial const& mon);
|
bool mul0_inverse(monomial const& mon);
|
||||||
bool parity0(monomial const& mon);
|
|
||||||
bool prefix_overflow(monomial const& mon);
|
bool prefix_overflow(monomial const& mon);
|
||||||
|
|
||||||
bool bit_blast(monomial const& mon);
|
bool bit_blast(monomial const& mon);
|
||||||
|
|
|
@ -35,16 +35,23 @@ namespace polysat {
|
||||||
TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
|
TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
|
||||||
|
|
||||||
has_conflict = true;
|
has_conflict = true;
|
||||||
auto vars = c.find_conflict_variables(idx);
|
if (l_false == operator()(idx))
|
||||||
for (auto v : vars)
|
return l_false;
|
||||||
if (resolve(v, idx))
|
|
||||||
return l_false;
|
|
||||||
}
|
}
|
||||||
if (has_conflict)
|
if (has_conflict)
|
||||||
return l_undef;
|
return l_undef;
|
||||||
return l_true;
|
return l_true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
lbool saturation::operator()(constraint_id idx) {
|
||||||
|
auto sc = c.get_constraint(idx);
|
||||||
|
auto vars = c.find_conflict_variables(idx);
|
||||||
|
for (auto v : vars)
|
||||||
|
if (resolve(v, idx))
|
||||||
|
return l_false;
|
||||||
|
return l_undef;
|
||||||
|
}
|
||||||
|
|
||||||
bool saturation::resolve(pvar v, constraint_id id) {
|
bool saturation::resolve(pvar v, constraint_id id) {
|
||||||
auto sc = c.get_constraint(id);
|
auto sc = c.get_constraint(id);
|
||||||
if (!sc.unfold_vars().contains(v))
|
if (!sc.unfold_vars().contains(v))
|
||||||
|
@ -209,12 +216,12 @@ namespace polysat {
|
||||||
/**
|
/**
|
||||||
* Expand the following axioms:
|
* Expand the following axioms:
|
||||||
* Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}
|
* Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}
|
||||||
* Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 2
|
* Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1
|
||||||
* Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 2 => 0x * 0y >= 2^N
|
* Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2^N
|
||||||
*
|
*
|
||||||
* ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}
|
* ~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}
|
||||||
* ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 2
|
* ~Ovfl(x,y) & msb(x) >= k => msb(y) <= N - k + 1
|
||||||
* ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 2 => 0x * 0y < 2^N
|
* ~Ovfl(x,y) & msb(x) >= k & msb(y) >= N - k + 1 => 0x * 0y < 2^N
|
||||||
*/
|
*/
|
||||||
void saturation::try_umul_blast(umul_ovfl const& sc) {
|
void saturation::try_umul_blast(umul_ovfl const& sc) {
|
||||||
auto x = sc.p();
|
auto x = sc.p();
|
||||||
|
@ -245,14 +252,14 @@ namespace polysat {
|
||||||
if (sc.sign()) {
|
if (sc.sign()) {
|
||||||
// Case ~Ovfl(x,y) is asserted by current assignment x * y is overflow
|
// Case ~Ovfl(x,y) is asserted by current assignment x * y is overflow
|
||||||
SASSERT(bx > 1 && by > 1);
|
SASSERT(bx > 1 && by > 1);
|
||||||
SASSERT(bx + by >= N + 2);
|
SASSERT(bx + by >= N + 1);
|
||||||
if (bx > (N + 1) / 2) {
|
if (bx > (N + 1) / 2) {
|
||||||
add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}",
|
add_clause("~Ovfl(x, y) & x <= y => x < 2^{(N + 1) div 2}",
|
||||||
{ d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) }, true);
|
{ d, ~C.ule(x, y), C.ult(x, rational::power_of_two((N + 1) / 2)) }, true);
|
||||||
}
|
}
|
||||||
else if (bx + by > N + 2)
|
else if (bx + by > N + 1)
|
||||||
add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k + 2",
|
add_clause("~Ovfl(x, y) & msb(x) >= k => msb(y) <= N - k + 1",
|
||||||
{d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 2)}, true);
|
{d, ~C.msb_ge(x, bx), C.msb_le(y, N - bx + 1)}, true);
|
||||||
else {
|
else {
|
||||||
auto x1 = c.mk_zero_extend(1, x);
|
auto x1 = c.mk_zero_extend(1, x);
|
||||||
auto y1 = c.mk_zero_extend(1, y);
|
auto y1 = c.mk_zero_extend(1, y);
|
||||||
|
@ -269,16 +276,16 @@ namespace polysat {
|
||||||
add_clause("Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}",
|
add_clause("Ovfl(x, y) & x <= y => y >= 2^{(N + 1) div 2}",
|
||||||
{ d, ~C.ule(x, y), C.uge(x, rational::power_of_two((N + 1) / 2)) }, true);
|
{ d, ~C.ule(x, y), C.uge(x, rational::power_of_two((N + 1) / 2)) }, true);
|
||||||
}
|
}
|
||||||
else if (bx + by < N + 2) {
|
else if (bx + by < N + 1) {
|
||||||
SASSERT(bx <= by);
|
SASSERT(bx <= by);
|
||||||
add_clause("Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 2",
|
add_clause("Ovfl(x, y) & msb(x) <= k => msb(y) >= N - k + 1",
|
||||||
{ d, ~C.msb_le(x, bx), C.msb_ge(y, N - bx + 2) }, true);
|
{ d, ~C.msb_le(x, bx), C.msb_ge(y, N - bx + 1) }, true);
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
auto x1 = c.mk_zero_extend(1, x);
|
auto x1 = c.mk_zero_extend(1, x);
|
||||||
auto y1 = c.mk_zero_extend(1, y);
|
auto y1 = c.mk_zero_extend(1, y);
|
||||||
add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 2 => 0x * 0y >= 2 ^ N",
|
add_clause("Ovfl(x, y) & msb(x) <= k & msb(y) <= N - k + 1 => 0x * 0y >= 2 ^ N",
|
||||||
{ d, ~C.msb_le(x, bx), ~C.msb_le(y, N - bx + 2), C.uge(x1 * y1, rational::power_of_two(N)) }, true);
|
{ d, ~C.msb_le(x, bx), ~C.msb_le(y, N - bx + 1), C.uge(x1 * y1, rational::power_of_two(N)) }, true);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -80,5 +80,6 @@ namespace polysat {
|
||||||
public:
|
public:
|
||||||
saturation(core& c);
|
saturation(core& c);
|
||||||
lbool operator()();
|
lbool operator()();
|
||||||
|
lbool operator()(constraint_id id);
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue