mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

integrate lambda expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-26 07:23:04 -07:00
parent bf4edef761
commit 520ce9a5ee
139 changed files with 2243 additions and 1506 deletions
Download patch file Download diff file Expand all files Collapse all files

135
src/ast/normal_forms/defined_names.cpp
View file

@ -16,17 +16,19 @@ Author:
Revision History:
--*/
#include "ast/normal_forms/defined_names.h"
#include "util/obj_hashtable.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/used_vars.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/array_decl_plugin.h"
struct defined_names::impl {
typedef obj_map<expr, app *> expr2name;
typedef obj_map<expr, proof *> expr2proof;
ast_manager & m_manager;
ast_manager & m;
symbol m_z3name;
/**
@ -60,9 +62,9 @@ struct defined_names::impl {
app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
void cache_new_name(expr * e, app * name);
void cache_new_name_intro_proof(expr * e, proof * pr);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result, symbol const& qid = symbol::null);
void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result, symbol const& qid = symbol::null);
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def);
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
void push_scope();
void pop_scope(unsigned num_scopes);
@ -74,12 +76,13 @@ struct defined_names::impl {
struct defined_names::pos_impl : public defined_names::impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def) override;
void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) override;
};
defined_names::impl::impl(ast_manager & m, char const * prefix):
m_manager(m),
m(m),
m_exprs(m),
m_names(m),
m_apply_proofs(m) {
@ -107,20 +110,20 @@ app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffe
sort * s = uv.get(i);
if (s) {
domain.push_back(s);
new_args.push_back(m_manager.mk_var(i, s));
new_args.push_back(m.mk_var(i, s));
var_sorts.push_back(s);
}
else {
var_sorts.push_back(m_manager.mk_bool_sort()); // could be any sort.
var_sorts.push_back(m.mk_bool_sort()); // could be any sort.
}
var_names.push_back(symbol(i));
}
sort * range = m_manager.get_sort(e);
func_decl * new_skolem_decl = m_manager.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.c_ptr(), range);
app * n = m_manager.mk_app(new_skolem_decl, new_args.size(), new_args.c_ptr());
TRACE("mk_definition_bug", tout << "gen_name: " << mk_ismt2_pp(n, m_manager) << "\n";
for (unsigned i = 0; i < var_sorts.size(); i++) tout << mk_pp(var_sorts[i], m_manager) << " ";
sort * range = m.get_sort(e);
func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.c_ptr(), range);
app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.c_ptr());
TRACE("mk_definition_bug", tout << "gen_name: " << mk_ismt2_pp(n, m) << "\n";
for (unsigned i = 0; i < var_sorts.size(); i++) tout << mk_pp(var_sorts[i], m) << " ";
tout << "\n";);
return n;
}
@ -148,22 +151,22 @@ void defined_names::impl::cache_new_name_intro_proof(expr * e, proof * pr) {
A quantifier is added around \c def_conjunct, if sorts and names are not empty.
In this case, The application \c name is used as a pattern for the new quantifier.
*/
void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result) {
void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result, symbol const& qid) {
SASSERT(sorts.size() == names.size());
if (sorts.empty())
result = def_conjunct;
else {
expr * patterns[1] = { m_manager.mk_pattern(name) };
quantifier_ref q(m_manager);
q = m_manager.mk_forall(sorts.size(),
expr * patterns[1] = { m.mk_pattern(name) };
quantifier_ref q(m);
q = m.mk_forall(sorts.size(),
sorts.c_ptr(),
names.c_ptr(),
def_conjunct,
1, symbol::null, symbol::null,
1, qid, symbol::null,
1, patterns);
TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m_manager) << "\n";);
elim_unused_vars(m_manager, q, params_ref(), result);
TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m_manager) << "\n";);
TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m) << "\n";);
result = elim_unused_vars(m, q, params_ref());
TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << result << "\n";);
}
}
@ -172,44 +175,81 @@ void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbo
A quantifier is added around \c def_conjunct, if sorts and names are not empty.
In this case, The application \c name is used as a pattern for the new quantifier.
*/
void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result) {
expr_ref tmp(m_manager);
bound_vars(sorts, names, def_conjunct, name, tmp);
void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result, symbol const& qid) {
expr_ref tmp(m);
bound_vars(sorts, names, def_conjunct, name, tmp, qid);
result.push_back(tmp);
}
#define MK_OR m_manager.mk_or
#define MK_NOT m_manager.mk_not
#define MK_EQ m_manager.mk_eq
#define MK_OR m.mk_or
#define MK_NOT m.mk_not
#define MK_EQ m.mk_eq
void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def) {
expr_ref_buffer defs(m_manager);
if (m_manager.is_bool(e)) {
void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) {
expr_ref_buffer defs(m);
if (m.is_bool(e)) {
bound_vars(var_sorts, var_names, MK_OR(MK_NOT(n), e), n, defs);
bound_vars(var_sorts, var_names, MK_OR(n, MK_NOT(e)), n, defs);
}
else if (m_manager.is_term_ite(e)) {
else if (m.is_term_ite(e)) {
bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs);
bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0), MK_EQ(n, to_app(e)->get_arg(2))), n, defs);
}
else if (is_lambda(e)) {
// n(y) = \x . M[x,y]
// =>
// n(y)[x] = M, forall x y
//
// NB. The pattern is incomplete.
// consider store(a, i, v) == \lambda j . if i = j then v else a[j]
// the instantiation rules for store(a, i, v) are:
// sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
// The first pattern is not included.
// TBD use a model-based scheme for exracting instantiations instead of
// using multi-patterns.
//
quantifier* q = to_quantifier(e);
expr_ref_vector args(m);
expr_ref n2(m), n3(m);
var_shifter vs(m);
vs(n, q->get_num_decls(), n2);
args.push_back(n2);
var_sorts.append(q->get_num_decls(), q->get_decl_sorts());
var_names.append(q->get_num_decls(), q->get_decl_names());
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i)));
}
array_util autil(m);
func_decl * f = 0;
if (autil.is_as_array(n2, f)) {
n3 = m.mk_app(f, args.size()-1, args.c_ptr() + 1);
}
else {
n3 = autil.mk_select(args.size(), args.c_ptr());
}
bound_vars(var_sorts, var_names, MK_EQ(q->get_expr(), n3), to_app(n3), defs, m.lambda_def_qid());
}
else {
bound_vars(var_sorts, var_names, MK_EQ(e, n), n, defs);
}
new_def = defs.size() == 1 ? defs[0] : m_manager.mk_and(defs.size(), defs.c_ptr());
new_def = mk_and(m, defs.size(), defs.c_ptr());
}
void defined_names::pos_impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def) {
void defined_names::pos_impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) {
bound_vars(var_sorts, var_names, MK_OR(MK_NOT(n), e), n, new_def);
}
bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
TRACE("mk_definition_bug", tout << "making name for:\n" << mk_ismt2_pp(e, m_manager) << "\n";);
TRACE("mk_definition_bug", tout << "making name for:\n" << mk_ismt2_pp(e, m) << "\n";);
app * n_ptr;
if (m_expr2name.find(e, n_ptr)) {
TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
n = n_ptr;
if (m_manager.proofs_enabled()) {
if (m.proofs_enabled()) {
proof * pr_ptr = nullptr;
m_expr2proof.find(e, pr_ptr);
SASSERT(pr_ptr);
@ -218,24 +258,24 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
return false;
}
else {
sort_ref_buffer var_sorts(m_manager);
sort_ref_buffer var_sorts(m);
buffer<symbol> var_names;
n = gen_name(e, var_sorts, var_names);
cache_new_name(e, n);
TRACE("mk_definition_bug", tout << "name: " << mk_ismt2_pp(n, m_manager) << "\n";);
TRACE("mk_definition_bug", tout << "name: " << mk_ismt2_pp(n, m) << "\n";);
// variables are in reverse order in quantifiers
std::reverse(var_sorts.c_ptr(), var_sorts.c_ptr() + var_sorts.size());
std::reverse(var_names.c_ptr(), var_names.c_ptr() + var_names.size());
mk_definition(e, n, var_sorts, var_names, new_def);
TRACE("mk_definition_bug", tout << "new_def:\n" << mk_ismt2_pp(new_def, m_manager) << "\n";);
TRACE("mk_definition_bug", tout << "new_def:\n" << mk_ismt2_pp(new_def, m) << "\n";);
if (m_manager.proofs_enabled()) {
new_def_pr = m_manager.mk_def_intro(new_def);
pr = m_manager.mk_apply_def(e, n, new_def_pr);
if (m.proofs_enabled()) {
new_def_pr = m.mk_def_intro(new_def);
pr = m.mk_apply_def(e, n, new_def_pr);
cache_new_name_intro_proof(e, pr);
}
return true;
@ -257,7 +297,7 @@ void defined_names::impl::pop_scope(unsigned num_scopes) {
SASSERT(sz == m_names.size());
while (old_sz != sz) {
--sz;
if (m_manager.proofs_enabled()) {
if (m.proofs_enabled()) {
m_expr2proof.erase(m_exprs.back());
m_apply_proofs.pop_back();
}
@ -296,6 +336,15 @@ bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_de
return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr);
}
expr_ref defined_names::mk_definition(expr * e, app * n) {
ast_manager& m = m_impl->m;
sort_ref_buffer var_sorts(m);
expr_ref new_def(m);
buffer<symbol> var_names;
m_impl->mk_definition(e, n, var_sorts, var_names, new_def);
return new_def;
}
void defined_names::push() {
m_impl->push_scope();
m_pos_impl->push_scope();

5
src/ast/normal_forms/defined_names.h
View file

@ -77,6 +77,11 @@ public:
*/
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
/**
\brief Create a definition for 'n' using 'e'.
*/
expr_ref mk_definition(expr * e, app * n);
void push();
void pop(unsigned num_scopes);
void reset();

30
src/ast/normal_forms/name_exprs.cpp
View file

@ -22,7 +22,7 @@ Notes:
class name_exprs_core : public name_exprs {
struct cfg : public default_rewriter_cfg {
ast_manager & m_manager;
ast_manager & m;
defined_names & m_defined_names;
expr_predicate & m_pred;
@ -33,7 +33,7 @@ class name_exprs_core : public name_exprs {
proof_ref_vector * m_def_proofs;
cfg(ast_manager & m, defined_names & n, expr_predicate & pred):
m_manager(m),
m(m),
m_defined_names(n),
m_pred(pred),
m_r(m),
@ -43,12 +43,12 @@ class name_exprs_core : public name_exprs {
}
void gen_name_for_expr(expr * n, expr * & t, proof * & t_pr) {
expr_ref new_def(m_manager);
proof_ref new_def_pr(m_manager);
expr_ref new_def(m);
proof_ref new_def_pr(m);
if (m_defined_names.mk_name(n, new_def, new_def_pr, m_r, m_pr)) {
m_def_exprs->push_back(new_def);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
m_def_proofs->push_back(new_def_pr);
}
@ -57,7 +57,7 @@ class name_exprs_core : public name_exprs {
}
bool get_subst(expr * s, expr * & t, proof * & t_pr) {
TRACE("name_exprs", tout << "get_subst:\n" << mk_ismt2_pp(s, m_manager) << "\n";);
TRACE("name_exprs", tout << "get_subst:\n" << mk_ismt2_pp(s, m) << "\n";);
if (m_pred(s)) {
gen_name_for_expr(s, t, t_pr);
return true;
@ -84,7 +84,7 @@ public:
m_cfg.m_def_exprs = &new_defs;
m_cfg.m_def_proofs = &new_def_proofs;
m_rw(n, r, p);
TRACE("name_exprs", tout << mk_ismt2_pp(n, m_rw.m()) << "\n---->\n" << mk_ismt2_pp(r, m_rw.m()) << "\n";);
TRACE("name_exprs", tout << mk_ismt2_pp(n, m_rw.m()) << "\n---->\n" << r << "\n";);
}
@ -99,11 +99,11 @@ name_exprs * mk_expr_namer(ast_manager & m, defined_names & n, expr_predicate &
class name_quantifier_labels : public name_exprs_core {
class pred : public expr_predicate {
ast_manager & m_manager;
ast_manager & m;
public:
pred(ast_manager & m):m_manager(m) {}
pred(ast_manager & m):m(m) {}
bool operator()(expr * t) override {
return is_quantifier(t) || m_manager.is_label(t);
return is_quantifier(t) || m.is_label(t);
}
};
@ -124,16 +124,16 @@ name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) {
class name_nested_formulas : public name_exprs_core {
struct pred : public expr_predicate {
ast_manager & m_manager;
ast_manager & m;
expr * m_root;
pred(ast_manager & m):m_manager(m), m_root(nullptr) {}
pred(ast_manager & m):m(m), m_root(0) {}
bool operator()(expr * t) override {
TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m_manager) << "\n";);
TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m) << "\n";);
if (is_app(t))
return to_app(t)->get_family_id() == m_manager.get_basic_family_id() && to_app(t)->get_num_args() > 0 && t != m_root;
return m_manager.is_label(t) || is_quantifier(t);
return to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0 && t != m_root;
return m.is_label(t) || is_quantifier(t);
}
};

237
src/ast/normal_forms/nnf.cpp
View file

@ -17,16 +17,16 @@ Notes:
Major revision on 2011-10-06
--*/
#include "util/warning.h"
#include "util/cooperate.h"
#include "ast/normal_forms/nnf.h"
#include "ast/normal_forms/nnf_params.hpp"
#include "util/warning.h"
#include "ast/used_vars.h"
#include "ast/well_sorted.h"
#include "ast/rewriter/var_subst.h"
#include "ast/normal_forms/name_exprs.h"
#include "ast/act_cache.h"
#include "util/cooperate.h"
#include "ast/rewriter/var_subst.h"
#include "ast/normal_forms/name_exprs.h"
#include "ast/ast_smt2_pp.h"
@ -67,36 +67,42 @@ enum nnf_mode {
class skolemizer {
typedef act_cache cache;
ast_manager & m_manager;
ast_manager & m;
symbol m_sk_hack;
bool m_sk_hack_enabled;
cache m_cache;
cache m_cache_pr;
void process(quantifier * q, expr_ref & r, proof_ref & p) {
if (q->get_kind() == lambda_k) {
TRACE("nnf", tout << expr_ref(q, m) << "\n";);
r = q;
p = nullptr;
return;
}
used_vars uv;
uv(q);
SASSERT(is_well_sorted(m(), q));
SASSERT(is_well_sorted(m, q));
unsigned sz = uv.get_max_found_var_idx_plus_1();
ptr_buffer<sort> sorts;
expr_ref_vector args(m());
expr_ref_vector args(m);
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
if (s != nullptr) {
sorts.push_back(s);
args.push_back(m().mk_var(i, s));
args.push_back(m.mk_var(i, s));
}
}
TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";);
expr_ref_vector substitution(m());
expr_ref_vector substitution(m);
unsigned num_decls = q->get_num_decls();
for (unsigned i = num_decls; i > 0; ) {
--i;
sort * r = q->get_decl_sort(i);
func_decl * sk_decl = m().mk_fresh_func_decl(q->get_decl_name(i), q->get_skid(), sorts.size(), sorts.c_ptr(), r);
app * sk = m().mk_app(sk_decl, args.size(), args.c_ptr());
func_decl * sk_decl = m.mk_fresh_func_decl(q->get_decl_name(i), q->get_skid(), sorts.size(), sorts.c_ptr(), r);
app * sk = m.mk_app(sk_decl, args.size(), args.c_ptr());
substitution.push_back(sk);
}
//
@ -106,7 +112,7 @@ class skolemizer {
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
if (s != nullptr)
substitution.push_back(m().mk_var(i, s));
substitution.push_back(m.mk_var(i, s));
else
substitution.push_back(nullptr);
}
@ -118,9 +124,9 @@ class skolemizer {
//
// (VAR 0) should be in the last position of substitution.
//
var_subst s(m());
SASSERT(is_well_sorted(m(), q->get_expr()));
expr_ref tmp(m());
var_subst s(m);
SASSERT(is_well_sorted(m, q->get_expr()));
expr_ref tmp(m);
expr * body = q->get_expr();
if (m_sk_hack_enabled) {
unsigned num_patterns = q->get_num_patterns();
@ -128,27 +134,27 @@ class skolemizer {
expr * p = q->get_pattern(i);
if (is_sk_hack(p)) {
expr * sk_hack = to_app(p)->get_arg(0);
if (q->is_forall()) // check whether is in negative/positive context.
tmp = m().mk_or(body, m().mk_not(sk_hack)); // negative context
if (q->get_kind() == forall_k) // check whether is in negative/positive context.
tmp = m.mk_or(body, m.mk_not(sk_hack)); // negative context
else
tmp = m().mk_and(body, sk_hack); // positive context
tmp = m.mk_and(body, sk_hack); // positive context
body = tmp;
}
}
}
s(body, substitution.size(), substitution.c_ptr(), r);
r = s(body, substitution.size(), substitution.c_ptr());
p = nullptr;
if (m().proofs_enabled()) {
if (q->is_forall())
p = m().mk_skolemization(m().mk_not(q), m().mk_not(r));
if (m.proofs_enabled()) {
if (q->get_kind() == forall_k)
p = m.mk_skolemization(m.mk_not(q), m.mk_not(r));
else
p = m().mk_skolemization(q, r);
p = m.mk_skolemization(q, r);
}
}
public:
skolemizer(ast_manager & m):
m_manager(m),
m(m),
m_sk_hack("sk_hack"),
m_sk_hack_enabled(false),
m_cache(m),
@ -159,25 +165,23 @@ public:
m_sk_hack_enabled = f;
}
ast_manager & m() const { return m_manager; }
void operator()(quantifier * q, expr_ref & r, proof_ref & p) {
r = m_cache.find(q);
if (r.get() != nullptr) {
p = nullptr;
if (m().proofs_enabled())
if (m.proofs_enabled())
p = static_cast<proof*>(m_cache_pr.find(q));
}
else {
process(q, r, p);
m_cache.insert(q, r);
if (m().proofs_enabled())
if (m.proofs_enabled())
m_cache_pr.insert(q, p);
}
}
bool is_sk_hack(expr * p) const {
SASSERT(m().is_pattern(p));
SASSERT(m.is_pattern(p));
if (to_app(p)->get_num_args() != 1)
return false;
expr * body = to_app(p)->get_arg(0);
@ -186,7 +190,7 @@ public:
func_decl * f = to_app(body)->get_decl();
if (!(f->get_name() == m_sk_hack && f->get_arity() == 1))
return false;
if (!m().is_bool(body)) {
if (!m.is_bool(body)) {
warning_msg("sk_hack constant must return a Boolean");
return false;
}
@ -233,8 +237,8 @@ struct nnf::imp {
#define POS_NQ_CIDX 1 // positive polarity and not nested in a quantifier
#define NEG_Q_CIDX 2 // negative polarity and nested in a quantifier
#define POS_Q_CIDX 3 // positive polarity and nested in a quantifier
ast_manager & m_manager;
ast_manager & m;
vector<frame> m_frame_stack;
expr_ref_vector m_result_stack;
@ -263,7 +267,7 @@ struct nnf::imp {
unsigned long long m_max_memory; // in bytes
imp(ast_manager & m, defined_names & n, params_ref const & p):
m_manager(m),
m(m),
m_result_stack(m),
m_todo_defs(m),
m_todo_proofs(m),
@ -279,9 +283,9 @@ struct nnf::imp {
m_name_quant = mk_quantifier_label_namer(m, n);
}
ast_manager & m() const { return m_manager; }
// ast_manager & m() const { return m; }
bool proofs_enabled() const { return m().proofs_enabled(); }
bool proofs_enabled() const { return m.proofs_enabled(); }
~imp() {
for (unsigned i = 0; i < 4; i++) {
@ -334,7 +338,7 @@ struct nnf::imp {
}
void push_frame(expr * t, bool pol, bool in_q, bool cache_res) {
m_frame_stack.push_back(frame(expr_ref(t, m()), pol, in_q, cache_res, m_result_stack.size()));
m_frame_stack.push_back(frame(expr_ref(t, m), pol, in_q, cache_res, m_result_stack.size()));
}
static unsigned get_cache_idx(bool pol, bool in_q) {
@ -382,8 +386,8 @@ struct nnf::imp {
cooperate("nnf");
if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m().canceled())
throw nnf_exception(m().limit().get_cancel_msg());
if (m.canceled())
throw nnf_exception(m.limit().get_cancel_msg());
}
void set_new_child_flag() {
@ -397,16 +401,16 @@ struct nnf::imp {
}
void skip(expr * t, bool pol) {
expr * r = pol ? t : m().mk_not(t);
expr * r = pol ? t : m.mk_not(t);
m_result_stack.push_back(r);
if (proofs_enabled()) {
m_result_pr_stack.push_back(m().mk_oeq_reflexivity(r));
m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r));
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
}
}
bool visit(expr * t, bool pol, bool in_q) {
SASSERT(m().is_bool(t));
SASSERT(m.is_bool(t));
if (m_mode == NNF_SKOLEM || (m_mode == NNF_QUANT && !in_q)) {
if (!has_quantifiers(t) && !has_labels(t)) {
@ -456,12 +460,12 @@ struct nnf::imp {
proof * mk_proof(bool pol, unsigned num_parents, proof * const * parents, app * old_e, app * new_e) {
if (pol) {
if (old_e->get_decl() == new_e->get_decl())
return m().mk_oeq_congruence(old_e, new_e, num_parents, parents);
else
return m().mk_nnf_pos(old_e, new_e, num_parents, parents);
return m.mk_oeq_congruence(old_e, new_e, num_parents, parents);
else
return m.mk_nnf_pos(old_e, new_e, num_parents, parents);
}
else
return m().mk_nnf_neg(old_e, new_e, num_parents, parents);
else
return m.mk_nnf_neg(old_e, new_e, num_parents, parents);
}
bool process_and_or(app * t, frame & fr) {
@ -473,11 +477,11 @@ struct nnf::imp {
return false;
}
app * r;
if (m().is_and(t) == fr.m_pol)
r = m().mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
if (m.is_and(t) == fr.m_pol)
r = m.mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
else
r = m().mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
r = m.mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -500,7 +504,7 @@ struct nnf::imp {
if (proofs_enabled()) {
pr = m_result_pr_stack.back();
if (!fr.m_pol) {
pr = m().mk_nnf_neg(t, r, 1, &pr);
pr = m.mk_nnf_neg(t, r, 1, &pr);
m_result_pr_stack.pop_back();
m_result_pr_stack.push_back(pr);
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
@ -526,10 +530,10 @@ struct nnf::imp {
app * r;
if (fr.m_pol)
r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos);
r = m.mk_or(2, m_result_stack.c_ptr() + fr.m_spos);
else
r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos);
r = m.mk_and(2, m_result_stack.c_ptr() + fr.m_spos);
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -570,7 +574,7 @@ struct nnf::imp {
expr * _then = rs[2];
expr * _else = rs[3];
app * r = m().mk_and(m().mk_or(_not_cond, _then), m().mk_or(_cond, _else));
app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else));
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -582,7 +586,7 @@ struct nnf::imp {
return true;
}
bool is_eq(app * t) const { return m().is_eq(t); }
bool is_eq(app * t) const { return m.is_eq(t); }
bool process_iff_xor(app * t, frame & fr) {
SASSERT(t->get_num_args() == 2);
@ -614,10 +618,10 @@ struct nnf::imp {
expr * not_rhs = rs[3];
app * r;
if (is_eq(t) == fr.m_pol)
r = m().mk_and(m().mk_or(not_lhs, rhs), m().mk_or(lhs, not_rhs));
if (is_eq(t) == fr.m_pol)
r = m.mk_and(m.mk_or(not_lhs, rhs), m.mk_or(lhs, not_rhs));
else
r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs));
r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs));
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -630,7 +634,7 @@ struct nnf::imp {
}
bool process_eq(app * t, frame & fr) {
if (m().is_iff(t))
if (m.is_bool(t->get_arg(0)))
return process_iff_xor(t, fr);
else
return process_default(t, fr);
@ -639,21 +643,20 @@ struct nnf::imp {
bool process_default(app * t, frame & fr) {
SASSERT(fr.m_i == 0);
if (m_mode == NNF_FULL || t->has_quantifiers() || t->has_labels()) {
expr_ref n2(m());
proof_ref pr2(m());
expr_ref n2(m);
proof_ref pr2(m);
if (m_mode == NNF_FULL || (m_mode != NNF_SKOLEM && fr.m_in_q))
m_name_nested_formulas->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
else
m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
if (!fr.m_pol)
n2 = m().mk_not(n2);
n2 = m.mk_not(n2);
m_result_stack.push_back(n2);
if (proofs_enabled()) {
if (!fr.m_pol) {
proof * prs[1] = { pr2 };
pr2 = m().mk_oeq_congruence(m().mk_not(t), static_cast<app*>(n2.get()), 1, prs);
pr2 = m.mk_oeq_congruence(m.mk_not(t), static_cast<app*>(n2.get()), 1, prs);
}
m_result_pr_stack.push_back(pr2);
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
@ -681,24 +684,24 @@ struct nnf::imp {
buffer<symbol> names;
bool pos;
m().is_label(t, pos, names);
expr_ref r(m());
proof_ref pr(m());
m.is_label(t, pos, names);
expr_ref r(m);
proof_ref pr(m);
if (fr.m_pol == pos) {
expr * lbl_lit = m().mk_label_lit(names.size(), names.c_ptr());
r = m().mk_and(arg, lbl_lit);
expr * lbl_lit = m.mk_label_lit(names.size(), names.c_ptr());
r = m.mk_and(arg, lbl_lit);
if (proofs_enabled()) {
expr_ref aux(m_manager);
aux = m().mk_label(true, names.size(), names.c_ptr(), arg);
pr = m().mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)),
m().mk_iff_oeq(m().mk_rewrite(aux, r)));
expr_ref aux(m);
aux = m.mk_label(true, names.size(), names.c_ptr(), arg);
pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)),
m.mk_iff_oeq(m.mk_rewrite(aux, r)));
}
}
else {
r = arg;
if (proofs_enabled()) {
proof * p1 = m().mk_iff_oeq(m().mk_rewrite(t, t->get_arg(0)));
pr = m().mk_transitivity(p1, arg_pr);
proof * p1 = m.mk_iff_oeq(m.mk_rewrite(t, t->get_arg(0)));
pr = m.mk_transitivity(p1, arg_pr);
}
}
@ -713,9 +716,9 @@ struct nnf::imp {
}
bool process_app(app * t, frame & fr) {
TRACE("nnf", tout << mk_ismt2_pp(t, m()) << "\n";);
SASSERT(m().is_bool(t));
if (t->get_family_id() == m().get_basic_family_id()) {
TRACE("nnf", tout << mk_ismt2_pp(t, m) << "\n";);
SASSERT(m.is_bool(t));
if (t->get_family_id() == m.get_basic_family_id()) {
switch (static_cast<basic_op_kind>(t->get_decl_kind())) {
case OP_AND: case OP_OR:
return process_and_or(t, fr);
@ -734,7 +737,7 @@ struct nnf::imp {
}
}
if (m().is_label(t)) {
if (m.is_label(t)) {
return process_label(t, fr);
}
@ -747,28 +750,51 @@ struct nnf::imp {
}
bool process_quantifier(quantifier * q, frame & fr) {
expr_ref r(m());
proof_ref pr(m());
TRACE("nnf", tout << expr_ref(q, m) << "\n";);
expr_ref r(m);
proof_ref pr(m);
if (fr.m_i == 0) {
fr.m_i = 1;
if (q->is_forall() == fr.m_pol || !m_skolemize) {
if (is_lambda(q)) {
if (!visit(q->get_expr(), fr.m_pol, true))
return false;
}
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
if (!visit(q->get_expr(), fr.m_pol, true))
return false;
}
else {
m_skolemizer(q, r, pr);
if (!visit(r, !q->is_forall(), fr.m_in_q))
if (!visit(r, !is_forall(q), fr.m_in_q))
return false;
}
}
if (q->is_forall() == fr.m_pol || !m_skolemize) {
if (is_lambda(q)) {
expr * new_expr = m_result_stack.back();
quantifier * new_q = m.update_quantifier(q, new_expr);
proof * new_q_pr = nullptr;
if (proofs_enabled()) {
// proof * new_expr_pr = m_result_pr_stack.back();
new_q_pr = m.mk_rewrite(q, new_q); // TBD use new_expr_pr
}
m_result_stack.pop_back();
m_result_stack.push_back(new_q);
if (proofs_enabled()) {
m_result_pr_stack.pop_back();
m_result_pr_stack.push_back(new_q_pr);
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
}
return true;
}
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
expr * new_expr = m_result_stack.back();
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr;
ptr_buffer<expr> new_patterns;
if (q->is_forall() == fr.m_pol) {
if (is_forall(q) == fr.m_pol) {
// collect non sk_hack patterns
unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; i++) {
@ -785,14 +811,19 @@ struct nnf::imp {
quantifier * new_q = nullptr;
proof * new_q_pr = nullptr;
if (fr.m_pol) {
new_q = m().update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), new_expr);
if (proofs_enabled())
new_q_pr = m().mk_nnf_pos(q, new_q, 1, &new_expr_pr);
new_q = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), new_expr);
if (proofs_enabled()) {
new_expr_pr = m.mk_bind_proof(q, new_expr_pr);
new_q_pr = m.mk_nnf_pos(q, new_q, 1, &new_expr_pr);
}
}
else {
new_q = m().update_quantifier(q, !q->is_forall(), new_patterns.size(), new_patterns.c_ptr(), new_expr);
if (proofs_enabled())
new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr);
quantifier_kind k = is_forall(q)? exists_k : forall_k;
new_q = m.update_quantifier(q, k, new_patterns.size(), new_patterns.c_ptr(), new_expr);
if (proofs_enabled()) {
new_expr_pr = m.mk_bind_proof(q, new_expr_pr);
new_q_pr = m.mk_nnf_neg(q, new_q, 1, &new_expr_pr);
}
}
m_result_stack.pop_back();
@ -809,7 +840,7 @@ struct nnf::imp {
// However, the proof must be updated
if (proofs_enabled()) {
m_skolemizer(q, r, pr); // retrieve the proof
pr = m().mk_transitivity(pr, m_result_pr_stack.back());
pr = m.mk_transitivity(pr, m_result_pr_stack.back());
m_result_pr_stack.pop_back();
m_result_pr_stack.push_back(pr);
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
@ -827,14 +858,14 @@ struct nnf::imp {
result_pr = m_result_pr_stack.back();
m_result_pr_stack.pop_back();
if (result_pr.get() == nullptr)
result_pr = m().mk_reflexivity(t);
result_pr = m.mk_reflexivity(t);
SASSERT(m_result_pr_stack.empty());
}
}
void process(expr * t, expr_ref & result, proof_ref & result_pr) {
TRACE("nnf", tout << "processing:\n" << mk_ismt2_pp(t, m()) << "\n";);
SASSERT(m().is_bool(t));
TRACE("nnf", tout << "processing:\n" << mk_ismt2_pp(t, m) << "\n";);
SASSERT(m.is_bool(t));
if (visit(t, true /* positive polarity */, false /* not nested in quantifier */)) {
recover_result(t, result, result_pr);
@ -883,13 +914,13 @@ struct nnf::imp {
unsigned old_sz2 = new_def_proofs.size();
for (unsigned i = 0; i < m_todo_defs.size(); i++) {
expr_ref dr(m());
proof_ref dpr(m());
expr_ref dr(m);
proof_ref dpr(m);
process(m_todo_defs.get(i), dr, dpr);
new_defs.push_back(dr);
if (proofs_enabled()) {
proof * new_pr = m().mk_modus_ponens(m_todo_proofs.get(i), dpr);
new_def_proofs.push_back(new_pr);
proof * new_pr = m.mk_modus_ponens(m_todo_proofs.get(i), dpr);
new_def_proofs.push_back(new_pr);
}
}
std::reverse(new_defs.c_ptr() + old_sz1, new_defs.c_ptr() + new_defs.size());
@ -909,7 +940,7 @@ nnf::~nnf() {
void nnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
m_imp->operator()(n, new_defs, new_def_proofs, r, p);
TRACE("nnf_result", tout << mk_ismt2_pp(n, m_imp->m()) << "\nNNF result:\n" << mk_ismt2_pp(r, m_imp->m()) << "\n";);
TRACE("nnf_result", tout << expr_ref(n, r.get_manager()) << "\nNNF result:\n" << new_defs << "\n" << r << "\n";);
}
void nnf::updt_params(params_ref const & p) {

14
src/ast/normal_forms/pull_quant.cpp
View file

@ -49,7 +49,8 @@ struct pull_quant::imp {
if (is_quantifier(child)) {
quantifier * q = to_quantifier(child);
expr * body = q->get_expr();
result = m_manager.update_quantifier(q, !q->is_forall(), m_manager.mk_not(body));
quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k;
result = m_manager.update_quantifier(q, k, m_manager.mk_not(body));
return true;
}
else {
@ -149,7 +150,7 @@ struct pull_quant::imp {
// 3) MBQI
std::reverse(var_sorts.begin(), var_sorts.end());
std::reverse(var_names.begin(), var_names.end());
result = m_manager.mk_quantifier(forall_children,
result = m_manager.mk_quantifier(forall_children ? forall_k : exists_k,
var_sorts.size(),
var_sorts.c_ptr(),
var_names.c_ptr(),
@ -220,9 +221,7 @@ struct pull_quant::imp {
expr_ref_buffer new_args(m_manager);
expr_ref new_arg(m_manager);
ptr_buffer<proof> proofs;
unsigned num = to_app(n)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(n)->get_arg(i);
for (expr * arg : *to_app(n)) {
pull_quant1(arg , new_arg);
new_args.push_back(new_arg);
if (new_arg != arg)
@ -277,10 +276,13 @@ struct pull_quant::imp {
expr_ref & result,
proof_ref & result_pr) {
if (old_q->is_exists()) {
if (is_exists(old_q)) {
UNREACHABLE();
return false;
}
if (is_lambda(old_q)) {
return false;
}
if (!is_forall(new_body))
return false;