From 773d938925c6be6c7afc7ff1a4c861c45a3b55b9 Mon Sep 17 00:00:00 2001
From: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
Date: Tue, 21 Nov 2017 13:24:14 -0800
Subject: [PATCH] re-adding simplified constraints based on model converter

Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
---
 src/sat/tactic/goal2sat.cpp            | 34 ++++++++++++++++++++++++--
 src/tactic/generic_model_converter.cpp |  2 +-
 2 files changed, 33 insertions(+), 3 deletions(-)

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 7c703653c..dc4200349 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -885,7 +885,8 @@ struct sat2goal::imp {
         sat::model_converter         m_mc;
         expr_ref_vector              m_var2expr;
         generic_model_converter_ref  m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
-        
+        generic_model_converter_ref  m_imc; // used to ensure correctness in incremental calls with simplifications that require model conversions
+
         sat_model_converter(ast_manager & m):
             m_var2expr(m) {
         }
@@ -894,6 +895,7 @@ struct sat2goal::imp {
         sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
             m_mc.copy(s.get_model_converter());
             m_fmc = alloc(generic_model_converter, m);
+            m_imc = nullptr;
         }
         
         ast_manager & m() { return m_var2expr.get_manager(); }
@@ -920,6 +922,7 @@ struct sat2goal::imp {
                     insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true);
                 }
             }
+            m_imc = nullptr;
         }
         
         virtual void operator()(model_ref & md) {
@@ -1026,7 +1029,34 @@ struct sat2goal::imp {
         }
 
         void operator()(expr_ref& formula) override {
-            NOT_IMPLEMENTED_YET();
+            if (!m_imc) {
+                m_imc = alloc(generic_model_converter, m());
+                sat::literal_vector updates;
+                m_mc.expand(updates);
+                sat::literal_vector clause;
+                expr_ref_vector tail(m());
+                expr_ref def(m());
+                for (sat::literal l : updates) {
+                    if (l == sat::null_literal) {
+                        sat::literal lit0 = clause[0];
+                        for (unsigned i = 1; i < clause.size(); ++i) {
+                            tail.push_back(lit2expr(~clause[i]));
+                        }
+                        def = m().mk_or(lit2expr(lit0), mk_and(tail));
+                        if (lit0.sign()) {
+                            lit0.neg();
+                            def = m().mk_not(def);
+                        }
+                        m_imc->add(lit2expr(lit0), def);
+                        clause.reset();
+                        tail.reset();
+                    }
+                    else {
+                        clause.push_back(l);
+                    }
+                }
+            }
+            (*m_imc)(formula);
         }
     };
 
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index aeec97260..19caa62ac 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -104,7 +104,6 @@ void generic_model_converter::operator()(expr_ref& fml) {
     unsigned min_idx = min_proc.m_min;
     for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
         entry const& e = m_add_entries[i];
-        m_add_entries.pop_back();
         unsigned arity = e.m_f->get_arity();
         if (arity == 0) {
             fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def));
@@ -115,5 +114,6 @@ void generic_model_converter::operator()(expr_ref& fml) {
         if (m_first_idx[e.m_f] == i) {
             m_first_idx.remove(e.m_f);
         }
+        m_add_entries.pop_back();
     }
 }