mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
local changes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
commit
fb5d2cae17
|
@ -701,7 +701,7 @@ typedef enum
|
|||
over Boolean connectives 'and' and 'or'.
|
||||
|
||||
|
||||
- Z3_OP_PR_NFF_NEG: Proof for a (negative) NNF step. Examples:
|
||||
- Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples:
|
||||
\nicebox{
|
||||
T1: (not s_1) ~ r_1
|
||||
...
|
||||
|
|
165
src/ast/rewriter/ast_counter.cpp
Normal file
165
src/ast/rewriter/ast_counter.cpp
Normal file
|
@ -0,0 +1,165 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ast_counter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Routines for counting features of terms, such as free variables.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-03-18.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast_counter.h"
|
||||
#include "var_subst.h"
|
||||
|
||||
void counter::update(unsigned el, int delta) {
|
||||
int & counter = get(el);
|
||||
SASSERT(!m_stay_non_negative || counter>=0);
|
||||
SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
|
||||
counter += delta;
|
||||
}
|
||||
|
||||
int & counter::get(unsigned el) {
|
||||
return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
|
||||
}
|
||||
|
||||
counter & counter::count(unsigned sz, const unsigned * els, int delta) {
|
||||
for(unsigned i=0; i<sz; i++) {
|
||||
update(els[i], delta);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
unsigned counter::get_positive_count() const {
|
||||
unsigned cnt = 0;
|
||||
iterator eit = begin();
|
||||
iterator eend = end();
|
||||
for(; eit!=eend; ++eit) {
|
||||
if( eit->m_value>0 ) {
|
||||
cnt++;
|
||||
}
|
||||
}
|
||||
return cnt;
|
||||
}
|
||||
|
||||
void counter::collect_positive(uint_set & acc) const {
|
||||
iterator eit = begin();
|
||||
iterator eend = end();
|
||||
for(; eit!=eend; ++eit) {
|
||||
if(eit->m_value>0) { acc.insert(eit->m_key); }
|
||||
}
|
||||
}
|
||||
|
||||
bool counter::get_max_positive(unsigned & res) const {
|
||||
bool found = false;
|
||||
iterator eit = begin();
|
||||
iterator eend = end();
|
||||
for(; eit!=eend; ++eit) {
|
||||
if( eit->m_value>0 && (!found || eit->m_key>res) ) {
|
||||
found = true;
|
||||
res = eit->m_key;
|
||||
}
|
||||
}
|
||||
return found;
|
||||
}
|
||||
|
||||
unsigned counter::get_max_positive() const {
|
||||
unsigned max_pos;
|
||||
VERIFY(get_max_positive(max_pos));
|
||||
return max_pos;
|
||||
}
|
||||
|
||||
int counter::get_max_counter_value() const {
|
||||
int res = 0;
|
||||
iterator eit = begin();
|
||||
iterator eend = end();
|
||||
for (; eit!=eend; ++eit) {
|
||||
if( eit->m_value>res ) {
|
||||
res = eit->m_value;
|
||||
}
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
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);
|
||||
for (unsigned j = 0; j < m_sorts.size(); ++j) {
|
||||
if (m_sorts[j]) {
|
||||
update(j, coef);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
unsigned var_counter::get_max_var(bool& has_var) {
|
||||
has_var = false;
|
||||
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: {
|
||||
quantifier* q = to_quantifier(e);
|
||||
m_todo.push_back(q->get_expr());
|
||||
m_scopes.push_back(scope + q->get_num_decls());
|
||||
break;
|
||||
}
|
||||
case AST_VAR: {
|
||||
if (to_var(e)->get_idx() >= scope + max_var) {
|
||||
has_var = true;
|
||||
max_var = to_var(e)->get_idx() - scope;
|
||||
}
|
||||
break;
|
||||
}
|
||||
case AST_APP: {
|
||||
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;
|
||||
}
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
m_visited.reset();
|
||||
return max_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;
|
||||
}
|
||||
|
107
src/ast/rewriter/ast_counter.h
Normal file
107
src/ast/rewriter/ast_counter.h
Normal file
|
@ -0,0 +1,107 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
ast_counter.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Routines for counting features of terms, such as free variables.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-03-18.
|
||||
Krystof Hoder (t-khoder) 2010-10-10.
|
||||
|
||||
Revision History:
|
||||
|
||||
Hoisted from dl_util.h 2013-03-18.
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#ifndef _AST_COUNTER_H_
|
||||
#define _AST_COUNTER_H_
|
||||
|
||||
#include "ast.h"
|
||||
#include "map.h"
|
||||
#include "uint_set.h"
|
||||
|
||||
class counter {
|
||||
protected:
|
||||
typedef u_map<int> map_impl;
|
||||
map_impl m_data;
|
||||
const bool m_stay_non_negative;
|
||||
public:
|
||||
typedef map_impl::iterator iterator;
|
||||
|
||||
counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
|
||||
|
||||
iterator begin() const { return m_data.begin(); }
|
||||
iterator end() const { return m_data.end(); }
|
||||
void update(unsigned el, int delta);
|
||||
int & get(unsigned el);
|
||||
|
||||
/**
|
||||
\brief Increase values of elements in \c els by \c delta.
|
||||
|
||||
The function returns a reference to \c *this to allow for expressions like
|
||||
counter().count(sz, arr).get_positive_count()
|
||||
*/
|
||||
counter & count(unsigned sz, const unsigned * els, int delta = 1);
|
||||
counter & count(const unsigned_vector & els, int delta = 1) {
|
||||
return count(els.size(), els.c_ptr(), delta);
|
||||
}
|
||||
|
||||
void collect_positive(uint_set & acc) const;
|
||||
unsigned get_positive_count() const;
|
||||
|
||||
bool get_max_positive(unsigned & res) const;
|
||||
unsigned get_max_positive() const;
|
||||
|
||||
/**
|
||||
Since the default counter value of a counter is zero, the result is never negative.
|
||||
*/
|
||||
int get_max_counter_value() const;
|
||||
};
|
||||
|
||||
class var_counter : public counter {
|
||||
protected:
|
||||
ptr_vector<sort> m_sorts;
|
||||
expr_fast_mark1 m_visited;
|
||||
ptr_vector<expr> m_todo;
|
||||
unsigned_vector m_scopes;
|
||||
unsigned get_max_var(bool & has_var);
|
||||
public:
|
||||
var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
|
||||
void count_vars(ast_manager & m, const app * t, int coef = 1);
|
||||
unsigned get_max_var(expr* e);
|
||||
unsigned get_next_var(expr* e);
|
||||
};
|
||||
|
||||
class ast_counter {
|
||||
typedef obj_map<ast, int> map_impl;
|
||||
map_impl m_data;
|
||||
bool m_stay_non_negative;
|
||||
public:
|
||||
typedef map_impl::iterator iterator;
|
||||
|
||||
ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
|
||||
|
||||
iterator begin() const { return m_data.begin(); }
|
||||
iterator end() const { return m_data.end(); }
|
||||
|
||||
int & get(ast * el) {
|
||||
return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
|
||||
}
|
||||
void update(ast * el, int delta){
|
||||
get(el) += delta;
|
||||
SASSERT(!m_stay_non_negative || get(el) >= 0);
|
||||
}
|
||||
|
||||
void inc(ast * el) { update(el, 1); }
|
||||
void dec(ast * el) { update(el, -1); }
|
||||
};
|
||||
|
||||
#endif
|
|
@ -26,6 +26,7 @@ Revision History:
|
|||
#include "var_subst.h"
|
||||
#include "ast_pp.h"
|
||||
#include "ast_counter.h"
|
||||
#include "expr_safe_replace.h"
|
||||
|
||||
//
|
||||
// Bring quantifiers of common type into prenex form.
|
||||
|
@ -42,7 +43,7 @@ public:
|
|||
|
||||
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
|
||||
quantifier_type qt = Q_none_pos;
|
||||
pull_quantifiers(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
|
@ -52,7 +53,7 @@ public:
|
|||
|
||||
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
|
||||
quantifier_type qt = Q_exists_pos;
|
||||
pull_quantifiers(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
|
@ -61,7 +62,7 @@ public:
|
|||
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
|
||||
quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
|
||||
expr_ref result(m);
|
||||
pull_quantifiers(fml, qt, vars, result);
|
||||
pull_quantifier(fml, qt, vars, result);
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(fml, m) << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
|
@ -78,7 +79,57 @@ public:
|
|||
expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
|
||||
instantiate(m, q, exprs, result);
|
||||
}
|
||||
|
||||
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
|
||||
unsigned index = var_counter().get_next_var(fml);
|
||||
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
|
||||
quantifier* q = to_quantifier(fml);
|
||||
index += q->get_num_decls();
|
||||
if (names) {
|
||||
names->append(q->get_num_decls(), q->get_decl_names());
|
||||
}
|
||||
if (sorts) {
|
||||
sorts->append(q->get_num_decls(), q->get_decl_sorts());
|
||||
}
|
||||
fml = q->get_expr();
|
||||
}
|
||||
if (!has_quantifiers(fml)) {
|
||||
return index;
|
||||
}
|
||||
app_ref_vector vars(m);
|
||||
pull_quantifier(is_forall, fml, vars);
|
||||
if (vars.empty()) {
|
||||
return index;
|
||||
}
|
||||
// replace vars by de-bruijn indices
|
||||
expr_safe_replace rep(m);
|
||||
svector<symbol> bound_names;
|
||||
ptr_vector<sort> bound_sorts;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
app* v = vars[i].get();
|
||||
if (names) {
|
||||
bound_names.push_back(v->get_decl()->get_name());
|
||||
}
|
||||
if (sorts) {
|
||||
bound_sorts.push_back(m.get_sort(v));
|
||||
}
|
||||
rep.insert(v, m.mk_var(index++, m.get_sort(v)));
|
||||
}
|
||||
if (names && !bound_names.empty()) {
|
||||
bound_names.reverse();
|
||||
bound_names.append(*names);
|
||||
names->reset();
|
||||
names->append(bound_names);
|
||||
}
|
||||
if (sorts && !bound_sorts.empty()) {
|
||||
bound_sorts.reverse();
|
||||
bound_sorts.append(*sorts);
|
||||
sorts->reset();
|
||||
sorts->append(bound_sorts);
|
||||
}
|
||||
rep(fml);
|
||||
return index;
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
|
@ -143,7 +194,7 @@ private:
|
|||
}
|
||||
|
||||
|
||||
void pull_quantifiers(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
|
||||
void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
|
||||
|
||||
if (!has_quantifiers(fml)) {
|
||||
result = fml;
|
||||
|
@ -159,7 +210,7 @@ private:
|
|||
if (m.is_and(fml)) {
|
||||
num_args = a->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
pull_quantifiers(a->get_arg(i), qt, vars, tmp);
|
||||
pull_quantifier(a->get_arg(i), qt, vars, tmp);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
m_rewriter.mk_and(args.size(), args.c_ptr(), result);
|
||||
|
@ -167,25 +218,25 @@ private:
|
|||
else if (m.is_or(fml)) {
|
||||
num_args = to_app(fml)->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
pull_quantifiers(to_app(fml)->get_arg(i), qt, vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
m_rewriter.mk_or(args.size(), args.c_ptr(), result);
|
||||
}
|
||||
else if (m.is_not(fml)) {
|
||||
pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
|
||||
negate(qt);
|
||||
result = m.mk_not(tmp);
|
||||
}
|
||||
else if (m.is_implies(fml)) {
|
||||
pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
|
||||
negate(qt);
|
||||
pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, result);
|
||||
pull_quantifier(to_app(fml)->get_arg(1), qt, vars, result);
|
||||
result = m.mk_implies(tmp, result);
|
||||
}
|
||||
else if (m.is_ite(fml)) {
|
||||
pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, tmp);
|
||||
pull_quantifiers(to_app(fml)->get_arg(2), qt, vars, result);
|
||||
pull_quantifier(to_app(fml)->get_arg(1), qt, vars, tmp);
|
||||
pull_quantifier(to_app(fml)->get_arg(2), qt, vars, result);
|
||||
result = m.mk_ite(to_app(fml)->get_arg(0), tmp, result);
|
||||
}
|
||||
else {
|
||||
|
@ -203,7 +254,7 @@ private:
|
|||
}
|
||||
set_quantifier_type(qt, q->is_forall());
|
||||
extract_quantifier(q, vars, tmp);
|
||||
pull_quantifiers(tmp, qt, vars, result);
|
||||
pull_quantifier(tmp, qt, vars, result);
|
||||
break;
|
||||
}
|
||||
case AST_VAR:
|
||||
|
@ -216,36 +267,6 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
|
||||
unsigned index = var_counter().get_next_var(fml);
|
||||
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
|
||||
quantifier* q = to_quantifier(fml);
|
||||
index += q->get_num_decls();
|
||||
if (names) {
|
||||
names->append(q->get_num_decls(), q->get_decl_names());
|
||||
}
|
||||
fml = q->get_expr();
|
||||
}
|
||||
if (!has_quantifiers(fml)) {
|
||||
return index;
|
||||
}
|
||||
app_ref_vector vars(m);
|
||||
pull_quantifier(is_forall, fml, vars);
|
||||
if (vars.empty()) {
|
||||
return index;
|
||||
}
|
||||
// replace vars by de-bruijn indices
|
||||
expr_safe_replace rep(m);
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
app* v = vars[i].get();
|
||||
if (names) {
|
||||
names->push_back(v->get_decl()->get_name());
|
||||
}
|
||||
rep.insert(v, m.mk_var(index++,m.get_sort(v)));
|
||||
}
|
||||
rep(fml);
|
||||
return index;
|
||||
}
|
||||
};
|
||||
|
||||
quantifier_hoister::quantifier_hoister(ast_manager& m) {
|
||||
|
@ -268,7 +289,6 @@ void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_
|
|||
m_impl->pull_quantifier(is_forall, fml, vars);
|
||||
}
|
||||
|
||||
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
|
||||
return m_impl->pull_quantifier(is_forall, fml, names);
|
||||
unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names) {
|
||||
return m_impl->pull_quantifier(is_forall, fml, sorts, names);
|
||||
}
|
||||
|
||||
|
|
|
@ -67,6 +67,7 @@ public:
|
|||
*/
|
||||
|
||||
unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -233,7 +233,7 @@ namespace datalog {
|
|||
table_fact row;
|
||||
for(; it!=iend; ++it) {
|
||||
it->get_fact(row);
|
||||
to_remove.append(row);
|
||||
to_remove.push_back(row);
|
||||
}
|
||||
remove_facts(to_remove.size(), to_remove.c_ptr());
|
||||
}
|
||||
|
|
|
@ -307,7 +307,7 @@ namespace datalog {
|
|||
r1->to_formula(concl);
|
||||
scoped_proof _sp(m);
|
||||
|
||||
proof* p = m.mk_asserted(fml);
|
||||
proof* p = r->get_proof();
|
||||
proof* premises[2] = { pr, p };
|
||||
|
||||
positions.push_back(std::make_pair(0, 1));
|
||||
|
@ -320,7 +320,7 @@ namespace datalog {
|
|||
else {
|
||||
r2->to_formula(concl);
|
||||
scoped_proof _sp(m);
|
||||
proof* p = m.mk_asserted(fml);
|
||||
proof* p = r->get_proof();
|
||||
if (sub.empty()) {
|
||||
pr = p;
|
||||
}
|
||||
|
@ -340,7 +340,7 @@ namespace datalog {
|
|||
pred = r->get_decl(0);
|
||||
}
|
||||
scoped_proof _sp(m);
|
||||
apply(m, b.m_pc.get(), pr);
|
||||
apply(m, b.m_ctx.get_proof_converter().get(), pr);
|
||||
b.m_answer = pr;
|
||||
return l_true;
|
||||
}
|
||||
|
@ -474,6 +474,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
proof_ref get_proof(model_ref& md, func_decl* pred, app* prop, unsigned level) {
|
||||
if (b.m_cancel) {
|
||||
return proof_ref(0, m);
|
||||
}
|
||||
TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
|
||||
|
||||
expr_ref prop_r(m), prop_v(m), fml(m), prop_body(m), tmp(m), body(m);
|
||||
|
@ -497,7 +500,7 @@ namespace datalog {
|
|||
SASSERT(r);
|
||||
r->to_formula(fml);
|
||||
IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";);
|
||||
prs.push_back(m.mk_asserted(fml));
|
||||
prs.push_back(r->get_proof());
|
||||
unsigned sz = r->get_uninterpreted_tail_size();
|
||||
|
||||
ptr_vector<sort> rule_vars;
|
||||
|
@ -536,8 +539,9 @@ namespace datalog {
|
|||
model_ref md;
|
||||
b.m_solver.get_model(md);
|
||||
IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
|
||||
proof_ref pr = get_proof(md, b.m_query_pred, to_app(level_query), level);
|
||||
apply(m, b.m_pc.get(), pr);
|
||||
proof_ref pr(m);
|
||||
pr = get_proof(md, b.m_query_pred, to_app(level_query), level);
|
||||
apply(m, b.m_ctx.get_proof_converter().get(), pr);
|
||||
b.m_answer = pr;
|
||||
}
|
||||
|
||||
|
@ -1034,7 +1038,7 @@ namespace datalog {
|
|||
var_subst vs(m, false);
|
||||
mk_subst(*rules[i], path, trace, sub);
|
||||
rules[i]->to_formula(fml);
|
||||
prs.push_back(m.mk_asserted(fml));
|
||||
prs.push_back(rules[i]->get_proof());
|
||||
unsigned sz = trace->get_num_args();
|
||||
if (sub.empty() && sz == 0) {
|
||||
pr = prs[0].get();
|
||||
|
@ -1112,7 +1116,6 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) {
|
||||
proof_ref pr(m);
|
||||
IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0););
|
||||
md->eval(trace, trace);
|
||||
md->eval(path, path);
|
||||
|
@ -1120,7 +1123,11 @@ namespace datalog {
|
|||
for (unsigned i = 0; i < b.m_solver.size(); ++i) {
|
||||
verbose_stream() << mk_pp(b.m_solver.get_formulas()[i], m) << "\n";
|
||||
});
|
||||
b.m_answer = get_proof(md, to_app(trace), to_app(path));
|
||||
scoped_proof _sp(m);
|
||||
proof_ref pr(m);
|
||||
pr = get_proof(md, to_app(trace), to_app(path));
|
||||
apply(m, b.m_ctx.get_proof_converter().get(), pr);
|
||||
b.m_answer = pr;
|
||||
}
|
||||
|
||||
};
|
||||
|
@ -1155,6 +1162,9 @@ namespace datalog {
|
|||
private:
|
||||
|
||||
void get_model(unsigned level) {
|
||||
if (b.m_cancel) {
|
||||
return;
|
||||
}
|
||||
rule_manager& rm = b.m_ctx.get_rule_manager();
|
||||
expr_ref level_query = mk_level_predicate(b.m_query_pred, level);
|
||||
model_ref md;
|
||||
|
@ -1212,7 +1222,7 @@ namespace datalog {
|
|||
r1->to_formula(concl);
|
||||
scoped_proof _sp(m);
|
||||
|
||||
proof* p = m.mk_asserted(fml);
|
||||
proof* p = r->get_proof();
|
||||
proof* premises[2] = { pr, p };
|
||||
|
||||
positions.push_back(std::make_pair(0, 1));
|
||||
|
@ -1225,7 +1235,7 @@ namespace datalog {
|
|||
else {
|
||||
r2->to_formula(concl);
|
||||
scoped_proof _sp(m);
|
||||
proof* p = m.mk_asserted(fml);
|
||||
proof* p = r->get_proof();
|
||||
if (sub.empty()) {
|
||||
pr = p;
|
||||
}
|
||||
|
@ -1245,7 +1255,7 @@ namespace datalog {
|
|||
pred = r->get_decl(0);
|
||||
}
|
||||
scoped_proof _sp(m);
|
||||
apply(m, b.m_pc.get(), pr);
|
||||
apply(m, b.m_ctx.get_proof_converter().get(), pr);
|
||||
b.m_answer = pr;
|
||||
}
|
||||
|
||||
|
@ -1409,18 +1419,15 @@ namespace datalog {
|
|||
|
||||
m_ctx.ensure_opened();
|
||||
m_rules.reset();
|
||||
|
||||
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
|
||||
datalog::rule_set old_rules(m_ctx.get_rules());
|
||||
datalog::rule_ref_vector query_rules(rule_manager);
|
||||
datalog::rule_ref query_rule(rule_manager);
|
||||
model_converter_ref mc = datalog::mk_skip_model_converter();
|
||||
m_pc = datalog::mk_skip_proof_converter();
|
||||
m_ctx.set_model_converter(mc);
|
||||
m_ctx.set_proof_converter(m_pc);
|
||||
rule_manager.mk_query(query, m_query_pred, query_rules, query_rule);
|
||||
m_ctx.add_rules(query_rules);
|
||||
expr_ref bg_assertion = m_ctx.get_background_assertion();
|
||||
|
||||
expr_ref bg_assertion = m_ctx.get_background_assertion();
|
||||
|
||||
m_ctx.set_output_predicate(m_query_pred);
|
||||
m_ctx.apply_default_transformation();
|
||||
|
||||
|
|
|
@ -39,7 +39,6 @@ namespace datalog {
|
|||
func_decl_ref m_query_pred;
|
||||
expr_ref m_answer;
|
||||
volatile bool m_cancel;
|
||||
proof_converter_ref m_pc;
|
||||
|
||||
void checkpoint();
|
||||
|
||||
|
|
|
@ -287,9 +287,6 @@ namespace datalog {
|
|||
|
||||
bool check_table::well_formed() const {
|
||||
get_plugin().m_count++;
|
||||
if (get_plugin().m_count == 497) {
|
||||
std::cout << "here\n";
|
||||
}
|
||||
iterator it = m_tocheck->begin(), end = m_tocheck->end();
|
||||
for (; it != end; ++it) {
|
||||
table_fact fact;
|
||||
|
@ -354,8 +351,8 @@ namespace datalog {
|
|||
return result;
|
||||
}
|
||||
|
||||
table_base * check_table::complement(func_decl* p) const {
|
||||
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p), m_checker->complement(p));
|
||||
table_base * check_table::complement(func_decl* p, const table_element * func_columns) const {
|
||||
check_table* result = alloc(check_table, get_plugin(), get_signature(), m_tocheck->complement(p, func_columns), m_checker->complement(p, func_columns));
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
@ -119,7 +119,7 @@ namespace datalog {
|
|||
virtual void add_fact(const table_fact & f);
|
||||
virtual void remove_fact(const table_element* fact);
|
||||
virtual bool contains_fact(const table_fact & f) const;
|
||||
virtual table_base * complement(func_decl* p) const;
|
||||
virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const;
|
||||
virtual table_base * clone() const;
|
||||
|
||||
virtual iterator begin() const { SASSERT(well_formed()); return m_tocheck->begin(); }
|
||||
|
|
|
@ -262,8 +262,10 @@ public:
|
|||
|
||||
case datalog::OK:
|
||||
break;
|
||||
|
||||
default:
|
||||
UNREACHABLE();
|
||||
// exception was raised.
|
||||
break;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -384,8 +384,8 @@ namespace datalog {
|
|||
void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
|
||||
SASSERT(r->get_positive_tail_size()==2);
|
||||
ast_manager & m = m_context.get_manager();
|
||||
var_counter counter;
|
||||
counter.count_vars(m, r);
|
||||
rule_counter counter;
|
||||
counter.count_rule_vars(m, r);
|
||||
app * t1 = r->get_tail(0);
|
||||
app * t2 = r->get_tail(1);
|
||||
counter.count_vars(m, t1, -1);
|
||||
|
|
|
@ -231,6 +231,7 @@ namespace datalog {
|
|||
m_rule_set(*this),
|
||||
m_rule_fmls(m),
|
||||
m_background(m),
|
||||
m_mc(0),
|
||||
m_closed(false),
|
||||
m_saturation_was_run(false),
|
||||
m_last_answer(m),
|
||||
|
@ -474,10 +475,11 @@ namespace datalog {
|
|||
void context::flush_add_rules() {
|
||||
datalog::rule_manager& rm = get_rule_manager();
|
||||
datalog::rule_ref_vector rules(rm);
|
||||
rm.set_model_converter(m_mc);
|
||||
rm.set_proof_converter(m_pc);
|
||||
scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
|
||||
rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
|
||||
expr* fml = m_rule_fmls[i].get();
|
||||
proof* p = generate_proof_trace()?m.mk_asserted(fml):0;
|
||||
rm.mk_rule(fml, p, rules, m_rule_names[i]);
|
||||
}
|
||||
add_rules(rules);
|
||||
m_rule_fmls.reset();
|
||||
|
@ -491,7 +493,11 @@ namespace datalog {
|
|||
void context::update_rule(expr* rl, symbol const& name) {
|
||||
datalog::rule_manager& rm = get_rule_manager();
|
||||
datalog::rule_ref_vector rules(rm);
|
||||
rm.mk_rule(rl, rules, name);
|
||||
proof* p = 0;
|
||||
if (generate_proof_trace()) {
|
||||
p = m.mk_asserted(rl);
|
||||
}
|
||||
rm.mk_rule(rl, p, rules, name);
|
||||
if (rules.size() != 1) {
|
||||
std::stringstream strm;
|
||||
strm << "Rule " << name << " has a non-trivial body. It cannot be modified";
|
||||
|
@ -685,7 +691,7 @@ namespace datalog {
|
|||
todo.push_back(e2);
|
||||
}
|
||||
else if (is_quantifier(e)) {
|
||||
todo.append(to_quantifier(e)->get_expr());
|
||||
todo.push_back(to_quantifier(e)->get_expr());
|
||||
}
|
||||
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
|
||||
m.is_true(e1)) {
|
||||
|
@ -739,6 +745,9 @@ namespace datalog {
|
|||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
if (generate_proof_trace() && !r->get_proof()) {
|
||||
m_rule_manager.mk_rule_asserted_proof(*r.get());
|
||||
}
|
||||
}
|
||||
|
||||
void context::add_rule(rule_ref& r) {
|
||||
|
@ -849,7 +858,7 @@ namespace datalog {
|
|||
void context::transform_rules(rule_transformer& transf) {
|
||||
SASSERT(m_closed); //we must finish adding rules before we start transforming them
|
||||
TRACE("dl", display_rules(tout););
|
||||
if (transf(m_rule_set, m_mc, m_pc)) {
|
||||
if (transf(m_rule_set, m_mc)) {
|
||||
//we have already ensured the negation is stratified and transformations
|
||||
//should not break the stratification
|
||||
m_rule_set.ensure_closed();
|
||||
|
@ -1037,6 +1046,8 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void context::new_query() {
|
||||
m_mc = mk_skip_model_converter();
|
||||
|
||||
flush_add_rules();
|
||||
m_last_status = OK;
|
||||
m_last_answer = 0;
|
||||
|
@ -1148,6 +1159,7 @@ namespace datalog {
|
|||
switch(get_engine()) {
|
||||
case DATALOG_ENGINE:
|
||||
return false;
|
||||
case PDR_ENGINE:
|
||||
case QPDR_ENGINE:
|
||||
ensure_pdr();
|
||||
m_pdr->display_certificate(out);
|
||||
|
@ -1241,7 +1253,7 @@ namespace datalog {
|
|||
ptr_vector<sort> sorts;
|
||||
get_free_vars(m_rule_fmls[i].get(), sorts);
|
||||
if (!sorts.empty()) {
|
||||
rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]);
|
||||
rm.mk_rule(m_rule_fmls[i].get(), 0, rule_refs, m_rule_names[i]);
|
||||
m_rule_fmls[i] = m_rule_fmls.back();
|
||||
m_rule_names[i] = m_rule_names.back();
|
||||
m_rule_fmls.pop_back();
|
||||
|
@ -1258,7 +1270,7 @@ namespace datalog {
|
|||
}
|
||||
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
|
||||
rules.push_back(m_rule_fmls[i].get());
|
||||
names.push_back(m_rule_names[i]);
|
||||
names.push_back(m_rule_names[i]);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -42,7 +42,6 @@ Revision History:
|
|||
#include"params.h"
|
||||
#include"trail.h"
|
||||
#include"model_converter.h"
|
||||
#include"proof_converter.h"
|
||||
#include"model2expr.h"
|
||||
#include"smt_params.h"
|
||||
#include"dl_rule_transformer.h"
|
||||
|
@ -85,9 +84,6 @@ namespace datalog {
|
|||
var_subst m_var_subst;
|
||||
rule_manager m_rule_manager;
|
||||
rule_transformer m_transf;
|
||||
model_converter_ref m_mc;
|
||||
proof_converter_ref m_pc;
|
||||
|
||||
trail_stack<context> m_trail;
|
||||
ast_ref_vector m_pinned;
|
||||
app_ref_vector m_vars;
|
||||
|
@ -99,6 +95,8 @@ namespace datalog {
|
|||
expr_ref_vector m_rule_fmls;
|
||||
svector<symbol> m_rule_names;
|
||||
expr_ref_vector m_background;
|
||||
model_converter_ref m_mc;
|
||||
proof_converter_ref m_pc;
|
||||
|
||||
scoped_ptr<pdr::dl_interface> m_pdr;
|
||||
scoped_ptr<bmc> m_bmc;
|
||||
|
@ -144,6 +142,7 @@ namespace datalog {
|
|||
var_subst & get_var_subst() { return m_var_subst; }
|
||||
dl_decl_util & get_decl_util() { return m_decl_util; }
|
||||
|
||||
bool generate_proof_trace() const { return m_params.generate_proof_trace(); }
|
||||
bool output_profile() const { return m_params.output_profile(); }
|
||||
bool fix_unbound_vars() const { return m_params.fix_unbound_vars(); }
|
||||
symbol default_table() const { return m_params.default_table(); }
|
||||
|
@ -317,15 +316,15 @@ namespace datalog {
|
|||
void reopen();
|
||||
void ensure_opened();
|
||||
|
||||
void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
|
||||
void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
|
||||
model_converter_ref& get_model_converter() { return m_mc; }
|
||||
proof_converter_ref& get_proof_converter() { return m_pc; }
|
||||
void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); }
|
||||
|
||||
void transform_rules();
|
||||
void transform_rules(rule_transformer::plugin* plugin);
|
||||
void transform_rules(rule_transformer& transf);
|
||||
void transform_rules();
|
||||
void transform_rules(rule_transformer& transf);
|
||||
void replace_rules(rule_set & rs);
|
||||
|
||||
void apply_default_transformation();
|
||||
void apply_default_transformation();
|
||||
|
||||
void collect_params(param_descrs& r);
|
||||
|
||||
|
|
|
@ -197,25 +197,18 @@ namespace datalog {
|
|||
}
|
||||
|
||||
fml2 = m.mk_implies(body, head);
|
||||
rm.mk_rule(fml2, new_rules, r.name());
|
||||
proof_ref p(m);
|
||||
rm.mk_rule(fml2, p, new_rules, r.name());
|
||||
SASSERT(new_rules.size() == 1);
|
||||
|
||||
TRACE("dl", new_rules[0]->display(m_ctx, tout << "new rule\n"););
|
||||
|
||||
rules.add_rule(new_rules[0].get());
|
||||
if (m_pc) {
|
||||
new_rules[0]->to_formula(fml2);
|
||||
m_pc->insert(fml1, fml2);
|
||||
}
|
||||
rm.mk_rule_rewrite_proof(r, *new_rules[0].get());
|
||||
return true;
|
||||
}
|
||||
|
||||
rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
ref<equiv_proof_converter> epc;
|
||||
if (pc) {
|
||||
epc = alloc(equiv_proof_converter, m);
|
||||
}
|
||||
m_pc = epc.get();
|
||||
rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
|
@ -227,9 +220,6 @@ namespace datalog {
|
|||
dealloc(rules);
|
||||
rules = 0;
|
||||
}
|
||||
if (pc) {
|
||||
pc = concat(pc.get(), epc.get());
|
||||
}
|
||||
return rules;
|
||||
}
|
||||
|
||||
|
|
|
@ -37,7 +37,6 @@ namespace datalog {
|
|||
rule_manager& rm;
|
||||
params_ref m_params;
|
||||
th_rewriter m_rewriter;
|
||||
equiv_proof_converter* m_pc;
|
||||
|
||||
typedef obj_map<app, var*> defs_t;
|
||||
|
||||
|
@ -55,7 +54,7 @@ namespace datalog {
|
|||
|
||||
virtual ~mk_array_blast();
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -21,7 +21,8 @@ Revision History:
|
|||
#include "bit_blaster_rewriter.h"
|
||||
#include "rewriter_def.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
#include "expr_safe_replace.h"
|
||||
#include "filter_model_converter.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -35,6 +36,73 @@ namespace datalog {
|
|||
// P(bv(x,y)) :- P_bv(x,y)
|
||||
// Query
|
||||
|
||||
// this model converter should be composed with a filter converter
|
||||
// that gets rid of the new functions.
|
||||
class bit_blast_model_converter : public model_converter {
|
||||
ast_manager& m;
|
||||
bv_util m_bv;
|
||||
func_decl_ref_vector m_old_funcs;
|
||||
func_decl_ref_vector m_new_funcs;
|
||||
public:
|
||||
bit_blast_model_converter(ast_manager& m):
|
||||
m(m),
|
||||
m_bv(m),
|
||||
m_old_funcs(m),
|
||||
m_new_funcs(m) {}
|
||||
|
||||
void insert(func_decl* old_f, func_decl* new_f) {
|
||||
m_old_funcs.push_back(old_f);
|
||||
m_new_funcs.push_back(new_f);
|
||||
}
|
||||
|
||||
virtual model_converter * translate(ast_translation & translator) {
|
||||
return alloc(bit_blast_model_converter, m);
|
||||
}
|
||||
|
||||
virtual void operator()(model_ref & model) {
|
||||
for (unsigned i = 0; i < m_new_funcs.size(); ++i) {
|
||||
func_decl* p = m_new_funcs[i].get();
|
||||
func_decl* q = m_old_funcs[i].get();
|
||||
func_interp* f = model->get_func_interp(p);
|
||||
expr_ref body(m);
|
||||
unsigned arity_p = p->get_arity();
|
||||
unsigned arity_q = q->get_arity();
|
||||
SASSERT(0 < arity_p);
|
||||
model->register_decl(p, f);
|
||||
func_interp* g = alloc(func_interp, m, arity_q);
|
||||
|
||||
if (f) {
|
||||
body = f->get_interp();
|
||||
SASSERT(!f->is_partial());
|
||||
SASSERT(body);
|
||||
}
|
||||
else {
|
||||
body = m.mk_false();
|
||||
}
|
||||
unsigned idx = 0;
|
||||
expr_ref arg(m), proj(m);
|
||||
expr_safe_replace sub(m);
|
||||
for (unsigned j = 0; j < arity_q; ++j) {
|
||||
sort* s = q->get_domain(j);
|
||||
arg = m.mk_var(j, s);
|
||||
if (m_bv.is_bv_sort(s)) {
|
||||
expr* args[1] = { arg };
|
||||
unsigned sz = m_bv.get_bv_size(s);
|
||||
for (unsigned k = 0; k < sz; ++k) {
|
||||
proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
|
||||
sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj);
|
||||
}
|
||||
}
|
||||
else {
|
||||
sub.insert(m.mk_var(idx++, s), arg);
|
||||
}
|
||||
}
|
||||
sub(body);
|
||||
g->set_else(body);
|
||||
model->register_decl(q, g);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
class expand_mkbv_cfg : public default_rewriter_cfg {
|
||||
|
||||
|
@ -43,7 +111,8 @@ namespace datalog {
|
|||
ast_manager& m;
|
||||
bv_util m_util;
|
||||
expr_ref_vector m_args, m_f_vars, m_g_vars;
|
||||
func_decl_ref_vector m_pinned;
|
||||
func_decl_ref_vector m_old_funcs;
|
||||
func_decl_ref_vector m_new_funcs;
|
||||
obj_map<func_decl,func_decl*> m_pred2blast;
|
||||
|
||||
|
||||
|
@ -57,10 +126,14 @@ namespace datalog {
|
|||
m_args(m),
|
||||
m_f_vars(m),
|
||||
m_g_vars(m),
|
||||
m_pinned(m)
|
||||
m_old_funcs(m),
|
||||
m_new_funcs(m)
|
||||
{}
|
||||
|
||||
~expand_mkbv_cfg() {}
|
||||
|
||||
func_decl_ref_vector const& old_funcs() const { return m_old_funcs; }
|
||||
func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
rule_manager& rm = m_context.get_rule_manager();
|
||||
|
@ -105,13 +178,18 @@ namespace datalog {
|
|||
domain.push_back(m.get_sort(m_args[i].get()));
|
||||
}
|
||||
g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f);
|
||||
m_pinned.push_back(g);
|
||||
m_old_funcs.push_back(f);
|
||||
m_new_funcs.push_back(g);
|
||||
m_pred2blast.insert(f, g);
|
||||
|
||||
// Create rule f(mk_mkbv(args)) :- g(args)
|
||||
|
||||
fml = m.mk_implies(m.mk_app(g, m_g_vars.size(), m_g_vars.c_ptr()), m.mk_app(f, m_f_vars.size(), m_f_vars.c_ptr()));
|
||||
rm.mk_rule(fml, m_rules, g->get_name());
|
||||
proof_ref pr(m);
|
||||
if (m_context.generate_proof_trace()) {
|
||||
pr = m.mk_asserted(fml); // or a def?
|
||||
}
|
||||
rm.mk_rule(fml, pr, m_rules, g->get_name());
|
||||
}
|
||||
result = m.mk_app(g, m_args.size(), m_args.c_ptr());
|
||||
result_pr = 0;
|
||||
|
@ -170,14 +248,11 @@ namespace datalog {
|
|||
m_blaster.updt_params(m_params);
|
||||
}
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO pc
|
||||
if (!m_context.get_params().bit_blast()) {
|
||||
return 0;
|
||||
}
|
||||
if (m_context.get_engine() != PDR_ENGINE) {
|
||||
return 0;
|
||||
}
|
||||
rule_manager& rm = m_context.get_rule_manager();
|
||||
unsigned sz = source.get_num_rules();
|
||||
expr_ref fml(m);
|
||||
|
@ -185,9 +260,13 @@ namespace datalog {
|
|||
rule_set * result = alloc(rule_set, m_context);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
rule * r = source.get_rule(i);
|
||||
r->to_formula(fml);
|
||||
r->to_formula(fml);
|
||||
if (blast(fml)) {
|
||||
rm.mk_rule(fml, m_rules, r->name());
|
||||
proof_ref pr(m);
|
||||
if (m_context.generate_proof_trace()) {
|
||||
pr = m.mk_asserted(fml); // loses original proof of r.
|
||||
}
|
||||
rm.mk_rule(fml, pr, m_rules, r->name());
|
||||
}
|
||||
else {
|
||||
m_rules.push_back(r);
|
||||
|
@ -197,6 +276,18 @@ namespace datalog {
|
|||
for (unsigned i = 0; i < m_rules.size(); ++i) {
|
||||
result->add_rule(m_rules.get(i));
|
||||
}
|
||||
|
||||
if (mc) {
|
||||
filter_model_converter* fmc = alloc(filter_model_converter, m);
|
||||
bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m);
|
||||
func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs();
|
||||
func_decl_ref_vector const& new_funcs = m_rewriter.m_cfg.new_funcs();
|
||||
for (unsigned i = 0; i < old_funcs.size(); ++i) {
|
||||
fmc->insert(new_funcs[i]);
|
||||
bvmc->insert(old_funcs[i], new_funcs[i]);
|
||||
}
|
||||
mc = concat(mc.get(), concat(bvmc, fmc));
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
@ -210,8 +301,8 @@ namespace datalog {
|
|||
dealloc(m_impl);
|
||||
}
|
||||
|
||||
rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
return (*m_impl)(source, mc, pc);
|
||||
rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
return (*m_impl)(source, mc);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -44,7 +44,7 @@ namespace datalog {
|
|||
mk_bit_blast(context & ctx, unsigned priority = 35000);
|
||||
~mk_bit_blast();
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -133,7 +133,7 @@ namespace datalog {
|
|||
tail.push_back(to_app(fml));
|
||||
is_neg.push_back(false);
|
||||
res = rm.mk(head, tail.size(), tail.c_ptr(), is_neg.c_ptr(), tgt->name());
|
||||
if (m_pc) {
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
src.to_formula(fml1);
|
||||
tgt->to_formula(fml2);
|
||||
res->to_formula(fml);
|
||||
|
@ -142,12 +142,13 @@ namespace datalog {
|
|||
sort* domain[3] = { ps, ps, m.mk_bool_sort() };
|
||||
func_decl* merge = m.mk_func_decl(symbol("merge-clauses"), 3, domain, ps); // TBD: ad-hoc proof rule
|
||||
expr* args[3] = { m.mk_asserted(fml1), m.mk_asserted(fml2), fml };
|
||||
m_pc->insert(m.mk_app(merge, 3, args));
|
||||
// ...m_pc->insert(m.mk_app(merge, 3, args));
|
||||
#else
|
||||
svector<std::pair<unsigned, unsigned> > pos;
|
||||
vector<expr_ref_vector> substs;
|
||||
proof* p = m.mk_asserted(fml1);
|
||||
m_pc->insert(m.mk_hyper_resolve(1, &p, fml, pos, substs));
|
||||
proof* p = src.get_proof();
|
||||
p = m.mk_hyper_resolve(1, &p, fml, pos, substs);
|
||||
res->set_proof(m, p);
|
||||
#endif
|
||||
}
|
||||
tgt = res;
|
||||
|
@ -170,13 +171,7 @@ namespace datalog {
|
|||
return true;
|
||||
}
|
||||
|
||||
rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
m_pc = 0;
|
||||
ref<replace_proof_converter> rpc;
|
||||
if (pc) {
|
||||
rpc = alloc(replace_proof_converter, m);
|
||||
m_pc = rpc.get();
|
||||
}
|
||||
rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
|
||||
for (; it != end; ++it) {
|
||||
|
@ -195,9 +190,6 @@ namespace datalog {
|
|||
rules->add_rule(r1.get());
|
||||
}
|
||||
}
|
||||
if (pc) {
|
||||
pc = concat(pc.get(), rpc.get());
|
||||
}
|
||||
return rules;
|
||||
}
|
||||
|
||||
|
|
|
@ -37,7 +37,6 @@ namespace datalog {
|
|||
rule_manager& rm;
|
||||
expr_ref_vector m_sub1, m_sub2;
|
||||
unsigned m_idx;
|
||||
replace_proof_converter* m_pc;
|
||||
|
||||
void mk_pred(app_ref& pred, app* p1, app* p2);
|
||||
|
||||
|
@ -53,7 +52,7 @@ namespace datalog {
|
|||
*/
|
||||
mk_coalesce(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -35,8 +35,7 @@ namespace datalog {
|
|||
|
||||
rule_set * mk_coi_filter::operator()(
|
||||
rule_set const & source,
|
||||
model_converter_ref& mc,
|
||||
proof_converter_ref& pc)
|
||||
model_converter_ref& mc)
|
||||
{
|
||||
if (source.get_num_rules()==0) {
|
||||
return 0;
|
||||
|
|
|
@ -40,8 +40,7 @@ namespace datalog {
|
|||
|
||||
|
||||
rule_set * operator()(rule_set const & source,
|
||||
model_converter_ref& mc,
|
||||
proof_converter_ref& pc);
|
||||
model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -708,8 +708,8 @@ namespace datalog {
|
|||
}
|
||||
|
||||
rule * mk_explanations::get_e_rule(rule * r) {
|
||||
var_counter ctr;
|
||||
ctr.count_vars(m_manager, r);
|
||||
rule_counter ctr;
|
||||
ctr.count_rule_vars(m_manager, r);
|
||||
unsigned max_var;
|
||||
unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
|
||||
unsigned head_var = next_var++;
|
||||
|
@ -875,8 +875,8 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
SASSERT(!mc && !pc);
|
||||
rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
SASSERT(!mc);
|
||||
if(source.get_num_rules()==0) {
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -82,7 +82,7 @@ namespace datalog {
|
|||
return get_union_decl(m_context);
|
||||
}
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
static expr* get_explanation(relation_base const& r);
|
||||
};
|
||||
|
|
|
@ -168,7 +168,15 @@ namespace datalog {
|
|||
fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head());
|
||||
TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";);
|
||||
rule_ref_vector rules(rm);
|
||||
rm.mk_rule(fml, rules, r.name());
|
||||
proof_ref pr(m);
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
scoped_proof _scp(m);
|
||||
expr_ref fml1(m);
|
||||
r.to_formula(fml1);
|
||||
pr = m.mk_rewrite(fml1, fml);
|
||||
pr = m.mk_modus_ponens(r.get_proof(), pr);
|
||||
}
|
||||
rm.mk_rule(fml, pr, rules, r.name());
|
||||
for (unsigned i = 0; i < rules.size(); ++i) {
|
||||
new_rules.add_rule(rules[i].get());
|
||||
m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs));
|
||||
|
@ -347,7 +355,7 @@ namespace datalog {
|
|||
m_quantifiers.reset();
|
||||
}
|
||||
|
||||
rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
reset();
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
for (; !m_has_quantifiers && it != end; ++it) {
|
||||
|
|
|
@ -77,7 +77,7 @@ namespace datalog {
|
|||
|
||||
void set_query(func_decl* q);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
bool has_quantifiers() { return m_has_quantifiers; }
|
||||
|
||||
|
|
|
@ -90,6 +90,7 @@ namespace datalog {
|
|||
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);
|
||||
m_result->add_rule(filter_rule);
|
||||
m_context.get_rule_manager().mk_rule_asserted_proof(*filter_rule);
|
||||
}
|
||||
else {
|
||||
dealloc(key);
|
||||
|
@ -135,12 +136,13 @@ namespace datalog {
|
|||
}
|
||||
new_is_negated.push_back(r->is_neg_tail(i));
|
||||
}
|
||||
if(rule_modified) {
|
||||
if (rule_modified) {
|
||||
remove_duplicate_tails(new_tail, new_is_negated);
|
||||
SASSERT(new_tail.size() == new_is_negated.size());
|
||||
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr());
|
||||
new_rule->set_accounting_parent_object(m_context, m_current);
|
||||
m_result->add_rule(new_rule);
|
||||
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule);
|
||||
m_modified = true;
|
||||
}
|
||||
else {
|
||||
|
@ -148,7 +150,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc, pc
|
||||
m_tail2filter.reset();
|
||||
m_result = alloc(rule_set, m_context);
|
||||
|
|
|
@ -72,7 +72,7 @@ namespace datalog {
|
|||
/**
|
||||
\brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values.
|
||||
*/
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -35,7 +35,7 @@ namespace datalog {
|
|||
// -----------------------------------
|
||||
|
||||
void mk_interp_tail_simplifier::rule_substitution::reset(rule * r) {
|
||||
unsigned var_cnt = m_context.get_rule_manager().get_var_counter().get_max_var(*r)+1;
|
||||
unsigned var_cnt = m_context.get_rule_manager().get_counter().get_max_rule_var(*r)+1;
|
||||
m_subst.reset();
|
||||
m_subst.reserve(1, var_cnt);
|
||||
m_rule = r;
|
||||
|
@ -541,8 +541,8 @@ namespace datalog {
|
|||
|
||||
rule_ref pro_var_eq_result(m_context.get_rule_manager());
|
||||
if (propagate_variable_equivalences(res, pro_var_eq_result)) {
|
||||
SASSERT(var_counter().get_max_var(*r.get())==0 ||
|
||||
var_counter().get_max_var(*r.get()) > var_counter().get_max_var(*pro_var_eq_result.get()));
|
||||
SASSERT(rule_counter().get_max_rule_var(*r.get())==0 ||
|
||||
rule_counter().get_max_rule_var(*r.get()) > rule_counter().get_max_rule_var(*pro_var_eq_result.get()));
|
||||
r = pro_var_eq_result;
|
||||
goto start;
|
||||
}
|
||||
|
@ -554,11 +554,13 @@ namespace datalog {
|
|||
|
||||
bool mk_interp_tail_simplifier::transform_rules(const rule_set & orig, rule_set & tgt) {
|
||||
bool modified = false;
|
||||
rule_manager& rm = m_context.get_rule_manager();
|
||||
rule_set::iterator rit = orig.begin();
|
||||
rule_set::iterator rend = orig.end();
|
||||
for (; rit!=rend; ++rit) {
|
||||
rule_ref new_rule(m_context.get_rule_manager());
|
||||
rule_ref new_rule(rm);
|
||||
if (transform_rule(*rit, new_rule)) {
|
||||
rm.mk_rule_rewrite_proof(**rit, *new_rule.get());
|
||||
bool is_modified = *rit != new_rule;
|
||||
modified |= is_modified;
|
||||
tgt.add_rule(new_rule);
|
||||
|
@ -570,8 +572,7 @@ namespace datalog {
|
|||
return modified;
|
||||
}
|
||||
|
||||
rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
if (source.get_num_rules() == 0) {
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -93,7 +93,7 @@ namespace datalog {
|
|||
*/
|
||||
bool transform_rule(rule * r, rule_ref& res);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -145,7 +145,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) {
|
||||
unsigned num_vars = rm.get_var_counter().get_max_var(r)+1;
|
||||
unsigned num_vars = rm.get_counter().get_max_rule_var(r)+1;
|
||||
unsigned arity = r.get_decl()->get_arity();
|
||||
unsigned num_columns = arity + num_vars;
|
||||
unsigned utsz = r.get_uninterpreted_tail_size();
|
||||
|
@ -310,7 +310,7 @@ namespace datalog {
|
|||
m_hb.reset();
|
||||
for (unsigned i = 0; i < src.size(); ++i) {
|
||||
vector<rational> v(src.A[i]);
|
||||
v.append(src.b[i]);
|
||||
v.push_back(src.b[i]);
|
||||
if (src.eq[i]) {
|
||||
m_hb.add_eq(v, rational(0));
|
||||
}
|
||||
|
@ -420,6 +420,7 @@ namespace datalog {
|
|||
new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name());
|
||||
}
|
||||
rules.add_rule(new_rule);
|
||||
rm.mk_rule_rewrite_proof(r, *new_rule); // should be weakening rule.
|
||||
}
|
||||
|
||||
class mk_karr_invariants::add_invariant_model_converter : public model_converter {
|
||||
|
@ -519,7 +520,7 @@ namespace datalog {
|
|||
m_hb.set_cancel(true);
|
||||
}
|
||||
|
||||
rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
if (!m_ctx.get_params().karr()) {
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -69,7 +69,7 @@ namespace datalog {
|
|||
|
||||
virtual void cancel();
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -317,8 +317,8 @@ namespace datalog {
|
|||
m_rules.push_back(r);
|
||||
}
|
||||
|
||||
rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
SASSERT(!mc && !pc);
|
||||
rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
SASSERT(!mc);
|
||||
unsigned init_rule_cnt = source.get_num_rules();
|
||||
{
|
||||
func_decl_set intentional;
|
||||
|
|
|
@ -121,7 +121,7 @@ namespace datalog {
|
|||
*/
|
||||
mk_magic_sets(context & ctx, rule * goal_rule);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -86,8 +86,8 @@ namespace datalog {
|
|||
}
|
||||
|
||||
|
||||
rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc
|
||||
|
||||
if (source.get_num_rules() == 0) {
|
||||
return 0;
|
||||
|
|
|
@ -35,7 +35,7 @@ namespace datalog {
|
|||
m(ctx.get_manager()),
|
||||
m_context(ctx) {}
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
private:
|
||||
|
||||
|
|
|
@ -65,8 +65,8 @@ namespace datalog {
|
|||
// -----------------------------------
|
||||
|
||||
bool rule_unifier::unify_rules(const rule& tgt, unsigned tgt_idx, const rule& src) {
|
||||
var_counter& vc = m_rm.get_var_counter();
|
||||
unsigned var_cnt = std::max(vc.get_max_var(tgt), vc.get_max_var(src))+1;
|
||||
rule_counter& vc = m_rm.get_counter();
|
||||
unsigned var_cnt = std::max(vc.get_max_rule_var(tgt), vc.get_max_rule_var(src))+1;
|
||||
m_subst.reset();
|
||||
m_subst.reserve(2, var_cnt);
|
||||
|
||||
|
@ -181,10 +181,10 @@ namespace datalog {
|
|||
}
|
||||
|
||||
if (m_unifier.apply(tgt, tail_index, src, res)) {
|
||||
if (m_pc) {
|
||||
if (m_context.generate_proof_trace()) {
|
||||
expr_ref_vector s1 = m_unifier.get_rule_subst(tgt, true);
|
||||
expr_ref_vector s2 = m_unifier.get_rule_subst(src, false);
|
||||
datalog::resolve_rule(m_pc, tgt, src, tail_index, s1, s2, *res.get());
|
||||
datalog::resolve_rule(tgt, src, tail_index, s1, s2, *res.get());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
@ -733,7 +733,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
// initialize substitution.
|
||||
var_counter& vc = m_rm.get_var_counter();
|
||||
rule_counter& vc = m_rm.get_counter();
|
||||
unsigned max_var = 0;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
rule* r = acc[i].get();
|
||||
|
@ -820,7 +820,7 @@ namespace datalog {
|
|||
del_rule(r2, j);
|
||||
}
|
||||
|
||||
max_var = std::max(max_var, vc.get_max_var(*r.get()));
|
||||
max_var = std::max(max_var, vc.get_max_rule_var(*r.get()));
|
||||
m_subst.reserve_vars(max_var+1);
|
||||
|
||||
}
|
||||
|
@ -837,11 +837,10 @@ namespace datalog {
|
|||
return done_something;
|
||||
}
|
||||
|
||||
rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
|
||||
bool something_done = false;
|
||||
ref<horn_subsume_model_converter> hsmc;
|
||||
ref<replace_proof_converter> hpc;
|
||||
|
||||
if (source.get_num_rules() == 0) {
|
||||
return 0;
|
||||
|
@ -858,11 +857,7 @@ namespace datalog {
|
|||
if (mc) {
|
||||
hsmc = alloc(horn_subsume_model_converter, m);
|
||||
}
|
||||
if (pc) {
|
||||
hpc = alloc(replace_proof_converter, m);
|
||||
}
|
||||
m_mc = hsmc.get();
|
||||
m_pc = hpc.get();
|
||||
|
||||
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
|
||||
|
||||
|
@ -889,9 +884,6 @@ namespace datalog {
|
|||
if (mc) {
|
||||
mc = concat(mc.get(), hsmc.get());
|
||||
}
|
||||
if (pc) {
|
||||
pc = concat(pc.get(), hpc.get());
|
||||
}
|
||||
}
|
||||
|
||||
return res.detach();
|
||||
|
|
|
@ -114,7 +114,6 @@ namespace datalog {
|
|||
ast_counter m_tail_pred_ctr;
|
||||
rule_set m_inlined_rules;
|
||||
horn_subsume_model_converter* m_mc;
|
||||
replace_proof_converter* m_pc;
|
||||
|
||||
|
||||
//used in try_to_inline_rule and do_eager_inlining
|
||||
|
@ -188,7 +187,6 @@ namespace datalog {
|
|||
m_pinned(m_rm),
|
||||
m_inlined_rules(m_context),
|
||||
m_mc(0),
|
||||
m_pc(0),
|
||||
m_unifier(ctx),
|
||||
m_head_index(m),
|
||||
m_tail_index(m),
|
||||
|
@ -198,7 +196,7 @@ namespace datalog {
|
|||
{}
|
||||
virtual ~mk_rule_inliner() { }
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -372,10 +372,10 @@ namespace datalog {
|
|||
new_negs.push_back(r->is_neg_tail(i));
|
||||
}
|
||||
|
||||
var_counter var_ctr;
|
||||
var_ctr.count_vars(m_manager, r);
|
||||
rule_counter ctr;
|
||||
ctr.count_rule_vars(m_manager, r);
|
||||
unsigned max_var_idx, new_var_idx_base;
|
||||
if(var_ctr.get_max_positive(max_var_idx)) {
|
||||
if(ctr.get_max_positive(max_var_idx)) {
|
||||
new_var_idx_base = max_var_idx+1;
|
||||
}
|
||||
else {
|
||||
|
@ -500,8 +500,8 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc
|
||||
m_modified = false;
|
||||
unsigned init_rule_cnt = source.get_num_rules();
|
||||
SASSERT(m_rules.empty());
|
||||
|
|
|
@ -69,7 +69,7 @@ namespace datalog {
|
|||
public:
|
||||
mk_similarity_compressor(context & ctx, unsigned threshold_count);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -310,8 +310,8 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void register_rule(rule * r) {
|
||||
var_counter counter;
|
||||
counter.count_vars(m, r, 1);
|
||||
rule_counter counter;
|
||||
counter.count_rule_vars(m, r, 1);
|
||||
|
||||
ptr_vector<app> & rule_content =
|
||||
m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;
|
||||
|
@ -706,19 +706,20 @@ namespace datalog {
|
|||
negs.c_ptr());
|
||||
|
||||
new_rule->set_accounting_parent_object(m_context, orig_r);
|
||||
|
||||
m_context.get_rule_manager().mk_rule_rewrite_proof(*orig_r, *new_rule);
|
||||
result->add_rule(new_rule);
|
||||
}
|
||||
while(!m_introduced_rules.empty()) {
|
||||
while (!m_introduced_rules.empty()) {
|
||||
result->add_rule(m_introduced_rules.back());
|
||||
m_context.get_rule_manager().mk_rule_asserted_proof(*m_introduced_rules.back());
|
||||
m_introduced_rules.pop_back();
|
||||
}
|
||||
return result;
|
||||
}
|
||||
};
|
||||
|
||||
rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc
|
||||
rule_set rs_aux_copy(m_context);
|
||||
rs_aux_copy.add_rules(source);
|
||||
if(!rs_aux_copy.is_closed()) {
|
||||
|
|
|
@ -53,7 +53,7 @@ namespace datalog {
|
|||
public:
|
||||
mk_simple_joins(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -164,10 +164,8 @@ namespace datalog {
|
|||
TRACE("dl", tout << "does not have fact\n" << mk_pp(fact, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
expr_ref fml(m);
|
||||
proof_ref new_p(m);
|
||||
r->to_formula(fml);
|
||||
new_p = m.mk_asserted(fml);
|
||||
new_p = r->get_proof();
|
||||
m_pinned_exprs.push_back(new_p);
|
||||
m_todo.pop_back();
|
||||
m_new_proof.insert(p, new_p);
|
||||
|
@ -784,6 +782,9 @@ namespace datalog {
|
|||
rm.fix_unbound_vars(new_rule, false);
|
||||
|
||||
TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
rm.mk_rule_asserted_proof(*new_rule.get());
|
||||
}
|
||||
}
|
||||
else {
|
||||
new_rule = &r;
|
||||
|
@ -801,7 +802,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc) {
|
||||
for (unsigned i = 0; i < src.get_num_rules(); ++i) {
|
||||
if (src.get_rule(i)->has_quantifiers()) {
|
||||
return 0;
|
||||
|
@ -809,8 +810,8 @@ namespace datalog {
|
|||
}
|
||||
ref<slice_proof_converter> spc;
|
||||
ref<slice_model_converter> smc;
|
||||
if (pc) {
|
||||
spc = alloc(slice_proof_converter, m_ctx);
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
spc = alloc(slice_proof_converter, m_ctx);
|
||||
}
|
||||
if (mc) {
|
||||
smc = alloc(slice_model_converter, *this, m);
|
||||
|
@ -834,7 +835,7 @@ namespace datalog {
|
|||
m_mc->add_sliceable(it->m_key, it->m_value);
|
||||
}
|
||||
}
|
||||
pc = concat(pc.get(), spc.get());
|
||||
m_ctx.add_proof_converter(spc.get());
|
||||
mc = concat(mc.get(), smc.get());
|
||||
return result;
|
||||
}
|
||||
|
|
|
@ -102,7 +102,7 @@ namespace datalog {
|
|||
|
||||
virtual ~mk_slice() { }
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
|
||||
func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; }
|
||||
|
||||
|
|
|
@ -166,7 +166,8 @@ namespace datalog {
|
|||
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
|
||||
res->set_accounting_parent_object(m_context, r);
|
||||
m_context.get_rule_manager().fix_unbound_vars(res, true);
|
||||
|
||||
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -208,10 +209,10 @@ namespace datalog {
|
|||
continue;
|
||||
}
|
||||
rule * defining_rule;
|
||||
TRUSTME(m_total_relation_defining_rules.find(head_pred, defining_rule));
|
||||
if(defining_rule) {
|
||||
VERIFY(m_total_relation_defining_rules.find(head_pred, defining_rule));
|
||||
if (defining_rule) {
|
||||
rule_ref totality_rule(m_context.get_rule_manager());
|
||||
TRUSTME(transform_rule(defining_rule, subs_index, totality_rule));
|
||||
VERIFY(transform_rule(defining_rule, subs_index, totality_rule));
|
||||
if(defining_rule!=totality_rule) {
|
||||
modified = true;
|
||||
}
|
||||
|
@ -331,8 +332,8 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc
|
||||
|
||||
m_have_new_total_rule = false;
|
||||
collect_ground_unconditional_rule_heads(source);
|
||||
|
|
|
@ -84,7 +84,7 @@ namespace datalog {
|
|||
reset_dealloc_values(m_ground_unconditional_rule_heads);
|
||||
}
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -238,6 +238,7 @@ namespace datalog {
|
|||
|
||||
unsigned new_rule_index = m_rules.size();
|
||||
m_rules.push_back(new_rule);
|
||||
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule.get());
|
||||
m_head_occurrence_ctr.inc(new_rule->get_head()->get_decl());
|
||||
|
||||
|
||||
|
@ -333,8 +334,8 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
// TODO mc, pc
|
||||
rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
// TODO mc
|
||||
m_modified = false;
|
||||
|
||||
m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
|
||||
|
|
|
@ -82,7 +82,7 @@ namespace datalog {
|
|||
public:
|
||||
mk_unbound_compressor(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -42,29 +42,20 @@ namespace datalog {
|
|||
if (m_unify.unify_rules(r, tail_idx, r2) &&
|
||||
m_unify.apply(r, tail_idx, r2, new_rule)) {
|
||||
expr_ref_vector s1 = m_unify.get_rule_subst(r, true);
|
||||
expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);
|
||||
resolve_rule(m_pc, r, r2, tail_idx, s1, s2, *new_rule.get());
|
||||
expr_ref_vector s2 = m_unify.get_rule_subst(r2, false);
|
||||
resolve_rule(r, r2, tail_idx, s1, s2, *new_rule.get());
|
||||
expand_tail(*new_rule.get(), tail_idx+r2.get_uninterpreted_tail_size(), src, dst);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
m_pc = 0;
|
||||
ref<replace_proof_converter> rpc;
|
||||
if (pc) {
|
||||
rpc = alloc(replace_proof_converter, m);
|
||||
m_pc = rpc.get();
|
||||
}
|
||||
rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc) {
|
||||
rule_set* rules = alloc(rule_set, m_ctx);
|
||||
rule_set::iterator it = source.begin(), end = source.end();
|
||||
for (; it != end; ++it) {
|
||||
expand_tail(**it, 0, source, *rules);
|
||||
}
|
||||
if (pc) {
|
||||
pc = concat(pc.get(), rpc.get());
|
||||
}
|
||||
return rules;
|
||||
}
|
||||
|
||||
|
|
|
@ -35,7 +35,6 @@ namespace datalog {
|
|||
ast_manager& m;
|
||||
rule_manager& rm;
|
||||
rule_unifier m_unify;
|
||||
replace_proof_converter* m_pc;
|
||||
|
||||
void expand_tail(rule& r, unsigned tail_idx, rule_set const& src, rule_set& dst);
|
||||
|
||||
|
@ -45,7 +44,7 @@ namespace datalog {
|
|||
*/
|
||||
mk_unfold(context & ctx);
|
||||
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
rule_set * operator()(rule_set const & source, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
@ -42,13 +42,13 @@ Revision History:
|
|||
#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_refs(ctx.get_manager()) {}
|
||||
m_ctx(ctx) {}
|
||||
|
||||
bool rule_manager::is_predicate(func_decl * f) const {
|
||||
return m_ctx.is_predicate(f);
|
||||
|
@ -89,111 +89,32 @@ namespace datalog {
|
|||
}
|
||||
};
|
||||
|
||||
void rule_manager::remove_labels(expr_ref& fml) {
|
||||
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);
|
||||
if (pr && fml != tmp) {
|
||||
|
||||
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
|
||||
}
|
||||
fml = tmp;
|
||||
}
|
||||
|
||||
|
||||
void rule_manager::mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name) {
|
||||
void rule_manager::mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name) {
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
proof_ref pr(p, m);
|
||||
expr_ref fml1(m);
|
||||
m_memoize_disj.reset();
|
||||
m_refs.reset();
|
||||
bind_variables(fml, true, fml1);
|
||||
unsigned num_rules = rules.size();
|
||||
mk_rule_core(fml1, rules, name);
|
||||
if (m_pc) {
|
||||
// big-step proof
|
||||
// m.mk_cnf_star(fml1, conj, 0, 0);
|
||||
//
|
||||
if (fml1 != fml && pr) {
|
||||
pr = m.mk_asserted(fml1);
|
||||
}
|
||||
remove_labels(fml1, pr);
|
||||
mk_rule_core_new(fml1, pr, rules, name);
|
||||
}
|
||||
|
||||
//
|
||||
// Hoist quantifier from rule (universal) or query (existential)
|
||||
//
|
||||
unsigned rule_manager::hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
|
||||
|
||||
unsigned index = var_counter().get_next_var(fml);
|
||||
while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
|
||||
quantifier* q = to_quantifier(fml);
|
||||
index += q->get_num_decls();
|
||||
if (names) {
|
||||
names->append(q->get_num_decls(), q->get_decl_names());
|
||||
}
|
||||
fml = q->get_expr();
|
||||
}
|
||||
if (!has_quantifiers(fml)) {
|
||||
return index;
|
||||
}
|
||||
app_ref_vector vars(m);
|
||||
quantifier_hoister qh(m);
|
||||
qh.pull_quantifier(is_forall, fml, vars);
|
||||
if (vars.empty()) {
|
||||
return index;
|
||||
}
|
||||
// replace vars by de-bruijn indices
|
||||
expr_safe_replace rep(m);
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
app* v = vars[i].get();
|
||||
if (names) {
|
||||
names->push_back(v->get_decl()->get_name());
|
||||
}
|
||||
rep.insert(v, m.mk_var(index++,m.get_sort(v)));
|
||||
}
|
||||
rep(fml);
|
||||
return index;
|
||||
}
|
||||
|
||||
void rule_manager::mk_rule_core(expr* _fml, rule_ref_vector& rules, symbol const& name) {
|
||||
app_ref_vector body(m);
|
||||
app_ref head(m);
|
||||
expr_ref e(m), fml(_fml, m);
|
||||
svector<bool> is_negated;
|
||||
TRACE("dl_rule", tout << mk_pp(fml, m) << "\n";);
|
||||
unsigned index = hoist_quantifier(true, fml, 0);
|
||||
check_app(fml);
|
||||
head = to_app(fml);
|
||||
|
||||
while (m.is_implies(head)) {
|
||||
e = head->get_arg(0);
|
||||
th_rewriter th_rwr(m);
|
||||
th_rwr(e);
|
||||
body.push_back(ensure_app(e));
|
||||
e = to_app(head)->get_arg(1);
|
||||
check_app(e);
|
||||
head = to_app(e.get());
|
||||
}
|
||||
symbol head_name = (name == symbol::null)?head->get_decl()->get_name():name;
|
||||
flatten_body(body);
|
||||
if (body.size() == 1 && m.is_or(body[0].get()) && contains_predicate(body[0].get())) {
|
||||
app* _or = to_app(body[0].get());
|
||||
for (unsigned i = 0; i < _or->get_num_args(); ++i) {
|
||||
e = m.mk_implies(_or->get_arg(i), head);
|
||||
mk_rule_core(e, rules, head_name);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
eliminate_disjunctions(body, rules, head_name);
|
||||
eliminate_quantifier_body(body, rules, head_name);
|
||||
hoist_compound(index, head, body);
|
||||
unsigned sz = body.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
app_ref b(body[i].get(), m);
|
||||
hoist_compound(index, b, body);
|
||||
body[i] = b;
|
||||
}
|
||||
TRACE("dl_rule",
|
||||
tout << mk_pp(head, m) << " :- ";
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
tout << mk_pp(body[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
void rule_manager::mk_negations(app_ref_vector& body, svector<bool>& is_negated) {
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
expr* e = body[i].get(), *e1;
|
||||
if (m.is_not(e, e1) && is_predicate(e1)) {
|
||||
|
@ -204,23 +125,105 @@ namespace datalog {
|
|||
else {
|
||||
is_negated.push_back(false);
|
||||
}
|
||||
}
|
||||
check_valid_rule(head, body.size(), body.c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
rules.push_back(mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name));
|
||||
|
||||
if (m_ctx.fix_unbound_vars()) {
|
||||
unsigned rule_cnt = rules.size();
|
||||
for (unsigned i=0; i<rule_cnt; ++i) {
|
||||
rule_ref r(rules[i].get(), *this);
|
||||
fix_unbound_vars(r, true);
|
||||
if (r.get()!=rules[i].get()) {
|
||||
rules[i] = r;
|
||||
}
|
||||
}
|
||||
void rule_manager::mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& 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]);
|
||||
}
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name);
|
||||
}
|
||||
}
|
||||
|
||||
void rule_manager::mk_rule_core2(expr* fml, proof* p, rule_ref_vector& 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);
|
||||
TRACE("dl_rule",
|
||||
tout << mk_pp(head, m) << " :- ";
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
tout << mk_pp(body[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
|
||||
mk_negations(body, is_negated);
|
||||
check_valid_rule(head, body.size(), body.c_ptr());
|
||||
|
||||
rule_ref r(*this);
|
||||
r = mk(head.get(), body.size(), body.c_ptr(), is_negated.c_ptr(), name);
|
||||
|
||||
expr_ref fml1(m);
|
||||
if (p) {
|
||||
r->to_formula(fml1);
|
||||
if (fml1 == fml) {
|
||||
// no-op.
|
||||
}
|
||||
else if (is_quantifier(fml1)) {
|
||||
p = m.mk_modus_ponens(p, m.mk_symmetry(m.mk_der(to_quantifier(fml1), fml)));
|
||||
}
|
||||
else {
|
||||
p = m.mk_modus_ponens(p, m.mk_rewrite(fml, fml1));
|
||||
}
|
||||
}
|
||||
|
||||
if (m_ctx.fix_unbound_vars()) {
|
||||
fix_unbound_vars(r, true);
|
||||
}
|
||||
|
||||
if (p) {
|
||||
expr_ref fml2(m);
|
||||
r->to_formula(fml2);
|
||||
if (fml1 != fml2) {
|
||||
p = m.mk_modus_ponens(p, m.mk_rewrite(fml1, fml2));
|
||||
}
|
||||
r->set_proof(m, p);
|
||||
}
|
||||
rules.push_back(r);
|
||||
}
|
||||
|
||||
unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) {
|
||||
expr* e1, *e2;
|
||||
unsigned index = m_counter.get_next_var(fml);
|
||||
if (::is_forall(fml)) {
|
||||
index += to_quantifier(fml)->get_num_decls();
|
||||
fml = to_quantifier(fml)->get_expr();
|
||||
}
|
||||
if (m.is_implies(fml, e1, e2)) {
|
||||
expr_ref_vector es(m);
|
||||
head = ensure_app(e2);
|
||||
datalog::flatten_and(e1, es);
|
||||
for (unsigned i = 0; i < es.size(); ++i) {
|
||||
body.push_back(ensure_app(es[i].get()));
|
||||
}
|
||||
}
|
||||
else {
|
||||
head = ensure_app(fml);
|
||||
}
|
||||
return index;
|
||||
}
|
||||
|
||||
void rule_manager::hoist_compound_predicates(unsigned index, app_ref& head, app_ref_vector& body) {
|
||||
unsigned sz = body.size();
|
||||
hoist_compound(index, head, body);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
app_ref b(body[i].get(), m);
|
||||
hoist_compound(index, b, body);
|
||||
body[i] = b;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void rule_manager::mk_query(expr* query, func_decl_ref& qpred, rule_ref_vector& query_rules, rule_ref& query_rule) {
|
||||
ptr_vector<sort> vars;
|
||||
svector<symbol> names;
|
||||
|
@ -230,7 +233,8 @@ namespace datalog {
|
|||
// Add implicit variables.
|
||||
// Remove existential prefix.
|
||||
bind_variables(query, false, q);
|
||||
hoist_quantifier(false, q, &names);
|
||||
quantifier_hoister qh(m);
|
||||
qh.pull_quantifier(false, q, 0, &names);
|
||||
// retrieve free variables.
|
||||
get_free_vars(q, vars);
|
||||
if (vars.contains(static_cast<sort*>(0))) {
|
||||
|
@ -288,7 +292,12 @@ namespace datalog {
|
|||
rule_expr = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), impl);
|
||||
}
|
||||
|
||||
mk_rule(rule_expr, query_rules);
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
proof_ref pr(m);
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
pr = m.mk_asserted(rule_expr);
|
||||
}
|
||||
mk_rule(rule_expr, pr, query_rules);
|
||||
SASSERT(query_rules.size() >= 1);
|
||||
query_rule = query_rules.back();
|
||||
}
|
||||
|
@ -368,73 +377,6 @@ namespace datalog {
|
|||
return false;
|
||||
}
|
||||
|
||||
void rule_manager::eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
|
||||
|
||||
app* b = body.get();
|
||||
expr* e1;
|
||||
bool negate_args = false;
|
||||
bool is_disj = false;
|
||||
unsigned num_disj = 0;
|
||||
expr* const* disjs = 0;
|
||||
if (!contains_predicate(b)) {
|
||||
return;
|
||||
}
|
||||
TRACE("dl_rule", tout << mk_ismt2_pp(b, m) << "\n";);
|
||||
if (m.is_or(b)) {
|
||||
is_disj = true;
|
||||
negate_args = false;
|
||||
num_disj = b->get_num_args();
|
||||
disjs = b->get_args();
|
||||
}
|
||||
if (m.is_not(b, e1) && m.is_and(e1)) {
|
||||
is_disj = true;
|
||||
negate_args = true;
|
||||
num_disj = to_app(e1)->get_num_args();
|
||||
disjs = to_app(e1)->get_args();
|
||||
}
|
||||
if (is_disj) {
|
||||
ptr_vector<sort> sorts0, sorts1;
|
||||
get_free_vars(b, sorts0);
|
||||
expr_ref_vector args(m);
|
||||
for (unsigned i = 0; i < sorts0.size(); ++i) {
|
||||
if (sorts0[i]) {
|
||||
args.push_back(m.mk_var(i,sorts0[i]));
|
||||
sorts1.push_back(sorts0[i]);
|
||||
}
|
||||
}
|
||||
app* old_head = 0;
|
||||
if (m_memoize_disj.find(b, old_head)) {
|
||||
body = old_head;
|
||||
}
|
||||
else {
|
||||
app_ref head(m);
|
||||
func_decl_ref f(m);
|
||||
f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
|
||||
m_ctx.register_predicate(f);
|
||||
head = m.mk_app(f, args.size(), args.c_ptr());
|
||||
|
||||
for (unsigned i = 0; i < num_disj; ++i) {
|
||||
expr_ref fml(m);
|
||||
expr* e = disjs[i];
|
||||
if (negate_args) e = m.mk_not(e);
|
||||
fml = m.mk_implies(e,head);
|
||||
mk_rule_core(fml, rules, name);
|
||||
}
|
||||
m_memoize_disj.insert(b, head);
|
||||
m_refs.push_back(b);
|
||||
m_refs.push_back(head);
|
||||
// update the body to be the newly introduced head relation
|
||||
body = head;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void rule_manager::eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
app_ref_vector::element_ref t = body[i];
|
||||
eliminate_disjunctions(t, rules, name);
|
||||
}
|
||||
}
|
||||
|
||||
bool rule_manager::is_forall(ast_manager& m, expr* e, quantifier*& q) {
|
||||
expr* e1, *e2;
|
||||
|
@ -453,40 +395,6 @@ namespace datalog {
|
|||
return false;
|
||||
}
|
||||
|
||||
void rule_manager::eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name) {
|
||||
quantifier* q;
|
||||
if (is_forall(m, body.get(), q) && contains_predicate(q)) {
|
||||
expr* e = q->get_expr();
|
||||
if (!is_predicate(e)) {
|
||||
ptr_vector<sort> sorts0, sorts1;
|
||||
get_free_vars(e, sorts0);
|
||||
expr_ref_vector args(m);
|
||||
for (unsigned i = 0; i < sorts0.size(); ++i) {
|
||||
if (sorts0[i]) {
|
||||
args.push_back(m.mk_var(i,sorts0[i]));
|
||||
sorts1.push_back(sorts0[i]);
|
||||
}
|
||||
}
|
||||
app_ref head(m), fml(m);
|
||||
func_decl_ref f(m);
|
||||
f = m.mk_fresh_func_decl(name.str().c_str(),"", sorts1.size(), sorts1.c_ptr(), m.mk_bool_sort());
|
||||
m_ctx.register_predicate(f);
|
||||
head = m.mk_app(f, args.size(), args.c_ptr());
|
||||
fml = m.mk_implies(e, head);
|
||||
mk_rule_core(fml, rules, name);
|
||||
// update the body to be the newly introduced head relation
|
||||
body = m.mk_eq(m.mk_true(), m.update_quantifier(q, head));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void rule_manager::eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name) {
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
app_ref_vector::element_ref t = body[i];
|
||||
eliminate_quantifier_body(t, rules, name);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
app_ref rule_manager::ensure_app(expr* e) {
|
||||
SASSERT(m.is_bool(e));
|
||||
|
@ -514,6 +422,7 @@ namespace datalog {
|
|||
r->m_head = head;
|
||||
r->m_name = name;
|
||||
r->m_tail_size = n;
|
||||
r->m_proof = 0;
|
||||
m.inc_ref(r->m_head);
|
||||
|
||||
app * * uninterp_tail = r->m_tail; //grows upwards
|
||||
|
@ -571,6 +480,11 @@ namespace datalog {
|
|||
if (normalize) {
|
||||
r->norm_vars(*this);
|
||||
}
|
||||
DEBUG_CODE(ptr_vector<sort> sorts;
|
||||
::get_free_vars(head, sorts);
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
::get_free_vars(tail[i], sorts);
|
||||
});
|
||||
return r;
|
||||
}
|
||||
|
||||
|
@ -710,7 +624,7 @@ namespace datalog {
|
|||
bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
|
||||
|
||||
unsigned q_var_cnt = unbound_vars.num_elems();
|
||||
unsigned max_var = m_var_counter.get_max_var(*r);
|
||||
unsigned max_var = m_counter.get_max_rule_var(*r);
|
||||
|
||||
expr_ref_vector subst(m);
|
||||
|
||||
|
@ -792,6 +706,27 @@ namespace datalog {
|
|||
r->set_accounting_parent_object(m_ctx, old_r);
|
||||
}
|
||||
|
||||
void rule_manager::mk_rule_rewrite_proof(rule& old_rule, rule& new_rule) {
|
||||
if (&old_rule != &new_rule &&
|
||||
!new_rule.get_proof() &&
|
||||
old_rule.get_proof()) {
|
||||
expr_ref fml(m);
|
||||
new_rule.to_formula(fml);
|
||||
scoped_proof _sc(m);
|
||||
proof* p = m.mk_rewrite(m.get_fact(old_rule.get_proof()), fml);
|
||||
new_rule.set_proof(m, m.mk_modus_ponens(old_rule.get_proof(), p));
|
||||
}
|
||||
}
|
||||
|
||||
void rule_manager::mk_rule_asserted_proof(rule& r) {
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
scoped_proof _scp(m);
|
||||
expr_ref fml(m);
|
||||
r.to_formula(fml);
|
||||
r.set_proof(m, m.mk_asserted(fml));
|
||||
}
|
||||
}
|
||||
|
||||
void rule_manager::substitute(rule_ref& r, unsigned sz, expr*const* es) {
|
||||
expr_ref tmp(m);
|
||||
app_ref new_head(m);
|
||||
|
@ -850,10 +785,23 @@ namespace datalog {
|
|||
for (unsigned i = 0; i < n; i++) {
|
||||
m.dec_ref(get_tail(i));
|
||||
}
|
||||
if (m_proof) {
|
||||
m.dec_ref(m_proof);
|
||||
}
|
||||
this->~rule();
|
||||
m.get_allocator().deallocate(get_obj_size(n), this);
|
||||
}
|
||||
|
||||
void rule::set_proof(ast_manager& m, proof* p) {
|
||||
if (p) {
|
||||
m.inc_ref(p);
|
||||
}
|
||||
if (m_proof) {
|
||||
m.dec_ref(m_proof);
|
||||
}
|
||||
m_proof = p;
|
||||
}
|
||||
|
||||
bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
|
||||
unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size();
|
||||
for (unsigned i = 0; i < len; i++) {
|
||||
|
@ -1031,6 +979,9 @@ namespace datalog {
|
|||
out << '}';
|
||||
}
|
||||
out << '\n';
|
||||
if (m_proof) {
|
||||
out << mk_pp(m_proof, m) << '\n';
|
||||
}
|
||||
}
|
||||
|
||||
void rule::to_formula(expr_ref& fml) const {
|
||||
|
@ -1120,3 +1071,4 @@ namespace datalog {
|
|||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -46,38 +46,25 @@ namespace datalog {
|
|||
*/
|
||||
class rule_manager
|
||||
{
|
||||
ast_manager& m;
|
||||
context& m_ctx;
|
||||
var_counter m_var_counter;
|
||||
obj_map<expr, app*> m_memoize_disj;
|
||||
expr_ref_vector m_refs;
|
||||
model_converter_ref m_mc;
|
||||
proof_converter_ref m_pc;
|
||||
ast_manager& m;
|
||||
context& m_ctx;
|
||||
rule_counter m_counter;
|
||||
|
||||
// only the context can create a rule_manager
|
||||
friend class context;
|
||||
|
||||
explicit rule_manager(context& ctx);
|
||||
|
||||
void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
|
||||
void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
|
||||
|
||||
/**
|
||||
\brief Move functions from predicate tails into the interpreted tail by introducing new variables.
|
||||
*/
|
||||
void hoist_compound_predicates(unsigned num_bound, app_ref& head, app_ref_vector& body);
|
||||
|
||||
void hoist_compound(unsigned& num_bound, app_ref& fml, app_ref_vector& body);
|
||||
|
||||
void flatten_body(app_ref_vector& body);
|
||||
|
||||
void remove_labels(expr_ref& fml);
|
||||
|
||||
void eliminate_disjunctions(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
void eliminate_disjunctions(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
void eliminate_quantifier_body(app_ref_vector::element_ref& body, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
void eliminate_quantifier_body(app_ref_vector& body, rule_ref_vector& rules, symbol const& name);
|
||||
void remove_labels(expr_ref& fml, proof_ref& pr);
|
||||
|
||||
app_ref ensure_app(expr* e);
|
||||
|
||||
|
@ -89,7 +76,15 @@ namespace datalog {
|
|||
|
||||
void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
unsigned hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
|
||||
void mk_negations(app_ref_vector& body, svector<bool>& is_negated);
|
||||
|
||||
void mk_rule_core_new(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
void mk_rule_core2(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name);
|
||||
|
||||
static expr_ref mk_implies(app_ref_vector const& body, expr* head);
|
||||
|
||||
unsigned extract_horn(expr* fml, app_ref_vector& body, app_ref& head);
|
||||
|
||||
/**
|
||||
\brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
|
||||
|
@ -109,7 +104,7 @@ namespace datalog {
|
|||
The formula is of the form (forall (...) (forall (...) (=> (and ...) head)))
|
||||
|
||||
*/
|
||||
void mk_rule(expr* fml, rule_ref_vector& rules, symbol const& name = symbol::null);
|
||||
void mk_rule(expr* fml, proof* p, rule_ref_vector& rules, symbol const& name = symbol::null);
|
||||
|
||||
/**
|
||||
\brief Create a Datalog query from an expression.
|
||||
|
@ -139,7 +134,15 @@ namespace datalog {
|
|||
/** make sure there are not non-quantified variables that occur only in interpreted predicates */
|
||||
void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
|
||||
|
||||
/**
|
||||
\brief add proof that new rule is obtained by rewriting old rule.
|
||||
*/
|
||||
void mk_rule_rewrite_proof(rule& old_rule, rule& new_rule);
|
||||
|
||||
/**
|
||||
\brief tag rule as asserted.
|
||||
*/
|
||||
void mk_rule_asserted_proof(rule& r);
|
||||
|
||||
/**
|
||||
\brief apply substitution to variables of rule.
|
||||
|
@ -170,7 +173,7 @@ namespace datalog {
|
|||
|
||||
static bool is_forall(ast_manager& m, expr* e, quantifier*& q);
|
||||
|
||||
var_counter& get_var_counter() { return m_var_counter; }
|
||||
rule_counter& get_counter() { return m_counter; }
|
||||
|
||||
};
|
||||
|
||||
|
@ -178,6 +181,7 @@ namespace datalog {
|
|||
friend class rule_manager;
|
||||
|
||||
app * m_head;
|
||||
proof* m_proof;
|
||||
unsigned m_tail_size:20;
|
||||
// unsigned m_reserve:12;
|
||||
unsigned m_ref_cnt;
|
||||
|
@ -209,6 +213,10 @@ namespace datalog {
|
|||
void get_used_vars(used_vars& uv) const;
|
||||
|
||||
public:
|
||||
|
||||
proof * get_proof() const { return m_proof; }
|
||||
|
||||
void set_proof(ast_manager& m, proof* p);
|
||||
|
||||
app * get_head() const { return m_head; }
|
||||
|
||||
|
|
|
@ -73,7 +73,7 @@ namespace datalog {
|
|||
m_dirty=true;
|
||||
}
|
||||
|
||||
bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc) {
|
||||
bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc) {
|
||||
ensure_ordered();
|
||||
|
||||
bool modified = false;
|
||||
|
@ -87,7 +87,7 @@ namespace datalog {
|
|||
for(; it!=end && !m_cancel; ++it) {
|
||||
plugin & p = **it;
|
||||
|
||||
rule_set * new_rules = p(rules, mc, pc);
|
||||
rule_set * new_rules = p(rules, mc);
|
||||
if (!new_rules) {
|
||||
continue;
|
||||
}
|
||||
|
|
|
@ -24,7 +24,6 @@ Revision History:
|
|||
#include"dl_rule.h"
|
||||
#include"dl_rule_set.h"
|
||||
#include"model_converter.h"
|
||||
#include"proof_converter.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -69,7 +68,7 @@ namespace datalog {
|
|||
\brief Transform the rule set using the registered transformation plugins. If the rule
|
||||
set has changed, return true; otherwise return false.
|
||||
*/
|
||||
bool operator()(rule_set & rules, model_converter_ref& mc, proof_converter_ref& pc);
|
||||
bool operator()(rule_set & rules, model_converter_ref& mc);
|
||||
};
|
||||
|
||||
class rule_transformer::plugin {
|
||||
|
@ -106,8 +105,7 @@ namespace datalog {
|
|||
The caller takes ownership of the returned \c rule_set object.
|
||||
*/
|
||||
virtual rule_set * operator()(rule_set const & source,
|
||||
model_converter_ref& mc,
|
||||
proof_converter_ref& pc) = 0;
|
||||
model_converter_ref& mc) = 0;
|
||||
|
||||
virtual void cancel() { m_cancel = true; }
|
||||
|
||||
|
|
|
@ -431,6 +431,29 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
|
||||
<<<<<<< HEAD
|
||||
=======
|
||||
|
||||
void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
|
||||
count_vars(m, r->get_head(), 1);
|
||||
unsigned n = r->get_tail_size();
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
count_vars(m, r->get_tail(i), coef);
|
||||
}
|
||||
}
|
||||
|
||||
unsigned rule_counter::get_max_rule_var(const rule & r) {
|
||||
m_todo.push_back(r.get_head());
|
||||
m_scopes.push_back(0);
|
||||
unsigned n = r.get_tail_size();
|
||||
bool has_var = false;
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
m_todo.push_back(r.get_tail(i));
|
||||
m_scopes.push_back(0);
|
||||
}
|
||||
return get_max_var(has_var);
|
||||
}
|
||||
>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
|
||||
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r) {
|
||||
if (mc) {
|
||||
|
@ -492,6 +515,44 @@ namespace datalog {
|
|||
pc->insert(pr);
|
||||
}
|
||||
|
||||
void resolve_rule(rule const& r1, rule const& r2, unsigned idx,
|
||||
expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
|
||||
if (!r1.get_proof()) {
|
||||
return;
|
||||
}
|
||||
SASSERT(r2.get_proof());
|
||||
ast_manager& m = s1.get_manager();
|
||||
expr_ref fml(m);
|
||||
res.to_formula(fml);
|
||||
vector<expr_ref_vector> substs;
|
||||
svector<std::pair<unsigned, unsigned> > positions;
|
||||
substs.push_back(s1);
|
||||
substs.push_back(s2);
|
||||
|
||||
scoped_proof _sc(m);
|
||||
proof_ref pr(m);
|
||||
proof_ref_vector premises(m);
|
||||
premises.push_back(r1.get_proof());
|
||||
premises.push_back(r2.get_proof());
|
||||
positions.push_back(std::make_pair(idx+1, 0));
|
||||
|
||||
TRACE("dl",
|
||||
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
|
||||
for (unsigned i = 0; i < s1.size(); ++i) {
|
||||
tout << mk_pp(s1[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
|
||||
for (unsigned i = 0; i < s2.size(); ++i) {
|
||||
tout << mk_pp(s2[i], m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
|
||||
res.set_proof(m, pr);
|
||||
}
|
||||
|
||||
class skip_model_converter : public model_converter {
|
||||
public:
|
||||
skip_model_converter() {}
|
||||
|
@ -519,10 +580,6 @@ namespace datalog {
|
|||
proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); }
|
||||
|
||||
|
||||
unsigned get_max_var(const rule & r, ast_manager & m) {
|
||||
var_counter ctr;
|
||||
return ctr.get_max_var(r);
|
||||
}
|
||||
|
||||
void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt) {
|
||||
SASSERT(tgt.empty());
|
||||
|
|
|
@ -27,6 +27,7 @@ Revision History:
|
|||
#include"replace_proof_converter.h"
|
||||
#include"substitution.h"
|
||||
#include"fixedpoint_params.hpp"
|
||||
#include"ast_counter.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -411,21 +412,26 @@ namespace datalog {
|
|||
}
|
||||
|
||||
|
||||
class rule_counter : public var_counter {
|
||||
public:
|
||||
rule_counter(bool stay_non_negative = true): var_counter(stay_non_negative) {}
|
||||
void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
|
||||
unsigned get_max_rule_var(const rule& r);
|
||||
};
|
||||
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r);
|
||||
|
||||
void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,
|
||||
expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res);
|
||||
|
||||
void resolve_rule(rule const& r1, rule const& r2, unsigned idx,
|
||||
expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res);
|
||||
|
||||
model_converter* mk_skip_model_converter();
|
||||
|
||||
proof_converter* mk_skip_proof_converter();
|
||||
|
||||
|
||||
/**
|
||||
Return maximal variable number, or zero is there isn't any
|
||||
*/
|
||||
// unsigned get_max_var(const rule & r, ast_manager & m);
|
||||
|
||||
void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt);
|
||||
|
||||
/**
|
||||
|
|
|
@ -22,12 +22,14 @@ Revision History:
|
|||
#include "dl_util.h"
|
||||
|
||||
void equiv_proof_converter::insert(expr* fml1, expr* fml2) {
|
||||
datalog::scoped_proof _sp(m);
|
||||
proof_ref p1(m), p2(m), p3(m);
|
||||
p1 = m.mk_asserted(fml1);
|
||||
p2 = m.mk_rewrite(fml1, fml2);
|
||||
p3 = m.mk_modus_ponens(p1, p2);
|
||||
TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
|
||||
SASSERT(m.has_fact(p3));
|
||||
m_replace.insert(p3);
|
||||
if (fml1 != fml2) {
|
||||
datalog::scoped_proof _sp(m);
|
||||
proof_ref p1(m), p2(m), p3(m);
|
||||
p1 = m.mk_asserted(fml1);
|
||||
p2 = m.mk_rewrite(fml1, fml2);
|
||||
p3 = m.mk_modus_ponens(p1, p2);
|
||||
TRACE("proof_converter", tout << mk_pp(p3.get(), m) << "\n";);
|
||||
SASSERT(m.has_fact(p3));
|
||||
m_replace.insert(p3);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -113,8 +113,8 @@ class horn_tactic : public tactic {
|
|||
todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
|
||||
}
|
||||
else if (m.is_ite(a)) {
|
||||
todo.append(to_app(a)->get_arg(1));
|
||||
todo.append(to_app(a)->get_arg(2));
|
||||
todo.push_back(to_app(a)->get_arg(1));
|
||||
todo.push_back(to_app(a)->get_arg(2));
|
||||
}
|
||||
else if (is_predicate(a)) {
|
||||
register_predicate(a);
|
||||
|
@ -270,21 +270,16 @@ class horn_tactic : public tactic {
|
|||
proof_converter_ref & pc) {
|
||||
|
||||
expr_ref fml(m);
|
||||
bool produce_models = g->models_enabled();
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
|
||||
if (produce_models) {
|
||||
mc = datalog::mk_skip_model_converter();
|
||||
}
|
||||
if (produce_proofs) {
|
||||
pc = datalog::mk_skip_proof_converter();
|
||||
}
|
||||
|
||||
func_decl* query_pred = to_app(q)->get_decl();
|
||||
m_ctx.set_output_predicate(query_pred);
|
||||
m_ctx.get_rules(); // flush adding rules.
|
||||
<<<<<<< HEAD
|
||||
m_ctx.set_model_converter(mc);
|
||||
m_ctx.set_proof_converter(pc);
|
||||
=======
|
||||
>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
|
||||
m_ctx.apply_default_transformation();
|
||||
|
||||
if (m_ctx.get_params().slice()) {
|
||||
|
|
|
@ -950,16 +950,45 @@ namespace pdr {
|
|||
return out;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Ensure that all nodes in the tree have associated models.
|
||||
get_trace and get_proof_trace rely on models to extract rules.
|
||||
*/
|
||||
void model_search::update_models() {
|
||||
obj_map<expr, model*> models;
|
||||
ptr_vector<model_node> todo;
|
||||
todo.push_back(m_root);
|
||||
while (!todo.empty()) {
|
||||
model_node* n = todo.back();
|
||||
if (n->get_model_ptr()) {
|
||||
models.insert(n->state(), n->get_model_ptr());
|
||||
}
|
||||
todo.pop_back();
|
||||
todo.append(n->children().size(), n->children().c_ptr());
|
||||
}
|
||||
|
||||
todo.push_back(m_root);
|
||||
while (!todo.empty()) {
|
||||
model_node* n = todo.back();
|
||||
model* md = 0;
|
||||
if (!n->get_model_ptr() && models.find(n->state(), md)) {
|
||||
model_ref mr(md);
|
||||
n->set_model(mr);
|
||||
}
|
||||
todo.pop_back();
|
||||
todo.append(n->children().size(), n->children().c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
Extract trace comprising of constraints
|
||||
and predicates that are satisfied from facts to the query.
|
||||
The resulting trace
|
||||
*/
|
||||
expr_ref model_search::get_trace(context const& ctx) const {
|
||||
expr_ref model_search::get_trace(context const& ctx) {
|
||||
pred_transformer& pt = get_root().pt();
|
||||
ast_manager& m = pt.get_manager();
|
||||
manager& pm = pt.get_pdr_manager();
|
||||
|
||||
datalog::context& dctx = ctx.get_context();
|
||||
datalog::rule_manager& rm = dctx.get_rule_manager();
|
||||
expr_ref_vector constraints(m), predicates(m);
|
||||
|
@ -968,22 +997,24 @@ namespace pdr {
|
|||
unsigned deltas[2];
|
||||
datalog::rule_ref rule(rm), r0(rm);
|
||||
model_node* n = m_root;
|
||||
datalog::var_counter& vc = rm.get_var_counter();
|
||||
datalog::rule_counter& vc = rm.get_counter();
|
||||
substitution subst(m);
|
||||
unifier unif(m);
|
||||
rule = n->get_rule();
|
||||
unsigned max_var = vc.get_max_var(*rule);
|
||||
unsigned max_var = vc.get_max_rule_var(*rule);
|
||||
predicates.push_back(rule->get_head());
|
||||
children.append(n);
|
||||
children.push_back(n);
|
||||
bool first = true;
|
||||
update_models();
|
||||
while (!children.empty()) {
|
||||
SASSERT(children.size() == predicates.size());
|
||||
expr_ref_vector binding(m);
|
||||
n = children.back();
|
||||
children.pop_back();
|
||||
TRACE("pdr", n->display(tout, 0););
|
||||
n->mk_instantiate(r0, rule, binding);
|
||||
|
||||
max_var = std::max(max_var, vc.get_max_var(*rule));
|
||||
max_var = std::max(max_var, vc.get_max_rule_var(*rule));
|
||||
subst.reset();
|
||||
subst.reserve(2, max_var+1);
|
||||
deltas[0] = 0;
|
||||
|
@ -1026,7 +1057,7 @@ namespace pdr {
|
|||
return pm.mk_and(constraints);
|
||||
}
|
||||
|
||||
proof_ref model_search::get_proof_trace(context const& ctx) const {
|
||||
proof_ref model_search::get_proof_trace(context const& ctx) {
|
||||
pred_transformer& pt = get_root().pt();
|
||||
ast_manager& m = pt.get_manager();
|
||||
datalog::context& dctx = ctx.get_context();
|
||||
|
@ -1042,8 +1073,10 @@ namespace pdr {
|
|||
proof* pr = 0;
|
||||
unifier.set_normalize(false);
|
||||
todo.push_back(m_root);
|
||||
update_models();
|
||||
while (!todo.empty()) {
|
||||
model_node* n = todo.back();
|
||||
TRACE("pdr", n->display(tout, 0););
|
||||
if (cache.find(n->state(), pr)) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
|
@ -1066,12 +1099,14 @@ namespace pdr {
|
|||
continue;
|
||||
}
|
||||
proof_ref rl(m);
|
||||
expr_ref fml0(m);
|
||||
expr_ref_vector binding(m);
|
||||
n->mk_instantiate(r0, r1, binding);
|
||||
r0->to_formula(fml0);
|
||||
proof_ref p1(m), p2(m);
|
||||
p1 = m.mk_asserted(fml0);
|
||||
p1 = r0->get_proof();
|
||||
if (!p1) {
|
||||
r0->display(dctx, std::cout);
|
||||
}
|
||||
SASSERT(p1);
|
||||
pfs[0] = p1;
|
||||
rls[0] = r1;
|
||||
TRACE("pdr",
|
||||
|
|
|
@ -240,6 +240,7 @@ namespace pdr {
|
|||
void erase_leaf(model_node& n);
|
||||
void remove_node(model_node& n);
|
||||
void enqueue_leaf(model_node& n); // add leaf to priority queue.
|
||||
void update_models();
|
||||
public:
|
||||
model_search(bool bfs): m_bfs(bfs), m_root(0) {}
|
||||
~model_search();
|
||||
|
@ -253,8 +254,8 @@ namespace pdr {
|
|||
void set_root(model_node* n);
|
||||
model_node& get_root() const { return *m_root; }
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
expr_ref get_trace(context const& ctx) const;
|
||||
proof_ref get_proof_trace(context const& ctx) const;
|
||||
expr_ref get_trace(context const& ctx);
|
||||
proof_ref get_proof_trace(context const& ctx);
|
||||
void backtrack_level(bool uses_level, model_node& n);
|
||||
};
|
||||
|
||||
|
@ -299,7 +300,7 @@ namespace pdr {
|
|||
decl2rel m_rels; // Map from relation predicate to fp-operator.
|
||||
func_decl_ref m_query_pred;
|
||||
pred_transformer* m_query;
|
||||
model_search m_search;
|
||||
mutable model_search m_search;
|
||||
lbool m_last_result;
|
||||
unsigned m_inductive_lvl;
|
||||
ptr_vector<core_generalizer> m_core_generalizers;
|
||||
|
|
|
@ -85,6 +85,7 @@ lbool dl_interface::query(expr * query) {
|
|||
m_pred2slice.reset();
|
||||
ast_manager& m = m_ctx.get_manager();
|
||||
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
|
||||
|
||||
datalog::rule_set old_rules(m_ctx.get_rules());
|
||||
func_decl_ref query_pred(m);
|
||||
datalog::rule_ref_vector query_rules(rule_manager);
|
||||
|
@ -112,8 +113,13 @@ lbool dl_interface::query(expr * query) {
|
|||
m_ctx.display_rules(tout);
|
||||
);
|
||||
|
||||
<<<<<<< HEAD
|
||||
m_ctx.set_output_predicate(query_pred);
|
||||
|
||||
=======
|
||||
|
||||
m_ctx.set_output_predicate(query_pred);
|
||||
>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
|
||||
m_ctx.apply_default_transformation();
|
||||
|
||||
if (m_ctx.get_params().slice()) {
|
||||
|
@ -141,10 +147,19 @@ lbool dl_interface::query(expr * query) {
|
|||
transf1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
|
||||
transf2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
|
||||
if (m_ctx.get_params().coalesce_rules()) {
|
||||
<<<<<<< HEAD
|
||||
m_ctx.transform_rules(transf1);
|
||||
=======
|
||||
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
|
||||
m_ctx.transform_rules(transformer1);
|
||||
>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
|
||||
}
|
||||
while (num_unfolds > 0) {
|
||||
<<<<<<< HEAD
|
||||
m_ctx.transform_rules(transf2);
|
||||
=======
|
||||
m_ctx.transform_rules(transformer2);
|
||||
>>>>>>> 26f4d3be202606ff0189aefc103de187caf06d5d
|
||||
--num_unfolds;
|
||||
}
|
||||
}
|
||||
|
@ -168,8 +183,8 @@ lbool dl_interface::query(expr * query) {
|
|||
|
||||
datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode.
|
||||
|
||||
m_context->set_proof_converter(pc);
|
||||
m_context->set_model_converter(mc);
|
||||
m_context->set_proof_converter(m_ctx.get_proof_converter());
|
||||
m_context->set_model_converter(m_ctx.get_model_converter());
|
||||
m_context->set_query(query_pred);
|
||||
m_context->set_axioms(bg_assertion);
|
||||
m_context->update_rules(m_pdr_rules);
|
||||
|
|
|
@ -228,11 +228,13 @@ namespace pdr {
|
|||
is_lower = !is_lower;
|
||||
}
|
||||
|
||||
vector<term_loc_t> bound;
|
||||
bound.push_back(std::make_pair(x, i));
|
||||
if (is_lower) {
|
||||
m_lb.insert(abs(r), std::make_pair(x, i));
|
||||
m_lb.insert(abs(r), bound);
|
||||
}
|
||||
else {
|
||||
m_ub.insert(abs(r), std::make_pair(x, i));
|
||||
m_ub.insert(abs(r), bound);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -612,8 +612,8 @@ namespace pdr {
|
|||
datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
|
||||
for (; it != end; ++it) {
|
||||
datalog::rule* r = *it;
|
||||
datalog::var_counter vc(true);
|
||||
unsigned max_var = vc.get_max_var(*r);
|
||||
datalog::rule_counter vc(true);
|
||||
unsigned max_var = vc.get_max_rule_var(*r);
|
||||
app_ref_vector body(m);
|
||||
for (unsigned i = 0; i < m_instantiations.size(); ++i) {
|
||||
if (r == m_instantiated_rules[i]) {
|
||||
|
|
|
@ -2492,7 +2492,13 @@ class qe_lite_tactic : public tactic {
|
|||
new_f = f;
|
||||
m_qe(new_f, new_pr);
|
||||
if (produce_proofs) {
|
||||
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
|
||||
expr* fact = m.get_fact(new_pr);
|
||||
if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) {
|
||||
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
|
||||
}
|
||||
else {
|
||||
new_pr = g->pr(i);
|
||||
}
|
||||
}
|
||||
g->update(i, new_f, new_pr, g->dep(i));
|
||||
}
|
||||
|
|
|
@ -317,7 +317,7 @@ namespace tb {
|
|||
for (unsigned i = utsz; i < tsz; ++i) {
|
||||
fmls.push_back(r->get_tail(i));
|
||||
}
|
||||
m_num_vars = 1 + r.get_manager().get_var_counter().get_max_var(*r);
|
||||
m_num_vars = 1 + r.get_manager().get_counter().get_max_rule_var(*r);
|
||||
m_head = r->get_head();
|
||||
m_predicates.reset();
|
||||
for (unsigned i = 0; i < utsz; ++i) {
|
||||
|
@ -1644,9 +1644,7 @@ namespace datalog {
|
|||
void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2,
|
||||
expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const {
|
||||
unsigned idx = r1.get_predicate_index();
|
||||
expr_ref fml1 = r1.to_formula();
|
||||
expr_ref fml2 = r2.to_formula();
|
||||
expr_ref fml3 = res.to_formula();
|
||||
expr_ref fml = res.to_formula();
|
||||
vector<expr_ref_vector> substs;
|
||||
svector<std::pair<unsigned, unsigned> > positions;
|
||||
substs.push_back(s1);
|
||||
|
@ -1654,13 +1652,12 @@ namespace datalog {
|
|||
scoped_proof _sc(m);
|
||||
proof_ref pr(m);
|
||||
proof_ref_vector premises(m);
|
||||
premises.push_back(m.mk_asserted(fml1));
|
||||
premises.push_back(m.mk_asserted(fml2));
|
||||
premises.push_back(m.mk_asserted(r1.to_formula()));
|
||||
premises.push_back(m.mk_asserted(r2.to_formula()));
|
||||
positions.push_back(std::make_pair(idx+1, 0));
|
||||
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
|
||||
pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs);
|
||||
pc.insert(pr);
|
||||
}
|
||||
|
||||
}
|
||||
};
|
||||
|
||||
tab::tab(context& ctx):
|
||||
|
|
|
@ -276,12 +276,35 @@ static void tst_bv_reset() {
|
|||
}
|
||||
}
|
||||
|
||||
static void tst_eq() {
|
||||
bit_vector b1, b2, b3;
|
||||
b1.resize(32);
|
||||
b2.resize(32);
|
||||
b3.resize(32);
|
||||
|
||||
b1.set(3, true);
|
||||
SASSERT(b1 != b2);
|
||||
SASSERT(!(b1 == b2));
|
||||
SASSERT(b2 == b3);
|
||||
|
||||
b3.set(3, true);
|
||||
SASSERT(b1 == b3);
|
||||
SASSERT(!(b1 != b3));
|
||||
|
||||
b2.set(31, true);
|
||||
b3.set(31);
|
||||
b3.unset(3);
|
||||
SASSERT(b2 == b3);
|
||||
SASSERT(!(b2 != b3));
|
||||
}
|
||||
|
||||
void tst_bit_vector() {
|
||||
tst_crash();
|
||||
tst_shift();
|
||||
tst_or();
|
||||
tst_and();
|
||||
tst_bv_reset();
|
||||
tst_eq();
|
||||
return;
|
||||
tst2();
|
||||
for (unsigned i = 0; i < 20; i++) {
|
||||
|
|
|
@ -116,7 +116,7 @@ void bit_vector::shift_right(unsigned k) {
|
|||
}
|
||||
}
|
||||
|
||||
bool bit_vector::operator==(bit_vector const & source) {
|
||||
bool bit_vector::operator==(bit_vector const & source) const {
|
||||
if (m_num_bits != source.m_num_bits)
|
||||
return false;
|
||||
unsigned n = num_words();
|
||||
|
@ -129,6 +129,7 @@ bool bit_vector::operator==(bit_vector const & source) {
|
|||
}
|
||||
unsigned bit_rest = source.m_num_bits % 32;
|
||||
unsigned mask = (1 << bit_rest) - 1;
|
||||
if (mask == 0) mask = UINT_MAX;
|
||||
return (m_data[i] & mask) == (source.m_data[i] & mask);
|
||||
}
|
||||
|
||||
|
|
|
@ -171,9 +171,9 @@ public:
|
|||
resize(sz, val);
|
||||
}
|
||||
|
||||
bool operator==(bit_vector const & other);
|
||||
bool operator==(bit_vector const & other) const;
|
||||
|
||||
bool operator!=(bit_vector const & other) { return !operator==(other); }
|
||||
bool operator!=(bit_vector const & other) const { return !operator==(other); }
|
||||
|
||||
bit_vector & operator=(bit_vector const & source) {
|
||||
m_num_bits = source.m_num_bits;
|
||||
|
|
|
@ -151,23 +151,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
vector(T const & e) :
|
||||
m_data(0) {
|
||||
push_back(e);
|
||||
}
|
||||
|
||||
vector(T const & t1, T const & t2) :
|
||||
m_data(0) {
|
||||
push_back(t1);
|
||||
push_back(t2);
|
||||
}
|
||||
|
||||
vector(T const & t1, T const & t2, T const & t3) :
|
||||
m_data(0) {
|
||||
push_back(t1);
|
||||
push_back(t2);
|
||||
push_back(t3);
|
||||
}
|
||||
|
||||
~vector() {
|
||||
destroy();
|
||||
|
|
Loading…
Reference in a new issue