mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

add activate for &

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-03 05:55:14 -08:00
parent 05e425e039
commit 68d9b44d67
2 changed files with 50 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -110,9 +110,12 @@ namespace polysat {
if (is_currently_true(s, is_positive))
return;
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));
}
@ -145,6 +148,22 @@ namespace polysat {
}
}
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());
}
@ -316,6 +335,31 @@ namespace polysat {
return l_undef;
}
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?
}
}
/**
* Produce lemmas for constraint: r == p & q
* r <= p
@ -354,7 +398,7 @@ namespace polysat {
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 = p().manager().power_of_2();
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() ...)

6
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:
@ -52,6 +50,10 @@ namespace polysat {
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; }