na

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/smt/smt_context.cpp

@@ -1601,7 +1601,7 @@ namespace smt {
             if (inconsistent())
                 return false;
         }
-#if 0
+#if 1
         if (at_search_level() && induction::should_try(*this)) {
             get_induction()();
         }

src/smt/smt_induction.cpp

@@ -158,7 +158,7 @@ enode_vector induction_lemmas::induction_positions(enode* n) {
     for (unsigned i = 0; i < todo.size(); ++i) {
         n = todo[i];
         for (enode* a : smt::enode::args(n)) {
-            add_todo(a);        
+            add_todo(a);
             if (!a->is_marked2() && viable_induction_term(n, a)) {
                 result.push_back(a);
                 a->set_mark2();
@@ -171,86 +171,7 @@ enode_vector induction_lemmas::induction_positions(enode* n) {
         n->unset_mark2();
     return result;
 }
-
-void induction_lemmas::abstract1(enode* n, enode* t, expr* x, abstractions& result) {
-    expr_safe_replace rep(m);
-    rep.insert(t->get_owner(), x);
-    expr_ref e(n->get_owner(), m);
-    rep(e);
-    result.push_back(abstraction(e));
-}
-
-/**
- * abstraction candidates for replacing different occurrence of t in n by x
- * it returns all possible non-empty subsets of t replaced by x.
- * 
- * TBD: add term sharing throttle.
- * TDD: add depth throttle.
- */
-void induction_lemmas::abstract(enode* n, enode* t, expr* x, abstractions& result) {
-    std::cout << "abs: " << result.size() << ": " << mk_pp(n->get_owner(), m) << "\n";
-    if (n->get_root() == t->get_root()) {
-        result.push_back(abstraction(m, x, n->get_owner(), t->get_owner()));
-        return;
-    }
-    func_decl* f = n->get_owner()->get_decl();
-    // check if n is a s
-    if (f->is_skolem()) {
-        expr_ref e(n->get_owner(), m);
-        result.push_back(abstraction(e));
-    }
-        
-    abstraction_args r1, r2;
-    r1.push_back(abstraction_arg(m));
-    for (enode* arg : enode::args(n)) {
-        unsigned n = result.size();
-        abstract(arg, t, x, result);
-        std::cout << result.size() << "\n";
-        for (unsigned i = n; i < result.size(); ++i) {
-            abstraction& a = result[i];
-            for (auto const& v : r1) {
-                r2.push_back(v);
-                r2.back().push_back(a);
-            }
-        }
-        r1.swap(r2);
-        r2.reset();
-        result.shrink(n);
-    }
-    for (auto const& a : r1) {
-        result.push_back(abstraction(m, m.mk_app(n->get_decl(), a.m_terms), a.m_eqs));
-    }
-};
 
-/**
- * filter generalizations based on value_generator
- * If all evaluations are counter-examples, include 
- * candidate generalization.
- */
-void induction_lemmas::filter_abstractions(bool sign, abstractions& abs) {
-    vector<expr_ref_vector> values;
-    expr_ref_vector fmls(m);
-    for (auto & a : abs) fmls.push_back(a.m_term);
-    std::cout << "sweep\n";
-    vs(fmls, values);
-    std::cout << "done sweep\n";
-    unsigned j = 0;
-    for (unsigned i = 0; i < fmls.size(); ++i) {
-        bool all_cex = true;
-        for (auto const& vec : values) {
-            if (vec[i] && (m.is_true(vec[i]) == sign))
-                continue;
-            all_cex = false;
-            break;
-        }
-        if (all_cex) {
-            abs[j++] = abs.get(i);
-        }
-    }
-    std::cout << "resulting size: " << j << " down from " << abs.size() << "\n";
-    abs.shrink(j);
-}
-
 /**
    extract substitutions for x into accessor values of the same sort.
    collect side-conditions for the accessors to be well defined.
@@ -308,35 +229,21 @@ void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y
  */
 
 void induction_lemmas::mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha) {
-    expr* alpha_e = ctx.bool_var2expr(alpha.var());
-    expr_ref beta(alpha_e, m);  
+    expr_ref beta(m);
+    ctx.literal2expr(alpha, beta);
     expr_safe_replace rep(m);
     for (auto const& p : subst) {
         rep.insert(p.first, p.second);
     }
     rep(beta);                          // set beta := alpha[sk/acc(acc2(sk))]
-    literal b_lit = mk_literal(beta);
-    if (alpha.sign()) b_lit.neg();
+    // alpha & is-c(sk) => ~alpha[sk/acc(sk)]
     literal_vector lits;
     lits.push_back(~alpha);
     for (expr* c : conds) lits.push_back(~mk_literal(c));
-    lits.push_back(b_lit);
+    lits.push_back(~mk_literal(beta));
     add_th_lemma(lits);
 }
 
-void induction_lemmas::create_hypotheses(unsigned depth, expr* sk, literal alpha) {
-    expr_ref_vector conds(m);
-    cond_substs_t subst;
-    expr* alpha_e = ctx.bool_var2expr(alpha.var());
-    mk_hypothesis_substs(depth, sk, subst);
-    for (auto& p : subst) {
-        expr_pair_vector vec;
-        vec.push_back(std::make_pair(sk, p.second));
-        mk_hypothesis_lemma(p.first, vec, alpha);
-    }
-}
-
-#if 0
 void induction_lemmas::create_hypotheses(unsigned depth, expr_ref_vector const& sks, literal alpha) {
     if (sks.empty())
         return;
@@ -350,55 +257,33 @@ void induction_lemmas::create_hypotheses(unsigned depth, expr_ref_vector const&
         // append the identity substitution:
         expr_ref_vector conds(m);
         subst.push_back(std::make_pair(conds, expr_ref(sk, m)));
-        
         substs.push_back(std::make_pair(sk, subst));
     }
 
     // create cross-product of instantiations:
     vector<std::pair<expr_ref_vector, expr_pair_vector>> s1, s2;
-    si.push_back(std::make_pair(expr_ref_vector(m), expr_pair_vector()));
+    s1.push_back(std::make_pair(expr_ref_vector(m), expr_pair_vector()));
     for (auto const& x2cond_sub : substs) {
+        s2.reset();
         for (auto const& cond_sub : x2cond_sub.second) {
-            s2.reset();
             for (auto const& cond_subs : s1) {
                 expr_pair_vector pairs(cond_subs.second);
                 expr_ref_vector conds(cond_subs.first);
-                pairs.push_back(x2cond_sub.first, cond_sub.second);
+                pairs.push_back(std::make_pair(x2cond_sub.first, cond_sub.second));
                 conds.append(cond_sub.first);
                 s2.push_back(std::make_pair(conds, pairs));
             }
-            s1.swap(s2);
         }
+        s1.swap(s2);
     }    
-    s1.pop_back(); // last substitution is the identity.
+    s1.pop_back(); // last substitution is the identity
 
     // extract lemmas from instantiations
     for (auto& p : s1) {
-        mk_hypothesis_lemam(p.first, p.second, alpha);
+        mk_hypothesis_lemma(p.first, p.second, alpha);
     }
 }
-#endif
 
-void induction_lemmas::create_lemmas(expr* sk, abstraction& a, literal lit) {
-    std::cout << "abstraction: " << a.m_term << "\n";
-    sort* s = m.get_sort(sk);
-    if (!m_dt.is_datatype(s))
-        return;
-    expr_ref alpha = a.m_term;
-    literal alpha_lit = mk_literal(alpha);
-    if (lit.sign()) alpha_lit.neg();
-
-    create_hypotheses(1, sk, alpha_lit);
-
-    literal_vector lits;
-    // phi & eqs => alpha
-    lits.push_back(~lit);
-    for (auto const& p : a.m_eqs) {
-        lits.push_back(~mk_literal(m.mk_eq(p.first, p.second)));
-    }
-    lits.push_back(alpha_lit);
-    add_th_lemma(lits);    
-}
 
 void induction_lemmas::add_th_lemma(literal_vector const& lits) {
     IF_VERBOSE(0, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n");
@@ -420,21 +305,35 @@ literal induction_lemmas::mk_literal(expr* e) {
 bool induction_lemmas::operator()(literal lit) {
     unsigned num = m_num_lemmas;
     enode* r = ctx.bool_var2enode(lit.var());
-    unsigned position = 0;
+    expr_ref_vector sks(m);
+    expr_safe_replace rep(m);
+
+    // have to be non-overlapping:
     for (enode* n : induction_positions(r)) {
         expr* t = n->get_owner();
-        sort* s = m.get_sort(t);
-        expr_ref sk(m.mk_fresh_const("sk", s), m);
-        std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n";
-        abstractions abs;
-        abstract1(r, n, sk, abs);            
-        if (abs.size() > 1) filter_abstractions(lit.sign(), abs);
-        for (abstraction& a : abs) {
-            create_lemmas(sk, a, lit);
+        if (is_uninterp_const(t)) { // for now, to avoid overlapping terms
+            sort* s = m.get_sort(t);
+            expr_ref sk(m.mk_fresh_const("sk", s), m);
+            sks.push_back(sk);
+            rep.insert(t, sk);
         }
-        ++position;
     }
-    return m_num_lemmas > num;
+    expr_ref alpha(m);
+    ctx.literal2expr(lit, alpha);
+    rep(alpha);
+    literal alpha_lit = mk_literal(alpha);
+
+    // alpha is the minimal instance of induction_positions where lit holds
+    // alpha & is-c(sk) => ~alpha[sk/acc(sk)]
+    create_hypotheses(1, sks, alpha_lit);
+    if (m_num_lemmas == num)
+        return false;
+    // lit => alpha
+    literal_vector lits;
+    lits.push_back(~lit);
+    lits.push_back(alpha_lit);
+    add_th_lemma(lits);        
+    return true;
 }
 
 induction_lemmas::induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs):

src/smt/smt_induction.h

@@ -58,30 +58,6 @@ namespace smt {
         unsigned       m_num_lemmas;
 
         typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
-
-        struct abstraction {
-            expr_ref         m_term;
-            expr_pair_vector m_eqs;
-            abstraction(expr_ref& e): m_term(e) {}
-            abstraction(ast_manager& m, expr* e, expr* n1, expr* n2): m_term(e, m) {
-                if (n1 != n2) m_eqs.push_back(std::make_pair(n1, n2));
-            }
-            abstraction(ast_manager& m, expr* e, expr_pair_vector const& eqs): 
-                m_term(e, m), m_eqs(eqs) {
-            }            
-        };
-        typedef vector<abstraction> abstractions;
-        
-        struct abstraction_arg {
-            expr_ref_vector   m_terms;
-            expr_pair_vector m_eqs;
-            abstraction_arg(ast_manager& m): m_terms(m) {}
-            void push_back(abstraction& a) {
-                m_terms.push_back(a.m_term);
-                m_eqs.append(a.m_eqs);
-            }
-        };
-        typedef vector<abstraction_arg> abstraction_args;
         typedef std::pair<expr_ref_vector, expr_ref> cond_subst_t;
         typedef vector<cond_subst_t> cond_substs_t;
 
@@ -90,14 +66,10 @@ namespace smt {
         bool viable_induction_children(enode* n);
         bool viable_induction_term(enode* p , enode* n);
         enode_vector induction_positions(enode* n);
-        void abstract(enode* n, enode* t, expr* x, abstractions& result);
-        void abstract1(enode* n, enode* t, expr* x, abstractions& result);
-        void filter_abstractions(bool sign, abstractions& abs);
-        void create_lemmas(expr* sk, abstraction& a, literal lit);
         void mk_hypothesis_substs(unsigned depth, expr* x, cond_substs_t& subst);
         void mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst);
         void mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha);
-        void create_hypotheses(unsigned depth, expr* sk, literal alpha);
+        void create_hypotheses(unsigned depth, expr_ref_vector const& sks, literal alpha);
         literal mk_literal(expr* e);
         void add_th_lemma(literal_vector const& lits);