fix bugs in flatten_clauses simplifier, switch proof/fml

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jan 4, 2023 · 6f95c77 · 6f95c77
1 parent d449073
commit 6f95c77
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h
@@ -32,6 +32,7 @@ class dependent_expr {
         m_fml(fml),
         m_proof(p),
         m_dep(d) {
+        SASSERT(fml);
         m.inc_ref(fml);
         m.inc_ref(d);
         m.inc_ref(p);
@@ -122,4 +123,4 @@ class dependent_expr {
 
 inline std::ostream& operator<<(std::ostream& out, dependent_expr const& d) {
     return d.display(out);
-}
+}
diff --git a/src/ast/simplifiers/flatten_clauses.h b/src/ast/simplifiers/flatten_clauses.h
@@ -67,8 +67,8 @@ class flatten_clauses : public dependent_expr_simplifier {
                     decomposed = true;
                 if (decomposed) {
                     for (expr* arg : *to_app(b)) 
-                        m_fmls.add(dependent_expr(m, nullptr, m.mk_or(a, mk_not(m, arg)), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, nullptr, m.mk_true(), nullptr));
+                        m_fmls.add(dependent_expr(m, m.mk_or(a, mk_not(m, arg)), nullptr,  de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, nullptr));
                     ++m_num_flat;
                     continue;
                 }
@@ -79,8 +79,8 @@ class flatten_clauses : public dependent_expr_simplifier {
                     decomposed = true;
                 if (decomposed) {
                     for (expr * arg : *to_app(b))
-                        m_fmls.add(dependent_expr(m, nullptr, m.mk_or(a, arg), de.dep()));
-                    m_fmls.update(idx, dependent_expr(m, nullptr, m.mk_true(), nullptr));
+                        m_fmls.add(dependent_expr(m, m.mk_or(a, arg), nullptr,  de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr,  nullptr));
                     ++m_num_flat;
                     continue;
                 }

diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp
@@ -56,7 +56,7 @@ class sat_smt_solver : public solver {
         ~dep_expr_state() override {}
         virtual unsigned qtail() const override { return s.m_fmls.size(); }
         dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
-        void update(unsigned i, dependent_expr const& j) override { s.m_fmls[i] = j; }
+        void update(unsigned i, dependent_expr const& j) override { SASSERT(j.fml());  s.m_fmls[i] = j; }
         void add(dependent_expr const& j) override { s.m_fmls.push_back(j); }
         bool inconsistent() override { return s.m_solver.inconsistent(); }
         model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }

diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
@@ -48,7 +48,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         dependent_expr_state(m),
         m(m),
         m_params(p),
-        m_dep(m, nullptr, nullptr, nullptr),
+        m_dep(m, m.mk_true(), nullptr, nullptr),
         m_factory(f)
     {}
 
@@ -129,7 +129,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         m_simp = nullptr;
         m_model_trail = nullptr;
         m_goal = nullptr;
-        m_dep = dependent_expr(m, nullptr, nullptr, nullptr);
+        m_dep = dependent_expr(m, m.mk_true(), nullptr, nullptr);
     }
 
     void collect_statistics(statistics & st) const override {