Eliminate raw use of output channel and valuation in quantifiers (#5933)

This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index b1cb330f6..da7c0d6d4 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -28,8 +28,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusPbe::SygusPbe(QuantifiersEngine* qe, SynthConjecture* p)
-    : SygusModule(qe, p)
+SygusPbe::SygusPbe(QuantifiersEngine* qe,
+                   QuantifiersInferenceManager& qim,
+                   SynthConjecture* p)
+    : SygusModule(qe, qim, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);