tweaking nlqsat

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 6, 2019 · 29f0897 · 29f0897
1 parent 5fbfc0f
commit 29f0897
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 12 deletions.
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
@@ -507,6 +507,7 @@ namespace nlsat {
             m_num_bool_vars--;
             m_dead[b]  = true;
             m_atoms[b] = nullptr;
+            m_bvalues[b] = l_undef;
             m_bid_gen.recycle(b);
         }
 
@@ -3109,7 +3110,8 @@ namespace nlsat {
 
         std::ostream& display(std::ostream & out) const {
             display(out, m_display_var);
-            return display_assignment(out);
+            display_assignment(out << "assignment:\n");
+            return out << "---\n";
         }
 
         std::ostream& display_vars(std::ostream & out) const {
@@ -3263,31 +3265,37 @@ namespace nlsat {
         as.copy(m_imp->m_assignment);
     }
 
-    void solver::get_bvalues(svector<lbool>& vs) {
+    void solver::get_bvalues(svector<bool_var> const& bvars, svector<lbool>& vs) {
         vs.reset();
-        unsigned sz = m_imp->m_bvalues.size();
-        for (bool_var b = 0; b < sz; ++b) {
-            if (m_imp->m_atoms[b] == nullptr) {
-                vs.push_back(m_imp->m_bvalues[b]);
-            }
-            else {
-                vs.push_back(l_undef); // don't save values from atoms.
+        for (bool_var b : bvars) {
+            vs.reserve(b + 1, l_undef);
+            if (!m_imp->m_atoms[b]) {
+                vs[b] = m_imp->m_bvalues[b];
             }
         }
         TRACE("nlsat", display(tout););
     }
 
     void solver::set_bvalues(svector<lbool> const& vs) {
         TRACE("nlsat", display(tout););
+        for (bool_var b = 0; b < vs.size(); ++b) {
+            if (vs[b] != l_undef) {
+                m_imp->m_bvalues[b] = vs[b];
+                SASSERT(!m_imp->m_atoms[b]);
+            }
+        }
+#if 0        
         m_imp->m_bvalues.reset();
         m_imp->m_bvalues.append(vs);
         m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);        
         for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) {
             atom* a = m_imp->m_atoms[i];
+            SASSERT(!a);
             if (a) {
                 m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false));
             }
         }
+#endif
         TRACE("nlsat", display(tout););
     }
 

diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
@@ -166,7 +166,7 @@ namespace nlsat {
         void get_rvalues(assignment& as);
         void set_rvalues(assignment const& as);
 
-        void get_bvalues(svector<lbool>& vs);
+        void get_bvalues(svector<bool_var> const& bvars, svector<lbool>& vs);
         void set_bvalues(svector<lbool> const& vs);
 
         /**

diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
@@ -102,7 +102,9 @@ namespace qe {
             void init_expr2var(app_ref_vector const& qvars) {
                 for (app* v : qvars) {
                     if (m.is_bool(v)) {
-                        m_a2b.insert(v, m_solver.mk_bool_var());
+                        nlsat::bool_var b = m_solver.mk_bool_var();
+                        m_solver.inc_ref(b);
+                        m_a2b.insert(v, b);
                     }
                     else {
                         // TODO: assert it is of type Real.
@@ -121,8 +123,12 @@ namespace qe {
             }
 
             void save_model(bool is_exists) {
+                svector<nlsat::bool_var> bvars;
+                for (auto const& kv : m_bvar2level) {
+                    bvars.push_back(kv.m_key);
+                }
                 m_solver.get_rvalues(m_rmodel);
-                m_solver.get_bvalues(m_bmodel);
+                m_solver.get_bvalues(bvars, m_bmodel);
                 m_valid_model = true;
                 if (is_exists) {
                     m_rmodel0.copy(m_rmodel);
@@ -311,6 +317,7 @@ namespace qe {
                 }
             }
             TRACE("qe", s.display(tout);
+                  tout << "assumptions\n";
                   for (nlsat::literal a : s.m_asms) {
                       s.m_solver.display(tout, a) << "\n";
                   });