From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Feb 2022 19:59:27 +0000 (-0600)
Subject: Fix non-termination in quantifiers rewriter (#8165)
X-Git-Tag: cvc5-1.0.0~374
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0b603261b43424bd0a08db4d9422ff7d005c33cb;p=cvc5.git

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 479bbba1e..4b98f8337 100644
--- 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 d1e02b75d..b3e9ec8c2 100644
--- 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 2ec4dc348..e2b234950 100644
--- 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
index 000000000..bc877485e
--- /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)