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.

4 files changed, 3 insertions, 11 deletions

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())