mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 01:32:17 +00:00
Code Activity

Reorganizing the code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-20 22:03:58 -07:00
parent 2b8fb6c718
commit 492484c5aa
125 changed files with 632 additions and 390 deletions
Download patch file Download diff file Expand all files Collapse all files

526
src/normal_forms/cnf.cpp Normal file
View 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/normal_forms/cnf.h Normal file
View 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/normal_forms/defined_names.cpp Normal file
View 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/normal_forms/defined_names.h Normal file
View 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_ */

167
src/normal_forms/name_exprs.cpp Normal file
View 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/normal_forms/name_exprs.h Normal file
View 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

1030
src/normal_forms/nnf.cpp Normal file
View file

File diff suppressed because it is too large Load diff

68
src/normal_forms/nnf.h Normal file
View file

@ -0,0 +1,68 @@
/*++
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();
};
// Old strategy framework
class assertion_set_strategy;
// Skolem Normal Form
assertion_set_strategy * mk_snf(params_ref const & p = params_ref());
// Negation Normal Form
assertion_set_strategy * mk_nnf(params_ref const & p = params_ref());
// New strategy framework
class tactic;
// Skolem Normal Form
tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
// Negation Normal Form
tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref());
#endif /* _NNF_H_ */

385
src/normal_forms/pull_quant.cpp Normal file
View 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/normal_forms/pull_quant.h Normal file
View 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_ */