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, 29 insertions, 0 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,