mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Added unsat core support to the macro-finder.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-08-25 20:21:57 +01:00
parent 31496b6625
commit b8a81bcb09
11 changed files with 169 additions and 125 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/ast/macros/macro_finder.cpp
View file

@ -32,27 +32,27 @@ bool macro_finder::is_macro(expr * n, app_ref & head, expr_ref & def) {
}
/**
\brief Detect macros of the form
\brief Detect macros of the form
1- (forall (X) (= (+ (f X) (R X)) c))
2- (forall (X) (<= (+ (f X) (R X)) c))
3- (forall (X) (>= (+ (f X) (R X)) c))
The second and third cases are first converted into
(forall (X) (= (f X) (+ c (* -1 (R x)) (k X))))
and
and
(forall (X) (<= (k X) 0)) when case 2
(forall (X) (>= (k X) 0)) when case 3
For case 2 & 3, the new quantifiers are stored in new_exprs and new_prs.
*/
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
if (!is_quantifier(n) || !to_quantifier(n)->is_forall())
return false;
arith_simplifier_plugin * as = get_arith_simp();
arith_util & autil = as->get_arith_util();
expr * body = to_quantifier(n)->get_expr();
unsigned num_decls = to_quantifier(n)->get_num_decls();
if (!autil.is_le(body) && !autil.is_ge(body) && !m_manager.is_eq(body))
return false;
if (!as->is_add(to_app(body)->get_arg(0)))
@ -63,7 +63,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
if (!m_util.is_arith_macro(body, num_decls, head, def, inv))
return false;
app_ref new_body(m_manager);
if (!inv || m_manager.is_eq(body))
new_body = m_manager.mk_app(to_app(body)->get_decl(), head, def);
else if (as->is_le(body))
@ -71,18 +71,19 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
else
new_body = autil.mk_le(head, def);
quantifier_ref new_q(m_manager);
quantifier_ref new_q(m_manager);
new_q = m_manager.update_quantifier(to_quantifier(n), new_body);
proof * new_pr = 0;
if (m_manager.proofs_enabled()) {
proof * rw = m_manager.mk_rewrite(n, new_q);
new_pr = m_manager.mk_modus_ponens(pr, rw);
}
expr_dependency * new_dep = dep;
if (m_manager.is_eq(body)) {
return m_macro_manager.insert(head->get_decl(), new_q, new_pr);
return m_macro_manager.insert(head->get_decl(), new_q, new_pr, new_dep);
}
// is ge or le
//
//
TRACE("macro_finder", tout << "is_arith_macro: is_ge or is_le\n";);
func_decl * f = head->get_decl();
func_decl * k = m_manager.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
@ -111,6 +112,10 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
new_prs.push_back(pr1);
new_prs.push_back(pr2);
}
if (dep) {
new_deps.push_back(new_dep);
new_deps.push_back(new_dep);
}
return true;
}
@ -118,7 +123,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
n is of the form: (forall (X) (iff (= (f X) t) def[X]))
Convert it into:
(forall (X) (= (f X) (ite def[X] t (k X))))
(forall (X) (not (= (k X) t)))
@ -126,13 +131,13 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_ex
The new quantifiers and proofs are stored in new_exprs and new_prs
*/
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, expr * def, quantifier * q, proof * pr, expr_dependency * dep,
expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps ) {
func_decl * f = head->get_decl();
func_decl * k = m.mk_fresh_func_decl(f->get_name(), symbol::null, f->get_arity(), f->get_domain(), f->get_range());
app * k_app = m.mk_app(k, head->get_num_args(), head->get_args());
app * ite = m.mk_ite(def, t, k_app);
app * body_1 = m.mk_eq(head, ite);
app * body_1 = m.mk_eq(head, ite);
app * body_2 = m.mk_not(m.mk_eq(k_app, t));
quantifier * q1 = m.update_quantifier(q, body_1);
expr * pats[1] = { m.mk_pattern(k_app) };
@ -153,6 +158,8 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
new_prs.push_back(pr1);
new_prs.push_back(pr2);
}
new_deps.push_back(dep);
new_deps.push_back(dep);
}
macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
@ -164,57 +171,67 @@ macro_finder::macro_finder(ast_manager & m, macro_manager & mm):
macro_finder::~macro_finder() {
}
bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "starting expand_macros:\n";
m_macro_manager.display(tout););
bool found_new_macro = false;
for (unsigned i = 0; i < num; i++) {
expr * n = exprs[i];
proof * pr = m_manager.proofs_enabled() ? prs[i] : 0;
expr_dependency * depi = deps != 0 ? deps[i] : 0;
expr_ref new_n(m_manager), def(m_manager);
proof_ref new_pr(m_manager);
m_macro_manager.expand_macros(n, pr, new_n, new_pr);
expr_dependency_ref new_dep(m_manager);
m_macro_manager.expand_macros(n, pr, depi, new_n, new_pr, new_dep);
app_ref head(m_manager), t(m_manager);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr, new_dep)) {
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);
found_new_macro = true;
}
else if (is_arith_macro(new_n, new_pr, new_exprs, new_prs)) {
else if (is_arith_macro(new_n, new_pr, new_dep, new_exprs, new_prs, new_deps)) {
TRACE("macro_finder_found", tout << "found new arith macro:\n" << new_n << "\n";);
found_new_macro = true;
}
else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
else if (m_util.is_pseudo_predicate_macro(new_n, head, t, def)) {
TRACE("macro_finder_found", tout << "found new pseudo macro:\n" << head << "\n" << t << "\n" << def << "\n";);
pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_exprs, new_prs);
pseudo_predicate_macro2macro(m_manager, head, t, def, to_quantifier(new_n), new_pr, new_dep, new_exprs, new_prs, new_deps);
found_new_macro = true;
}
else {
new_exprs.push_back(new_n);
if (m_manager.proofs_enabled())
new_prs.push_back(new_pr);
if (deps != 0)
new_deps.push_back(new_dep);
}
}
return found_new_macro;
}
void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
void macro_finder::operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
TRACE("macro_finder", tout << "processing macros...\n";);
expr_ref_vector _new_exprs(m_manager);
proof_ref_vector _new_prs(m_manager);
if (expand_macros(num, exprs, prs, _new_exprs, _new_prs)) {
expr_dependency_ref_vector _new_deps(m_manager);
if (expand_macros(num, exprs, prs, deps, _new_exprs, _new_prs, _new_deps)) {
while (true) {
expr_ref_vector old_exprs(m_manager);
proof_ref_vector old_prs(m_manager);
expr_dependency_ref_vector old_deps(m_manager);
_new_exprs.swap(old_exprs);
_new_prs.swap(old_prs);
_new_deps.swap(old_deps);
SASSERT(_new_exprs.empty());
SASSERT(_new_prs.empty());
if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), _new_exprs, _new_prs))
SASSERT(_new_deps.empty());
if (!expand_macros(old_exprs.size(), old_exprs.c_ptr(), old_prs.c_ptr(), old_deps.c_ptr(),
_new_exprs, _new_prs, _new_deps))
break;
}
}
new_exprs.append(_new_exprs);
new_prs.append(_new_prs);
new_deps.append(_new_deps);
}

17
src/ast/macros/macro_finder.h
View file

@ -23,32 +23,23 @@ Revision History:
#include "ast/simplifier/arith_simplifier_plugin.h"
bool is_macro_head(expr * n, unsigned num_decls);
bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, obj_hashtable<func_decl> const * forbidden_set, app * & head, expr * & def);
inline bool is_simple_macro(ast_manager & m, expr * n, unsigned num_decls, app * & head, expr * & def) {
return is_simple_macro(m, n, num_decls, 0, head, def);
}
/**
\brief Macro finder is responsible for finding universally quantified sub-formulas that can be used
as macros.
*/
class macro_finder {
ast_manager & m_manager;
ast_manager & m_manager;
macro_manager & m_macro_manager;
macro_util & m_util;
arith_simplifier_plugin * get_arith_simp() { return m_util.get_arith_simp(); }
bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool is_arith_macro(expr * n, proof * pr, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool expand_macros(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
bool is_arith_macro(expr * n, proof * pr, expr_dependency * dep, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
bool is_macro(expr * n, app_ref & head, expr_ref & def);
bool is_pseudo_head(expr * n, unsigned num_decls, app * & head, app * & t);
bool is_pseudo_predicate_macro(expr * n, app * & head, app * & t, expr * & def);
public:
macro_finder(ast_manager & m, macro_manager & mm);
~macro_finder();
void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
void operator()(unsigned num, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
};
#endif /* MACRO_FINDER_H_ */

26
src/ast/macros/macro_manager.cpp
View file

@ -25,13 +25,14 @@ Revision History:
#include "ast/ast_pp.h"
#include "ast/recurse_expr_def.h"
macro_manager::macro_manager(ast_manager & m, simplifier & s):
macro_manager::macro_manager(ast_manager & m, simplifier & s) :
m_manager(m),
m_simplifier(s),
m_util(m, s),
m_decls(m),
m_macros(m),
m_macro_prs(m),
m_macro_deps(m),
m_forbidden(m),
m_deps(m) {
m_util.set_forbidden_set(&m_forbidden_set);
@ -60,13 +61,16 @@ void macro_manager::restore_decls(unsigned old_sz) {
for (unsigned i = old_sz; i < sz; i++) {
m_decl2macro.erase(m_decls.get(i));
m_deps.erase(m_decls.get(i));
if (m_manager.proofs_enabled())
if (m_manager.proofs_enabled()) {
m_decl2macro_pr.erase(m_decls.get(i));
m_decl2macro_dep.erase(m_decls.get(i));
}
}
m_decls.shrink(old_sz);
m_macros.shrink(old_sz);
if (m_manager.proofs_enabled())
m_macro_prs.shrink(old_sz);
m_macro_deps.shrink(old_sz);
}
void macro_manager::restore_forbidden(unsigned old_sz) {
@ -79,16 +83,18 @@ void macro_manager::restore_forbidden(unsigned old_sz) {
void macro_manager::reset() {
m_decl2macro.reset();
m_decl2macro_pr.reset();
m_decl2macro_dep.reset();
m_decls.reset();
m_macros.reset();
m_macro_prs.reset();
m_macro_deps.reset();
m_scopes.reset();
m_forbidden_set.reset();
m_forbidden.reset();
m_deps.reset();
}
bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) {
TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(m, m_manager) << "\n";);
// if we already have a macro for f then return false;
@ -115,6 +121,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
m_macro_prs.push_back(pr);
m_decl2macro_pr.insert(f, pr);
}
m_macro_deps.push_back(dep);
m_decl2macro_dep.insert(f, dep);
TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
@ -195,7 +203,8 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
macro_manager::macro_expander::macro_expander(ast_manager & m, macro_manager & mm, simplifier & s):
simplifier(m),
m_macro_manager(mm) {
m_macro_manager(mm),
m_used_macro_dependencies(m) {
// REMARK: theory simplifier should not be used by macro_expander...
// is_arith_macro rewrites a quantifer such as:
// forall (x Int) (= (+ x (+ (f x) 1)) 2)
@ -286,34 +295,41 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
}
else {
p = 0;
expr_dependency * ed = m_macro_manager.m_decl2macro_dep.find(d);
m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed);
}
return true;
}
return false;
}
void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr) {
void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep) {
if (has_macros()) {
// Expand macros with "real" proof production support (NO rewrite*)
expr_ref old_n(m_manager);
proof_ref old_pr(m_manager);
expr_dependency_ref old_dep(m_manager);
old_n = n;
old_pr = pr;
old_dep = dep;
for (;;) {
macro_expander proc(m_manager, *this, m_simplifier);
proof_ref n_eq_r_pr(m_manager);
TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m_manager) << "\n";);
proc(old_n, r, n_eq_r_pr);
new_pr = m_manager.mk_modus_ponens(old_pr, n_eq_r_pr);
new_dep = m_manager.mk_join(old_dep, proc.m_used_macro_dependencies);
if (r.get() == old_n.get())
return;
old_n = r;
old_pr = new_pr;
old_dep = new_dep;
}
}
else {
r = n;
new_pr = pr;
new_dep = dep;
}
}

7
src/ast/macros/macro_manager.h
View file

@ -42,9 +42,11 @@ class macro_manager {
obj_map<func_decl, quantifier *> m_decl2macro; // func-decl -> quantifier
obj_map<func_decl, proof *> m_decl2macro_pr; // func-decl -> quantifier_proof
obj_map<func_decl, expr_dependency *> m_decl2macro_dep; // func-decl -> unsat core dependency
func_decl_ref_vector m_decls;
quantifier_ref_vector m_macros;
proof_ref_vector m_macro_prs;
expr_dependency_ref_vector m_macro_deps;
obj_hashtable<func_decl> m_forbidden_set;
func_decl_ref_vector m_forbidden;
struct scope {
@ -64,6 +66,7 @@ class macro_manager {
virtual bool get_subst(expr * n, expr_ref & r, proof_ref & p);
virtual void reduce1_quantifier(quantifier * q);
public:
expr_dependency_ref m_used_macro_dependencies;
macro_expander(ast_manager & m, macro_manager & mm, simplifier & s);
~macro_expander();
};
@ -74,7 +77,7 @@ public:
~macro_manager();
ast_manager & get_manager() const { return m_manager; }
macro_util & get_util() { return m_util; }
bool insert(func_decl * f, quantifier * m, proof * pr);
bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep);
bool has_macros() const { return !m_macros.empty(); }
void push_scope();
void pop_scope(unsigned num_scopes);
@ -90,7 +93,7 @@ public:
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; }
void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
void expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref & new_pr);
void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
};

29
src/ast/macros/quasi_macros.cpp
View file

@ -264,17 +264,16 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
// Find out how many non-ground appearences for each uninterpreted function there are
for ( unsigned i = 0 ; i < n ; i++ )
for (unsigned i = 0 ; i < n ; i++)
find_occurrences(exprs[i]);
TRACE("quasi_macros", tout << "Occurrences: " << std::endl;
for (occurrences_map::iterator it = m_occurrences.begin();
it != m_occurrences.end();
it++)
tout << it->m_key->get_name() << ": " << it->m_value << std::endl; );
TRACE("quasi_macros",
tout << "Occurrences: " << std::endl;
for (auto & kd : m_occurrences)
tout << kd.m_key->get_name() << ": " << kd.m_value << std::endl; );
// Find all macros
for ( unsigned i = 0 ; i < n ; i++ ) {
for (unsigned i = 0 ; i < n ; i++) {
app_ref a(m_manager);
expr_ref t(m_manager);
if (is_quasi_macro(exprs[i], a, t)) {
@ -285,7 +284,8 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
proof * pr = 0;
if (m_manager.proofs_enabled())
pr = m_manager.mk_def_axiom(macro);
if (m_macro_manager.insert(a->get_decl(), macro, pr))
expr_dependency * dep = 0;
if (m_macro_manager.insert(a->get_decl(), macro, pr, dep))
res = true;
}
}
@ -293,21 +293,24 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
return res;
}
void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
for ( unsigned i = 0 ; i < n ; i++ ) {
void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
for (unsigned i = 0 ; i < n ; i++) {
expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager);
proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
m_macro_manager.expand_macros(exprs[i], p, r, pr);
expr_dependency * dep = deps[i];
expr_dependency_ref new_dep(m_manager);
m_macro_manager.expand_macros(exprs[i], p, dep, r, pr, new_dep);
m_simplifier(r, rs, ps);
new_exprs.push_back(rs);
new_prs.push_back(ps);
new_deps.push_back(new_dep);
}
}
bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) {
bool quasi_macros::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps) {
if (find_macros(n, exprs)) {
apply_macros(n, exprs, prs, new_exprs, new_prs);
apply_macros(n, exprs, prs, deps, new_exprs, new_prs, new_deps);
return true;
} else {
// just copy them over

4
src/ast/macros/quasi_macros.h
View file

@ -54,7 +54,7 @@ class quasi_macros {
void find_occurrences(expr * e);
bool find_macros(unsigned n, expr * const * exprs);
void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
public:
quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
@ -63,7 +63,7 @@ public:
/**
\brief Find pure function macros and apply them.
*/
bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_dependency * const * deps, expr_ref_vector & new_exprs, proof_ref_vector & new_prs, expr_dependency_ref_vector & new_deps);
};
#endif

70
src/smt/asserted_formulas.cpp
View file

@ -75,7 +75,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
void asserted_formulas::setup() {
switch (m_params.m_lift_ite) {
case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE;
m_params.m_ng_lift_ite = LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
@ -84,7 +84,7 @@ void asserted_formulas::setup() {
default:
break;
}
if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false;
}
@ -97,7 +97,7 @@ void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifie
s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params);
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp));
}
@ -140,7 +140,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
if (inconsistent())
if (inconsistent())
return;
if (!m_params.m_preprocess) {
push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs);
@ -175,7 +175,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
}
void asserted_formulas::assert_expr(expr * e) {
if (inconsistent())
if (inconsistent())
return;
assert_expr(e, m.mk_asserted(e));
}
@ -197,7 +197,7 @@ void asserted_formulas::push_scope() {
m_bv_sharing.push_scope();
commit();
}
void asserted_formulas::pop_scope(unsigned num_scopes) {
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
m_bv_sharing.pop_scope(num_scopes);
@ -228,15 +228,15 @@ void asserted_formulas::reset() {
#ifdef Z3DEBUG
bool asserted_formulas::check_well_sorted() const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false;
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false;
}
return true;
}
#endif
void asserted_formulas::reduce() {
if (inconsistent())
if (inconsistent())
return;
if (canceled()) {
return;
@ -253,7 +253,7 @@ void asserted_formulas::reduce() {
#define INVOKE(COND, FUNC) if (COND) { FUNC; IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); } TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); TRACE("reduce_step", display(tout << #FUNC << " ");); CASSERT("well_sorted",check_well_sorted()); if (inconsistent() || canceled()) { TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return; }
set_eliminate_and(false); // do not eliminate and before nnf.
INVOKE(m_params.m_propagate_booleans, propagate_booleans());
INVOKE(m_params.m_propagate_values, propagate_values());
@ -266,18 +266,18 @@ void asserted_formulas::reduce() {
INVOKE(m_params.m_lift_ite != LI_NONE, lift_ite());
INVOKE(m_params.m_eliminate_term_ite && m_params.m_lift_ite != LI_FULL, eliminate_term_ite());
INVOKE(m_params.m_refine_inj_axiom && has_quantifiers(), refine_inj_axiom());
INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall());
TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout););
INVOKE(m_params.m_distribute_forall && has_quantifiers(), apply_distribute_forall());
TRACE("qbv_bug", tout << "after distribute_forall:\n"; display(tout););
INVOKE(m_params.m_macro_finder && has_quantifiers(), find_macros());
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
INVOKE(m_params.m_ematching && has_quantifiers(), infer_patterns());
INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
// temporary HACK: make sure that arith & bv are list-assoc
// temporary HACK: make sure that arith & bv are list-assoc
// this may destroy some simplification steps such as max_bv_sharing
reduce_asserted_formulas();
reduce_asserted_formulas();
CASSERT("well_sorted",check_well_sorted());
@ -291,7 +291,7 @@ void asserted_formulas::reduce() {
void asserted_formulas::eliminate_and() {
IF_IVERBOSE(10, verbose_stream() << "(smt.eliminating-and)\n";);
set_eliminate_and(true);
reduce_asserted_formulas();
reduce_asserted_formulas();
TRACE("after_elim_and", display(tout););
}
@ -331,10 +331,10 @@ void asserted_formulas::display(std::ostream & out) const {
void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
if (!m_asserted_formulas.empty()) {
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++)
for (unsigned i = 0; i < sz; i++)
ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false);
out << "asserted formulas:\n";
for (unsigned i = 0; i < sz; i++)
for (unsigned i = 0; i < sz; i++)
out << "#" << m_asserted_formulas[i]->get_id() << " ";
out << "\n";
}
@ -387,8 +387,12 @@ void asserted_formulas::find_macros_core() {
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned sz = m_asserted_formulas.size();
m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
expr_dependency_ref_vector new_deps(m);
m_macro_finder->operator()(sz - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
0, // 0 == No dependency tracking
new_exprs, new_prs, new_deps);
swap_asserted_formulas(new_exprs, new_prs);
reduce_and_solve();
}
@ -409,12 +413,14 @@ void asserted_formulas::apply_quasi_macros() {
IF_IVERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
TRACE("before_quasi_macros", display(tout););
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
quasi_macros proc(m, m_macro_manager, m_simplifier);
while (proc(m_asserted_formulas.size() - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
proof_ref_vector new_prs(m);
quasi_macros proc(m, m_macro_manager, m_simplifier);
expr_dependency_ref_vector new_deps(m);
while (proc(m_asserted_formulas.size() - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
new_exprs, new_prs)) {
0, // 0 == No dependency tracking
new_exprs, new_prs, new_deps)) {
swap_asserted_formulas(new_exprs, new_prs);
new_exprs.reset();
new_prs.reset();
@ -430,7 +436,7 @@ void asserted_formulas::nnf_cnf() {
proof_ref_vector new_prs(m);
expr_ref_vector push_todo(m);
proof_ref_vector push_todo_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
@ -460,8 +466,8 @@ void asserted_formulas::nnf_cnf() {
CASSERT("well_sorted",is_well_sorted(m, r1));
if (canceled()) {
return;
}
}
if (m.proofs_enabled())
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
else
@ -598,7 +604,7 @@ void asserted_formulas::propagate_values() {
// C is a set which contains formulas of the form
// { x = n }, where x is a variable and n a numeral.
// R contains the rest.
//
//
// - new_exprs1 is the set C
// - new_exprs2 is the set R
//
@ -663,7 +669,7 @@ void asserted_formulas::propagate_values() {
// x->n will be removed from m_cache. If we don't do that, the next transformation
// may simplify constraints in C using these entries, and the variables x in C
// will be (silently) eliminated, and models produced by Z3 will not contain them.
flush_cache();
flush_cache();
}
TRACE("propagate_values", tout << "after:\n"; display(tout););
}
@ -786,7 +792,7 @@ void asserted_formulas::refine_inj_axiom() {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);
m_asserted_formulas.set(i, new_n);
if (m.proofs_enabled()) {
proof_ref new_pr(m);
proof_ref new_pr(m);
new_pr = m.mk_rewrite(n, new_n);
new_pr = m.mk_modus_ponens(pr, new_pr);
m_asserted_formula_prs.set(i, new_pr);
@ -860,7 +866,7 @@ void asserted_formulas::max_bv_sharing() {
}
reduce_asserted_formulas();
TRACE("bv_sharing", display(tout););
}
#ifdef Z3DEBUG

14
src/smt/asserted_formulas.h
View file

@ -49,7 +49,7 @@ class asserted_formulas {
macro_manager m_macro_manager;
scoped_ptr<macro_finder> m_macro_finder;
bit2int m_bit2int;
maximise_bv_sharing m_bv_sharing;
@ -87,7 +87,7 @@ class asserted_formulas {
bool apply_bit2int();
void lift_ite();
bool elim_bvs_from_quantifiers();
void ng_lift_ite();
void ng_lift_ite();
#ifdef Z3DEBUG
bool check_well_sorted() const;
#endif
@ -112,8 +112,8 @@ public:
unsigned get_num_formulas() const { return m_asserted_formulas.size(); }
unsigned get_formulas_last_level() const;
unsigned get_qhead() const { return m_asserted_qhead; }
void commit();
void commit(unsigned new_qhead);
void commit();
void commit(unsigned new_qhead);
expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
@ -129,7 +129,7 @@ public:
void collect_statistics(statistics & st) const;
// TODO: improve precision of the following method.
bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ }
// -----------------------------------
//
// Macros
@ -140,9 +140,7 @@ public:
func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); }
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_macro_manager.get_macro_interpretation(i, interp); }
quantifier * get_macro_quantifier(func_decl * f) const { return m_macro_manager.get_macro_quantifier(f); }
// auxiliary function used to create a logic context based on a model.
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_macro_manager.insert(f, m, pr); }
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_macro_manager.insert(f, m, pr, dep); }
};
#endif /* ASSERTED_FORMULAS_H_ */

4
src/smt/smt_context.h
View file

@ -209,7 +209,7 @@ namespace smt {
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.add_rec_funs_to_model();
m_ctx.add_rec_funs_to_model();
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}
@ -1568,7 +1568,7 @@ namespace smt {
func_decl * get_macro_func_decl(unsigned i) const { return m_asserted_formulas.get_macro_func_decl(i); }
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const { return m_asserted_formulas.get_macro_interpretation(i, interp); }
quantifier * get_macro_quantifier(func_decl * f) const { return m_asserted_formulas.get_macro_quantifier(f); }
void insert_macro(func_decl * f, quantifier * m, proof * pr) { m_asserted_formulas.insert_macro(f, m, pr); }
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
};
};

12
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -49,9 +49,9 @@ class macro_finder_tactic : public tactic {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("macro-finder", *g);
fail_if_unsat_core_generation("macro-finder", g);
bool produce_proofs = g->proofs_enabled();
bool unsat_core_enabled = g->unsat_core_enabled();
simplifier simp(m_manager);
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
@ -69,17 +69,21 @@ class macro_finder_tactic : public tactic {
expr_ref_vector forms(m_manager), new_forms(m_manager);
proof_ref_vector proofs(m_manager), new_proofs(m_manager);
unsigned size = g->size();
expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
unsigned size = g->size();
for (unsigned idx = 0; idx < size; idx++) {
forms.push_back(g->form(idx));
proofs.push_back(g->pr(idx));
deps.push_back(g->dep(idx));
}
mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
g->reset();
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
g->assert_expr(new_forms.get(i),
produce_proofs ? new_proofs.get(i) : 0,
unsat_core_enabled ? new_deps.get(i) : 0);
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();

52
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -35,22 +35,22 @@ class quasi_macros_tactic : public tactic {
imp(ast_manager & m, params_ref const & p) : m_manager(m) {
updt_params(p);
}
ast_manager & m() const { return m_manager; }
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("quasi-macros", *g);
fail_if_unsat_core_generation("quasi-macros", g);
bool produce_proofs = g->proofs_enabled();
bool produce_unsat_cores = g->unsat_core_enabled();
simplifier simp(m_manager);
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
bsimp->set_eliminate_and(true);
@ -61,34 +61,40 @@ class quasi_macros_tactic : public tactic {
bv_simplifier_params bv_params;
bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
simp.register_plugin(bvsimp);
macro_manager mm(m_manager, simp);
quasi_macros qm(m_manager, mm, simp);
bool more = true;
expr_ref_vector forms(m_manager), new_forms(m_manager);
proof_ref_vector proofs(m_manager), new_proofs(m_manager);
expr_dependency_ref_vector deps(m_manager), new_deps(m_manager);
unsigned size = g->size();
for (unsigned i = 0; i < size; i++) {
forms.push_back(g->form(i));
proofs.push_back(g->pr(i));
deps.push_back(g->dep(i));
}
while (more) { // CMW: use repeat(...) ?
if (m().canceled())
throw tactic_exception(m().limit().get_cancel_msg());
new_forms.reset();
new_proofs.reset();
more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs);
new_deps.reset();
more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), deps.c_ptr(), new_forms, new_proofs, new_deps);
forms.swap(new_forms);
proofs.swap(new_proofs);
proofs.swap(new_proofs);
deps.swap(new_deps);
}
g->reset();
for (unsigned i = 0; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0);
g->assert_expr(forms.get(i),
produce_proofs ? proofs.get(i) : 0,
produce_unsat_cores ? deps.get(i) : 0);
extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();
@ -108,7 +114,7 @@ class quasi_macros_tactic : public tactic {
void updt_params(params_ref const & p) {
}
};
imp * m_imp;
params_ref m_params;
@ -121,7 +127,7 @@ public:
virtual tactic * translate(ast_manager & m) {
return alloc(quasi_macros_tactic, m, m_params);
}
virtual ~quasi_macros_tactic() {
dealloc(m_imp);
}
@ -136,19 +142,19 @@ public:
insert_produce_models(r);
insert_produce_proofs(r);
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
(*m_imp)(in, result, mc, pc, core);
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp);
std::swap(d, m_imp);
dealloc(d);
}