From 8c11c5b2683aa13160447aef302d82115a08081a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 16 Mar 2021 14:14:33 -0500
Subject: Further standardization of strings statistics (#6128)

Also eliminates use of raw output channel in strings.
---
 src/theory/inference_id.h | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'src/theory/inference_id.h')

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index b6d0d3c25..4af7761a0 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -384,7 +384,6 @@ enum class InferenceId
   STRINGS_CARD_SP,
   // The cardinality inference for strings, see Liang et al CAV 2014.
   STRINGS_CARDINALITY,
-  //-------------------- end base solver
   //-------------------- core solver
   // A cycle in the empty string equivalence class, e.g.:
   //   x ++ y = "" => x = ""
@@ -522,14 +521,12 @@ enum class InferenceId
   // is unknown, we apply the inference:
   //   len(s) != len(t) V len(s) = len(t)
   STRINGS_DEQ_LENGTH_SP,
-  //-------------------- end core solver
   //-------------------- codes solver
   // str.to_code( v ) = rewrite( str.to_code(c) )
   // where v is the proxy variable for c.
   STRINGS_CODE_PROXY,
   // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
   STRINGS_CODE_INJ,
-  //-------------------- end codes solver
   //-------------------- regexp solver
   // regular expression normal form conflict
   //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
@@ -565,7 +562,6 @@ enum class InferenceId
   STRINGS_RE_DELTA_CONF,
   // regular expression derive ???
   STRINGS_RE_DERIVE,
-  //-------------------- end regexp solver
   //-------------------- extended function solver
   // Standard extended function inferences from context-dependent rewriting
   // produced by constant substitutions. See Reynolds et al CAV 2017. These are
@@ -611,11 +607,16 @@ enum class InferenceId
   // f(x1, .., xn) and P is the reduction predicate for f
   // (see theory_strings_preprocess).
   STRINGS_REDUCTION,
-  //-------------------- end extended function solver
   //-------------------- prefix conflict
   // prefix conflict (coarse-grained)
   STRINGS_PREFIX_CONFLICT,
-  //-------------------- end prefix conflict
+  //-------------------- other
+  // a lemma added during term registration for an atomic term
+  STRINGS_REGISTER_TERM_ATOMIC,
+  // a lemma added during term registration
+  STRINGS_REGISTER_TERM,
+  // a split during collect model info
+  STRINGS_CMI_SPLIT,
   //-------------------------------------- end strings theory
 
   //-------------------------------------- uf theory
-- 
cgit v1.2.3