add laxer check for oeq_quant_intro

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

src/ast/ast.cpp

@@ -2847,10 +2847,10 @@ proof * ast_manager::mk_bind_proof(quantifier * q, proof * p) {
 }
 
 proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
-	if (!p) return nullptr;
+    if (!p) return nullptr;
-	SASSERT(q1->get_num_decls() == q2->get_num_decls());
+    SASSERT(q1->get_num_decls() == q2->get_num_decls());
-	SASSERT(has_fact(p));
+    SASSERT(has_fact(p));
-	SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p)));
+    SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p)));
     return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2));
 }
 
@@ -2858,7 +2858,7 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof
     if (!p) return nullptr;
     SASSERT(q1->get_num_decls() == q2->get_num_decls());
     SASSERT(has_fact(p));
-    SASSERT(is_oeq(get_fact(p)));
+    SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p)));
     return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_oeq(q1, q2));
 }
 

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -480,11 +480,9 @@ public:
         solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
         solver_ref sNotB = sf(m, p, false /* no proofs */, true, true, symbol::null);
         sA->assert_expr(a);
-        sNotA->assert_expr(m.mk_not(a));
         sB->assert_expr(b);
-        sNotB->assert_expr(m.mk_not(b));
         qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get());
-        qe::euf_arith_mbi_plugin pB(sB.get(), sNotB.get());
+        qe::prop_mbi_plugin pB(sB.get());
         pA.set_shared(vars);
         pB.set_shared(vars);
         lbool res = mbi.pogo(pA, pB, itp);

src/math/simplex/model_based_opt.cpp

@@ -266,6 +266,7 @@ namespace opt {
     void model_based_opt::update_value(unsigned x, rational const& val) {
         rational old_val = m_var2value[x];
         m_var2value[x] = val;
+        SASSERT(val.is_int() || !is_int(x));
         unsigned_vector const& row_ids = m_var2row_ids[x];
         for (unsigned row_id : row_ids) {
             rational coeff = get_coefficient(row_id, x);
@@ -530,6 +531,7 @@ namespace opt {
         SASSERT(t_le == dst.m_type && t_le == src.m_type);
         SASSERT(src_c.is_int());
         SASSERT(dst_c.is_int());
+        SASSERT(m_var2value[x].is_int());
 
         rational abs_src_c = abs(src_c);
         rational abs_dst_c = abs(dst_c);            
@@ -805,6 +807,7 @@ namespace opt {
         unsigned v = m_var2value.size();
         m_var2value.push_back(value);
         m_var2is_int.push_back(is_int);
+        SASSERT(value.is_int() || !is_int);
         m_var2row_ids.push_back(unsigned_vector());
         return v;
     }
@@ -1017,7 +1020,6 @@ namespace opt {
             else {
                 result = def(m_rows[glb_index], x);
             }
-            m_var2value[x] = eval(result);
         }
 
         // The number of matching lower and upper bounds is small.
@@ -1114,8 +1116,7 @@ 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;

src/qe/qe_arith.cpp

@@ -41,7 +41,7 @@ namespace qe {
         bool              m_check_purified;  // check that variables are properly pure 
 
         void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
-            TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
+            // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
             rational w;
             if (ts.find(x, w)) {
                 ts.insert(x, w + v);
@@ -92,8 +92,8 @@ namespace qe {
                 rational r1, r2;
                 expr_ref val1 = eval(e1); 
                 expr_ref val2 = eval(e2);
-                TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";);
+                //TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";);
-                TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";);
+                //TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";);
                 if (!a.is_numeral(val1, r1)) return false;
                 if (!a.is_numeral(val2, r2)) return false;
                 SASSERT(r1 != r2);
@@ -306,14 +306,14 @@ namespace qe {
                 return vector<def>();
             }
             model_evaluator eval(model);
-            TRACE("qe", model_smt2_pp(tout, m, model, 0););
+            TRACE("qe", tout << model;);
             // eval.set_model_completion(true);
 
             opt::model_based_opt mbo;
             obj_map<expr, unsigned> tids;
             expr_ref_vector pinned(m);
             unsigned j = 0;
-            TRACE("qe", tout << "fmls: " << fmls << "\n";);
+            TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
             for (unsigned i = 0; i < fmls.size(); ++i) {
                 expr * fml = fmls.get(i);
                 if (!linearize(mbo, eval, fml, fmls, tids)) {
@@ -325,7 +325,6 @@ namespace qe {
                 }
             }
             fmls.shrink(j);
-            TRACE("qe", tout << "linearized: " << fmls << "\n";);
 
             // fmls holds residue,
             // mbo holds linear inequalities that are in scope

src/qe/qe_mbi.cpp

@@ -25,52 +25,6 @@ Notes:
   Other theories: DT, ARR reduced to EUF
   BV is EUF/Boolean.
 
-  Purify EUF1 & LIRA1 & EUF2 & LIRA2
-
-  Then EUF1 & EUF2   |- false
-       LIRA1 & LIRA2 |- false
-
-  Sketch of approach by example:
-
-       A: s <= 2a <= t     & f(a) = q
-
-       B: t <= 2b <= s + 1 & f(b) != q
-
-  1. Extract arithmetic consequences of A over shared vocabulary.
-
-       A -> s <= t & (even(t) | s < t)
-
-  2a. Send to B, have B solve shared variables with EUF_B.
-        epsilon b . B & A_pure
-        epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t)
-        = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t)
-        = even(t) & t = s
-        b := t div 2
-
-      B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1
-
-  3a. Send purified result to A
-      A & B_pure -> false
-
-      Invoke the ping-pong principle to extract interpolant.
-
-  2b. Solve for shared variables with EUF.
-
-    epsilon a . A
-  = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q
-
-  3b. Send to B. Produces core
-          s < t & f((s + 1) div 2) = q
-
-  4b Solve again in arithmetic for shared variables with EUF.
-
-    epsion a . A & (s >= t | f((s + 1) div 2) != q)
-
-         a := t div 2 | s = t & f(t div 2) = q & even(t)
-
-    Send to B, produces core (s != t | f(t div 2) != q)
-
-  5b. There is no longer a solution for A. A is unsat.
 
 --*/
 
@@ -240,15 +194,24 @@ namespace qe {
     // euf_arith_mbi
 
     struct euf_arith_mbi_plugin::is_atom_proc {
-        ast_manager& m;
+        ast_manager&         m;
-        expr_ref_vector& m_atoms;
+        expr_ref_vector&     m_atoms;
-        is_atom_proc(expr_ref_vector& atoms): m(atoms.m()), m_atoms(atoms) {}
+        obj_hashtable<expr>& m_atom_set;
+
+        is_atom_proc(expr_ref_vector& atoms, obj_hashtable<expr>& atom_set): 
+            m(atoms.m()), m_atoms(atoms), m_atom_set(atom_set) {}
+
         void operator()(app* a) {
-            if (m.is_eq(a)) {
+            if (m_atom_set.contains(a)) {
+                // continue
+            }
+            else if (m.is_eq(a)) {
                 m_atoms.push_back(a);
+                m_atom_set.insert(a);
             }
             else if (m.is_bool(a) && a->get_family_id() != m.get_basic_family_id()) {
                 m_atoms.push_back(a);
+                m_atom_set.insert(a);
             }
         }
         void operator()(expr*) {}
@@ -275,38 +238,44 @@ namespace qe {
     euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot):
         mbi_plugin(s->get_manager()),
         m_atoms(m),
+        m_fmls(m),
         m_solver(s),
         m_dual_solver(sNot) {
         params_ref p;
         p.set_bool("core.minimize", true);
         m_solver->updt_params(p);
         m_dual_solver->updt_params(p);
-        expr_ref_vector fmls(m);
+        m_solver->get_assertions(m_fmls);
-        m_solver->get_assertions(fmls);
+        collect_atoms(m_fmls);
+    }
+
+    void euf_arith_mbi_plugin::collect_atoms(expr_ref_vector const& fmls) {
         expr_fast_mark1 marks;
-        is_atom_proc proc(m_atoms);
+        is_atom_proc proc(m_atoms, m_atom_set);
         for (expr* e : fmls) {
             quick_for_each_expr(proc, marks, e);
         }
     }
 
     bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) {
-            model_evaluator mev(*mdl.get());
+        lits.reset();
-            lits.reset();
+        for (expr* e : m_atoms) {
-            for (expr* e : m_atoms) {
+            if (mdl->is_true(e)) {
-                if (mev.is_true(e)) {
+                lits.push_back(e);
-                    lits.push_back(e);
-                }
-                else if (mev.is_false(e)) {
-                    lits.push_back(m.mk_not(e));
-                }
             }
-            TRACE("qe", tout << "atoms from model: " << lits << "\n";);
+            else if (mdl->is_false(e)) {
-        lbool r = m_dual_solver->check_sat(lits);
+                lits.push_back(m.mk_not(e));
+            }
+        }
+        TRACE("qe", tout << "atoms from model: " << lits << "\n";);
+        solver_ref dual = m_dual_solver->translate(m, m_dual_solver->get_params());
+        dual->assert_expr(mk_not(mk_and(m_fmls)));
+        lbool r = dual->check_sat(lits);
+        TRACE("qe", dual->display(tout << "dual result " << r << "\n"););
         if (l_false == r) {
-                // use the dual solver to find a 'small' implicant
+            // use the dual solver to find a 'small' implicant
-                lits.reset();
+            lits.reset();
-            m_dual_solver->get_unsat_core(lits);
+            dual->get_unsat_core(lits);
             return true;
         }
         else {
@@ -351,15 +320,15 @@ namespace qe {
             for (auto const& def : defs) {
                 lits.push_back(m.mk_eq(def.var, def.term));
             }
-            TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";);
+            TRACE("qe", tout << "# arith defs " << defs.size() << " avars: " << avars << " " << lits << "\n";);
 
             // 3. Project the remaining literals with respect to EUF.
             term_graph tg(m);
             tg.set_vars(m_shared, false);
             tg.add_lits(lits);
             lits.reset();
-            lits.append(tg.project(*mdl));
+            //lits.append(tg.project(*mdl));
-            //lits.append(tg.project());
+            lits.append(tg.project());
             TRACE("qe", tout << "project: " << lits << "\n";);
             return mbi_sat;
         }
@@ -374,7 +343,9 @@ namespace qe {
     }
 
     void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) {
-        m_solver->assert_expr(mk_not(mk_and(lits)));
+        collect_atoms(lits);
+        m_fmls.push_back(mk_not(mk_and(lits)));
+        m_solver->assert_expr(m_fmls.back());
     }
 
 

src/qe/qe_mbi.h

@@ -104,17 +104,19 @@ namespace qe {
     };
 
     class euf_arith_mbi_plugin : public mbi_plugin {
-        expr_ref_vector m_atoms;
+        expr_ref_vector     m_atoms;
-        solver_ref   m_solver;
+        obj_hashtable<expr> m_atom_set;
-        solver_ref   m_dual_solver;
+        expr_ref_vector     m_fmls;
+        solver_ref          m_solver;
+        solver_ref          m_dual_solver;
         struct is_atom_proc;
         struct is_arith_var_proc;
 
         app_ref_vector get_arith_vars(expr_ref_vector const& lits);
         bool get_literals(model_ref& mdl, expr_ref_vector& lits);
-
+        void collect_atoms(expr_ref_vector const& fmls);
     public:
-        euf_arith_mbi_plugin(solver* s, solver* sNot);
+        euf_arith_mbi_plugin(solver* s, solver* emptySolver);
         ~euf_arith_mbi_plugin() override {}
         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
         void block(expr_ref_vector const& lits) override;

src/qe/qe_solve_plugin.cpp

@@ -99,7 +99,7 @@ namespace qe {
                     v = e;
                     a_val = rational(1)/a_val;
                     t = mk_term(is_int, a_val, sign, done);
-                    TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << e << " := " << t << "\n";);
+                    TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << t << "\n";);
                     return true;
                 }
                 else {

src/qe/qe_term_graph.cpp

@@ -125,7 +125,7 @@ namespace qe {
             children(term const* _t):t(*_t) {}
             ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
             ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
-        };
+        };        
 
         // Congruence table hash function is based on
         // roots of children and function declaration.
@@ -198,8 +198,23 @@ namespace qe {
             }
             while (curr != this);
         }
+
+        std::ostream& display(std::ostream& out) const {
+            out << "expr: " << m_expr << " class: ";
+            term const* r = this;
+            do {
+                out << r->get_id() << " ";
+                r = &r->get_next();
+            }
+            while (r != this);
+            out << "\n";
+            return out;
+        }
     };
 
+    static std::ostream& operator<<(std::ostream& out, term const& t) {
+        return t.display(out);
+    }
 
     bool term_graph::is_variable_proc::operator()(const expr * e) const {
         if (!is_app(e)) return false;
@@ -516,10 +531,7 @@ namespace qe {
 
     void term_graph::display(std::ostream &out) {
         for (term * t : m_terms) {
-            out << mk_pp(t->get_expr(), m) << " is root " << t->is_root()
+            out << *t;
-                << " cls sz " << t->get_class_size()
-                << " term " << t
-                << "\n";
         }
     }
 
@@ -608,7 +620,7 @@ namespace qe {
                 term* t = worklist.back();
                 worklist.pop_back();
                 t->set_mark(false);
-                if (m_term2app.contains(t->get_id()))
+                if (m_term2app.contains(t->get_id())) 
                     continue;
                 if (!t->is_theory() && is_projected(*t))
                     continue;
@@ -641,6 +653,7 @@ namespace qe {
             // and can be mined using other means, such as theory
             // aware core minimization
             m_tg.reset_marks();
+            TRACE("qe", m_tg.display(tout << "after purify\n"););
         }
 
         void solve_core() {
@@ -695,6 +708,7 @@ namespace qe {
                 if (!m.is_eq(lit) && find_app(lit, e))
                     res.push_back(e);
             }
+            TRACE("qe", tout << "literals: " << res << "\n";);
         }
 
         void mk_pure_equalities(const term &t, expr_ref_vector &res) {
@@ -736,7 +750,8 @@ namespace qe {
             while (r != &t);
         }
 
-        void mk_equalities(bool pure, expr_ref_vector &res) {
+        template<bool pure>
+        void mk_equalities(expr_ref_vector &res) {
             for (term *t : m_tg.m_terms) {
                 if (!t->is_root()) continue;
                 if (!m_root2rep.contains(t->get_id())) continue;
@@ -745,14 +760,15 @@ namespace qe {
                 else
                     mk_unpure_equalities(*t, res);
             }
+            TRACE("qe", tout << "literals: " << res << "\n";);
         }
 
         void mk_pure_equalities(expr_ref_vector &res) {
-            return mk_equalities(true, res);
+            mk_equalities<true>(res);
         }
 
         void mk_unpure_equalities(expr_ref_vector &res) {
-            return mk_equalities(false, res);
+            mk_equalities<false>(res);
         }
 
         // TBD: generalize for also the case of a (:var n)
@@ -813,6 +829,11 @@ namespace qe {
             TRACE("qe", tout << "after distinct: " << res << "\n";);
         }
 
+        std::ostream& display(std::ostream& out) const {
+            
+            return out;
+        }
+
     public:
         projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}