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 93786f6468aba698d6b851c86c776170ebbc635b..3e5fb2b4a69d4e199c0b2aec804950310fdcfeeb 100644 (file)
--- 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 8fda24a13d7dfd90ed761e69c446ad02e3cb0e68..d6be8cafd15288a011ea41e38012bf365704a857 100644 (file)
--- 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 (file)
index 0000000..a98c6e5
--- /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)