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

optimize rule preprocessing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-26 14:40:20 -07:00
parent b644fb9875
commit 8038c719fb
10 changed files with 149 additions and 112 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/ast_counter.cpp
View file

@ -110,24 +110,27 @@ unsigned var_counter::get_max_var(bool& has_var) {
unsigned max_var = 0;
while (!m_todo.empty()) {
expr* e = m_todo.back();
unsigned scope = m_scopes.back();
m_todo.pop_back();
m_scopes.pop_back();
if (m_visited.is_marked(e)) {
continue;
}
m_visited.mark(e, true);
switch(e->get_kind()) {
case AST_QUANTIFIER: {
var_counter aux_counter;
quantifier* q = to_quantifier(e);
m_todo.push_back(q->get_expr());
m_scopes.push_back(scope + q->get_num_decls());
bool has_var1 = false;
unsigned max_v = aux_counter.get_max_var(has_var1);
if (max_v > max_var + q->get_num_decls()) {
max_var = max_v - q->get_num_decls();
has_var = true;
}
break;
}
case AST_VAR: {
if (to_var(e)->get_idx() >= scope + max_var) {
if (to_var(e)->get_idx() >= max_var) {
has_var = true;
max_var = to_var(e)->get_idx() - scope;
max_var = to_var(e)->get_idx();
}
break;
}
@ -135,7 +138,6 @@ unsigned var_counter::get_max_var(bool& has_var) {
app* a = to_app(e);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
m_todo.push_back(a->get_arg(i));
m_scopes.push_back(scope);
}
break;
}
@ -152,14 +154,12 @@ unsigned var_counter::get_max_var(bool& has_var) {
unsigned var_counter::get_max_var(expr* e) {
bool has_var = false;
m_todo.push_back(e);
m_scopes.push_back(0);
return get_max_var(has_var);
}
unsigned var_counter::get_next_var(expr* e) {
bool has_var = false;
m_todo.push_back(e);
m_scopes.push_back(0);
unsigned mv = get_max_var(has_var);
if (has_var) mv++;
return mv;

30
src/muz_qe/dl_context.cpp
View file

@ -41,7 +41,6 @@ Revision History:
#include"for_each_expr.h"
#include"ast_smt_pp.h"
#include"ast_smt2_pp.h"
#include"expr_functors.h"
#include"dl_mk_partial_equiv.h"
#include"dl_mk_bit_blast.h"
#include"dl_mk_array_blast.h"
@ -227,6 +226,8 @@ namespace datalog {
m_rule_manager(*this),
m_elim_unused_vars(m),
m_abstractor(m),
m_contains_p(*this),
m_check_pred(m_contains_p, m),
m_transf(*this),
m_trail(*this),
m_pinned(m),
@ -302,18 +303,19 @@ namespace datalog {
expr_ref context::bind_variables(expr* fml, bool is_forall) {
expr_ref result(m);
app_ref_vector const & vars = m_vars;
rule_manager& rm = get_rule_manager();
if (vars.empty()) {
result = fml;
}
else {
ptr_vector<sort> sorts;
m_names.reset();
m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
get_free_vars(result, sorts);
rm.collect_vars(result);
ptr_vector<sort>& sorts = rm.get_var_sorts();
if (sorts.empty()) {
result = fml;
}
else {
svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
if (i < vars.size()) {
@ -324,15 +326,15 @@ namespace datalog {
}
}
if (i < vars.size()) {
names.push_back(vars[i]->get_decl()->get_name());
m_names.push_back(vars[i]->get_decl()->get_name());
}
else {
names.push_back(symbol(i));
m_names.push_back(symbol(i));
}
}
quantifier_ref q(m);
sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result);
m_elim_unused_vars(q, result);
}
}
@ -608,28 +610,16 @@ namespace datalog {
}
}
class context::contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
void context::check_existential_tail(rule_ref& r) {
unsigned ut_size = r->get_uninterpreted_tail_size();
unsigned t_size = r->get_tail_size();
contains_pred contains_p(*this);
check_pred check_pred(contains_p, get_manager());
TRACE("dl", r->display_smt2(get_manager(), tout); tout << "\n";);
for (unsigned i = ut_size; i < t_size; ++i) {
app* t = r->get_tail(i);
TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
if (check_pred(t)) {
if (m_check_pred(t)) {
std::ostringstream out;
out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate";
throw default_exception(out.str());

17
src/muz_qe/dl_context.h
View file

@ -46,6 +46,8 @@ Revision History:
#include"smt_params.h"
#include"dl_rule_transformer.h"
#include"expr_abstract.h"
#include"expr_functors.h"
namespace datalog {
@ -77,6 +79,18 @@ namespace datalog {
typedef obj_map<const func_decl, svector<symbol> > pred2syms;
typedef obj_map<const sort, sort_domain*> sort_domain_map;
class contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
ast_manager & m;
smt_params & m_fparams;
params_ref m_params_ref;
@ -87,10 +101,13 @@ namespace datalog {
rule_manager m_rule_manager;
unused_vars_eliminator m_elim_unused_vars;
expr_abstractor m_abstractor;
contains_pred m_contains_p;
check_pred m_check_pred;
rule_transformer m_transf;
trail_stack<context> m_trail;
ast_ref_vector m_pinned;
app_ref_vector m_vars;
svector<symbol> m_names;
sort_domain_map m_sorts;
func_decl_set m_preds;
sym2decl m_preds_by_name;

63
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -369,11 +369,14 @@ namespace datalog {
mk_interp_tail_simplifier::mk_interp_tail_simplifier(context & ctx, unsigned priority)
: plugin(priority),
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx) {
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx),
m_tail(m),
m_itail_members(m),
m_conj(m) {
m_cfg = alloc(normalizer_cfg, m);
m_rw = alloc(normalizer_rw, m, *m_cfg);
}
@ -404,15 +407,15 @@ namespace datalog {
return false;
}
ptr_vector<expr> todo;
m_todo.reset();
m_leqs.reset();
for (unsigned i = u_len; i < len; i++) {
todo.push_back(r->get_tail(i));
m_todo.push_back(r->get_tail(i));
SASSERT(!r->is_neg_tail(i));
}
m_rule_subst.reset(r);
obj_hashtable<expr> leqs;
expr_ref_vector trail(m);
expr_ref tmp1(m), tmp2(m);
bool found_something = false;
@ -420,10 +423,10 @@ namespace datalog {
#define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; }
#define IS_FLEX(_x) (is_var(_x) || m.is_value(_x))
while (!todo.empty()) {
while (!m_todo.empty()) {
expr * arg1, *arg2;
expr * t0 = todo.back();
todo.pop_back();
expr * t0 = m_todo.back();
m_todo.pop_back();
expr* t = t0;
bool neg = m.is_not(t, t);
if (is_var(t)) {
@ -431,7 +434,7 @@ namespace datalog {
}
else if (!neg && m.is_and(t)) {
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
m_todo.append(a->get_num_args(), a->get_args());
}
else if (!neg && m.is_eq(t, arg1, arg2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
TRY_UNIFY(arg1, arg2);
@ -459,12 +462,12 @@ namespace datalog {
else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) {
tmp1 = a.mk_sub(arg1, arg2);
tmp2 = a.mk_sub(arg2, arg1);
if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
if (false && m_leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
TRY_UNIFY(arg1, arg2);
}
else {
trail.push_back(tmp1);
leqs.insert(tmp1);
m_leqs.insert(tmp1);
}
}
}
@ -504,12 +507,12 @@ namespace datalog {
}
app_ref head(r->get_head(), m);
app_ref_vector tail(m);
svector<bool> tail_neg;
m_tail.reset();
m_tail_neg.reset();
for (unsigned i=0; i<u_len; i++) {
tail.push_back(r->get_tail(i));
tail_neg.push_back(r->is_neg_tail(i));
m_tail.push_back(r->get_tail(i));
m_tail_neg.push_back(r->is_neg_tail(i));
}
bool modified = false;
@ -521,12 +524,12 @@ namespace datalog {
SASSERT(!r->is_neg_tail(u_len));
}
else {
expr_ref_vector itail_members(m);
m_itail_members.reset();
for (unsigned i=u_len; i<len; i++) {
itail_members.push_back(r->get_tail(i));
m_itail_members.push_back(r->get_tail(i));
SASSERT(!r->is_neg_tail(i));
}
itail = m.mk_and(itail_members.size(), itail_members.c_ptr());
itail = m.mk_and(m_itail_members.size(), m_itail_members.c_ptr());
modified = true;
}
@ -542,21 +545,21 @@ namespace datalog {
SASSERT(m.is_bool(simp_res));
if (modified) {
expr_ref_vector conjs(m);
flatten_and(simp_res, conjs);
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
m_conj.reset();
flatten_and(simp_res, m_conj);
for (unsigned i = 0; i < m_conj.size(); ++i) {
expr* e = m_conj[i].get();
if (is_app(e)) {
tail.push_back(to_app(e));
m_tail.push_back(to_app(e));
}
else {
tail.push_back(m.mk_eq(e, m.mk_true()));
m_tail.push_back(m.mk_eq(e, m.mk_true()));
}
tail_neg.push_back(false);
m_tail_neg.push_back(false);
}
SASSERT(tail.size() == tail_neg.size());
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
SASSERT(m_tail.size() == m_tail_neg.size());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr());
res->set_accounting_parent_object(m_context, r);
}
else {

6
src/muz_qe/dl_mk_interp_tail_simplifier.h
View file

@ -71,6 +71,12 @@ namespace datalog {
th_rewriter & m_simp;
arith_util a;
rule_substitution m_rule_subst;
ptr_vector<expr> m_todo;
obj_hashtable<expr> m_leqs;
app_ref_vector m_tail;
expr_ref_vector m_itail_members;
expr_ref_vector m_conj;
svector<bool> m_tail_neg;
normalizer_cfg* m_cfg;
normalizer_rw* m_rw;

63
src/muz_qe/dl_rule.cpp
View file

@ -40,15 +40,18 @@ Revision History:
#include"quant_hoist.h"
#include"expr_replacer.h"
#include"bool_rewriter.h"
#include"qe_lite.h"
#include"expr_safe_replace.h"
#include"hnf.h"
namespace datalog {
rule_manager::rule_manager(context& ctx)
: m(ctx.get_manager()),
m_ctx(ctx),
m_body(m),
m_head(m),
m_args(m),
m_hnf(m),
m_qe(m),
m_cfg(m),
m_rwr(m, false, m_cfg) {}
@ -179,13 +182,13 @@ namespace datalog {
}
void rule_manager::mk_rule_core(expr* fml, proof* p, rule_set& rules, symbol const& name) {
hnf h(m);
expr_ref_vector fmls(m);
proof_ref_vector prs(m);
h.set_name(name);
h(fml, p, fmls, prs);
for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) {
m_ctx.register_predicate(h.get_fresh_predicates()[i], false);
m_hnf.reset();
m_hnf.set_name(name);
m_hnf(fml, p, fmls, prs);
for (unsigned i = 0; i < m_hnf.get_fresh_predicates().size(); ++i) {
m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false);
}
for (unsigned i = 0; i < fmls.size(); ++i) {
mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name);
@ -194,24 +197,23 @@ namespace datalog {
void rule_manager::mk_horn_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
app_ref_vector body(m);
app_ref head(m);
svector<bool> is_negated;
unsigned index = extract_horn(fml, body, head);
hoist_compound_predicates(index, head, body);
m_body.reset();
m_neg.reset();
unsigned index = extract_horn(fml, m_body, m_head);
hoist_compound_predicates(index, m_head, m_body);
TRACE("dl_rule",
tout << mk_pp(head, m) << " :- ";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << " ";
for (unsigned i = 0; i < m_body.size(); ++i) {
tout << mk_pp(m_body[i].get(), m) << " ";
}
tout << "\n";);
mk_negations(body, is_negated);
check_valid_rule(head, body.size(), body.c_ptr());
mk_negations(m_body, m_neg);
check_valid_rule(m_head, m_body.size(), m_body.c_ptr());
rule_ref r(*this);
r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
r = mk(m_head.get(), m_body.size(), m_body.c_ptr(), m_neg.c_ptr(), name);
expr_ref fml1(m);
if (p) {
@ -380,28 +382,28 @@ namespace datalog {
fml = m.mk_not(fml);
return;
}
expr_ref_vector args(m);
if (!m_ctx.is_predicate(fml)) {
return;
}
m_args.reset();
for (unsigned i = 0; i < fml->get_num_args(); ++i) {
e = fml->get_arg(i);
if (!is_app(e)) {
args.push_back(e);
m_args.push_back(e);
continue;
}
app* b = to_app(e);
if (m.is_value(b)) {
args.push_back(e);
m_args.push_back(e);
}
else {
var* v = m.mk_var(num_bound++, m.get_sort(b));
args.push_back(v);
m_args.push_back(v);
body.push_back(m.mk_eq(v, b));
}
}
fml = m.mk_app(fml->get_decl(), args.size(), args.c_ptr());
fml = m.mk_app(fml->get_decl(), m_args.size(), m_args.c_ptr());
TRACE("dl_rule", tout << mk_pp(fml.get(), m) << "\n";);
}
@ -565,29 +567,22 @@ namespace datalog {
void rule_manager::reduce_unbound_vars(rule_ref& r) {
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned t_len = r->get_tail_size();
ptr_vector<sort> vars;
uint_set index_set;
qe_lite qe(m);
expr_ref_vector conjs(m);
if (ut_len == t_len) {
return;
}
get_free_vars(r->get_head(), vars);
reset_collect_vars();
accumulate_vars(r->get_head());
for (unsigned i = 0; i < ut_len; ++i) {
get_free_vars(r->get_tail(i), vars);
accumulate_vars(r->get_tail(i));
}
var_idx_set& index_set = finalize_collect_vars();
for (unsigned i = ut_len; i < t_len; ++i) {
conjs.push_back(r->get_tail(i));
}
for (unsigned i = 0; i < vars.size(); ++i) {
if (vars[i]) {
index_set.insert(i);
}
}
qe(index_set, false, conjs);
m_qe(index_set, false, conjs);
bool change = conjs.size() != t_len - ut_len;
for (unsigned i = 0; !change && i < conjs.size(); ++i) {
change = r->get_tail(ut_len+i) != conjs[i].get();

8
src/muz_qe/dl_rule.h
View file

@ -28,6 +28,8 @@ Revision History:
#include"model_converter.h"
#include"ast_counter.h"
#include"rewriter.h"
#include"hnf.h"
#include"qe_lite.h"
namespace datalog {
@ -66,6 +68,12 @@ namespace datalog {
var_idx_set m_var_idx;
ptr_vector<expr> m_todo;
ast_mark m_mark;
app_ref_vector m_body;
app_ref m_head;
expr_ref_vector m_args;
svector<bool> m_neg;
hnf m_hnf;
qe_lite m_qe;
remove_label_cfg m_cfg;
rewriter_tpl<remove_label_cfg> m_rwr;

33
src/muz_qe/hnf.cpp
View file

@ -71,6 +71,9 @@ class hnf::imp {
obj_map<expr, app*> m_memoize_disj;
obj_map<expr, proof*> m_memoize_proof;
func_decl_ref_vector m_fresh_predicates;
expr_ref_vector m_body;
proof_ref_vector m_defs;
public:
imp(ast_manager & m):
@ -82,7 +85,9 @@ public:
m_refs(m),
m_name("P"),
m_qh(m),
m_fresh_predicates(m) {
m_fresh_predicates(m),
m_body(m),
m_defs(m) {
}
void operator()(expr * n,
@ -182,13 +187,13 @@ private:
void mk_horn(expr_ref& fml, proof_ref& premise) {
expr* e1, *e2;
expr_ref_vector body(m);
proof_ref_vector defs(m);
expr_ref fml0(m), fml1(m), fml2(m), head(m);
proof_ref p(m);
fml0 = fml;
m_names.reset();
m_sorts.reset();
m_body.reset();
m_defs.reset();
m_qh.pull_quantifier(true, fml0, &m_sorts, &m_names);
if (premise){
fml1 = bind_variables(fml0);
@ -199,12 +204,12 @@ private:
}
head = fml0;
while (m.is_implies(head, e1, e2)) {
body.push_back(e1);
m_body.push_back(e1);
head = e2;
}
datalog::flatten_and(body);
datalog::flatten_and(m_body);
if (premise) {
p = m.mk_rewrite(fml0, mk_implies(body, head));
p = m.mk_rewrite(fml0, mk_implies(m_body, head));
}
//
@ -214,8 +219,8 @@ private:
// A -> C
// B -> C
//
if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
app* _or = to_app(body[0].get());
if (m_body.size() == 1 && m.is_or(m_body[0].get()) && contains_predicate(m_body[0].get())) {
app* _or = to_app(m_body[0].get());
unsigned sz = _or->get_num_args();
expr* const* args = _or->get_args();
for (unsigned i = 0; i < sz; ++i) {
@ -224,7 +229,7 @@ private:
}
if (premise) {
expr_ref f1 = bind_variables(mk_implies(body, head));
expr_ref f1 = bind_variables(mk_implies(m_body, head));
expr* f2 = m.mk_and(sz, m_todo.c_ptr()+m_todo.size()-sz);
proof_ref p2(m), p3(m);
p2 = m.mk_def_axiom(m.mk_iff(f1, f2));
@ -240,13 +245,13 @@ private:
}
eliminate_disjunctions(body, defs);
p = mk_congruence(p, body, head, defs);
eliminate_disjunctions(m_body, m_defs);
p = mk_congruence(p, m_body, head, m_defs);
eliminate_quantifier_body(body, defs);
p = mk_congruence(p, body, head, defs);
eliminate_quantifier_body(m_body, m_defs);
p = mk_congruence(p, m_body, head, m_defs);
fml2 = mk_implies(body, head);
fml2 = mk_implies(m_body, head);
fml = bind_variables(fml2);

17
src/muz_qe/horn_subsume_model_converter.cpp
View file

@ -28,10 +28,8 @@ Revision History:
#include "well_sorted.h"
void horn_subsume_model_converter::insert(app* head, expr* body) {
func_decl_ref pred(m);
expr_ref body_res(m);
VERIFY(mk_horn(head, body, pred, body_res));
insert(pred.get(), body_res.get());
m_delay_head.push_back(head);
m_delay_body.push_back(body);
}
void horn_subsume_model_converter::insert(app* head, unsigned sz, expr* const* body) {
@ -148,6 +146,7 @@ bool horn_subsume_model_converter::mk_horn(
}
void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
//
// predicates that have not been assigned values
// in the Horn model are assumed false.
@ -174,6 +173,16 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
void horn_subsume_model_converter::operator()(model_ref& mr) {
func_decl_ref pred(m);
expr_ref body_res(m);
for (unsigned i = 0; i < m_delay_head.size(); ++i) {
VERIFY(mk_horn(m_delay_head[i].get(), m_delay_body[i].get(), pred, body_res));
insert(pred.get(), body_res.get());
}
m_delay_head.reset();
m_delay_body.reset();
TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
for (unsigned i = m_funcs.size(); i > 0; ) {
--i;

6
src/muz_qe/horn_subsume_model_converter.h
View file

@ -43,6 +43,8 @@ class horn_subsume_model_converter : public model_converter {
func_decl_ref_vector m_funcs;
expr_ref_vector m_bodies;
th_rewriter m_rewrite;
app_ref_vector m_delay_head;
expr_ref_vector m_delay_body;
void add_default_false_interpretation(expr* e, model_ref& md);
@ -56,7 +58,9 @@ class horn_subsume_model_converter : public model_converter {
public:
horn_subsume_model_converter(ast_manager& m): m(m), m_funcs(m), m_bodies(m), m_rewrite(m) {}
horn_subsume_model_converter(ast_manager& m):
m(m), m_funcs(m), m_bodies(m), m_rewrite(m),
m_delay_head(m), m_delay_body(m) {}
bool mk_horn(expr* clause, func_decl_ref& pred, expr_ref& body);