From 0b603261b43424bd0a08db4d9422ff7d005c33cb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 13:59:27 -0600 Subject: [PATCH] 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. --- src/theory/quantifiers/quantifiers_rewriter.cpp | 6 ++++++ src/theory/quantifiers/quantifiers_rewriter.h | 8 ++++++-- test/regress/CMakeLists.txt | 1 + .../regress0/quantifiers/issue8159-3-qext-nterm.smt2 | 9 +++++++++ 4 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue8159-3-qext-nterm.smt2 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) -- 2.30.2