mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

anf translation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-05 21:09:52 -08:00
parent c473cd78d8
commit 2acab46388
3 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -96,6 +96,7 @@ namespace dd {
pdd pdd_manager::mul(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_mul_op), this); }
pdd pdd_manager::reduce(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_reduce_op), this); }
pdd pdd_manager::mk_val(rational const& r) { return pdd(imk_val(r), this); }
pdd pdd_manager::mk_val(unsigned r) { return mk_val(rational(r)); }
pdd pdd_manager::mul(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_mul_op), this); }
pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); }
pdd pdd_manager::zero() { return pdd(zero_pdd, this); }
@ -103,6 +104,7 @@ namespace dd {
pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); }
pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { pdd q(mk_val(x)); if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; }
pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; }
pdd pdd_manager::subst_val(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {

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

@ -253,6 +253,7 @@ namespace dd {
pdd mk_var(unsigned i);
pdd mk_val(rational const& r);
pdd mk_val(unsigned r);
pdd zero();
pdd one();
pdd minus(pdd const& a);
@ -263,6 +264,7 @@ namespace dd {
pdd mul(rational const& c, pdd const& b);
pdd mk_or(pdd const& p, pdd const& q);
pdd mk_xor(pdd const& p, pdd const& q);
pdd mk_xor(pdd const& p, unsigned q);
pdd mk_not(pdd const& p);
pdd reduce(pdd const& a, pdd const& b);
pdd subst_val(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
@ -325,6 +327,7 @@ namespace dd {
pdd operator&(pdd const& other) const { return m.mul(*this, other); }
pdd operator|(pdd const& other) const { return m.mk_or(*this, other); }
pdd operator^(pdd const& other) const { return m.mk_xor(*this, other); }
pdd operator^(unsigned other) const { return m.mk_xor(*this, other); }
pdd operator*(rational const& other) const { return m.mul(other, *this); }
pdd operator+(rational const& other) const { return m.add(other, *this); }
@ -360,6 +363,9 @@ namespace dd {
inline pdd operator+(int x, pdd const& b) { return b + rational(x); }
inline pdd operator+(pdd const& b, int x) { return b + rational(x); }
inline pdd operator^(unsigned x, pdd const& b) { return b + x; }
inline pdd operator^(bool x, pdd const& b) { return b + x; }
inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }

9
src/sat/sat_anf_simplifier.cpp
View file

@ -372,9 +372,7 @@ namespace sat {
void anf_simplifier::add_bin(solver::bin_clause const& b, pdd_solver& ps) {
auto& m = ps.get_manager();
auto v = lit2pdd(b.first);
auto w = lit2pdd(b.second);
dd::pdd p = (v | w) + 1;
dd::pdd p = (lit2pdd(b.first) | lit2pdd(b.second)) ^ true;
ps.add(p);
TRACE("anf_simplifier", tout << "bin: " << b.first << " " << b.second << " : " << p << "\n";);
}
@ -384,7 +382,7 @@ namespace sat {
auto& m = ps.get_manager();
dd::pdd p = m.zero();
for (literal l : c) p |= lit2pdd(l);
p = p + 1;
p = p ^ true;
ps.add(p);
TRACE("anf_simplifier", tout << "clause: " << c << " : " << p << "\n";);
}
@ -408,7 +406,8 @@ namespace sat {
void anf_simplifier::add_if(literal head, literal c, literal th, literal el, pdd_solver& ps) {
auto& m = ps.get_manager();
dd::pdd p = lit2pdd(head) ^ (lit2pdd(c) & lit2pdd(th)) ^ (~lit2pdd(c) & lit2pdd(el));
dd::pdd cond = lit2pdd(c);
dd::pdd p = lit2pdd(head) ^ (cond & lit2pdd(th)) ^ (~cond & lit2pdd(el));
ps.add(p);
TRACE("anf_simplifier", tout << "ite: " << head << " == " << c << "?" << th << ":" << el << " poly : " << p << "\n";);
}