From bc5de34f98cde1c1aa77649654ddc6271f8c692b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Mar 2022 17:35:12 -0500 Subject: [PATCH] Fix return value for candidate rewrite database (#8354) Currently causes sygus reconstruction to return spurious solutions, due to being justified by candidate rewrites. --- src/theory/quantifiers/candidate_rewrite_database.cpp | 11 +++++++++++ src/theory/quantifiers/candidate_rewrite_database.h | 3 ++- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 62d8e3cf4..8d8e2fcb9 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -262,6 +262,17 @@ Node CandidateRewriteDatabase::addTerm(Node sol, d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz); } } + // If we failed to verify, then we return the original term. This is done + // so that the user of this method is not told of a rewrite rule that + // may not hold. Furthermore, note that the term is not added to the lazy + // trie in the sygus sampler. This means that the set of rewrites is not + // complete, as we are discarding the current solution. Ideally, we would + // store a list of terms (that are pairwise unknown to be equal) at each + // leaf of the lazy trie. + if (!verified) + { + eq_sol = sol; + } } // We count this as a rewrite if we did not explicitly rule it out. // The value of is_unique_term is false iff this call resulted in a rewrite. diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index f81bcfd7b..a7a06b5bc 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -88,7 +88,8 @@ class CandidateRewriteDatabase : public ExprMiner * @param out The stream to output rewrite rules on. * @param rew_print Set to true if this class printed a rewrite involving sol. * @return A previous term eq_sol added to this class, such that sol is - * equivalent to eq_sol based on the criteria used by this class. + * equivalent to eq_sol based on the criteria used by this class. We return + * only terms that are verified to be equivalent to sol. */ Node addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print); Node addTerm(Node sol, bool rec, std::ostream& out); -- 2.30.2