From e5984dd3979ece320b465e5ed65538ae644e737b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 30 Nov 2022 23:04:38 -0800
Subject: [PATCH] add cnf/nnf simplifier

---
 src/ast/simplifiers/cnf_nnf.h             | 17 ++++++++++++-----
 src/sat/sat_solver/sat_smt_preprocess.cpp |  3 +++
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/ast/simplifiers/cnf_nnf.h b/src/ast/simplifiers/cnf_nnf.h
index eb80387d6..56cdc1367 100644
--- a/src/ast/simplifiers/cnf_nnf.h
+++ b/src/ast/simplifiers/cnf_nnf.h
@@ -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); }
 };
diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp
index e3d6b3edb..7c716c481 100644
--- a/src/sat/sat_solver/sat_smt_preprocess.cpp
+++ b/src/sat/sat_solver/sat_smt_preprocess.cpp
@@ -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?