mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2013-01-21 08:27:56 -08:00
parent a3eb6d121f 87e9015675
commit 7cad0b4a1f
3 changed files with 662 additions and 229 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/substitution/substitution.cpp
View file

@ -58,6 +58,7 @@ void substitution::pop_scope(unsigned num_scopes) {
} }
m_vars.shrink(old_sz); m_vars.shrink(old_sz);
m_scopes.shrink(new_lvl); m_scopes.shrink(new_lvl);
m_apply_cache.reset();
} }
inline void substitution::apply_visit(expr_offset const & n, bool & visited) { inline void substitution::apply_visit(expr_offset const & n, bool & visited) {

210
src/muz_qe/qe_lite.cpp
View file

@ -36,6 +36,7 @@ Revision History:
#include "for_each_expr.h" #include "for_each_expr.h"
#include "expr_safe_replace.h" #include "expr_safe_replace.h"
#include "cooperate.h" #include "cooperate.h"
#include "datatype_decl_plugin.h"
class is_variable_proc { class is_variable_proc {
public: public:
@ -80,6 +81,7 @@ namespace eq {
class der { class der {
ast_manager & m; ast_manager & m;
arith_util a; arith_util a;
datatype_util dt;
is_variable_proc* m_is_variable; is_variable_proc* m_is_variable;
var_subst m_subst; var_subst m_subst;
expr_ref_vector m_new_exprs; expr_ref_vector m_new_exprs;
@ -215,14 +217,15 @@ namespace eq {
(not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))), (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))),
and can be viewed as a disequality. and can be viewed as a disequality.
*/ */
bool is_var_diseq(expr * e, var * & v, expr_ref & t) { bool is_var_diseq(expr * e, ptr_vector<var>& vs, expr_ref_vector& ts) {
expr* e1; expr* e1;
if (m.is_not(e, e1)) { if (m.is_not(e, e1)) {
return is_var_eq(e, v, t); return is_var_eq(e, vs, ts);
} }
else if (is_var_eq(e, v, t) && m.is_bool(v)) { else if (is_var_eq(e, vs, ts) && vs.size() == 1 && m.is_bool(vs[0])) {
bool_rewriter(m).mk_not(t, t); expr_ref tmp(m);
m_new_exprs.push_back(t); bool_rewriter(m).mk_not(ts[0].get(), tmp);
ts[0] = tmp;
return true; return true;
} }
else { else {
@ -230,11 +233,11 @@ namespace eq {
} }
} }
bool solve_arith_core(app * lhs, expr * rhs, expr * eq, var* & var, expr_ref & def) { bool solve_arith_core(app * lhs, expr * rhs, expr * eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
SASSERT(a.is_add(lhs)); SASSERT(a.is_add(lhs));
bool is_int = a.is_int(lhs); bool is_int = a.is_int(lhs);
expr * a1; expr * a1, *v;
expr * v; expr_ref def(m);
rational a_val; rational a_val;
unsigned num = lhs->get_num_args(); unsigned num = lhs->get_num_args();
unsigned i; unsigned i;
@ -255,7 +258,7 @@ namespace eq {
} }
if (i == num) if (i == num)
return false; return false;
var = to_var(v); vs.push_back(to_var(v));
expr_ref inv_a(m); expr_ref inv_a(m);
if (!a_val.is_one()) { if (!a_val.is_one()) {
inv_a = a.mk_numeral(rational(1)/a_val, is_int); inv_a = a.mk_numeral(rational(1)/a_val, is_int);
@ -282,35 +285,48 @@ namespace eq {
def = a.mk_sub(rhs, a.mk_add(other_args.size(), other_args.c_ptr())); def = a.mk_sub(rhs, a.mk_add(other_args.size(), other_args.c_ptr()));
break; break;
} }
m_new_exprs.push_back(def); ts.push_back(def);
return true; return true;
} }
bool arith_solve(expr * lhs, expr * rhs, expr * eq, var* & var, expr_ref & t) { bool arith_solve(expr * lhs, expr * rhs, expr * eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
return return
(a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, t)) || (a.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, vs, ts)) ||
(a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, t)); (a.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, vs, ts));
} }
bool trival_solve(expr* lhs, expr* rhs, expr* eq, var* & v, expr_ref& t) { bool trivial_solve(expr* lhs, expr* rhs, expr* eq, ptr_vector<var>& vs, expr_ref_vector& ts) {
if (!is_variable(lhs)) { if (!is_variable(lhs)) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
} }
if (!is_variable(lhs)) { if (!is_variable(lhs)) {
return false; return false;
} }
v = to_var(lhs); vs.push_back(to_var(lhs));
t = rhs; ts.push_back(rhs);
TRACE("der", tout << mk_pp(eq, m) << "\n";); TRACE("qe_lite", tout << mk_pp(eq, m) << "\n";);
return true; return true;
} }
bool same_vars(ptr_vector<var> const& vs1, ptr_vector<var> const& vs2) const {
if (vs1.size() != vs2.size()) {
return false;
}
for (unsigned i = 0; i < vs1.size(); ++i) {
if (vs1[i] != vs2[i]) {
return false;
}
}
return true;
}
/** /**
\brief Return true if e can be viewed as a variable equality. \brief Return true if e can be viewed as a variable equality.
*/ */
bool is_var_eq(expr * e, var * & v, expr_ref & t) { bool is_var_eq(expr * e, ptr_vector<var>& vs, expr_ref_vector & ts) {
expr* lhs, *rhs; expr* lhs, *rhs;
// (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
@ -323,16 +339,15 @@ namespace eq {
if (!is_neg_var(m, lhs)) { if (!is_neg_var(m, lhs)) {
return false; return false;
} }
v = to_var(lhs); vs.push_back(to_var(lhs));
t = m.mk_not(rhs); ts.push_back(m.mk_not(rhs));
m_new_exprs.push_back(t); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true; return true;
} }
if (trival_solve(lhs, rhs, e, v, t)) { if (trivial_solve(lhs, rhs, e, vs, ts)) {
return true; return true;
} }
if (arith_solve(lhs, rhs, e, v, t)) { if (arith_solve(lhs, rhs, e, vs, ts)) {
return true; return true;
} }
return false; return false;
@ -341,12 +356,13 @@ namespace eq {
// (ite cond (= VAR t) (= VAR t2)) case // (ite cond (= VAR t) (= VAR t2)) case
expr* cond, *e2, *e3; expr* cond, *e2, *e3;
if (m.is_ite(e, cond, e2, e3)) { if (m.is_ite(e, cond, e2, e3)) {
if (is_var_eq(e2, v, t)) { if (is_var_eq(e2, vs, ts)) {
expr_ref t2(m); expr_ref_vector ts2(m);
var* v2; ptr_vector<var> vs2;
if (is_var_eq(e3, v2, t2) && v2 == v) { if (is_var_eq(e3, vs2, ts2) && same_vars(vs, vs2)) {
t = m.mk_ite(cond, t, t2); for (unsigned i = 0; i < vs.size(); ++i) {
m_new_exprs.push_back(t); ts[i] = m.mk_ite(cond, ts[i].get(), ts2[i].get());
}
return true; return true;
} }
} }
@ -355,17 +371,17 @@ namespace eq {
// VAR = true case // VAR = true case
if (is_variable(e)) { if (is_variable(e)) {
t = m.mk_true(); ts.push_back(m.mk_true());
v = to_var(e); vs.push_back(to_var(e));
TRACE("der", tout << mk_pp(e, m) << "\n";); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true; return true;
} }
// VAR = false case // VAR = false case
if (is_neg_var(m, e)) { if (is_neg_var(m, e)) {
t = m.mk_false(); ts.push_back(m.mk_false());
v = to_var(to_app(e)->get_arg(0)); vs.push_back(to_var(to_app(e)->get_arg(0)));
TRACE("der", tout << mk_pp(e, m) << "\n";); TRACE("qe_lite", tout << mk_pp(e, m) << "\n";);
return true; return true;
} }
@ -373,12 +389,12 @@ namespace eq {
} }
bool is_var_def(bool check_eq, expr* e, var*& v, expr_ref& t) { bool is_var_def(bool check_eq, expr* e, ptr_vector<var>& vs, expr_ref_vector& ts) {
if (check_eq) { if (check_eq) {
return is_var_eq(e, v, t); return is_var_eq(e, vs, ts);
} }
else { else {
return is_var_diseq(e, v, t); return is_var_diseq(e, vs, ts);
} }
} }
@ -393,7 +409,7 @@ namespace eq {
der_sort_vars(m_inx2var, m_map, m_order); der_sort_vars(m_inx2var, m_map, m_order);
TRACE("der", TRACE("qe_lite",
tout << "Elimination m_order:" << std::endl; tout << "Elimination m_order:" << std::endl;
for(unsigned i=0; i<m_order.size(); i++) for(unsigned i=0; i<m_order.size(); i++)
{ {
@ -520,8 +536,6 @@ namespace eq {
} }
void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) { void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) {
var * v = 0;
expr_ref t(m);
def_count = 0; def_count = 0;
largest_vinx = 0; largest_vinx = 0;
m_map.reset(); m_map.reset();
@ -532,24 +546,102 @@ namespace eq {
// Find all definitions // Find all definitions
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
checkpoint(); checkpoint();
if (is_var_def(is_exists, args[i], v, t)) { ptr_vector<var> vs;
unsigned idx = v->get_idx(); expr_ref_vector ts(m);
if(m_map.get(idx, 0) == 0) { if (is_var_def(is_exists, args[i], vs, ts)) {
m_map.reserve(idx + 1, 0); for (unsigned j = 0; j < vs.size(); ++j) {
m_inx2var.reserve(idx + 1, 0); var* v = vs[j];
m_map[idx] = t; expr* t = ts[j].get();
m_inx2var[idx] = v; unsigned idx = v->get_idx();
m_pos2var[i] = idx; if (m_map.get(idx, 0) == 0) {
def_count++; m_map.reserve(idx + 1, 0);
largest_vinx = std::max(idx, largest_vinx); m_inx2var.reserve(idx + 1, 0);
m_map[idx] = t;
m_inx2var[idx] = v;
m_pos2var[i] = idx;
def_count++;
largest_vinx = std::max(idx, largest_vinx);
m_new_exprs.push_back(t);
}
} }
} }
} }
} }
void flatten_definitions(expr_ref_vector& conjs) {
TRACE("qe_lite",
expr_ref tmp(m);
tmp = m.mk_and(conjs.size(), conjs.c_ptr());
tout << mk_pp(tmp, m) << "\n";);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* c = conjs[i].get();
expr* l, *r;
if (m.is_false(c)) {
conjs[0] = c;
conjs.resize(1);
break;
}
if (is_ground(c)) {
continue;
}
if (!m.is_eq(c, l, r)) {
continue;
}
if (!is_app(l) || !is_app(r)) {
continue;
}
if (dt.is_constructor(to_app(l)->get_decl())) {
flatten_constructor(to_app(l), to_app(r), conjs);
conjs[i] = conjs.back();
conjs.pop_back();
--i;
continue;
}
if (dt.is_constructor(to_app(r)->get_decl())) {
flatten_constructor(to_app(r), to_app(l), conjs);
conjs[i] = conjs.back();
conjs.pop_back();
--i;
continue;
}
}
TRACE("qe_lite",
expr_ref tmp(m);
tmp = m.mk_and(conjs.size(), conjs.c_ptr());
tout << "after flatten\n" << mk_pp(tmp, m) << "\n";);
}
void flatten_constructor(app* c, app* r, expr_ref_vector& conjs) {
SASSERT(dt.is_constructor(c));
func_decl* d = c->get_decl();
if (dt.is_constructor(r->get_decl())) {
app* b = to_app(r);
if (d == b->get_decl()) {
for (unsigned j = 0; j < c->get_num_args(); ++j) {
conjs.push_back(m.mk_eq(c->get_arg(j), b->get_arg(j)));
}
}
else {
conjs.push_back(m.mk_false());
}
}
else {
func_decl* rec = dt.get_constructor_recognizer(d);
conjs.push_back(m.mk_app(rec, r));
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d);
for (unsigned i = 0; i < acc.size(); ++i) {
conjs.push_back(m.mk_eq(c->get_arg(i), m.mk_app(acc[i], r)));
}
}
}
bool reduce_var_set(expr_ref_vector& conjs) { bool reduce_var_set(expr_ref_vector& conjs) {
unsigned def_count = 0; unsigned def_count = 0;
unsigned largest_vinx = 0; unsigned largest_vinx = 0;
flatten_definitions(conjs);
find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx);
@ -578,12 +670,22 @@ namespace eq {
} }
public: public:
der(ast_manager & m): m(m), a(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m), m_cancel(false) {} der(ast_manager & m):
m(m),
a(m),
dt(m),
m_is_variable(0),
m_subst(m),
m_new_exprs(m),
m_subst_map(m),
m_new_args(m),
m_rewriter(m),
m_cancel(false) {}
void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
TRACE("der", tout << mk_pp(q, m) << "\n";); TRACE("qe_lite", tout << mk_pp(q, m) << "\n";);
pr = 0; pr = 0;
r = q; r = q;
reduce_quantifier(q, r, pr); reduce_quantifier(q, r, pr);

680
src/muz_qe/tab_context.cpp
View file

@ -23,93 +23,324 @@ Revision History:
#include "dl_context.h" #include "dl_context.h"
#include "dl_mk_rule_inliner.h" #include "dl_mk_rule_inliner.h"
#include "smt_kernel.h" #include "smt_kernel.h"
#include "matcher.h"
#include "qe_lite.h" #include "qe_lite.h"
#include "bool_rewriter.h" #include "bool_rewriter.h"
#include "th_rewriter.h"
#include "datatype_decl_plugin.h"
namespace datalog { namespace tb {
#if 0
// semantic matcher. // semantic matcher.
class tab_matcher { class matcher {
typedef std::pair<expr *, expr *> expr_pair; typedef std::pair<expr *, expr *> expr_pair;
ast_manager& m;
svector<expr_pair> m_todo; svector<expr_pair> m_todo;
datatype_util m_dt;
lbool is_eq(expr* _s, expr* _t) {
if (_s == _t) {
return l_true;
}
if (!is_app(_s) || !is_app(_t)) {
return l_undef;
}
app* s = to_app(_s);
app* t = to_app(_t);
if (m.is_value(s) && m.is_value(t)) {
IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
return l_false;
}
if (m_dt.is_constructor(s) && m_dt.is_constructor(t)) {
if (s->get_decl() == t->get_decl()) {
lbool state = l_true;
for (unsigned i = 0; i < s->get_num_args(); ++i) {
// move is_eq: decompose arguments to constraints.
switch (is_eq(s->get_arg(i), t->get_arg(i))) {
case l_undef:
state = l_undef;
break;
case l_false:
return l_false;
default:
break;
}
}
return state;
}
else {
IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";);
return l_false;
}
}
return l_undef;
}
bool match_var(var* v, app* t, substitution& s, expr_ref_vector& conds) {
expr_offset r;
if (s.find(v, 0, r)) {
app* p = to_app(r.get_expr());
switch (is_eq(p, t)) {
case l_true:
break;
case l_false:
return false;
default:
conds.push_back(m.mk_eq(p, t));
break;
}
}
else {
s.insert(v, 0, expr_offset(t, 1));
}
return true;
}
bool match_app(app* p, app* t, substitution& s, expr_ref_vector& conds) {
if (p->get_decl() == t->get_decl() &&
p->get_num_args() == t->get_num_args()) {
for (unsigned i = 0; i < p->get_num_args(); ++i) {
m_todo.push_back(expr_pair(p->get_arg(i), t->get_arg(i)));
}
return true;
}
else {
switch(is_eq(p, t)) {
case l_true:
return true;
case l_false:
return false;
default:
conds.push_back(m.mk_eq(p, t));
return true;
}
}
}
public: public:
matcher(ast_manager& m): m(m) {} matcher(ast_manager& m): m(m), m_dt(m) {}
bool operator()(expr* pat, expr* term, substitution& s, expr_ref_vector& side_conds) { bool operator()(expr* pat, expr* term, substitution& s, expr_ref_vector& conds) {
m_todo.reset(); m_todo.reset();
m_todo.push_back(expr_pair(pat, term)); m_todo.push_back(expr_pair(pat, term));
while (!m_todo.empty()) { while (!m_todo.empty()) {
expr_pair const& p = m_todo.back(); expr_pair const& p = m_todo.back();
pat = p.first; pat = p.first;
term = p.second; term = p.second;
if (is_var(pat)) { m_todo.pop_back();
if (!is_app(term)) {
IF_VERBOSE(2, verbose_stream() << "term is not app\n";);
return false;
}
else if (is_var(pat) && match_var(to_var(pat), to_app(term), s, conds)) {
continue;
}
else if (!is_app(pat)) {
IF_VERBOSE(2, verbose_stream() << "pattern is not app\n";);
return false;
}
else if (!match_app(to_app(pat), to_app(term), s, conds)) {
return false;
} }
} }
return true;
} }
}; };
#endif
class goal {
th_rewriter m_rw;
datalog::rule_ref m_goal;
app_ref m_head;
app_ref_vector m_predicates;
expr_ref m_constraint;
unsigned m_index;
unsigned m_num_vars;
unsigned m_predicate_index;
unsigned m_rule_index;
unsigned m_ref;
public:
goal(datalog::rule_manager& rm):
m_rw(rm.get_manager()),
m_goal(rm),
m_head(rm.get_manager()),
m_predicates(rm.get_manager()),
m_constraint(rm.get_manager()),
m_index(0),
m_num_vars(0),
m_predicate_index(0),
m_rule_index(0),
m_ref(0) {
}
void set_rule_index(unsigned i) { m_rule_index = i; }
unsigned get_rule_index() const { return m_rule_index; }
void inc_rule_index() { m_rule_index++; }
unsigned get_predicate_index() const { return m_predicate_index; }
void set_predicate_index(unsigned i) { m_predicate_index = i; }
unsigned get_num_predicates() const { return m_predicates.size(); }
app* get_predicate(unsigned i) const { return m_predicates[i]; }
expr* get_constraint() const { return m_constraint; }
datalog::rule const& get_rule() const { return *m_goal; }
unsigned get_num_vars() const { return m_num_vars; }
unsigned get_index() const { return m_index; }
app* get_head() const { return m_head; }
void init(datalog::rule_ref& g) {
m_goal = g;
m_index = 0;
m_predicate_index = 0;
m_rule_index = 0;
m_num_vars = 1 + g.get_manager().get_var_counter().get_max_var(*g);
init();
// IF_VERBOSE(1, display(verbose_stream()););
}
void set_index(unsigned index) {
m_index = index;
}
void inc_ref() {
m_ref++;
}
void dec_ref() {
--m_ref;
if (m_ref == 0) {
dealloc(this);
}
}
void display(std::ostream& out) const {
ast_manager& m = m_head.get_manager();
expr_ref_vector fmls(m);
expr_ref fml(m);
for (unsigned i = 0; i < m_predicates.size(); ++i) {
fmls.push_back(m_predicates[i]);
}
fmls.push_back(m_constraint);
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml);
out << mk_pp(fml, m) << "\n";
}
private:
// x = t[y], if x does not occur in t[y], then add t[y] to subst.
void init() {
m_predicates.reset();
ast_manager& m = m_head.get_manager();
unsigned delta[1] = { 0 };
datalog::rule_manager& rm = m_goal.m();
unsigned num_vars = rm.get_var_counter().get_max_var(*m_goal);
substitution subst(m);
subst.reserve(1, num_vars+1);
expr_ref_vector fmls(m);
expr_ref tmp(m);
unsigned utsz = m_goal->get_uninterpreted_tail_size();
unsigned tsz = m_goal->get_tail_size();
for (unsigned i = utsz; i < tsz; ++i) {
fmls.push_back(m_goal->get_tail(i));
}
datalog::flatten_and(fmls);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* e = fmls[i].get();
expr* t, *v;
if ((m.is_eq(e, v, t) && is_var(v) && !subst.contains(to_var(v), 0)) ||
(m.is_eq(e, t, v) && is_var(v) && !subst.contains(to_var(v), 0))) {
subst.push_scope();
subst.insert(to_var(v)->get_idx(), 0, expr_offset(t, 0));
if (!subst.acyclic()) {
subst.pop_scope();
}
}
}
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint);
subst.apply(1, delta, expr_offset(m_constraint, 0), m_constraint);
subst.apply(1, delta, expr_offset(m_goal->get_head(), 0), tmp);
m_head = to_app(tmp);
m_rw(m_constraint);
for (unsigned i = 0; i < utsz; ++i) {
subst.apply(1, delta, expr_offset(m_goal->get_tail(i), 0), tmp);
m_predicates.push_back(to_app(tmp));
}
}
};
// subsumption index structure. // subsumption index structure.
class tab_index { class index {
ast_manager& m; ast_manager& m;
rule_manager& rm; datalog::rule_manager& rm;
context& m_ctx; datalog::context& m_ctx;
app_ref_vector m_preds; app_ref_vector m_preds;
expr_ref m_precond; expr_ref m_precond;
rule_ref_vector m_rules; expr_ref_vector m_sideconds;
svector<unsigned> m_num_vars; vector<ref<goal> > m_index;
matcher m_matcher; matcher m_matcher;
substitution m_subst; substitution m_subst;
qe_lite m_qe; qe_lite m_qe;
uint_set m_empty_set; uint_set m_empty_set;
bool_rewriter m_rw; bool_rewriter m_rw;
smt_params m_fparams; smt_params m_fparams;
smt::kernel m_solver; smt::kernel m_solver;
volatile bool m_cancel;
public: public:
tab_index(ast_manager& m, rule_manager& rm, context& ctx): index(datalog::context& ctx):
m(m), m(ctx.get_manager()),
rm(rm), rm(ctx.get_rule_manager()),
m_ctx(ctx), m_ctx(ctx),
m_preds(m), m_preds(m),
m_precond(m), m_precond(m),
m_rules(rm), m_sideconds(m),
m_matcher(m), m_matcher(m),
m_subst(m), m_subst(m),
m_qe(m), m_qe(m),
m_rw(m), m_rw(m),
m_solver(m, m_fparams) {} m_solver(m, m_fparams),
m_cancel(false) {}
void insert(rule* r) { void insert(ref<goal>& g) {
m_rules.push_back(r); m_index.push_back(g);
m_num_vars.push_back(1+rm.get_var_counter().get_max_var(*r));
} }
bool is_subsumed(rule const& r) { bool is_subsumed(goal const& g, unsigned& subsumer) {
setup(r); setup(g);
m_solver.push(); m_solver.push();
m_solver.assert_expr(m_precond); m_solver.assert_expr(m_precond);
bool found = find_match(); bool found = find_match(subsumer);
m_solver.pop(1); m_solver.pop(1);
return found; return found;
} }
void cancel() {
m_cancel = true;
m_solver.cancel();
m_qe.set_cancel(true);
}
void cleanup() {
m_solver.reset_cancel();
m_qe.set_cancel(false);
m_cancel = false;
}
private: private:
void setup(rule const& r) { void setup(goal const& g) {
m_preds.reset(); m_preds.reset();
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
expr_ref_vector vars(m); expr_ref_vector vars(m);
expr_ref fml(m); expr_ref fml(m);
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
r.get_vars(sorts); for (unsigned i = 0; i < g.get_num_predicates(); ++i) {
unsigned utsz = r.get_uninterpreted_tail_size(); get_free_vars(g.get_predicate(i), sorts);
unsigned tsz = r.get_tail_size(); }
get_free_vars(g.get_constraint(), sorts);
var_subst vs(m, false); var_subst vs(m, false);
for (unsigned i = 0; i < sorts.size(); ++i) { for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) { if (!sorts[i]) {
@ -117,24 +348,27 @@ namespace datalog {
} }
vars.push_back(m.mk_const(symbol(i), sorts[i])); vars.push_back(m.mk_const(symbol(i), sorts[i]));
} }
for (unsigned i = 0; i < utsz; ++i) { for (unsigned i = 0; i < g.get_num_predicates(); ++i) {
fml = r.get_tail(i); vs(g.get_predicate(i), vars.size(), vars.c_ptr(), fml);
vs(fml, vars.size(), vars.c_ptr(), fml);
m_preds.push_back(to_app(fml)); m_preds.push_back(to_app(fml));
} }
for (unsigned i = utsz; i < tsz; ++i) { vs(g.get_constraint(), vars.size(), vars.c_ptr(), fml);
fml = r.get_tail(i); fmls.push_back(fml);
vs(fml, vars.size(), vars.c_ptr(), fml);
fmls.push_back(fml);
}
m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); m_precond = m.mk_and(fmls.size(), fmls.c_ptr());
IF_VERBOSE(2,
verbose_stream() << "setup-match: ";
for (unsigned i = 0; i < m_preds.size(); ++i) {
verbose_stream() << mk_pp(m_preds[i].get(), m) << " ";
}
verbose_stream() << mk_pp(m_precond, m) << "\n";);
} }
// extract pre_cond => post_cond validation obligation from match. // extract pre_cond => post_cond validation obligation from match.
bool find_match() { bool find_match(unsigned& subsumer) {
for (unsigned i = 0; i < m_rules.size(); ++i) { for (unsigned i = 0; !m_cancel && i < m_index.size(); ++i) {
if (match_rule(i)) { if (match_rule(i)) {
subsumer = m_index[i]->get_index();
return true; return true;
} }
} }
@ -145,44 +379,62 @@ namespace datalog {
// for now: skip multiple matches within the same rule (incomplete). // for now: skip multiple matches within the same rule (incomplete).
// //
bool match_rule(unsigned rule_index) { bool match_rule(unsigned rule_index) {
rule const& r = *m_rules[rule_index]; goal const& g = *m_index[rule_index];
unsigned num_vars = m_num_vars[rule_index];
m_subst.reset(); m_subst.reset();
m_subst.reserve(2, num_vars); m_subst.reserve(2, g.get_num_vars());
// IF_VERBOSE(1, r.display(m_ctx, verbose_stream() << "try-match\n");); IF_VERBOSE(2, g.display(verbose_stream() << "try-match\n"););
return match_predicates(0, r); return match_predicates(0, g);
} }
bool match_predicates(unsigned predicate_index, rule const& r) {
if (predicate_index == r.get_uninterpreted_tail_size()) { bool match_predicates(unsigned predicate_index, goal const& g) {
return check_substitution(r); if (predicate_index == g.get_num_predicates()) {
return check_substitution(g);
} }
app* p = r.get_tail(predicate_index);
for (unsigned i = 0; i < m_preds.size(); ++i) { app* q = g.get_predicate(predicate_index);
for (unsigned i = 0; !m_cancel && i < m_preds.size(); ++i) {
app* p = m_preds[i].get();
m_subst.push_scope(); m_subst.push_scope();
if (m_matcher(p, m_preds[i].get(), m_subst) && unsigned limit = m_sideconds.size();
match_predicates(predicate_index + 1, r)) { IF_VERBOSE(2,
for (unsigned j = 0; j < predicate_index; ++j) verbose_stream() << " ";
verbose_stream() << mk_pp(q, m) << " = " << mk_pp(p, m) << "\n";
);
if (q->get_decl() == p->get_decl() &&
m_matcher(q, p, m_subst, m_sideconds) &&
match_predicates(predicate_index + 1, g)) {
return true; return true;
} }
m_subst.pop_scope(); m_subst.pop_scope(1);
m_sideconds.resize(limit);
} }
return false; return false;
} }
bool check_substitution(rule const& r) { bool check_substitution(goal const& g) {
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
unsigned deltas[2] = {0, 0}; unsigned deltas[2] = {0, 0};
expr_ref_vector fmls(m);
expr_ref q(m), postcond(m); expr_ref q(m), postcond(m);
expr_ref_vector fmls(m_sideconds);
for (unsigned i = utsz; i < tsz; ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
app* p = r.get_tail(i); m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q);
m_subst.apply(2, deltas, expr_offset(p, 0), q); fmls[i] = q;
fmls.push_back(q);
} }
m_subst.apply(2, deltas, expr_offset(g.get_constraint(), 0), q);
fmls.push_back(q);
IF_VERBOSE(2,
for (unsigned i = 0; i < g.get_num_predicates(); ++i) {
verbose_stream() << " ";
}
q = m.mk_and(fmls.size(), fmls.c_ptr());
verbose_stream() << "check: " << mk_pp(q, m) << "\n";);
m_qe(m_empty_set, false, fmls); m_qe(m_empty_set, false, fmls);
m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond); m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond);
@ -205,7 +457,107 @@ namespace datalog {
} }
}; };
enum tab_instruction { // predicate selection strategy.
class selection {
datalog::context& m_ctx;
ast_manager& m;
datalog::rule_manager& rm;
datatype_util dt;
obj_map<func_decl, unsigned_vector> m_scores;
unsigned_vector m_score_values;
public:
selection(datalog::context& ctx):
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
dt(m) {
}
void init(datalog::rule_set const& rules) {
m_scores.reset();
goal g(rm);
datalog::rule_ref r(rm);
datalog::rule_set::iterator it = rules.begin();
datalog::rule_set::iterator end = rules.end();
for (; it != end; ++it) {
r = *it;
g.init(r);
app* p = g.get_head();
unsigned_vector scores;
score_predicate(p, scores);
insert_score(p->get_decl(), scores);
}
}
unsigned select(goal const& g) {
unsigned min_distance = UINT_MAX;
unsigned result = 0;
unsigned_vector& scores = m_score_values;
for (unsigned i = 0; i < g.get_num_predicates(); ++i) {
scores.reset();
score_predicate(g.get_predicate(i), scores);
unsigned dist = compute_distance(g.get_predicate(i)->get_decl(), scores);
if (dist < min_distance) {
min_distance = dist;
result = i;
}
}
return result;
}
private:
unsigned compute_distance(func_decl* f, unsigned_vector const& scores) {
unsigned_vector f_scores;
unsigned dist = 0;
if (m_scores.find(f, f_scores)) {
SASSERT(f_scores.size() == scores.size());
for (unsigned i = 0; i < scores.size(); ++i) {
unsigned d1 = scores[i] - f_scores[i];
dist += d1*d1;
}
}
// else there is no rule.
return dist;
}
void score_predicate(app* p, unsigned_vector& scores) {
for (unsigned i = 0; i < p->get_num_args(); ++i) {
scores.push_back(score_argument(p->get_arg(i)));
}
}
unsigned score_argument(expr* arg) {
if (is_var(arg)) {
return 0;
}
if (m.is_value(arg)) {
return 3;
}
if (is_app(arg) && dt.is_constructor(to_app(arg)->get_decl())) {
return 2;
}
return 1;
}
void insert_score(func_decl* f, unsigned_vector const& scores) {
obj_map<func_decl, unsigned_vector>::obj_map_entry* e = m_scores.find_core(f);
if (e) {
unsigned_vector & old_scores = e->get_data().m_value;
SASSERT(scores.size() == old_scores.size());
for (unsigned i = 0; i < scores.size(); ++i) {
old_scores[i] += scores[i];
}
}
else {
m_scores.insert(f, scores);
}
}
};
enum instruction {
SELECT_RULE, SELECT_RULE,
SELECT_PREDICATE, SELECT_PREDICATE,
BACKTRACK, BACKTRACK,
@ -214,7 +566,7 @@ namespace datalog {
CANCEL CANCEL
}; };
std::ostream& operator<<(std::ostream& out, tab_instruction i) { std::ostream& operator<<(std::ostream& out, instruction i) {
switch(i) { switch(i) {
case SELECT_RULE: return out << "select-rule"; case SELECT_RULE: return out << "select-rule";
case SELECT_PREDICATE: return out << "select-predicate"; case SELECT_PREDICATE: return out << "select-predicate";
@ -225,8 +577,9 @@ namespace datalog {
} }
return out << "unmatched instruction"; return out << "unmatched instruction";
} }
};
namespace datalog {
class tab::imp { class tab::imp {
struct stats { struct stats {
@ -234,58 +587,20 @@ namespace datalog {
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
unsigned m_num_unfold; unsigned m_num_unfold;
unsigned m_num_no_unfold; unsigned m_num_no_unfold;
unsigned m_num_subsume; unsigned m_num_subsumed;
}; };
class goal {
public:
rule_ref m_goal;
// app_ref m_head;
// app_ref_vector m_predicates;
// expr_ref m_constraint;
unsigned m_index;
unsigned m_predicate_index;
unsigned m_rule_index;
goal(rule_manager& rm):
m_goal(rm),
// m_head(m),
// m_predicates(m),
// m_constraint(m),
m_index(0),
m_predicate_index(0),
m_rule_index(0) {
}
#if 0
private:
void init() {
m_head = m_goal.get_head();
unsigned utsz = m_goal->get_uninterpreted_tail_size();
unsigned tsz = m_goal->get_tail_size();
for (unsigned i = 0; i < utsz; ++i) {
m_predicates.push_back(m_goal->get_tail(i));
}
expr_ref fmls(m);
for (unsigned i = utsz; i < tsz; ++i) {
fmls.push_back(m_goal->get_tail(i));
}
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint);
}
#endif
};
context& m_ctx; context& m_ctx;
ast_manager& m; ast_manager& m;
rule_manager& rm; rule_manager& rm;
tab_index m_subsumption_index; tb::index m_index;
tb::selection m_selection;
smt_params m_fparams; smt_params m_fparams;
smt::kernel m_solver; smt::kernel m_solver;
rule_unifier m_unifier; rule_unifier m_unifier;
rule_set m_rules; rule_set m_rules;
vector<goal> m_goals; vector<ref<tb::goal> > m_goals;
goal m_goal; tb::instruction m_instruction;
tab_instruction m_instruction;
unsigned m_goal_index; unsigned m_goal_index;
volatile bool m_cancel; volatile bool m_cancel;
stats m_stats; stats m_stats;
@ -294,12 +609,12 @@ namespace datalog {
m_ctx(ctx), m_ctx(ctx),
m(ctx.get_manager()), m(ctx.get_manager()),
rm(ctx.get_rule_manager()), rm(ctx.get_rule_manager()),
m_subsumption_index(m, rm, ctx), m_index(ctx),
m_selection(ctx),
m_solver(m, m_fparams), m_solver(m, m_fparams),
m_unifier(ctx), m_unifier(ctx),
m_rules(ctx), m_rules(ctx),
m_goal(rm), m_instruction(tb::SELECT_PREDICATE),
m_instruction(SELECT_PREDICATE),
m_cancel(false), m_cancel(false),
m_goal_index(0) m_goal_index(0)
{ {
@ -314,21 +629,27 @@ namespace datalog {
m_ctx.ensure_opened(); m_ctx.ensure_opened();
m_rules.reset(); m_rules.reset();
m_rules.add_rules(m_ctx.get_rules()); m_rules.add_rules(m_ctx.get_rules());
m_selection.init(m_rules);
rule_ref_vector query_rules(rm); rule_ref_vector query_rules(rm);
rule_ref goal(rm); rule_ref goal(rm);
func_decl_ref query_pred(m); func_decl_ref query_pred(m);
rm.mk_query(query, query_pred, query_rules, goal); rm.mk_query(query, query_pred, query_rules, goal);
init_goal(goal); init_goal(goal);
IF_VERBOSE(1, display_goal(m_goal, verbose_stream());); IF_VERBOSE(1, display_goal(*get_goal(), verbose_stream() << "g" << get_goal()->get_index() << " "););
return run(); return run();
} }
void cancel() { void cancel() {
m_cancel = true; m_cancel = true;
m_index.cleanup();
m_solver.cancel();
} }
void cleanup() { void cleanup() {
m_cancel = false; m_cancel = false;
m_goals.reset(); m_goals.reset();
m_index.cleanup();
m_solver.reset_cancel();
} }
void reset_statistics() { void reset_statistics() {
m_stats.reset(); m_stats.reset();
@ -336,7 +657,7 @@ namespace datalog {
void collect_statistics(statistics& st) const { void collect_statistics(statistics& st) const {
st.update("tab.num_unfold", m_stats.m_num_unfold); st.update("tab.num_unfold", m_stats.m_num_unfold);
st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold); st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold);
st.update("tab.num_subsume", m_stats.m_num_subsume); st.update("tab.num_subsumed", m_stats.m_num_subsumed);
} }
void display_certificate(std::ostream& out) const { void display_certificate(std::ostream& out) const {
// TBD // TBD
@ -348,90 +669,100 @@ namespace datalog {
private: private:
void select_predicate() { void select_predicate() {
rule_ref& query = m_goal.m_goal; unsigned num_predicates = get_goal()->get_num_predicates();
unsigned num_predicates = query->get_uninterpreted_tail_size();
if (num_predicates == 0) { if (num_predicates == 0) {
m_instruction = UNSATISFIABLE; m_instruction = tb::UNSATISFIABLE;
IF_VERBOSE(2, query->display(m_ctx, verbose_stream()); ); IF_VERBOSE(2, get_goal()->display(verbose_stream()); );
} }
else { else {
m_instruction = SELECT_RULE; m_instruction = tb::SELECT_RULE;
unsigned pi = 0; // TBD replace by better selection function. unsigned pi = m_selection.select(*get_goal());
m_goal.m_predicate_index = pi; get_goal()->set_predicate_index(pi);
m_goal.m_rule_index = 0; get_goal()->set_rule_index(0);
IF_VERBOSE(2, verbose_stream() << mk_pp(query->get_tail(pi), m) << "\n";); IF_VERBOSE(2, verbose_stream() << mk_pp(get_goal()->get_predicate(pi), m) << "\n";);
} }
} }
void apply_rule(rule const& r) { void apply_rule(rule const& r) {
rule_ref& query = m_goal.m_goal; ref<tb::goal> goal = get_goal();
rule const& query = goal->get_rule();
rule_ref new_query(rm); rule_ref new_query(rm);
if (m_unifier.unify_rules(*query, m_goal.m_predicate_index, r) && if (m_unifier.unify_rules(query, goal->get_predicate_index(), r) &&
m_unifier.apply(*query, m_goal.m_predicate_index, r, new_query) && m_unifier.apply(query, goal->get_predicate_index(), r, new_query) &&
l_false != query_is_sat(*new_query.get()) && l_false != query_is_sat(*new_query.get())) {
!query_is_subsumed(*new_query.get())) { ref<tb::goal> next_goal = init_goal(new_query);
m_stats.m_num_unfold++; unsigned subsumer = 0;
m_subsumption_index.insert(query.get());
m_goals.push_back(m_goal);
init_goal(new_query);
IF_VERBOSE(1, IF_VERBOSE(1,
display_premise(m_goals.back(), verbose_stream()); display_premise(*goal, verbose_stream() << "g" << next_goal->get_index() << " ");
display_goal(m_goal, verbose_stream());); display_goal(*next_goal, verbose_stream()););
m_instruction = SELECT_PREDICATE; if (m_index.is_subsumed(*next_goal, subsumer)) {
IF_VERBOSE(1, verbose_stream() << "subsumed by " << subsumer << "\n";);
m_stats.m_num_subsumed++;
m_goals.pop_back();
m_instruction = tb::SELECT_RULE;
}
else {
m_stats.m_num_unfold++;
m_index.insert(next_goal);
m_instruction = tb::SELECT_PREDICATE;
}
} }
else { else {
m_stats.m_num_no_unfold++; m_stats.m_num_no_unfold++;
m_instruction = SELECT_RULE; m_instruction = tb::SELECT_RULE;
} }
} }
void select_rule() { void select_rule() {
func_decl* p = m_goal.m_goal->get_decl(m_goal.m_predicate_index); func_decl* p = get_goal()->get_predicate(get_goal()->get_predicate_index())->get_decl();
rule_vector const& rules = m_rules.get_predicate_rules(p); rule_vector const& rules = m_rules.get_predicate_rules(p);
if (rules.size() <= m_goal.m_rule_index) { if (rules.size() <= get_goal()->get_rule_index()) {
m_instruction = BACKTRACK; m_instruction = tb::BACKTRACK;
} }
else { else {
apply_rule(*rules[m_goal.m_rule_index++]); unsigned index = get_goal()->get_rule_index();
get_goal()->inc_rule_index();
apply_rule(*rules[index]);
} }
} }
void backtrack() { void backtrack() {
SASSERT(!m_goals.empty());
m_goals.pop_back();
if (m_goals.empty()) { if (m_goals.empty()) {
m_instruction = SATISFIABLE; m_instruction = tb::SATISFIABLE;
} }
else { else {
m_goal = m_goals.back(); m_instruction = tb::SELECT_RULE;
m_goals.pop_back();
m_instruction = SELECT_RULE;
} }
} }
lbool run() { lbool run() {
m_instruction = SELECT_PREDICATE; m_instruction = tb::SELECT_PREDICATE;
while (true) { while (true) {
IF_VERBOSE(2, verbose_stream() << m_instruction << "\n";);
if (m_cancel) { if (m_cancel) {
cleanup(); cleanup();
return l_undef; return l_undef;
} }
switch(m_instruction) { switch(m_instruction) {
case SELECT_PREDICATE: case tb::SELECT_PREDICATE:
select_predicate(); select_predicate();
break; break;
case SELECT_RULE: case tb::SELECT_RULE:
select_rule(); select_rule();
break; break;
case BACKTRACK: case tb::BACKTRACK:
backtrack(); backtrack();
break; break;
case SATISFIABLE: case tb::SATISFIABLE:
return l_false; return l_false;
case UNSATISFIABLE: case tb::UNSATISFIABLE:
return l_true; return l_true;
case CANCEL: case tb::CANCEL:
m_cancel = false; cleanup();
return l_undef; return l_undef;
} }
} }
@ -456,7 +787,9 @@ namespace datalog {
names.push_back(symbol(i)); names.push_back(symbol(i));
} }
fml = m.mk_and(fmls.size(), fmls.c_ptr()); fml = m.mk_and(fmls.size(), fmls.c_ptr());
fml = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml); if (!sorts.empty()) {
fml = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml);
}
m_solver.push(); m_solver.push();
m_solver.assert_expr(fml); m_solver.assert_expr(fml);
lbool is_sat = m_solver.check(); lbool is_sat = m_solver.check();
@ -467,24 +800,21 @@ namespace datalog {
return is_sat; return is_sat;
} }
bool query_is_subsumed(rule const& query) { ref<tb::goal> init_goal(rule_ref& new_query) {
return m_subsumption_index.is_subsumed(query); ref<tb::goal> goal = alloc(tb::goal, rm);
goal->init(new_query);
goal->set_index(m_goal_index++);
m_goals.push_back(goal);
return goal;
} }
void init_goal(rule_ref& new_query) { ref<tb::goal> get_goal() const { return m_goals.back(); }
m_goal.m_goal = new_query;
m_goal.m_index = m_goal_index++;
m_goal.m_predicate_index = 0;
m_goal.m_rule_index = 0;
}
void display_premise(tb::goal& p, std::ostream& out) {
void display_premise(goal& p, std::ostream& out) { out << "{g" << p.get_index() << " p" << p.get_predicate_index() << " r" << p.get_rule_index() << "}\n";
out << "[" << p.m_index << "]: " << p.m_predicate_index << ":" << p.m_rule_index << "\n";
} }
void display_goal(goal& g, std::ostream& out) { void display_goal(tb::goal& g, std::ostream& out) {
out << g.m_index << " "; g.display(out);
g.m_goal->display(m_ctx, out);
} }
}; };