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

merge unary minus

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-17 17:10:35 -08:00
parent 9e4a7ae4b8
commit f7eb5f8840
2 changed files with 6 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,6 +63,7 @@ namespace dd {
pdd pdd_manager::mk_val(rational const& r) { return pdd(imk_val(r), this); }
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::minus(pdd const& b) { return pdd(apply(zero_pdd, b.root, pdd_sub_op), this); }
pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
bool first = true;
@ -422,44 +423,8 @@ namespace dd {
pdd pdd_manager::mk_var(unsigned i) {
reserve_var(i);
std::cout << m_var2pdd[i] << "\n";
return pdd(m_var2pdd[i], this);
}
pdd pdd_manager::minus(pdd const &b) {
bool first = true;
while (true) {
try {
return pdd(minus_rec(b.root), this);
}
catch (const mem_out &) {
if (!first) throw;
try_gc();
first = false;
}
}
}
pdd_manager::PDD pdd_manager::minus_rec(PDD b) {
if (is_zero(b)) {
return zero_pdd;
}
if (is_val(b)) {
return imk_val(-val(b));
}
op_entry* e1 = pop_entry(b, b, pdd_minus_op);
op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
if (check_result(e1, e2, b, b, pdd_minus_op))
return e2->m_result;
push(minus_rec(lo(b)));
push(minus_rec(hi(b)));
PDD r = make_node(level(b), read(2), read(1));
pop(2);
e1->m_result = r;
return r;
}
unsigned pdd_manager::pdd_size(pdd const& b) {
init_mark();

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

@ -45,9 +45,8 @@ namespace dd {
pdd_add_op = 2,
pdd_sub_op = 3,
pdd_mul_op = 4,
pdd_minus_op = 5,
pdd_reduce_op = 6,
pdd_no_op = 7
pdd_reduce_op = 5,
pdd_no_op = 6
};
struct pdd_node {
@ -147,14 +146,13 @@ namespace dd {
bool is_new_node() const { return m_is_new_node; }
PDD apply(PDD arg1, PDD arg2, pdd_op op);
PDD apply_rec(PDD arg1, PDD arg2, pdd_op op);
PDD reduce_on_match(PDD a, PDD b);
bool lm_divides(PDD p, PDD q) const;
PDD lt_quotient(PDD p, PDD q);
PDD apply_rec(PDD arg1, PDD arg2, pdd_op op);
PDD imk_val(rational const& r);
PDD minus_rec(PDD a);
PDD imk_val(rational const& r);
void push(PDD b);
void pop(unsigned num_scopes);