mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix #1874 by removing nnf.skolemize option

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-14 18:17:34 -07:00
parent 70f3fa36c5
commit 5b51e69137
5 changed files with 47 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -258,7 +258,6 @@ struct nnf::imp {
// configuration ----------------
nnf_mode m_mode;
bool m_ignore_labels;
bool m_skolemize;
// ------------------------------
name_exprs * m_name_nested_formulas;
@ -312,7 +311,6 @@ struct nnf::imp {
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
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());
}
@ -759,7 +757,7 @@ struct nnf::imp {
if (!visit(q->get_expr(), fr.m_pol, true))
return false;
}
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
else if (is_forall(q) == fr.m_pol) {
if (!visit(q->get_expr(), fr.m_pol, true))
return false;
}
@ -788,7 +786,7 @@ struct nnf::imp {
}
return true;
}
else if (is_forall(q) == fr.m_pol || !m_skolemize) {
else if (is_forall(q) == fr.m_pol) {
expr * new_expr = m_result_stack.back();
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr;

3
src/ast/normal_forms/nnf_params.pyg
View file

@ -5,5 +5,4 @@ def_module_params('nnf',
('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')))
('ignore_labels', BOOL, False, 'remove/ignore labels in the input formula, this option is ignored if proofs are enabled')))

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

@ -24,11 +24,11 @@ Notes:
struct pull_quant::imp {
struct rw_cfg : public default_rewriter_cfg {
ast_manager & m_manager;
ast_manager & m;
shift_vars m_shift;
rw_cfg(ast_manager & m):
m_manager(m),
m(m),
m_shift(m) {
}
@ -43,14 +43,14 @@ struct pull_quant::imp {
// 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)) {
if (m.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();
quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k;
result = m_manager.update_quantifier(q, k, m_manager.mk_not(body));
result = m.update_quantifier(q, k, m.mk_not(body));
return true;
}
else {
@ -86,7 +86,7 @@ struct pull_quant::imp {
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() ? nullptr : s.bare_str()));
var_names.push_back(m.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str()));
else
var_names.push_back(s);
}
@ -96,8 +96,8 @@ struct pull_quant::imp {
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);
expr_ref_buffer new_adjusted_children(m);
expr_ref adjusted_child(m);
unsigned num_decls = var_sorts.size();
unsigned shift_amount = 0;
TRACE("pull_quant", tout << "Result num decls:" << num_decls << "\n";);
@ -108,7 +108,7 @@ struct pull_quant::imp {
// 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";);
mk_pp(child, m) << "\n---->\n" << mk_pp(adjusted_child, m) << "\n";);
}
else {
quantifier * nested_q = to_quantifier(child);
@ -130,8 +130,8 @@ struct pull_quant::imp {
shift_amount, // shift2 (shift by this amount 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";);
" shift2: " << (num_decls - nested_q->get_num_decls()) << "\n" << mk_pp(nested_q->get_expr(), m) <<
"\n---->\n" << mk_pp(adjusted_child, m) << "\n";);
shift_amount += nested_q->get_num_decls();
}
new_adjusted_children.push_back(adjusted_child);
@ -150,11 +150,11 @@ struct pull_quant::imp {
// 3) MBQI
std::reverse(var_sorts.begin(), var_sorts.end());
std::reverse(var_names.begin(), var_names.end());
result = m_manager.mk_quantifier(forall_children ? forall_k : exists_k,
result = m.mk_quantifier(forall_children ? forall_k : exists_k,
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()),
m.mk_app(d, new_adjusted_children.size(), new_adjusted_children.c_ptr()),
w,
qid);
return true;
@ -167,7 +167,7 @@ struct pull_quant::imp {
void pull_quant1(func_decl * d, unsigned num_children, expr * const * children, expr_ref & result) {
if (!pull_quant1_core(d, num_children, children, result)) {
result = m_manager.mk_app(d, num_children, children);
result = m.mk_app(d, num_children, children);
}
}
@ -185,7 +185,7 @@ struct pull_quant::imp {
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(),
result = m.mk_forall(var_sorts.size(),
var_sorts.c_ptr(),
var_names.c_ptr(),
nested_q->get_expr(),
@ -201,7 +201,7 @@ struct pull_quant::imp {
}
else {
SASSERT(!is_quantifier(new_expr));
result = m_manager.update_quantifier(q, new_expr);
result = m.update_quantifier(q, new_expr);
}
}
@ -218,36 +218,36 @@ struct pull_quant::imp {
void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
pr = nullptr;
if (is_app(n)) {
expr_ref_buffer new_args(m_manager);
expr_ref new_arg(m_manager);
expr_ref_buffer new_args(m);
expr_ref new_arg(m);
ptr_buffer<proof> proofs;
for (expr * arg : *to_app(n)) {
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)));
proofs.push_back(m.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.proofs_enabled()) {
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
proof * p1 = proofs.empty() ? nullptr : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
proof * p2 = r1 == r ? nullptr : m_manager.mk_pull_quant(r1, to_quantifier(r));
pr = m_manager.mk_transitivity(p1, p2);
if (m.proofs_enabled()) {
app * r1 = m.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
proof * p1 = proofs.empty() ? nullptr : m.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
proof * p2 = r1 == r ? nullptr : m.mk_pull_quant(r1, to_quantifier(r));
pr = m.mk_transitivity(p1, p2);
}
}
else if (is_quantifier(n)) {
expr_ref new_expr(m_manager);
expr_ref new_expr(m);
pull_quant1(to_quantifier(n)->get_expr(), new_expr);
pull_quant1(to_quantifier(n), new_expr, r);
if (m_manager.proofs_enabled()) {
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
if (m.proofs_enabled()) {
quantifier * q1 = m.update_quantifier(to_quantifier(n), new_expr);
proof * p1 = nullptr;
if (n != q1) {
proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr));
p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
proof * p0 = m.mk_pull_quant(n, to_quantifier(new_expr));
p1 = m.mk_quant_intro(to_quantifier(n), q1, p0);
}
proof * p2 = q1 == r ? nullptr : m_manager.mk_pull_quant(q1, to_quantifier(r));
pr = m_manager.mk_transitivity(p1, p2);
proof * p2 = q1 == r ? nullptr : m.mk_pull_quant(q1, to_quantifier(r));
pr = m.mk_transitivity(p1, p2);
}
}
else {
@ -256,14 +256,14 @@ struct pull_quant::imp {
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (!m_manager.is_or(f) && !m_manager.is_and(f) && !m_manager.is_not(f))
if (!m.is_or(f) && !m.is_and(f) && !m.is_not(f))
return BR_FAILED;
if (!pull_quant1_core(f, num, args, result))
return BR_FAILED;
if (m_manager.proofs_enabled()) {
result_pr = m_manager.mk_pull_quant(m_manager.mk_app(f, num, args),
if (m.proofs_enabled()) {
result_pr = m.mk_pull_quant(m.mk_app(f, num, args),
to_quantifier(result.get()));
}
return BR_DONE;
@ -277,8 +277,11 @@ struct pull_quant::imp {
proof_ref & result_pr) {
if (is_exists(old_q)) {
UNREACHABLE();
return false;
result = m.mk_not(new_body);
result = m.mk_not(m.update_quantifier(old_q, exists_k, result));
if (m.proofs_enabled())
m.mk_rewrite(old_q, result);
return true;
}
if (is_lambda(old_q)) {
return false;
@ -288,8 +291,8 @@ struct pull_quant::imp {
return false;
pull_quant1_core(old_q, new_body, result);
if (m_manager.proofs_enabled())
result_pr = m_manager.mk_pull_quant(old_q, to_quantifier(result.get()));
if (m.proofs_enabled())
result_pr = m.mk_pull_quant(old_q, to_quantifier(result.get()));
return true;
}
};

15
src/sat/sat_solver.cpp
View file

@ -1106,6 +1106,10 @@ namespace sat {
m_restart_threshold = m_config.m_restart_initial;
}
if (reached_max_conflicts()) {
return l_undef;
}
// iff3_finder(*this)();
simplify_problem();
if (check_inconsistent()) return l_false;
@ -1718,17 +1722,6 @@ namespace sat {
#endif
}
unsigned solver::get_hash() const {
unsigned result = 0;
for (clause* cp : m_clauses) {
result = combine_hash(cp->size(), combine_hash(result, cp->id()));
}
for (clause* cp : m_learned) {
result = combine_hash(cp->size(), combine_hash(result, cp->id()));
}
return result;
}
bool solver::set_root(literal l, literal r) {
return !m_ext || m_ext->set_root(l, r);
}

2
src/sat/sat_solver.h
View file

@ -569,8 +569,6 @@ namespace sat {
private:
unsigned get_hash() const;
typedef hashtable<unsigned, u_hash, u_eq> index_set;
u_map<index_set> m_antecedents;