3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

prepare term-graph for cc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-09 14:50:46 -07:00 committed by Arie Gurfinkel
parent 14696f03f7
commit d26609ebdd
6 changed files with 193 additions and 96 deletions

View file

@ -421,7 +421,7 @@ public:
for (func_decl* v : m_vars) {
vars.push_back(v);
}
qe::interpolator mbi;
qe::interpolator mbi(m);
expr_ref a(m_a, m);
expr_ref b(m_b, m);
expr_ref itp(m);
@ -433,7 +433,7 @@ public:
sB->assert_expr(b);
qe::prop_mbi_plugin pA(sA.get());
qe::prop_mbi_plugin pB(sB.get());
lbool res = mbi.binary(pA, pB, vars, itp);
lbool res = mbi.pingpong(pA, pB, vars, itp);
ctx.regular_stream() << res << " " << itp << "\n";
}

View file

@ -49,8 +49,8 @@ namespace qe {
if (m.is_true(mdl->get_const_interp(c))) {
lits.push_back(m.mk_const(c));
}
else {
lits.push_back(m.mk_not(m.mk_const(c)));
else if (m.is_false(mdl->get_const_interp(c))) {
lits.push_back(m.mk_const(c));
}
}
}
@ -105,10 +105,8 @@ namespace qe {
/** --------------------------------------------------------------
* ping-pong interpolation of Gurfinkel & Vizel
* compute a binary interpolant.
* TBD: also implement the one-sided versions that create clausal interpolants.
*/
lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
ast_manager& m = vars.get_manager();
lbool interpolator::pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
model_ref mdl;
expr_ref_vector lits(m);
bool turn = true;
@ -156,4 +154,12 @@ namespace qe {
last_res = next_res;
}
}
/**
* TBD: also implement the one-sided versions that create clausal interpolants.
*/
lbool interpolator::pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
NOT_IMPLEMENTED_YET();
return l_undef;
}
};

View file

@ -81,8 +81,11 @@ namespace qe {
* use cases for interpolation.
*/
class interpolator {
ast_manager& m;
public:
static lbool binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
interpolator(ast_manager& m):m(m) {}
lbool pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
lbool pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
};
#if 0

View file

@ -27,7 +27,7 @@ namespace qe {
class term {
// -- an app represented by this term
app* m_app;
expr* m_app; // NSB: to make usable with exprs
// -- root of the equivalence class
term* m_root;
// -- next element in the equivalence class (cyclic linked list)
@ -43,27 +43,87 @@ class term {
unsigned m_interpreted:1;
// -- terms that contain this term as a child
//ptr_vector<term> m_uses;
ptr_vector<term> m_parents;
// ptr_vector<term> m_args;
// arguments of term.
ptr_vector<term> m_children;
public:
term(app* a) : m_app(a), m_root(this), m_next(this),
m_class_size(1), m_mark(false), m_mark2(false),
m_interpreted(false) {}
term(expr* a, u_map<term*>& app2term) :
m_app(a),
m_root(this),
m_next(this),
m_class_size(1),
m_mark(false),
m_mark2(false),
m_interpreted(false) {
if (!is_app(a)) return;
for (expr* e : *to_app(a)) {
term* t = app2term[e->get_id()];
t->m_parents.push_back(this);
m_children.push_back(t);
}
}
~term() {}
unsigned get_id() const {return m_app->get_id();}
class parents {
term const& t;
public:
parents(term const& _t):t(_t) {}
parents(term const* _t):t(*_t) {}
ptr_vector<term>::const_iterator begin() const { return t.m_parents.begin(); }
ptr_vector<term>::const_iterator end() const { return t.m_parents.end(); }
};
class children {
term const& t;
public:
children(term const& _t):t(_t) {}
children(term const* _t):t(*_t) {}
ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
};
// Congruence table hash function is based on
// roots of children and function declaration.
struct cg_hash {
unsigned operator()(term const* t) const {
unsigned a, b, c;
a = b = c = t->get_decl_id();
for (term * ch : children(t)) {
a = ch->get_root().get_id();
mix(a, b, c);
}
return c;
}
};
struct cg_eq {
bool operator()(term * t1, term * t2) const {
if (t1->get_decl_id() != t2->get_decl_id()) return false;
if (t1->m_children.size() != t2->m_children.size()) return false;
for (unsigned i = 0, sz = t1->m_children.size(); i < sz; ++ i) {
if (t1->m_children[i]->get_root().get_id() != t2->m_children[i]->get_root().get_id()) return false;
}
return true;
}
};
unsigned get_id() const { return m_app->get_id();}
unsigned get_decl_id() const { return is_app(m_app) ? to_app(m_app)->get_decl()->get_id() : m_app->get_id(); }
bool is_marked() const {return m_mark;}
void set_mark(bool v){m_mark = v;}
bool is_marked2() const {return m_mark2;}
void set_mark2(bool v){m_mark2 = v;}
bool is_marked2() const {return m_mark2;} // NSB: where is this used?
void set_mark2(bool v){m_mark2 = v;} // NSB: where is this used?
bool is_interpreted() const {return m_interpreted;}
void mark_as_interpreted() {m_interpreted=true;}
app* get_app() const {return m_app;}
expr* get_app() const {return m_app;}
unsigned get_num_args() const { return is_app(m_app) ? to_app(m_app)->get_num_args() : 0; }
term &get_root() const {return *m_root;}
bool is_root() const {return m_root == this;}
@ -98,6 +158,8 @@ public:
}
};
class arith_term_graph_plugin : public term_graph_plugin {
term_graph &m_g;
ast_manager &m;
@ -244,6 +306,7 @@ public:
term_graph::term_graph(ast_manager &man) : m(man), m_lits(m), m_pinned(m) {
m_plugins.register_plugin (alloc(arith_term_graph_plugin, *this));
}
term_graph::~term_graph() {
reset();
}
@ -251,7 +314,7 @@ term_graph::~term_graph() {
static family_id get_family_id(ast_manager &m, app *lit) {
family_id fid = null_family_id;
expr *e1, *e2, *e3;
expr *e1 = nullptr, *e2 = nullptr, *e3 = nullptr;
// strip negation
if (!m.is_not (lit, e1)) { e1 = lit; }
@ -285,14 +348,14 @@ bool term_graph::is_internalized(app *a) {
return m_app2term.contains(a->get_id());
}
term* term_graph::get_term(app *a) {
term* term_graph::get_term(expr *a) {
term *res;
return m_app2term.find (a->get_id(), res) ? res : nullptr;
}
term *term_graph::mk_term(app *a) {
term * t = alloc(term, a);
if (a->get_num_args() == 0 && m.is_unique_value(a)){
term *term_graph::mk_term(expr *a) {
term * t = alloc(term, a, m_app2term);
if (t->get_num_args() == 0 && m.is_unique_value(a)){
t->mark_as_interpreted();
}
@ -301,37 +364,32 @@ term *term_graph::mk_term(app *a) {
return t;
}
term *term_graph::internalize_term(app *t) {
term *term_graph::internalize_term(expr *t) {
term *res = get_term(t);
if (!res) {
for (expr * arg : *t) {
SASSERT(is_app(arg));
internalize_term(::to_app(arg));
if (is_app(t)) {
for (expr * arg : *::to_app(t)) {
internalize_term(arg);
}
}
res = mk_term(t);
}
return res;
}
void term_graph::internalize_eq(app *a1, app* a2) {
internalize_lit(a1);
internalize_lit(a2);
void term_graph::internalize_eq(expr *a1, expr* a2) {
internalize_term(a1);
internalize_term(a2);
merge(get_term(a1)->get_root(), get_term(a2)->get_root());
}
void term_graph::internalize_lit(app* lit) {
if (is_internalized(lit)) return;
expr *e1, *e2;
if (m.is_eq (lit, e1, e2)) {
SASSERT(is_app(e1));
SASSERT(is_app(e2));
internalize_eq (::to_app(e1), ::to_app(e2));
expr *e1 = nullptr, *e2 = nullptr;
if (m.is_eq (lit, e1, e2)) {
internalize_eq (e1, e2);
}
else {
// NSB: this is thrown away.
// Is caller responsible for maintaining other predicates than equalities?
internalize_term(lit);
}
}
@ -351,50 +409,61 @@ void term_graph::merge (term &t1, term &t2) {
// make 'a' be the root of the equivalence class of 'b'
b->set_root(*a);
for (term *it = &b->get_next(); it != b; it = &it->get_next()) {
// TBD: remove parents of it from the cg table.
it->set_root(*a);
}
// merge equivalence classes
a->merge_eq_class(*b);
// TBD: insert parents of b's old equilvalence class into the cg table
// and propagate equalities.
// -- merge might have invalidated term2map cache
// NSB: ??? what is ownership model of pinned in m_terms?
m_term2app.reset();
m_pinned.reset();
m_pinned.reset();
}
app* term_graph::mk_app_core (app *a) {
expr_ref_vector kids(m);
for (expr * arg : *a) {
kids.push_back (mk_app(::to_app(arg)));
expr* term_graph::mk_app_core (expr *e) {
if (is_app(e)) {
expr_ref_vector kids(m);
app* a = ::to_app(e);
for (expr * arg : *a) {
kids.push_back (mk_app(arg));
}
app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr());
m_pinned.push_back(res);
return res;
}
else {
return e;
}
app* res = m.mk_app(a->get_decl(), a->get_num_args(), kids.c_ptr());
m_pinned.push_back(res);
return res;
}
app_ref term_graph::mk_app(term const &r) {
expr_ref term_graph::mk_app(term const &r) {
SASSERT(r.is_root());
if (r.get_app()->get_num_args() == 0) {
return app_ref(r.get_app(), m);
if (r.get_num_args() == 0) {
return expr_ref(r.get_app(), m);
}
app* res;
expr* res = nullptr;
if (m_term2app.find(r.get_id(), res)) {
return app_ref(res, m);
return expr_ref(res, m);
}
res = mk_app_core (r.get_app());
m_term2app.insert(r.get_id(), res);
return app_ref(res, m);
return expr_ref(res, m);
}
app_ref term_graph::mk_app(app *a) {
expr_ref term_graph::mk_app(expr *a) {
term *t = get_term(a);
if (!t)
return app_ref(a, m);
return expr_ref(a, m);
else
return mk_app(t->get_root());
@ -402,10 +471,10 @@ app_ref term_graph::mk_app(app *a) {
void term_graph::mk_equalities(term const &t, app_ref_vector &out) {
SASSERT(t.is_root());
app_ref rep(mk_app(t), m);
expr_ref rep(mk_app(t), m);
for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
app* mem = mk_app_core(it->get_app());
expr* mem = mk_app_core(it->get_app());
out.push_back (m.mk_eq (rep, mem));
}
}
@ -414,10 +483,9 @@ void term_graph::mk_all_equalities(term const &t, app_ref_vector &out) {
mk_equalities(t, out);
for (term *it = &t.get_next(); it != &t; it = &it->get_next ()) {
app* a1 = mk_app_core (it->get_app());
expr* a1 = mk_app_core (it->get_app());
for (term *it2 = &it->get_next(); it2 != &t; it2 = &it2->get_next()) {
app *a2;
a2 = mk_app_core(it2->get_app());
expr* a2 = mk_app_core(it2->get_app());
out.push_back (m.mk_eq (a1, a2));
}
}
@ -436,19 +504,16 @@ bool term_graph::term_le(term const &t1, term const &t2) {
// prefer constants over applications
// prefer uninterpreted constants over values
// prefer smaller expressions over larger ones
app *a1, *a2;
a1 = t1.get_app();
a2 = t2.get_app();
if (a1->get_num_args() == 0 && a2->get_num_args() > 0) {
if (t1.get_num_args() == 0 && t2.get_num_args() > 0) {
return true;
}
// NSB: how does this possibly define an order?
if (a1->get_num_args() == a2->get_num_args()) {
return m.is_value(a2);
if (t1.get_num_args() == t2.get_num_args()) {
// NSB: how does this possibly define an order?
return m.is_value(t2.get_app());
}
unsigned sz1 = get_num_exprs(a1);
unsigned sz2 = get_num_exprs(a2);
unsigned sz1 = get_num_exprs(t1.get_app());
unsigned sz2 = get_num_exprs(t1.get_app());
return sz1 < sz2;
}
@ -481,12 +546,13 @@ void term_graph::display(std::ostream &out) {
<< "\n";
}
}
void term_graph::to_lits (app_ref_vector &lits, bool all_equalities) {
pick_roots();
for (app * a : m_lits) {
if (is_internalized(a)) {
lits.push_back (mk_app(a));
lits.push_back (::to_app(mk_app(a)));
}
}
@ -499,6 +565,7 @@ void term_graph::to_lits (app_ref_vector &lits, bool all_equalities) {
mk_equalities(*t, lits);
}
}
void term_graph::to_lits (expr_ref_vector &lits, bool all_equalities) {
app_ref_vector out(m);
to_lits (out, all_equalities);
@ -522,4 +589,18 @@ void term_graph::reset() {
m_lits.reset();
}
expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) {
obj_hashtable<func_decl> _decls;
for (func_decl* f : decls) _decls.insert(f);
// . propagate representatives up over parents.
// use work-list + marking to propagate.
// . produce equalities over represented classes.
// . produce other literals over represented classes
// (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls)
expr_ref_vector result(m);
NOT_IMPLEMENTED_YET();
return result;
}
}

View file

@ -39,23 +39,22 @@ namespace qe {
};
class term_graph {
ast_manager &m;
ast_manager & m;
ptr_vector<term> m_terms;
app_ref_vector m_lits;
u_map<term* > m_app2term;
app_ref_vector m_pinned;
u_map<app*> m_term2app;
app_ref_vector m_lits;
u_map<term* > m_app2term;
app_ref_vector m_pinned;
u_map<expr*> m_term2app;
plugin_manager<term_graph_plugin> m_plugins;
void merge(term &t1, term &t2);
term *mk_term(app *t);
term *get_term(app *t);
term *mk_term(expr *t);
term *get_term(expr *t);
term *internalize_term(app *t);
void internalize_eq(app *a1, app *a2);
term *internalize_term(expr *t);
void internalize_eq(expr *a1, expr *a2);
void internalize_lit(app *lit);
bool is_internalized(app *a);
@ -66,27 +65,35 @@ namespace qe {
void reset_marks();
app *mk_app_core(app* a);
app_ref mk_app(term const &t);
app_ref mk_app(app *a);
expr* mk_app_core(expr* a);
expr_ref mk_app(term const &t);
expr_ref mk_app(expr *a);
void mk_equalities(term const &t, app_ref_vector &out);
void mk_all_equalities(term const &t, app_ref_vector &out);
void display(std::ostream &out);
void display(std::ostream &out);
public:
term_graph(ast_manager &man);
~term_graph();
ast_manager &get_ast_manager() const { return m;}
ast_manager& get_ast_manager() const { return m;}
void add_lit(app *lit);
void add_lits(expr_ref_vector const &lits) {
for (expr* e : lits) add_lit(::to_app(e));
}
void add_eq(expr* a, expr* b);
void reset();
void to_lits(app_ref_vector &lits, bool all_equalities = false);
void to_lits(expr_ref_vector &lits, bool all_equalities = false);
app_ref to_app();
/**
* Return literals obtained by projecting added literals
* onto the vocabulary of decls (if exclude is false) or outside the
* vocabulary of decls (if exclude is true).
*/
expr_ref_vector project(func_decl_ref_vector const& decls, bool exclude);
};

View file

@ -627,7 +627,7 @@ namespace smt {
*/
void context::remove_parents_from_cg_table(enode * r1) {
// Remove parents from the congruence table
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
#if 0
{
static unsigned num_eqs = 0;
@ -672,7 +672,7 @@ namespace smt {
*/
void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) {
enode_vector & r2_parents = r2->m_parents;
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
if (!parent->is_marked())
continue;
parent->unset_mark();
@ -1002,7 +1002,7 @@ namespace smt {
r2->m_parents.shrink(r2_num_parents);
// try to reinsert parents of r1 that are not cgr
for (enode * parent : r1->get_parents()) {
for (enode * parent : enode::parents(r1)) {
TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
if (parent->is_cgc_enabled()) {
enode * cg = parent->m_cg;
@ -1197,7 +1197,7 @@ namespace smt {
bool context::is_diseq_slow(enode * n1, enode * n2) const {
if (n1->get_num_parents() > n2->get_num_parents())
std::swap(n1, n2);
for (enode * parent : n1->get_parents()) {
for (enode * parent : enode::parents(n1)) {
if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false &&
((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) ||
(parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) {
@ -1229,7 +1229,7 @@ namespace smt {
return false;
if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
for (enode* p1 : r1->get_parents()) {
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
if (p1->is_eq())
@ -1239,7 +1239,7 @@ namespace smt {
func_decl * f = p1->get_decl();
TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
unsigned num_args = p1->get_num_args();
for (enode * p2 : r2->get_parents()) {
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
continue;
if (p2->is_eq())
@ -1277,7 +1277,7 @@ namespace smt {
}
almost_cg_table & table = *(m_almost_cg_tables[depth]);
table.reset(r1, r2);
for (enode* p1 : r1->get_parents()) {
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
if (p1->is_eq())
@ -1288,7 +1288,7 @@ namespace smt {
}
if (table.empty())
return false;
for (enode * p2 : r2->get_parents()) {
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
continue;
if (p2->is_eq())
@ -4285,7 +4285,7 @@ namespace smt {
theory_var_list * l = n->get_th_var_list();
theory_id th_id = l->get_th_id();
for (enode* parent : n->get_parents()) {
for (enode * parent : enode::parents(n)) {
family_id fid = parent->get_owner()->get_family_id();
if (fid != th_id && fid != m_manager.get_basic_family_id()) {
TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);