src/theory/inference_id.h

   1 /*********************                                                        */
   2 /*! \file inference_id.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Gereon Kremer, Yoni Zohar
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Inference enumeration.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__INFERENCE_ID_H
  18 #define CVC4__THEORY__INFERENCE_ID_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "util/safe_print.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /** Types of inferences used in the procedure
  29  *
  30  * Note: The order in this enum matters in certain cases (e.g. inferences
  31  * related to normal forms in strings), where inferences that come first are
  32  * generally preferred.
  33  *
  34  * Notice that an inference is intentionally distinct from PfRule. An
  35  * inference captures *why* we performed a reasoning step, and a PfRule
  36  * rule captures *what* reasoning step was used. For instance, the inference
  37  * LEN_SPLIT translates to PfRule::SPLIT. The use of stats on inferences allows
  38  * us to know that we performed N splits (PfRule::SPLIT) because we wanted
  39  * to split on lengths for string equalities (Inference::LEN_SPLIT).
  40  */
  41 enum class InferenceId
  42 {
  43   // ---------------------------------- arith theory
  44   //-------------------- preprocessing
  45   ARITH_PP_ELIM_OPERATORS,
  46   //-------------------- nonlinear core
  47   // simple congruence x=y => f(x)=f(y)
  48   ARITH_NL_CONGRUENCE,
  49   // shared term value split (for naive theory combination)
  50   ARITH_NL_SHARED_TERM_VALUE_SPLIT,
  51   // checkModel found a conflict with a quadratic equality
  52   ARITH_NL_CM_QUADRATIC_EQ,
  53   //-------------------- nonlinear incremental linearization solver
  54   // splitting on zero (NlSolver::checkSplitZero)
  55   ARITH_NL_SPLIT_ZERO,
  56   // based on sign (NlSolver::checkMonomialSign)
  57   ARITH_NL_SIGN,
  58   // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
  59   ARITH_NL_COMPARISON,
  60   // based on inferring bounds (NlSolver::checkMonomialInferBounds)
  61   ARITH_NL_INFER_BOUNDS,
  62   // same as above, for inferences that introduce new terms
  63   ARITH_NL_INFER_BOUNDS_NT,
  64   // factoring (NlSolver::checkFactoring)
  65   ARITH_NL_FACTOR,
  66   // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
  67   ARITH_NL_RES_INFER_BOUNDS,
  68   // tangent planes (NlSolver::checkTangentPlanes)
  69   ARITH_NL_TANGENT_PLANE,
  70   //-------------------- nonlinear transcendental solver
  71   // purification of arguments to transcendental functions
  72   ARITH_NL_T_PURIFY_ARG,
  73   // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
  74   ARITH_NL_T_INIT_REFINE,
  75   // pi bounds
  76   ARITH_NL_T_PI_BOUND,
  77   // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
  78   ARITH_NL_T_MONOTONICITY,
  79   // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
  80   ARITH_NL_T_TANGENT,
  81   // secant refinement, the dual of the above inference
  82   ARITH_NL_T_SECANT,
  83   //-------------------- nonlinear iand solver
  84   // initial refinements (IAndSolver::checkInitialRefine)
  85   ARITH_NL_IAND_INIT_REFINE,
  86   // value refinements (IAndSolver::checkFullRefine)
  87   ARITH_NL_IAND_VALUE_REFINE,
  88   // sum refinements (IAndSolver::checkFullRefine)
  89   ARITH_NL_IAND_SUM_REFINE,
  90   // bitwise refinements (IAndSolver::checkFullRefine)
  91   ARITH_NL_IAND_BITWISE_REFINE,
  92   //-------------------- nonlinear cad solver
  93   // conflict / infeasible subset obtained from cad
  94   ARITH_NL_CAD_CONFLICT,
  95   // excludes an interval for a single variable
  96   ARITH_NL_CAD_EXCLUDED_INTERVAL,
  97   //-------------------- nonlinear icp solver
  98   // conflict obtained from icp
  99   ARITH_NL_ICP_CONFLICT,
 100   // propagation / contraction of variable bounds from icp
 101   ARITH_NL_ICP_PROPAGATION,
 102   // ---------------------------------- end arith theory
 103
 104   // ---------------------------------- arrays theory
 105   ARRAYS_EXT,
 106   ARRAYS_READ_OVER_WRITE,
 107   ARRAYS_READ_OVER_WRITE_1,
 108   ARRAYS_READ_OVER_WRITE_CONTRA,
 109   // ---------------------------------- end arrays theory
 110
 111   // ---------------------------------- bags theory
 112   BAG_NON_NEGATIVE_COUNT,
 113   BAG_MK_BAG_SAME_ELEMENT,
 114   BAG_MK_BAG,
 115   BAG_EQUALITY,
 116   BAG_DISEQUALITY,
 117   BAG_EMPTY,
 118   BAG_UNION_DISJOINT,
 119   BAG_UNION_MAX,
 120   BAG_INTERSECTION_MIN,
 121   BAG_DIFFERENCE_SUBTRACT,
 122   BAG_DIFFERENCE_REMOVE,
 123   BAG_DUPLICATE_REMOVAL,
 124   // ---------------------------------- end bags theory
 125
 126   // ---------------------------------- bitvector theory
 127   BV_BITBLAST_CONFLICT,
 128   BV_LAZY_CONFLICT,
 129   BV_LAZY_LEMMA,
 130   BV_SIMPLE_LEMMA,
 131   BV_SIMPLE_BITBLAST_LEMMA,
 132   BV_EXTF_LEMMA,
 133   BV_EXTF_COLLAPSE,
 134   // ---------------------------------- end bitvector theory
 135
 136   // ---------------------------------- datatypes theory
 137   // (= k t) for fresh k
 138   DATATYPES_PURIFY,
 139   // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
 140   DATATYPES_UNIF,
 141   // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))
 142   DATATYPES_INST,
 143   // (or ((_ is C1) t) V ... V ((_ is Cn) t))
 144   DATATYPES_SPLIT,
 145   // (or ((_ is Ci) t) V (not ((_ is Ci) t)))
 146   DATATYPES_BINARY_SPLIT,
 147   // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
 148   DATATYPES_LABEL_EXH,
 149   // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
 150   DATATYPES_COLLAPSE_SEL,
 151   // (= (Ci t1...tn) (Cj t1...tn)) => false
 152   DATATYPES_CLASH_CONFLICT,
 153   // ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false
 154   DATATYPES_TESTER_CONFLICT,
 155   // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false
 156   DATATYPES_TESTER_MERGE_CONFLICT,
 157   // bisimilarity for codatatypes
 158   DATATYPES_BISIMILAR,
 159   // corecursive singleton equality
 160   DATATYPES_REC_SINGLETON_EQ,
 161   // corecursive singleton equality (not (= k1 k2)) for fresh k1, k2
 162   DATATYPES_REC_SINGLETON_FORCE_DEQ,
 163   // cycle conflict for datatypes
 164   DATATYPES_CYCLE,
 165   //-------------------- datatypes size/height
 166   // (>= (dt.size t) 0)
 167   DATATYPES_SIZE_POS,
 168   // (=> (= (dt.height t) 0) => (and (= (dt.height (sel_1 t)) 0) .... ))
 169   DATATYPES_HEIGHT_ZERO,
 170   // ---------------------------------- end datatypes theory
 171
 172   // ---------------------------------- sep theory
 173   // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
 174   SEP_PTO_NEG_PROP,
 175   // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
 176   SEP_PTO_PROP,
 177   // ---------------------------------- end sep theory
 178
 179   // ---------------------------------- sets theory
 180   //-------------------- sets core solver
 181   SETS_COMPREHENSION,
 182   SETS_DEQ,
 183   SETS_DOWN_CLOSURE,
 184   SETS_EQ_MEM,
 185   SETS_EQ_MEM_CONFLICT,
 186   SETS_MEM_EQ,
 187   SETS_MEM_EQ_CONFLICT,
 188   SETS_PROXY,
 189   SETS_PROXY_SINGLETON,
 190   SETS_SINGLETON_EQ,
 191   SETS_UP_CLOSURE,
 192   SETS_UP_CLOSURE_2,
 193   SETS_UP_UNIV,
 194   SETS_UNIV_TYPE,
 195   //-------------------- sets cardinality solver
 196   // cycle of cardinalities, hence all sets have the same
 197   SETS_CARD_CYCLE,
 198   // two sets have the same cardinality
 199   SETS_CARD_EQUAL,
 200   SETS_CARD_GRAPH_EMP,
 201   SETS_CARD_GRAPH_EMP_PARENT,
 202   SETS_CARD_GRAPH_EQ_PARENT,
 203   SETS_CARD_GRAPH_EQ_PARENT_2,
 204   SETS_CARD_GRAPH_PARENT_SINGLETON,
 205   // cardinality is at least the number of elements we already know
 206   SETS_CARD_MINIMAL,
 207   // negative members are part of the universe
 208   SETS_CARD_NEGATIVE_MEMBER,
 209   // all sets have non-negative cardinality
 210   SETS_CARD_POSITIVE,
 211   // the universe is a superset of every set
 212   SETS_CARD_UNIV_SUPERSET,
 213   // cardinality of the universe is at most cardinality of the type
 214   SETS_CARD_UNIV_TYPE,
 215   //-------------------- sets relations solver
 216   SETS_RELS_IDENTITY_DOWN,
 217   SETS_RELS_IDENTITY_UP,
 218   SETS_RELS_JOIN_COMPOSE,
 219   SETS_RELS_JOIN_IMAGE_DOWN,
 220   SETS_RELS_JOIN_SPLIT_1,
 221   SETS_RELS_JOIN_SPLIT_2,
 222   SETS_RELS_PRODUCE_COMPOSE,
 223   SETS_RELS_PRODUCT_SPLIT,
 224   SETS_RELS_TCLOSURE_FWD,
 225   SETS_RELS_TRANSPOSE_EQ,
 226   SETS_RELS_TRANSPOSE_REV,
 227   SETS_RELS_TUPLE_REDUCTION,
 228   //-------------------------------------- end sets theory
 229
 230   //-------------------------------------- strings theory
 231   //-------------------- base solver
 232   // initial normalize singular
 233   //   x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
 234   //   x1 ++ ... ++ xn = xi
 235   STRINGS_I_NORM_S,
 236   // initial constant merge
 237   //   explain_constant(x, c) => x = c
 238   // Above, explain_constant(x,c) is a basic explanation of why x must be equal
 239   // to string constant c, which is computed by taking arguments of
 240   // concatenation terms that are entailed to be constants. For example:
 241   //  ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
 242   STRINGS_I_CONST_MERGE,
 243   // initial constant conflict
 244   //    ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
 245   // where c1 != c2.
 246   STRINGS_I_CONST_CONFLICT,
 247   // initial normalize
 248   // Given two concatenation terms, this is applied when we find that they are
 249   // equal after e.g. removing strings that are currently empty. For example:
 250   //   y = "" ^ z = "" => x ++ y = z ++ x
 251   STRINGS_I_NORM,
 252   // injectivity of seq.unit
 253   // (seq.unit x) = (seq.unit y) => x=y, or
 254   // (seq.unit x) = (seq.unit c) => x=c
 255   STRINGS_UNIT_INJ,
 256   // unit constant conflict
 257   // (seq.unit x) = C => false if |C| != 1.
 258   STRINGS_UNIT_CONST_CONFLICT,
 259   // injectivity of seq.unit for disequality
 260   // (seq.unit x) != (seq.unit y) => x != y, or
 261   // (seq.unit x) != (seq.unit c) => x != c
 262   STRINGS_UNIT_INJ_DEQ,
 263   // A split due to cardinality
 264   STRINGS_CARD_SP,
 265   // The cardinality inference for strings, see Liang et al CAV 2014.
 266   STRINGS_CARDINALITY,
 267   //-------------------- end base solver
 268   //-------------------- core solver
 269   // A cycle in the empty string equivalence class, e.g.:
 270   //   x ++ y = "" => x = ""
 271   // This is typically not applied due to length constraints implying emptiness.
 272   STRINGS_I_CYCLE_E,
 273   // A cycle in the containment ordering.
 274   //   x = y ++ x => y = "" or
 275   //   x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
 276   // This is typically not applied due to length constraints implying emptiness.
 277   STRINGS_I_CYCLE,
 278   // Flat form constant
 279   //   x = y ^ x = z ++ c ... ^ y = z ++ d => false
 280   // where c and d are distinct constants.
 281   STRINGS_F_CONST,
 282   // Flat form unify
 283   //   x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
 284   // Notice flat form instances are similar to normal form inferences but do
 285   // not involve recursive explanations.
 286   STRINGS_F_UNIFY,
 287   // Flat form endpoint empty
 288   //   x = y ^ x = z ^ y = z ++ y' => y' = ""
 289   STRINGS_F_ENDPOINT_EMP,
 290   // Flat form endpoint equal
 291   //   x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
 292   STRINGS_F_ENDPOINT_EQ,
 293   // Flat form not contained
 294   // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
 295   STRINGS_F_NCTN,
 296   // Normal form equality conflict
 297   //   x = N[x] ^ y = N[y] ^ x=y => false
 298   // where Rewriter::rewrite(N[x]=N[y]) = false.
 299   STRINGS_N_EQ_CONF,
 300   // Given two normal forms, infers that the remainder one of them has to be
 301   // empty. For example:
 302   //    If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
 303   STRINGS_N_ENDPOINT_EMP,
 304   // Given two normal forms, infers that two components have to be the same if
 305   // they have the same length. For example:
 306   //   If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
 307   STRINGS_N_UNIFY,
 308   // Given two normal forms, infers that the endpoints have to be the same. For
 309   // example:
 310   //   If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
 311   STRINGS_N_ENDPOINT_EQ,
 312   // Given two normal forms with constant endpoints, infers a conflict if the
 313   // endpoints do not agree. For example:
 314   //   If "abc" ++ ... = "bc" ++ ... then conflict
 315   STRINGS_N_CONST,
 316   // infer empty, for example:
 317   //     (~) x = ""
 318   // This is inferred when we encounter an x such that x = "" rewrites to a
 319   // constant. This inference is used for instance when we otherwise would have
 320   // split on the emptiness of x but the rewriter tells us the emptiness of x
 321   // can be inferred.
 322   STRINGS_INFER_EMP,
 323   // string split constant propagation, for example:
 324   //     x = y, x = "abc", y = y1 ++ "b" ++ y2
 325   //       implies y1 = "a" ++ y1'
 326   STRINGS_SSPLIT_CST_PROP,
 327   // string split variable propagation, for example:
 328   //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
 329   //       implies x1 = y1 ++ x1'
 330   // This is inspired by Zheng et al CAV 2015.
 331   STRINGS_SSPLIT_VAR_PROP,
 332   // length split, for example:
 333   //     len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
 334   // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
 335   STRINGS_LEN_SPLIT,
 336   // length split empty, for example:
 337   //     z = "" V z != ""
 338   // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
 339   STRINGS_LEN_SPLIT_EMP,
 340   // string split constant
 341   //    x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
 342   //      implies y1 = "c" ++ y1'
 343   // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
 344   STRINGS_SSPLIT_CST,
 345   // string split variable, for example:
 346   //    x = y, x = x1 ++ x2, y = y1 ++ y2
 347   //      implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
 348   // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
 349   STRINGS_SSPLIT_VAR,
 350   // flat form loop, for example:
 351   //    x = y, x = x1 ++ z, y = z ++ y2
 352   //      implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
 353   //        for fresh u, u1, u2.
 354   // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
 355   STRINGS_FLOOP,
 356   // loop conflict ???
 357   STRINGS_FLOOP_CONFLICT,
 358   // Normal form inference
 359   // x = y ^ z = y => x = z
 360   // This is applied when y is the normal form of both x and z.
 361   STRINGS_NORMAL_FORM,
 362   // Normal form not contained, same as FFROM_NCTN but for normal forms
 363   STRINGS_N_NCTN,
 364   // Length normalization
 365   //   x = y => len( x ) = len( y )
 366   // Typically applied when y is the normal form of x.
 367   STRINGS_LEN_NORM,
 368   // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
 369   // inference:
 370   //   x = "" v x != ""
 371   STRINGS_DEQ_DISL_EMP_SPLIT,
 372   // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1, we apply the
 373   // inference:
 374   //   x = "a" v x != "a"
 375   STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT,
 376   // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != "", we apply the
 377   // inference:
 378   //   ni = x ++ x' ++ ... ^ nj = "abc" ++ y' ++ ... ^ x != "" --->
 379   //     x = k1 ++ k2 ^ len(k1) = 1 ^ (k1 != "a" v x = "a" ++  k2)
 380   STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT,
 381   // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y), we apply the
 382   // inference:
 383   //   ni = x ++ x' ++ ... ^ nj = y ++ y' ++ ... ^ ni != nj ^ len(x) != len(y)
 384   //     --->
 385   //       len(k1) = len(x) ^ len(k2) = len(y) ^ (y = k1 ++ k3 v x = k1 ++ k2)
 386   STRINGS_DEQ_DISL_STRINGS_SPLIT,
 387   // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y), we apply the
 388   // inference:
 389   //   x = y v x != y
 390   STRINGS_DEQ_STRINGS_EQ,
 391   // When x ++ x' ++ ... != y ++ y' ++ ... and we do not know how the lengths
 392   // of x and y compare, we apply the inference:
 393   //   len(x) = len(y) v len(x) != len(y)
 394   STRINGS_DEQ_LENS_EQ,
 395   // When px ++ x ++ ... != py ^ len(px ++ x ++ ...) = len(py), we apply the
 396   // following inference that infers that the remainder of the longer normal
 397   // form must be empty:
 398   //   ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
 399   //     x = "" ^ ...
 400   STRINGS_DEQ_NORM_EMP,
 401   // When two strings are disequal s != t and the comparison of their lengths
 402   // is unknown, we apply the inference:
 403   //   len(s) != len(t) V len(s) = len(t)
 404   STRINGS_DEQ_LENGTH_SP,
 405   //-------------------- end core solver
 406   //-------------------- codes solver
 407   // str.to_code( v ) = rewrite( str.to_code(c) )
 408   // where v is the proxy variable for c.
 409   STRINGS_CODE_PROXY,
 410   // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
 411   STRINGS_CODE_INJ,
 412   //-------------------- end codes solver
 413   //-------------------- regexp solver
 414   // regular expression normal form conflict
 415   //   ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
 416   // where y is the normal form computed for x.
 417   STRINGS_RE_NF_CONFLICT,
 418   // regular expression unfolding
 419   // This is a general class of inferences of the form:
 420   //   (x in R) => F
 421   // where F is formula expressing the next step of checking whether x is in
 422   // R.  For example:
 423   //   (x in (R)*) =>
 424   //   x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
 425   STRINGS_RE_UNFOLD_POS,
 426   // Same as above, for negative memberships
 427   STRINGS_RE_UNFOLD_NEG,
 428   // intersection inclusion conflict
 429   //   (x in R1 ^ ~ x in R2) => false  where [[includes(R2,R1)]]
 430   // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
 431   STRINGS_RE_INTER_INCLUDE,
 432   // intersection conflict, using regexp intersection computation
 433   //   (x in R1 ^ x in R2) => false   where [[intersect(R1, R2) = empty]]
 434   STRINGS_RE_INTER_CONF,
 435   // intersection inference
 436   //   (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
 437   STRINGS_RE_INTER_INFER,
 438   // regular expression delta
 439   //   (x = "" ^ x in R) => C
 440   // where "" in R holds if and only if C holds.
 441   STRINGS_RE_DELTA,
 442   // regular expression delta conflict
 443   //   (x = "" ^ x in R) => false
 444   // where R does not accept the empty string.
 445   STRINGS_RE_DELTA_CONF,
 446   // regular expression derive ???
 447   STRINGS_RE_DERIVE,
 448   //-------------------- end regexp solver
 449   //-------------------- extended function solver
 450   // Standard extended function inferences from context-dependent rewriting
 451   // produced by constant substitutions. See Reynolds et al CAV 2017. These are
 452   // inferences of the form:
 453   //   X = Y => f(X) = t   when   rewrite( f(Y) ) = t
 454   // where X = Y is a vector of equalities, where some of Y may be constants.
 455   STRINGS_EXTF,
 456   // Same as above, for normal form substitutions.
 457   STRINGS_EXTF_N,
 458   // Decompositions based on extended function inferences from context-dependent
 459   // rewriting produced by constant substitutions. This is like the above, but
 460   // handles cases where the inferred predicate is not necessarily an equality
 461   // involving f(X). For example:
 462   //   x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
 463   // This is generally only inferred if contains( y, "B" ) is a known term in
 464   // the current context.
 465   STRINGS_EXTF_D,
 466   // Same as above, for normal form substitutions.
 467   STRINGS_EXTF_D_N,
 468   // Extended function equality rewrite. This is an inference of the form:
 469   //   t = s => P
 470   // where P is a predicate implied by rewrite( t = s ).
 471   // Typically, t is an application of an extended function and s is a constant.
 472   // It is generally only inferred if P is a predicate over known terms.
 473   STRINGS_EXTF_EQ_REW,
 474   // contain transitive
 475   //   ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
 476   STRINGS_CTN_TRANS,
 477   // contain decompose
 478   //  str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
 479   //  ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
 480   STRINGS_CTN_DECOMPOSE,
 481   // contain neg equal
 482   //   ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
 483   STRINGS_CTN_NEG_EQUAL,
 484   // contain positive
 485   //   str.contains( x, y ) => x = w1 ++ y ++ w2
 486   // where w1 and w2 are skolem variables.
 487   STRINGS_CTN_POS,
 488   // All reduction inferences of the form:
 489   //   f(x1, .., xn) = y ^ P(x1, ..., xn, y)
 490   // where f is an extended function, y is the purification variable for
 491   // f(x1, .., xn) and P is the reduction predicate for f
 492   // (see theory_strings_preprocess).
 493   STRINGS_REDUCTION,
 494   //-------------------- end extended function solver
 495   //-------------------- prefix conflict
 496   // prefix conflict (coarse-grained)
 497   STRINGS_PREFIX_CONFLICT,
 498   //-------------------- end prefix conflict
 499   //-------------------------------------- end strings theory
 500
 501   //-------------------------------------- uf theory
 502   // Clause from the uf symmetry breaker
 503   UF_BREAK_SYMMETRY,
 504   //-------------------- cardinality extension to UF
 505   // The inferences below are described in Reynolds' thesis 2013.
 506   // conflict of the form (card_T n) => (not (distinct t1 ... tn))
 507   UF_CARD_CLIQUE,
 508   // conflict of the form (not (card_T1 n1)) ^ ... (not (card_Tk nk)) ^ (card n)
 509   // where n1 + ... + nk >= n, where (card n) is a combined cardinality
 510   // constraint.
 511   UF_CARD_COMBINED,
 512   // (not (card_T n)) => (distinct t1 ... tn)
 513   UF_CARD_ENFORCE_NEGATIVE,
 514   // used to make the index terms in cardinality constraints equal
 515   UF_CARD_EQUIV,
 516   // conflict of the form (not (card_T1 n)) ^ (card_T2 m) where the cardinality
 517   // of T2 can be assumed to be without loss of generality larger than T1 due to
 518   // monotonicity reasoning (Claessen et al 2011).
 519   UF_CARD_MONOTONE_COMBINED,
 520   // conflict of the form (not (card_T n)) ^ (card_T m) where n>m
 521   UF_CARD_SIMPLE_CONFLICT,
 522   // equality split requested by cardinality solver
 523   //  (or (= t1 t2) (not (= t1 t2))
 524   // to satisfy the cardinality constraints on the type of t1, t2.
 525   UF_CARD_SPLIT,
 526   //-------------------- end cardinality extension to UF
 527   //-------------------- HO extension to UF
 528   // Encodes an n-ary application as a chain of binary HO_APPLY applications
 529   //   (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
 530   UF_HO_APP_ENCODE,
 531   // A lemma corresponding to the definition of a skolem k used to convert
 532   // HO_APPLY terms to APPLY_UF terms. This is of the form:
 533   //   (forall x1 ... xn) (@ (@ k x1) ... xn) = t
 534   // where notice that t is a function whose free variables (if any) are
 535   // x1 ... xn.
 536   UF_HO_APP_CONV_SKOLEM,
 537   // Adds an extensionality lemma to witness that disequal functions have
 538   // different applications
 539   //   (not (= (f sk1 .. skn) (g sk1 .. skn))
 540   UF_HO_EXTENSIONALITY,
 541   //-------------------- model-construction specific part
 542   // These rules are necessary to ensure that we build models properly. For more
 543   // details see Section 3.3 of Barbosa et al. CADE'19.
 544   //
 545   // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
 546   // equivalent by adding the equality as a lemma
 547   //   (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
 548   UF_HO_MODEL_APP_ENCODE,
 549   // Adds an extensionality lemma to witness that disequal functions have
 550   // different applications
 551   //   (not (= (f sk1 .. skn) (g sk1 .. skn))
 552   UF_HO_MODEL_EXTENSIONALITY,
 553   //-------------------- end model-construction specific part
 554   //-------------------- end HO extension to UF
 555   //-------------------------------------- end uf theory
 556
 557   //-------------------------------------- unknown
 558   UNKNOWN
 559 };
 560
 561 /**
 562  * Converts an inference to a string. Note: This function is also used in
 563  * `safe_print()`. Changing this functions name or signature will result in
 564  * `safe_print()` printing "<unsupported>" instead of the proper strings for
 565  * the enum values.
 566  *
 567  * @param i The inference
 568  * @return The name of the inference
 569  */
 570 const char* toString(InferenceId i);
 571
 572 /**
 573  * Writes an inference name to a stream.
 574  *
 575  * @param out The stream to write to
 576  * @param i The inference to write to the stream
 577  * @return The stream
 578  */
 579 std::ostream& operator<<(std::ostream& out, InferenceId i);
 580
 581 }  // namespace theory
 582 }  // namespace CVC4
 583
 584 #endif /* CVC4__THEORY__INFERENCE_H */