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 /src | |
| parent | 71d0ce95f1e5ab74f3b0074494d4e8a4137fd079 (diff) | |
Fix solution filtering for streaming abducts (#3143)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/solution_filter.cpp | 5 |
1 files changed, 3 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; |