From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Aug 2019 14:40:36 +0000 (-0500)
Subject: Fix solution filtering for streaming abducts (#3143)
X-Git-Tag: cvc5-1.0.0~4054
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=613bf2cc56a80af66f2cad9e55374136c5a346f8;p=cvc5.git

Fix solution filtering for streaming abducts (#3143)
---

diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index 2c6186372..8c664fec5 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -55,10 +55,11 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
   {
     curr = d_curr_sols.size() == 1
                ? d_curr_sols[0]
-               : nm->mkNode(d_isStrong ? AND : OR, d_curr_sols);
+               : nm->mkNode(d_isStrong ? OR : AND, d_curr_sols);
     Node imp = nm->mkNode(AND, basen.negate(), curr);
     Trace("sygus-sol-implied")
-        << "  implies: check subsumed " << imp << "..." << std::endl;
+        << "  implies: check subsumed (strong=" << d_isStrong << ") " << imp
+        << "..." << std::endl;
     // check the satisfiability query
     Result r = doCheck(imp);
     Trace("sygus-sol-implied") << "  implies: ...got : " << r << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2c65c7e14..99b464d09 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1630,6 +1630,7 @@ set(regress_1_tests
   regress1/strings/type002.smt2
   regress1/strings/type003.smt2
   regress1/strings/username_checker_min.smt2
+  regress1/sygus-abduct-ex1-grammar.smt2
   regress1/sygus-abduct-test.smt2
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
diff --git a/test/regress/regress1/sygus-abduct-ex1-grammar.smt2 b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
new file mode 100644
index 000000000..17971f184
--- /dev/null
+++ b/test/regress/regress1/sygus-abduct-ex1-grammar.smt2
@@ -0,0 +1,28 @@
+; COMMAND-LINE: --produce-abducts --sygus-stream --sygus-abort-size=3
+; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
+; SCRUBBER: sed -e 's/.*(>= j (+ 1 1))/SPURIOUS/; s/(define-fun.*//; /^$/d'
+; EXIT: 1
+
+(set-logic QF_LIA)
+(set-option :produce-abducts true)
+
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (and (>= n 0) (>= m 0)))
+(assert (< n i))
+(assert (< (+ i j) m))
+
+; This test ensures that (>= j (+ 1 1)) is not printed as a solution,
+; since it is spurious: (>= j 0) is a stronger solution and will be enumerated
+; first.
+(get-abduct A 
+  (not (<= n m))
+  ((GA Bool) (GI Int))
+  (
+  (GA Bool ((>= GI GI)))
+  (GI Int ((+ GI GI) (- GI) i j 0 1))
+  )
+)