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.

28 files changed, 166 insertions, 94 deletions

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 884a7c428..8a787ca2d 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -169,6 +169,35 @@ enum class InferenceId
   DATATYPES_HEIGHT_ZERO,
   // ---------------------------------- end datatypes theory
 
+  //-------------------------------------- quantifiers theory
+  // skolemization
+  QUANTIFIERS_SKOLEMIZE,
+  // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
+  QUANTIFIERS_REDUCE_ALPHA_EQ,
+  //-------------------- counterexample-guided instantiation
+  // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
+  // counterexample literal is G1.
+  QUANTIFIERS_CEGQI_CEX_DEP,
+  // 0 < delta
+  QUANTIFIERS_CEGQI_VTS_LB_DELTA,
+  // delta < c, for positive c
+  QUANTIFIERS_CEGQI_VTS_UB_DELTA,
+  // infinity > c
+  QUANTIFIERS_CEGQI_VTS_LB_INF,
+  //-------------------- sygus solver
+  // preprocessing a sygus conjecture based on quantifier elimination, of the
+  // form Q <=> Q_preprocessed
+  QUANTIFIERS_SYGUS_QE_PREPROC,
+  // G or ~G where G is the active guard for a sygus enumerator
+  QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT,
+  // manual exclusion of a current solution
+  QUANTIFIERS_SYGUS_EXCLUDE_CURRENT,
+  // manual exclusion of a current solution for sygus-stream
+  QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT,
+  // ~Q where Q is a PBE conjecture with conflicting examples
+  QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA,
+  //-------------------------------------- end quantifiers theory
+
   // ---------------------------------- sep theory
   // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
   SEP_PTO_NEG_PROP,
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 442532e82..a79fbb9b6 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe,
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
       d_added_cbqi_lemma(qs.getUserContext()),
-      d_vtsCache(new VtsTermCache(qe)),
+      d_vtsCache(new VtsTermCache(qim)),
       d_bv_invert(nullptr)
 {
   d_small_const =
@@ -147,7 +147,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
         Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;
-        d_quantEngine->getOutputChannel().lemma(dep_lemma);
+        d_qim.lemma(dep_lemma, InferenceId::QUANTIFIERS_CEGQI_CEX_DEP);
       }
 
       //must register all sub-quantifiers of counterexample lemma, register their lemmas
@@ -166,11 +166,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
     DecisionStrategy* dlds = nullptr;
     if (itds == d_dstrat.end())
     {
-      d_dstrat[q].reset(
-          new DecisionStrategySingleton("CexLiteral",
-                                        ceLit,
-                                        d_qstate.getSatContext(),
-                                        d_quantEngine->getValuation()));
+      d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
+                                                      ceLit,
+                                                      d_qstate.getSatContext(),
+                                                      d_qstate.getValuation()));
       dlds = d_dstrat[q].get();
     }
     else
@@ -201,10 +200,12 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
         Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = getCounterexampleLiteral(q);
         bool value;
-        if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
+        if (d_qstate.getValuation().hasSatValue(cel, value))
+        {
           Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
           if( !value ){
-            if( d_quantEngine->getValuation().isDecision( cel ) ){
+            if (d_qstate.getValuation().isDecision(cel))
+            {
               Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
               Trace("cegqi") << "Inactive : " << q << std::endl;
@@ -438,14 +439,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
       if( !delta.isNull() ){
         Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
         Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
-        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+        d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
       }
       std::vector< Node > inf;
       d_vtsCache->getVtsTerms(inf, true, false, false);
       for( unsigned i=0; i<inf.size(); i++ ){
         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
         Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
-        d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
+        d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
       }
     }
   }
@@ -461,7 +462,7 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
   NodeManager * nm = NodeManager::currentNM();
   Node g = nm->mkSkolem("g", nm->booleanType());
   // ensure that it is a SAT literal
-  Node ceLit = d_quantEngine->getValuation().ensureLiteral(g);
+  Node ceLit = d_qstate.getValuation().ensureLiteral(g);
   d_ce_lit[q] = ceLit;
   return ceLit;
 }
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index ecc52e47c..e782a1b6f 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 
 using namespace CVC4::kind;
 
@@ -24,7 +24,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-VtsTermCache::VtsTermCache(QuantifiersEngine* qe) : d_qe(qe)
+VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 }
@@ -66,7 +66,7 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create)
                        nm->realType(),
                        "free delta for virtual term substitution");
       Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
-      d_qe->getOutputChannel().lemma(delta_lem);
+      d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
     }
     if (d_vts_delta.isNull())
     {
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index b9b86dd8b..7b54412c8 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -24,8 +24,6 @@
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
 /** Attribute to mark Skolems as virtual terms */
 struct VirtualTermSkolemAttributeId
 {
@@ -35,6 +33,8 @@ typedef expr::Attribute<VirtualTermSkolemAttributeId, bool>
 
 namespace quantifiers {
 
+class QuantifiersInferenceManager;
+
 /** Virtual term substitution term cache
  *
  * This class stores skolems corresponding to virtual terms (e.g. delta and
@@ -70,7 +70,7 @@ namespace quantifiers {
 class VtsTermCache
 {
  public:
-  VtsTermCache(QuantifiersEngine* qe);
+  VtsTermCache(QuantifiersInferenceManager& qim);
   ~VtsTermCache() {}
   /**
    * Get vts delta. The argument isFree indicates if we are getting the
@@ -122,8 +122,8 @@ class VtsTermCache
   bool containsVtsInfinity(Node n, bool isFree = false);
 
  private:
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** constants */
   Node d_zero;
   /** The virtual term substitution delta */
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 875c74aa4..5df350fe5 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -29,12 +29,13 @@ namespace inst {
 
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
+    quantifiers::QuantifiersState& qs,
     quantifiers::QuantifiersInferenceManager& qim,
     quantifiers::QuantifiersRegistry& qr,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qs, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index af7020bfc..b99a8504d 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -93,6 +93,7 @@ class HigherOrderTrigger : public Trigger
 
  private:
   HigherOrderTrigger(QuantifiersEngine* qe,
+                     quantifiers::QuantifiersState& qs,
                      quantifiers::QuantifiersInferenceManager& qim,
                      quantifiers::QuantifiersRegistry& qr,
                      Node q,
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 2a1e38c3c..e7635f200 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -283,6 +283,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     if (d_is_single_trigger[patTerms[0]])
     {
       tr = Trigger::mkTrigger(d_quantEngine,
+                              d_qstate,
                               d_qim,
                               d_qreg,
                               f,
@@ -321,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       }
       // will possibly want to get an old trigger
       tr = Trigger::mkTrigger(d_quantEngine,
+                              d_qstate,
                               d_qim,
                               d_qreg,
                               f,
@@ -364,6 +366,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         {
           d_single_trigger_gen[patTerms[index]] = true;
           Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
+                                            d_qstate,
                                             d_qim,
                                             d_qreg,
                                             f,
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index ca2f1bdc5..14913bdc1 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -107,6 +107,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     for (size_t i = 0, usize = ugw.size(); i < usize; i++)
     {
       Trigger* t = Trigger::mkTrigger(d_quantEngine,
+                                      d_qstate,
                                       d_qim,
                                       d_qreg,
                                       q,
@@ -170,8 +171,14 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
     d_user_gen_wait[q].push_back(nodes);
     return;
   }
-  Trigger* t = Trigger::mkTrigger(
-      d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW);
+  Trigger* t = Trigger::mkTrigger(d_quantEngine,
+                                  d_qstate,
+                                  d_qim,
+                                  d_qreg,
+                                  q,
+                                  nodes,
+                                  true,
+                                  Trigger::TR_MAKE_NEW);
   if (t)
   {
     d_user_gen[q].push_back(t);
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index d8d3aa098..d57c3356e 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
@@ -35,15 +36,16 @@ namespace inst {
 
 /** trigger class constructor */
 Trigger::Trigger(QuantifiersEngine* qe,
+                 quantifiers::QuantifiersState& qs,
                  quantifiers::QuantifiersInferenceManager& qim,
                  quantifiers::QuantifiersRegistry& qr,
                  Node q,
                  std::vector<Node>& nodes)
-    : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
-  Valuation& val = qe->getValuation();
+  Valuation& val = d_qstate.getValuation();
   for (const Node& n : nodes)
   {
     Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
@@ -114,7 +116,7 @@ uint64_t Trigger::addInstantiations()
   {
     // for each ground term t that does not exist in the equality engine, we
     // add a purification lemma of the form (k = t).
-    eq::EqualityEngine* ee = d_quantEngine->getState().getEqualityEngine();
+    eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
     for (const Node& gt : d_groundTerms)
     {
       if (!ee->hasTerm(gt))
@@ -233,6 +235,7 @@ bool Trigger::mkTriggerTerms(Node q,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersState& qs,
                             quantifiers::QuantifiersInferenceManager& qim,
                             quantifiers::QuantifiersRegistry& qr,
                             Node f,
@@ -275,11 +278,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   Trigger* t;
   if (!ho_apps.empty())
   {
-    t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps);
+    t = new HigherOrderTrigger(qe, qs, qim, qr, f, trNodes, ho_apps);
   }
   else
   {
-    t = new Trigger(qe, qim, qr, f, trNodes);
+    t = new Trigger(qe, qs, qim, qr, f, trNodes);
   }
 
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
@@ -287,6 +290,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 }
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersState& qs,
                             quantifiers::QuantifiersInferenceManager& qim,
                             quantifiers::QuantifiersRegistry& qr,
                             Node f,
@@ -297,7 +301,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 {
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars);
+  return mkTrigger(qe, qs, qim, qr, f, nodes, keepAll, trOption, useNVars);
 }
 
 int Trigger::getActiveScore() {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 21888ff8f..014cf2185 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -30,6 +30,7 @@ namespace theory {
 class QuantifiersEngine;
 
 namespace quantifiers {
+class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
 }
@@ -163,6 +164,7 @@ class Trigger {
     TR_RETURN_NULL  //return null if a duplicate is found
   };
   static Trigger* mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersState& qs,
                             quantifiers::QuantifiersInferenceManager& qim,
                             quantifiers::QuantifiersRegistry& qr,
                             Node q,
@@ -172,6 +174,7 @@ class Trigger {
                             size_t useNVars = 0);
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
+                            quantifiers::QuantifiersState& qs,
                             quantifiers::QuantifiersInferenceManager& qim,
                             quantifiers::QuantifiersRegistry& qr,
                             Node q,
@@ -196,6 +199,7 @@ class Trigger {
  protected:
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
   Trigger(QuantifiersEngine* ie,
+          quantifiers::QuantifiersState& qs,
           quantifiers::QuantifiersInferenceManager& qim,
           quantifiers::QuantifiersRegistry& qr,
           Node q,
@@ -245,6 +249,8 @@ class Trigger {
   std::vector<Node> d_groundTerms;
   /** The quantifiers engine associated with this trigger. */
   QuantifiersEngine* d_quantEngine;
+  /** Reference to the quantifiers state */
+  quantifiers::QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& d_qim;
   /** The quantifiers registry */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index e8b9f5dea..b9a3e1f34 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -498,7 +498,7 @@ void BoundedIntegers::checkOwnership(Node f)
                 new IntRangeDecisionHeuristic(r,
                                               d_qstate.getSatContext(),
                                               d_qstate.getUserContext(),
-                                              d_quantEngine->getValuation(),
+                                              d_qstate.getValuation(),
                                               isProxy));
             d_quantEngine->getTheoryEngine()
                 ->getDecisionManager()
@@ -726,7 +726,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem);
+      d_qim.lemma(lem, InferenceId::UNKNOWN);
     }
     return false;
   }else{
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 232499fbf..cc7f24a12 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -100,7 +100,7 @@ bool Instantiate::addInstantiation(
     Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
 {
   // For resource-limiting (also does a time check).
-  d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep);
+  d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
   Assert(!d_qstate.isInConflict());
   Assert(terms.size() == q[0].getNumChildren());
   Assert(d_term_db != nullptr);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index c09c78158..a97888d36 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -30,8 +30,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
-    : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false)
+Cegis::Cegis(QuantifiersEngine* qe,
+             QuantifiersInferenceManager& qim,
+             SynthConjecture* p)
+    : SygusModule(qe, qim, p), d_eval_unfold(nullptr), d_usingSymCons(false)
 {
   d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
 }
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index c466afe0f..c1415d92f 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -41,7 +41,9 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersEngine* qe, SynthConjecture* p);
+  Cegis(QuantifiersEngine* qe,
+        QuantifiersInferenceManager& qim,
+        SynthConjecture* p);
   ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node conj,
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 4549a0945..db2a972d5 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -69,8 +69,9 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
 }
 
 CegisCoreConnective::CegisCoreConnective(QuantifiersEngine* qe,
+                                         QuantifiersInferenceManager& qim,
                                          SynthConjecture* p)
-    : Cegis(qe, p)
+    : Cegis(qe, qim, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index d70624f0a..cdc43658d 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -155,7 +155,9 @@ class VariadicTrie
 class CegisCoreConnective : public Cegis
 {
  public:
-  CegisCoreConnective(QuantifiersEngine* qe, SynthConjecture* p);
+  CegisCoreConnective(QuantifiersEngine* qe,
+                      QuantifiersInferenceManager& qim,
+                      SynthConjecture* p);
   ~CegisCoreConnective() {}
   /**
    * Return whether this module has the possibility to construct solutions. This
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 239fa3c94..c548f7f8f 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -30,8 +30,9 @@ namespace quantifiers {
 
 CegisUnif::CegisUnif(QuantifiersEngine* qe,
                      QuantifiersState& qs,
+                     QuantifiersInferenceManager& qim,
                      SynthConjecture* p)
-    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, p)
+    : Cegis(qe, qim, p), d_sygus_unif(p), d_u_enum_manager(qe, qs, qim, p)
 {
 }
 
@@ -216,7 +217,7 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums,
                     << "CegisUnif::lemma, inter-unif-enumerator "
                        "symmetry breaking lemma : "
                     << slem << "\n";
-                d_qe->getOutputChannel().lemma(slem);
+                d_qim.lemma(slem, InferenceId::UNKNOWN);
                 addedUnifEnumSymBreakLemma = true;
                 break;
               }
@@ -364,7 +365,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums,
   {
     Trace("cegis-unif-lemma")
         << "CegisUnif::lemma, separation lemma : " << lem << "\n";
-    d_qe->getOutputChannel().lemma(lem);
+    d_qim.lemma(lem, InferenceId::UNKNOWN);
   }
   Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
   return false;
@@ -399,9 +400,13 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
 }
 
 CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
-    QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* parent)
-    : DecisionStrategyFmf(qs.getSatContext(), qe->getValuation()),
+    QuantifiersEngine* qe,
+    QuantifiersState& qs,
+    QuantifiersInferenceManager& qim,
+    SynthConjecture* parent)
+    : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
       d_qe(qe),
+      d_qim(qim),
       d_parent(parent)
 {
   d_initialized = false;
@@ -503,7 +508,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       //   G_uq_i => size(ve) >= log_2( i-1 )
       // In other words, if we use i conditions, then we allow terms in our
       // solution whose size is at most log_2(i-1).
-      d_qe->getOutputChannel().lemma(fair_lemma);
+      d_qim.lemma(fair_lemma, InferenceId::UNKNOWN);
     }
   }
 
@@ -611,7 +616,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
     Trace("cegis-unif-enum-lemma")
         << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
         << sym_break_red_ops << "\n";
-    d_qe->getOutputChannel().lemma(sym_break_red_ops);
+    d_qim.lemma(sym_break_red_ops, InferenceId::UNKNOWN);
   }
   // symmetry breaking between enumerators
   if (!si.d_enums[index].empty() && index == 0)
@@ -622,7 +627,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
     Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
     Trace("cegis-unif-enum-lemma")
         << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
-    d_qe->getOutputChannel().lemma(sym_break);
+    d_qim.lemma(sym_break, InferenceId::UNKNOWN);
   }
   // register the enumerator
   si.d_enums[index].push_back(e);
@@ -678,7 +683,7 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
   Node lem = NodeManager::currentNM()->mkNode(OR, disj);
   Trace("cegis-unif-enum-lemma")
       << "CegisUnifEnum::lemma, domain:" << lem << "\n";
-  d_qe->getOutputChannel().lemma(lem);
+  d_qim.lemma(lem, InferenceId::UNKNOWN);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ee9ae0132..9db77fd95 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -49,6 +49,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
  public:
   CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
                                 QuantifiersState& qs,
+                                QuantifiersInferenceManager& qim,
                                 SynthConjecture* parent);
   /** Make the n^th literal of this strategy (G_uq_n).
    *
@@ -101,6 +102,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** reference to the parent conjecture */
@@ -204,7 +207,10 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
 class CegisUnif : public Cegis
 {
  public:
-  CegisUnif(QuantifiersEngine* qe, QuantifiersState& qs, SynthConjecture* p);
+  CegisUnif(QuantifiersEngine* qe,
+            QuantifiersState& qs,
+            QuantifiersInferenceManager& qim,
+            SynthConjecture* p);
   ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 807764230..49a9b1ea0 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -20,8 +20,10 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersEngine* qe, SynthConjecture* p)
-    : d_qe(qe), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
+SygusModule::SygusModule(QuantifiersEngine* qe,
+                         QuantifiersInferenceManager& qim,
+                         SynthConjecture* p)
+    : d_qe(qe), d_qim(qim), d_tds(qe->getTermDatabaseSygus()), d_parent(p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 7eef6c46a..e150e52af 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 
 class SynthConjecture;
 class TermDbSygus;
+class QuantifiersInferenceManager;
 
 /** SygusModule
  *
@@ -53,7 +54,9 @@ class TermDbSygus;
 class SygusModule
 {
  public:
-  SygusModule(QuantifiersEngine* qe, SynthConjecture* p);
+  SygusModule(QuantifiersEngine* qe,
+              QuantifiersInferenceManager& qim,
+              SynthConjecture* p);
   virtual ~SygusModule() {}
   /** initialize
    *
@@ -150,8 +153,10 @@ class SygusModule
  protected:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** sygus term database of d_qe */
-  quantifiers::TermDbSygus* d_tds;
+  TermDbSygus* d_tds;
   /** reference to the parent conjecture */
   SynthConjecture* d_parent;
 };
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);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 1999f82c3..df99bc452 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -86,7 +86,9 @@ class SynthConjecture;
 class SygusPbe : public SygusModule
 {
  public:
-  SygusPbe(QuantifiersEngine* qe, SynthConjecture* p);
+  SygusPbe(QuantifiersEngine* qe,
+           QuantifiersInferenceManager& qim,
+           SynthConjecture* p);
   ~SygusPbe();
 
   /** initialize this class
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 723f11979..0fcba916b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -58,10 +58,10 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(qe)),
       d_exampleInfer(new ExampleInfer(d_tds)),
-      d_ceg_pbe(new SygusPbe(qe, this)),
-      d_ceg_cegis(new Cegis(qe, this)),
-      d_ceg_cegisUnif(new CegisUnif(qe, qs, this)),
-      d_sygus_ccore(new CegisCoreConnective(qe, this)),
+      d_ceg_pbe(new SygusPbe(qe, qim, this)),
+      d_ceg_cegis(new Cegis(qe, qim, this)),
+      d_ceg_cegisUnif(new CegisUnif(qe, qs, qim, this)),
+      d_sygus_ccore(new CegisCoreConnective(qe, qim, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
@@ -102,7 +102,7 @@ void SynthConjecture::assign(Node q)
   // initialize the guard
   d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
   d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
-  d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+  d_feasible_guard = d_qstate.getValuation().ensureLiteral(d_feasible_guard);
   AlwaysAssert(!d_feasible_guard.isNull());
 
   // pre-simplify the quantified formula based on the process utility
@@ -202,7 +202,7 @@ void SynthConjecture::assign(Node q)
   {
     // there is a contradictory example pair, the conjecture is infeasible.
     Node infLem = d_feasible_guard.negate();
-    d_qe->getOutputChannel().lemma(infLem);
+    d_qim.lemma(infLem, InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA);
     // we don't need to continue initialization in this case
     return;
   }
@@ -240,13 +240,13 @@ void SynthConjecture::assign(Node q)
       new DecisionStrategySingleton("sygus_feasible",
                                     d_feasible_guard,
                                     d_qstate.getSatContext(),
-                                    d_qe->getValuation()));
+                                    d_qstate.getValuation()));
   d_qe->getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
   // this must be called, both to ensure that the feasible guard is
   // decided on with true polariy, but also to ensure that output channel
   // has been used on this call to check.
-  d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
+  d_qim.requirePhase(d_feasible_guard, true);
 
   Node gneg = d_feasible_guard.negate();
   for (unsigned i = 0; i < guarded_lemmas.size(); i++)
@@ -254,7 +254,7 @@ void SynthConjecture::assign(Node q)
     Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
     Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem
                          << std::endl;
-    d_qe->getOutputChannel().lemma(lem);
+    d_qim.lemma(lem, InferenceId::UNKNOWN);
   }
 
   Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation()
@@ -273,7 +273,7 @@ bool SynthConjecture::needsCheck()
   bool value;
   Assert(!d_feasible_guard.isNull());
   // non or fully single invocation : look at guard only
-  if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
+  if (d_qstate.getValuation().hasSatValue(d_feasible_guard, value))
   {
     if (!value)
     {
@@ -610,7 +610,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       // We should set incomplete, since a "sat" answer should not be
       // interpreted as "infeasible", which would make a difference in the rare
       // case where e.g. we had a finite grammar and exhausted the grammar.
-      d_qe->getOutputChannel().setIncomplete();
+      d_qim.setIncomplete();
       return false;
     }
     // otherwise we are unsat, and we will process the solution below
@@ -780,7 +780,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
     Node g = d_tds->getActiveGuardForEnumerator(e);
     if (!g.isNull())
     {
-      Node gstatus = d_qe->getValuation().getSatValue(g);
+      Node gstatus = d_qstate.getValuation().getSatValue(g);
       if (gstatus.isNull() || !gstatus.getConst<bool>())
       {
         Trace("sygus-engine-debug")
@@ -936,7 +936,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
       TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
       Trace("sygus-active-gen-debug") << std::endl;
     }
-    d_qe->getOutputChannel().lemma(lem);
+    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT);
   }
   else
   {
@@ -1024,7 +1024,7 @@ void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums,
     exc_lem = exc_lem.negate();
     Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
                          << exc_lem << std::endl;
-    d_qe->getOutputChannel().lemma(exc_lem);
+    d_qim.lemma(exc_lem, InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT);
   }
 }
 
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 3aa782272..9653c4c9d 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -94,7 +94,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
   Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
                         << std::endl;
   Trace("sygus-engine-debug") << std::endl;
-  Valuation& valuation = d_quantEngine->getValuation();
+  Valuation& valuation = d_qstate.getValuation();
   std::vector<SynthConjecture*> activeCheckConj;
   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
@@ -151,7 +151,7 @@ void SynthEngine::assignConjecture(Node q)
     {
       Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
                            << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem);
+      d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC);
       // we've reduced the original to a preprocessed version, return
       return;
     }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index e800a52cf..bc5cd1fda 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -564,11 +564,11 @@ void TermDbSygus::registerEnumerator(Node e,
     // make the guard
     Node ag = nm->mkSkolem("eG", nm->booleanType());
     // must ensure it is a literal immediately here
-    ag = d_quantEngine->getValuation().ensureLiteral(ag);
+    ag = d_qstate.getValuation().ensureLiteral(ag);
     // must ensure that it is asserted as a literal before we begin solving
     Node lem = nm->mkNode(OR, ag, ag.negate());
-    d_quantEngine->getOutputChannel().requirePhase(ag, true);
-    d_quantEngine->getOutputChannel().lemma(lem);
+    d_qim.requirePhase(ag, true);
+    d_qim.lemma(lem, InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT);
     d_enum_to_active_guard[e] = ag;
   }
 }
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index e59b788b6..9fdf0aa7f 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -218,11 +218,11 @@ void SygusInst::reset_round(Theory::Effort e)
       Node lit = getCeLiteral(q);
 
       bool value;
-      if (d_quantEngine->getValuation().hasSatValue(lit, value))
+      if (d_qstate.getValuation().hasSatValue(lit, value))
       {
         if (!value)
         {
-          if (!d_quantEngine->getValuation().isDecision(lit))
+          if (!d_qstate.getValuation().isDecision(lit))
           {
             model->setQuantifierActive(q, false);
             d_active_quant.erase(q);
@@ -459,7 +459,7 @@ Node SygusInst::getCeLiteral(Node q)
 
   NodeManager* nm = NodeManager::currentNM();
   Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
-  Node lit = d_quantEngine->getValuation().ensureLiteral(sk);
+  Node lit = d_qstate.getValuation().ensureLiteral(sk);
   d_ce_lits[q] = lit;
   return lit;
 }
@@ -517,11 +517,8 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
    * counterexample literal is decided on first. It is user-context dependent.
    */
   Assert(d_dstrat.find(q) == d_dstrat.end());
-  DecisionStrategy* ds =
-      new DecisionStrategySingleton("CeLiteral",
-                                    lit,
-                                    d_qstate.getSatContext(),
-                                    d_quantEngine->getValuation());
+  DecisionStrategy* ds = new DecisionStrategySingleton(
+      "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
 
   d_dstrat[q].reset(ds);
   d_quantEngine->getDecisionManager()->registerStrategy(
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f9edbda35..ec4cb7905 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -127,12 +127,6 @@ DecisionManager* QuantifiersEngine::getDecisionManager()
   return d_decManager;
 }
 
-OutputChannel& QuantifiersEngine::getOutputChannel()
-{
-  return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
-}
-Valuation& QuantifiersEngine::getValuation() { return d_qstate.getValuation(); }
-
 quantifiers::QuantifiersState& QuantifiersEngine::getState()
 {
   return d_qstate;
@@ -591,7 +585,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   {
     if( setIncomplete ){
       Trace("quant-engine") << "Set incomplete flag." << std::endl;
-      getOutputChannel().setIncomplete();
+      d_qim.setIncomplete();
     }
     //output debug stats
     d_instantiate->debugPrintModel();
@@ -609,6 +603,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
   BoolMap::const_iterator it = d_quants_red.find( q );
   if( it==d_quants_red.end() ){
     Node lem;
+    InferenceId id = InferenceId::UNKNOWN;
     std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
     if( itr==d_quants_red_lem.end() ){
       if (d_qmodules->d_alpha_equiv)
@@ -616,6 +611,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
         Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
         //add equivalence with another quantified formula
         lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
+        id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
         if( !lem.isNull() ){
           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
           ++(d_statistics.d_red_alpha_equiv);
@@ -626,7 +622,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
       lem = itr->second;
     }
     if( !lem.isNull() ){
-      getOutputChannel().lemma( lem );
+      d_qim.lemma(lem, id);
     }
     d_quants_red[q] = !lem.isNull();
     return !lem.isNull();
@@ -721,7 +717,9 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
         Trace("quantifiers-sk-debug")
             << "Skolemize lemma : " << slem << std::endl;
       }
-      getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY);
+      d_qim.trustedLemma(lem,
+                         InferenceId::QUANTIFIERS_SKOLEMIZE,
+                         LemmaProperty::NEEDS_JUSTIFY);
     }
     return;
   }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f01158ee2..c8f9cd6ad 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -69,10 +69,6 @@ class QuantifiersEngine {
   TheoryEngine* getTheoryEngine() const;
   /** Get the decision manager */
   DecisionManager* getDecisionManager();
-  /** get default output channel for the quantifiers engine */
-  OutputChannel& getOutputChannel();
-  /** get default valuation for the quantifiers engine */
-  Valuation& getValuation();
   /** The quantifiers state object */
   quantifiers::QuantifiersState& getState();
   /** The quantifiers inference manager */