na

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

src/cmd_context/cmd_context.cpp

@@ -1674,7 +1674,7 @@ void cmd_context::add_declared_functions(model& mdl) {
             expr* val = mdl.get_some_value(f->get_range());
             if (f->get_arity() == 0) {
                 mdl.register_decl(f, val);
-                }
+            }
             else {
                 func_interp* fi = alloc(func_interp, m(), f->get_arity());
                 fi->set_else(val);

src/qe/mbp/mbp_plugin.cpp

@@ -341,6 +341,7 @@ namespace mbp {
             m_non_ground.mark(v);
         for (unsigned i = 0; m.inc() && i < lits.size(); ++i) 
             lits[i] = purify(inv, eval, lits.get(i), lits); 
+        std::cout << m_pure_eqs << "\n";
         lits.append(m_pure_eqs);
         TRACE("mbp", tout << lits << "\n";);
     }
@@ -371,7 +372,7 @@ namespace mbp {
                 m_pure_eqs.push_back(m.mk_eq(t, s));
             unsigned i = 0;
             for (expr* arg : *t) 
-                push_back(lits, inv.invert_arg(t, i++, eval(arg)));            
+                inv.invert_arg(t, i++, eval(arg), lits);    
             m_to_visit.pop_back();
         }
         else 

src/qe/mbp/mbp_plugin.h

@@ -43,7 +43,7 @@ namespace mbp {
     class euf_inverter {
     public:
         virtual expr* invert_app(app* t, expr* value) = 0;
-        virtual expr* invert_arg(app* t, unsigned i, expr* value) = 0;
+        virtual void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) = 0;
     };
 
     class project_plugin {

src/sat/smt/arith_axioms.cpp

@@ -301,10 +301,17 @@ namespace arith {
             return;
         expr* e1 = var2expr(v1);
         expr* e2 = var2expr(v2);
+        if (e1 == e2)
+            return;
         literal le, ge;
-        literal eq = eq_internalize(e1, e2);
         if (a.is_numeral(e1))
             std::swap(e1, e2);
+        if (a.is_numeral(e1)) {
+            add_unit(~mk_literal(m.mk_eq(e1, e2)));
+            std::cout << "two numerals\n";
+            return;
+        }
+        literal eq = eq_internalize(e1, e2);
         if (a.is_numeral(e2)) {
             le = mk_literal(a.mk_le(e1, e2));
             ge = mk_literal(a.mk_ge(e1, e2));
@@ -313,9 +320,19 @@ namespace arith {
             expr_ref diff(a.mk_sub(e1, e2), m);
             expr_ref zero(a.mk_numeral(rational(0), a.is_int(e1)), m);
             rewrite(diff);
+            if (a.is_numeral(diff)) {
+                std::cout << "diff " << diff << " " << mk_pp(e1, m) << " " << mk_pp(e2, m) << "\n";
+                if (zero == diff)
+                    add_unit(eq);
+                else 
+                    add_unit(~eq);
+                return;
+            }
             le = mk_literal(a.mk_le(diff, zero));
             ge = mk_literal(a.mk_ge(diff, zero));
         }
+        std::cout << mk_pp(e1, m) << " " << mk_pp(e2, m) << " ";
+        std::cout << le << " " << ge << "\n";
         add_clause(~eq, le);
         add_clause(~eq, ge);
         add_clause(~le, ~ge, eq);

src/sat/smt/q_mbi.cpp

@@ -190,6 +190,7 @@ namespace q {
         app_ref_vector vars(qb.vars);
         mbp::project_plugin proj(m);
         proj.purify(m_model_fixer, *m_model, vars, fmls);
+        std::cout << "fmls\n" << fmls << "\n";
         for (unsigned i = 0; i < vars.size(); ++i) {
             app* v = vars.get(i);
             auto* p = get_plugin(v);

src/sat/smt/q_model_fixer.cpp

@@ -221,18 +221,18 @@ namespace q {
         return value; 
     }
 
-    expr* model_fixer::invert_arg(app* t, unsigned i, expr* value)  { 
+    void model_fixer::invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits)  { 
         TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";);
         auto const* md = get_projection_data(t->get_decl(), i);
         if (!md)
-            return m.mk_true();
+            return;
         auto* proj = get_projection(t->get_decl()->get_domain(i));
         if (!proj)
-            return m.mk_true();
+            return;
 
         unsigned sz = md->values.size();
         if (sz <= 1) 
-            return m.mk_true();
+            return;
         
         //
         // md->values are sorted
@@ -251,13 +251,18 @@ namespace q {
 
         expr* arg = t->get_arg(i);
 
-        if (is_lt(md->values[1]))
-            return proj->mk_lt(arg, term(1));
+        if (is_lt(md->values[1])) {
+            lits.push_back(proj->mk_lt(arg, term(1)));
+            return;
+        }
 
         for (unsigned j = 2; j < sz; ++j) 
-            if (is_lt(md->values[j]))
-                return m.mk_and(proj->mk_le(term(j-1), arg), proj->mk_lt(arg, term(j)));
-        
-        return proj->mk_le(term(sz-1), arg);
+            if (is_lt(md->values[j])) {
+                lits.push_back(proj->mk_le(term(j - 1), arg));
+                lits.push_back(proj->mk_lt(arg, term(j)));
+                return;
+            }
+
+        lits.push_back(proj->mk_le(term(sz-1), arg));
     }
 }

src/sat/smt/q_model_fixer.h

@@ -108,7 +108,7 @@ namespace q {
         quantifier_macro_info* operator()(quantifier* q) override;
 
         expr* invert_app(app* t, expr* value) override;
-        expr* invert_arg(app* t, unsigned i, expr* value) override;
+        void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) override;
     };
 
 }