Properly restrict PBE symmetry breaking for abduction queries (#7269)

This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.

It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.

2 files changed, 12 insertions, 5 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
index 1b5b3f5af..1170eee82 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -46,7 +46,7 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
   // First, must be unique up to rewriting
   if (bterms.find(bnr) != bterms.end())
   {
-    Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+    Trace("sygus-enum-exc") << "Exclude (by rewriting): " << bn << std::endl;
     return false;
   }
   // insert to builtin term cache, regardless of whether it is redundant
@@ -55,8 +55,6 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
   // callback-specific add term
   if (!addTermInternal(n, bn, bnr))
   {
-    Trace("sygus-enum-exc")
-        << "Exclude: " << bn << " due to callback" << std::endl;
     return false;
   }
   Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index ab2a73cb0..4fa8ba78e 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -204,7 +204,16 @@ void SynthConjecture::assign(Node q)
     }
   }
   // initialize the example inference utility
-  if (!d_exampleInfer->initialize(d_base_inst, d_candidates))
+  // Notice that we must also consider the side condition when inferring
+  // whether the conjecture is PBE. This ensures we do not prune solutions
+  // that may satisfy the side condition based on equivalence-up-to-examples
+  // with solutions that do not.
+  Node conjForExamples = d_base_inst;
+  if (!d_embedSideCondition.isNull())
+  {
+    conjForExamples = nm->mkNode(AND, d_embedSideCondition, d_base_inst);
+  }
+  if (d_exampleInfer!=nullptr && !d_exampleInfer->initialize(conjForExamples, d_candidates))
   {
     // there is a contradictory example pair, the conjecture is infeasible.
     Node infLem = d_feasible_guard.negate();
@@ -761,7 +770,7 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e)
   }
   // otherwise, allocate it
   Node f = d_tds->getSynthFunForEnumerator(e);
-  bool hasExamples = (d_exampleInfer->hasExamples(f)
+  bool hasExamples = (d_exampleInfer != nullptr && d_exampleInfer->hasExamples(f)
                       && d_exampleInfer->getNumExamples(f) != 0);
   d_enumManager[e].reset(new EnumValueManager(
       d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples));