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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-26 14:31:05 -08:00
parent 2c6e6b1fdb
commit 914856b9ba
5 changed files with 216 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -23,13 +23,13 @@ Revision History:
namespace dd {
pdd_manager::pdd_manager(unsigned num_vars) {
pdd_manager::pdd_manager(unsigned num_vars, semantics s) {
m_spare_entry = nullptr;
m_max_num_nodes = 1 << 24; // up to 16M nodes
m_mark_level = 0;
m_disable_gc = false;
m_is_new_node = false;
m_mod2_semantics = false;
m_semantics = s;
// add dummy nodes for operations, and 0, 1 pdds.
for (unsigned i = 0; i < pdd_no_op; ++i) {
@ -61,7 +61,7 @@ namespace dd {
}
pdd pdd_manager::add(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_add_op), this); }
pdd pdd_manager::sub(pdd const& a, pdd const& b) { pdd m(minus(b)); return pdd(apply(a.root, m.root, pdd_add_op), this); }
pdd pdd_manager::sub(pdd const& a, pdd const& b) { return pdd(apply(a.root, b.root, pdd_sub_op), this); }
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); }
@ -71,6 +71,8 @@ namespace dd {
pdd pdd_manager::one() { return pdd(one_pdd, this); }
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) { return (p*q*2) - p - q; }
pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; }
pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
bool first = true;
@ -108,6 +110,11 @@ namespace dd {
pdd_manager::PDD pdd_manager::apply_rec(PDD p, PDD q, pdd_op op) {
switch (op) {
case pdd_sub_op:
if (is_zero(q)) return p;
if (is_val(p) && is_val(q)) return imk_val(val(p) - val(q));
if (m_semantics != mod2_e) break;
op = pdd_add_op;
case pdd_add_op:
if (is_zero(p)) return q;
if (is_zero(q)) return p;
@ -163,6 +170,35 @@ namespace dd {
npop = 1;
}
break;
case pdd_sub_op:
if (is_val(p)) {
push(apply_rec(p, lo(q), op));
r = make_node(level_q, read(1), hi(q));
npop = 1;
}
else if (is_val(q)) {
push(apply_rec(lo(p), q, op));
r = make_node(level_p, read(1), hi(p));
npop = 1;
}
else if (level_p == level_q) {
push(apply_rec(lo(p), lo(q), op));
push(apply_rec(hi(p), hi(q), op));
r = make_node(level_p, read(2), read(1));
}
else if (level_p > level_q) {
// x*hi(p) + (lo(p) - q)
push(apply_rec(lo(p), q, op));
r = make_node(level_p, read(1), hi(p));
npop = 1;
}
else {
// x*hi(q) + (p - lo(q))
push(apply_rec(p, lo(q), op));
r = make_node(level_q, read(1), hi(q));
npop = 1;
}
break;
case pdd_mul_op:
SASSERT(!is_val(p));
if (is_val(q)) {
@ -171,17 +207,18 @@ namespace dd {
r = make_node(level_p, read(2), read(1));
}
else if (level_p == level_q) {
if (m_mod2_semantics) {
if (m_semantics != free_e) {
//
// (xa+b)*(xc+d) mod2 == x(ac+bc+ad) + bd
// == x((a+b)(c+d)+bd) + bd
// (xa+b)*(xc+d) == x(ac+bc+ad) + bd
// == x((a+b)(c+d)-bd) + bd
// because x*x = x
//
push(apply_rec(lo(p), lo(q), pdd_mul_op));
unsigned bd = read(1);
push(apply_rec(hi(p), lo(p), pdd_add_op));
push(apply_rec(hi(q), lo(q), pdd_add_op));
push(apply_rec(read(1), read(2), pdd_mul_op));
push(apply_rec(read(1), bd, pdd_add_op));
push(apply_rec(read(1), bd, pdd_sub_op));
r = make_node(level_p, bd, read(1));
npop = 5;
}
@ -243,7 +280,7 @@ namespace dd {
}
pdd pdd_manager::minus(pdd const& a) {
if (m_mod2_semantics) {
if (m_semantics == mod2_e) {
return a;
}
bool first = true;
@ -264,7 +301,7 @@ namespace dd {
}
pdd_manager::PDD pdd_manager::minus_rec(PDD a) {
SASSERT(!m_mod2_semantics);
SASSERT(m_semantics != mod2_e);
if (is_zero(a)) return zero_pdd;
if (is_val(a)) return imk_val(-val(a));
op_entry* e1 = pop_entry(a, a, pdd_minus_op);
@ -358,7 +395,7 @@ namespace dd {
while (!is_val(x)) p.push_back(var(x)), x = hi(x);
pc = val(x);
qc = val(y);
if (!m_mod2_semantics && pc.is_int() && qc.is_int()) {
if (m_semantics != mod2_e && pc.is_int() && qc.is_int()) {
rational g = gcd(pc, qc);
pc /= g;
qc /= g;
@ -461,6 +498,17 @@ namespace dd {
return is_binary(p.root);
}
/**
Determine if p is a monomial.
*/
bool pdd_manager::is_monomial(PDD p) {
while (true) {
if (is_val(p)) return true;
if (!is_zero(lo(p))) return false;
p = hi(p);
}
}
/*
\brief determine if v occurs as a leaf variable.
*/
@ -522,7 +570,7 @@ 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_mod2_semantics) return imk_val(mod(r, rational(2)));
if (m_semantics == mod2_e) return imk_val(mod(r, rational(2)));
const_info info;
if (!m_mpq_table.find(r, info)) {
init_value(info, r);

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

@ -41,6 +41,9 @@ namespace dd {
class pdd;
class pdd_manager {
public:
enum semantics { free_e, mod2_e, zero_one_vars_e };
private:
friend pdd;
typedef unsigned PDD;
@ -52,10 +55,11 @@ namespace dd {
enum pdd_op {
pdd_add_op = 2,
pdd_minus_op = 3,
pdd_mul_op = 4,
pdd_reduce_op = 5,
pdd_no_op = 6
pdd_sub_op = 3,
pdd_minus_op = 4,
pdd_mul_op = 5,
pdd_reduce_op = 6,
pdd_no_op = 7
};
struct node {
@ -151,7 +155,7 @@ namespace dd {
bool m_disable_gc;
bool m_is_new_node;
unsigned m_max_num_nodes;
bool m_mod2_semantics;
semantics m_semantics;
unsigned_vector m_free_vars;
unsigned_vector m_free_values;
rational m_freeze_value;
@ -230,10 +234,9 @@ namespace dd {
struct mem_out {};
pdd_manager(unsigned nodes);
pdd_manager(unsigned nodes, semantics s = free_e);
~pdd_manager();
void set_mod2_semantics() { m_mod2_semantics = true; }
void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
void set_level2var(unsigned_vector const& level2var);
unsigned_vector const& get_level2var() const { return m_level2var; }
@ -249,6 +252,8 @@ namespace dd {
pdd mul(pdd const& a, pdd const& b);
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_not(pdd const& p);
pdd reduce(pdd const& a, pdd const& b);
bool is_linear(PDD p);
@ -257,6 +262,8 @@ namespace dd {
bool is_binary(PDD p);
bool is_binary(pdd const& p);
bool is_monomial(PDD p);
// create an spoly r if leading monomials of a and b overlap
bool try_spoly(pdd const& a, pdd const& b, pdd& r);
@ -293,22 +300,28 @@ namespace dd {
bool is_zero() const { return m.is_zero(root); }
bool is_linear() const { return m.is_linear(root); }
bool is_binary() const { return m.is_binary(root); }
bool is_monomial() const { return m.is_monomial(root); }
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
pdd minus() const { return m.minus(*this); }
pdd operator-() const { return m.minus(*this); }
pdd operator+(pdd const& other) const { return m.add(*this, other); }
pdd operator-(pdd const& other) const { return m.sub(*this, other); }
pdd operator*(pdd const& other) const { return m.mul(*this, other); }
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*(rational const& other) const { return m.mul(other, *this); }
pdd operator+(rational const& other) const { return m.add(other, *this); }
pdd operator|(pdd const& other) const { return m.mk_or(*this, other); }
pdd operator~() const { return m.mk_not(*this); }
pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); }
pdd reduce(pdd const& other) const { return m.reduce(*this, other); }
bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
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; }
bool operator<(pdd const& b) const { return m.lt(*this, b); }
bool operator<(pdd const& other) const { return m.lt(*this, other); }
unsigned dag_size() const { return m.dag_size(*this); }
double tree_size() const { return m.tree_size(*this); }
@ -323,16 +336,17 @@ 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-(rational const& r, pdd const& b) { return r + b.minus(); }
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)); }
inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }
inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; }
inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; }
std::ostream& operator<<(std::ostream& out, pdd const& b);
}

66
src/math/grobner/pdd_grobner.cpp
View file

@ -186,13 +186,14 @@ namespace dd {
void grobner::simplify() {
try {
while (simplify_linear_step(true) ||
simplify_elim_pure_step() ||
simplify_linear_step(false) ||
simplify_cc_step() ||
simplify_leaf_step() ||
/*simplify_elim_dual_step() ||*/
false) {
while (!done() &&
(simplify_linear_step(true) ||
simplify_elim_pure_step() ||
simplify_cc_step() ||
simplify_linear_step(false) ||
simplify_leaf_step() ||
/*simplify_elim_dual_step() ||*/
false)) {
DEBUG_CODE(invariant(););
TRACE("grobner", display(tout););
}
@ -209,6 +210,7 @@ namespace dd {
};
bool grobner::simplify_linear_step(bool binary) {
TRACE("grobner", tout << "binary " << binary << "\n";);
equation_vector linear;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
@ -243,12 +245,14 @@ namespace dd {
continue;
}
simplify_using(*dst, *src, changed_leading_term);
if (check_conflict(*dst)) {
return false;
}
if (is_trivial(*dst)) {
trivial.push_back(dst);
}
else if (is_conflict(dst)) {
pop_equation(dst);
set_conflict(dst);
return true;
}
else if (changed_leading_term) {
pop_equation(dst);
push_equation(to_simplify, dst);
@ -257,7 +261,7 @@ namespace dd {
if (all_reduced) {
linear[j++] = src;
}
}
}
linear.shrink(j);
for (equation* src : linear) {
pop_equation(src);
@ -277,6 +281,7 @@ namespace dd {
since px = ry
*/
bool grobner::simplify_cc_step() {
TRACE("grobner", tout << "cc\n";);
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
@ -309,6 +314,7 @@ namespace dd {
\brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
*/
bool grobner::simplify_leaf_step() {
TRACE("grobner", tout << "leaf\n";);
use_list_t use_list = get_use_list();
bool reduced = false;
equation_vector leaves;
@ -329,8 +335,14 @@ namespace dd {
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
add_to_use(e2, use_list);
if (check_conflict(*e2)) {
return false;
if (is_trivial(*e2)) {
pop_equation(e2);
retire(e2);
}
else if (e2->poly().is_val()) {
pop_equation(e2);
set_conflict(*e2);
return true;
}
else if (changed_leading_term) {
pop_equation(e2);
@ -346,6 +358,7 @@ namespace dd {
\brief treat equations as processed if top variable occurs only once.
*/
bool grobner::simplify_elim_pure_step() {
TRACE("grobner", tout << "pure\n";);
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : m_to_simplify) {
@ -387,8 +400,9 @@ namespace dd {
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
if (check_conflict(*e2)) {
break;
if (is_conflict(e2)) {
pop_equation(e2);
set_conflict(e2);
}
// when e2 is trivial, leading term is changed
SASSERT(!is_trivial(*e2) || changed_leading_term);
@ -470,7 +484,7 @@ namespace dd {
do {
simplified = false;
for (equation* p : eqs) {
if (simplify_source_target(*p, eq, changed_leading_term)) {
if (try_simplify_using(eq, *p, changed_leading_term)) {
simplified = true;
}
if (canceled() || eq.poly().is_val()) {
@ -493,7 +507,7 @@ namespace dd {
for (unsigned i = 0; i < sz; ++i) {
equation& target = *set[i];
bool changed_leading_term = false;
bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
bool simplified = !done() && try_simplify_using(target, eq, changed_leading_term);
if (simplified && is_trivial(target)) {
retire(&target);
}
@ -521,7 +535,7 @@ namespace dd {
return true if the target was simplified.
set changed_leading_term if the target is in the m_processed set and the leading term changed.
*/
bool grobner::simplify_source_target(equation const& src, equation& dst, bool& changed_leading_term) {
bool grobner::try_simplify_using(equation& dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) {
return false;
}
@ -585,7 +599,7 @@ namespace dd {
if (!simplify_using(m_processed, eq)) return false;
TRACE("grobner", display(tout << "eq = ", eq););
superpose(eq);
return simplify_to_simplify(eq);
return simplify_watch(eq);
}
void grobner::tuned_init() {
@ -596,6 +610,7 @@ namespace dd {
m_level2var[i] = l2v[i];
m_var2level[l2v[i]] = i;
}
m_watch.reset();
m_watch.reserve(m_level2var.size());
m_levelp1 = m_level2var.size();
for (equation* eq : m_to_simplify) add_to_watch(*eq);
@ -611,7 +626,7 @@ namespace dd {
}
}
bool grobner::simplify_to_simplify(equation const& eq) {
bool grobner::simplify_watch(equation const& eq) {
unsigned v = eq.poly().var();
auto& watch = m_watch[v];
unsigned j = 0;
@ -620,13 +635,16 @@ namespace dd {
SASSERT(target.state() == to_simplify);
SASSERT(target.poly().var() == v);
bool changed_leading_term = false;
if (!done()) simplify_source_target(eq, target, changed_leading_term);
if (!done()) {
try_simplify_using(target, eq, changed_leading_term);
}
if (is_trivial(target)) {
retire(&target);
}
else if (check_conflict(target)) {
// pushed to solved
}
else if (is_conflict(target)) {
pop_equation(target);
set_conflict(target);
}
else if (target.poly().var() != v) {
// move to other watch list
m_watch[target.poly().var()].push_back(_target);

10
src/math/grobner/pdd_grobner.h
View file

@ -125,16 +125,18 @@ private:
bool done();
void superpose(equation const& eq1, equation const& eq2);
void superpose(equation const& eq);
bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term);
bool simplify_using(equation& eq, equation_vector const& eqs);
bool simplify_using(equation_vector& set, equation const& eq);
void simplify_using(equation & dst, equation const& src, bool& changed_leading_term);
bool try_simplify_using(equation& target, equation const& source, bool& changed_leading_term);
bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); }
bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }
bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
bool check_conflict(equation& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); }
bool is_conflict(equation const* eq) const { return is_conflict(*eq); }
bool is_conflict(equation const& eq) const { return eq.poly().is_val() && !is_trivial(eq); }
bool check_conflict(equation& eq) { return is_conflict(eq) && (set_conflict(eq), true); }
void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); }
void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); }
bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; }
@ -147,7 +149,7 @@ private:
bool tuned_step();
void tuned_init();
equation* tuned_pick_next();
bool simplify_to_simplify(equation const& eq);
bool simplify_watch(equation const& eq);
void add_to_watch(equation& eq);
void del_equation(equation& eq) { del_equation(&eq); }

95
src/test/pdd_grobner.cpp
View file

@ -2,6 +2,7 @@
#include "math/grobner/pdd_grobner.h"
#include "ast/bv_decl_plugin.h"
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/reg_decl_plugins.h"
@ -74,6 +75,71 @@ namespace dd {
//
}
expr_ref elim_or(ast_manager& m, expr* e) {
obj_map<expr, expr*> cache;
expr_ref_vector trail(m), todo(m), args(m);
todo.push_back(e);
while (!todo.empty()) {
expr* f = todo.back(), *g;
if (!is_app(f)) {
cache.insert(f, f);
}
if (cache.contains(f)) {
todo.pop_back();
continue;
}
app* a = to_app(f);
args.reset();
for (expr* arg : *a) {
if (cache.find(arg, g)) {
args.push_back(g);
}
else {
todo.push_back(arg);
}
}
if (args.size() != a->get_num_args()) {
continue;
}
todo.pop_back();
if (m.is_or(a)) {
for (unsigned i = 0; i < args.size(); ++i) {
args[i] = mk_not(m, args.get(i));
}
g = m.mk_not(m.mk_and(args.size(), args.c_ptr()));
}
else if (m.is_and(a)) {
g = m.mk_and(args.size(), args.c_ptr());
trail.push_back(g);
}
else if (m.is_eq(a)) {
expr* x = args.get(0);
expr* y = args.get(1);
if (m.is_not(x, x)) {
g = m.mk_xor(x, y);
}
else if (m.is_not(y, y)) {
g = m.mk_xor(x, y);
}
else {
g = m.mk_not(m.mk_xor(x, y));
}
}
else if (m.is_not(a)) {
g = mk_not(m, args.get(0));
}
else {
g = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
}
trail.push_back(g);
cache.insert(a, g);
}
return expr_ref(cache[e], m);
}
void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) {
expr* a, *b;
pdd v1 = p.mk_var(id2var[e->get_id()]);
@ -90,17 +156,17 @@ namespace dd {
}
else if (m.is_not(e, a)) {
pdd v2 = p.mk_var(id2var[a->get_id()]);
q = v1 + v2 - 1;
q = v1 - ~v2;
}
else if (m.is_eq(e, a, b)) {
pdd v2 = p.mk_var(id2var[a->get_id()]);
pdd v3 = p.mk_var(id2var[b->get_id()]);
// v1 = (v2 = v3)
// 111, 100 = 0
// 001, 010 = 0
// 000, 011 = 1
// 110, 101 = 1
q = v1 - v2 - v3 + 1 + 2*v2*v3 - 2*v1*v2*v3;
q = v1 - ~(v2 ^ v3);
}
else if (m.is_xor(e, a, b)) {
pdd v2 = p.mk_var(id2var[a->get_id()]);
pdd v3 = p.mk_var(id2var[b->get_id()]);
q = v1 - (v2 ^ v3);
}
else if (is_uninterp_const(e)) {
return;
@ -131,13 +197,18 @@ namespace dd {
unsigned_vector id2var;
collect_id2var(id2var, fmls);
pdd_manager p(id2var.size());
if (use_mod2) p.set_mod2_semantics();
pdd_manager p(id2var.size(), use_mod2 ? pdd_manager::mod2_e : pdd_manager::zero_one_vars_e);
grobner g(m.limit(), p);
for (expr* e : subterms(fmls)) {
add_def(id2var, to_app(e), m, p, g);
}
if (!use_mod2) { // should be built-in
for (expr* e : subterms(fmls)) {
pdd v = p.mk_var(id2var[e->get_id()]);
g.add(v*v - v);
}
}
for (expr* e : fmls) {
g.add(1 - p.mk_var(id2var[e->get_id()]));
}
@ -152,8 +223,8 @@ namespace dd {
ast_manager m;
reg_decl_plugins(m);
bv_util bv(m);
expr_ref x(m.mk_const("x", bv.mk_sort(4)), m);
expr_ref y(m.mk_const("y", bv.mk_sort(4)), m);
expr_ref x(m.mk_const("x", bv.mk_sort(3)), m);
expr_ref y(m.mk_const("y", bv.mk_sort(3)), m);
expr_ref xy(bv.mk_bv_mul(x, y), m);
expr_ref yx(bv.mk_bv_mul(y, x), m);
expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m);
@ -166,7 +237,7 @@ namespace dd {
expr_ref_vector fmls(m);
for (unsigned i = 0; i < g->size(); ++i) {
fmls.push_back(g->form(i));
fmls.push_back(elim_or(m, g->form(i)));
}
test_simplify(fmls, true);
test_simplify(fmls, false);