updates to mbqi

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

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

src/muz/spacer/spacer_util.cpp

@@ -90,33 +90,33 @@ namespace spacer {
         if (!m_model) { return; }
         m_mev = alloc(model_evaluator, *m_model);
     }
-
+    
     bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) {
         m_mev->set_model_completion (model_completion);
         try {
             m_mev->operator() (e, result);
             return true;
-        }
+        } 
         catch (model_evaluator_exception &ex) {
             (void)ex;
             TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";);
             return false;
         }
     }
-
+    
     bool model_evaluator_util::eval(const expr_ref_vector &v,
                                     expr_ref& res, bool model_completion) {
         expr_ref e(m);
         e = mk_and (v);
         return eval(e, res, model_completion);
     }
-
+    
-
+    
     bool model_evaluator_util::is_true(const expr_ref_vector &v) {
         expr_ref res(m);
         return eval (v, res, false) && m.is_true (res);
     }
-
+    
     bool model_evaluator_util::is_false(expr *x) {
         expr_ref res(m);
         return eval(x, res, false) && m.is_false (res);
@@ -126,7 +126,7 @@ namespace spacer {
         expr_ref res(m);
         return eval(x, res, false) && m.is_true (res);
     }
-
+    
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
         ast_manager& m = fml.get_manager();
         expr_ref_vector conjs(m);
@@ -172,16 +172,16 @@ namespace spacer {
                     SASSERT(orig_size <= 1 + conjs.size());
                     if (i + 1 == orig_size) {
                         // no-op.
-                    }
+                    } 
                     else if (orig_size <= conjs.size()) {
                         // no-op
-                    }
+                    } 
                     else {
                         SASSERT(orig_size == 1 + conjs.size());
                         --orig_size;
                         --i;
                     }
-                }
+                } 
                 else {
                     conjs[i] = tmp;
                 }
@@ -199,7 +199,7 @@ namespace spacer {
         ast_manager& m;
     public:
         ite_hoister(ast_manager& m): m(m) {}
-
+        
         br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
             if (m.is_ite(f)) {
                 return BR_FAILED;
@@ -234,7 +234,7 @@ namespace spacer {
         }
         ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}
     };
-
+    
     class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
         ite_hoister_cfg m_cfg;
     public:
@@ -242,7 +242,7 @@ namespace spacer {
             rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
             m_cfg(m, p) {}
     };
-
+    
     void hoist_non_bool_if(expr_ref& fml) {
         ast_manager& m = fml.get_manager();
         scoped_no_proof _sp(m);
@@ -274,7 +274,7 @@ namespace spacer {
         bool is_arith_expr(expr *e) const {
             return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
         }
-
+        
         bool is_offset(expr* e) const {
             if (a.is_numeral(e)) {
                 return true;
@@ -358,7 +358,7 @@ namespace spacer {
                 !a.is_mul(lhs) &&
                 !a.is_mul(rhs);
         }
-
+        
         bool test_term(expr* e) const {
             if (m.is_bool(e)) {
                 return true;
@@ -403,9 +403,9 @@ namespace spacer {
 
     public:
         test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
-
+        
         void test_for_utvpi() { m_test_for_utvpi = true; }
-
+        
         void operator()(expr* e)  {
             if (!m_is_dl) {
                 return;
@@ -422,7 +422,7 @@ namespace spacer {
                     m_is_dl = test_term(a->get_arg(i));
                 }
             }
-
+            
             if (!m_is_dl) {
                 char const* msg = "non-diff: ";
                 if (m_test_for_utvpi) {
@@ -431,10 +431,10 @@ namespace spacer {
                 IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
             }
         }
-
+        
         bool is_dl() const { return m_is_dl; }
     };
-
+    
     bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
         test_diff_logic test(m);
         expr_fast_mark1 mark;
@@ -443,7 +443,7 @@ namespace spacer {
         }
         return test.is_dl();
     }
-
+    
     bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
         test_diff_logic test(m);
         test.test_for_utvpi();
@@ -455,7 +455,7 @@ namespace spacer {
     }
 
 
-    void subst_vars(ast_manager& m,
+    void subst_vars(ast_manager& m, 
                     app_ref_vector const& vars,
                     model* M, expr_ref& fml) {
         expr_safe_replace sub (m);
@@ -506,7 +506,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
             flatten_and (fml, flat);
             fml = mk_and(flat);
         }
-
+        
 
         // uncomment for benchmarks
         //to_mbp_benchmark(verbose_stream(), fml, vars);
@@ -523,7 +523,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
         qe_lite qe(m, p, false);
         qe (vars, fml);
         rw (fml);
-
+        
         TRACE ("spacer_mbp",
                tout << "After qe_lite:\n";
                tout << mk_pp (fml, m) << "\n";
@@ -531,7 +531,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
 
         SASSERT (!m.is_false (fml));
 
-
+        
         // sort out vars into bools, arith (int/real), and arrays
         for (app* v : vars) {
             if (m.is_bool (v)) {
@@ -545,7 +545,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
                 arith_vars.push_back (v);
             }
         }
-
+        
         // substitute Booleans
         if (!bool_sub.empty()) {
             bool_sub (fml);
@@ -555,13 +555,13 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
             TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; );
             bool_sub.reset ();
         }
-
+        
         TRACE ("spacer_mbp",
                tout << "Array vars:\n";
                tout << array_vars;);
-
+        
         vars.reset ();
-
+        
         // project arrays
         {
             scoped_no_proof _sp (m);
@@ -572,14 +572,14 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
             srw (fml);
             SASSERT (!m.is_false (fml));
         }
-
+        
         TRACE ("spacer_mbp",
                tout << "extended model:\n";
                model_pp (tout, *M);
                tout << "Auxiliary variables of index and value sorts:\n";
                tout << vars;
                );
-
+        
         if (vars.empty()) { break; }
         }
 

src/qe/qe_arrays.cpp

@@ -157,8 +157,8 @@ namespace qe {
 
     static bool is_eq(expr_ref_vector const& xs, expr_ref_vector const& ys) {
         for (unsigned i = 0; i < xs.size(); ++i) if (xs[i] != ys[i]) return false;
-        return true;
+                return true;
-    }
+            } 
 
     static bool is_eq(vector<rational> const& xs, vector<rational> const& ys) {
         for (unsigned i = 0; i < xs.size(); ++i) if (xs[i] != ys[i]) return false;
@@ -984,9 +984,9 @@ namespace qe {
                     TRACE("qe", tout << "non-arithmetic index sort for Ackerman" << mk_pp(srt, m) << "\n";);
                     // TBD: generalize to also bit-vectors.
                     is_numeric = false;
-                }                
+                }
             }
-            
+
             unsigned start = m_idxs.size (); // append at the end
             for (app * a : sel_terms) {
                 expr_ref_vector idxs(m, arity, a->get_args() + 1);
@@ -1018,13 +1018,13 @@ namespace qe {
             }
 
             if (is_numeric) {
-                // sort reprs by their value and add a chain of strict inequalities
+            // sort reprs by their value and add a chain of strict inequalities
-                compare_idx cmp(*this);
+            compare_idx cmp(*this);
-                std::sort(m_idxs.begin() + start, m_idxs.end(), cmp);                
+            std::sort(m_idxs.begin() + start, m_idxs.end(), cmp);
                 for (unsigned i = start; i + 1 < m_idxs.size(); ++i) {
-                    m_idx_lits.push_back (mk_lex_lt(m_idxs[i].idx, m_idxs[i+1].idx));
+                m_idx_lits.push_back (mk_lex_lt(m_idxs[i].idx, m_idxs[i+1].idx));
-                }
             }
+        }
             else if (arity == 1) {
                 // create distinct constraint.
                 expr_ref_vector xs(m);
@@ -1163,12 +1163,12 @@ namespace qe {
                     return BR_DONE;
                 }
                 return BR_FAILED;
-            }
+    }
 
             lbool compare(expr* x, expr* y) {
                 NOT_IMPLEMENTED_YET();
                 return l_undef;
-            }
+    }
         };
 
         struct indices {
@@ -1181,10 +1181,10 @@ namespace qe {
                 for (unsigned i = 0; i < n; ++i) {
                     VERIFY(model.eval(vars[i], val));
                     m_values.push_back(val);
-                }
+    }
             }
         };
-        
+
         ast_manager& m;
         array_util   a;
         scoped_ptr<contains_app> m_var;
@@ -1194,6 +1194,67 @@ namespace qe {
 
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
             return false;
+    }
+
+        bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
+
+            TRACE("qe", tout << mk_pp(var, m) << "\n" << lits;);
+            m_var = alloc(contains_app, m, var);
+
+            // reduce select-store redeces based on model.
+            // rw_cfg rw(m);
+            // rw(lits);
+
+            // try first to solve for var.
+            if (solve_eq(model, vars, lits)) {
+                return true;
+            } 
+
+            app_ref_vector selects(m);
+
+            // check that only non-select occurrences are in disequalities.
+            if (!check_diseqs(lits, selects)) {
+                TRACE("qe", tout << "Could not project " << mk_pp(var, m) << " for:\n" << lits << "\n";);
+                return false;
+            }
+
+            // remove disequalities.
+            elim_diseqs(lits);
+
+            // Ackerman reduction on remaining select occurrences
+            // either replace occurrences by model value or other node
+            // that is congruent to model value.
+
+            ackermanize_select(model, selects, vars, lits);
+           
+            TRACE("qe", tout << selects << "\n" << lits << "\n";);
+            return true;
+        }
+
+        void ackermanize_select(model& model, app_ref_vector const& selects, app_ref_vector& vars, expr_ref_vector& lits) {
+            expr_ref_vector vals(m), reps(m);
+            expr_ref val(m);
+            expr_safe_replace sub(m);
+
+            if (selects.empty()) {
+                return;
+            }
+
+            app_ref sel(m);
+            for (unsigned i = 0; i < selects.size(); ++i) {                
+                sel = m.mk_fresh_const("sel", m.get_sort(selects[i]));
+                VERIFY (model.eval(selects[i], val));
+                model.register_decl(sel->get_decl(), val);
+                vals.push_back(to_app(val));
+                reps.push_back(val);               // TODO: direct pass could handle nested selects.
+                vars.push_back(sel);
+                sub.insert(selects[i], val);
+            }
+
+            sub(lits);
+            remove_true(lits);
+            project_plugin::partition_args(model, selects, lits);
+            project_plugin::partition_values(model, reps, lits);
         }
 
         void remove_true(expr_ref_vector& lits) {
@@ -1216,6 +1277,80 @@ namespace qe {
             }
         }
         
+        // check that x occurs only under selects or in disequalities.
+        bool check_diseqs(expr_ref_vector const& lits, app_ref_vector& selects) {
+            expr_mark mark;
+            ptr_vector<app> todo;
+            app* e;
+            for (unsigned i = 0; i < lits.size(); ++i) {
+                e = to_app(lits[i]);
+                if (is_diseq_x(e)) {
+                    continue;
+                }
+                if (contains_x(e)) {
+                    todo.push_back(e);
+                }
+            }
+            while (!todo.empty()) {
+                e = todo.back();
+                todo.pop_back();                    
+                if (mark.is_marked(e)) {
+                    continue;
+                }
+                mark.mark(e);
+                if (m_var->x() == e) {
+                    return false;
+                }
+                unsigned start = 0;
+                if (a.is_select(e)) {
+                    if (e->get_arg(0) == m_var->x()) {
+                        start = 1;
+                        selects.push_back(e);
+                    } 
+                }
+                for (unsigned i = start; i < e->get_num_args(); ++i) {
+                    todo.push_back(to_app(e->get_arg(i)));
+                }
+            }
+            return true;
+        }
+
+        void elim_diseqs(expr_ref_vector& lits) {
+            for (unsigned i = 0; i < lits.size(); ++i) {
+                if (is_diseq_x(lits[i].get())) {
+                    project_plugin::erase(lits, i);
+                }
+            }
+        }
+
+        bool is_update_x(app* e) {
+            do {
+                if (m_var->x() == e) {
+                    return true;
+                }
+                if (a.is_store(e) && contains_x(e->get_arg(0))) {
+                    for (unsigned i = 1; i < e->get_num_args(); ++i) {
+                        if (contains_x(e->get_arg(i))) {
+                            return false;
+                        }
+                    }
+                    e = to_app(e->get_arg(0));
+                    continue;
+                }
+            }
+            while (false);
+            return false;
+        }
+
+        bool is_diseq_x(expr* e) {
+            expr *f, * s, *t;
+            if (m.is_not(e, f) && m.is_eq(f, s, t)) {
+                if (contains_x(s) && !contains_x(t) && is_update_x(to_app(s))) return true;
+                if (contains_x(t) && !contains_x(s) && is_update_x(to_app(t))) return true;
+            }
+            return false;
+        }
+
         bool solve_eq(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
             // find an equality to solve for.
             expr* s, *t;
@@ -1367,13 +1502,7 @@ namespace qe {
     }
     
     bool array_project_plugin::operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
-        ast_manager& m = vars.get_manager();
+        return (*m_imp)(model, var, vars, lits);
-        app_ref_vector vvars(m, 1, &var);
-        expr_ref fml = mk_and(lits);
-        (*this)(model, vvars, fml, vars, false);
-        lits.reset();
-        flatten_and(fml, lits);
-        return true;
     }
 
     bool array_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
@@ -1390,11 +1519,11 @@ namespace qe {
         array_project_eqs_util pe (m);
         pe (mdl, arr_vars, fml, aux_vars);
         TRACE ("qe",
-               tout << "Projected array eqs: " << fml << "\n";
+               tout << "Projected array eqs:\n" << fml << "\n";
-               tout << "Remaining array vars: " << arr_vars << "\n";
+               tout << "Remaining array vars:\n" << arr_vars;
-               tout << "Aux vars: " << aux_vars << "\n";
+               tout << "Aux vars:\n" << aux_vars;
               );
-
+        
         // 2. reduce selects
         array_select_reducer rs (m);
         rs (mdl, arr_vars, fml, reduce_all_selects);
@@ -1406,8 +1535,8 @@ namespace qe {
         ps (mdl, arr_vars, fml, aux_vars);
 
         TRACE ("qe",
-               tout << "Projected array selects: " << fml << "\n";
+               tout << "Projected array selects:\n" << fml << "\n";
-               tout << "All aux vars: " << aux_vars << "\n";
+               tout << "All aux vars:\n" << aux_vars;
               );
     }
 

src/qe/qe_mbp.cpp

@@ -77,6 +77,40 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
     return expr_ref(nullptr, m);
 }
 
+void project_plugin::partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits) {
+    ast_manager& m = vals.get_manager();
+    expr_ref val(m);
+    expr_ref_vector trail(m), reps(m);
+    obj_map<expr, expr*> roots;
+    for (unsigned i = 0; i < vals.size(); ++i) {
+        expr* v = vals[i], *root;
+        VERIFY (model.eval(v, val));
+        if (roots.find(val, root)) {
+            lits.push_back(m.mk_eq(v, root));
+        }
+        else {
+            roots.insert(val, v);
+            trail.push_back(val);
+            reps.push_back(v);
+        }
+    }
+    if (reps.size() > 1) {                
+        lits.push_back(mk_distinct(reps));
+    }
+}
+
+void project_plugin::partition_args(model& model, app_ref_vector const& selects, expr_ref_vector& lits) {
+    ast_manager& m = selects.get_manager();
+    if (selects.empty()) return;
+    unsigned num_args = selects[0]->get_decl()->get_arity();
+    for (unsigned j = 1; j < num_args; ++j) {
+        expr_ref_vector args(m);            
+        for (unsigned i = 0; i < selects.size(); ++i) {
+            args.push_back(selects[i]->get_arg(j));
+        }
+        project_plugin::partition_values(model, args, lits);
+    }
+}
 
 void project_plugin::erase(expr_ref_vector& lits, unsigned& i) {
     lits[i] = lits.back();
@@ -100,6 +134,7 @@ class mbp::impl {
 
     // parameters
     bool m_reduce_all_selects;
+    bool m_native_mbp;
     bool m_dont_sub;
 
     void add_plugin(project_plugin* p) {
@@ -287,7 +322,8 @@ class mbp::impl {
         void operator() (app *n) {
             expr *e1, *e2;
             if (m_array.is_select (n)) {
-                for (expr * arg : *n) {
+                for (unsigned i = 1; i < n->get_num_args(); ++i) {
+                    expr * arg = n->get_arg(i);
                     if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) 
                         m_res.push_back (arg);
                 } 
@@ -340,7 +376,8 @@ class mbp::impl {
         // -- evaluate to initialize eval cache
         (void) eval (fml);
         unsigned j = 0;
-        for (app * v : vars) {
+        for (unsigned i = 0; i < vars.size (); ++i) {
+            app* v = vars.get(i);
             if (!project_var (eval, v, fml)) {
                 vars[j++] = v;
             }
@@ -350,6 +387,7 @@ class mbp::impl {
 
 public:
 
+
     opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
         arith_project_plugin arith(m);
         return arith.maximize(fmls, mdl, t, ge, gt);
@@ -490,6 +528,7 @@ public:
     void updt_params(params_ref const& p) {
         m_params.append(p);
         m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false);
+        m_native_mbp = m_params.get_bool("native_mbp", false);
         m_dont_sub   = m_params.get_bool("dont_sub", false);
     }
 
@@ -508,7 +547,6 @@ public:
 
     bool validate_model(model& model, expr_ref_vector const& fmls) {
         expr_ref val(m);
-        model_evaluator eval(model);
         for (expr * f : fmls) {
             VERIFY(model.eval(f, val) && m.is_true(val)); 
         }
@@ -637,19 +675,26 @@ public:
                    tout << "extended model:\n";
                    model_pp (tout, mdl);
                    tout << "Auxiliary variables of index and value sorts:\n";
-                   tout << vars << "\n";
+                   tout << vars;
                    );            
             
         }
         // project reals and ints
         if (!arith_vars.empty ()) {
-            TRACE ("qe", tout << "Arith vars: " << arith_vars << "\n";);
+            TRACE ("qe", tout << "Arith vars:\n" << arith_vars;);
                         
+            if (m_native_mbp) {
             expr_ref_vector fmls(m);
             flatten_and (fml, fmls);
             
             (*this)(true, arith_vars, mdl, fmls);
             fml = mk_and (fmls);
+                SASSERT (arith_vars.empty ());
+            } 
+            else {
+                NOT_IMPLEMENTED_YET();
+                // qe::arith_project (mdl, arith_vars, fml);
+            }
                         
             TRACE ("qe",
                    tout << "Projected arith vars:\n" << fml << "\n";
@@ -693,6 +738,7 @@ void mbp::updt_params(params_ref const& p) {
        
 void mbp::get_param_descrs(param_descrs & r) {
     r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects");
+    r.insert("native_mbp", CPK_BOOL, "(default: false) switch between native and spacer tailored mbp");
     r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables");
 }