Add identifiers for sources of incompleteness (#6311)

This PR classifies all internal kinds of incompleteness as identifiers.

It makes it so TheoryEngine records an identifier when its incomplete flag is set.

The next step will be to possibly communicate this value to the user.

34 files changed, 216 insertions, 50 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4db7b202e..918c5a45a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -632,6 +632,8 @@ libcvc4_add_sources(
   theory/fp/theory_fp_type_rules.cpp
   theory/fp/type_enumerator.h
   theory/interrupted.h
+  theory/incomplete_id.cpp
+  theory/incomplete_id.h
   theory/inference_id.cpp
   theory/inference_id.h
   theory/inference_manager_buffered.cpp
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 03563006b..16142886f 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -489,7 +489,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS
         Trace("nl-ext") << "...failed to send lemma in "
                            "NonLinearExtension, set incomplete"
                         << std::endl;
-        d_containing.getOutputChannel().setIncomplete();
+        d_containing.getOutputChannel().setIncomplete(IncompleteId::ARITH_NL);
         return Result::Sat::SAT_UNKNOWN;
       }
     }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e68ff7d11..2c339cd0c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -206,7 +206,7 @@ void TheoryArith::postCheck(Effort level)
     else if (d_internal->foundNonlinear())
     {
       // set incomplete
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
     }
   }
 }
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 08fa0164b..709ecbfa1 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -139,10 +139,10 @@ void EngineOutputChannel::requirePhase(TNode n, bool phase)
   d_engine->getPropEngine()->requirePhase(n, phase);
 }
 
-void EngineOutputChannel::setIncomplete()
+void EngineOutputChannel::setIncomplete(IncompleteId id)
 {
-  Trace("theory") << "setIncomplete()" << std::endl;
-  d_engine->setIncomplete(d_theory);
+  Trace("theory") << "setIncomplete(" << id << ")" << std::endl;
+  d_engine->setIncomplete(d_theory, id);
 }
 
 void EngineOutputChannel::spendResource(ResourceManager::Resource r)
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 8b497547b..a9bae38a3 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -58,7 +58,7 @@ class EngineOutputChannel : public theory::OutputChannel
 
   void requirePhase(TNode n, bool phase) override;
 
-  void setIncomplete() override;
+  void setIncomplete(IncompleteId id) override;
 
   void spendResource(ResourceManager::Resource r) override;
 
diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
new file mode 100644
index 000000000..340e2c208
--- /dev/null
+++ b/src/theory/incomplete_id.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file incomplete_id.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of incompleteness enumeration.
+ **/
+
+#include "theory/incomplete_id.h"
+
+#include <iostream>
+
+namespace cvc5 {
+namespace theory {
+
+const char* toString(IncompleteId i)
+{
+  switch (i)
+  {
+    case IncompleteId::ARITH_NL_DISABLED: return "ARITH_NL_DISABLED";
+    case IncompleteId::ARITH_NL: return "ARITH_NL";
+    case IncompleteId::QUANTIFIERS: return "QUANTIFIERS";
+    case IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY:
+      return "QUANTIFIERS_SYGUS_NO_VERIFY";
+    case IncompleteId::QUANTIFIERS_CEGQI: return "QUANTIFIERS_CEGQI";
+    case IncompleteId::QUANTIFIERS_FMF: return "QUANTIFIERS_FMF";
+    case IncompleteId::QUANTIFIERS_RECORDED_INST:
+      return "QUANTIFIERS_RECORDED_INST";
+    case IncompleteId::SEP: return "SEP";
+    case IncompleteId::SETS_RELS_CARD: return "SETS_RELS_CARD";
+    case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
+    case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY:
+      return "STRINGS_REGEXP_NO_SIMPLIFY";
+    case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED";
+    case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED";
+    case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE";
+    case IncompleteId::UNKNOWN: return "UNKNOWN";
+    default: return "?IncompleteId?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, IncompleteId i)
+{
+  out << toString(i);
+  return out;
+}
+
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
new file mode 100644
index 000000000..67754b67d
--- /dev/null
+++ b/src/theory/incomplete_id.h
@@ -0,0 +1,83 @@
+/*********************                                                        */
+/*! \file incomplete_id.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Incompleteness enumeration.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__INCOMPLETE_ID_H
+#define CVC4__THEORY__INCOMPLETE_ID_H
+
+#include <iosfwd>
+
+namespace cvc5 {
+namespace theory {
+
+/**
+ * Reasons for incompleteness in CVC4.
+ */
+enum class IncompleteId
+{
+  // the non-linear arithmetic solver was disabled
+  ARITH_NL_DISABLED,
+  // the non-linear arithmetic solver was incomplete
+  ARITH_NL,
+  // incomplete due to lack of a complete quantifiers strategy
+  QUANTIFIERS,
+  // we failed to verify the correctness of a candidate solution in SyGuS
+  QUANTIFIERS_SYGUS_NO_VERIFY,
+  // incomplete due to counterexample-guided instantiation not being complete
+  QUANTIFIERS_CEGQI,
+  // incomplete due to finite model finding not being complete
+  QUANTIFIERS_FMF,
+  // incomplete due to explicitly recorded instantiations
+  QUANTIFIERS_RECORDED_INST,
+  // incomplete due to separation logic
+  SEP,
+  // relations were used in combination with set cardinality constraints
+  SETS_RELS_CARD,
+  // we skipped processing a looping word equation
+  STRINGS_LOOP_SKIP,
+  // we could not simplify a regular expression membership
+  STRINGS_REGEXP_NO_SIMPLIFY,
+  // HO extensionality axiom was disabled
+  UF_HO_EXT_DISABLED,
+  // UF+cardinality solver was disabled
+  UF_CARD_DISABLED,
+  // UF+cardinality solver used in an incomplete mode
+  UF_CARD_MODE,
+
+  //-------------------------------------- unknown
+  UNKNOWN
+};
+
+/**
+ * Converts an incompleteness id to a string.
+ *
+ * @param i The incompleteness identifier
+ * @return The name of the incompleteness identifier
+ */
+const char* toString(IncompleteId i);
+
+/**
+ * Writes an incompleteness identifier to a stream.
+ *
+ * @param out The stream to write to
+ * @param i The incompleteness identifier to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, IncompleteId i);
+
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC4__THEORY__INCOMPLETE_ID_H */
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 89957ded6..3e91bff44 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -14,11 +14,11 @@
 
 #include "cvc4_private.h"
 
-#include <iosfwd>
-
 #ifndef CVC4__THEORY__INFERENCE_ID_H
 #define CVC4__THEORY__INFERENCE_ID_H
 
+#include <iosfwd>
+
 namespace cvc5 {
 namespace theory {
 
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index b86a4d647..0a3fa3904 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -19,6 +19,7 @@
 #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
 #define CVC4__THEORY__OUTPUT_CHANNEL_H
 
+#include "theory/incomplete_id.h"
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
 
@@ -150,7 +151,7 @@ class OutputChannel {
    * this context level.  If SAT is later determined by the
    * TheoryEngine, it should actually return an UNKNOWN result.
    */
-  virtual void setIncomplete() = 0;
+  virtual void setIncomplete(IncompleteId id) = 0;
 
   /**
    * "Spend" a "resource."  The meaning is specific to the context in
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 74469e7de..5afea1e9b 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -296,9 +296,10 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
   }
 }
 
-bool InstStrategyCegqi::checkComplete()
+bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
 {
   if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+    incId = IncompleteId::QUANTIFIERS_CEGQI;
     return false;
   }else{
     return true;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 6d4ee047f..85724a915 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -85,7 +85,7 @@ class InstStrategyCegqi : public QuantifiersModule
   /** check */
   void check(Theory::Effort e, QEffort quant_e) override;
   /** check complete */
-  bool checkComplete() override;
+  bool checkComplete(IncompleteId& incId) override;
   /** check complete for quantified formula */
   bool checkCompleteFor(Node q) override;
   /** check ownership */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 1c46e425d..5fa139681 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -112,8 +112,14 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
   }
 }
 
-bool ModelEngine::checkComplete() {
-  return !d_incomplete_check;
+bool ModelEngine::checkComplete(IncompleteId& incId)
+{
+  if (d_incomplete_check)
+  {
+    incId = IncompleteId::QUANTIFIERS_FMF;
+    return false;
+  }
+  return true;
 }
 
 bool ModelEngine::checkCompleteFor( Node q ) {
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 2547f2831..5a983d726 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -55,7 +55,7 @@ public:
  QEffort needsModel(Theory::Effort e) override;
  void reset_round(Theory::Effort e) override;
  void check(Theory::Effort e, QEffort quant_e) override;
- bool checkComplete() override;
+ bool checkComplete(IncompleteId& incId) override;
  bool checkCompleteFor(Node q) override;
  void registerQuantifier(Node f) override;
  void assertNode(Node f) override;
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 62376bff6..8fc1c4d13 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -74,12 +74,13 @@ bool Instantiate::reset(Theory::Effort e)
 }
 
 void Instantiate::registerQuantifier(Node q) {}
-bool Instantiate::checkComplete()
+bool Instantiate::checkComplete(IncompleteId& incId)
 {
   if (!d_recordedInst.empty())
   {
     Trace("quant-engine-debug")
         << "Set incomplete due to recorded instantiations." << std::endl;
+    incId = IncompleteId::QUANTIFIERS_RECORDED_INST;
     return false;
   }
   return true;
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index b3c056506..b56938fd1 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -117,7 +117,7 @@ class Instantiate : public QuantifiersUtil
   /** identify */
   std::string identify() const override { return "Instantiate"; }
   /** check incomplete */
-  bool checkComplete() override;
+  bool checkComplete(IncompleteId& incId) override;
 
   //--------------------------------------rewrite objects
   /** add instantiation rewriter */
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index e6d5eee76..01a51ccff 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -104,8 +104,11 @@ class QuantifiersModule
    *
    * This is called just before the quantifiers engine will return
    * with no lemmas added during a LAST_CALL effort check.
+   *
+   * If this method returns false, it should update incId to the reason for
+   * why the module was incomplete.
    */
-  virtual bool checkComplete() { return true; }
+  virtual bool checkComplete(IncompleteId& incId) { return true; }
   /** Check was complete for quantified formula q
    *
    * If for each quantified formula q, some module returns true for
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 7cd89c7d8..90955226c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/incomplete_id.h"
 #include "theory/theory.h"
 
 namespace cvc5 {
@@ -49,9 +50,10 @@ public:
   /** Check complete?
    *
    * Returns false if the utility's reasoning was globally incomplete
-   * (e.g. "sat" must be replaced with "incomplete").
+   * (e.g. "sat" must be replaced with "incomplete"). If this method returns
+   * false, it should update incId to the reason for incompleteness.
    */
-  virtual bool checkComplete() { return true; }
+  virtual bool checkComplete(IncompleteId& incId) { return true; }
 };
 
 class QuantPhaseReq
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6db632b11..c9ef1205c 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -616,7 +616,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       // We should set incomplete, since a "sat" answer should not be
       // interpreted as "infeasible", which would make a difference in the rare
       // case where e.g. we had a finite grammar and exhausted the grammar.
-      d_qim.setIncomplete();
+      d_qim.setIncomplete(IncompleteId::QUANTIFIERS_SYGUS_NO_VERIFY);
       return false;
     }
     // otherwise we are unsat, and we will process the solution below
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0bcf1d19c..21c82e9eb 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -205,6 +205,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   d_qim.reset();
   bool setIncomplete = false;
+  IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS;
 
   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
   if( needsCheck ){
@@ -354,7 +355,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
             //sources of incompleteness
             for (QuantifiersUtil*& util : d_util)
             {
-              if (!util->checkComplete())
+              if (!util->checkComplete(setIncompleteId))
               {
                 Trace("quant-engine-debug") << "Set incomplete because utility "
                                             << util->identify().c_str()
@@ -372,7 +373,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
               //check if we should set the incomplete flag
               for (QuantifiersModule*& mdl : d_modules)
               {
-                if (!mdl->checkComplete())
+                if (!mdl->checkComplete(setIncompleteId))
                 {
                   Trace("quant-engine-debug")
                       << "Set incomplete because module "
@@ -447,7 +448,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   {
     if( setIncomplete ){
       Trace("quant-engine") << "Set incomplete flag." << std::endl;
-      d_qim.setIncomplete();
+      d_qim.setIncomplete(setIncompleteId);
     }
     //output debug stats
     d_qim.getInstantiate()->debugPrintModel();
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 5585b36ab..db842e5a8 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -899,7 +899,7 @@ void TheorySep::postCheck(Effort level)
 
   if (needAddLemma)
   {
-    d_im.setIncomplete();
+    d_im.setIncomplete(IncompleteId::SEP);
   }
   Trace("sep-check") << "Sep::check(): " << level
                      << " done, conflict=" << d_state.isInConflict()
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 3aa97672d..5001b51dd 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -41,7 +41,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      SkolemCache& skc)
     : d_deq(state.getSatContext()),
       d_termProcessed(state.getUserContext()),
-      d_full_check_incomplete(false),
+      d_fullCheckIncomplete(false),
+      d_fullCheckIncompleteId(IncompleteId::UNKNOWN),
       d_external(external),
       d_state(state),
       d_im(im),
@@ -208,7 +209,8 @@ bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
 void TheorySetsPrivate::fullEffortReset()
 {
   Assert(d_equalityEngine->consistent());
-  d_full_check_incomplete = false;
+  d_fullCheckIncomplete = false;
+  d_fullCheckIncompleteId = IncompleteId::UNKNOWN;
   d_most_common_type.clear();
   d_most_common_type_term.clear();
   d_card_enabled = false;
@@ -295,7 +297,8 @@ void TheorySetsPrivate::fullEffortCheck()
           // some kinds of cardinality we cannot handle
           if (d_rels->isRelationKind(nk0))
           {
-            d_full_check_incomplete = true;
+            d_fullCheckIncomplete = true;
+            d_fullCheckIncompleteId = IncompleteId::SETS_RELS_CARD;
             Trace("sets-incomplete")
                 << "Sets : incomplete because of " << n << "." << std::endl;
             // TODO (#1124):  The issue can be divided into 4 parts
@@ -789,9 +792,9 @@ void TheorySetsPrivate::postCheck(Theory::Effort level)
       {
         fullEffortCheck();
         if (!d_state.isInConflict() && !d_im.hasSentLemma()
-            && d_full_check_incomplete)
+            && d_fullCheckIncomplete)
         {
-          d_im.setIncomplete();
+          d_im.setIncomplete(d_fullCheckIncompleteId);
         }
       }
     }
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index c2f266971..3c3469b07 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -122,7 +122,9 @@ class TheorySetsPrivate {
    * is incomplete for some reason (for instance, if we combine cardinality
    * with a relation or extended function kind).
    */
-  bool d_full_check_incomplete;
+  bool d_fullCheckIncomplete;
+  /** The reason we set the above flag to true */
+  IncompleteId d_fullCheckIncompleteId;
   std::map< Node, TypeNode > d_most_common_type;
   std::map< Node, Node > d_most_common_type_term;
 
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 6a461cb7a..f38acfac2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1778,7 +1778,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   }
   else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
   {
-    d_im.setIncomplete();
+    d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
     return ProcessLoopResult::SKIPPED;
   }
 
@@ -1931,7 +1931,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     else if (options::stringProcessLoopMode()
              == options::ProcessLoopMode::SIMPLE)
     {
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
       return ProcessLoopResult::SKIPPED;
     }
 
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index ff3803b7e..8a0429fae 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -241,8 +241,6 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
   return true;
 }
 
-void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
-
 void InferenceManager::addToExplanation(Node a,
                                         Node b,
                                         std::vector<Node>& exp) const
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index cb5560f2b..cfb8614ca 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -201,12 +201,6 @@ class InferenceManager : public InferenceManagerBuffered
    * otherwise. A split is trivial if a=b rewrites to a constant.
    */
   bool sendSplit(Node a, Node b, InferenceId infer, bool preq = true);
-  /**
-   * Set that we are incomplete for the current set of assertions (in other
-   * words, we must answer "unknown" instead of "sat"); this calls the output
-   * channel's setIncomplete method.
-   */
-  void setIncomplete();
 
   //----------------------------constructing antecedants
   /**
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 7510b26ca..85d66cd54 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -303,7 +303,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
           else
           {
             // otherwise we are incomplete
-            d_im.setIncomplete();
+            d_im.setIncomplete(IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY);
           }
         }
         if (d_state.isInConflict())
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2210caf6a..dd130e28a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -234,6 +234,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_inSatMode(false),
       d_hasShutDown(false),
       d_incomplete(context, false),
+      d_incompleteTheory(context, THEORY_BUILTIN),
+      d_incompleteId(context, IncompleteId::UNKNOWN),
       d_propagationMap(context),
       d_propagationMapTimestamp(context, 0),
       d_propagatedLiterals(context),
@@ -1454,6 +1456,14 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
   }
 }
 
+void TheoryEngine::setIncomplete(theory::TheoryId theory,
+                                 theory::IncompleteId id)
+{
+  d_incomplete = true;
+  d_incompleteTheory = theory;
+  d_incompleteId = id;
+}
+
 theory::TrustNode TheoryEngine::getExplanation(
     std::vector<NodeTheoryPair>& explanationVector)
 {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8960b324d..cc3de2e50 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -199,13 +199,14 @@ class TheoryEngine {
    * context level or below).
    */
   context::CDO<bool> d_incomplete;
+  /** The theory and identifier that (most recently) set incomplete */
+  context::CDO<theory::TheoryId> d_incompleteTheory;
+  context::CDO<theory::IncompleteId> d_incompleteId;
 
   /**
    * Called by the theories to notify that the current branch is incomplete.
    */
-  void setIncomplete(theory::TheoryId theory) {
-    d_incomplete = true;
-  }
+  void setIncomplete(theory::TheoryId theory, theory::IncompleteId id);
 
   /**
    * Mapping of propagations from recievers to senders.
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index e7c89e703..1ca866871 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -517,7 +517,10 @@ void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
   d_out.safePoint(r);
 }
 
-void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
+void TheoryInferenceManager::setIncomplete(IncompleteId id)
+{
+  d_out.setIncomplete(id);
+}
 
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index e911fb41e..380ba6e48 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -370,7 +370,7 @@ class TheoryInferenceManager
    * Notification from a theory that it realizes it is incomplete at
    * this context level.
    */
-  void setIncomplete();
+  void setIncomplete(IncompleteId id);
 
  protected:
   /**
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index eb6145f9c..6ba459452 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1432,7 +1432,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       // cardinality constraint from user input, set incomplete   
       Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::UF_CARD_MODE);
     }
   }
   Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index ee3753e92..78171349d 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -227,7 +227,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
     // are present
     if (hasFunctions)
     {
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED);
     }
     return 0;
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9cb37a26d..e23bc0c45 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -177,7 +177,7 @@ bool TheoryUF::preNotifyFact(
       else
       {
         // support for cardinality constraints is not enabled, set incomplete
-        d_im.setIncomplete();
+        d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED);
       }
     }
     // don't need to assert cardinality constraints if not producing models
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 9be954059..425e61bc2 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -137,7 +137,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel
   }
 
   void requirePhase(TNode, bool) override {}
-  void setIncomplete() override {}
+  void setIncomplete(theory::IncompleteId id) override {}
   void handleUserAttribute(const char* attr, theory::Theory* t) override {}
 
   void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); }