experiment with arithmetic core generalizers

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

src/muz_qe/fixedpoint_params.pyg

@@ -44,6 +44,7 @@ def_module_params('fixedpoint',
                           ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
                           ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
                           ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
+                          ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"),
                           ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
                           ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
                                                                         "checking for reachability (not only during cube weakening)"),

src/muz_qe/pdr_context.cpp

@@ -1477,6 +1477,10 @@ namespace pdr {
         if (m_params.inductive_reachability_check()) {
             m_core_generalizers.push_back(alloc(core_induction_generalizer, *this));
         }
+        if (m_params.use_arith_inductive_generalizer()) {
+            m_core_generalizers.push_back(alloc(core_arith_inductive_generalizer, *this));
+        }
+        
     }
 
     void context::get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info>& rs) const {

src/muz_qe/pdr_generalizers.cpp

@@ -28,7 +28,9 @@ Revision History:
 namespace pdr {
 
 
-    //
+    // ------------------------
+    // core_bool_inductive_generalizer
+
     // main propositional induction generalizer.
     // drop literals one by one from the core and check if the core is still inductive.
     //    
@@ -97,6 +99,9 @@ namespace pdr {
         }
     }
 
+    // ------------------------
+    // core_farkas_generalizer 
+
     // 
     // for each disjunct of core:
     //     weaken predecessor.
@@ -142,6 +147,158 @@ namespace pdr {
     }
 
 
+    // -----------------------------
+    // core_arith_inductive_generalizer 
+
+    core_arith_inductive_generalizer::core_arith_inductive_generalizer(context& ctx):
+        core_generalizer(ctx), 
+        m(ctx.get_manager()),
+        a(m),
+        m_refs(m) {}
+
+    void core_arith_inductive_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
+        if (core.size() <= 1) {
+            return;
+        }
+        reset();
+        expr_ref e(m), t1(m), t2(m), t3(m);
+        rational r;
+        
+        TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; });
+
+        svector<eq> eqs;
+        get_eqs(core, eqs);
+        
+        for (unsigned eq = 0; eq < eqs.size(); ++eq) {
+            rational r = eqs[eq].m_value;
+            expr* x = eqs[eq].m_term;
+            unsigned k = eqs[eq].m_i;
+            unsigned l = eqs[eq].m_j;
+
+            expr_ref_vector new_core(m);
+            for (unsigned i = 0; i < core.size(); ++i) {
+                if (i == k || k == l) {
+                    new_core.push_back(m.mk_true());
+                }
+                else {
+                    if (!substitute_alias(r, x, core[i].get(), e)) {
+                        e = core[i].get();
+                    }
+                    new_core.push_back(e);
+                }
+            }
+            if (abs(r) >= rational(2) && a.is_int(x)) {
+                new_core[k] = m.mk_eq(a.mk_mod(x, a.mk_numeral(abs(r), true)), a.mk_numeral(rational(0), true));
+                new_core[l] = a.mk_ge(x, a.mk_numeral(r, true));
+            }
+
+            bool inductive = n.pt().check_inductive(n.level(), new_core, uses_level);
+
+            IF_VERBOSE(1, 
+                       verbose_stream() << (inductive?"":"non") << "inductive\n";
+                       for (unsigned j = 0; j < new_core.size(); ++j) { 
+                           verbose_stream() << mk_pp(new_core[j].get(), m) << "\n"; 
+                       });
+
+            if (inductive) {
+                core.reset();
+                core.append(new_core);
+            }
+        }
+    }    
+
+    void core_arith_inductive_generalizer::insert_bound(bool is_lower, expr* x, rational const& r, unsigned i) {
+        if (r.is_neg()) {
+            expr_ref e(m);
+            e = a.mk_uminus(x);
+            m_refs.push_back(e);
+            x = e;
+            is_lower = !is_lower;
+        }
+
+        if (is_lower) {
+            m_lb.insert(abs(r), std::make_pair(x, i));
+        }
+        else {
+            m_ub.insert(abs(r), std::make_pair(x, i));
+        }
+    }
+
+    void core_arith_inductive_generalizer::reset() {
+        m_refs.reset();
+        m_lb.reset();
+        m_ub.reset();
+    }
+
+    void core_arith_inductive_generalizer::get_eqs(expr_ref_vector const& core, svector<eq>& eqs) {
+        expr* e1, *x, *y;
+        expr_ref e(m);
+        rational r;
+
+        for (unsigned i = 0; i < core.size(); ++i) {
+            e = core[i];
+            if (m.is_not(e, e1) && a.is_le(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) {
+                // not (<= x r) <=> x >= r + 1
+                insert_bound(true, x, r + rational(1), i);
+            }
+            else if (m.is_not(e, e1) && a.is_ge(e1, x, y) && a.is_numeral(y, r) && a.is_int(x)) {
+                // not (>= x r) <=> x <= r - 1
+                insert_bound(false, x, r - rational(1), i);
+            }
+            else if (a.is_le(e, x, y) && a.is_numeral(y, r)) {
+                insert_bound(false, x, r, i);
+            }
+            else if (a.is_ge(e, x, y) && a.is_numeral(y, r)) {
+                insert_bound(true, x, r, i);
+            }
+        }
+        bounds_t::iterator it = m_lb.begin(), end = m_lb.end();
+        for (; it != end; ++it) {
+            rational r = it->m_key;
+            vector<term_loc_t> & terms1 = it->m_value;
+            vector<term_loc_t> terms2;
+            if (r >= rational(2) && m_ub.find(r, terms2)) {
+                bool done = false;
+                for (unsigned i = 0; !done && i < terms1.size(); ++i) {
+                    for (unsigned j = 0; !done && j < terms2.size(); ++j) {
+                        expr* t1 = terms1[i].first;
+                        expr* t2 = terms2[j].first;
+                        if (t1 == t2) {
+                            eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second));
+                            done = true;
+                        }
+                        else {
+                            e = m.mk_eq(t1, t2);
+                            th_rewriter rw(m);
+                            rw(e);
+                            if (m.is_true(e)) {
+                                eqs.push_back(eq(t1, r, terms1[i].second, terms2[j].second));
+                                done = true;                                
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    bool core_arith_inductive_generalizer::substitute_alias(rational const& r, expr* x, expr* e, expr_ref& result) {
+        rational r2;
+        expr* y, *z, *e1;
+        if (m.is_not(e, e1) && substitute_alias(r, x, e1, result)) {
+            result = m.mk_not(result);
+            return true;
+        }
+        if (a.is_le(e, y, z) && a.is_numeral(z, r2) && r == r2) {
+            result = a.mk_le(y, x);
+            return true;
+        }
+        if (a.is_ge(e, y, z) && a.is_numeral(z, r2) && r == r2) {
+            result = a.mk_ge(y, x);
+            return true;
+        }
+        return false;
+    }
 
 
     // 

src/muz_qe/pdr_generalizers.h

@@ -33,6 +33,37 @@ namespace pdr {
         virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
     };
 
+    template <typename T>
+    class r_map : public map<rational, T, rational::hash_proc, rational::eq_proc> {
+    };
+
+    class core_arith_inductive_generalizer : public core_generalizer {
+        typedef std::pair<expr*, unsigned> term_loc_t;
+        typedef r_map<vector<term_loc_t> > bounds_t;
+
+        ast_manager&    m;
+        arith_util      a;
+        expr_ref_vector m_refs;
+        bounds_t        m_lb;
+        bounds_t        m_ub;
+
+        struct eq {
+            expr*    m_term;
+            rational m_value;
+            unsigned m_i;
+            unsigned m_j;
+            eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {}
+        };
+        void reset();
+        void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i);
+        void get_eqs(expr_ref_vector const& core, svector<eq>& eqs);
+        bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result);
+    public:
+        core_arith_inductive_generalizer(context& ctx);
+        virtual ~core_arith_inductive_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };
+
     class core_farkas_generalizer : public core_generalizer {
         farkas_learner m_farkas_learner;
     public:

src/muz_qe/pdr_smt_context_manager.cpp

@@ -88,7 +88,6 @@ namespace pdr {
                   for (unsigned i = 0; i < assumptions.size(); ++i) {
                       pp.add_assumption(assumptions[i].get());
                   }
-                  pp.display_smt2(tout, m.mk_true());
 
                   static unsigned lemma_id = 0;
                   std::ostringstream strm;
@@ -97,6 +96,7 @@ namespace pdr {
                   pp.display_smt2(out, m.mk_true());
                   out.close();
                   lemma_id++;
+                  tout << "pdr_check: " << strm.str() << "\n";
               });
         lbool result = m_context.check(assumptions.size(), assumptions.c_ptr());
         if (!m.is_true(m_pred)) {