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, 6 insertions, 0 deletions

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 */