add a way to supress lambdas

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

src/sat/sat_drat.cpp

@@ -214,7 +214,10 @@ namespace sat {
             return;
         
         if (m_check_unsat) 
-            assign_propagate(l);        
+            assign_propagate(l);
+
+        if (m_trim)
+            append(mk_clause(1, &l, st.is_redundant()), st);
 
         m_units.push_back(l);
     }
@@ -307,11 +310,15 @@ namespace sat {
                 }
             }
         }
+
+        if (!m_check_unsat)
+            return;
+
         switch (num_watch) {
         case 0:
             m_inconsistent = true;
             break;
-        case 1:
+        case 1:            
             assign_propagate(l1);
             break;
         default: {
@@ -553,12 +560,10 @@ namespace sat {
         for (unsigned i = m_proof.size(); i-- > 0; ) {
             auto const & [c, st] = m_proof[i];
             if (match(n, lits, c)) {
-                if (st.is_deleted()) {
+                if (st.is_deleted()) 
                     num_del++;
-                }
+                else 
-                else {
                     num_add++;
-                }
             }
         }
         return num_add > num_del;
@@ -596,8 +601,8 @@ namespace sat {
                 continue;
             unsigned num_true = 0;
             unsigned num_undef = 0;
-            for (unsigned j = 0; j < c.size(); ++j) {
+            for (literal lit : c) {
-                switch (value(c[j])) {
+                switch (value(lit)) {
                 case l_true: num_true++; break;
                 case l_undef: num_undef++; break;
                 default: break;
@@ -651,6 +656,8 @@ namespace sat {
     }
 
     void drat::assign_propagate(literal l) {
+        if (!m_check_unsat)
+            return;
         unsigned num_units = m_units.size();
         assign(l);
         for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) 

src/sat/sat_solver.cpp

@@ -600,9 +600,8 @@ namespace sat {
         else {
             m_clauses.push_back(r);
         }
-        if (m_config.m_drat) {
+        if (m_config.m_drat) 
             m_drat.add(*r, st);
-        }
         for (literal l : *r) {
             m_touched[l.var()] = m_touch_index;
         }

src/smt/qi_queue.cpp

@@ -232,6 +232,7 @@ namespace smt {
         expr_ref  s_instance(m);
         proof_ref pr(m);
         m_context.get_rewriter()(instance, s_instance, pr);
+
         TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << s_instance << "\n";);
         if (m.is_true(s_instance)) {
             TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m););

src/smt/smt_context.cpp

@@ -3743,7 +3743,7 @@ namespace smt {
         if (status == l_false) {
             return false;
         }
-        if (status == l_true && !m_qmanager->has_quantifiers() && !m_has_lambda) {
+        if (status == l_true && !m_qmanager->has_quantifiers() && m_lambdas.empty()) {
             return false;
         }
         if (status == l_true && m_qmanager->has_quantifiers()) {
@@ -3766,7 +3766,7 @@ namespace smt {
                 break;
             }
         }
-        if (status == l_true && m_has_lambda) {
+        if (status == l_true && !m_lambdas.empty()) {
             m_last_search_failure = LAMBDAS;
             status = l_undef;
             return false;
@@ -4010,7 +4010,7 @@ namespace smt {
         TRACE("final_check_step", tout << "RESULT final_check: " << result << "\n";);
         if (result == FC_GIVEUP && f != OK)
             m_last_search_failure = f;
-        if (result == FC_DONE && m_has_lambda) {
+        if (result == FC_DONE && !m_lambdas.empty()) {
             m_last_search_failure = LAMBDAS;
             result = FC_GIVEUP;
         }

src/smt/smt_context.h

@@ -773,7 +773,7 @@ namespace smt {
 
         void internalize_quantifier(quantifier * q, bool gate_ctx);
 
-        bool m_has_lambda = false;
+        obj_hashtable<quantifier> m_lambdas, m_non_lambdas;
         void internalize_lambda(quantifier * q);
 
         void internalize_formula_core(app * n, bool gate_ctx);
@@ -783,6 +783,9 @@ namespace smt {
         friend class set_enode_flag_trail;
 
     public:
+
+        void add_non_lambda(quantifier* q);
+        
         void set_enode_flag(bool_var v, bool is_new_var);
 
     protected:

src/smt/smt_internalizer.cpp

@@ -606,8 +606,21 @@ namespace smt {
         bool_var bv = get_bool_var(fa);
         assign(literal(bv, false), nullptr);
         mark_as_relevant(bv);
-        push_trail(value_trail<bool>(m_has_lambda));
+        if (m_non_lambdas.contains(q))
-        m_has_lambda = true;
+            return;
+        push_trail(insert_obj_trail<quantifier>(m_lambdas, q));
+        m_lambdas.insert(q);
+    }
+
+    void context::add_non_lambda(quantifier* q) {
+        if (m_non_lambdas.contains(q))
+            return;
+        m_non_lambdas.insert(q);
+        push_trail(insert_obj_trail<quantifier>(m_lambdas, q));
+        if (m_lambdas.contains(q)) {
+            m_lambdas.remove(q);
+            push_trail(remove_obj_trail<quantifier>(m_lambdas, q));
+        }
     }
 
     /**

src/smt/theory_seq.cpp

@@ -1455,7 +1455,9 @@ bool theory_seq::internalize_term(app* term) {
     if (ctx.e_internalized(term)) {
         mk_var(ctx.get_enode(term));
         return true;
-    }    
+    }
+
+    suppress_lambda(term);
 
     if (m.is_bool(term) && 
         (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) {
@@ -1490,6 +1492,23 @@ bool theory_seq::internalize_term(app* term) {
     return true;
 }
 
+void theory_seq::suppress_lambda(app* term) {
+    if (!m_util.str.is_map(term) && !m_util.str.is_mapi(term) &&
+        !m_util.str.is_foldl(term) && !m_util.str.is_foldli(term))
+        return;
+    
+    expr* fn = to_app(term)->get_arg(0);
+    quantifier* q = nullptr;
+    if (is_lambda(fn)) 
+        q = to_quantifier(fn);
+    else if (is_app(fn))
+        q = m.is_lambda_def(to_app(fn)->get_decl());
+
+    if (q) 
+        ctx.add_non_lambda(q);
+}
+
+
 void theory_seq::add_length(expr* l) {
     expr* e = nullptr;
     VERIFY(m_util.str.is_length(l, e));

src/smt/theory_seq.h

@@ -388,6 +388,7 @@ namespace smt {
         bool internalize_atom(app* atom, bool) override;
         bool internalize_term(app*) override;
         void internalize_eq_eh(app * atom, bool_var v) override;
+        void suppress_lambda(app* term);
         void new_eq_eh(theory_var, theory_var) override;
         void new_diseq_eh(theory_var, theory_var) override;
         void assign_eh(bool_var v, bool is_true) override;