mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-28 12:48:10 -07:00
commit 8abdefef6d
46 changed files with 954 additions and 377 deletions
Download patch file Download diff file Expand all files Collapse all files

226
src/muz_qe/clp_context.cpp Normal file
View file

@ -0,0 +1,226 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
clp_context.cpp
Abstract:
Bounded CLP (symbolic simulation using Z3) context.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
--*/
#include "clp_context.h"
#include "dl_context.h"
#include "unifier.h"
#include "var_subst.h"
#include "substitution.h"
namespace datalog {
class clp::imp {
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
unsigned m_num_unfold;
unsigned m_num_no_unfold;
unsigned m_num_subsumed;
};
context& m_ctx;
ast_manager& m;
rule_manager& rm;
smt_params m_fparams;
smt::kernel m_solver;
var_subst m_var_subst;
expr_ref_vector m_ground;
app_ref_vector m_goals;
volatile bool m_cancel;
stats m_stats;
public:
imp(context& ctx):
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_solver(m, m_fparams), // TBD: can be replaced by efficient BV solver.
m_var_subst(m, false),
m_ground(m),
m_goals(m),
m_cancel(false)
{
// m_fparams.m_relevancy_lvl = 0;
m_fparams.m_mbqi = false;
m_fparams.m_soft_timeout = 1000;
}
~imp() {}
lbool query(expr* query) {
m_ctx.ensure_opened();
m_solver.reset();
m_goals.reset();
rm.mk_query(query, m_ctx.get_rules());
expr_ref head(m);
head = m_ctx.get_rules().last()->get_head();
ground(head);
m_goals.push_back(to_app(head));
return search(20, 0);
}
void cancel() {
m_cancel = true;
m_solver.cancel();
}
void cleanup() {
m_cancel = false;
m_goals.reset();
m_solver.reset_cancel();
}
void reset_statistics() {
m_stats.reset();
}
void collect_statistics(statistics& st) const {
//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_subsumed", m_stats.m_num_subsumed);
}
void display_certificate(std::ostream& out) const {
expr_ref ans = get_answer();
out << mk_pp(ans, m) << "\n";
}
expr_ref get_answer() const {
return expr_ref(m.mk_true(), m);
}
private:
void reset_ground() {
m_ground.reset();
}
void ground(expr_ref& e) {
ptr_vector<sort> sorts;
get_free_vars(e, sorts);
if (m_ground.size() < sorts.size()) {
m_ground.resize(sorts.size());
}
for (unsigned i = 0; i < sorts.size(); ++i) {
if (sorts[i] && !m_ground[i].get()) {
m_ground[i] = m.mk_fresh_const("c",sorts[i]);
}
}
m_var_subst(e, m_ground.size(), m_ground.c_ptr(), e);
}
lbool search(unsigned depth, unsigned index) {
if (index == m_goals.size()) {
return l_true;
}
if (depth == 0) {
return l_undef;
}
IF_VERBOSE(1, verbose_stream() << "search " << depth << " " << index << "\n";);
unsigned num_goals = m_goals.size();
app* head = m_goals[index].get();
rule_vector const& rules = m_ctx.get_rules().get_predicate_rules(head->get_decl());
lbool status = l_false;
for (unsigned i = 0; i < rules.size(); ++i) {
rule* r = rules[i];
m_solver.push();
reset_ground();
expr_ref tmp(m);
tmp = r->get_head();
IF_VERBOSE(2, verbose_stream() << index << " " << mk_pp(tmp, m) << "\n";);
ground(tmp);
for (unsigned j = 0; j < head->get_num_args(); ++j) {
expr_ref eq(m);
eq = m.mk_eq(head->get_arg(j), to_app(tmp)->get_arg(j));
m_solver.assert_expr(eq);
}
for (unsigned j = r->get_uninterpreted_tail_size(); j < r->get_tail_size(); ++j) {
tmp = r->get_tail(j);
ground(tmp);
m_solver.assert_expr(tmp);
}
lbool is_sat = m_solver.check();
switch (is_sat) {
case l_false:
break;
case l_true:
if (depth == 1 && (index+1 > m_goals.size() || r->get_uninterpreted_tail_size() > 0)) {
status = l_undef;
break;
}
for (unsigned j = 0; j < r->get_uninterpreted_tail_size(); ++j) {
tmp = r->get_tail(j);
ground(tmp);
m_goals.push_back(to_app(tmp));
}
switch(search(depth-1, index+1)) {
case l_undef:
status = l_undef;
// fallthrough
case l_false:
m_goals.resize(num_goals);
break;
case l_true:
return l_true;
}
break;
case l_undef:
status = l_undef;
throw default_exception("undef");
}
m_solver.pop(1);
}
return status;
}
proof_ref get_proof() const {
return proof_ref(0, m);
}
};
clp::clp(context& ctx):
m_imp(alloc(imp, ctx)) {
}
clp::~clp() {
dealloc(m_imp);
}
lbool clp::query(expr* query) {
return m_imp->query(query);
}
void clp::cancel() {
m_imp->cancel();
}
void clp::cleanup() {
m_imp->cleanup();
}
void clp::reset_statistics() {
m_imp->reset_statistics();
}
void clp::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}
void clp::display_certificate(std::ostream& out) const {
m_imp->display_certificate(out);
}
expr_ref clp::get_answer() {
return m_imp->get_answer();
}
};

45
src/muz_qe/clp_context.h Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
clp_context.h
Abstract:
Bounded CLP (symbolic simulation using Z3) context.
Author:
Nikolaj Bjorner (nbjorner) 2013-04-26
Revision History:
--*/
#ifndef _CLP_CONTEXT_H_
#define _CLP_CONTEXT_H_
#include "ast.h"
#include "lbool.h"
#include "statistics.h"
namespace datalog {
class context;
class clp {
class imp;
imp* m_imp;
public:
clp(context& ctx);
~clp();
lbool query(expr* query);
void cancel();
void cleanup();
void reset_statistics();
void collect_statistics(statistics& st) const;
void display_certificate(std::ostream& out) const;
expr_ref get_answer();
};
};
#endif

71
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"
@ -49,7 +48,6 @@ Revision History:
#include"dl_mk_quantifier_abstraction.h"
#include"dl_mk_quantifier_instantiation.h"
#include"datatype_decl_plugin.h"
#include"expr_abstract.h"
namespace datalog {
@ -226,6 +224,10 @@ namespace datalog {
m_rewriter(m),
m_var_subst(m),
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),
@ -301,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;
expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
get_free_vars(result, sorts);
m_names.reset();
m_abstractor(0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
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()) {
@ -323,16 +326,16 @@ 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);
elim_unused_vars(m, q, result);
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), m_names.c_ptr(), result);
m_elim_unused_vars(q, result);
}
}
return result;
@ -544,6 +547,8 @@ namespace datalog {
throw default_exception("get_num_levels is not supported for bmc");
case TAB_ENGINE:
throw default_exception("get_num_levels is not supported for tab");
case CLP_ENGINE:
throw default_exception("get_num_levels is not supported for clp");
default:
throw default_exception("unknown engine");
}
@ -562,6 +567,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -581,6 +588,8 @@ namespace datalog {
throw default_exception("operation is not supported for BMC engine");
case TAB_ENGINE:
throw default_exception("operation is not supported for TAB engine");
case CLP_ENGINE:
throw default_exception("operation is not supported for CLP engine");
default:
throw default_exception("unknown engine");
}
@ -607,28 +616,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());
@ -720,6 +717,10 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
case CLP_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
default:
UNREACHABLE();
break;
@ -993,6 +994,9 @@ namespace datalog {
else if (e == symbol("tab")) {
m_engine = TAB_ENGINE;
}
else if (e == symbol("clp")) {
m_engine = CLP_ENGINE;
}
if (m_engine == LAST_ENGINE) {
expr_fast_mark1 mark;
@ -1028,6 +1032,8 @@ namespace datalog {
return bmc_query(query);
case TAB_ENGINE:
return tab_query(query);
case CLP_ENGINE:
return clp_query(query);
default:
UNREACHABLE();
return rel_query(query);
@ -1092,11 +1098,22 @@ namespace datalog {
}
}
void context::ensure_clp() {
if (!m_clp.get()) {
m_clp = alloc(clp, *this);
}
}
lbool context::tab_query(expr* query) {
ensure_tab();
return m_tab->query(query);
}
lbool context::clp_query(expr* query) {
ensure_clp();
return m_clp->query(query);
}
void context::ensure_rel() {
if (!m_rel.get()) {
m_rel = alloc(rel_context, *this);
@ -1137,6 +1154,10 @@ namespace datalog {
ensure_tab();
m_last_answer = m_tab->get_answer();
return m_last_answer.get();
case CLP_ENGINE:
ensure_clp();
m_last_answer = m_clp->get_answer();
return m_last_answer.get();
default:
UNREACHABLE();
}
@ -1162,6 +1183,10 @@ namespace datalog {
ensure_tab();
m_tab->display_certificate(out);
return true;
case CLP_ENGINE:
ensure_clp();
m_clp->display_certificate(out);
return true;
default:
return false;
}

25
src/muz_qe/dl_context.h
View file

@ -45,6 +45,9 @@ Revision History:
#include"model2expr.h"
#include"smt_params.h"
#include"dl_rule_transformer.h"
#include"expr_abstract.h"
#include"expr_functors.h"
#include"clp_context.h"
namespace datalog {
@ -76,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;
@ -84,10 +99,15 @@ namespace datalog {
th_rewriter m_rewriter;
var_subst m_var_subst;
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;
@ -104,6 +124,7 @@ namespace datalog {
scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
scoped_ptr<tab> m_tab;
scoped_ptr<clp> m_clp;
bool m_closed;
bool m_saturation_was_run;
@ -457,6 +478,8 @@ namespace datalog {
void ensure_tab();
void ensure_clp();
void ensure_rel();
void new_query();
@ -469,6 +492,8 @@ namespace datalog {
lbool tab_query(expr* query);
lbool clp_query(expr* query);
void check_quantifier_free(rule_ref& r);
void check_uninterpreted_free(rule_ref& r);
void check_existential_tail(rule_ref& r);

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";);

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;

98
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,37 @@ 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_tail(m),
m_itail_members(m),
m_conj(m) {
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";
@ -385,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;
@ -401,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)) {
@ -412,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);
@ -440,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);
}
}
}
@ -485,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;
@ -502,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;
}
@ -523,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 {

33
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,23 @@ 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;
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;
class normalizer_cfg;
void simplify_expr(app * a, expr_ref& res);
@ -77,13 +89,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

30
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;
@ -709,8 +705,7 @@ namespace datalog {
#define PRT(_x_) ((_x_)?"T":"F")
bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
bool done_something = false;
unsigned sz = rules->get_num_rules();
@ -731,7 +726,7 @@ namespace datalog {
svector<bool>& can_expand = m_head_visitor.can_expand();
for (unsigned i = 0; i < sz; ++i) {
add_rule(source, acc[i].get(), i);
add_rule(*rules, acc[i].get(), i);
}
// initialize substitution.
@ -808,7 +803,7 @@ namespace datalog {
TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
del_rule(r, i);
add_rule(source, rl_res.get(), i);
add_rule(*rules, rl_res.get(), i);
r = rl_res;
@ -828,13 +823,15 @@ namespace datalog {
}
}
if (done_something) {
rules = alloc(rule_set, m_context);
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
for (unsigned i = 0; i < sz; ++i) {
if (valid.get(i)) {
rules->add_rule(acc[i].get());
res->add_rule(acc[i].get());
}
}
TRACE("dl", rules->display(tout););
res->inherit_predicates(*rules);
TRACE("dl", res->display(tout););
rules = res.detach();
}
return done_something;
}
@ -871,11 +868,17 @@ namespace datalog {
// try eager inlining
if (do_eager_inlining(res)) {
something_done = true;
}
}
TRACE("dl", res->display(tout << "after eager inlining\n"););
}
if (something_done) {
res->inherit_predicates(source);
}
else {
res = alloc(rule_set, source);
}
if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
if (m_context.get_params().inline_linear() && inline_linear(res)) {
something_done = true;
}
@ -883,7 +886,6 @@ namespace datalog {
res = 0;
}
else {
res->inherit_predicates(source);
m_context.add_model_converter(hsmc.get());
}

2
src/muz_qe/dl_mk_rule_inliner.h
View file

@ -172,7 +172,7 @@ namespace datalog {
/**
Inline predicates that are known to not be join-points.
*/
bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
bool inline_linear(scoped_ptr<rule_set>& rules);
void add_rule(rule_set const& rule_set, rule* r, unsigned i);
void del_rule(rule* r, unsigned i);

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);

3
src/muz_qe/dl_mk_slice.cpp
View file

@ -725,6 +725,9 @@ namespace datalog {
m_mc->add_predicate(p, f);
}
}
else if (src.is_output_predicate(p)) {
dst.set_output_predicate(p);
}
}
}

6
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -241,6 +241,7 @@ namespace datalog {
tgt.add_rule(new_rule);
subs_index.add(new_rule);
}
tgt.inherit_predicates(orig);
TRACE("dl",
tout << "original set size: "<<orig.get_num_rules()<<"\n"
<< "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
@ -338,7 +339,7 @@ namespace datalog {
rule_set * res = alloc(rule_set, m_context);
bool modified = transform_rules(source, *res);
if(!m_have_new_total_rule && !modified) {
if (!m_have_new_total_rule && !modified) {
dealloc(res);
return 0;
}
@ -347,7 +348,7 @@ namespace datalog {
//During the construction of the new set we may discover new total relations
//(by quantifier elimination on the uninterpreted tails).
SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
while(m_have_new_total_rule) {
while (m_have_new_total_rule) {
m_have_new_total_rule = false;
rule_set * old = res;
@ -355,7 +356,6 @@ namespace datalog {
transform_rules(*old, *res);
dealloc(old);
}
res->inherit_predicates(source);
return res;
}

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;

172
src/muz_qe/dl_rule.cpp
View file

@ -40,15 +40,20 @@ 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_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) {}
void rule_manager::inc_ref(rule * r) {
if (r) {
@ -67,29 +72,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 +93,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);
@ -125,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);
@ -140,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) {
@ -326,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";);
}
@ -511,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();
@ -570,15 +619,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 +954,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();
@ -1004,16 +1052,14 @@ namespace datalog {
}
svector<symbol> names;
used_symbols<> us;
us(fml);
sorts.reverse();
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) {
sorts[i] = m.mk_bool_sort();
}
}
us(fml);
sorts.reverse();
for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
func_decl_ref f(m);

49
src/muz_qe/dl_rule.h
View file

@ -27,6 +27,9 @@ Revision History:
#include"proof_converter.h"
#include"model_converter.h"
#include"ast_counter.h"
#include"rewriter.h"
#include"hnf.h"
#include"qe_lite.h"
namespace datalog {
@ -47,9 +50,33 @@ 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;
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;
// only the context can create a rule_manager
friend class context;
@ -90,6 +117,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 +129,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++) {

21
src/muz_qe/dl_util.h
View file

@ -54,6 +54,7 @@ namespace datalog {
BMC_ENGINE,
QBMC_ENGINE,
TAB_ENGINE,
CLP_ENGINE,
LAST_ENGINE
};
@ -81,33 +82,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)

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);

16
src/muz_qe/horn_tactic.cpp
View file

@ -125,12 +125,13 @@ class horn_tactic : public tactic {
enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
formula_kind get_formula_kind(expr_ref& f) {
normalize(f);
expr_ref tmp(f);
normalize(tmp);
ast_mark mark;
expr_ref_vector args(m), body(m);
expr_ref head(m);
expr* a = 0, *a1 = 0;
datalog::flatten_or(f, args);
datalog::flatten_or(tmp, args);
for (unsigned i = 0; i < args.size(); ++i) {
a = args[i].get();
check_predicate(mark, a);
@ -147,12 +148,12 @@ class horn_tactic : public tactic {
body.push_back(m.mk_not(a));
}
}
f = m.mk_and(body.size(), body.c_ptr());
if (head) {
f = m.mk_implies(f, head);
// f = m.mk_implies(f, head);
return IS_RULE;
}
else {
f = m.mk_and(body.size(), body.c_ptr());
return IS_QUERY;
}
}
@ -171,7 +172,7 @@ class horn_tactic : public tactic {
tactic_report report("horn", *g);
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {
if (produce_proofs) {
if (!m_ctx.get_params().generate_proof_trace()) {
params_ref params = m_ctx.get_params().p;
params.set_bool("generate_proof_trace", true);
@ -239,10 +240,13 @@ class horn_tactic : public tactic {
switch (is_reachable) {
case l_true: {
// goal is unsat
g->assert_expr(m.mk_false());
if (produce_proofs) {
proof_ref proof = m_ctx.get_proof();
pc = proof2proof_converter(m, proof);
g->assert_expr(m.mk_false(), proof, 0);
}
else {
g->assert_expr(m.mk_false());
}
break;
}

14
src/muz_qe/pdr_context.cpp
View file

@ -43,6 +43,7 @@ Notes:
#include "ast_ll_pp.h"
#include "proof_checker.h"
#include "smt_value_sort.h"
#include "proof_utils.h"
namespace pdr {
@ -275,7 +276,7 @@ namespace pdr {
src.pop_back();
}
else if (is_invariant(tgt_level, curr, false, assumes_level)) {
add_property(curr, assumes_level?tgt_level:infty_level);
TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);
src[i] = src.back();
@ -1225,6 +1226,7 @@ namespace pdr {
m_search(m_params.bfs_model_search()),
m_last_result(l_undef),
m_inductive_lvl(0),
m_expanded_lvl(0),
m_cancel(false)
{
}
@ -1680,6 +1682,9 @@ namespace pdr {
proof = m_search.get_proof_trace(*this);
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
apply(m, m_pc.get(), proof);
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
// proof_utils::push_instantiations_up(proof);
// TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
return proof;
}
@ -1711,6 +1716,7 @@ namespace pdr {
bool reachable;
while (true) {
checkpoint();
m_expanded_lvl = lvl;
reachable = check_reachability(lvl);
if (reachable) {
throw model_exception();
@ -1769,6 +1775,10 @@ namespace pdr {
void context::expand_node(model_node& n) {
SASSERT(n.is_open());
expr_ref_vector cube(m);
if (n.level() < m_expanded_lvl) {
m_expanded_lvl = n.level();
}
if (n.pt().is_reachable(n.state())) {
TRACE("pdr", tout << "reachable\n";);
@ -1835,7 +1845,7 @@ namespace pdr {
if (m_params.simplify_formulas_pre()) {
simplify_formulas();
}
for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
checkpoint();
bool all_propagated = true;
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();

1
src/muz_qe/pdr_context.h
View file

@ -303,6 +303,7 @@ namespace pdr {
mutable model_search m_search;
lbool m_last_result;
unsigned m_inductive_lvl;
unsigned m_expanded_lvl;
ptr_vector<core_generalizer> m_core_generalizers;
stats m_stats;
volatile bool m_cancel;

30
src/muz_qe/pdr_util.cpp
View file

@ -1081,6 +1081,7 @@ namespace pdr {
arith_util a;
bv_util bv;
bool m_is_dl;
bool m_test_for_utvpi;
bool is_numeric(expr* e) const {
if (a.is_numeral(e)) {
@ -1115,6 +1116,16 @@ namespace pdr {
}
return false;
}
if (m_test_for_utvpi) {
if (a.is_mul(e, e1, e2)) {
if (is_minus_one(e1)) {
return is_offset(e2);
}
if (is_minus_one(e2)) {
return is_offset(e1);
}
}
}
return !is_arith_expr(e);
}
@ -1140,6 +1151,9 @@ namespace pdr {
if (!a.is_add(lhs, arg1, arg2))
return false;
// x
if (m_test_for_utvpi) {
return is_offset(arg1) && is_offset(arg2);
}
if (is_arith_expr(arg1))
std::swap(arg1, arg2);
if (is_arith_expr(arg1))
@ -1209,8 +1223,10 @@ namespace pdr {
}
public:
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
void test_for_utvpi() { m_test_for_utvpi = true; }
void operator()(expr* e) {
if (!m_is_dl) {
return;
@ -1248,6 +1264,16 @@ namespace pdr {
return test.is_dl();
}
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
test_diff_logic test(m);
test.test_for_utvpi();
expr_fast_mark1 mark;
for (unsigned i = 0; i < num_fmls; ++i) {
quick_for_each_expr(test, mark, fmls[i]);
}
return test.is_dl();
}
}
template class rewriter_tpl<pdr::ite_hoister_cfg>;

2
src/muz_qe/pdr_util.h
View file

@ -151,6 +151,8 @@ namespace pdr {
bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
}
#endif

91
src/muz_qe/proof_utils.cpp
View file

@ -1,6 +1,7 @@
#include "dl_util.h"
#include "proof_utils.h"
#include "ast_smt2_pp.h"
#include "var_subst.h"
class reduce_hypotheses {
typedef obj_hashtable<expr> expr_set;
@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) {
obj_map<proof,proof*> cache;
::permute_unit_resolution(refs, cache, pr);
}
class push_instantiations_up_cl {
ast_manager& m;
public:
push_instantiations_up_cl(ast_manager& m): m(m) {}
void operator()(proof_ref& p) {
expr_ref_vector s0(m);
p = push(p, s0);
}
private:
proof* push(proof* p, expr_ref_vector const& sub) {
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
for (unsigned i = 0; i < premises.size(); ++i) {
compose(substs[i], sub);
premises[i] = push(premises[i].get(), substs[i]);
substs[i].reset();
}
instantiate(sub, conclusion);
return
m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion,
positions,
substs);
}
if (sub.empty()) {
return p;
}
if (m.is_modus_ponens(p)) {
SASSERT(m.get_num_parents(p) == 2);
proof* p0 = m.get_parent(p, 0);
proof* p1 = m.get_parent(p, 1);
if (m.get_fact(p0) == m.get_fact(p)) {
return push(p0, sub);
}
expr* e1, *e2;
if (m.is_rewrite(p1, e1, e2) &&
is_quantifier(e1) && is_quantifier(e2) &&
to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
expr_ref r1(e1,m), r2(e2,m);
instantiate(sub, r1);
instantiate(sub, r2);
p1 = m.mk_rewrite(r1, r2);
return m.mk_modus_ponens(push(p0, sub), p1);
}
}
premises.push_back(p);
substs.push_back(sub);
conclusion = m.get_fact(p);
instantiate(sub, conclusion);
return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
}
void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
for (unsigned i = 0; i < sub.size(); ++i) {
expr_ref e(m);
var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
sub[i] = e;
}
}
void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
if (sub.empty()) {
return;
}
if (!is_forall(fml)) {
return;
}
quantifier* q = to_quantifier(fml);
if (q->get_num_decls() != sub.size()) {
TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
tout << mk_pp(q, m) << "\n";
tout << sub.size() << "\n";);
return;
}
var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
}
};
void proof_utils::push_instantiations_up(proof_ref& pr) {
push_instantiations_up_cl push(pr.get_manager());
push(pr);
}

6
src/muz_qe/proof_utils.h
View file

@ -36,6 +36,12 @@ public:
*/
static void permute_unit_resolution(proof_ref& pr);
/**
\brief Push instantiations created in hyper-resolutions up to leaves.
This produces a "ground" proof where leaves are annotated by instantiations.
*/
static void push_instantiations_up(proof_ref& pr);
};
#endif

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);