disable term enumeration by default

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

src/ast/pattern/pattern_inference.cpp

@@ -540,7 +540,7 @@ bool pattern_inference_cfg::is_forbidden(app * n) const {
     // Remark: skolem constants should not be used in patterns, since they do not
     // occur outside of the quantifier. That is, Z3 will never match this kind of
     // pattern.
-    if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
+    if (false && m_params.m_pi_avoid_skolems && decl->is_skolem()) {
         CTRACE(pattern_inference_skolem, decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }

src/params/smt_params_helper.pyg

@@ -12,7 +12,7 @@ def_module_params(module_name='smt',
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
                           ('ho_matching', BOOL, False, 'higher-order matching for quantifier instantiation'),
                           ('ho_matching_bound', UINT, 10000, 'per-problem expansion-step budget of the higher-order matching search; bounds the (undecidable) HO unification to guarantee termination'),
-                          ('term_enumeration', BOOL, True, 'use term enumeration to populate instantiation sets for higher-order variables during model-based quantifier instantiation'),
+                          ('term_enumeration', BOOL, False, 'use term enumeration to populate instantiation sets for higher-order variables during model-based quantifier instantiation'),
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'),
 	                  ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'),
 	                  ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'),

src/smt/seq_regex.cpp

@@ -872,7 +872,9 @@ namespace smt {
             lits.push_back(~lit);
             if (!m.is_true(cond)) {
                 expr_ref ncond(mk_not(m, cond), m);
-                lits.push_back(th.mk_literal(mk_forall(m, hd, ncond)));
+                expr_ref facond = mk_forall(m, hd, ncond);
+                ctx.internalize(facond, true); // make sure fa is internalized, and assumed in positive polarity only.
+                lits.push_back(th.mk_literal(facond));
             }
             expr_ref is_empty1 = sk().mk_is_empty(r, re().mk_union(u, r), n);    
             lits.push_back(th.mk_literal(is_empty1)); 

src/smt/smt_context.h

@@ -983,6 +983,8 @@ namespace smt {
 
         void internalize(expr * n, bool gate_ctx, unsigned generation);
 
+        enode *non_ground_internalize(expr *e);
+
         clause * mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k = CLS_AUX, clause_del_eh * del_eh = nullptr);
 
         void mk_clause(literal l1, literal l2, justification * j);

src/smt/smt_internalizer.cpp

@@ -419,6 +419,28 @@ namespace smt {
         internalize_rec(n, gate_ctx);
     }
 
+    enode *context::non_ground_internalize(expr *e) {
+        if (e_internalized(e))
+            return get_enode(e);
+        if (is_ground(e)) {
+            internalize(e, false);
+            return get_enode(e);
+        }
+        for (auto arg : subterms::ground(expr_ref(e, m))) {
+            if ((is_forall(arg) || is_exists(arg)) && !e_internalized(arg)) {
+                expr_ref fn(m.mk_fresh_const("proxy-expr", e->get_sort()), m);
+                expr_ref eq(m.mk_eq(fn, e), m);
+                assert_expr(eq);
+                internalize_assertions();
+                if (!e_internalized(fn)) 
+                    internalize(fn, false);
+                return get_enode(fn);
+            }
+        }
+        internalize(e, false);
+        return get_enode(e);
+    }
+
     void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
         internalize_deep(exprs, num_exprs);
         for (unsigned i = 0; i < num_exprs; ++i) 

src/smt/smt_theory.cpp

@@ -152,7 +152,8 @@ namespace smt {
         expr_ref e(_e, m);
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
-            ctx.internalize(_e, is_quantifier(_e));
+            auto n = ctx.non_ground_internalize(_e);
+            _e = n->get_expr();            
         }
         literal lit = ctx.get_literal(_e);
         ctx.mark_as_relevant(lit);

src/smt/theory_array_full.cpp

@@ -626,17 +626,8 @@ namespace smt {
         for (unsigned i = 0; i < lam->get_num_decls(); ++i) 
             args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
         expr_ref val(mk_select(args), m);
-        ctx.get_rewriter()(val);
+        auto val_e = ctx.non_ground_internalize(val);
-        if (has_quantifiers(val)) {
+        return try_assign_eq(val_e->get_expr(), def);
-            expr_ref fn(m.mk_fresh_const("lambda-body", val->get_sort()), m);
-            expr_ref eq(m.mk_eq(fn, val), m);
-            ctx.assert_expr(eq);
-            ctx.internalize_assertions();
-            val = fn;
-        }
-        ctx.internalize(def, false);
-        ctx.internalize(val.get(), false);
-        return try_assign_eq(val.get(), def);
     }
 
     bool theory_array_full::instantiate_choice_axiom(enode* ch) {