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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c3df86bf3b954ac40f568b34dbc584dbc1b017ec..387fd89277966db87b8721d99737428e7541e8cf 100644 (file)
--- 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 edd00a6dd58918c1ce4e6cf77344e72cb2939a7f..a28117d87bfb7935cc657c67c4ccf7a690ea4861 100644 (file)
--- 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 7698b19aab08ba64cfb68251113f4f95b741232b..1b10d47f20fd7b854de62a38caa4edc6a37bf413 100644 (file)
--- 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 (file)
index 0000000..a6f31ac
--- /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