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 62d8e3cf41467edb2a3713b4d333f43b1f0823a1..8d8e2fcb9200af56d265316d0ff742599347bb75 100644 (file)
--- 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 f81bcfd7b969ae1919000d03b0369d78f43a74f7..a7a06b5bcaeabf083f9d96751689e907f37b234f 100644 (file)
--- 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);