From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 2 Apr 2022 02:48:35 +0000 (-0500)
Subject: Ignore irrelevant exponential terms (#8534)
X-Git-Tag: cvc5-1.0.0~41
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d94ee09f56c82be899dd796c91c767a8711302e4;p=cvc5.git

Ignore irrelevant exponential terms (#8534)

Fixes #8517.
---

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 93786f646..3e5fb2b4a 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -153,6 +153,14 @@ void ExponentialSolver::checkMonotonic()
 
   for (const Node& tf : it->second)
   {
+    Node mva = d_data->d_model.computeAbstractModelValue(tf);
+    if (mva == tf)
+    {
+      // if it was not assigned a model value by the linear solver, it is
+      // not a relevant term. This can happen for terms like (exp (exp 1.0)),
+      // where (exp 1.0) is not relevant until we purify (exp (exp 1.0)).
+      continue;
+    }
     Node a = tf[0];
     Node mvaa = d_data->d_model.computeAbstractModelValue(a);
     if (mvaa.isConst())
@@ -178,7 +186,8 @@ void ExponentialSolver::checkMonotonic()
     Assert(sargval.isConst());
     Node s = tf_arg_to_term[sarg];
     Node sval = d_data->d_model.computeAbstractModelValue(s);
-    Assert(sval.isConst());
+    Assert(sval.isConst()) << "non-constant model value " << sval << " for "
+                           << s;
 
     // store the concavity region
     d_data->d_tf_region[s] = 1;
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 8fda24a13..d6be8cafd 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2229,6 +2229,7 @@ set(regress_1_tests
   regress1/quantifiers/issue8456-2-syqi-ic.smt2
   regress1/quantifiers/issue8456-syqi-ic.smt2
   regress1/quantifiers/issue8497-syqi-str-fmf.smt2
+  regress1/quantifiers/issue8517-exp-exp.smt2
   regress1/quantifiers/issue8520-cegqi-nl-cov.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
diff --git a/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2
new file mode 100644
index 000000000..a98c6e5c2
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2
@@ -0,0 +1,6 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-const x1 Bool)
+(assert (forall ((r Real)) (= x (and x1 (= r 2) (= 0.0 (exp (exp 1.0))) (= 3 (/ (- r) (- r)))))))
+(check-sat)