Preprare central model building for RANs (#7951)

This PR uses a new utility isEvaluationResult() instead of isConst() within the core model building. This prepares model building for model values that are not constants (in the sense of isConst()) but still constant-lilke values, like real algebraic numbers.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 97774a739fc71a1ad5b86a27291e1c03c9543af5..ef25d7819b89d6855656a821a4b1cf3d4ab427aa 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1019,10 +1019,10 @@ Node SolverEngine::getValue(const Node& ex) const
          || resultNode.getType().isSubtypeOf(expectedType))
       << "Run with -t smt for details.";
 
-  // Ensure it's a constant, or a lambda (for uninterpreted functions). This
-  // assertion only holds for models that do not have approximate values.
-  Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
-         || resultNode.isConst());
+  // Ensure it's a value (constant or const-ish like real algebraic
+  // numbers), or a lambda (for uninterpreted functions). This assertion only
+  // holds for models that do not have approximate values.
+  Assert(m->hasApproximations() || TheoryModel::isValue(resultNode));
 
   if (d_env->getOptions().smt.abstractValues && resultNode.getType().isArray())
   {

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6a083b7e330a3ffdb68de6d503f5d7e83171c67c..6a0d50ac0c4546b849dfa0140f7f9d07b728ef57 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -803,5 +803,11 @@ std::string TheoryModel::debugPrintModelEqc() const
   return ss.str();
 }
 
+bool TheoryModel::isValue(TNode node)
+{
+  return node.isConst() || node.getKind() == Kind::REAL_ALGEBRAIC_NUMBER
+         || node.getKind() == Kind::LAMBDA;
+}
+
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 6d900b39edb3bc4a2b0ca98fb1fbfba88840d40a..c1f7c880fca72bf4642b582ccce0f3082ee79767 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -357,6 +357,12 @@ class TheoryModel : protected EnvObj
    */
   std::string debugPrintModelEqc() const;
 
+  /**
+   * Is the node n a "value"? This is true if n is constant, a constant-like
+   * value (e.g. a real algebraic number) or if n is a lambda.
+   */
+  static bool isValue(TNode node);
+
  protected:
   /** Unique name of this model */
   std::string d_name;

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 4aea1ad9d8098d1d1cf80ebd90d3e5dcd5f18584..193a55294d38164c9e11c1f250eae14ddfd2bf24 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -79,7 +79,7 @@ Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
     {
       Trace("model-builder-debug") << "...try to normalize" << std::endl;
       Node normalized = normalize(m, n, true);
-      if (normalized.isConst())
+      if (TheoryModel::isValue(normalized))
       {
         return normalized;
       }
@@ -101,7 +101,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
     // Members of exclusion set must have values, otherwise we are not yet
     // assignable.
     Node er = eset[i];
-    if (er.isConst())
+    if (TheoryModel::isValue(er))
     {
       // already processed
       continue;
@@ -125,11 +125,6 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
   return true;
 }
 
-bool TheoryEngineModelBuilder::isValue(TNode n)
-{
-  return n.getKind() == kind::LAMBDA || n.isConst();
-}
-
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
   if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL
@@ -508,7 +503,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       // applicable. We check if n is a value here, e.g. a term for which
       // isConst returns true, or a lambda. The latter is required only for
       // higher-order.
-      if (isValue(n))
+      if (TheoryModel::isValue(n))
       {
         Assert(constRep.isNull());
         constRep = n;
@@ -737,7 +732,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             }
             if (!normalized.isNull())
             {
-              Assert(normalized.isConst());
+              Assert(TheoryModel::isValue(normalized));
               typeConstSet.add(tb, normalized);
               assignConstantRep(tm, *i2, normalized);
               Trace("model-builder") << "    Eval: Setting constant rep of "
@@ -776,7 +771,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             Trace("model-builder") << "    Normalizing rep (" << rep
                                    << "), normalized to (" << normalized << ")"
                                    << endl;
-            if (normalized.isConst())
+            if (TheoryModel::isValue(normalized))
             {
               changed = true;
               typeConstSet.add(tb, normalized);
@@ -1208,7 +1203,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
         {
           ri = normalize(m, ri, evalOnly);
         }
-        if (!ri.isConst())
+        if (!TheoryModel::isValue(ri))
         {
           childrenConst = false;
         }
@@ -1255,7 +1250,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
       Node rc = m->getRepresentative(un[j]);
       Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned "
                                     << rc << std::endl;
-      Assert(rc.isConst());
+      Assert(TheoryModel::isValue(rc));
       children.push_back(rc);
     }
     Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index b716ad7d8a8b89755dd83f3cca3fa3d5284b9301..fb6204b69001b82c4498216fe06389b2b92c943a 100644 (file)
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -126,11 +126,6 @@ class TheoryEngineModelBuilder : protected EnvObj
    * state of the model m.
    */
   Node evaluateEqc(TheoryModel* m, TNode r);
-  /**
-   * Is the node n a "value"? This is true if n is constant, or if n is a
-   * lambda.
-   */
-  static bool isValue(TNode n);
   /** is n an assignable expression?
    *
    * A term n is an assignable expression if its value is unconstrained by a