Throw logic exception if a transcendental function is encountered when nl-ext is...

Fixes cvc5/cvc5-projects#376.

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 43004c21ef88f71b30d3f030843aed5dc4df20b1..6f8bd56a5bfae13a2a570f3381b033e79aba9fd4 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -20,7 +20,10 @@
 
 #include "options/arith_options.h"
 #include "options/smt_options.h"
+#include "printer/smt2/smt2_printer.h"
+#include "smt/logic_exception.h"
 #include "theory/arith/arith_state.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/bound_inference.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
@@ -86,6 +89,19 @@ void NonlinearExtension::preRegisterTerm(TNode n)
   // register terms with extended theory, to find extended terms that can be
   // eliminated by context-depedendent simplification.
   d_extTheory.registerTerm(n);
+  // logic exceptions based on the configuration of nl-ext: if we are a
+  // transcendental function, we require nl-ext=full.
+  Kind k = n.getKind();
+  if (isTranscendentalKind(k))
+  {
+    if (options().arith.nlExt != options::NlExtMode::FULL)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindString(k)
+         << " requires nl-ext mode to be set to value 'full'";
+      throw LogicException(ss.str());
+    }
+  }
 }
 
 void NonlinearExtension::processSideEffect(const NlLemma& se)

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 5af2902290f51224cf676d6e88c9a3af1a2ac06a..4d7d95a86557c84faed3dd10ef74dbdd01ddda61 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -78,15 +78,14 @@ void TranscendentalState::init(const std::vector<Node>& xts,
   // for computing congruence
   std::map<Kind, ArgTrie> argTrie;
   NodeMap::const_iterator itp;
-  for (std::size_t i = 0, xsize = xts.size(); i < xsize; ++i)
+  for (const Node& a : xts)
   {
+    Kind ak = a.getKind();
     // Ignore if it is not a transcendental
-    if (!isTranscendentalKind(xts[i].getKind()))
+    if (!isTranscendentalKind(ak))
     {
       continue;
     }
-    Node a = xts[i];
-    Kind ak = a.getKind();
     bool consider = true;
     // if we've already assigned a purified term
     itp = d_trPurify.find(a);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 55d81d96434e37f81d0be51622c005ad43d5d702..0e1e84f1ab74bc9d54b2abac3186aab91f14eff7 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -801,6 +801,7 @@ set(regress_0_tests
   regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
   regress0/nl/nta/issue8183-tc-pi.smt2
   regress0/nl/nta/issue8208-red-nred.smt2
+  regress0/nl/nta/proj-issue376.smt2
   regress0/nl/nta/proj-issue403.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
   regress0/nl/nta/real-pi.smt2

diff --git a/test/regress/regress0/nl/nta/proj-issue376.smt2 b/test/regress/regress0/nl/nta/proj-issue376.smt2
new file mode 100644 (file)
index 0000000..7f28a6d
--- /dev/null
+++ b/test/regress/regress0/nl/nta/proj-issue376.smt2
@@ -0,0 +1,6 @@
+; EXPECT: (error "Term of kind real.pi requires nl-ext mode to be set to value 'full'")
+; EXIT: 1
+(set-logic ALL)
+(set-option :nl-ext light)
+(assert (< real.pi 0.0))
+(check-sat)