Fix solution filtering for streaming abducts (#3143)

diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index 2c6186372be0c0d50972876653f2083a006dc2f3..8c664fec52818f1921dab2ac4fd9962d3afcf66e 100644 (file)
--- 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 2c65c7e140b3e20991cc5662f8bdbfc4608748b0..99b464d0937a591c9e98745f6a9c54f88b2d854c 100644 (file)
--- 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 (file)
index 0000000..17971f1
--- /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))
+  )
+)