mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

add cnf/nnf simplifier

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-30 23:04:38 -08:00
parent e3e2c21632
commit e5984dd397
2 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/simplifiers/cnf_nnf.h
View file

@ -18,17 +18,20 @@ Author:
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/normal_forms/nnf.h"
#include "ast/rewriter/th_rewriter.h"
class cnf_nnf_simplifier : public dependent_expr_simplifier {
defined_names m_defined_names;
th_rewriter m_rewriter;
public:
cnf_nnf_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
dependent_expr_simplifier(m, fmls),
m_pull(m) {
m_defined_names(m),
m_rewriter(m, p){
}
char const* name() const override { return "cnf-nnf"; }
@ -41,17 +44,21 @@ public:
expr_ref r(m);
unsigned sz = qtail();
for (unsigned i = qhead(); i < sz && m.inc(); ++i) {
auto d = m_fmls[idx];
auto d = m_fmls[i];
push_todo.reset();
push_todo_prs.reset();
apply_nnf(d.fml(), push_todo, push_todo_prs, r, pr);
m_fmls.update(i, dependent_expr(m, r, d.dep()));
for (expr* f : m_push_todo) {
for (expr* f : push_todo) {
if (!m.inc())
break;
m_rewriter(f, r, pr);
m_fmls.add(i, depdendent_expr(m, r, d.dep()));
m_fmls.add(dependent_expr(m, r, d.dep()));
}
}
}
void push() override { dependent_expr_simplifier::push(); m_defined_names.push(); }
void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_defined_names.pop(n); }
};

3
src/sat/sat_solver/sat_smt_preprocess.cpp
View file

@ -34,6 +34,7 @@ Author:
#include "ast/simplifiers/push_ite.h"
#include "ast/simplifiers/elim_term_ite.h"
#include "ast/simplifiers/flatten_clauses.h"
#include "ast/simplifiers/cnf_nnf.h"
#include "sat/sat_params.hpp"
#include "smt/params/smt_params.h"
#include "sat/sat_solver/sat_smt_preprocess.h"
@ -48,6 +49,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
s.add_simplifier(alloc(propagate_values, m, p, st));
s.add_simplifier(alloc(euf::solve_eqs, m, st));
s.add_simplifier(alloc(elim_unconstrained, m, st));
if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
@ -62,6 +64,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
s.add_simplifier(alloc(flatten_clauses, m, p, st));
//
// add:
// euf_completion?