Fix non-termination in quantifiers rewriter (#8165)

Caused by 2 rewrite steps (conditional splitting and extended rewriting) being inverses of each other when miniscoping is disabled.

Fixes the third benchmark on #8159.

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 479bbba1ee142171b9401ad3e38ac1369005baee..4b98f83378182f61cb9e6bee2cb91a079028ca34 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -683,6 +683,12 @@ Node QuantifiersRewriter::computeCondSplit(Node body,
   }
   Trace("cond-var-split-debug")
       << "Conditional var elim split " << body << "?" << std::endl;
+  // we only do this splitting if miniscoping is enabled, as this is
+  // required to eliminate variables in conjuncts below
+  if (!d_opts.quantifiers.miniscopeQuant)
+  {
+    return body;
+  }
 
   if (bk == ITE
       || (bk == EQUAL && body[0].getType().isBoolean()

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index d1e02b75d693dea060a2d8a0fbae3e07c94ba960..b3e9ec8c2c6cb29a22ce7b37a01dd9782ab7ffca 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -45,8 +45,6 @@ enum RewriteStep
   COMPUTE_MINISCOPING,
   /** Aggressive miniscoping */
   COMPUTE_AGGRESSIVE_MINISCOPING,
-  /** Apply the extended rewriter to quantified formula bodies */
-  COMPUTE_EXT_REWRITE,
   /**
    * Term processing (e.g. simplifying terms based on ITE lifting,
    * eliminating extended arithmetic symbols).
@@ -58,6 +56,12 @@ enum RewriteStep
   COMPUTE_VAR_ELIMINATION,
   /** Conditional splitting */
   COMPUTE_COND_SPLIT,
+  /**
+   * Apply the extended rewriter to quantified formula bodies. This step
+   * must come last, since it may invert other steps above, e.g. conditional
+   * splitting.
+   */
+  COMPUTE_EXT_REWRITE,
   /** Placeholder for end of steps */
   COMPUTE_LAST
 };

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2ec4dc34890bc32902bd4711f62a60d00fe7af18..e2b234950a652605d9783f68fc546353b6f643c3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1010,6 +1010,7 @@ set(regress_0_tests
   regress0/quantifiers/issue6999-deq-elim.smt2
   regress0/quantifiers/issue7353-var-elim-par-dt.smt2
   regress0/quantifiers/issue8001-mem-leak.smt2
+  regress0/quantifiers/issue8159-3-qext-nterm.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2

diff --git a/test/regress/regress0/quantifiers/issue8159-3-qext-nterm.smt2 b/test/regress/regress0/quantifiers/issue8159-3-qext-nterm.smt2
new file mode 100644 (file)
index 0000000..bc87748
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue8159-3-qext-nterm.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --no-debug-check-models
+; EXPECT: sat
+(set-logic NIA)
+(set-option :ext-rewrite-quant true)
+(set-info :status sat)
+(declare-fun v4 () Bool)
+(declare-fun v92 () Bool)
+(assert (forall ((q688 Bool)) (or v4 (and v92 q688))))
+(check-sat)