Skip to content

Commit

Permalink
more scaffolding
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Mar 21, 2021
1 parent a1f484f commit 2fef6dc
Show file tree
Hide file tree
Showing 16 changed files with 475 additions and 151 deletions.
22 changes: 0 additions & 22 deletions src/ast/bv_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -841,28 +841,6 @@ bool bv_recognizers::is_bit2bool(expr* e, expr*& bv, unsigned& idx) const {
return true;
}

bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational & result) {
if (n.is_one()) {
result = n;
return true;
}

if (!mod(n, rational(2)).is_one()) {
return false;
}

rational g;
rational x;
rational y;
g = gcd(n, rational::power_of_two(bv_size), x, y);
if (x.is_neg()) {
x = mod(x, rational::power_of_two(bv_size));
}
SASSERT(x.is_pos());
SASSERT(mod(x * n, rational::power_of_two(bv_size)).is_one());
result = x;
return true;
}

bv_util::bv_util(ast_manager & m):
bv_recognizers(m.mk_family_id(symbol("bv"))),
Expand Down
1 change: 0 additions & 1 deletion src/ast/bv_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -379,7 +379,6 @@ class bv_recognizers {
rational norm(rational const & val, unsigned bv_size, bool is_signed) const ;
rational norm(rational const & val, unsigned bv_size) const { return norm(val, bv_size, false); }
bool has_sign_bit(rational const & n, unsigned bv_size) const;
bool mult_inverse(rational const & n, unsigned bv_size, rational & result);
};

class bv_util : public bv_recognizers {
Expand Down
4 changes: 2 additions & 2 deletions src/ast/rewriter/bv_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2520,7 +2520,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
unsigned sz;
if (m_util.is_bv_mul(lhs, c, x) &&
m_util.is_numeral(c, c_val, sz) &&
m_util.mult_inverse(c_val, sz, c_inv_val)) {
c_val.mult_inverse(sz, c_inv_val)) {

SASSERT(m_util.norm(c_val * c_inv_val, sz).is_one());

Expand Down Expand Up @@ -2562,7 +2562,7 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
for (; !found && i < num_args; ++i) {
expr* arg = to_app(rhs)->get_arg(i);
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
m_util.mult_inverse(c2_val, sz, c2_inv_val)) {
c2_val.mult_inverse(sz, c2_inv_val)) {
found = true;
}
}
Expand Down
89 changes: 72 additions & 17 deletions src/math/dd/dd_pdd.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,14 +23,16 @@ Revision History:

namespace dd {

pdd_manager::pdd_manager(unsigned num_vars, semantics s) {
pdd_manager::pdd_manager(unsigned num_vars, semantics s, unsigned power_of_2) {
m_spare_entry = nullptr;
m_max_num_nodes = 1 << 24; // up to 16M nodes
m_mark_level = 0;
m_dmark_level = 0;
m_disable_gc = false;
m_is_new_node = false;
m_semantics = s;
m_mod2N = rational::power_of_two(power_of_2);
m_power_of_2 = power_of_2;
unsigned_vector l2v;
for (unsigned i = 0; i < num_vars; ++i) l2v.push_back(i);
init_nodes(l2v);
Expand Down Expand Up @@ -109,16 +111,65 @@ namespace dd {
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, unsigned v, rational const& val) {
pdd r = mk_var(v) + val;
return pdd(apply(p.root, r.root, pdd_subst_val_op), this);
}


/**
* A polynomial is non-zero if the constant coefficient
* is a power of two such that none of the coefficients to
* non-constant monomials divide it.
* Example: 2^4*x + 2 is non-zero for every x.
*/

bool pdd_manager::is_non_zero(PDD p) {
if (is_val(p))
return !is_zero(p);
if (m_semantics != mod2N_e)
return false;
PDD q = p;
while (!is_val(q))
q = lo(q);
auto const& v = val(q);
if (v.is_zero())
return false;
unsigned p2 = v.trailing_zeros();
init_mark();
SASSERT(m_todo.empty());
m_todo.push_back(hi(p));
while (!is_val(lo(p))) {
p = lo(p);
m_todo.push_back(hi(p));
}
while (!m_todo.empty()) {
PDD r = m_todo.back();
m_todo.pop_back();
if (is_marked(r))
continue;
set_mark(r);
if (!is_val(r)) {
m_todo.push_back(lo(r));
m_todo.push_back(hi(r));
}
else if (val(r).trailing_zeros() <= p2) {
m_todo.reset();
return false;
}
}
return true;
}

pdd pdd_manager::subst_val(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 =
[&](pr const& a, pr const& b) { return m_var2level[a.first] < m_var2level[b.first]; };
std::sort(s.begin(), s.end(), compare_level);
pdd r(one());
for (auto const& q : s) {
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);
}

Expand Down Expand Up @@ -256,7 +307,7 @@ namespace dd {
r = make_node(level_p, read(2), read(1));
}
else if (level_p == level_q) {
if (m_semantics != free_e) {
if (m_semantics != free_e && m_semantics != mod2N_e) {
//
// (xa+b)*(xc+d) == x(ac+bc+ad) + bd
// == x((a+b)(c+d)-bd) + bd
Expand Down Expand Up @@ -334,9 +385,9 @@ namespace dd {
case pdd_subst_val_op:
SASSERT(!is_val(p));
SASSERT(!is_val(q));
SASSERT(level_p = level_q);
push(apply_rec(lo(p), hi(q), pdd_subst_val_op)); // lo := subst(lo(p), s)
push(apply_rec(hi(p), hi(q), pdd_subst_val_op)); // hi := subst(hi(p), s)
SASSERT(level_p == level_q);
push(apply_rec(lo(p), q, pdd_subst_val_op)); // lo := subst(lo(p), s)
push(apply_rec(hi(p), q, pdd_subst_val_op)); // hi := subst(hi(p), s)
push(apply_rec(lo(q), read(1), pdd_mul_op)); // hi := hi*s[var(p)]
r = apply_rec(read(1), read(3), pdd_add_op); // r := hi + lo := subst(lo(p),s) + s[var(p)]*subst(hi(p),s)
npop = 3;
Expand Down Expand Up @@ -721,9 +772,14 @@ namespace dd {
}

pdd_manager::PDD pdd_manager::imk_val(rational const& r) {
if (r.is_zero()) return zero_pdd;
if (r.is_one()) return one_pdd;
if (m_semantics == mod2_e) return imk_val(mod(r, rational(2)));
if (r.is_zero())
return zero_pdd;
if (r.is_one())
return one_pdd;
if (m_semantics == mod2_e)
return imk_val(mod(r, rational(2)));
if (m_semantics == mod2N_e && (r < 0 || r >= m_mod2N))
return imk_val(mod(r, m_mod2N));
const_info info;
if (!m_mpq_table.find(r, info)) {
init_value(info, r);
Expand Down Expand Up @@ -1073,13 +1129,12 @@ namespace dd {
auto mons = to_monomials(b);
bool first = true;
for (auto& m : mons) {
if (!first) {
if (m.first.is_neg()) out << " - ";
else out << " + ";
}
else {
if (m.first.is_neg()) out << "- ";
}
if (!first)
out << " ";
if (m.first.is_neg())
out << "- ";
else if (!first)
out << "+ ";
first = false;
rational c = abs(m.first);
m.second.reverse();
Expand Down
16 changes: 13 additions & 3 deletions src/math/dd/dd_pdd.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ namespace dd {

class pdd_manager {
public:
enum semantics { free_e, mod2_e, zero_one_vars_e };
enum semantics { free_e, mod2_e, zero_one_vars_e, mod2N_e };
private:
friend test;
friend pdd;
Expand Down Expand Up @@ -140,7 +140,7 @@ namespace dd {

typedef ptr_hashtable<op_entry, hash_entry, eq_entry> op_table;

svector<node> m_nodes;
svector<node> m_nodes;
vector<rational> m_values;
op_table m_op_cache;
node_table m_node_table;
Expand All @@ -163,6 +163,8 @@ namespace dd {
unsigned_vector m_free_vars;
unsigned_vector m_free_values;
rational m_freeze_value;
rational m_mod2N;
unsigned m_power_of_2 { 0 };

void reset_op_cache();
void init_nodes(unsigned_vector const& l2v);
Expand Down Expand Up @@ -204,6 +206,7 @@ namespace dd {
inline bool is_one(PDD p) const { return p == one_pdd; }
inline bool is_val(PDD p) const { return m_nodes[p].is_val(); }
inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); }
bool is_non_zero(PDD p);
inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
Expand Down Expand Up @@ -252,7 +255,7 @@ namespace dd {

struct mem_out {};

pdd_manager(unsigned nodes, semantics s = free_e);
pdd_manager(unsigned nodes, semantics s = free_e, unsigned power_of_2 = 0);
~pdd_manager();

semantics get_semantics() const { return m_semantics; }
Expand All @@ -278,6 +281,7 @@ namespace dd {
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_val(pdd const& a, unsigned v, rational const& val);

bool is_linear(PDD p) { return degree(p) == 1; }
bool is_linear(pdd const& p);
Expand All @@ -300,6 +304,8 @@ namespace dd {
double tree_size(pdd const& p);
unsigned num_vars() const { return m_var2pdd.size(); }

unsigned power_of_2() const { return m_power_of_2; }

unsigned_vector const& free_vars(pdd const& p);

std::ostream& display(std::ostream& out);
Expand Down Expand Up @@ -334,6 +340,7 @@ namespace dd {
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
bool is_binary() const { return m.is_binary(root); }
bool is_monomial() const { return m.is_monomial(root); }
bool is_non_zero() const { return m.is_non_zero(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }

pdd operator-() const { return m.minus(*this); }
Expand All @@ -353,11 +360,14 @@ namespace dd {
bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }

pdd subst_val(vector<std::pair<unsigned, rational>> 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); }

std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
bool operator==(pdd const& other) const { return root == other.root; }
bool operator!=(pdd const& other) const { return root != other.root; }

unsigned power_of_2() const { return m.power_of_2(); }

unsigned dag_size() const { return m.dag_size(*this); }
double tree_size() const { return m.tree_size(*this); }
unsigned degree() const { return m.degree(*this); }
Expand Down
Loading

0 comments on commit 2fef6dc

Please sign in to comment.