flag incomplete on lambdas #5803

src/smt/smt_context.cpp

@@ -3731,7 +3731,7 @@ namespace smt {
         if (status == l_false) {
             return false;
         }
-        if (status == l_true && !m_qmanager->has_quantifiers()) {
+        if (status == l_true && !m_qmanager->has_quantifiers() && !m_has_lambda) {
             return false;
         }
         if (status == l_true && m_qmanager->has_quantifiers()) {
@@ -3754,6 +3754,11 @@ namespace smt {
                 break;
             }
         }
+        if (status == l_true && m_has_lambda) {
+            m_last_search_failure = LAMBDAS;
+            status = l_undef;
+            return false;
+        }
         inc_limits();
         if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
             SASSERT(!inconsistent());
@@ -3765,13 +3770,13 @@ namespace smt {
                 pop_scope(m_scope_lvl - curr_lvl);
                 SASSERT(at_search_level());
             }
-            for (theory* th : m_theory_set) {
+            for (theory* th : m_theory_set) 
-                if (!inconsistent()) th->restart_eh();
+                if (!inconsistent()) 
-            }
+                    th->restart_eh();
+
             TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
-            if (!inconsistent()) {
+            if (!inconsistent()) 
                 m_qmanager->restart_eh();
-            }
             if (inconsistent()) {
                 VERIFY(!resolve_conflict());
                 status = l_false;
@@ -3993,6 +3998,10 @@ 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) {
+            m_last_search_failure = LAMBDAS;
+            result = FC_GIVEUP;
+        }
         return result;
     }
 

src/smt/smt_context.h

@@ -773,6 +773,7 @@ namespace smt {
 
         void internalize_quantifier(quantifier * q, bool gate_ctx);
 
+        bool m_has_lambda = false;
         void internalize_lambda(quantifier * q);
 
         void internalize_formula_core(app * n, bool gate_ctx);

src/smt/smt_context_pp.cpp

@@ -56,6 +56,8 @@ namespace smt {
             return out;
         case QUANTIFIERS:
             return out << "QUANTIFIERS";
+        case LAMBDAS:
+            return out << "LAMBDAS";
         }
         UNREACHABLE();
         return out << "?";
@@ -79,6 +81,7 @@ namespace smt {
         }
         case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
+        case LAMBDAS: r = "(incomplete lambdas)"; break;
         case UNKNOWN: r = m_unknown; break;
         }
         return r;

src/smt/smt_failure.h

@@ -31,6 +31,7 @@ namespace smt {
         NUM_CONFLICTS, //!< Maximum number of conflicts was reached
         THEORY,        //!< Theory is incomplete
         RESOURCE_LIMIT,
+        LAMBDAS,       //!< Logical context contains lambdas.
         QUANTIFIERS    //!< Logical context contains universal quantifiers.
     };
 

src/smt/smt_internalizer.cpp

@@ -605,6 +605,8 @@ 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));
+        m_has_lambda = true;
     }
 
     /**

src/smt/theory_array_full.cpp

@@ -763,7 +763,6 @@ namespace smt {
             app_ref sel1(m), sel2(m);
             sel1 = mk_select(args1);
             sel2 = mk_select(args2);
-            std::cout << "small domain " << sel1 << " " << sel2 << "\n";
             is_new = try_assign_eq(sel1, sel2);
 #endif
         }