Add inference ids for remainder of sygus solver (#6977)

Now, all inferences throughout cvc5 in our regression are properly marked with an InferenceId.

This PR includes minor simplifications to the interface for sygus modules. In particular it changes the behavior to send inferences via the inference manager instead of passing them around as a vector.

1 files changed, 13 insertions, 7 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 892ee6dd4..27a1e3f3b 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -44,8 +44,7 @@ SygusPbe::~SygusPbe() {}
 
 bool SygusPbe::initialize(Node conj,
                           Node n,
-                          const std::vector<Node>& candidates,
-                          std::vector<Node>& lemmas)
+                          const std::vector<Node>& candidates)
 {
   Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
@@ -166,8 +165,7 @@ bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
 bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
                                    const std::vector<Node>& enum_values,
                                    const std::vector<Node>& candidates,
-                                   std::vector<Node>& candidate_values,
-                                   std::vector<Node>& lems)
+                                   std::vector<Node>& candidate_values)
 {
   Assert(enums.size() == enum_values.size());
   if( !enums.empty() ){
@@ -234,9 +232,10 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
         Assert(!g.isNull());
         for (unsigned k = 0, size = enum_lems.size(); k < size; k++)
         {
-          enum_lems[k] = nm->mkNode(OR, g.negate(), enum_lems[k]);
+          Node lem = nm->mkNode(OR, g.negate(), enum_lems[k]);
+          d_qim.addPendingLemma(lem,
+                                InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE);
         }
-        lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
       }
     }
   }
@@ -244,7 +243,14 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
     Node c = candidates[i];
     //build decision tree for candidate
     std::vector<Node> sol;
-    if (d_sygus_unif[c]->constructSolution(sol, lems))
+    std::vector<Node> lems;
+    bool solSuccess = d_sygus_unif[c]->constructSolution(sol, lems);
+    for (const Node& lem : lems)
+    {
+      d_qim.addPendingLemma(lem,
+                            InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL);
+    }
+    if (solSuccess)
     {
       Assert(sol.size() == 1);
       candidate_values.push_back(sol[0]);