diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-02 09:40:36 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-02 09:40:36 -0500 |
| commit | 613bf2cc56a80af66f2cad9e55374136c5a346f8 (patch) | |
| tree | 1378a3c216635f578fd4c2105d90e9dc28318a60 | |
| parent | 71d0ce95f1e5ab74f3b0074494d4e8a4137fd079 (diff) | |
Fix solution filtering for streaming abducts (#3143)
| -rw-r--r-- | src/theory/quantifiers/solution_filter.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-ex1-grammar.smt2 | 28 |
3 files changed, 32 insertions, 2 deletions
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)) + ) +) |