#5324

src/qe/mbp/mbp_arith.cpp

@@ -281,9 +281,9 @@ namespace mbp {
             obj_map<expr, unsigned> tids;
             expr_ref_vector pinned(m);
             unsigned j = 0;
-            TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
-            for (unsigned i = 0; i < fmls.size(); ++i) {
-                expr * fml = fmls.get(i);
+            TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";
+                  for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";);
+            for (expr* fml : fmls) {
                 if (!linearize(mbo, eval, fml, fmls, tids)) {
                     TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";);
                     fmls[j++] = fml;

src/qe/mbp/mbp_plugin.cpp

@@ -102,6 +102,8 @@ namespace mbp {
         model_evaluator eval(model);
         eval.set_expand_array_equalities(true);
         TRACE("qe", tout << fmls << "\n";);
+        DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); });
+
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;
             SASSERT(m.is_bool(fml));

src/sat/smt/euf_model.cpp

@@ -229,17 +229,23 @@ namespace euf {
         // TODO
     }
 
+    void solver::model_updated(model_ref& mdl) {
+        m_values2root.reset();
+        for (enode* n : m_egraph.nodes())
+            if (n->is_root() && m_values.get(n->get_expr_id())) 
+                m_values[n->get_expr_id()] = (*mdl)(n->get_expr());            
+    }
+
     obj_map<expr,enode*> const& solver::values2root() {    
         if (!m_values2root.empty())
             return m_values2root;
         for (enode* n : m_egraph.nodes())
             if (n->is_root() && m_values.get(n->get_expr_id()))
                 m_values2root.insert(m_values.get(n->get_expr_id()), n);
-#if 0
-        for (auto kv : m_values2root) {
-            std::cout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";
-        }
-#endif
+        TRACE("model", 
+              for (auto kv : m_values2root) 
+                  tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";);
+
         return m_values2root;
     }
 

src/sat/smt/euf_solver.h

@@ -149,7 +149,7 @@ namespace euf {
 
         // model building
         expr_ref_vector m_values;
-        obj_map<expr, enode*> m_values2root;
+        obj_map<expr, enode*> m_values2root;        
         bool include_func_interp(func_decl* f);
         void register_macros(model& mdl);
         void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl);
@@ -370,6 +370,7 @@ namespace euf {
         // model construction
         void update_model(model_ref& mdl);
         obj_map<expr, enode*> const& values2root();
+        void model_updated(model_ref& mdl);
         expr* node2value(enode* n) const;
 
         // diagnostics

src/sat/smt/q_mbi.cpp

@@ -377,6 +377,7 @@ namespace q {
         m_model->reset_eval_cache();
         for (app* v : qb.vars)
             m_model->register_decl(v->get_decl(), mdl(v));
+        ctx.model_updated(m_model);
         if (qb.var_args.empty())
             return;
         var_subst subst(m);
@@ -416,7 +417,16 @@ namespace q {
             expr_ref value = (*m_model)(term);
             expr* s = m_model_fixer.invert_app(term, value);
             rep.insert(term, s);
-            eqs.push_back(m.mk_eq(term, s));
+            expr_ref eq(m.mk_eq(term, s), m);
+            if (m_model->is_false(eq)) {
+                IF_VERBOSE(0,
+                    verbose_stream() << mk_pp(s, m) << " := " << (*m_model)(s) << "\n";
+                verbose_stream() << mk_pp(term, m) << " := " << (*m_model)(term) << "\n";
+                verbose_stream() << value << " -> " << (*m_model)(ctx.values2root()[value]->get_expr()) << "\n";
+                verbose_stream() << (*m_model)(s) << " -> " << (*m_model)(ctx.values2root()[(*m_model)(s)]->get_expr()) << "\n";
+                verbose_stream() << *m_model << "\n";);
+            }
+            eqs.push_back(eq);
         }
         rep(fmls);
         fmls.append(eqs);

src/sat/smt/q_model_fixer.cpp

@@ -218,13 +218,14 @@ namespace q {
 
     expr* model_fixer::invert_app(app* t, expr* value) {
         euf::enode* r = nullptr;
+        auto& v2r = ctx.values2root();
         TRACE("q",
-            tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
-              if (ctx.values2root().find(value, r)) 
+              tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
+              if (v2r.find(value, r)) 
                   tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
-              ctx.display(tout);
+              ctx.display(tout);              
               );
-        if (ctx.values2root().find(value, r))
+        if (v2r.find(value, r)) 
             return r->get_expr();
         return value;
     }