mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
61bd5a69ec
commit
12a255e36b
195 changed files with 11 additions and 526 deletions
526
src/ast/normal_forms/cnf.cpp
Normal file
526
src/ast/normal_forms/cnf.cpp
Normal file
|
|
@ -0,0 +1,526 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
cnf.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-01-23.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include"cnf.h"
|
||||
#include"ast_pp.h"
|
||||
#include"ast_ll_pp.h"
|
||||
|
||||
unsigned cnf_entry::hash() const {
|
||||
unsigned a = m_node->get_id();
|
||||
unsigned b = m_polarity;
|
||||
unsigned c = m_in_q;
|
||||
mix(a,b,c);
|
||||
return c;
|
||||
}
|
||||
|
||||
bool cnf_entry::operator==(cnf_entry const & k) const {
|
||||
return m_node == k.m_node && m_polarity == k.m_polarity && m_in_q == k.m_in_q;
|
||||
}
|
||||
|
||||
cnf_cache::cnf_cache(ast_manager & m):
|
||||
m_manager(m) {
|
||||
}
|
||||
|
||||
void cnf_cache::insert(cnf_entry const & k, expr * r, proof * pr) {
|
||||
SASSERT(!m_cache.contains(k));
|
||||
m_manager.inc_ref(r);
|
||||
m_manager.inc_ref(pr);
|
||||
m_cache.insert(k, expr_proof_pair(r, pr));
|
||||
}
|
||||
|
||||
void cnf_cache::reset() {
|
||||
cache::iterator it = m_cache.begin();
|
||||
cache::iterator end = m_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
expr_proof_pair & pair = (*it).m_value;
|
||||
m_manager.dec_ref(pair.first);
|
||||
m_manager.dec_ref(pair.second);
|
||||
}
|
||||
m_cache.reset();
|
||||
}
|
||||
|
||||
void cnf::cache_result(expr * e, bool in_q, expr * r, proof * pr) {
|
||||
SASSERT(r);
|
||||
TRACE("cnf", tout << "caching result for: " << e->get_id() << " " << r->get_id() << "\n";);
|
||||
m_cache.insert(cnf_entry(e, true, in_q), r, pr);
|
||||
}
|
||||
|
||||
void cnf::visit(expr * n, bool in_q, bool & visited) {
|
||||
if (!is_cached(n, in_q)) {
|
||||
m_todo.push_back(std::make_pair(n, in_q));
|
||||
visited = false;
|
||||
}
|
||||
}
|
||||
|
||||
bool cnf::visit_children(expr * n, bool in_q) {
|
||||
bool visited = true;
|
||||
switch(n->get_kind()) {
|
||||
case AST_APP:
|
||||
if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_label(n)) {
|
||||
unsigned j = to_app(n)->get_num_args();
|
||||
while (j > 0) {
|
||||
--j;
|
||||
visit(to_app(n)->get_arg(j), in_q, visited);
|
||||
}
|
||||
}
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
visit(to_quantifier(n)->get_expr(), true, visited);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return visited;
|
||||
}
|
||||
|
||||
void cnf::reduce1(expr * n, bool in_q) {
|
||||
switch(n->get_kind()) {
|
||||
case AST_APP:
|
||||
if (m_manager.is_or(n))
|
||||
reduce1_or(to_app(n), in_q);
|
||||
else if (m_manager.is_and(n))
|
||||
reduce1_and(to_app(n), in_q);
|
||||
else if (m_manager.is_label(n))
|
||||
reduce1_label(to_app(n), in_q);
|
||||
else
|
||||
cache_result(n, in_q, n, 0);
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
reduce1_quantifier(to_quantifier(n), in_q);
|
||||
break;
|
||||
default:
|
||||
cache_result(n, in_q, n, 0);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void cnf::get_args(app * n, bool in_q, ptr_buffer<expr> & new_args, ptr_buffer<proof> & new_arg_prs) {
|
||||
unsigned num = n->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr * new_arg = 0;
|
||||
proof * new_arg_pr = 0;
|
||||
get_cached(n->get_arg(i), in_q, new_arg, new_arg_pr);
|
||||
SASSERT(new_arg);
|
||||
new_args.push_back(new_arg);
|
||||
if (new_arg_pr)
|
||||
new_arg_prs.push_back(new_arg_pr);
|
||||
}
|
||||
}
|
||||
|
||||
void cnf::flat_args(func_decl * d, ptr_buffer<expr> const & args, ptr_buffer<expr> & flat_args) {
|
||||
ptr_buffer<expr>::const_iterator it = args.begin();
|
||||
ptr_buffer<expr>::const_iterator end = args.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * arg = *it;
|
||||
if (is_app_of(arg, d))
|
||||
flat_args.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
|
||||
else
|
||||
flat_args.push_back(arg);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return the approximated size of distributing OR over AND on
|
||||
(OR args[0] .... args[sz-1])
|
||||
*/
|
||||
approx_nat cnf::approx_result_size_for_disj(ptr_buffer<expr> const & args) {
|
||||
approx_nat r(1);
|
||||
ptr_buffer<expr>::const_iterator it = args.begin();
|
||||
ptr_buffer<expr>::const_iterator end = args.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * arg = *it;
|
||||
if (m_manager.is_and(arg))
|
||||
r *= to_app(arg)->get_num_args();
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true if it is too expensive to process the disjunction of args
|
||||
*/
|
||||
inline bool cnf::is_too_expensive(approx_nat approx_result_size, ptr_buffer<expr> const & args) {
|
||||
// (OR A (AND B C)) is always considered cheap.
|
||||
if (args.size() == 2 && (!m_manager.is_and(args[0]) || !m_manager.is_and(args[1])))
|
||||
return false;
|
||||
return !(approx_result_size < m_params.m_cnf_factor);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a (positive) name for the expressions of the form (AND ...) in args.
|
||||
Store the result in new_args.
|
||||
*/
|
||||
void cnf::name_args(ptr_buffer<expr> const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs) {
|
||||
ptr_buffer<expr>::const_iterator it = args.begin();
|
||||
ptr_buffer<expr>::const_iterator end = args.end();
|
||||
for (; it != end; ++it) {
|
||||
expr * arg = *it;
|
||||
if (m_manager.is_and(arg)) {
|
||||
expr_ref new_def(m_manager);
|
||||
proof_ref new_def_pr(m_manager);
|
||||
app_ref new_arg(m_manager);
|
||||
proof_ref new_arg_pr(m_manager);
|
||||
|
||||
if (m_defined_names.mk_pos_name(to_app(arg), new_def, new_def_pr, new_arg, new_arg_pr)) {
|
||||
m_todo_defs.push_back(new_def);
|
||||
if (m_manager.proofs_enabled())
|
||||
m_todo_proofs.push_back(new_def_pr);
|
||||
}
|
||||
new_args.push_back(new_arg);
|
||||
|
||||
if (m_manager.fine_grain_proofs())
|
||||
new_arg_prs.push_back(new_arg_pr);
|
||||
else
|
||||
m_coarse_proofs.push_back(new_arg_pr);
|
||||
}
|
||||
else
|
||||
new_args.push_back(arg);
|
||||
}
|
||||
}
|
||||
|
||||
void cnf::distribute(app * n, app * & r, proof * & pr) {
|
||||
SASSERT(m_manager.is_or(n));
|
||||
buffer<unsigned> sz;
|
||||
buffer<unsigned> it;
|
||||
ptr_buffer<expr> new_args;
|
||||
unsigned num = n->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
it.push_back(0);
|
||||
if (m_manager.is_and(arg))
|
||||
sz.push_back(to_app(arg)->get_num_args());
|
||||
else
|
||||
sz.push_back(1);
|
||||
}
|
||||
|
||||
do {
|
||||
ptr_buffer<expr> lits;
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
if (m_manager.is_and(arg)) {
|
||||
SASSERT(it[i] < to_app(arg)->get_num_args());
|
||||
lits.push_back(to_app(arg)->get_arg(it[i]));
|
||||
}
|
||||
else {
|
||||
SASSERT(it[i] == 0);
|
||||
lits.push_back(arg);
|
||||
}
|
||||
}
|
||||
app * n = m_manager.mk_or(lits.size(), lits.c_ptr());
|
||||
new_args.push_back(n);
|
||||
}
|
||||
while (product_iterator_next(sz.size(), sz.c_ptr(), it.c_ptr()));
|
||||
SASSERT(!new_args.empty());
|
||||
if (new_args.size() == 1)
|
||||
r = to_app(new_args[0]);
|
||||
else
|
||||
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
|
||||
pr = 0;
|
||||
if (m_manager.fine_grain_proofs() && r != n)
|
||||
pr = m_manager.mk_iff_oeq(m_manager.mk_distributivity(n, r));
|
||||
}
|
||||
|
||||
void cnf::push_quant(quantifier * q, expr * & r, proof * & pr) {
|
||||
SASSERT(is_forall(q));
|
||||
expr * e = q->get_expr();
|
||||
pr = 0;
|
||||
if (m_manager.is_and(e)) {
|
||||
expr_ref_buffer new_args(m_manager);
|
||||
unsigned num = to_app(e)->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
quantifier_ref aux(m_manager);
|
||||
aux = m_manager.update_quantifier(q, 0, 0, 0, 0, to_app(e)->get_arg(i));
|
||||
expr_ref new_arg(m_manager);
|
||||
elim_unused_vars(m_manager, aux, new_arg);
|
||||
new_args.push_back(new_arg);
|
||||
}
|
||||
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
|
||||
if (m_manager.fine_grain_proofs())
|
||||
pr = m_manager.mk_iff_oeq(m_manager.mk_push_quant(q, r));
|
||||
}
|
||||
else {
|
||||
r = q;
|
||||
}
|
||||
}
|
||||
|
||||
void cnf::reduce1_or(app * n, bool in_q) {
|
||||
ptr_buffer<expr> new_args;
|
||||
ptr_buffer<proof> new_arg_prs;
|
||||
get_args(n, in_q, new_args, new_arg_prs);
|
||||
expr * r;
|
||||
proof * pr = 0;
|
||||
if (in_q || m_params.m_cnf_mode == CNF_OPPORTUNISTIC || m_params.m_cnf_mode == CNF_FULL) {
|
||||
ptr_buffer<expr> f_args;
|
||||
flat_args(n->get_decl(), new_args, f_args);
|
||||
TRACE("cnf_or", for (unsigned i = 0; i < f_args.size(); i++) tout << mk_pp(f_args[i], m_manager) << "\n";);
|
||||
approx_nat result_size = approx_result_size_for_disj(f_args);
|
||||
TRACE("cnf_or", tout << mk_pp(n, m_manager) << "\napprox. result: " << result_size << "\n";);
|
||||
if (m_params.m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_params.m_cnf_factor) {
|
||||
expr_ref_buffer cheap_args(m_manager);
|
||||
proof_ref_buffer cheap_args_pr(m_manager);
|
||||
bool named_args;
|
||||
if (is_too_expensive(result_size, f_args)) {
|
||||
named_args = true;
|
||||
name_args(f_args, cheap_args, cheap_args_pr);
|
||||
}
|
||||
else {
|
||||
named_args = false;
|
||||
cheap_args.append(f_args.size(), f_args.c_ptr());
|
||||
}
|
||||
|
||||
app_ref r1(m_manager);
|
||||
r1 = m_manager.mk_or(cheap_args.size(), cheap_args.c_ptr());
|
||||
|
||||
// Proof gen support ---------------------------
|
||||
// r1 is (OR cheap_args) it is only built if proofs are enabled.
|
||||
// p1 is a proof for (= n r1)
|
||||
proof * p1 = 0;
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
proof * prs[3];
|
||||
app * r[2];
|
||||
r[0] = m_manager.mk_or(new_args.size(), new_args.c_ptr());
|
||||
prs[0] = n == r[0] ? 0 : m_manager.mk_oeq_congruence(n, r[0], new_arg_prs.size(), new_arg_prs.c_ptr());
|
||||
r[1] = m_manager.mk_or(f_args.size(), f_args.c_ptr());
|
||||
prs[1] = r[0] == r[1] ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r[0], r[1]));
|
||||
prs[2] = r[1] == r1 ? 0 : m_manager.mk_oeq_congruence(r[1], r1, cheap_args_pr.size(), cheap_args_pr.c_ptr());
|
||||
p1 = m_manager.mk_transitivity(3, prs);
|
||||
}
|
||||
// --------------------------------------------
|
||||
|
||||
expr_ref r2(m_manager);
|
||||
proof_ref p2(m_manager);
|
||||
m_pull.pull_quant2(r1, r2, p2);
|
||||
|
||||
if (is_quantifier(r2)) {
|
||||
expr * e = to_quantifier(r2)->get_expr();
|
||||
SASSERT(m_manager.is_or(e));
|
||||
app * d_r;
|
||||
proof * d_pr;
|
||||
distribute(to_app(e), d_r, d_pr);
|
||||
quantifier_ref r3(m_manager);
|
||||
r3 = m_manager.update_quantifier(to_quantifier(r2), d_r);
|
||||
proof * push_pr;
|
||||
push_quant(r3, r, push_pr);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
// p1 is a proof of n == r1
|
||||
// p2 is a proof of r1 == r2
|
||||
p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2);
|
||||
proof * p3 = r2 == r3 ? 0 : m_manager.mk_oeq_quant_intro(to_quantifier(r2), r3, d_pr);
|
||||
CTRACE("cnf_or", p1, tout << "p1:\n" << mk_pp(m_manager.get_fact(p1), m_manager) << "\n";);
|
||||
CTRACE("cnf_or", p2, tout << "p2:\n" << mk_pp(m_manager.get_fact(p2), m_manager) << "\n";);
|
||||
CTRACE("cnf_or", p3, tout << "p3:\n" << mk_pp(m_manager.get_fact(p3), m_manager) << "\n";);
|
||||
TRACE("cnf_or", tout << "r2 == r3: " << (r2 == r3) << "\n"
|
||||
<< mk_pp(r2, m_manager) << "\n" << mk_pp(r3, m_manager) << "\n";);
|
||||
pr = m_manager.mk_transitivity(p1, p2, p3, push_pr);
|
||||
}
|
||||
cache_result(n, in_q, r, pr);
|
||||
}
|
||||
else {
|
||||
SASSERT(p2 == 0);
|
||||
SASSERT(r1 == r2);
|
||||
SASSERT(m_manager.is_or(r2));
|
||||
app * r3;
|
||||
distribute(to_app(r2), r3, pr);
|
||||
r = r3;
|
||||
pr = m_manager.mk_transitivity(p1, pr);
|
||||
cache_result(n, in_q, r, pr);
|
||||
}
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
r = m_manager.mk_or(new_args.size(), new_args.c_ptr());
|
||||
if (m_manager.fine_grain_proofs() && n != r)
|
||||
pr = m_manager.mk_oeq_congruence(n, to_app(r), new_arg_prs.size(), new_arg_prs.c_ptr());
|
||||
cache_result(n, in_q, r, pr);
|
||||
}
|
||||
|
||||
void cnf::reduce1_and(app * n, bool in_q) {
|
||||
ptr_buffer<expr> new_args;
|
||||
ptr_buffer<proof> new_arg_prs;
|
||||
get_args(n, in_q, new_args, new_arg_prs);
|
||||
app * r;
|
||||
proof * pr = 0;
|
||||
if (in_q || m_params.m_cnf_mode == CNF_OPPORTUNISTIC || m_params.m_cnf_mode == CNF_FULL) {
|
||||
ptr_buffer<expr> f_args;
|
||||
flat_args(n->get_decl(), new_args, f_args);
|
||||
r = m_manager.mk_and(f_args.size(), f_args.c_ptr());
|
||||
if (m_manager.fine_grain_proofs() && n != r) {
|
||||
app * r0 = m_manager.mk_and(new_args.size(), new_args.c_ptr());
|
||||
proof * p0 = r0 == n ? 0 : m_manager.mk_oeq_congruence(n, r0, new_arg_prs.size(), new_arg_prs.c_ptr());
|
||||
proof * p1 = r0 == r ? 0 : m_manager.mk_iff_oeq(m_manager.mk_rewrite(r0, r));
|
||||
pr = m_manager.mk_transitivity(p0, p1);
|
||||
}
|
||||
}
|
||||
else {
|
||||
r = m_manager.mk_and(new_args.size(), new_args.c_ptr());
|
||||
if (m_manager.fine_grain_proofs() && n != r)
|
||||
pr = m_manager.mk_oeq_congruence(n, r, new_arg_prs.size(), new_arg_prs.c_ptr());
|
||||
}
|
||||
cache_result(n, in_q, r, pr);
|
||||
}
|
||||
|
||||
void cnf::reduce1_label(app * n, bool in_q) {
|
||||
expr * r;
|
||||
proof * pr = 0;
|
||||
expr * new_arg;
|
||||
proof * new_arg_pr;
|
||||
get_cached(n->get_arg(0), true, new_arg, new_arg_pr);
|
||||
if (in_q || m_params.m_cnf_mode == CNF_FULL) {
|
||||
// TODO: in the current implementation, labels are removed during CNF translation.
|
||||
// This is satisfactory for Boogie, since it does not use labels inside quantifiers,
|
||||
// and we only need CNF_QUANT for Superposition Calculus.
|
||||
r = new_arg;
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
proof * p0 = m_manager.mk_iff_oeq(m_manager.mk_rewrite(n, n->get_arg(0)));
|
||||
pr = m_manager.mk_transitivity(p0, new_arg_pr);
|
||||
}
|
||||
}
|
||||
else {
|
||||
r = m_manager.mk_app(n->get_decl(), new_arg);
|
||||
if (m_manager.fine_grain_proofs() && n != r)
|
||||
pr = m_manager.mk_oeq_congruence(n, to_app(r), 1, &new_arg_pr);
|
||||
}
|
||||
cache_result(n, in_q, r, pr);
|
||||
}
|
||||
|
||||
void cnf::reduce1_quantifier(quantifier * q, bool in_q) {
|
||||
expr * new_expr;
|
||||
proof * new_expr_pr;
|
||||
get_cached(q->get_expr(), true, new_expr, new_expr_pr);
|
||||
expr_ref r(m_manager);
|
||||
proof_ref pr(m_manager);
|
||||
if (m_manager.is_and(new_expr) && q->is_forall()) {
|
||||
quantifier_ref q1(m_manager);
|
||||
q1 = m_manager.update_quantifier(q, new_expr);
|
||||
expr_ref q2(m_manager);
|
||||
proof_ref p2(m_manager);
|
||||
m_pull.pull_quant2(q1, q2, p2);
|
||||
expr * q3;
|
||||
proof * p3;
|
||||
push_quant(to_quantifier(q2), q3, p3);
|
||||
r = q3;
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr);
|
||||
p2 = p2 == 0 ? 0 : m_manager.mk_iff_oeq(p2);
|
||||
pr = m_manager.mk_transitivity(p1, p2, p3);
|
||||
}
|
||||
}
|
||||
else if ((m_manager.is_or(new_expr) || is_forall(new_expr)) && q->is_forall()) {
|
||||
quantifier_ref q1(m_manager);
|
||||
q1 = m_manager.update_quantifier(q, new_expr);
|
||||
m_pull.pull_quant2(q1, r, pr);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
pr = pr == 0 ? 0 : m_manager.mk_iff_oeq(pr);
|
||||
proof * p1 = q == q1 ? 0 : m_manager.mk_oeq_quant_intro(q, q1, new_expr_pr);
|
||||
pr = m_manager.mk_transitivity(p1, pr);
|
||||
}
|
||||
}
|
||||
else {
|
||||
r = m_manager.update_quantifier(q, new_expr);
|
||||
if (m_manager.fine_grain_proofs() && r != q)
|
||||
pr = q == r ? 0 : m_manager.mk_oeq_quant_intro(q, to_quantifier(r), new_expr_pr);
|
||||
}
|
||||
|
||||
cache_result(q, in_q, r, pr);
|
||||
TRACE("cnf_quant", tout << mk_pp(q, m_manager) << "\n" << mk_pp(r, m_manager) << "\n";);
|
||||
}
|
||||
|
||||
cnf::cnf(ast_manager & m, defined_names & n, cnf_params & params):
|
||||
m_params(params),
|
||||
m_manager(m),
|
||||
m_defined_names(n),
|
||||
m_pull(m),
|
||||
m_cache(m),
|
||||
m_todo_defs(m),
|
||||
m_todo_proofs(m),
|
||||
m_coarse_proofs(m) {
|
||||
}
|
||||
|
||||
cnf::~cnf() {
|
||||
}
|
||||
|
||||
void cnf::reduce(expr * n, expr_ref & r, proof_ref & pr) {
|
||||
m_coarse_proofs.reset();
|
||||
m_todo.reset();
|
||||
m_todo.push_back(expr_bool_pair(n, false));
|
||||
while (!m_todo.empty()) {
|
||||
expr_bool_pair pair = m_todo.back();
|
||||
expr * n = pair.first;
|
||||
bool in_q = pair.second;
|
||||
if (is_cached(n, in_q)) {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
else if (visit_children(n, in_q)) {
|
||||
m_todo.pop_back();
|
||||
reduce1(n, in_q);
|
||||
}
|
||||
}
|
||||
expr * r2;
|
||||
proof * pr2;
|
||||
get_cached(n, false, r2, pr2);
|
||||
r = r2;
|
||||
switch (m_manager.proof_mode()) {
|
||||
case PGM_DISABLED:
|
||||
pr = m_manager.mk_undef_proof();
|
||||
break;
|
||||
case PGM_COARSE:
|
||||
remove_duplicates(m_coarse_proofs);
|
||||
pr = n == r2 ? m_manager.mk_reflexivity(n) : m_manager.mk_cnf_star(n, r2, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
|
||||
break;
|
||||
case PGM_FINE:
|
||||
pr = pr2 == 0 ? m_manager.mk_reflexivity(n) : pr2;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void cnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & pr) {
|
||||
if (m_params.m_cnf_mode == CNF_DISABLED) {
|
||||
r = n;
|
||||
pr = m_manager.mk_reflexivity(n);
|
||||
return;
|
||||
}
|
||||
|
||||
reset();
|
||||
reduce(n, r, pr);
|
||||
for (unsigned i = 0; i < m_todo_defs.size(); i++) {
|
||||
expr_ref dr(m_manager);
|
||||
proof_ref dpr(m_manager);
|
||||
reduce(m_todo_defs.get(i), dr, dpr);
|
||||
m_result_defs.push_back(dr);
|
||||
if (m_manager.proofs_enabled()) {
|
||||
proof * new_pr = m_manager.mk_modus_ponens(m_todo_proofs.get(i), dpr);
|
||||
m_result_def_proofs.push_back(new_pr);
|
||||
}
|
||||
else
|
||||
m_result_def_proofs.push_back(m_manager.mk_undef_proof());
|
||||
}
|
||||
std::reverse(m_result_defs.begin(), m_result_defs.end());
|
||||
new_defs.append(m_result_defs.size(), m_result_defs.c_ptr());
|
||||
std::reverse(m_result_def_proofs.begin(), m_result_def_proofs.end());
|
||||
new_def_proofs.append(m_result_def_proofs.size(), m_result_def_proofs.c_ptr());
|
||||
}
|
||||
|
||||
void cnf::reset() {
|
||||
m_cache.reset();
|
||||
m_todo.reset();
|
||||
m_todo_defs.reset();
|
||||
m_todo_proofs.reset();
|
||||
m_result_defs.reset();
|
||||
m_result_def_proofs.reset();
|
||||
}
|
||||
121
src/ast/normal_forms/cnf.h
Normal file
121
src/ast/normal_forms/cnf.h
Normal file
|
|
@ -0,0 +1,121 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
cnf.h
|
||||
|
||||
Abstract:
|
||||
|
||||
CNF translation
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-01-17.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _CNF_H_
|
||||
#define _CNF_H_
|
||||
|
||||
#include"cnf_params.h"
|
||||
#include"pull_quant.h"
|
||||
#include"nnf.h"
|
||||
#include"approx_nat.h"
|
||||
|
||||
/**
|
||||
\brief Entry into the todo list of the CNF translator. It is also used as the key in the CNF cache.
|
||||
*/
|
||||
struct cnf_entry {
|
||||
expr * m_node;
|
||||
bool m_polarity:1;
|
||||
bool m_in_q:1;
|
||||
cnf_entry():m_node(0), m_polarity(false), m_in_q(false) {}
|
||||
cnf_entry(expr * n, bool p, bool in_q):m_node(n), m_polarity(p), m_in_q(in_q) {}
|
||||
unsigned hash() const;
|
||||
bool operator==(cnf_entry const & k) const;
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Cache for CNF transformation. It is a mapping from (expr, polarity, in_q) -> (expr, proof)
|
||||
*/
|
||||
class cnf_cache {
|
||||
public:
|
||||
typedef std::pair<expr *, proof *> expr_proof_pair;
|
||||
|
||||
typedef map<cnf_entry, expr_proof_pair, obj_hash<cnf_entry>, default_eq<cnf_entry> > cache;
|
||||
|
||||
ast_manager & m_manager;
|
||||
cache m_cache;
|
||||
|
||||
public:
|
||||
cnf_cache(ast_manager & m);
|
||||
~cnf_cache() { reset(); }
|
||||
void insert(cnf_entry const & k, expr * r, proof * pr);
|
||||
bool contains(cnf_entry const & k) const { return m_cache.contains(k); }
|
||||
void get(cnf_entry const & k, expr * & r, proof * & pr) const { expr_proof_pair tmp; m_cache.find(k, tmp); r = tmp.first; pr = tmp.second; }
|
||||
void reset();
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Functor for converting expressions into CNF. The functor can
|
||||
optionally process subformulas nested in quantifiers. New names may be
|
||||
introduced for subformulas that are too expensive to be put into CNF.
|
||||
|
||||
NNF translation must be applied before converting to CNF.
|
||||
|
||||
- To use CNF_QUANT, we must use at least NNF_QUANT
|
||||
- To use CNF_OPPORTUNISTIC, we must use at least NNF_QUANT
|
||||
- To use CNF_FULL, we must use NNF_FULL
|
||||
*/
|
||||
class cnf {
|
||||
typedef std::pair<expr *, bool> expr_bool_pair;
|
||||
cnf_params & m_params;
|
||||
ast_manager & m_manager;
|
||||
defined_names & m_defined_names;
|
||||
pull_quant m_pull;
|
||||
cnf_cache m_cache;
|
||||
svector<expr_bool_pair> m_todo;
|
||||
expr_ref_vector m_todo_defs;
|
||||
proof_ref_vector m_todo_proofs;
|
||||
ptr_vector<expr> m_result_defs;
|
||||
ptr_vector<proof> m_result_def_proofs;
|
||||
proof_ref_vector m_coarse_proofs;
|
||||
|
||||
void cache_result(expr * e, bool in_q, expr * r, proof * pr);
|
||||
void get_cached(expr * n, bool in_q, expr * & r, proof * & pr) const { m_cache.get(cnf_entry(n, true, in_q), r, pr); }
|
||||
bool is_cached(expr * n, bool in_q) const { return m_cache.contains(cnf_entry(n, true, in_q)); }
|
||||
|
||||
void visit(expr * n, bool in_q, bool & visited);
|
||||
bool visit_children(expr * n, bool in_q);
|
||||
|
||||
void get_args(app * n, bool in_q, ptr_buffer<expr> & new_args, ptr_buffer<proof> & new_arg_prs);
|
||||
void flat_args(func_decl * d, ptr_buffer<expr> const & args, ptr_buffer<expr> & flat_args);
|
||||
approx_nat approx_result_size_for_disj(ptr_buffer<expr> const & args);
|
||||
bool is_too_expensive(approx_nat approx_result_size, ptr_buffer<expr> const & args);
|
||||
void name_args(ptr_buffer<expr> const & args, expr_ref_buffer & new_args, proof_ref_buffer & new_arg_prs);
|
||||
void distribute(app * arg, app * & r, proof * & pr);
|
||||
void push_quant(quantifier * q, expr * & r, proof * & pr);
|
||||
void reduce1(expr * n, bool in_q);
|
||||
void reduce1_or(app * n, bool in_q);
|
||||
void reduce1_and(app * n, bool in_q);
|
||||
void reduce1_label(app * n, bool in_q);
|
||||
void reduce1_quantifier(quantifier * q, bool in_q);
|
||||
|
||||
void reduce(expr * n, expr_ref & r, proof_ref & pr);
|
||||
public:
|
||||
cnf(ast_manager & m, defined_names & n, cnf_params & params);
|
||||
~cnf();
|
||||
void operator()(expr * n, // [IN] expression that should be put into CNF
|
||||
expr_ref_vector & new_defs, // [OUT] new definitions
|
||||
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
|
||||
expr_ref & r, // [OUT] resultant expression
|
||||
proof_ref & p // [OUT] proof for (~ n r)
|
||||
);
|
||||
|
||||
void reset();
|
||||
};
|
||||
|
||||
#endif /* _CNF_H_ */
|
||||
|
||||
226
src/ast/normal_forms/defined_names.cpp
Normal file
226
src/ast/normal_forms/defined_names.cpp
Normal file
|
|
@ -0,0 +1,226 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
defined_names.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-01-14.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"defined_names.h"
|
||||
#include"used_vars.h"
|
||||
#include"var_subst.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"ast_pp.h"
|
||||
|
||||
defined_names::impl::impl(ast_manager & m, char const * prefix):
|
||||
m_manager(m),
|
||||
m_exprs(m),
|
||||
m_names(m),
|
||||
m_apply_proofs(m) {
|
||||
if (prefix)
|
||||
m_z3name = prefix;
|
||||
}
|
||||
|
||||
defined_names::impl::~impl() {
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
|
||||
where sk is a fresh variable name, and x_i's are the free variables of \c e.
|
||||
|
||||
Store in var_sorts and var_names information about the free variables of \c e. This data
|
||||
is used to create an universal quantifier over the definition of the new name.
|
||||
*/
|
||||
app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names) {
|
||||
used_vars uv;
|
||||
uv(e);
|
||||
unsigned num_vars = uv.get_max_found_var_idx_plus_1();
|
||||
ptr_buffer<expr> new_args;
|
||||
ptr_buffer<sort> domain;
|
||||
for (unsigned i = 0; i < num_vars; i++) {
|
||||
sort * s = uv.get(i);
|
||||
if (s) {
|
||||
domain.push_back(s);
|
||||
new_args.push_back(m_manager.mk_var(i, s));
|
||||
var_sorts.push_back(s);
|
||||
}
|
||||
else {
|
||||
var_sorts.push_back(m_manager.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) << " ";
|
||||
tout << "\n";);
|
||||
return n;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Cache \c n as a name for expression \c e.
|
||||
*/
|
||||
void defined_names::impl::cache_new_name(expr * e, app * n) {
|
||||
m_expr2name.insert(e, n);
|
||||
m_exprs.push_back(e);
|
||||
m_names.push_back(n);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Cache \c pr as a proof that m_expr2name[e] is a name for expression \c e.
|
||||
*/
|
||||
void defined_names::impl::cache_new_name_intro_proof(expr * e, proof * pr) {
|
||||
SASSERT(m_expr2name.contains(e));
|
||||
m_expr2proof.insert(e, pr);
|
||||
m_apply_proofs.push_back(pr);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given a definition conjunct \c def of the name \c name, store in \c result this definition.
|
||||
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) {
|
||||
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(),
|
||||
sorts.c_ptr(),
|
||||
names.c_ptr(),
|
||||
def_conjunct,
|
||||
1, symbol::null, 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, result);
|
||||
TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m_manager) << "\n";);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Given a definition conjunct \c def of the name \c name, store in \c result this definition.
|
||||
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);
|
||||
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
|
||||
|
||||
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)) {
|
||||
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)) {
|
||||
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 {
|
||||
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());
|
||||
}
|
||||
|
||||
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) {
|
||||
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";);
|
||||
|
||||
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()) {
|
||||
proof * pr_ptr;
|
||||
m_expr2proof.find(e, pr_ptr);
|
||||
SASSERT(pr_ptr);
|
||||
pr = pr_ptr;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
sort_ref_buffer var_sorts(m_manager);
|
||||
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";);
|
||||
// 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";);
|
||||
|
||||
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);
|
||||
cache_new_name_intro_proof(e, pr);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
void defined_names::impl::push_scope() {
|
||||
SASSERT(m_exprs.size() == m_names.size());
|
||||
m_lims.push_back(m_exprs.size());
|
||||
}
|
||||
|
||||
void defined_names::impl::pop_scope(unsigned num_scopes) {
|
||||
unsigned lvl = m_lims.size();
|
||||
SASSERT(num_scopes <= lvl);
|
||||
unsigned new_lvl = lvl - num_scopes;
|
||||
unsigned old_sz = m_lims[new_lvl];
|
||||
unsigned sz = m_exprs.size();
|
||||
SASSERT(old_sz <= sz);
|
||||
SASSERT(sz == m_names.size());
|
||||
while (old_sz != sz) {
|
||||
--sz;
|
||||
if (m_manager.proofs_enabled()) {
|
||||
m_expr2proof.erase(m_exprs.back());
|
||||
m_apply_proofs.pop_back();
|
||||
}
|
||||
m_expr2name.erase(m_exprs.back());
|
||||
m_exprs.pop_back();
|
||||
m_names.pop_back();
|
||||
}
|
||||
SASSERT(m_exprs.size() == old_sz);
|
||||
m_lims.shrink(new_lvl);
|
||||
}
|
||||
|
||||
void defined_names::impl::reset() {
|
||||
m_expr2name.reset();
|
||||
m_expr2proof.reset();
|
||||
m_exprs.reset();
|
||||
m_names.reset();
|
||||
m_apply_proofs.reset();
|
||||
m_lims.reset();
|
||||
}
|
||||
|
||||
|
||||
|
||||
151
src/ast/normal_forms/defined_names.h
Normal file
151
src/ast/normal_forms/defined_names.h
Normal file
|
|
@ -0,0 +1,151 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
defined_names.h
|
||||
|
||||
Abstract:
|
||||
|
||||
In some transformations, we need to name expressions.
|
||||
These expressions are stored in a table.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-01-14.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _DEFINED_NAMES_H_
|
||||
#define _DEFINED_NAMES_H_
|
||||
|
||||
#include"ast.h"
|
||||
#include"obj_hashtable.h"
|
||||
|
||||
/**
|
||||
\brief Mapping from expressions to skolem functions that are used to name them.
|
||||
|
||||
The mapping supports backtracking using the methods #push_scope and #pop_scope.
|
||||
*/
|
||||
class defined_names {
|
||||
|
||||
struct impl {
|
||||
typedef obj_map<expr, app *> expr2name;
|
||||
typedef obj_map<expr, proof *> expr2proof;
|
||||
ast_manager & m_manager;
|
||||
symbol m_z3name;
|
||||
|
||||
/**
|
||||
\brief Mapping from expressions to their names. A name is an application.
|
||||
If the expression does not have free variables, then the name is just a constant.
|
||||
*/
|
||||
expr2name m_expr2name;
|
||||
/**
|
||||
\brief Mapping from expressions to the apply-def proof.
|
||||
That is, for each expression e, m_expr2proof[e] is the
|
||||
proof e and m_expr2name[2] are observ. equivalent.
|
||||
|
||||
This mapping is not used if proof production is disabled.
|
||||
*/
|
||||
expr2proof m_expr2proof;
|
||||
|
||||
/**
|
||||
\brief Domain of m_expr2name. It is used to keep the expressions
|
||||
alive and for backtracking
|
||||
*/
|
||||
expr_ref_vector m_exprs;
|
||||
expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
|
||||
proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
|
||||
|
||||
|
||||
unsigned_vector m_lims; //!< Backtracking support.
|
||||
|
||||
impl(ast_manager & m, char const * prefix);
|
||||
virtual ~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);
|
||||
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);
|
||||
void reset();
|
||||
};
|
||||
|
||||
struct pos_impl : public impl {
|
||||
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
|
||||
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
|
||||
};
|
||||
|
||||
impl m_impl;
|
||||
pos_impl m_pos_impl;
|
||||
public:
|
||||
defined_names(ast_manager & m, char const * fresh_prefix = "z3name"):m_impl(m, fresh_prefix), m_pos_impl(m, fresh_prefix) {}
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// High-level API
|
||||
//
|
||||
// -----------------------------------
|
||||
|
||||
/**
|
||||
\brief Create a name for expression \c e if it doesn't already exists.
|
||||
|
||||
Return true if a new name was created, and false if a name already exists for \c e.
|
||||
|
||||
The resultant new name is stored in n, and a [apply-def] proof
|
||||
that (= e n) is stored into pr.
|
||||
|
||||
If true is returned, then the definition of the new name is
|
||||
stored into new_def, and a [def-intro] proof into new_def_pr.
|
||||
|
||||
The proofs are not produced when proof generation is disabled.
|
||||
|
||||
The definition of an expression e with name n is:
|
||||
|
||||
- (and (or (not e) n) (or e (not n))) if e is an formula.
|
||||
- (and (or (not c) (= n t1)) (or c (= n t2))) if e is an if-then-else term of the form (ite c t1 t2)
|
||||
- (= n e) if e is a term.
|
||||
|
||||
Remark: the definitions are closed with an universal quantifier if e contains free variables.
|
||||
*/
|
||||
bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
|
||||
return m_impl.mk_name(e, new_def, new_def_pr, n, pr);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Create a name for a positive occurrence of the expression \c e.
|
||||
|
||||
Return true if a new pos-name was created, and false if a pos-name already exists for \c e.
|
||||
|
||||
If true is returned, then the definition of the new name is stored into new_def.
|
||||
It has the form: (or (not n) e)
|
||||
|
||||
Remark: the definitions are closed with an universal quantifier if e contains free variables.
|
||||
*/
|
||||
bool mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
|
||||
return m_pos_impl.mk_name(e, new_def, new_def_pr, n, pr);
|
||||
}
|
||||
|
||||
void push_scope() {
|
||||
m_impl.push_scope();
|
||||
m_pos_impl.push_scope();
|
||||
}
|
||||
|
||||
void pop_scope(unsigned num_scopes) {
|
||||
m_impl.pop_scope(num_scopes);
|
||||
m_pos_impl.pop_scope(num_scopes);
|
||||
}
|
||||
|
||||
void reset() {
|
||||
m_impl.reset();
|
||||
m_pos_impl.reset();
|
||||
}
|
||||
};
|
||||
|
||||
#endif /* _DEFINED_NAMES_H_ */
|
||||
|
||||
160
src/ast/normal_forms/elim_term_ite.cpp
Normal file
160
src/ast/normal_forms/elim_term_ite.cpp
Normal file
|
|
@ -0,0 +1,160 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
elim_term_ite.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-06-12.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"elim_term_ite.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
void elim_term_ite::operator()(expr * n,
|
||||
expr_ref_vector & new_defs,
|
||||
proof_ref_vector & new_def_proofs,
|
||||
expr_ref & r,
|
||||
proof_ref & pr) {
|
||||
|
||||
m_coarse_proofs.reset();
|
||||
m_new_defs = &new_defs;
|
||||
m_new_def_proofs = &new_def_proofs;
|
||||
reduce_core(n);
|
||||
expr * r2;
|
||||
proof * pr2;
|
||||
get_cached(n, r2, pr2);
|
||||
r = r2;
|
||||
switch (m_manager.proof_mode()) {
|
||||
case PGM_DISABLED:
|
||||
pr = m_manager.mk_undef_proof();
|
||||
break;
|
||||
case PGM_COARSE:
|
||||
remove_duplicates(m_coarse_proofs);
|
||||
pr = n == r2 ? m_manager.mk_oeq_reflexivity(n) : m_manager.mk_apply_defs(n, r, m_coarse_proofs.size(), m_coarse_proofs.c_ptr());
|
||||
break;
|
||||
case PGM_FINE:
|
||||
pr = pr2 == 0 ? m_manager.mk_oeq_reflexivity(n) : pr2;
|
||||
break;
|
||||
}
|
||||
m_coarse_proofs.reset();
|
||||
}
|
||||
|
||||
void elim_term_ite::reduce_core(expr * n) {
|
||||
m_todo.reset();
|
||||
if (!is_cached(n)) {
|
||||
m_todo.push_back(n);
|
||||
while (!m_todo.empty()) {
|
||||
expr * n = m_todo.back();
|
||||
if (is_cached(n)) {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
else if (visit_children(n)) {
|
||||
m_todo.pop_back();
|
||||
reduce1(n);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool elim_term_ite::visit_children(expr * n) {
|
||||
bool visited = true;
|
||||
unsigned j;
|
||||
switch(n->get_kind()) {
|
||||
case AST_VAR:
|
||||
return true;
|
||||
case AST_APP:
|
||||
j = to_app(n)->get_num_args();
|
||||
while (j > 0) {
|
||||
--j;
|
||||
visit(to_app(n)->get_arg(j), visited);
|
||||
}
|
||||
return visited;
|
||||
case AST_QUANTIFIER:
|
||||
visit(to_quantifier(n)->get_expr(), visited);
|
||||
return visited;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
void elim_term_ite::reduce1(expr * n) {
|
||||
switch (n->get_kind()) {
|
||||
case AST_VAR:
|
||||
cache_result(n, n, 0);
|
||||
break;
|
||||
case AST_APP:
|
||||
reduce1_app(to_app(n));
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
reduce1_quantifier(to_quantifier(n));
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
}
|
||||
|
||||
void elim_term_ite::reduce1_app(app * n) {
|
||||
m_args.reset();
|
||||
|
||||
func_decl * decl = n->get_decl();
|
||||
proof_ref p1(m_manager);
|
||||
get_args(n, m_args, p1);
|
||||
if (!m_manager.fine_grain_proofs())
|
||||
p1 = 0;
|
||||
|
||||
expr_ref r(m_manager);
|
||||
r = m_manager.mk_app(decl, m_args.size(), m_args.c_ptr());
|
||||
if (m_manager.is_term_ite(r)) {
|
||||
expr_ref new_def(m_manager);
|
||||
proof_ref new_def_pr(m_manager);
|
||||
app_ref new_r(m_manager);
|
||||
proof_ref new_pr(m_manager);
|
||||
if (m_defined_names.mk_name(r, new_def, new_def_pr, new_r, new_pr)) {
|
||||
CTRACE("elim_term_ite_bug", new_def.get() == 0, tout << mk_ismt2_pp(r, m_manager) << "\n";);
|
||||
SASSERT(new_def.get() != 0);
|
||||
m_new_defs->push_back(new_def);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
m_new_def_proofs->push_back(new_def_pr);
|
||||
new_pr = m_manager.mk_transitivity(p1, new_pr);
|
||||
}
|
||||
else {
|
||||
// [Leo] This looks fishy... why do we add 0 into m_coarse_proofs when fine_grain_proofs are disabled?
|
||||
new_pr = 0;
|
||||
if (m_manager.proofs_enabled())
|
||||
m_coarse_proofs.push_back(new_pr);
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(new_def.get() == 0);
|
||||
if (!m_manager.fine_grain_proofs())
|
||||
new_pr = 0;
|
||||
}
|
||||
cache_result(n, new_r, new_pr);
|
||||
}
|
||||
else {
|
||||
cache_result(n, r, p1);
|
||||
}
|
||||
}
|
||||
|
||||
void elim_term_ite::reduce1_quantifier(quantifier * q) {
|
||||
expr * new_body;
|
||||
proof * new_body_pr;
|
||||
get_cached(q->get_expr(), new_body, new_body_pr);
|
||||
|
||||
quantifier * new_q = m_manager.update_quantifier(q, new_body);
|
||||
proof * p = q == new_q ? 0 : m_manager.mk_oeq_quant_intro(q, new_q, new_body_pr);
|
||||
cache_result(q, new_q, p);
|
||||
}
|
||||
|
||||
|
||||
|
||||
50
src/ast/normal_forms/elim_term_ite.h
Normal file
50
src/ast/normal_forms/elim_term_ite.h
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
elim_term_ite.h
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2008-06-12.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _ELIM_TERM_ITE_H_
|
||||
#define _ELIM_TERM_ITE_H_
|
||||
|
||||
#include"simplifier.h"
|
||||
#include"defined_names.h"
|
||||
|
||||
class elim_term_ite : public simplifier {
|
||||
defined_names & m_defined_names;
|
||||
proof_ref_vector m_coarse_proofs;
|
||||
expr_ref_vector * m_new_defs;
|
||||
proof_ref_vector * m_new_def_proofs;
|
||||
void reduce_core(expr * n);
|
||||
bool visit_children(expr * n);
|
||||
void reduce1(expr * n);
|
||||
void reduce1_app(app * n);
|
||||
void reduce1_quantifier(quantifier * q);
|
||||
public:
|
||||
elim_term_ite(ast_manager & m, defined_names & d):simplifier(m), m_defined_names(d), m_coarse_proofs(m) {
|
||||
m_use_oeq = true;
|
||||
enable_ac_support(false);
|
||||
}
|
||||
virtual ~elim_term_ite() {}
|
||||
void operator()(expr * n, // [IN]
|
||||
expr_ref_vector & new_defs, // [OUT] new definitions
|
||||
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
|
||||
expr_ref & r, // [OUT] resultant expression
|
||||
proof_ref & pr // [OUT] proof for (~ n r)
|
||||
);
|
||||
};
|
||||
|
||||
#endif /* _ELIM_TERM_ITE_H_ */
|
||||
|
||||
167
src/ast/normal_forms/name_exprs.cpp
Normal file
167
src/ast/normal_forms/name_exprs.cpp
Normal file
|
|
@ -0,0 +1,167 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
name_exprs.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Goodies for naming nested expressions.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-10-06
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"name_exprs.h"
|
||||
#include"rewriter_def.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
class name_exprs_core : public name_exprs {
|
||||
struct cfg : public default_rewriter_cfg {
|
||||
ast_manager & m_manager;
|
||||
defined_names & m_defined_names;
|
||||
expr_predicate & m_pred;
|
||||
|
||||
app_ref m_r;
|
||||
proof_ref m_pr;
|
||||
|
||||
expr_ref_vector * m_def_exprs;
|
||||
proof_ref_vector * m_def_proofs;
|
||||
|
||||
cfg(ast_manager & m, defined_names & n, expr_predicate & pred):
|
||||
m_manager(m),
|
||||
m_defined_names(n),
|
||||
m_pred(pred),
|
||||
m_r(m),
|
||||
m_pr(m),
|
||||
m_def_exprs(0),
|
||||
m_def_proofs(0) {
|
||||
}
|
||||
|
||||
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);
|
||||
|
||||
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())
|
||||
m_def_proofs->push_back(new_def_pr);
|
||||
}
|
||||
|
||||
t = m_r.get();
|
||||
t_pr = m_pr.get();
|
||||
}
|
||||
|
||||
bool get_subst(expr * s, expr * & t, proof * & t_pr) {
|
||||
TRACE("name_exprs", tout << "get_subst:\n" << mk_ismt2_pp(s, m_manager) << "\n";);
|
||||
if (m_pred(s)) {
|
||||
gen_name_for_expr(s, t, t_pr);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
typedef rewriter_tpl<cfg> rw;
|
||||
|
||||
cfg m_cfg;
|
||||
rw m_rw;
|
||||
|
||||
public:
|
||||
name_exprs_core(ast_manager & m, defined_names & n, expr_predicate & pred):
|
||||
m_cfg(m, n, pred),
|
||||
m_rw(m, m.proofs_enabled(), m_cfg) {
|
||||
}
|
||||
|
||||
virtual ~name_exprs_core() {
|
||||
}
|
||||
|
||||
virtual void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
|
||||
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";);
|
||||
}
|
||||
|
||||
virtual void set_cancel(bool f) {
|
||||
m_rw.set_cancel(f);
|
||||
}
|
||||
|
||||
virtual void reset() {
|
||||
m_rw.reset();
|
||||
}
|
||||
};
|
||||
|
||||
name_exprs * mk_expr_namer(ast_manager & m, defined_names & n, expr_predicate & pred) {
|
||||
return alloc(name_exprs_core, m, n, pred);
|
||||
}
|
||||
|
||||
class name_quantifier_labels : public name_exprs_core {
|
||||
class pred : public expr_predicate {
|
||||
ast_manager & m_manager;
|
||||
public:
|
||||
pred(ast_manager & m):m_manager(m) {}
|
||||
virtual bool operator()(expr * t) {
|
||||
return is_quantifier(t) || m_manager.is_label(t);
|
||||
}
|
||||
};
|
||||
|
||||
pred m_pred;
|
||||
public:
|
||||
name_quantifier_labels(ast_manager & m, defined_names & n):
|
||||
name_exprs_core(m, n, m_pred),
|
||||
m_pred(m) {
|
||||
}
|
||||
|
||||
virtual ~name_quantifier_labels() {
|
||||
}
|
||||
};
|
||||
|
||||
name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n) {
|
||||
return alloc(name_quantifier_labels, m, n);
|
||||
}
|
||||
|
||||
class name_nested_formulas : public name_exprs_core {
|
||||
struct pred : public expr_predicate {
|
||||
ast_manager & m_manager;
|
||||
expr * m_root;
|
||||
|
||||
pred(ast_manager & m):m_manager(m), m_root(0) {}
|
||||
|
||||
virtual bool operator()(expr * t) {
|
||||
TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m_manager) << "\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);
|
||||
}
|
||||
};
|
||||
|
||||
pred m_pred;
|
||||
|
||||
public:
|
||||
name_nested_formulas(ast_manager & m, defined_names & n):
|
||||
name_exprs_core(m, n, m_pred),
|
||||
m_pred(m) {
|
||||
}
|
||||
|
||||
virtual ~name_nested_formulas() {
|
||||
}
|
||||
|
||||
virtual void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
|
||||
m_pred.m_root = n;
|
||||
TRACE("name_exprs", tout << "operator()\n";);
|
||||
name_exprs_core::operator()(n, new_defs, new_def_proofs, r, p);
|
||||
}
|
||||
};
|
||||
|
||||
name_exprs * mk_nested_formula_namer(ast_manager & m, defined_names & n) {
|
||||
return alloc(name_nested_formulas, m, n);
|
||||
}
|
||||
|
||||
void del_name_exprs(name_exprs * functor) {
|
||||
dealloc(functor);
|
||||
}
|
||||
65
src/ast/normal_forms/name_exprs.h
Normal file
65
src/ast/normal_forms/name_exprs.h
Normal file
|
|
@ -0,0 +1,65 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
name_exprs.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Goodies for naming nested expressions.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-10-06
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _NAME_EXPRS_H_
|
||||
#define _NAME_EXPRS_H_
|
||||
|
||||
#include"ast.h"
|
||||
#include"defined_names.h"
|
||||
|
||||
class expr_predicate {
|
||||
public:
|
||||
virtual bool operator()(expr * t) = 0;
|
||||
};
|
||||
|
||||
class name_exprs {
|
||||
public:
|
||||
virtual ~name_exprs() {}
|
||||
virtual void operator()(expr * n, // [IN] expression that contain the sub-expressions to be named
|
||||
expr_ref_vector & new_defs, // [OUT] new definitions
|
||||
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
|
||||
expr_ref & r, // [OUT] resultant expression
|
||||
proof_ref & p // [OUT] proof for (iff n p)
|
||||
) = 0;
|
||||
|
||||
virtual void set_cancel(bool f) = 0;
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
virtual void reset() = 0;
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Create an expression "namer" that will create replace nested expressions that satisfy pred with new
|
||||
fresh declarations.
|
||||
*/
|
||||
name_exprs * mk_expr_namer(ast_manager & m, defined_names & n, expr_predicate & pred);
|
||||
|
||||
/**
|
||||
\brief Create an expression "namer" that will replace quantifiers and labels with new fresh declarations.
|
||||
*/
|
||||
name_exprs * mk_quantifier_label_namer(ast_manager & m, defined_names & n);
|
||||
|
||||
/**
|
||||
\brief Create an expression "namer" that will replace all nested formulas and term if-then-elses with
|
||||
fresh declarations.
|
||||
*/
|
||||
name_exprs * mk_nested_formula_namer(ast_manager & m, defined_names & n);
|
||||
|
||||
void del_name_exprs(name_exprs * functor);
|
||||
|
||||
#endif
|
||||
927
src/ast/normal_forms/nnf.cpp
Normal file
927
src/ast/normal_forms/nnf.cpp
Normal file
|
|
@ -0,0 +1,927 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
nnf.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Negation Normal Form & Skolemization
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-11
|
||||
|
||||
Notes:
|
||||
Major revision on 2011-10-06
|
||||
|
||||
--*/
|
||||
#include"nnf.h"
|
||||
#include"warning.h"
|
||||
#include"used_vars.h"
|
||||
#include"well_sorted.h"
|
||||
#include"var_subst.h"
|
||||
|
||||
#include"name_exprs.h"
|
||||
#include"act_cache.h"
|
||||
#include"cooperate.h"
|
||||
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
class skolemizer {
|
||||
typedef act_cache cache;
|
||||
|
||||
ast_manager & m_manager;
|
||||
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) {
|
||||
used_vars uv;
|
||||
uv(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());
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
sort * s = uv.get(i);
|
||||
if (s != 0) {
|
||||
sorts.push_back(s);
|
||||
args.push_back(m().mk_var(i, s));
|
||||
}
|
||||
}
|
||||
|
||||
TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";);
|
||||
|
||||
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());
|
||||
substitution.push_back(sk);
|
||||
}
|
||||
//
|
||||
// (VAR 0) is in the first position of substitution.
|
||||
// (VAR num_decls-1) is in the last position.
|
||||
//
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
sort * s = uv.get(i);
|
||||
if (s != 0)
|
||||
substitution.push_back(m().mk_var(i, s));
|
||||
else
|
||||
substitution.push_back(0);
|
||||
}
|
||||
//
|
||||
// (VAR num_decls) ... (VAR num_decls+sz-1)
|
||||
// are in positions num_decls .. num_decls+sz-1
|
||||
//
|
||||
std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size());
|
||||
//
|
||||
// (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());
|
||||
expr * body = q->get_expr();
|
||||
if (m_sk_hack_enabled) {
|
||||
unsigned num_patterns = q->get_num_patterns();
|
||||
for (unsigned i = 0; i < num_patterns; ++i) {
|
||||
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
|
||||
else
|
||||
tmp = m().mk_and(body, sk_hack); // positive context
|
||||
body = tmp;
|
||||
}
|
||||
}
|
||||
}
|
||||
s(body, substitution.size(), substitution.c_ptr(), r);
|
||||
SASSERT(is_well_sorted(m(), r));
|
||||
p = 0;
|
||||
if (m().proofs_enabled()) {
|
||||
if (q->is_forall())
|
||||
p = m().mk_skolemization(m().mk_not(q), m().mk_not(r));
|
||||
else
|
||||
p = m().mk_skolemization(q, r);
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
skolemizer(ast_manager & m, params_ref const & p):
|
||||
m_manager(m),
|
||||
m_sk_hack("sk_hack"),
|
||||
m_cache(m),
|
||||
m_cache_pr(m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_sk_hack_enabled = p.get_bool(":nnf-sk-hack", false);
|
||||
}
|
||||
|
||||
static void get_param_descrs(param_descrs & r) {
|
||||
r.insert(":nnf-sk-hack", CPK_BOOL, "(default: false) hack for VCC");
|
||||
}
|
||||
|
||||
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() != 0) {
|
||||
p = 0;
|
||||
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())
|
||||
m_cache_pr.insert(q, p);
|
||||
}
|
||||
}
|
||||
|
||||
bool is_sk_hack(expr * p) const {
|
||||
SASSERT(m().is_pattern(p));
|
||||
if (to_app(p)->get_num_args() != 1)
|
||||
return false;
|
||||
expr * body = to_app(p)->get_arg(0);
|
||||
if (!is_app(body))
|
||||
return false;
|
||||
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)) {
|
||||
warning_msg("sk_hack constant must return a Boolean");
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
typedef default_exception nnf_params_exception;
|
||||
typedef default_exception nnf_exception;
|
||||
|
||||
struct nnf::imp {
|
||||
|
||||
struct frame {
|
||||
expr * m_curr;
|
||||
unsigned m_i:28;
|
||||
unsigned m_pol:1; // pos/neg polarity
|
||||
unsigned m_in_q:1; // true if m_curr is nested in a quantifier
|
||||
unsigned m_new_child:1;
|
||||
unsigned m_cache_result:1;
|
||||
unsigned m_spos; // top of the result stack, when the frame was created.
|
||||
frame(expr * n, bool pol, bool in_q, bool cache_res, unsigned spos):
|
||||
m_curr(n),
|
||||
m_i(0),
|
||||
m_pol(pol),
|
||||
m_in_q(in_q),
|
||||
m_new_child(false),
|
||||
m_cache_result(cache_res),
|
||||
m_spos(spos) {
|
||||
}
|
||||
};
|
||||
|
||||
// There are four caches:
|
||||
#define NEG_NQ_CIDX 0 // negative polarity and not nested in a quantifier
|
||||
#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;
|
||||
svector<frame> m_frame_stack;
|
||||
expr_ref_vector m_result_stack;
|
||||
|
||||
typedef act_cache cache;
|
||||
cache * m_cache[4];
|
||||
|
||||
expr_ref_vector m_todo_defs;
|
||||
proof_ref_vector m_todo_proofs;
|
||||
|
||||
// proof generation goodness ----
|
||||
proof_ref_vector m_result_pr_stack;
|
||||
cache * m_cache_pr[4];
|
||||
// ------------------------------
|
||||
|
||||
skolemizer m_skolemizer;
|
||||
|
||||
// configuration ----------------
|
||||
nnf_mode m_mode;
|
||||
bool m_ignore_labels;
|
||||
bool m_skolemize;
|
||||
// ------------------------------
|
||||
|
||||
name_exprs * m_name_nested_formulas;
|
||||
name_exprs * m_name_quant;
|
||||
|
||||
symbol m_skolem;
|
||||
|
||||
volatile bool m_cancel;
|
||||
unsigned long long m_max_memory; // in bytes
|
||||
|
||||
imp(ast_manager & m, defined_names & n, params_ref const & p):
|
||||
m_manager(m),
|
||||
m_result_stack(m),
|
||||
m_todo_defs(m),
|
||||
m_todo_proofs(m),
|
||||
m_result_pr_stack(m),
|
||||
m_skolemizer(m, p),
|
||||
m_skolem("skolem"),
|
||||
m_cancel(false) {
|
||||
updt_local_params(p);
|
||||
for (unsigned i = 0; i < 4; i++) {
|
||||
m_cache[i] = alloc(act_cache, m);
|
||||
if (m.proofs_enabled())
|
||||
m_cache_pr[i] = alloc(act_cache, m);
|
||||
}
|
||||
m_name_nested_formulas = mk_nested_formula_namer(m, n);
|
||||
m_name_quant = mk_quantifier_label_namer(m, n);
|
||||
}
|
||||
|
||||
ast_manager & m() const { return m_manager; }
|
||||
|
||||
bool proofs_enabled() const { return m().proofs_enabled(); }
|
||||
|
||||
~imp() {
|
||||
for (unsigned i = 0; i < 4; i++) {
|
||||
dealloc(m_cache[i]);
|
||||
if (proofs_enabled())
|
||||
dealloc(m_cache_pr[i]);
|
||||
}
|
||||
del_name_exprs(m_name_nested_formulas);
|
||||
del_name_exprs(m_name_quant);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
updt_local_params(p);
|
||||
m_skolemizer.updt_params(p);
|
||||
}
|
||||
|
||||
void updt_local_params(params_ref const & p) {
|
||||
symbol mode_sym = p.get_sym(":nnf-mode", m_skolem);
|
||||
if (mode_sym == m_skolem)
|
||||
m_mode = NNF_SKOLEM;
|
||||
else if (mode_sym == "full")
|
||||
m_mode = NNF_FULL;
|
||||
else if (mode_sym == "quantifiers")
|
||||
m_mode = NNF_QUANT;
|
||||
else
|
||||
throw nnf_params_exception("invalid NNF mode");
|
||||
|
||||
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << p << "\n";);
|
||||
|
||||
m_ignore_labels = p.get_bool(":nnf-ignore-labels", false);
|
||||
m_skolemize = p.get_bool(":skolemize", true);
|
||||
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
|
||||
}
|
||||
|
||||
static void get_param_descrs(param_descrs & r) {
|
||||
insert_max_memory(r);
|
||||
r.insert(":nnf-mode", CPK_SYMBOL,
|
||||
"(default: skolem) NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full");
|
||||
r.insert(":nnf-ignore-labels", CPK_BOOL,
|
||||
"(default: false) remove/ignore labels in the input formula, this option is ignored if proofs are enabled");
|
||||
r.insert(":skolemize", CPK_BOOL,
|
||||
"(default: true) skolemize (existential force) quantifiers");
|
||||
skolemizer::get_param_descrs(r);
|
||||
}
|
||||
|
||||
void reset() {
|
||||
m_frame_stack.reset();
|
||||
m_result_stack.reset();
|
||||
m_result_pr_stack.reset();
|
||||
m_todo_defs.reset();
|
||||
m_todo_proofs.reset();
|
||||
}
|
||||
|
||||
void reset_cache() {
|
||||
for (unsigned i = 0; i < 4; i++) {
|
||||
m_cache[i]->reset();
|
||||
if (proofs_enabled())
|
||||
m_cache_pr[i]->reset();
|
||||
}
|
||||
}
|
||||
|
||||
void push_frame(expr * t, bool pol, bool in_q, bool cache_res) {
|
||||
m_frame_stack.push_back(frame(t, pol, in_q, cache_res, m_result_stack.size()));
|
||||
}
|
||||
|
||||
static unsigned get_cache_idx(bool pol, bool in_q) {
|
||||
return static_cast<unsigned>(in_q) * 2 + static_cast<unsigned>(pol);
|
||||
}
|
||||
|
||||
void cache_result(expr * t, bool pol, bool in_q, expr * v, proof * pr) {
|
||||
unsigned idx = get_cache_idx(pol, in_q);
|
||||
m_cache[idx]->insert(t, v);
|
||||
if (proofs_enabled())
|
||||
m_cache_pr[idx]->insert(t, pr);
|
||||
}
|
||||
|
||||
expr * get_cached(expr * t, bool pol, bool in_q) const {
|
||||
return m_cache[get_cache_idx(pol, in_q)]->find(t);
|
||||
}
|
||||
|
||||
proof * get_cached_pr(expr * t, bool pol, bool in_q) const {
|
||||
SASSERT(proofs_enabled());
|
||||
return static_cast<proof*>(m_cache_pr[get_cache_idx(pol, in_q)]->find(t));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true if the result for (t, pol, in_q) is already cached,
|
||||
and store the result on the stack.
|
||||
*/
|
||||
bool process_cached(expr * t, bool pol, bool in_q) {
|
||||
expr * r = get_cached(t, pol, in_q);
|
||||
if (r) {
|
||||
m_result_stack.push_back(r);
|
||||
if (proofs_enabled()) {
|
||||
proof * pr = get_cached_pr(t, pol, in_q);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
m_frame_stack.pop_back();
|
||||
set_new_child_flag(t, r);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
cooperate("nnf");
|
||||
if (memory::get_allocation_size() > m_max_memory)
|
||||
throw nnf_exception(TACTIC_MAX_MEMORY_MSG);
|
||||
if (m_cancel)
|
||||
throw nnf_exception(TACTIC_CANCELED_MSG);
|
||||
}
|
||||
|
||||
void set_new_child_flag() {
|
||||
if (!m_frame_stack.empty())
|
||||
m_frame_stack.back().m_new_child = true;
|
||||
}
|
||||
|
||||
void set_new_child_flag(expr * old_t, expr * new_t) {
|
||||
if (old_t != new_t)
|
||||
set_new_child_flag();
|
||||
}
|
||||
|
||||
void skip(expr * t, bool pol) {
|
||||
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));
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
}
|
||||
|
||||
bool visit(expr * t, bool pol, bool in_q) {
|
||||
SASSERT(m().is_bool(t));
|
||||
|
||||
if (m_mode == NNF_SKOLEM || (m_mode == NNF_QUANT && !in_q)) {
|
||||
if (!has_quantifiers(t) && !has_labels(t)) {
|
||||
skip(t, pol);
|
||||
return true; // t does not need to be processed
|
||||
}
|
||||
}
|
||||
|
||||
bool cache_res = t->get_ref_count() > 1;
|
||||
|
||||
if (cache_res) {
|
||||
expr * r = get_cached(t, pol, in_q);
|
||||
if (r) {
|
||||
m_result_stack.push_back(r);
|
||||
set_new_child_flag(t, r);
|
||||
if (proofs_enabled()) {
|
||||
proof * pr = get_cached_pr(t, pol, in_q);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true; // t was already processed
|
||||
}
|
||||
}
|
||||
|
||||
switch (t->get_kind()) {
|
||||
case AST_APP:
|
||||
if (to_app(t)->get_num_args() == 0) {
|
||||
skip(t, pol);
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
push_frame(t, pol, in_q, cache_res);
|
||||
return false;
|
||||
}
|
||||
case AST_QUANTIFIER:
|
||||
push_frame(t, pol, in_q, cache_res);
|
||||
return false;
|
||||
case AST_VAR:
|
||||
skip(t, pol);
|
||||
return true;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
else
|
||||
return m().mk_nnf_neg(old_e, new_e, num_parents, parents);
|
||||
}
|
||||
|
||||
bool process_and_or(app * t, frame & fr) {
|
||||
unsigned num_args = t->get_num_args();
|
||||
while (fr.m_i < num_args) {
|
||||
expr * arg = t->get_arg(fr.m_i);
|
||||
fr.m_i++;
|
||||
if (!visit(arg, fr.m_pol, fr.m_in_q))
|
||||
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);
|
||||
else
|
||||
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()) {
|
||||
proof * pr = mk_proof(fr.m_pol, t->get_num_args(), m_result_pr_stack.c_ptr() + fr.m_spos, t, r);
|
||||
m_result_pr_stack.shrink(fr.m_spos);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_not(app * t, frame & fr) {
|
||||
if (fr.m_i == 0) {
|
||||
fr.m_i = 1;
|
||||
if (!visit(t->get_arg(0), !fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
}
|
||||
expr * r = m_result_stack.back();
|
||||
proof * pr = 0;
|
||||
if (proofs_enabled()) {
|
||||
pr = m_result_pr_stack.back();
|
||||
if (!fr.m_pol) {
|
||||
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());
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_implies(app * t, frame & fr) {
|
||||
SASSERT(t->get_num_args() == 2);
|
||||
switch (fr.m_i) {
|
||||
case 0:
|
||||
fr.m_i = 1;
|
||||
if (!visit(t->get_arg(0), !fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
case 1:
|
||||
fr.m_i = 2;
|
||||
if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
app * r;
|
||||
if (fr.m_pol)
|
||||
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);
|
||||
|
||||
m_result_stack.shrink(fr.m_spos);
|
||||
m_result_stack.push_back(r);
|
||||
if (proofs_enabled()) {
|
||||
proof * pr = mk_proof(fr.m_pol, 2, m_result_pr_stack.c_ptr() + fr.m_spos, t, r);
|
||||
m_result_pr_stack.shrink(fr.m_spos);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_ite(app * t, frame & fr) {
|
||||
SASSERT(t->get_num_args() == 3);
|
||||
switch (fr.m_i) {
|
||||
case 0:
|
||||
fr.m_i = 1;
|
||||
if (!visit(t->get_arg(0), true, fr.m_in_q))
|
||||
return false;
|
||||
case 1:
|
||||
fr.m_i = 2;
|
||||
if (!visit(t->get_arg(0), false, fr.m_in_q))
|
||||
return false;
|
||||
case 2:
|
||||
fr.m_i = 3;
|
||||
if (!visit(t->get_arg(1), fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
case 3:
|
||||
fr.m_i = 4;
|
||||
if (!visit(t->get_arg(2), fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
expr * const * rs = m_result_stack.c_ptr() + fr.m_spos;
|
||||
expr * _cond = rs[0];
|
||||
expr * _not_cond = rs[1];
|
||||
expr * _then = rs[2];
|
||||
expr * _else = rs[3];
|
||||
|
||||
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()) {
|
||||
proof * pr = mk_proof(fr.m_pol, 4, m_result_pr_stack.c_ptr() + fr.m_spos, t, r);
|
||||
m_result_pr_stack.shrink(fr.m_spos);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); }
|
||||
|
||||
bool process_iff_xor(app * t, frame & fr) {
|
||||
SASSERT(t->get_num_args() == 2);
|
||||
switch (fr.m_i) {
|
||||
case 0:
|
||||
fr.m_i = 1;
|
||||
if (!visit(t->get_arg(0), true, fr.m_in_q))
|
||||
return false;
|
||||
case 1:
|
||||
fr.m_i = 2;
|
||||
if (!visit(t->get_arg(0), false, fr.m_in_q))
|
||||
return false;
|
||||
case 2:
|
||||
fr.m_i = 3;
|
||||
if (!visit(t->get_arg(1), true, fr.m_in_q))
|
||||
return false;
|
||||
case 3:
|
||||
fr.m_i = 4;
|
||||
if (!visit(t->get_arg(1), false, fr.m_in_q))
|
||||
return false;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
expr * const * rs = m_result_stack.c_ptr() + fr.m_spos;
|
||||
expr * lhs = rs[0];
|
||||
expr * not_lhs = rs[1];
|
||||
expr * rhs = rs[2];
|
||||
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));
|
||||
else
|
||||
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()) {
|
||||
proof * pr = mk_proof(fr.m_pol, 4, m_result_pr_stack.c_ptr() + fr.m_spos, t, r);
|
||||
m_result_pr_stack.shrink(fr.m_spos);
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_eq(app * t, frame & fr) {
|
||||
if (m().is_bool(t->get_arg(0)))
|
||||
return process_iff_xor(t, fr);
|
||||
else
|
||||
return process_default(t, fr);
|
||||
}
|
||||
|
||||
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());
|
||||
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);
|
||||
|
||||
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);
|
||||
}
|
||||
m_result_pr_stack.push_back(pr2);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
}
|
||||
else {
|
||||
skip(t, fr.m_pol);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_label(app * t, frame & fr) {
|
||||
if (fr.m_i == 0) {
|
||||
fr.m_i = 1;
|
||||
if (!visit(t->get_arg(0), fr.m_pol, fr.m_in_q))
|
||||
return false;
|
||||
}
|
||||
|
||||
expr * arg = m_result_stack.back();
|
||||
proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
|
||||
|
||||
if (m_ignore_labels && !proofs_enabled())
|
||||
return true; // the result is already on the stack
|
||||
|
||||
|
||||
buffer<symbol> names;
|
||||
bool pos;
|
||||
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);
|
||||
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)));
|
||||
}
|
||||
}
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
m_result_stack.pop_back();
|
||||
m_result_stack.push_back(r);
|
||||
if (proofs_enabled()) {
|
||||
m_result_pr_stack.pop_back();
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_app(app * t, frame & fr) {
|
||||
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);
|
||||
case OP_NOT:
|
||||
return process_not(t, fr);
|
||||
case OP_IMPLIES:
|
||||
return process_implies(t, fr);
|
||||
case OP_ITE:
|
||||
return process_ite(t, fr);
|
||||
case OP_IFF:
|
||||
case OP_XOR:
|
||||
return process_iff_xor(t, fr);
|
||||
case OP_EQ:
|
||||
return process_eq(t, fr);
|
||||
default:
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (m().is_label(t)) {
|
||||
return process_label(t, fr);
|
||||
}
|
||||
|
||||
return process_default(t, fr);
|
||||
}
|
||||
|
||||
bool process_var(var * v, frame & fr) {
|
||||
skip(v, fr.m_pol);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool process_quantifier(quantifier * q, frame & fr) {
|
||||
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 (!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))
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
if (q->is_forall() == fr.m_pol || !m_skolemize) {
|
||||
expr * new_expr = m_result_stack.back();
|
||||
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
|
||||
|
||||
ptr_buffer<expr> new_patterns;
|
||||
|
||||
if (q->is_forall() == fr.m_pol) {
|
||||
// collect non sk_hack patterns
|
||||
unsigned num_patterns = q->get_num_patterns();
|
||||
for (unsigned i = 0; i < num_patterns; i++) {
|
||||
expr * pat = q->get_pattern(i);
|
||||
if (!m_skolemizer.is_sk_hack(pat))
|
||||
new_patterns.push_back(pat);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// New quantifier has existential force.
|
||||
// So, ignore patterns
|
||||
}
|
||||
|
||||
quantifier * new_q = 0;
|
||||
proof * new_q_pr = 0;
|
||||
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);
|
||||
}
|
||||
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);
|
||||
}
|
||||
|
||||
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());
|
||||
}
|
||||
}
|
||||
else {
|
||||
// Quantifier was skolemized.
|
||||
// The result is already on the stack.
|
||||
// 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());
|
||||
m_result_pr_stack.pop_back();
|
||||
m_result_pr_stack.push_back(pr);
|
||||
SASSERT(m_result_stack.size() == m_result_pr_stack.size());
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) {
|
||||
// recover result from the top of the stack.
|
||||
result = m_result_stack.back();
|
||||
m_result_stack.pop_back();
|
||||
SASSERT(m_result_stack.empty());
|
||||
if (proofs_enabled()) {
|
||||
result_pr = m_result_pr_stack.back();
|
||||
m_result_pr_stack.pop_back();
|
||||
if (result_pr.get() == 0)
|
||||
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));
|
||||
|
||||
if (visit(t, true /* positive polarity */, false /* not nested in quantifier */)) {
|
||||
recover_result(t, result, result_pr);
|
||||
return;
|
||||
}
|
||||
SASSERT(!m_frame_stack.empty());
|
||||
while (!m_frame_stack.empty()) {
|
||||
checkpoint();
|
||||
frame & fr = m_frame_stack.back();
|
||||
expr * t = fr.m_curr;
|
||||
|
||||
if (fr.m_i == 0 && t->get_ref_count() > 1 && process_cached(t, fr.m_pol, fr.m_in_q))
|
||||
continue;
|
||||
|
||||
bool status;
|
||||
|
||||
switch (t->get_kind()) {
|
||||
case AST_APP:
|
||||
status = process_app(to_app(t), fr);
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
status = process_quantifier(to_quantifier(t), fr);
|
||||
break;
|
||||
case AST_VAR:
|
||||
status = process_var(to_var(t), fr);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
status = true;
|
||||
break;
|
||||
}
|
||||
|
||||
if (status) {
|
||||
if (fr.m_cache_result)
|
||||
cache_result(fr.m_curr, fr.m_pol, fr.m_in_q, m_result_stack.back(), proofs_enabled() ? m_result_pr_stack.back() : 0);
|
||||
m_frame_stack.pop_back();
|
||||
}
|
||||
}
|
||||
recover_result(t, result, result_pr);
|
||||
}
|
||||
|
||||
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & pr) {
|
||||
reset();
|
||||
process(n, r, pr);
|
||||
unsigned old_sz1 = new_defs.size();
|
||||
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());
|
||||
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);
|
||||
}
|
||||
}
|
||||
std::reverse(new_defs.c_ptr() + old_sz1, new_defs.c_ptr() + new_defs.size());
|
||||
std::reverse(new_def_proofs.c_ptr() + old_sz2, new_def_proofs.c_ptr() + new_def_proofs.size());
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) {
|
||||
TRACE("nnf", tout << "nnf constructor: " << p << "\n";);
|
||||
m_imp = alloc(imp, m, n, p);
|
||||
}
|
||||
|
||||
nnf::nnf(ast_manager & m, defined_names & n, nnf_params & np) {
|
||||
params_ref p;
|
||||
if (np.m_nnf_mode == NNF_FULL)
|
||||
p.set_sym(":nnf-mode", symbol("full"));
|
||||
else if (np.m_nnf_mode == NNF_QUANT)
|
||||
p.set_sym(":nnf-mode", symbol("quantifiers"));
|
||||
|
||||
if (np.m_nnf_ignore_labels)
|
||||
p.set_bool(":nnf-ignore-labels", true);
|
||||
|
||||
if (np.m_nnf_sk_hack)
|
||||
p.set_bool(":nnf-sk-hack", true);
|
||||
m_imp = alloc(imp, m, n, p);
|
||||
}
|
||||
|
||||
nnf::~nnf() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
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";);
|
||||
}
|
||||
|
||||
void nnf::updt_params(params_ref const & p) {
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
void nnf::get_param_descrs(param_descrs & r) {
|
||||
imp::get_param_descrs(r);
|
||||
}
|
||||
|
||||
void nnf::set_cancel(bool f) {
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
|
||||
void nnf::reset() {
|
||||
m_imp->reset();
|
||||
}
|
||||
|
||||
void nnf::reset_cache() {
|
||||
m_imp->reset_cache();
|
||||
}
|
||||
|
||||
54
src/ast/normal_forms/nnf.h
Normal file
54
src/ast/normal_forms/nnf.h
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
nnf.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Negation Normal Form & Skolemization
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-11
|
||||
|
||||
Notes:
|
||||
Major revision on 2011-10-06
|
||||
|
||||
--*/
|
||||
#ifndef _NNF_H_
|
||||
#define _NNF_H_
|
||||
|
||||
#include"ast.h"
|
||||
#include"nnf_params.h"
|
||||
#include"params.h"
|
||||
#include"defined_names.h"
|
||||
|
||||
class nnf {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
public:
|
||||
nnf(ast_manager & m, defined_names & n, params_ref const & p = params_ref());
|
||||
nnf(ast_manager & m, defined_names & n, nnf_params & params); // for backward compatibility
|
||||
~nnf();
|
||||
|
||||
void operator()(expr * n, // [IN] expression that should be put into NNF
|
||||
expr_ref_vector & new_defs, // [OUT] new definitions
|
||||
proof_ref_vector & new_def_proofs, // [OUT] proofs of the new definitions
|
||||
expr_ref & r, // [OUT] resultant expression
|
||||
proof_ref & p // [OUT] proof for (~ n r)
|
||||
);
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
|
||||
void cancel() { set_cancel(true); }
|
||||
void reset_cancel() { set_cancel(false); }
|
||||
void set_cancel(bool f);
|
||||
|
||||
void reset();
|
||||
void reset_cache();
|
||||
};
|
||||
|
||||
#endif /* _NNF_H_ */
|
||||
385
src/ast/normal_forms/pull_quant.cpp
Normal file
385
src/ast/normal_forms/pull_quant.cpp
Normal file
|
|
@ -0,0 +1,385 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pull_quant.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Pull nested quantifiers.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-20
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"pull_quant.h"
|
||||
#include"ast_pp.h"
|
||||
#include"for_each_expr.h"
|
||||
|
||||
void pull_quant::pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
|
||||
ptr_buffer<sort> var_sorts;
|
||||
buffer<symbol> var_names;
|
||||
symbol qid;
|
||||
int w = INT_MAX;
|
||||
|
||||
// The input formula is in Skolem normal form...
|
||||
// So all children are forall (positive context) or exists (negative context).
|
||||
// Remark: (AND a1 ...) may be represented (NOT (OR (NOT a1) ...)))
|
||||
// So, when pulling a quantifier over a NOT, it becomes an exists.
|
||||
|
||||
if (m_manager.is_not(d)) {
|
||||
SASSERT(num_children == 1);
|
||||
expr * child = children[0];
|
||||
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));
|
||||
}
|
||||
else {
|
||||
result = m_manager.mk_not(child);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
bool found_quantifier = false;
|
||||
bool forall_children;
|
||||
|
||||
for (unsigned i = 0; i < num_children; i++) {
|
||||
expr * child = children[i];
|
||||
if (is_quantifier(child)) {
|
||||
|
||||
if (!found_quantifier) {
|
||||
found_quantifier = true;
|
||||
forall_children = is_forall(child);
|
||||
}
|
||||
else {
|
||||
// Since the initial formula was in SNF, all children must be EXISTS or FORALL.
|
||||
SASSERT(forall_children == is_forall(child));
|
||||
}
|
||||
|
||||
quantifier * nested_q = to_quantifier(child);
|
||||
if (var_sorts.empty()) {
|
||||
// use the qid of one of the nested quantifiers.
|
||||
qid = nested_q->get_qid();
|
||||
}
|
||||
w = std::min(w, nested_q->get_weight());
|
||||
unsigned j = nested_q->get_num_decls();
|
||||
while (j > 0) {
|
||||
--j;
|
||||
var_sorts.push_back(nested_q->get_decl_sort(j));
|
||||
symbol s = nested_q->get_decl_name(j);
|
||||
if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
|
||||
var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str()));
|
||||
else
|
||||
var_names.push_back(s);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!var_sorts.empty()) {
|
||||
SASSERT(found_quantifier);
|
||||
// adjust the variable ids in formulas in new_children
|
||||
expr_ref_buffer new_adjusted_children(m_manager);
|
||||
expr_ref adjusted_child(m_manager);
|
||||
unsigned num_decls = var_sorts.size();
|
||||
unsigned shift_amount = 0;
|
||||
TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";);
|
||||
for (unsigned i = 0; i < num_children; i++) {
|
||||
expr * child = children[i];
|
||||
if (!is_quantifier(child)) {
|
||||
// increment the free variables in child by num_decls because
|
||||
// child will be in the scope of num_decls bound variables.
|
||||
m_shift(child, num_decls, adjusted_child);
|
||||
TRACE("pull_quant", tout << "shifted by: " << num_decls << "\n" <<
|
||||
mk_pp(child, m_manager) << "\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
|
||||
}
|
||||
else {
|
||||
quantifier * nested_q = to_quantifier(child);
|
||||
SASSERT(num_decls >= nested_q->get_num_decls());
|
||||
// Assume nested_q is of the form
|
||||
// forall xs. P(xs, ys)
|
||||
// where xs (ys) represents the set of bound (free) variables.
|
||||
//
|
||||
// - the index of the variables xs must be increased by shift_amount.
|
||||
// That is, the number of new bound variables that will precede the bound
|
||||
// variables xs.
|
||||
//
|
||||
// - the index of the variables ys must be increased by num_decls - nested_q->get_num_decls.
|
||||
// That is, the total number of new bound variables that will be in the scope
|
||||
// of nested_q->get_expr().
|
||||
m_shift(nested_q->get_expr(),
|
||||
nested_q->get_num_decls(), // bound for shift1/shift2
|
||||
num_decls - nested_q->get_num_decls(), // shift1 (shift by this ammount if var idx >= bound)
|
||||
shift_amount, // shift2 (shift by this ammount if var idx < bound)
|
||||
adjusted_child);
|
||||
TRACE("pull_quant", tout << "shifted bound: " << nested_q->get_num_decls() << " shift1: " << shift_amount <<
|
||||
" shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m_manager) <<
|
||||
"\n---->\n" << mk_pp(adjusted_child, m_manager) << "\n";);
|
||||
shift_amount += nested_q->get_num_decls();
|
||||
}
|
||||
new_adjusted_children.push_back(adjusted_child);
|
||||
}
|
||||
|
||||
// Remark: patterns are ignored.
|
||||
// This is ok, since this functor is used in one of the following cases:
|
||||
//
|
||||
// 1) Superposition calculus is being used, so the
|
||||
// patterns are useless.
|
||||
//
|
||||
// 2) No patterns were provided, and the functor is used
|
||||
// to increase the effectiveness of the pattern inference
|
||||
// procedure.
|
||||
//
|
||||
// 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,
|
||||
var_sorts.size(),
|
||||
var_sorts.c_ptr(),
|
||||
var_names.c_ptr(),
|
||||
m_manager.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
|
||||
w,
|
||||
qid);
|
||||
}
|
||||
else {
|
||||
SASSERT(!found_quantifier);
|
||||
result = m_manager.mk_app(d, num_children, children);
|
||||
}
|
||||
}
|
||||
|
||||
void pull_quant::pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {
|
||||
// The original formula was in SNF, so the original quantifiers must be universal.
|
||||
SASSERT(is_forall(q));
|
||||
if (is_forall(new_expr)) {
|
||||
quantifier * nested_q = to_quantifier(new_expr);
|
||||
ptr_buffer<sort> var_sorts;
|
||||
buffer<symbol> var_names;
|
||||
var_sorts.append(q->get_num_decls(), const_cast<sort**>(q->get_decl_sorts()));
|
||||
var_sorts.append(nested_q->get_num_decls(), const_cast<sort**>(nested_q->get_decl_sorts()));
|
||||
var_names.append(q->get_num_decls(), const_cast<symbol*>(q->get_decl_names()));
|
||||
var_names.append(nested_q->get_num_decls(), const_cast<symbol*>(nested_q->get_decl_names()));
|
||||
// Remark: patterns are ignored.
|
||||
// See comment in reduce1_app
|
||||
result = m_manager.mk_forall(var_sorts.size(),
|
||||
var_sorts.c_ptr(),
|
||||
var_names.c_ptr(),
|
||||
nested_q->get_expr(),
|
||||
std::min(q->get_weight(), nested_q->get_weight()),
|
||||
q->get_qid());
|
||||
}
|
||||
else {
|
||||
SASSERT(!is_quantifier(new_expr));
|
||||
result = m_manager.update_quantifier(q, new_expr);
|
||||
}
|
||||
}
|
||||
|
||||
void pull_quant::pull_quant1(expr * n, expr_ref & result) {
|
||||
if (is_app(n))
|
||||
pull_quant1(to_app(n)->get_decl(), to_app(n)->get_num_args(), to_app(n)->get_args(), result);
|
||||
else if (is_quantifier(n))
|
||||
pull_quant1(to_quantifier(n), to_quantifier(n)->get_expr(), result);
|
||||
else
|
||||
result = n;
|
||||
}
|
||||
|
||||
// Code for proof generation...
|
||||
void pull_quant::pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
|
||||
pr = 0;
|
||||
if (is_app(n)) {
|
||||
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);
|
||||
pull_quant1(arg , new_arg);
|
||||
new_args.push_back(new_arg);
|
||||
if (new_arg != arg)
|
||||
proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
|
||||
}
|
||||
pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
|
||||
proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
}
|
||||
}
|
||||
else if (is_quantifier(n)) {
|
||||
expr_ref new_expr(m_manager);
|
||||
pull_quant1(to_quantifier(n)->get_expr(), new_expr);
|
||||
pull_quant1(to_quantifier(n), new_expr, r);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
|
||||
proof * p1 = 0;
|
||||
if (n != q1) {
|
||||
proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr));
|
||||
p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
|
||||
}
|
||||
proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
}
|
||||
}
|
||||
else {
|
||||
r = n;
|
||||
}
|
||||
}
|
||||
|
||||
bool pull_quant::visit_children(expr * n) {
|
||||
bool visited = true;
|
||||
unsigned j;
|
||||
switch(n->get_kind()) {
|
||||
case AST_APP:
|
||||
// This transformation is also applied after the formula
|
||||
// has been converted into a SNF using only OR and NOT.
|
||||
if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) {
|
||||
j = to_app(n)->get_num_args();
|
||||
while (j > 0) {
|
||||
--j;
|
||||
visit(to_app(n)->get_arg(j), visited);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// This class assumes the formula is in skolem normal form.
|
||||
SASSERT(!has_quantifiers(n));
|
||||
}
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
if (to_quantifier(n)->is_forall())
|
||||
visit(to_quantifier(n)->get_expr(), visited);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return visited;
|
||||
}
|
||||
|
||||
void pull_quant::reduce1(expr * n) {
|
||||
switch(n->get_kind()) {
|
||||
case AST_APP:
|
||||
reduce1_app(to_app(n));
|
||||
break;
|
||||
case AST_VAR:
|
||||
cache_result(n, n, 0);
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
reduce1_quantifier(to_quantifier(n));
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
void pull_quant::reduce1_app(app * n) {
|
||||
if (m_manager.is_or(n) || m_manager.is_and(n) || m_manager.is_not(n)) {
|
||||
ptr_buffer<expr> new_children;
|
||||
ptr_buffer<proof> new_children_proofs;
|
||||
unsigned num = n->get_num_args();
|
||||
for (unsigned i = 0; i < num; i++) {
|
||||
expr * new_child = 0;
|
||||
proof * new_child_pr = 0;
|
||||
get_cached(n->get_arg(i), new_child, new_child_pr);
|
||||
new_children.push_back(new_child);
|
||||
if (new_child_pr) {
|
||||
new_children_proofs.push_back(new_child_pr);
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref r(m_manager);
|
||||
pull_quant1(n->get_decl(), new_children.size(), new_children.c_ptr(), r);
|
||||
proof * pr = 0;
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
app * n_prime = m_manager.mk_app(n->get_decl(), new_children.size(), new_children.c_ptr());
|
||||
TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n";
|
||||
tout << mk_pp(n_prime, m_manager) << "\n";);
|
||||
proof * p1 = n == n_prime ? 0 : m_manager.mk_congruence(n, n_prime,
|
||||
new_children_proofs.size(), new_children_proofs.c_ptr());
|
||||
proof * p2 = n_prime == r ? 0 : m_manager.mk_pull_quant(n_prime, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
}
|
||||
cache_result(n, r, pr);
|
||||
return;
|
||||
}
|
||||
TRACE("proof_bug", tout << mk_pp(n, m_manager) << "\n";);
|
||||
cache_result(n, n, 0);
|
||||
}
|
||||
|
||||
void pull_quant::reduce1_quantifier(quantifier * q) {
|
||||
if (q->is_forall()) {
|
||||
expr * new_expr;
|
||||
proof * new_expr_pr;
|
||||
get_cached(q->get_expr(), new_expr, new_expr_pr);
|
||||
expr_ref r(m_manager);
|
||||
pull_quant1(q, new_expr, r);
|
||||
proof * pr = 0;
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
quantifier * q_prime = m_manager.update_quantifier(q, new_expr);
|
||||
proof * p1 = q == q_prime ? 0 : m_manager.mk_quant_intro(q, q_prime, new_expr_pr);
|
||||
proof * p2 = q_prime == r ? 0 : m_manager.mk_pull_quant(q_prime, to_quantifier(r));
|
||||
pr = m_manager.mk_transitivity(p1, p2);
|
||||
}
|
||||
cache_result(q, r, pr);
|
||||
return;
|
||||
}
|
||||
// should be unreachable, right?
|
||||
UNREACHABLE();
|
||||
cache_result(q, q, 0);
|
||||
}
|
||||
|
||||
pull_quant::pull_quant(ast_manager & m):
|
||||
base_simplifier(m),
|
||||
m_shift(m) {
|
||||
}
|
||||
|
||||
void pull_quant::operator()(expr * n, expr_ref & r, proof_ref & p) {
|
||||
flush_cache();
|
||||
m_todo.push_back(n);
|
||||
while (!m_todo.empty()) {
|
||||
expr * n = m_todo.back();
|
||||
if (is_cached(n))
|
||||
m_todo.pop_back();
|
||||
else if (visit_children(n)) {
|
||||
m_todo.pop_back();
|
||||
reduce1(n);
|
||||
}
|
||||
}
|
||||
|
||||
expr * result;
|
||||
proof * result_proof;
|
||||
get_cached(n, result, result_proof);
|
||||
|
||||
r = result;
|
||||
|
||||
switch (m_manager.proof_mode()) {
|
||||
case PGM_DISABLED:
|
||||
p = m_manager.mk_undef_proof();
|
||||
break;
|
||||
case PGM_COARSE:
|
||||
if (result == n)
|
||||
p = m_manager.mk_reflexivity(n);
|
||||
else
|
||||
p = m_manager.mk_pull_quant_star(n, to_quantifier(result));
|
||||
break;
|
||||
case PGM_FINE:
|
||||
SASSERT(result_proof || result == n);
|
||||
p = result_proof ? result_proof : m_manager.mk_reflexivity(n);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
bool pull_nested_quant::visit_quantifier(quantifier * q) {
|
||||
// do not recurse.
|
||||
return true;
|
||||
}
|
||||
|
||||
void pull_nested_quant::reduce1_quantifier(quantifier * q) {
|
||||
expr_ref r(m_manager);
|
||||
proof_ref pr(m_manager);
|
||||
m_pull(q, r, pr);
|
||||
cache_result(q, r, pr);
|
||||
}
|
||||
67
src/ast/normal_forms/pull_quant.h
Normal file
67
src/ast/normal_forms/pull_quant.h
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
/*++
|
||||
Copyright (c) 2007 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
pull_quant.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Pull nested quantifiers.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2008-01-20
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _PULL_QUANT_H_
|
||||
#define _PULL_QUANT_H_
|
||||
|
||||
#include"simplifier.h"
|
||||
#include"var_subst.h"
|
||||
|
||||
/**
|
||||
\brief Pull nested quantifiers in a formula.
|
||||
|
||||
\warning It assumes the input formula is in NNF.
|
||||
|
||||
\remark pull_quant(F) is a quantifier if F contains a quantifier.
|
||||
|
||||
\remark If pull_quant(F) is a quantifier then its weight is
|
||||
Min{weight(Q') | Q' is a quantifier nested in F}
|
||||
*/
|
||||
class pull_quant : public base_simplifier {
|
||||
protected:
|
||||
shift_vars m_shift;
|
||||
bool visit_children(expr * n);
|
||||
void reduce1(expr *);
|
||||
void reduce1_app(app * n);
|
||||
void reduce1_quantifier(quantifier * q);
|
||||
|
||||
public:
|
||||
pull_quant(ast_manager & m);
|
||||
virtual ~pull_quant() {}
|
||||
void operator()(expr * n, expr_ref & r, proof_ref & p);
|
||||
void reset() { flush_cache(); }
|
||||
void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result);
|
||||
void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result);
|
||||
void pull_quant1(expr * n, expr_ref & result);
|
||||
void pull_quant2(expr * n, expr_ref & r, proof_ref & pr);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief After applying this transformation the formula will not
|
||||
contain nested quantifiers.
|
||||
*/
|
||||
class pull_nested_quant : public simplifier {
|
||||
pull_quant m_pull;
|
||||
virtual bool visit_quantifier(quantifier * q);
|
||||
virtual void reduce1_quantifier(quantifier * q);
|
||||
public:
|
||||
pull_nested_quant(ast_manager & m):simplifier(m), m_pull(m) { enable_ac_support(false); }
|
||||
virtual ~pull_nested_quant() {}
|
||||
};
|
||||
|
||||
#endif /* _PULL_QUANT_H_ */
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
#include "proof_checker.h"
|
||||
#include "ast_ll_pp.h"
|
||||
#include "ast_pp.h"
|
||||
#include "spc_decl_plugin.h"
|
||||
// include "spc_decl_plugin.h"
|
||||
#include "ast_smt_pp.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "front_end_params.h"
|
||||
|
|
@ -86,7 +86,7 @@ proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked
|
|||
m.register_plugin(fam_name, alloc(hyp_decl_plugin));
|
||||
}
|
||||
m_hyp_fid = m.get_family_id(fam_name);
|
||||
m_spc_fid = m.get_family_id("spc");
|
||||
// m_spc_fid = m.get_family_id("spc");
|
||||
m_nil = m_manager.mk_const(m_hyp_fid, OP_NIL);
|
||||
}
|
||||
|
||||
|
|
@ -117,13 +117,16 @@ bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) {
|
|||
if (p->get_family_id() == m_manager.get_basic_family_id()) {
|
||||
return check1_basic(p, side_conditions);
|
||||
}
|
||||
#if 0
|
||||
if (p->get_family_id() == m_spc_fid) {
|
||||
return check1_spc(p, side_conditions);
|
||||
}
|
||||
#endif
|
||||
return false;
|
||||
}
|
||||
|
||||
bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
|
||||
#if 0
|
||||
decl_kind k = p->get_decl_kind();
|
||||
bool is_univ = false;
|
||||
expr_ref fact(m_manager), fml(m_manager);
|
||||
|
|
@ -174,6 +177,9 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
|
|||
UNREACHABLE();
|
||||
}
|
||||
return false;
|
||||
#else
|
||||
return true;
|
||||
#endif
|
||||
}
|
||||
|
||||
bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ class proof_checker {
|
|||
expr_ref_vector m_pinned;
|
||||
obj_map<expr, expr*> m_hypotheses;
|
||||
family_id m_hyp_fid;
|
||||
family_id m_spc_fid;
|
||||
// family_id m_spc_fid;
|
||||
app_ref m_nil;
|
||||
bool m_dump_lemmas;
|
||||
std::string m_logic;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue