avoid repeated internalization of lambda Z3Prover#4169

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

Author: NikolajBjorner

src/smt/params/smt_params.cpp

@@ -26,6 +26,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_random_seed = p.random_seed();
     m_relevancy_lvl = p.relevancy();
     m_ematching   = p.ematching();
+    m_induction   = p.induction();
     m_clause_proof = p.clause_proof();
     m_phase_selection = static_cast<phase_selection>(p.phase_selection());
     if (m_phase_selection > PS_THEORY) throw default_exception("illegal phase selection numeral");
@@ -111,6 +112,7 @@ void smt_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_display_features);
     DISPLAY_PARAM(m_new_core2th_eq);
     DISPLAY_PARAM(m_ematching);
+    DISPLAY_PARAM(m_induction);
     DISPLAY_PARAM(m_clause_proof);
 
     DISPLAY_PARAM(m_case_split_strategy);

src/smt/params/smt_params.h

@@ -110,6 +110,7 @@ struct smt_params : public preprocessor_params,
     bool             m_display_features;
     bool             m_new_core2th_eq;
     bool             m_ematching;
+    bool             m_induction;
     bool             m_clause_proof;
 
     // -----------------------------------
@@ -262,6 +263,7 @@ struct smt_params : public preprocessor_params,
         m_display_features(false),
         m_new_core2th_eq(true),
         m_ematching(true),
+        m_induction(false),
         m_clause_proof(false),
         m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
         m_rel_case_split_order(0),

src/smt/params/smt_params_helper.pyg

@@ -37,6 +37,7 @@ def_module_params(module_name='smt',
                           ('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
                           ('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
                           ('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
+                          ('induction', BOOL, False, 'enable generation of induction lemmas'),
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),

src/smt/smt_induction.cpp

@@ -55,6 +55,8 @@ literal_vector collect_induction_literals::pre_select() {
             continue;
         result.push_back(lit);
     }
+    TRACE("induction", ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n"););
+
     ctx.push_trail(value_trail<context, unsigned>(m_literal_index));
     m_literal_index = ctx.assigned_literals().size();
     return result;
@@ -68,11 +70,6 @@ void collect_induction_literals::model_sweep_filter(literal_vector& candidates)
     vector<expr_ref_vector> values;
     vs(terms, values);
     unsigned j = 0;
-    IF_VERBOSE(1, 
-               verbose_stream() << "terms: " << terms << "\n";
-               for (auto const& vec : values) {
-                   verbose_stream() << "assignment: " << vec << "\n";
-               });
     for (unsigned i = 0; i < terms.size(); ++i) {
         literal lit = candidates[i];
         bool is_viable_candidate = true;
@@ -109,14 +106,26 @@ literal_vector collect_induction_literals::operator()() {
 // create_induction_lemmas
 
 bool create_induction_lemmas::is_induction_candidate(enode* n) {
-    expr* e = n->get_owner();
+    app* e = n->get_owner();
     if (m.is_value(e))
         return false;
-    // TBD: filter if n is equivalent to a value.
+    bool in_good_context = false;
+    for (enode* p : n->get_parents()) {
+        app* o = p->get_owner();
+        if (o->get_family_id() != m.get_basic_family_id())
+            in_good_context = true;
+    }
+    if (!in_good_context)
+        return false;
+
+    // avoid recursively unfolding skolem terms.
+    if (e->get_num_args() > 0 && e->get_family_id() == null_family_id) {
+        return false;
+    }
     sort* s = m.get_sort(e);
     if (m_dt.is_datatype(s) && m_dt.is_recursive(s))
         return true;
-
+    
     // potentially also induction on integers, sequences
     // m_arith.is_int(s)
     //  return true;
@@ -160,14 +169,24 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) {
  * TDD: add depth throttle.
  */
 void create_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()));
     }
+#if 0
+    // check if n is a s
+    if (is_skolem(n->get_owner())) {
+        result.push_back(abstraction(m, n->get_owner()));
+        return;
+    }
+#endif
+        
     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) {
@@ -193,7 +212,9 @@ void create_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;
@@ -207,15 +228,17 @@ void create_induction_lemmas::filter_abstractions(bool sign, abstractions& abs)
             abs[j++] = abs.get(i);
         }
     }
+    std::cout << "resulting size: " << j << " down from " << abs.size() << "\n";
     abs.shrink(j);
 }
 
 /*
  * Create simple induction lemmas of the form:
  *
- * lit & a.eqs() & is-c(t) => is-c(sk);
  * lit & a.eqs() => alpha
- * lit & a.eqs() & is-c(t) => ~beta
+ * alpha & is-c(sk) => ~beta
+ * 
+ * alpha & is-c(t) => is-c(sk);
  *
  * where 
  *       lit   = is a formula containing t
@@ -242,50 +265,59 @@ void create_induction_lemmas::create_lemmas(expr* t, expr* sk, abstraction& a, l
         return;
     expr_ref alpha = a.m_term;
     auto const& eqs = a.m_eqs;
+    literal alpha_lit = null_literal;
     literal_vector common_literals; 
     for (func_decl* c : *m_dt.get_datatype_constructors(s)) {
         func_decl* is_c = m_dt.get_constructor_recognizer(c);
         bool has_1recursive = false;
         for (func_decl* acc : *m_dt.get_constructor_accessors(c)) {
             if (acc->get_range() != s)
                 continue;
-            if (common_literals.empty()) {
-                common_literals.push_back(~lit);
-                for (auto const& p : eqs) {
-                    common_literals.push_back(~mk_literal(m.mk_eq(p.first, p.second)));
-                }
+            if (alpha_lit == null_literal) {
+                alpha_lit = mk_literal(alpha);
+                if (lit.sign()) alpha_lit.neg();
             }
             has_1recursive = true;
-            literal_vector lits(common_literals);
-            lits.push_back(~mk_literal(m.mk_app(is_c, t))); 
             expr_ref beta(alpha);
             expr_safe_replace rep(m);
             rep.insert(sk, m.mk_app(acc, sk));
             rep(beta);
             literal b_lit = mk_literal(beta);
             if (lit.sign()) b_lit.neg();
+
+            // alpha & is_c(sk) => ~beta
+            literal_vector lits;
+            lits.push_back(~alpha_lit);
+            lits.push_back(~mk_literal(m.mk_app(is_c, sk))); 
             lits.push_back(~b_lit);
             add_th_lemma(lits);               
         }
+
+        // alpha & is_c(t) => is_c(sk)
         if (has_1recursive) {
-            literal_vector lits(common_literals);
+            literal_vector lits;
+            lits.push_back(~alpha_lit);
             lits.push_back(~mk_literal(m.mk_app(is_c, t)));
             lits.push_back(mk_literal(m.mk_app(is_c, sk)));
             add_th_lemma(lits);
         }
     }
-    if (!common_literals.empty()) {
-        literal_vector lits(common_literals);
-        literal a_lit = mk_literal(alpha);
-        if (lit.sign()) a_lit.neg();
-        lits.push_back(a_lit);
+
+    // phi & eqs => alpha
+    if (alpha_lit != null_literal) {
+        literal_vector lits;
+        lits.push_back(~lit);
+        for (auto const& p : eqs) {
+            lits.push_back(~mk_literal(m.mk_eq(p.first, p.second)));
+        }
+        lits.push_back(alpha_lit);
         add_th_lemma(lits);
     }
 }
 
 void create_induction_lemmas::add_th_lemma(literal_vector const& lits) {
     IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream() << "lemma:\n", lits) << "\n");
-    ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_LEMMA);
+    ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, smt::CLS_TH_AXIOM); // CLS_TH_LEMMA, but then should re-instance if GC'ed
     ++m_num_lemmas;
 }
 
@@ -301,8 +333,8 @@ literal create_induction_lemmas::mk_literal(expr* e) {
 func_decl* create_induction_lemmas::mk_skolem(sort* s) {
     func_decl* f = nullptr;
     if (!m_sort2skolem.find(s, f)) {
-        sort* domain[2] = { s, m.mk_bool_sort() };
-        f = m.mk_fresh_func_decl("sk", 2, domain, s);
+        sort* domain[3] = { m_a.mk_int(), s, m.mk_bool_sort() };
+        f = m.mk_fresh_func_decl("sk", 3, domain, s);
         m_pinned.push_back(f);
         m_pinned.push_back(s);
         m_sort2skolem.insert(s, f);
@@ -314,10 +346,11 @@ func_decl* create_induction_lemmas::mk_skolem(sort* s) {
 bool create_induction_lemmas::operator()(literal lit) {
     unsigned num = m_num_lemmas;
     enode* r = ctx.bool_var2enode(lit.var());
+    unsigned position = 0;
     for (enode* n : induction_positions(r)) {
         expr* t = n->get_owner();
         sort* s = m.get_sort(t);
-        expr_ref sk(m.mk_app(mk_skolem(s), t, r->get_owner()), m);
+        expr_ref sk(m.mk_app(mk_skolem(s), m_a.mk_int(position), t, r->get_owner()), m);
         std::cout << "abstract " << mk_pp(t, m) << " " << sk << "\n";
         abstractions abs;
         abstract(r, n, sk, abs);            
@@ -326,6 +359,8 @@ bool create_induction_lemmas::operator()(literal lit) {
         for (abstraction& a : abs) {
             create_lemmas(t, sk, a, lit);
         }
+        std::cout << "lemmas created\n";
+        ++position;
     }
     return m_num_lemmas > num;
 }
@@ -335,6 +370,7 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v
     m(m),
     vs(vs),
     m_dt(m),
+    m_a(m),
     m_pinned(m),
     m_num_lemmas(0)
 {}

src/smt/smt_induction.h

@@ -20,6 +20,7 @@
 #include "smt/smt_types.h"
 #include "ast/rewriter/value_sweep.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
 
 namespace smt {
 
@@ -52,6 +53,7 @@ namespace smt {
         ast_manager& m;
         value_sweep& vs;
         datatype::util m_dt;
+        arith_util     m_a;
         obj_map<sort, func_decl*> m_sort2skolem;
         ast_ref_vector m_pinned;
         unsigned m_num_lemmas;

src/smt/smt_internalizer.cpp

@@ -558,6 +558,9 @@ namespace smt {
     void context::internalize_lambda(quantifier * q) {
         TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";);
         SASSERT(is_lambda(q));
+        if (e_internalized(q)) {
+            return;
+        }
         app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m);
         app_ref eq(m), lam_app(m);
         expr_ref_vector vars(m);

src/smt/theory_recfun.cpp

@@ -21,7 +21,6 @@ Revision History:
 #include "ast/ast_util.h"
 #include "ast/for_each_expr.h"
 #include "smt/theory_recfun.h"
-#include "smt/params/smt_params_helper.hpp"
 
 
 #define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
@@ -357,6 +356,7 @@ namespace smt {
         literal_vector preds;
         auto & vars = e.m_def->get_vars();
 
+        unsigned max_depth = 0;
         for (recfun::case_def const & c : e.m_def->get_cases()) {
             // applied predicate to `args`
             app_ref pred_applied = c.apply_case_predicate(e.m_args);
@@ -376,15 +376,25 @@ namespace smt {
             }
             else if (!is_enabled_guard(pred_applied)) {
                 disable_guard(pred_applied, guards);
+                max_depth = std::max(depth, max_depth);
                 continue;
             }
             activate_guard(pred_applied, guards);
         }
         // the disjunction of branches is asserted
         // to close the available cases. 
-        std::function<literal_vector(void)> fn2 = [&]() { return preds; };
-        scoped_trace_stream _tr2(*this, fn2);
-        ctx().mk_th_axiom(get_id(), preds);
+        {
+            scoped_trace_stream _tr2(*this, preds);
+            ctx().mk_th_axiom(get_id(), preds);
+        }
+        (void)max_depth;
+        // add_induction_lemmas(max_depth);
+    }
+
+    void theory_recfun::add_induction_lemmas(unsigned depth) {
+        if (depth > 4 && ctx().get_fparams().m_induction && induction::should_try(ctx())) {
+            ctx().get_induction()();
+        }
     }
 
     void theory_recfun::activate_guard(expr* pred_applied, expr_ref_vector const& guards) {

src/smt/theory_recfun.h

@@ -127,6 +127,7 @@ namespace smt {
         void assert_body_axiom(body_expansion & e);
         literal mk_literal(expr* e);
 
+        void add_induction_lemmas(unsigned depth);
         void disable_guard(expr* guard, expr_ref_vector const& guards);
         unsigned get_depth(expr* e);
         void set_depth(unsigned d, expr* e);