Do not apply unconstrained simplification when quantifiers are present (#4532)

Fixes #4437.

This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.

It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.

10 files changed, 33 insertions, 23 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 08e6f317c..449c0c31e 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -346,7 +346,7 @@ header = "options/smt_options.h"
   long       = "unconstrained-simp"
   type       = "bool"
   default    = "false"
-  help       = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)"
+  help       = "turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis). Fully supported only in (subsets of) the logic QF_ABV."
 
 [[option]]
   name       = "repeatSimp"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 081990a45..f29e03380 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
   std::vector<api::Sort> argTypes;
 }
   : LPAREN_TOK quantOp[kind]
-    { PARSER_STATE->pushScope(true); }
+    {
+      if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS))
+      {
+        PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
+      }
+      PARSER_STATE->pushScope(true);
+    }
     boundVarList[bvl]
     term[f, f2] RPAREN_TOK
     {
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 5d544ae57..b74909824 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -91,6 +91,15 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
         d_unconstrained.insert(current);
       }
     }
+    else if (current.isClosure())
+    {
+      // Throw an exception. This should never happen in practice unless the
+      // user specifically enabled unconstrained simplification in an illegal
+      // logic.
+      throw LogicException(
+          "Cannot use unconstrained simplification in this logic, due to "
+          "(possibly internally introduced) quantified formula.");
+    }
     else
     {
       for (TNode childNode : current)
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index ac4fd0a03..7fc13e17d 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -62,7 +62,11 @@ class UnconstrainedSimplifier : public PreprocessingPass
   theory::SubstitutionMap d_substitutions;
 
   const LogicInfo& d_logicInfo;
-
+  /**
+   * Visit all subterms in assertion. This method throws a LogicException if
+   * there is a subterm that is unhandled by this preprocessing pass (e.g. a
+   * quantified formula).
+   */
   void visitAll(TNode assertion);
   Node newUnconstrainedVar(TypeNode t, TNode var);
   void processUnconstrained();
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b66d4e973..801f38b29 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -740,6 +740,7 @@ set(regress_0_tests
   regress0/quantifiers/issue3655.smt2
   regress0/quantifiers/issue4086-infs.smt2
   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
+  regress0/quantifiers/issue4437-unc-quant.smt2
   regress0/quantifiers/issue4476-ext-rew.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
@@ -1127,8 +1128,6 @@ set(regress_0_tests
   regress0/uflra/simple.03.cvc
   regress0/uflra/simple.04.cvc
   regress0/unconstrained/4481.smt2
-  regress0/unconstrained/4484.smt2
-  regress0/unconstrained/4486.smt2
   regress0/unconstrained/arith.smt2
   regress0/unconstrained/arith3.smt2
   regress0/unconstrained/arith4.smt2
diff --git a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2
new file mode 100644
index 000000000..61f792999
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2
@@ -0,0 +1,7 @@
+; EXPECT: (error "Parse Error: issue4437-unc-quant.smt2:6.15: Quantifier used in non-quantified logic.")
+; EXIT: 1
+(set-logic QF_AUFBVLIA)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (forall ((c (_ BitVec 8))) (= (bvashr c a) b)))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2
index 028607093..19179f4d7 100644
--- a/test/regress/regress0/unconstrained/4481.smt2
+++ b/test/regress/regress0/unconstrained/4481.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
-; EXPECT: unsat
+; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.")
+; EXIT: 1
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2
deleted file mode 100644
index f2f11295b..000000000
--- a/test/regress/regress0/unconstrained/4484.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --unconstrained-simp
-; EXPECT: unsat
-(set-logic QF_NIRA)
-(set-info :status unsat)
-(declare-fun a () Real)
-(assert (= (to_int a) 2))
-(assert (= (to_int (/ a 2.0)) 2))
-(check-sat)
diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2
deleted file mode 100644
index 01771ce66..000000000
--- a/test/regress/regress0/unconstrained/4486.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --unconstrained-simp
-; EXPECT: sat
-(set-logic ALL)
-(set-info :status sat)
-(declare-fun x () Real)
-(assert (is_int x))
-(assert (is_int (+ x 1)))
-(check-sat)
diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 63a95bb78..6109a01dd 100644
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.6)
-(set-logic QF_SLIA)
+(set-logic SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)