From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2020 14:25:57 +0000 (-0500)
Subject: Do not traverse quantifiers in nl ext purify (#3982)
X-Git-Tag: cvc5-1.0.0~3534
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2758b664c43de299d0ba80537f09ccdda026119;p=cvc5.git

Do not traverse quantifiers in nl ext purify (#3982)
---

diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index a6da281ba..eb5728228 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -45,6 +45,11 @@ Node NlExtPurify::purifyNlTerms(TNode n,
       return (*find).second;
     }
   }
+  if (n.isClosure())
+  {
+    // don't traverse quantified formulas
+    return n;
+  }
   Node ret = n;
   if (n.getNumChildren() > 0)
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e0e8b236e..aaf340ce7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1297,6 +1297,7 @@ set(regress_1_tests
   regress1/ho/SYO056^1.p
   regress1/hole6.cvc
   regress1/ite5.smt2
+  regress1/issue3970-nl-ext-purify.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
diff --git a/test/regress/regress1/issue3970-nl-ext-purify.smt2 b/test/regress/regress1/issue3970-nl-ext-purify.smt2
new file mode 100644
index 000000000..5fbddf13d
--- /dev/null
+++ b/test/regress/regress1/issue3970-nl-ext-purify.smt2
@@ -0,0 +1,37 @@
+(set-logic QF_UFNRA)
+(set-option :nl-ext-purify true)
+(set-option :sygus-inference true)
+(set-info :status unsat)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(declare-const r3 Real)
+(declare-const r5 Real)
+(assert v8)
+(declare-const v10 Bool)
+(assert (= 169 r5))
+(declare-const v11 Bool)
+(assert v5)
+(declare-const v12 Bool)
+(declare-const r7 Real)
+(assert (not v1))
+(assert v10)
+(declare-const v13 Bool)
+(declare-const r8 Real)
+(assert (not (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
+(assert v4)
+(assert (and (distinct v3 v4 (= 169 r5) (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v11 v7 (= 169 r5)) (> 0.816577 169 569703 0.26205) (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3) v3 (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v5 v10))
+(declare-const v14 Bool)
+(assert (or (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v6 (or (<= 0.26205 r7 353 569703) v7 v8 v13 v3) v5 v6 (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
+(declare-const v15 Bool)
+(assert (xor v3 v11 v9 v3))
+(declare-const v16 Bool)
+(assert (xor v2 v8))
+(check-sat)