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

optimize rule processing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-26 11:43:06 -07:00
parent 83add2bd9b
commit c58b4f9a53
28 changed files with 267 additions and 200 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -93,7 +93,9 @@ void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) {
m_sorts.reset();
::get_free_vars(pred->get_arg(i), m_sorts);
m_todo.reset();
m_mark.reset();
::get_free_vars(m_mark, m_todo, pred->get_arg(i), m_sorts);
for (unsigned j = 0; j < m_sorts.size(); ++j) {
if (m_sorts[j]) {
update(j, coef);

2
src/ast/rewriter/ast_counter.h
View file

@ -38,6 +38,7 @@ public:
counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
void reset() { m_data.reset(); }
iterator begin() const { return m_data.begin(); }
iterator end() const { return m_data.end(); }
void update(unsigned el, int delta);
@ -71,6 +72,7 @@ protected:
ptr_vector<sort> m_sorts;
expr_fast_mark1 m_visited;
ptr_vector<expr> m_todo;
ast_mark m_mark;
unsigned_vector m_scopes;
unsigned get_max_var(bool & has_var);
public:

35
src/ast/rewriter/var_subst.cpp
View file

@ -17,7 +17,6 @@ Notes:
--*/
#include"var_subst.h"
#include"used_vars.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
#include"ast_smt2_pp.h"
@ -40,7 +39,7 @@ void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, exp
tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
SASSERT(is_well_sorted(m, q));
if (is_ground(q->get_expr())) {
// ignore patterns if the body is a ground formula.
@ -51,11 +50,11 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
result = q;
return;
}
used_vars used;
used.process(q->get_expr());
m_used.reset();
m_used.process(q->get_expr());
unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; i++)
used.process(q->get_pattern(i));
m_used.process(q->get_pattern(i));
unsigned num_no_patterns = q->get_num_no_patterns();
for (unsigned i = 0; i < num_no_patterns; i++)
used.process(q->get_no_pattern(i));
@ -110,9 +109,8 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size());
expr_ref new_expr(m);
var_subst subst(m);
subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
m_subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
if (num_removed == num_decls) {
result = new_expr;
@ -145,7 +143,12 @@ void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
num_no_patterns,
new_no_patterns.c_ptr());
to_quantifier(result)->set_no_unused_vars();
SASSERT(is_well_sorted(m, result));
SASSERT(is_well_sorted(m, result));
}
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
unused_vars_eliminator el(m);
el(q, result);
}
void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result) {
@ -161,9 +164,7 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
}
static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sorts) {
ast_mark mark;
ptr_vector<expr> todo;
static void get_free_vars_offset(ast_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
@ -175,7 +176,9 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
switch(e->get_kind()) {
case AST_QUANTIFIER: {
quantifier* q = to_quantifier(e);
get_free_vars_offset(q->get_expr(), offset+q->get_num_decls(), sorts);
ast_mark mark1;
ptr_vector<expr> todo1;
get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
break;
}
case AST_VAR: {
@ -207,5 +210,11 @@ static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sor
void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
get_free_vars_offset(e, 0, sorts);
ast_mark mark;
ptr_vector<expr> todo;
get_free_vars_offset(mark, todo, 0, e, sorts);
}
void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
get_free_vars_offset(mark, todo, 0, e, sorts);
}

12
src/ast/rewriter/var_subst.h
View file

@ -20,6 +20,7 @@ Notes:
#define _VAR_SUBST_H_
#include"rewriter.h"
#include"used_vars.h"
/**
\brief Alias for var_shifter class.
@ -53,6 +54,15 @@ public:
/**
\brief Eliminate the unused variables from \c q. Store the result in \c r.
*/
class unused_vars_eliminator {
ast_manager& m;
var_subst m_subst;
used_vars m_used;
public:
unused_vars_eliminator(ast_manager& m): m(m), m_subst(m) {}
void operator()(quantifier* q, expr_ref& r);
};
void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
/**
@ -73,6 +83,8 @@ void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref
*/
void get_free_vars(expr* e, ptr_vector<sort>& sorts);
void get_free_vars(ast_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts);
#endif

3
src/muz_qe/dl_context.cpp
View file

@ -226,6 +226,7 @@ namespace datalog {
m_rewriter(m),
m_var_subst(m),
m_rule_manager(*this),
m_elim_unused_vars(m),
m_transf(*this),
m_trail(*this),
m_pinned(m),
@ -332,7 +333,7 @@ namespace datalog {
quantifier_ref q(m);
sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
elim_unused_vars(m, q, result);
m_elim_unused_vars(q, result);
}
}
return result;

1
src/muz_qe/dl_context.h
View file

@ -84,6 +84,7 @@ namespace datalog {
th_rewriter m_rewriter;
var_subst m_var_subst;
rule_manager m_rule_manager;
unused_vars_eliminator m_elim_unused_vars;
rule_transformer m_transf;
trail_stack<context> m_trail;
ast_ref_vector m_pinned;

4
src/muz_qe/dl_finite_product_relation.cpp
View file

@ -1291,8 +1291,8 @@ namespace datalog {
m_renaming_for_inner_rel(m_manager) {
relation_manager & rmgr = r.get_manager();
idx_set cond_columns;
collect_vars(m_manager, m_cond, cond_columns);
rule_manager& rm = r.get_context().get_rule_manager();
idx_set& cond_columns = rm.collect_vars(m_cond);
unsigned sig_sz = r.get_signature().size();
for(unsigned i=0; i<sig_sz; i++) {

7
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -145,7 +145,6 @@ namespace datalog {
expr_ref_vector conjs(m), new_conjs(m);
expr_ref tmp(m);
expr_safe_replace sub(m);
uint_set lhs_vars, rhs_vars;
bool change = false;
bool inserted = false;
@ -161,10 +160,8 @@ namespace datalog {
if (is_store_def(e, x, y)) {
// enforce topological order consistency:
uint_set lhs;
collect_vars(m, x, lhs_vars);
collect_vars(m, y, rhs_vars);
lhs = lhs_vars;
uint_set lhs = rm.collect_vars(x);
uint_set rhs_vars = rm.collect_vars(y);
lhs &= rhs_vars;
if (!lhs.empty()) {
TRACE("dl", tout << "unusable equality " << mk_pp(e, m) << "\n";);

1
src/muz_qe/dl_mk_array_blast.h
View file

@ -38,6 +38,7 @@ namespace datalog {
rule_manager& rm;
params_ref m_params;
th_rewriter m_rewriter;
ptr_vector<sort> m_vars;
mk_interp_tail_simplifier m_simplifier;
typedef obj_map<app, var*> defs_t;

28
src/muz_qe/dl_mk_filter_rules.cpp
View file

@ -27,9 +27,10 @@ namespace datalog {
mk_filter_rules::mk_filter_rules(context & ctx):
plugin(2000),
m_context(ctx),
m_manager(ctx.get_manager()),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_result(0),
m_pinned(m_manager) {
m_pinned(m) {
}
mk_filter_rules::~mk_filter_rules() {
@ -52,14 +53,14 @@ namespace datalog {
*/
bool mk_filter_rules::is_candidate(app * pred) {
if (!m_context.is_predicate(pred)) {
TRACE("mk_filter_rules", tout << mk_pp(pred, m_manager) << "\nis not a candidate because it is interpreted.\n";);
TRACE("mk_filter_rules", tout << mk_pp(pred, m) << "\nis not a candidate because it is interpreted.\n";);
return false;
}
var_idx_set used_vars;
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) {
expr * arg = pred->get_arg(i);
if (m_manager.is_value(arg))
if (m.is_value(arg))
return true;
SASSERT(is_var(arg));
unsigned vidx = to_var(arg)->get_idx();
@ -74,10 +75,10 @@ namespace datalog {
\brief Create a "filter" (if it doesn't exist already) for the given predicate.
*/
func_decl * mk_filter_rules::mk_filter_decl(app * pred, var_idx_set const & non_local_vars) {
sort_ref_buffer filter_domain(m_manager);
sort_ref_buffer filter_domain(m);
filter_key * key = alloc(filter_key, m_manager);
mk_new_rule_tail(m_manager, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
filter_key * key = alloc(filter_key, m);
mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
func_decl * filter_decl = 0;
if (!m_tail2filter.find(key, filter_decl)) {
filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"),
@ -85,8 +86,8 @@ namespace datalog {
m_pinned.push_back(filter_decl);
m_tail2filter.insert(key, filter_decl);
app_ref filter_head(m_manager);
filter_head = m_manager.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app_ref filter_head(m);
filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app * filter_tail = key->new_pred;
rule * filter_rule = m_context.get_rule_manager().mk(filter_head, 1, &filter_tail, (const bool *)0);
filter_rule->set_accounting_parent_object(m_context, m_current);
@ -104,16 +105,15 @@ namespace datalog {
void mk_filter_rules::process(rule * r) {
m_current = r;
app * new_head = r->get_head();
app_ref_vector new_tail(m_manager);
app_ref_vector new_tail(m);
svector<bool> new_is_negated;
unsigned sz = r->get_tail_size();
bool rule_modified = false;
for (unsigned i = 0; i < sz; i++) {
app * tail = r->get_tail(i);
if (is_candidate(tail)) {
TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m_manager) << "\n";);
var_idx_set non_local_vars;
collect_non_local_vars(m_manager, r, tail, non_local_vars);
TRACE("mk_filter_rules", tout << "is_candidate: " << mk_pp(tail, m) << "\n";);
var_idx_set non_local_vars = rm.collect_rule_vars_ex(r, tail);
func_decl * filter_decl = mk_filter_decl(tail, non_local_vars);
ptr_buffer<expr> new_args;
var_idx_set used_vars;
@ -129,7 +129,7 @@ namespace datalog {
}
}
SASSERT(new_args.size() == filter_decl->get_arity());
new_tail.push_back(m_manager.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
new_tail.push_back(m.mk_app(filter_decl, new_args.size(), new_args.c_ptr()));
rule_modified = true;
}
else {

3
src/muz_qe/dl_mk_filter_rules.h
View file

@ -59,7 +59,8 @@ namespace datalog {
typedef obj_map<filter_key, func_decl*> filter_cache;
context & m_context;
ast_manager & m_manager;
ast_manager & m;
rule_manager & rm;
filter_cache m_tail2filter;
rule_set * m_result;
rule * m_current;

45
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -67,24 +67,23 @@ namespace datalog {
void mk_interp_tail_simplifier::rule_substitution::get_result(rule_ref & res) {
SASSERT(m_rule);
app_ref new_head(m);
apply(m_rule->get_head(), new_head);
apply(m_rule->get_head(), m_head);
app_ref_vector tail(m);
svector<bool> tail_neg;
m_tail.reset();
m_neg.reset();
unsigned tail_len = m_rule->get_tail_size();
for (unsigned i=0; i<tail_len; i++) {
app_ref new_tail_el(m);
apply(m_rule->get_tail(i), new_tail_el);
tail.push_back(new_tail_el);
tail_neg.push_back(m_rule->is_neg_tail(i));
m_tail.push_back(new_tail_el);
m_neg.push_back(m_rule->is_neg_tail(i));
}
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
SASSERT(tail.size() == tail_neg.size());
res = m_context.get_rule_manager().mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
SASSERT(m_tail.size() == m_neg.size());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr());
res->set_accounting_parent_object(m_context, m_rule);
res->norm_vars(res.get_manager());
}
@ -362,14 +361,34 @@ namespace datalog {
}
};
class mk_interp_tail_simplifier::normalizer_rw : public rewriter_tpl<normalizer_cfg> {
public:
normalizer_rw(ast_manager& m, normalizer_cfg& cfg): rewriter_tpl<normalizer_cfg>(m, false, cfg) {}
};
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_cfg = alloc(normalizer_cfg, m);
m_rw = alloc(normalizer_rw, m, *m_cfg);
}
mk_interp_tail_simplifier::~mk_interp_tail_simplifier() {
dealloc(m_rw);
dealloc(m_cfg);
}
void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res)
{
expr_ref simp1_res(m);
m_simp(a, simp1_res);
normalizer_cfg r_cfg(m);
rewriter_tpl<normalizer_cfg> rwr(m, false, r_cfg);
expr_ref dl_form_e(m);
rwr(simp1_res.get(), res);
(*m_rw)(simp1_res.get(), res);
/*if (simp1_res.get()!=res.get()) {
std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";

27
src/muz_qe/dl_mk_interp_tail_simplifier.h
View file

@ -34,15 +34,17 @@ namespace datalog {
{
ast_manager& m;
context& m_context;
substitution m_subst;
unifier m_unif;
rule * m_rule;
substitution m_subst;
unifier m_unif;
app_ref m_head;
app_ref_vector m_tail;
svector<bool> m_neg;
rule * m_rule;
void apply(app * a, app_ref& res);
public:
rule_substitution(context & ctx)
: m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_rule(0) {}
: m(ctx.get_manager()), m_context(ctx), m_subst(m), m_unif(m), m_head(m), m_tail(m), m_rule(0) {}
/**
Reset substitution and get it ready for working with rule r.
@ -61,13 +63,17 @@ namespace datalog {
}
};
class normalizer_cfg;
class normalizer_rw;
ast_manager & m;
context & m_context;
th_rewriter & m_simp;
arith_util a;
rule_substitution m_rule_subst;
normalizer_cfg* m_cfg;
normalizer_rw* m_rw;
class normalizer_cfg;
void simplify_expr(app * a, expr_ref& res);
@ -77,13 +83,8 @@ namespace datalog {
/** Return true if something was modified */
bool transform_rules(const rule_set & orig, rule_set & tgt);
public:
mk_interp_tail_simplifier(context & ctx, unsigned priority=40000)
: plugin(priority),
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx) {}
mk_interp_tail_simplifier(context & ctx, unsigned priority=40000);
virtual ~mk_interp_tail_simplifier();
/**If rule should be retained, assign transformed version to res and return true;
if rule can be deleted, return false.

3
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -28,6 +28,7 @@ namespace datalog {
plugin(10000, true),
m_context(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_pinned(m),
m_goal(goal, m) {
}
@ -259,7 +260,7 @@ namespace datalog {
}
new_tail.push_back(curr);
negations.push_back(r->is_neg_tail(curr_index));
collect_vars(m, curr, bound_vars);
bound_vars |= rm.collect_vars(curr);
}

1
src/muz_qe/dl_mk_magic_sets.h
View file

@ -95,6 +95,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager& rm;
ast_ref_vector m_pinned;
/**
\brief Predicates from the original set that appear in a head of a rule

4
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -505,9 +505,6 @@ namespace datalog {
unsigned head_arity = head_pred->get_arity();
//var_idx_set head_vars;
//var_idx_set same_strat_vars;
//collect_vars(m, r->get_head(), head_vars);
unsigned pt_len = r->get_positive_tail_size();
for (unsigned ti=0; ti<pt_len; ++ti) {
@ -518,7 +515,6 @@ namespace datalog {
SASSERT(pred_strat<=head_strat);
if (pred_strat==head_strat) {
//collect_vars(m, r->get_head(), same_strat_vars);
if (pred->get_arity()>head_arity
|| (pred->get_arity()==head_arity && pred->get_id()>=head_pred->get_id()) ) {
return false;

27
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -29,7 +29,8 @@ namespace datalog {
mk_simple_joins::mk_simple_joins(context & ctx):
plugin(1000),
m_context(ctx) {
m_context(ctx),
rm(ctx.get_rule_manager()) {
}
class join_planner {
@ -120,6 +121,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager & rm;
var_subst & m_var_subst;
rule_set & m_rs_aux_copy; //reference to a rule_set that will allow to ask for stratum levels
@ -130,10 +132,13 @@ namespace datalog {
ptr_hashtable<rule, ptr_hash<rule>, ptr_eq<rule> > m_modified_rules;
ast_ref_vector m_pinned;
mutable ptr_vector<sort> m_vars;
public:
join_planner(context & ctx, rule_set & rs_aux_copy)
: m_context(ctx), m(ctx.get_manager()), m_var_subst(ctx.get_var_subst()),
: m_context(ctx), m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_var_subst(ctx.get_var_subst()),
m_rs_aux_copy(rs_aux_copy),
m_introduced_rules(ctx.get_rule_manager()),
m_pinned(ctx.get_manager())
@ -175,9 +180,7 @@ namespace datalog {
unsigned max_var_idx = 0;
{
var_idx_set orig_var_set;
collect_vars(m, t1, orig_var_set);
collect_vars(m, t2, orig_var_set);
var_idx_set& orig_var_set = rm.collect_vars(t1, t2);
var_idx_set::iterator ovit = orig_var_set.begin();
var_idx_set::iterator ovend = orig_var_set.end();
for(; ovit!=ovend; ++ovit) {
@ -323,14 +326,13 @@ namespace datalog {
}
for(unsigned i=0; i<pos_tail_size; i++) {
app * t1 = r->get_tail(i);
var_idx_set t1_vars;
collect_vars(m, t1, t1_vars);
var_idx_set t1_vars = rm.collect_vars(t1);
counter.count_vars(m, t1, -1); //temporarily remove t1 variables from counter
for(unsigned j=i+1; j<pos_tail_size; j++) {
app * t2 = r->get_tail(j);
counter.count_vars(m, t2, -1); //temporarily remove t2 variables from counter
var_idx_set scope_vars(t1_vars);
collect_vars(m, t2, scope_vars);
var_idx_set scope_vars = rm.collect_vars(t2);
scope_vars |= t1_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, t2, 1); //restore t2 variables in counter
@ -472,8 +474,7 @@ namespace datalog {
while(!added_tails.empty()) {
app * a_tail = added_tails.back(); //added tail
var_idx_set a_tail_vars;
collect_vars(m, a_tail, a_tail_vars);
var_idx_set a_tail_vars = rm.collect_vars(a_tail);
counter.count_vars(m, a_tail, -1); //temporarily remove a_tail variables from counter
for(unsigned i=0; i<len; i++) {
@ -484,8 +485,8 @@ namespace datalog {
}
counter.count_vars(m, o_tail, -1); //temporarily remove o_tail variables from counter
var_idx_set scope_vars(a_tail_vars);
collect_vars(m, o_tail, scope_vars);
var_idx_set scope_vars = rm.collect_vars(o_tail);
scope_vars |= a_tail_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, o_tail, 1); //restore o_tail variables in counter

3
src/muz_qe/dl_mk_simple_joins.h
View file

@ -49,7 +49,8 @@ namespace datalog {
We say that a rule containing C_i's is a rule with a "big tail".
*/
class mk_simple_joins : public rule_transformer::plugin {
context & m_context;
context & m_context;
rule_manager & rm;
public:
mk_simple_joins(context & ctx);

28
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -27,7 +27,8 @@ namespace datalog {
plugin(500),
m_context(ctx),
m(ctx.get_manager()),
m_rules(ctx.get_rule_manager()),
rm(ctx.get_rule_manager()),
m_rules(rm),
m_pinned(m) {
}
@ -47,10 +48,7 @@ namespace datalog {
}
unsigned var_idx = to_var(head_arg)->get_idx();
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
return tail_vars.contains(var_idx);
return rm.collect_tail_vars(r).contains(var_idx);
}
void mk_unbound_compressor::add_task(func_decl * pred, unsigned arg_index) {
@ -83,8 +81,7 @@ namespace datalog {
void mk_unbound_compressor::detect_tasks(rule_set const& source, unsigned rule_index) {
rule * r = m_rules.get(rule_index);
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
var_idx_set& tail_vars = rm.collect_tail_vars(r);
app * head = r->get_head();
func_decl * head_pred = head->get_decl();
@ -94,9 +91,9 @@ namespace datalog {
}
unsigned n = head_pred->get_arity();
var_counter head_var_counter;
head_var_counter.count_vars(m, head, 1);
rm.get_counter().reset();
rm.get_counter().count_vars(m, head, 1);
for (unsigned i=0; i<n; i++) {
expr * arg = head->get_arg(i);
@ -107,7 +104,7 @@ namespace datalog {
if (!tail_vars.contains(var_idx)) {
//unbound
unsigned occurence_cnt = head_var_counter.get(var_idx);
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if (occurence_cnt == 1) {
TRACE("dl", r->display(m_context, tout << "Compress: "););
@ -121,15 +118,14 @@ namespace datalog {
void mk_unbound_compressor::try_compress(rule_set const& source, unsigned rule_index) {
start:
rule * r = m_rules.get(rule_index);
var_idx_set tail_vars;
collect_tail_vars(m, r, tail_vars);
var_idx_set& tail_vars = rm.collect_tail_vars(r);
app * head = r->get_head();
func_decl * head_pred = head->get_decl();
unsigned head_arity = head_pred->get_arity();
var_counter head_var_counter;
head_var_counter.count_vars(m, head);
rm.get_counter().reset();
rm.get_counter().count_vars(m, head);
unsigned arg_index;
for (arg_index = 0; arg_index < head_arity; arg_index++) {
@ -140,7 +136,7 @@ namespace datalog {
unsigned var_idx = to_var(arg)->get_idx();
if (!tail_vars.contains(var_idx)) {
//unbound
unsigned occurence_cnt = head_var_counter.get(var_idx);
unsigned occurence_cnt = rm.get_counter().get(var_idx);
SASSERT(occurence_cnt>0);
if ( occurence_cnt==1 && m_in_progress.contains(c_info(head_pred, arg_index)) ) {
//we have found what to compress

1
src/muz_qe/dl_mk_unbound_compressor.h
View file

@ -52,6 +52,7 @@ namespace datalog {
context & m_context;
ast_manager & m;
rule_manager & rm;
rule_ref_vector m_rules;
bool m_modified;
todo_stack m_todo;

101
src/muz_qe/dl_rule.cpp
View file

@ -48,7 +48,9 @@ namespace datalog {
rule_manager::rule_manager(context& ctx)
: m(ctx.get_manager()),
m_ctx(ctx) {}
m_ctx(ctx),
m_cfg(m),
m_rwr(m, false, m_cfg) {}
void rule_manager::inc_ref(rule * r) {
if (r) {
@ -67,29 +69,20 @@ namespace datalog {
}
}
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
return BR_FAILED;
br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
};
return BR_FAILED;
}
void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m);
remove_label_cfg r_cfg(m);
rewriter_tpl<remove_label_cfg> rwr(m, false, r_cfg);
rwr(fml, tmp);
m_rwr(fml, tmp);
if (pr && fml != tmp) {
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
@ -97,6 +90,67 @@ namespace datalog {
fml = tmp;
}
var_idx_set& rule_manager::collect_vars(expr* e) {
return collect_vars(e, 0);
}
var_idx_set& rule_manager::collect_vars(expr* e1, expr* e2) {
reset_collect_vars();
if (e1) accumulate_vars(e1);
if (e2) accumulate_vars(e2);
return finalize_collect_vars();
}
void rule_manager::reset_collect_vars() {
m_vars.reset();
m_var_idx.reset();
m_todo.reset();
m_mark.reset();
}
var_idx_set& rule_manager::finalize_collect_vars() {
unsigned sz = m_vars.size();
for (unsigned i=0; i<sz; ++i) {
if (m_vars[i]) m_var_idx.insert(i);
}
return m_var_idx;
}
var_idx_set& rule_manager::collect_tail_vars(rule * r) {
reset_collect_vars();
unsigned n = r->get_tail_size();
for (unsigned i=0;i<n;i++) {
accumulate_vars(r->get_tail(i));
}
return finalize_collect_vars();
}
var_idx_set& rule_manager::collect_rule_vars_ex(rule * r, app* t) {
reset_collect_vars();
unsigned n = r->get_tail_size();
accumulate_vars(r->get_head());
for (unsigned i=0;i<n;i++) {
if (r->get_tail(i) != t) {
accumulate_vars(r->get_tail(i));
}
}
return finalize_collect_vars();
}
var_idx_set& rule_manager::collect_rule_vars(rule * r) {
reset_collect_vars();
unsigned n = r->get_tail_size();
accumulate_vars(r->get_head());
for (unsigned i=0;i<n;i++) {
accumulate_vars(r->get_tail(i));
}
return finalize_collect_vars();
}
void rule_manager::accumulate_vars(expr* e) {
::get_free_vars(m_mark, m_todo, e, m_vars);
}
void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
@ -570,15 +624,14 @@ namespace datalog {
return;
}
ptr_vector<sort> free_rule_vars;
var_counter vctr;
app_ref_vector tail(m);
svector<bool> tail_neg;
app_ref head(r->get_head(), m);
get_free_vars(r, free_rule_vars);
collect_rule_vars(r);
vctr.count_vars(m, head);
ptr_vector<sort>& free_rule_vars = m_vars;
for (unsigned i = 0; i < ut_len; i++) {
app * t = r->get_tail(i);
@ -906,7 +959,7 @@ namespace datalog {
}
void rule::norm_vars(rule_manager & rm) {
used_vars used;
used_vars& used = rm.reset_used();
get_used_vars(used);
unsigned first_unsused = used.get_max_found_var_idx_plus_1();

41
src/muz_qe/dl_rule.h
View file

@ -27,6 +27,7 @@ Revision History:
#include"proof_converter.h"
#include"model_converter.h"
#include"ast_counter.h"
#include"rewriter.h"
namespace datalog {
@ -47,9 +48,27 @@ namespace datalog {
*/
class rule_manager
{
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);
};
ast_manager& m;
context& m_ctx;
rule_counter m_counter;
used_vars m_used;
ptr_vector<sort> m_vars;
var_idx_set m_var_idx;
ptr_vector<expr> m_todo;
ast_mark m_mark;
remove_label_cfg m_cfg;
rewriter_tpl<remove_label_cfg> m_rwr;
// only the context can create a rule_manager
friend class context;
@ -90,6 +109,10 @@ namespace datalog {
*/
void reduce_unbound_vars(rule_ref& r);
void reset_collect_vars();
var_idx_set& finalize_collect_vars();
public:
ast_manager& get_manager() const { return m; }
@ -98,6 +121,24 @@ namespace datalog {
void dec_ref(rule * r);
used_vars& reset_used() { m_used.reset(); return m_used; }
var_idx_set& collect_vars(expr * pred);
var_idx_set& collect_vars(expr * e1, expr* e2);
var_idx_set& collect_rule_vars(rule * r);
var_idx_set& collect_rule_vars_ex(rule * r, app* t);
var_idx_set& collect_tail_vars(rule * r);
void accumulate_vars(expr* pred);
ptr_vector<sort>& get_var_sorts() { return m_vars; }
var_idx_set& get_var_idx() { return m_var_idx; }
/**
\brief Create a Datalog rule from a Horn formula.
The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))

3
src/muz_qe/dl_sieve_relation.cpp
View file

@ -567,8 +567,7 @@ namespace datalog {
const relation_signature sig = r.get_signature();
unsigned sz = sig.size();
var_idx_set cond_vars;
collect_vars(m, condition, cond_vars);
var_idx_set& cond_vars = get_context().get_rule_manager().collect_vars(condition);
expr_ref_vector subst_vect(m);
subst_vect.resize(sz);
unsigned subst_ofs = sz-1;

50
src/muz_qe/dl_util.cpp
View file

@ -158,36 +158,7 @@ namespace datalog {
::get_free_vars(trm, vars);
return var_idx < vars.size() && vars[var_idx] != 0;
}
void collect_vars(ast_manager & m, expr * e, var_idx_set & result) {
ptr_vector<sort> vars;
::get_free_vars(e, vars);
unsigned sz = vars.size();
for(unsigned i=0; i<sz; ++i) {
if(vars[i]) { result.insert(i); }
}
}
void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result) {
unsigned n = r->get_tail_size();
for(unsigned i=0;i<n;i++) {
collect_vars(m, r->get_tail(i), result);
}
}
void get_free_tail_vars(rule * r, ptr_vector<sort>& sorts) {
unsigned n = r->get_tail_size();
for(unsigned i=0;i<n;i++) {
get_free_vars(r->get_tail(i), sorts);
}
}
void get_free_vars(rule * r, ptr_vector<sort>& sorts) {
get_free_vars(r->get_head(), sorts);
get_free_tail_vars(r, sorts);
}
unsigned count_variable_arguments(app * pred)
{
SASSERT(is_uninterp(pred));
@ -202,26 +173,6 @@ namespace datalog {
return res;
}
void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result) {
collect_vars(m, r->get_head(), result);
unsigned sz = r->get_tail_size();
for (unsigned i = 0; i < sz; i++) {
app * curr = r->get_tail(i);
if (curr != t)
collect_vars(m, curr, result);
}
}
void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result) {
collect_vars(m, r->get_head(), result);
unsigned sz = r->get_tail_size();
for (unsigned i = 0; i < sz; i++) {
app * curr = r->get_tail(i);
if (curr != t_1 && curr != t_2)
collect_vars(m, curr, result);
}
}
void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var,
sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
expr_ref_buffer new_args(m);
@ -404,6 +355,7 @@ namespace datalog {
void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
reset();
count_vars(m, r->get_head(), 1);
unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; i++) {

20
src/muz_qe/dl_util.h
View file

@ -81,33 +81,13 @@ namespace datalog {
void flatten_or(expr* fml, expr_ref_vector& result);
bool contains_var(expr * trm, unsigned var_idx);
/**
\brief Collect the variables in \c pred.
\pre \c pred must be a valid head or tail.
*/
void collect_vars(ast_manager & m, expr * pred, var_idx_set & result);
void collect_tail_vars(ast_manager & m, rule * r, var_idx_set & result);
void get_free_vars(rule * r, ptr_vector<sort>& sorts);
/**
\brief Return number of arguments of \c pred that are variables
*/
unsigned count_variable_arguments(app * pred);
/**
\brief Store in \c result the set of variables used by \c r when ignoring the tail \c t.
*/
void collect_non_local_vars(ast_manager & m, rule const * r, app * t, var_idx_set & result);
/**
\brief Store in \c result the set of variables used by \c r when ignoring the tail elements \c t_1 and \c t_2.
*/
void collect_non_local_vars(ast_manager & m, rule const * r, app * t_1, app * t_2, var_idx_set & result);
template<typename T>
void copy_nonvariables(app * src, T& tgt)

8
src/muz_qe/qe_lite.cpp
View file

@ -2525,15 +2525,15 @@ public:
m_params(p) {
m_imp = alloc(imp, m, p);
}
virtual tactic * translate(ast_manager & m) {
return alloc(qe_lite_tactic, m, m_params);
}
virtual ~qe_lite_tactic() {
dealloc(m_imp);
}
virtual tactic * translate(ast_manager & m) {
return alloc(qe_lite_tactic, m, m_params);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
// m_imp->updt_params(p);

2
src/smt/theory_diff_logic.h
View file

@ -316,7 +316,7 @@ namespace smt {
m_nc_functor(*this) {
}
~theory_diff_logic() {
virtual ~theory_diff_logic() {
reset_eh();
}

3
src/util/memory_manager.cpp
View file

@ -231,9 +231,8 @@ void * memory::allocate(size_t s) {
return 0;
s = s + sizeof(size_t); // we allocate an extra field!
void * r = malloc(s);
if (r == 0) {
if (r == 0)
throw_out_of_memory();
}
*(static_cast<size_t*>(r)) = s;
g_memory_thread_alloc_size += s;
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {