fixes in new solver

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

src/ast/euf/euf_egraph.cpp

@@ -672,6 +672,9 @@ namespace euf {
                 out << " " << p->get_expr_id();
             out << "] ";
         }
+        if (n->value() != l_undef) {
+            out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
+        }
         if (n->has_th_vars()) {
             out << "[t";
             for (auto v : enode_th_vars(n))

src/math/lp/nla_core.cpp

@@ -1462,7 +1462,6 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
         bound += checks[i].first;
     uint_set seen;
     while (bound > 0 && !done() && m_lemma_vec->empty()) {
-        SASSERT(bound > 0);
         unsigned n = random() % bound;
         for (unsigned i = 0; i < sz; ++i) {
             if (seen.contains(i))

src/sat/smt/arith_diagnostics.cpp

@@ -56,7 +56,7 @@ namespace arith {
                     scoped_anum an(m_nla->am());
                     m_nla->am().display(out << " = ", nl_value(v, an));
                 }
-                else if (m_model_is_initialized && is_registered_var(v)) 
+                else if (can_get_value(v))  
                     out << " = " << get_value(v);
                 if (is_int(v)) 
                     out << ", int";

src/sat/smt/arith_solver.cpp

@@ -84,6 +84,7 @@ namespace arith {
     }
 
     bool solver::unit_propagate() {
+        m_model_is_initialized = false;
         if (!m_new_eq && m_new_bounds.empty() && m_asserted_qhead == m_asserted.size())
             return false;
 
@@ -572,6 +573,10 @@ namespace arith {
                 value = ~value;
             if (!found_bad && value == get_phase(n->bool_var()))
                 continue;
+            TRACE("arith",
+                tout << eval << " " << value << " " << ctx.bpp(n) << "\n";
+                tout << mdl << "\n";
+                s().display(tout););
             IF_VERBOSE(0, 
                        verbose_stream() << eval << " " << value << " " << ctx.bpp(n) << "\n";
                        verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
@@ -642,6 +647,7 @@ namespace arith {
         for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) {
             unsigned v = m_bounds_trail[i];
             api_bound* b = m_bounds[v].back();
+            m_bool_var2bound.erase(b->get_lit().var());
             // del_use_lists(b);
             dealloc(b);
             m_bounds[v].pop_back();

src/sat/smt/arith_solver.h

@@ -318,6 +318,9 @@ namespace arith {
         vector<constraint_bound>        m_upper_terms;
         vector<constraint_bound>        m_history;
 
+        bool can_get_value(theory_var v) const {
+            return is_registered_var(v) && m_model_is_initialized;
+        }
 
         // solving
         void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2);

src/sat/smt/euf_model.cpp

@@ -22,51 +22,6 @@ Author:
 
 namespace euf {
 
-    void solver::update_model(model_ref& mdl) {
-        for (auto* mb : m_solvers)
-            mb->init_model();
-        deps_t deps;
-        m_values.reset();
-        m_values2root.reset();
-        collect_dependencies(deps);
-        deps.topological_sort();
-        dependencies2values(deps, mdl);
-        values2model(deps, mdl);
-        for (auto* mb : m_solvers)
-            mb->finalize_model(*mdl);
-        // validate_model(*mdl);
-    }
-
-    bool solver::include_func_interp(func_decl* f) {
-        if (f->is_skolem())
-            return false;
-        if (f->get_family_id() == null_family_id)
-            return true;
-        if (f->get_family_id() == m.get_basic_family_id())
-            return false;
-        euf::th_model_builder* mb = func_decl2solver(f);
-        return mb && mb->include_func_interp(f);
-    }
-
-    void solver::collect_dependencies(deps_t& deps) {
-        for (enode* n : m_egraph.nodes()) {
-            auto* mb = sort2solver(m.get_sort(n->get_expr()));
-            if (mb)
-                mb->add_dep(n, deps);
-            else
-                deps.insert(n, nullptr);
-        }
-
-        TRACE("euf",
-              for (auto const& d : deps.deps()) 
-                  if (d.m_value) {
-                      tout << mk_bounded_pp(d.m_key->get_expr(), m) << ":\n";
-                      for (auto* n : *d.m_value)
-                          tout << "   " << mk_bounded_pp(n->get_expr(), m) << "\n";
-                  }
-              );
-    }
-
     class solver::user_sort {
         ast_manager& m;
         model_ref& mdl;
@@ -94,10 +49,63 @@ namespace euf {
             }
             vals->push_back(value);
         }
+
+        void register_value(expr* val) {
+            factory.register_value(val);
+        }
     };
 
-    void solver::dependencies2values(deps_t& deps, model_ref& mdl) {
+    void solver::update_model(model_ref& mdl) {
-        user_sort user_sort(*this, m_values, mdl);
+        for (auto* mb : m_solvers)
+            mb->init_model();
+        deps_t deps;
+        m_values.reset();
+        m_values2root.reset();
+        user_sort us(*this, m_values, mdl);
+        collect_dependencies(us, deps);
+        deps.topological_sort();
+        dependencies2values(us, deps, mdl);
+        values2model(deps, mdl);
+        for (auto* mb : m_solvers)
+            mb->finalize_model(*mdl);
+        // validate_model(*mdl);
+    }
+
+    bool solver::include_func_interp(func_decl* f) {
+        if (f->is_skolem())
+            return false;
+        if (f->get_family_id() == null_family_id)
+            return true;
+        if (f->get_family_id() == m.get_basic_family_id())
+            return false;
+        euf::th_model_builder* mb = func_decl2solver(f);
+        return mb && mb->include_func_interp(f);
+    }
+
+    void solver::collect_dependencies(user_sort& us, deps_t& deps) {
+        for (enode* n : m_egraph.nodes()) {
+            expr* e = n->get_expr();
+            sort* srt = m.get_sort(e);
+            auto* mb = sort2solver(srt);
+            if (mb)
+                mb->add_dep(n, deps);
+            else
+                deps.insert(n, nullptr);
+            if (n->is_root() && m.is_uninterp(srt) && m.is_value(e))
+                us.register_value(e);
+        }
+
+        TRACE("euf",
+              for (auto const& d : deps.deps()) 
+                  if (d.m_value) {
+                      tout << mk_bounded_pp(d.m_key->get_expr(), m) << ":\n";
+                      for (auto* n : *d.m_value)
+                          tout << "   " << mk_bounded_pp(n->get_expr(), m) << "\n";
+                  }
+              );
+    }
+
+    void solver::dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl) {
         for (enode* n : deps.top_sorted()) {
             unsigned id = n->get_root_id();
             if (m_values.get(id, nullptr))
@@ -134,9 +142,13 @@ namespace euf {
                 }
                 continue;
             }
+            if (m.is_value(n->get_root()->get_expr())) {
+                m_values.set(id, n->get_root()->get_expr());
+                continue;
+            }
             sort* srt = m.get_sort(e);
             if (m.is_uninterp(srt)) 
-                user_sort.add(id, srt);            
+                us.add(id, srt);            
             else if (auto* mbS = sort2solver(srt))
                 mbS->add_value(n, *mdl, m_values);
             else if (auto* mbE = expr2solver(e))

src/sat/smt/euf_solver.cpp

@@ -137,6 +137,8 @@ namespace euf {
     void solver::unhandled_function(func_decl* f) {
         if (m_unhandled_functions.contains(f))
             return;
+        if (m.is_model_value(f))
+            return;
         m_unhandled_functions.push_back(f);
         m_trail.push(push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");

src/sat/smt/euf_solver.h

@@ -141,8 +141,8 @@ namespace euf {
         obj_map<expr, enode*> m_values2root;
         bool include_func_interp(func_decl* f);
         void register_macros(model& mdl);
-        void dependencies2values(deps_t& deps, model_ref& mdl);
+        void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl);
-        void collect_dependencies(deps_t& deps);
+        void collect_dependencies(user_sort& us, deps_t& deps);
         void values2model(deps_t const& deps, model_ref& mdl);
         void validate_model(model& mdl);
 

src/sat/smt/q_mbi.cpp

@@ -99,13 +99,13 @@ namespace q {
 
     lbool mbqi::check_forall(quantifier* q) {
         quantifier* q_flat = m_qs.flatten(q);
+        init_solver();
+        ::solver::scoped_push _sp(*m_solver);
         auto* qb = specialize(q_flat);
         if (!qb)
             return l_undef;
         if (m.is_false(qb->mbody))
             return l_true;
-        init_solver();
-        ::solver::scoped_push _sp(*m_solver);
         m_solver->assert_expr(qb->mbody);
         lbool r = m_solver->check_sat(0, nullptr);
         if (r == l_undef)

src/sat/smt/sat_dual_solver.cpp

@@ -33,6 +33,7 @@ namespace sat {
         m_roots.push_scope();
         m_tracked_vars.push_scope();
         m_units.push_scope();
+        m_vars.push_scope();
     }
 
     void dual_solver::pop(unsigned num_scopes) {
@@ -40,6 +41,14 @@ namespace sat {
         unsigned old_sz = m_tracked_vars.old_size(num_scopes);
         for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
             m_is_tracked[m_tracked_vars[i]] = false; 
+        old_sz = m_vars.old_size(num_scopes);
+        for (unsigned i = m_vars.size(); i-- > old_sz; ) {
+            unsigned v = m_vars[i];
+            unsigned w = m_ext2var[v];
+            m_ext2var[v] = null_bool_var;
+            m_var2ext[w] = null_bool_var;
+        }
+        m_vars.pop_scope(num_scopes);
         m_units.pop_scope(num_scopes);
         m_roots.pop_scope(num_scopes);
         m_tracked_vars.pop_scope(num_scopes);
@@ -51,6 +60,7 @@ namespace sat {
             w = m_solver.mk_var();
             m_ext2var.setx(v, w, null_bool_var);
             m_var2ext.setx(w, v, null_bool_var);
+            m_vars.push_back(v);
         }
         return w;
     }

src/sat/smt/sat_dual_solver.h

@@ -34,6 +34,7 @@ namespace sat {
         bool_var_vector m_is_tracked;
         unsigned_vector m_ext2var;
         unsigned_vector m_var2ext;
+        lim_svector<unsigned> m_vars;
         void add_literal(literal lit);
 
         bool_var ext2var(bool_var v);