Add trascendental function kinds to list of unevaluated operators (#4640)

Fixes #4636.

This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b63566c2961e8af191cfb5a1d1bd7fd2adf1e1b0..c25090f383abbbe51e0cc3d2e37648b1ed2e6420 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -72,6 +72,10 @@ void TheoryArith::finishInit()
   {
     // witness is used to eliminate square root
     tm->setUnevaluatedKind(kind::WITNESS);
+    // we only need to add the operators that are not syntax sugar
+    tm->setUnevaluatedKind(kind::EXPONENTIAL);
+    tm->setUnevaluatedKind(kind::SINE);
+    tm->setUnevaluatedKind(kind::PI);
   }
 }
 

diff --git a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
index 69bb74e849092751b9fdc07b57a18fad37fe55f1..75d4b6e3a86adf178b7dc23f5c8d338a3ae53241 100644 (file)
--- a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
+++ b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --quiet --no-check-models
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)