Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)

Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a69542b17c8a8b6bed8762e7a04eb20a3148ded3..e1ce29b65af006347887269bdc76b9b77cb8254f 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1124,11 +1124,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
       return ret;
     }
-    if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
-    {
-      parseError(
-          "eqrange predicate requires option --arrays-exp to be enabled.");
-    }
     if (kind == api::SINGLETON && args.size() == 1)
     {
       api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9e69c9f7188c9371b61577ea8d57a772ab73b3f8..93eadde43c609aa5deabdd0d4883fb7f019ba682 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
 
 TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
 {
-  // first, see if we need to expand definitions
+  // first, check for logic exceptions
+  Kind k = term.getKind();
+  if (!options().arrays.arraysExp)
+  {
+    if (k == kind::EQ_RANGE)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << k
+         << " not supported in default mode, try --arrays-exp";
+      throw LogicException(ss.str());
+    }
+  }
+  // see if we need to expand definitions
   TrustNode texp = d_rewriter.expandDefinition(term);
   if (!texp.isNull())
   {
@@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
   d_ppEqualityEngine.addTerm(term);
   NodeManager* nm = NodeManager::currentNM();
   Node ret;
-  switch (term.getKind()) {
+  switch (k)
+  {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da9c9f00141aa5544a15cf3a05b909e2b6f91cae..272867d0caa53482443e2742595b96120956e486 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -558,6 +558,7 @@ set(regress_0_tests
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
   regress0/echo.smt2
+  regress0/eqrange0.smt2
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2

diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2
new file mode 100644 (file)
index 0000000..01713d1
--- /dev/null
+++ b/test/regress/regress0/eqrange0.smt2
@@ -0,0 +1,6 @@
+; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp")
+; EXIT: 1
+(set-logic QF_AUFLIA)
+(declare-const a (Array Int Int))
+(assert (eqrange a a 0 0))
+(check-sat)