mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 16:03:16 +00:00
Code Activity

update to use incremental substitution

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-23 03:00:25 +01:00
parent 6f689c3c1f
commit cbbf1381f7
19 changed files with 167 additions and 89 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -165,7 +165,11 @@ namespace dd {
return true;
}
pdd pdd_manager::subst_val(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
}
pdd pdd_manager::subst_val0(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {
typedef std::pair<unsigned, rational> pr;
vector<pr> s(_s);
std::function<bool (pr const&, pr const&)> compare_level =
@ -173,10 +177,16 @@ namespace dd {
std::sort(s.begin(), s.end(), compare_level);
pdd r(one());
for (auto const& q : s)
r = (r * mk_var(q.first)) + q.second;
return pdd(apply(p.root, r.root, pdd_subst_val_op), this);
r = (r * mk_var(q.first)) + q.second;
return subst_val(p, r);
}
pdd pdd_manager::subst_add(pdd const& s, unsigned v, rational const& val) {
pdd v_val = mk_var(v) + val;
return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
}
pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
bool first = true;
SASSERT(well_formed());
@ -247,6 +257,14 @@ namespace dd {
}
if (is_val(p) || is_val(q)) return p;
break;
case pdd_subst_add_op:
if (is_one(p)) return q;
SASSERT(!is_val(p));
SASSERT(!is_val(q));
if (level(p) < level(q))
// p*hi(q) + lo(q)
return make_node(level(q), lo(q), p);
break;
default:
UNREACHABLE();
break;
@ -404,6 +422,14 @@ namespace dd {
npop = 3;
}
break;
case pdd_subst_add_op:
SASSERT(!is_val(p));
SASSERT(!is_val(q));
SASSERT(level_p > level_q);
push(apply_rec(hi(p), q, pdd_subst_add_op)); // hi := add_subst(hi(p), q)
r = make_node(level_p, lo(p), read(1)); // r := hi*var(p) + lo(p)
npop = 1;
break;
default:
r = null_pdd;
UNREACHABLE();
@ -415,6 +441,7 @@ namespace dd {
return r;
}
pdd pdd_manager::minus(pdd const& a) {
if (m_semantics == mod2_e) {
return a;

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

@ -68,8 +68,9 @@ namespace dd {
pdd_mul_op = 5,
pdd_reduce_op = 6,
pdd_subst_val_op = 7,
pdd_div_const_op = 8,
pdd_no_op = 9
pdd_subst_add_op = 8,
pdd_div_const_op = 9,
pdd_no_op = 10
};
struct node {
@ -338,8 +339,10 @@ namespace dd {
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);
pdd subst_val0(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
pdd subst_val(pdd const& a, unsigned v, rational const& val);
pdd subst_val(pdd const& a, pdd const& s);
pdd subst_add(pdd const& s, unsigned v, rational const& val);
bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
pdd reduce(unsigned v, pdd const& a, pdd const& b);
void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
@ -436,8 +439,10 @@ namespace dd {
bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); }
pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); }
pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
bool operator==(pdd const& other) const { return root == other.root; }