From 624b03d3826f790bf1354276a974b5f76afe14c8 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 7 Feb 2022 12:22:58 -0800
Subject: [PATCH] Improve combination of NRA and transcendentals (#8075)

This PR tackles two issues when combining transcendental reasoning with nonlinear arithmetic.
Firstly, the NRAT logic would inadvertently have transcendental reasoning disabled because we only checked for integers. This simply adds an additional check at the end to enforce transcendental reasoning if necessary.
Secondly, we assert that we never add multiple substitutions for the same variable. This weakens the check to allow add the very same substitution multiple times.
Fixes #7984.
---
 src/smt/set_defaults.cpp                             |  7 +++++++
 src/theory/arith/nl/nl_model.cpp                     | 12 ++++++++----
 test/regress/CMakeLists.txt                          |  1 +
 .../regress0/arith/issue7984-quant-trans.smt2        |  8 ++++++++
 4 files changed, 24 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/arith/issue7984-quant-trans.smt2

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c3df86bf3..387fd8927 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -829,6 +829,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
   }
 #endif
+  if (logic.isTheoryEnabled(theory::THEORY_ARITH) && logic.areTranscendentalsUsed())
+  {
+      if (!opts.arith.nlExtWasSetByUser)
+      {
+        opts.arith.nlExt = options::NlExtMode::FULL;
+      }
+  }
 }
 
 bool SetDefaults::isSygus(const Options& opts) const
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index edd00a6dd..a28117d87 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -278,10 +278,14 @@ bool NlModel::addSubstitution(TNode v, TNode s)
   // should not set exact bound more than once
   if (d_substitutions.contains(v))
   {
-    Trace("nl-ext-model") << "...ERROR: already has value." << std::endl;
-    // this should never happen since substitutions should be applied eagerly
-    Assert(false);
-    return false;
+    Node cur = d_substitutions.getSubs(v);
+    if (cur != s)
+    {
+      Trace("nl-ext-model") << "...ERROR: already has value: " << cur << std::endl;
+      // this should never happen since substitutions should be applied eagerly
+      Assert(false);
+      return false;
+    }
   }
   // if we previously had an approximate bound, the exact bound should be in its
   // range
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7698b19aa..1b10d47f2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -63,6 +63,7 @@ set(regress_0_tests
   regress0/arith/issue4525.smt2
   regress0/arith/issue5219-conflict-rewrite.smt2
   regress0/arith/issue5761-ppr.smt2
+  regress0/arith/issue7984-quant-trans.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc.smt2
diff --git a/test/regress/regress0/arith/issue7984-quant-trans.smt2 b/test/regress/regress0/arith/issue7984-quant-trans.smt2
new file mode 100644
index 000000000..a6f31ac99
--- /dev/null
+++ b/test/regress/regress0/arith/issue7984-quant-trans.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --check-models
+; EXPECT: (error "Cannot run check-model on a model with approximate values.")
+; EXIT: 1
+(set-logic QF_NRAT)
+(set-option :re-elim-agg true)
+(declare-fun r6 () Real)
+(assert (= 0.0 (cos r6)))
+(check-sat)
\ No newline at end of file
-- 
2.30.2