From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 21 Mar 2022 22:35:12 +0000 (-0500)
Subject: Fix return value for candidate rewrite database (#8354)
X-Git-Tag: cvc5-1.0.0~218
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc5de34f98cde1c1aa77649654ddc6271f8c692b;p=cvc5.git

Fix return value for candidate rewrite database (#8354)

Currently causes sygus reconstruction to return spurious solutions, due to being justified by candidate rewrites.
---

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);