From 62a7f715faf99ff8ab6db34f3c790dfaf337c24c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 23:00:32 -0600
Subject: [PATCH] Throw logic exception if a transcendental function is
 encountered when nl-ext is not full (#8212)

Fixes cvc5/cvc5-projects#376.
---
 src/theory/arith/nl/nonlinear_extension.cpp      | 16 ++++++++++++++++
 .../nl/transcendental/transcendental_state.cpp   |  7 +++----
 test/regress/CMakeLists.txt                      |  1 +
 test/regress/regress0/nl/nta/proj-issue376.smt2  |  6 ++++++
 4 files changed, 26 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/nl/nta/proj-issue376.smt2

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 43004c21e..6f8bd56a5 100644
--- 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 5af290229..4d7d95a86 100644
--- 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 55d81d964..0e1e84f1a 100644
--- 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
index 000000000..7f28a6d45
--- /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)
-- 
2.30.2