From 0045ba2af7b31243c545828494d11f53e16f59db Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Jun 2020 11:45:41 -0500 Subject: [PATCH] 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). --- src/theory/arith/theory_arith.cpp | 4 ++++ test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b63566c29..c25090f38 100644 --- 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 69bb74e84..75d4b6e3a 100644 --- 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) -- 2.30.2