mb-skolem for arithmetic with model repair

The contract is that users of mb-skolem ensure that
interface equalities are preserved (by adding a
sufficient set of disequalities, such as a chain
x1 < x2 < x3 .., to force that solutions for
x_i does not clash).

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

src/math/simplex/model_based_opt.cpp

@@ -51,7 +51,8 @@ namespace opt {
                 m_div = -v.m_coeff;
             }
         }        
-        m_coeff = r.m_coeff - r.m_value;
+        m_coeff = r.m_coeff;
+        if (r.m_type == opt::t_lt) m_coeff += m_div;
         normalize();
         SASSERT(m_div.is_pos());
     }
@@ -983,7 +984,7 @@ namespace opt {
                 }
                 else {
                     result = def();
-                    result.m_coeff = eval(x);
+                    m_var2value[x] = rational::zero();
                 }
                 SASSERT(eval(result) == eval(x));
             }
@@ -1008,8 +1009,8 @@ namespace opt {
             else {
                 result = def(m_rows[glb_index], x);
             }
+            m_var2value[x] = eval(result);
 #endif
-            SASSERT(eval(result) == eval(x));
         }
 
         // The number of matching lower and upper bounds is small.
@@ -1106,7 +1107,8 @@ namespace opt {
         }
         def result = project(y, compute_def);
         if (compute_def) {
-            result = (result * D) + u;            
+            result = (result * D) + u;      
+            m_var2value[x] = eval(result);
         }
         SASSERT(!compute_def || eval(result) == eval(x));
         return result;
@@ -1204,7 +1206,7 @@ namespace opt {
         def result;
         if (compute_def) {
             result = def(m_rows[row_id1], x);
-            SASSERT(eval(result) == eval(x));
+            m_var2value[x] = eval(result);
         }
         retire_row(row_id1);
         return result;

src/model/model_core.cpp

@@ -47,8 +47,8 @@ bool model_core::eval(func_decl* f, expr_ref & r) const {
 
 void model_core::register_decl(func_decl * d, expr * v) {
     SASSERT(d->get_arity() == 0);
-    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0);
-    if (entry->get_data().m_value == 0) {
+    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, nullptr);
+    if (entry->get_data().m_value == nullptr) {
         // new entry
         m_decls.push_back(d);
         m_const_decls.push_back(d);
@@ -67,8 +67,8 @@ void model_core::register_decl(func_decl * d, expr * v) {
 void model_core::register_decl(func_decl * d, func_interp * fi) {
     SASSERT(d->get_arity() > 0);
     SASSERT(&fi->m() == &m_manager);
-    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
-    if (entry->get_data().m_value == 0) {
+    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr);
+    if (entry->get_data().m_value == nullptr) {
         // new entry
         m_decls.push_back(d);
         m_func_decls.push_back(d);

src/qe/qe_arith.cpp

@@ -360,7 +360,7 @@ namespace qe {
 
             ptr_vector<expr> index2expr;
             for (auto& kv : tids) {
-                index2expr.setx(kv.m_value, kv.m_key, 0);
+                index2expr.setx(kv.m_value, kv.m_key, nullptr);
             }
 
             j = 0;
@@ -454,6 +454,8 @@ namespace qe {
                     else if (!d.m_div.is_one() && !is_int) {
                         t = a.mk_div(t, a.mk_numeral(d.m_div, is_int));
                     }
+                    update_model(model, to_app(x), eval(t));
+                    
                     SASSERT(eval(t) == eval(x));
                     result.push_back(def(expr_ref(x, m), t));
                 }
@@ -461,6 +463,22 @@ namespace qe {
             return result;
         }        
 
+        void update_model(model& mdl, app* x, expr_ref const& val) {
+            if (is_uninterp_const(x)) {
+                mdl.register_decl(x->get_decl(), val);
+            }
+            else {
+                func_interp* fi = mdl.get_func_interp(x->get_decl());
+                if (!fi) return;
+                model_evaluator eval(mdl);
+                expr_ref_vector args(m);
+                for (expr* arg : *x) {
+                    args.push_back(eval(arg));
+                }
+                fi->insert_entry(args.c_ptr(), val);
+            }
+        }
+
         expr_ref mk_add(expr_ref_vector const& ts) {
             switch (ts.size()) {
             case 0:

src/qe/qe_mbi.cpp

@@ -259,7 +259,7 @@ namespace qe {
         app_ref_vector& m_vars;
         arith_util      arith;
         obj_hashtable<func_decl> m_exclude;
-        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): 
+        is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared):
             m(vars.m()), m_vars(vars), arith(m) {
             for (func_decl* f : shared) m_exclude.insert(f);
         }
@@ -484,7 +484,7 @@ namespace qe {
                         return l_true, mbp of local, mdl of local & blocked
                   else if !is_sat(local & lits) then
                       return l_false, mbp of local, nullptr
-                  else // is_sat(local & lits) && !is_sat(local & lits & blocked)
+                  else if is_sat(local & lits) && !is_sat(local & lits & blocked)
                       MISSING CASE
                       MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
                       in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked)

src/qe/qe_term_graph.cpp

@@ -35,6 +35,7 @@ namespace qe {
             }
         };
     }
+
     namespace is_pure_ns {
         struct found{};
         struct proc {
@@ -776,7 +777,7 @@ namespace qe {
             for (auto &kv : val2rep) {
                 expr *rep = kv.m_value;
                 if (!m.is_unique_value(rep))
-                    reps.push_back(kv.m_value);
+                reps.push_back(kv.m_value);
             }
 
             if (reps.size() <= 1) return;