From 13819c4ae33a103b1075e816772a305b16db9157 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 22 Feb 2021 17:19:20 -0600 Subject: 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. --- src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers/sygus/sygus_pbe.cpp') 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); -- cgit v1.2.3