mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

merged

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-06 11:05:49 -08:00
commit 9ab1210cc2
518 changed files with 21452 additions and 22650 deletions
Download patch file Download diff file Expand all files Collapse all files

524
src/ast/normal_forms/cnf.cpp
View file

@ -1,524 +0,0 @@
/*++
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"var_subst.h"
#include"ast_util.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);
if (is_too_expensive(result_size, f_args)) {
name_args(f_args, cheap_args, cheap_args_pr);
}
else {
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
View file

@ -1,121 +0,0 @@
/*++
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_ */

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

@ -18,6 +18,7 @@ Notes:
--*/
#include"nnf.h"
#include"nnf_params.hpp"
#include"warning.h"
#include"used_vars.h"
#include"well_sorted.h"
@ -29,6 +30,40 @@ Notes:
#include"ast_smt2_pp.h"
/**
\brief NNF translation mode. The cheapest mode is NNF_SKOLEM, and
the most expensive is NNF_FULL.
*/
enum nnf_mode {
NNF_SKOLEM, /* A subformula is put into NNF only if it contains
quantifiers or labels. The result of the
transformation will be in skolem normal form.
If a formula is too expensive to be put into NNF,
then nested quantifiers and labels are renamed.
This mode is sufficient when using E-matching.
*/
NNF_QUANT, /* A subformula is put into NNF if it contains
quantifiers, labels, or is in the scope of a
quantifier. The result of the transformation will be
in skolem normal form, and the body of quantifiers
will be in NNF. If a ground formula is too expensive to
be put into NNF, then nested quantifiers and labels
are renamed.
This mode is sufficient when using Superposition
Calculus.
Remark: If the problem does not contain quantifiers,
then NNF_QUANT is identical to NNF_SKOLEM.
*/
NNF_OPPORTUNISTIC, /* Similar to NNF_QUANT, but a subformula is
also put into NNF, if it is
cheap. Otherwise, the nested quantifiers and
labels are renamed. */
NNF_FULL /* Everything is put into NNF. */
};
class skolemizer {
typedef act_cache cache;
@ -112,20 +147,16 @@ class skolemizer {
}
public:
skolemizer(ast_manager & m, params_ref const & p):
skolemizer(ast_manager & m):
m_manager(m),
m_sk_hack("sk_hack"),
m_sk_hack_enabled(false),
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");
void set_sk_hack(bool f) {
m_sk_hack_enabled = f;
}
ast_manager & m() const { return m_manager; }
@ -219,8 +250,6 @@ struct nnf::imp {
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
@ -230,10 +259,9 @@ struct nnf::imp {
m_todo_defs(m),
m_todo_proofs(m),
m_result_pr_stack(m),
m_skolemizer(m, p),
m_skolem("skolem"),
m_skolemizer(m),
m_cancel(false) {
updt_local_params(p);
updt_params(p);
for (unsigned i = 0; i < 4; i++) {
m_cache[i] = alloc(act_cache, m);
if (m.proofs_enabled())
@ -257,14 +285,10 @@ struct nnf::imp {
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)
void updt_params(params_ref const & _p) {
nnf_params p(_p);
symbol mode_sym = p.mode();
if (mode_sym == "skolem")
m_mode = NNF_SKOLEM;
else if (mode_sym == "full")
m_mode = NNF_FULL;
@ -272,23 +296,17 @@ struct nnf::imp {
m_mode = NNF_QUANT;
else
throw nnf_params_exception("invalid NNF mode");
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
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));
m_ignore_labels = p.ignore_labels();
m_skolemize = p.skolemize();
m_max_memory = megabytes_to_bytes(p.max_memory());
m_skolemizer.set_sk_hack(p.sk_hack());
}
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);
nnf_params::collect_param_descrs(r);
}
void reset() {
@ -880,21 +898,6 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) {
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);
}

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

@ -21,7 +21,6 @@ Notes:
#define _NNF_H_
#include"ast.h"
#include"nnf_params.h"
#include"params.h"
#include"defined_names.h"
@ -30,7 +29,6 @@ class nnf {
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
@ -41,6 +39,9 @@ public:
);
void updt_params(params_ref const & p);
/*
REG_MODULE_PARAMS('nnf', 'nnf::get_param_descrs')
*/
static void get_param_descrs(param_descrs & r);
void cancel() { set_cancel(true); }

9
src/ast/normal_forms/nnf_params.pyg Normal file
View file

@ -0,0 +1,9 @@
def_module_params('nnf',
description='negation normal form',
export=True,
params=(max_memory_param(),
('sk_hack', BOOL, False, 'hack for VCC'),
('mode', SYMBOL, 'skolem',
'NNF translation mode: skolem (skolem normal form), quantifiers (skolem normal form + quantifiers in NNF), full'),
('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled'),
('skolemize', BOOL, True, 'skolemize (existential force) quantifiers')))