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