From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 Feb 2022 23:56:33 +0000 (-0600)
Subject: Ensure variables are constrained in model when equal to transcendental function apps... 
X-Git-Tag: cvc5-1.0.0~383
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8b52b5cfa2fbfcb6d3450b9e03b2fa680af605d;p=cvc5.git

Ensure variables are constrained in model when equal to transcendental function apps (#8153)

Fixes #8147.
---

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index f3393caae..5a410ba2d 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -41,13 +41,6 @@ void CheckModels::checkModel(TheoryModel* m,
   // If this function is running, the user gave --check-model (or equivalent),
   // and if verbose(1) is on, the user gave --verbose (or equivalent).
 
-  // check-model is not guaranteed to succeed if approximate values were used.
-  // Thus, we intentionally abort here.
-  if (m->hasApproximations())
-  {
-    throw RecoverableModalException(
-        "Cannot run check-model on a model with approximate values.");
-  }
   Node sepHeap, sepNeq;
   if (m->getHeapModel(sepHeap, sepNeq))
   {
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 6a254fc54..c394512d1 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -455,13 +455,15 @@ void TranscendentalSolver::postProcessModel(std::map<Node, Node>& arithModel,
                                             const std::set<Node>& termSet)
 {
   Trace("nl-ext") << "TranscendentalSolver::postProcessModel" << std::endl;
-  std::unordered_set<Node> trReps;
+  // map from equivalence classes to a transcendental function application,
+  // if it exists.
+  std::unordered_map<Node, Node> trReps;
   for (const Node& n : termSet)
   {
     if (isTranscendentalKind(n.getKind()))
     {
       Node r = d_astate.getRepresentative(n);
-      trReps.insert(r);
+      trReps[r] = n;
     }
   }
   if (trReps.empty())
@@ -469,25 +471,29 @@ void TranscendentalSolver::postProcessModel(std::map<Node, Node>& arithModel,
     Trace("nl-ext") << "...no transcendental functions" << std::endl;
     return;
   }
-  std::vector<Node> rmFromModel;
+  std::unordered_map<Node, Node>::iterator it;
   for (auto& am : arithModel)
   {
+    // skip integer variables
+    if (am.first.getType().isInteger())
+    {
+      continue;
+    }
     Node r = d_astate.getRepresentative(am.first);
-    if (trReps.find(r) != trReps.end())
+    it = trReps.find(r);
+    // if it is in the same equivalence class as a trancendental function
+    // application, we replace its value in the model with that application
+    if (it != trReps.end())
     {
-      Trace("nl-ext") << "...erase value for " << am.first
-                      << ", since approximate" << std::endl;
-      rmFromModel.push_back(am.first);
+      Trace("nl-ext") << "...abstract value for " << am.first << " to "
+                      << it->second << std::endl;
+      am.second = it->second;
     }
     else
     {
       Trace("nl-ext") << "...keep model value for " << am.first << std::endl;
     }
   }
-  for (const Node& n : rmFromModel)
-  {
-    arithModel.erase(n);
-  }
 }
 
 }  // namespace transcendental
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index f8c7b8c9b..413d4535f 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -153,9 +153,16 @@ class TranscendentalSolver : protected EnvObj
   void checkTranscendentalTangentPlanes();
 
   /**
-   * Post-process model. This ensures that the domain of arithModel does not
-   * contain terms that are equal to any transcendental function applications,
+   * Post-process model. This ensures that for all terms t in the domain of
+   * arithModel, if t is in the same equivalence class as a transcendental
+   * function application, then arithModel[t] maps to one such application.
+   *
+   * This is to ensure that the linear model is ignored for such terms,
    * as their values cannot be properly represented in the model.
+   *
+   * It is important to map such terms t to a transcendental function
+   * application, or otherwise they would be unconstrained, leading to
+   * spurious models.
    */
   void postProcessModel(std::map<Node, Node>& arithModel,
                         const std::set<Node>& termSet);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b28651d95..71219634b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -789,6 +789,7 @@ set(regress_0_tests
   regress0/nl/nta/exp-n0.5-ub.smt2
   regress0/nl/nta/exp-neg2-unsat-unsound.smt2
   regress0/nl/nta/exp1-ub.smt2
+  regress0/nl/nta/issue8147-unc-model.smt2
   regress0/nl/nta/real-pi.smt2
   regress0/nl/nta/sin-sym.smt2
   regress0/nl/nta/sqrt-simple.smt2
diff --git a/test/regress/regress0/nl/nta/issue8147-unc-model.smt2 b/test/regress/regress0/nl/nta/issue8147-unc-model.smt2
new file mode 100644
index 000000000..1acdab13b
--- /dev/null
+++ b/test/regress/regress0/nl/nta/issue8147-unc-model.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x Bool)
+(declare-fun a () Real)
+(declare-fun r () Real)
+(declare-fun v () Real)
+(assert (and (xor (= a 1.0) x) (= 1 (- v (exp (* r v))))))
+(check-sat)