fix model conversion bugs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/cmd_context/cmd_context.cpp

@@ -1419,7 +1419,9 @@ void cmd_context::restore_assertions(unsigned old_sz) {
         SASSERT(m_assertions.empty());
         return;
     }
-    SASSERT(old_sz <= m_assertions.size());
+    if (old_sz == m_assertions.size())
+        return;
+    SASSERT(old_sz < m_assertions.size());
     SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
     restore(m(), m_assertions, old_sz);
     if (produce_unsat_cores())
@@ -1520,7 +1522,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     }
     display_sat_result(r);
     if (r == l_true) {
-        complete_model();
         validate_model();
     }
     validate_check_sat_result(r);
@@ -1528,9 +1529,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         // get_opt()->display_assignment(regular_stream());
     }
 
-    if (r == l_true && m_params.m_dump_models) {
+    model_ref md;
-        model_ref md;
+    if (r == l_true && m_params.m_dump_models && is_model_available(md)) {
-        get_check_sat_result()->get_model(md);
         display_model(md);
     }
 }
@@ -1695,14 +1695,10 @@ struct contains_underspecified_op_proc {
 /**
     \brief Complete the model if necessary.
 */
-void cmd_context::complete_model() {
+void cmd_context::complete_model(model_ref& md) const {
-    model_ref md;
+    if (gparams::get_value("model.completion") != "true" || !md.get())
-    if (!is_model_available(md) ||
-        gparams::get_value("model.completion") != "true")
         return;
 
-    get_check_sat_result()->get_model(md);
-    SASSERT(md.get() != 0);
     params_ref p;
     p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
     p.set_uint("sort_store", true);
@@ -1770,7 +1766,6 @@ void cmd_context::validate_model() {
         return;
     if (!is_model_available(md))
         return;
-    get_check_sat_result()->get_model(md);
     SASSERT(md.get() != 0);
     params_ref p;
     p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree.
@@ -1902,6 +1897,7 @@ bool cmd_context::is_model_available(model_ref& md) const {
         has_manager() &&
         (cs_state() == css_sat || cs_state() == css_unknown)) {
         get_check_sat_result()->get_model(md);
+        complete_model(md);
         return md.get() != 0;
     }
     return false;

src/cmd_context/cmd_context.h

@@ -365,7 +365,7 @@ public:
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
-    void complete_model();
+    void complete_model(model_ref& mdl) const;
     void validate_model();
     void display_model(model_ref& mdl);
 

src/cmd_context/pdecl.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "cmd_context/pdecl.h"
 #include "ast/datatype_decl_plugin.h"
+#include <sstream>
 using namespace format_ns;
 
 class psort_inst_cache {
@@ -866,8 +867,6 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
 }
 
 psort * pdecl_manager::register_psort(psort * n) {
-    enable_trace("register_psort");
-    TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
     psort * r = m_table.insert_if_not_there(n);
     if (r != n) {
         del_decl_core(n);
@@ -947,7 +946,6 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
-enable_trace("register_psort");
     TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";);   
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);

src/sat/sat_model_converter.cpp

@@ -347,6 +347,17 @@ namespace sat {
         return result;
     }
 
+    void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) {
+        for (unsigned j = 0; j < sz; ++j) {
+            if (v == clause[j].var()) {
+                std::swap(clause[0], clause[j]);
+                return;
+            }
+        }
+        IF_VERBOSE(0, verbose_stream() << "not found: v" << v << " " << clause << "\n";);
+        UNREACHABLE();
+    }
+
     void model_converter::expand(literal_vector& update_stack) {
         sat::literal_vector clause;
         for (entry const& e : m_entries) {
@@ -357,34 +368,23 @@ namespace sat {
                 if (l == null_literal) {
                     elim_stack* st = e.m_elim_stack[index];                    
                     if (st) {
-                        // clause sizes increase
+                        // clause sizes increase, so we can always swap
-                        elim_stackv const& stack = st->stack();
+                        // the blocked literal to the front from the prefix.
-                        unsigned sz = stack.size();
+                        for (auto const& p : st->stack()) {
-                        for (unsigned i = 0; i < sz; ++i) {
+                            unsigned csz = p.first;
-                            unsigned csz = stack[i].first;
+                            literal lit = p.second;
-                            literal lit = stack[i].second;
+                            swap(lit.var(), csz, clause);
-                            BOOL found = false;
-                            unsigned j = 0;
-                            for (j = 0; j < csz; ++j) {
-                                if (clause[j] == lit) {
-                                    std::swap(clause[j], clause[0]);
-                                    found = true;
-                                    break;
-                                }
-                            }
-                            SASSERT(found);
                             update_stack.append(csz, clause.c_ptr());
                             update_stack.push_back(null_literal);
                         }
                     }
+                    swap(e.var(), clause.size(), clause);
                     update_stack.append(clause);
                     update_stack.push_back(null_literal);
                     clause.reset();
-                    continue;
                 }
-                clause.push_back(l);
+                else {
-                if (l.var() == e.var()) {
+                    clause.push_back(l);
-                    std::swap(clause[0], clause.back());
                 }
             }
         }

src/sat/sat_model_converter.h

@@ -94,6 +94,8 @@ namespace sat {
 
         bool legal_to_flip(bool_var v) const;
 
+        void swap(bool_var v, unsigned sz, literal_vector& clause);
+
     public:
         model_converter();
         ~model_converter();

src/sat/sat_simplifier.cpp

@@ -231,7 +231,7 @@ namespace sat {
         if (bce_enabled() || abce_enabled() || bca_enabled()) {
             elim_blocked_clauses();
         }
-        si.check_watches();
+        if (!m_need_cleanup) si.check_watches();
 
         if (!learned) {
             m_num_calls++;
@@ -680,7 +680,7 @@ namespace sat {
     }
 
     void simplifier::elim_lit(clause & c, literal l) {
-        TRACE("elim_lit", tout << "processing: " << c << "\n";);
+        TRACE("elim_lit", tout << "processing: " << l << " @ " << c << "\n";);
         m_need_cleanup = true;
         m_num_elim_lits++;
         insert_elim_todo(l.var());
@@ -979,23 +979,23 @@ namespace sat {
 
         void operator()() {
             integrity_checker si(s.s);
-            si.check_watches();
+            //si.check_watches();
             if (s.bce_enabled()) {
                 block_clauses();
             }
-            si.check_watches();
+            //si.check_watches();
             if (s.abce_enabled()) {
                 cce<false>();
             }
-            si.check_watches();
+            //si.check_watches();
             if (s.cce_enabled()) {
                 cce<true>();
             }
-            si.check_watches();
+            //si.check_watches();
             if (s.bca_enabled()) {
                 bca();
             }
-            si.check_watches();
+            //si.check_watches();
         }
 
         void block_clauses() {
@@ -1829,7 +1829,6 @@ namespace sat {
                     return true;
             }
         }
-
         return true;
     }
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -54,7 +54,6 @@ class inc_sat_solver : public solver {
     unsigned            m_fmls_head;
     expr_ref_vector     m_core;
     atom2bool_var       m_map;
-    model_ref           m_model;
     scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
     tactic_ref          m_preprocess;
     unsigned            m_num_scopes;
@@ -183,7 +182,6 @@ public:
 
         TRACE("sat", tout << _assumptions << "\n";);
         dep2asm_t dep2asm;
-        m_model = 0;
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
@@ -289,12 +287,6 @@ public:
         r.reset();
         r.append(m_core.size(), m_core.c_ptr());
     }
-    virtual void get_model_core(model_ref & mdl) {
-        if (!m_model.get()) {
-            extract_model();
-        }
-        mdl = m_model;
-    }
     virtual proof * get_proof() {
         UNREACHABLE();
         return 0;
@@ -302,7 +294,6 @@ public:
 
     virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
         if (!is_internalized()) {
-            m_model = 0;
             lbool r = internalize_formulas();
             if (r != l_true) return expr_ref_vector(m);
         }
@@ -789,14 +780,14 @@ private:
         }
     }
 
-    void extract_model() {
+    virtual void get_model_core(model_ref & mdl) {
         TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
         if (!m_solver.model_is_current()) {
-            m_model = 0;
+            mdl = nullptr;
             return;
         }
         sat::model const & ll_m = m_solver.get_model();
-        model_ref md = alloc(model, m);
+        mdl = alloc(model, m);
         for (auto const& kv : m_map) {
             expr * n   = kv.m_key;
             if (is_app(n) && to_app(n)->get_num_args() > 0) {
@@ -805,40 +796,39 @@ private:
             sat::bool_var v = kv.m_value;
             switch (sat::value_at(v, ll_m)) {
             case l_true:
-                md->register_decl(to_app(n)->get_decl(), m.mk_true());
+                mdl->register_decl(to_app(n)->get_decl(), m.mk_true());
                 break;
             case l_false:
-                md->register_decl(to_app(n)->get_decl(), m.mk_false());
+                mdl->register_decl(to_app(n)->get_decl(), m.mk_false());
                 break;
             default:
                 break;
             }
         }
-        m_model = md;
+        //IF_VERBOSE(0, model_v2_pp(verbose_stream(), *mdl, true););
-        //IF_VERBOSE(0, model_v2_pp(verbose_stream(), *m_model, true););
 
         if (m_sat_mc) {
-          //  IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
+            //IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
-            (*m_sat_mc)(m_model);
+            (*m_sat_mc)(mdl);
         }
         insert_const2bits();
         if (m_mc0) {            
-          //  IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
+            //IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
-            (*m_mc0)(m_model);
+            (*m_mc0)(mdl);
         }
-        TRACE("sat", model_smt2_pp(tout, m, *m_model, 0););
+        TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
+        
+        // IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
 
-        // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "after\n"););
+#if 0
-
-#if 1
         IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
-        model_evaluator eval(*m_model);
+        model_evaluator eval(*mdl);
         for (expr * f : m_fmls) {
             expr_ref tmp(m);
             eval(f, tmp);
             CTRACE("sat", !m.is_true(tmp),
                    tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n";
-                   model_smt2_pp(tout, m, *(m_model.get()), 0););
+                   model_smt2_pp(tout, m, *(mdl.get()), 0););
             if (!m.is_true(tmp)) {
                 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
                 IF_VERBOSE(0, verbose_stream() << m_params << "\n";);

src/tactic/generic_model_converter.cpp

@@ -38,6 +38,7 @@ void generic_model_converter::add(func_decl * d, expr* e) {
 
 void generic_model_converter::operator()(model_ref & md) {
     TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
+    // IF_VERBOSE(0, verbose_stream() << "Apply converter " << m_orig << "\n";);
     model_evaluator ev(*(md.get()));
     ev.set_model_completion(true);
     ev.set_expand_array_equalities(false);    

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -152,14 +152,14 @@ public:
     virtual void get_model_core(model_ref & mdl) {
         m_solver->get_model(mdl);
         if (mdl) {
-            model_converter_ref mc = bounded_model_converter();
+            model_converter_ref mc = local_model_converter();
             if (mc) (*mc)(mdl);
         }
     }
     model_converter* external_model_converter() const {
-        return concat(mc0(), bounded_model_converter());
+        return concat(mc0(), local_model_converter());
     }
-    model_converter* bounded_model_converter() const {
+    model_converter* local_model_converter() const {
         if (m_int2bv.empty() && m_bv_fns.empty()) return nullptr;
         generic_model_converter* mc = alloc(generic_model_converter, m, "bounded_int2bv");
         for (func_decl* f : m_bv_fns) 
@@ -178,7 +178,7 @@ public:
     }
 
     virtual model_converter_ref get_model_converter() const { 
-        model_converter_ref mc = concat(mc0(), bounded_model_converter());
+        model_converter_ref mc = external_model_converter();
         mc = concat(mc.get(), m_solver->get_model_converter().get());
         return mc;
     }

src/tactic/portfolio/enum2bv_solver.cpp

@@ -92,11 +92,11 @@ public:
     virtual void get_model_core(model_ref & mdl) { 
         m_solver->get_model(mdl);
         if (mdl) {
-            model_converter_ref mc = enum_model_converter();
+            model_converter_ref mc = local_model_converter();
             if (mc) (*mc)(mdl);
         }
     } 
-    model_converter* enum_model_converter() const {
+    model_converter* local_model_converter() const {
         if (m_rewriter.enum2def().empty() && 
             m_rewriter.enum2bv().empty()) {
             return nullptr;
@@ -110,7 +110,7 @@ public:
     }
 
     model_converter* external_model_converter() const {
-        return concat(mc0(), enum_model_converter());
+        return concat(mc0(), local_model_converter());
     }
 
     virtual model_converter_ref get_model_converter() const { 

src/tactic/portfolio/pb2bv_solver.cpp

@@ -91,14 +91,15 @@ public:
     virtual void get_model_core(model_ref & mdl) { 
         m_solver->get_model(mdl);
         if (mdl) {
-            filter_model(mdl);            
+            model_converter_ref mc = local_model_converter();
+            if (mc) (*mc)(mdl);
         }
     } 
     model_converter* external_model_converter() const {
-        return concat(mc0(), filter_model_converter());
+        return concat(mc0(), local_model_converter());
     }
     virtual model_converter_ref get_model_converter() const { 
-        model_converter_ref mc = concat(mc0(), filter_model_converter());
+        model_converter_ref mc = external_model_converter();
         mc = concat(mc.get(), m_solver->get_model_converter().get());
         return mc;
     }
@@ -113,7 +114,7 @@ public:
         flush_assertions(); 
         return m_solver->get_consequences(asms, vars, consequences); }
 
-    model_converter* filter_model_converter() const {
+    model_converter* local_model_converter() const {
         if (m_rewriter.fresh_constants().empty()) {
             return nullptr;
         }
@@ -125,13 +126,6 @@ public:
         return filter;
     }
 
-    void filter_model(model_ref& mdl) {
-        model_converter_ref mc = filter_model_converter();
-        if (mc.get()) {
-            (*mc)(mdl);
-        }
-    }
-
     virtual unsigned get_num_assertions() const {
         flush_assertions();
         return m_solver->get_num_assertions();