From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 13 May 2022 15:20:53 +0000 (-0500)
Subject: Refactor logic exceptions during preregistration for arithmetic (#8769)
X-Git-Tag: cvc5-1.0.1~138
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8eebe0aaea199f8bd7ae8ef3348ca2985b20b59;p=cvc5.git

Refactor logic exceptions during preregistration for arithmetic (#8769)

Fixes #8755.
---

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 7f822c043..611cb6e81 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -20,8 +20,6 @@
 
 #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"
@@ -86,30 +84,6 @@ 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());
-    }
-  }
-  if (isTranscendentalKind(k) || k == Kind::IAND || k == Kind::POW2)
-  {
-    if (options().arith.nlCov && !options().arith.nlCovForce)
-    {
-      std::stringstream ss;
-      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindString(k)
-         << " is not compatible with using the coverings-based solver. If you know what you are doing, "
-          "you can try --nl-cov-force, but expect crashes or incorrect results.";
-      throw LogicException(ss.str());
-    }
-  }
 }
 
 void NonlinearExtension::processSideEffect(const NlLemma& se)
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bd1a04dfd..f6847c964 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -16,14 +16,16 @@
 #include "theory/arith/theory_arith.h"
 
 #include "options/smt_options.h"
+#include "printer/smt2/smt2_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_rule.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_evaluator.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/equality_solver.h"
-#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/linear/theory_arith_private.h"
+#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -108,6 +110,44 @@ void TheoryArith::finishInit()
 
 void TheoryArith::preRegisterTerm(TNode n)
 {
+  // handle logic exceptions
+  Kind k = n.getKind();
+  bool isTransKind = isTranscendentalKind(k);
+  // note that we don't throw an exception for non-linear multiplication in
+  // linear logics, since this is caught in the linear solver with a more
+  // informative error message
+  if (isTransKind || k == IAND || k == POW2)
+  {
+    if (d_nonlinearExtension == nullptr)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindString(k)
+         << " requires the logic to include non-linear arithmetic";
+      throw LogicException(ss.str());
+    }
+    // logic exceptions based on the configuration of nl-ext: if we are a
+    // transcendental function, we require nl-ext=full.
+    if (isTransKind)
+    {
+      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());
+      }
+    }
+    if (options().arith.nlCov && !options().arith.nlCovForce)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindString(k)
+         << " is not compatible with using the coverings-based solver. If "
+            "you know what you are doing, "
+            "you can try --nl-cov-force, but expect crashes or incorrect "
+            "results.";
+      throw LogicException(ss.str());
+    }
+  }
   if (d_nonlinearExtension != nullptr)
   {
     d_nonlinearExtension->preRegisterTerm(n);
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 57fe6bf72..727508583 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -818,6 +818,7 @@ set(regress_0_tests
   regress0/nl/issue8744-int.smt2
   regress0/nl/issue8744-real.smt2
   regress0/nl/issue8744-real-cov.smt2
+  regress0/nl/issue8755-nl-logic-exception.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/cli/regress0/nl/issue8755-nl-logic-exception.smt2 b/test/regress/cli/regress0/nl/issue8755-nl-logic-exception.smt2
new file mode 100644
index 000000000..29705d553
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8755-nl-logic-exception.smt2
@@ -0,0 +1,7 @@
+; EXPECT: (error "Term of kind int.pow2 requires the logic to include non-linear arithmetic")
+; EXIT: 1
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (= (- x y) (int.pow2 x)))
+(check-sat)