1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Gereon Kremer, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * Inference enumeration.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__INFERENCE_ID_H
19 #define CVC5__THEORY__INFERENCE_ID_H
23 #include "expr/node.h"
28 /** Types of inferences used in the procedure
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.
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).
41 enum class InferenceId
43 // ---------------------------------- core
44 // a conflict when two constants merge in the equality engine (of any theory)
46 // a split from theory combination
48 // ---------------------------------- arith theory
49 //-------------------- linear core
50 // black box conflicts. It's magic.
52 // conflicting equality
54 // conflicting lower bound
56 // conflict due to trichotomy
57 ARITH_CONF_TRICHOTOMY
,
58 // conflicting upper bound
60 // conflict from simplex
62 // conflict from sum-of-infeasibility simplex
63 ARITH_CONF_SOI_SIMPLEX
,
64 // introduces split on a disequality
66 // tighten integer inequalities to ceiling
68 // tighten integer inequalities to floor
73 ARITH_DIO_DECOMPOSITION
,
74 // unate lemma during presolve
78 // a split that occurs when the non-linear solver changes values of arithmetic
79 // variables in a model, but those variables are inconsistent with assignments
80 // from another theory
81 ARITH_SPLIT_FOR_NL_MODEL
,
82 //-------------------- preprocessing
83 // equivalence of term and its preprocessed form
84 ARITH_PP_ELIM_OPERATORS
,
85 // a lemma from arithmetic preprocessing
86 ARITH_PP_ELIM_OPERATORS_LEMMA
,
87 //-------------------- nonlinear core
88 // simple congruence x=y => f(x)=f(y)
90 // shared term value split (for naive theory combination)
91 ARITH_NL_SHARED_TERM_VALUE_SPLIT
,
92 // checkModel found a conflict with a quadratic equality
93 ARITH_NL_CM_QUADRATIC_EQ
,
94 //-------------------- nonlinear incremental linearization solver
95 // splitting on zero (NlSolver::checkSplitZero)
97 // based on sign (NlSolver::checkMonomialSign)
99 // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
101 // based on inferring bounds (NlSolver::checkMonomialInferBounds)
102 ARITH_NL_INFER_BOUNDS
,
103 // same as above, for inferences that introduce new terms
104 ARITH_NL_INFER_BOUNDS_NT
,
105 // factoring (NlSolver::checkFactoring)
107 // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
108 ARITH_NL_RES_INFER_BOUNDS
,
109 // tangent planes (NlSolver::checkTangentPlanes)
110 ARITH_NL_TANGENT_PLANE
,
111 //-------------------- nonlinear transcendental solver
112 // purification of arguments to transcendental functions
113 ARITH_NL_T_PURIFY_ARG
,
114 // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
115 ARITH_NL_T_INIT_REFINE
,
118 // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
119 ARITH_NL_T_MONOTONICITY
,
120 // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
122 // secant refinement, the dual of the above inference
124 //-------------------- nonlinear iand solver
125 // initial refinements (IAndSolver::checkInitialRefine)
126 ARITH_NL_IAND_INIT_REFINE
,
127 // value refinements (IAndSolver::checkFullRefine)
128 ARITH_NL_IAND_VALUE_REFINE
,
129 // sum refinements (IAndSolver::checkFullRefine)
130 ARITH_NL_IAND_SUM_REFINE
,
131 // bitwise refinements (IAndSolver::checkFullRefine)
132 ARITH_NL_IAND_BITWISE_REFINE
,
133 //-------------------- nonlinear pow2 solver
134 // initial refinements (Pow2Solver::checkInitialRefine)
135 ARITH_NL_POW2_INIT_REFINE
,
136 // value refinements (Pow2Solver::checkFullRefine)
137 ARITH_NL_POW2_VALUE_REFINE
,
138 // monotonicity refinements (Pow2Solver::checkFullRefine)
139 ARITH_NL_POW2_MONOTONE_REFINE
,
140 // trivial refinements (Pow2Solver::checkFullRefine)
141 ARITH_NL_POW2_TRIVIAL_CASE_REFINE
,
142 //-------------------- nonlinear cad solver
143 // conflict / infeasible subset obtained from cad
144 ARITH_NL_CAD_CONFLICT
,
145 // excludes an interval for a single variable
146 ARITH_NL_CAD_EXCLUDED_INTERVAL
,
147 //-------------------- nonlinear icp solver
148 // conflict obtained from icp
149 ARITH_NL_ICP_CONFLICT
,
150 // propagation / contraction of variable bounds from icp
151 ARITH_NL_ICP_PROPAGATION
,
152 // ---------------------------------- end arith theory
154 // ---------------------------------- arrays theory
156 ARRAYS_READ_OVER_WRITE
,
157 ARRAYS_READ_OVER_WRITE_1
,
158 ARRAYS_READ_OVER_WRITE_CONTRA
,
159 // ---------------------------------- end arrays theory
161 // ---------------------------------- bags theory
162 BAG_NON_NEGATIVE_COUNT
,
163 BAG_MK_BAG_SAME_ELEMENT
,
170 BAG_INTERSECTION_MIN
,
171 BAG_DIFFERENCE_SUBTRACT
,
172 BAG_DIFFERENCE_REMOVE
,
173 BAG_DUPLICATE_REMOVAL
,
174 // ---------------------------------- end bags theory
176 // ---------------------------------- bitvector theory
177 BV_BITBLAST_CONFLICT
,
178 BV_BITBLAST_INTERNAL_EAGER_LEMMA
,
179 BV_BITBLAST_INTERNAL_BITBLAST_LEMMA
,
184 // ---------------------------------- end bitvector theory
186 // ---------------------------------- datatypes theory
187 // (= k t) for fresh k
189 // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
191 // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))
193 // (or ((_ is C1) t) V ... V ((_ is Cn) t))
195 // (or ((_ is Ci) t) V (not ((_ is Ci) t)))
196 DATATYPES_BINARY_SPLIT
,
197 // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
199 // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
200 DATATYPES_COLLAPSE_SEL
,
201 // (= (Ci t1...tn) (Cj t1...tn)) => false
202 DATATYPES_CLASH_CONFLICT
,
203 // ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false
204 DATATYPES_TESTER_CONFLICT
,
205 // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false
206 DATATYPES_TESTER_MERGE_CONFLICT
,
207 // bisimilarity for codatatypes
209 // corecursive singleton equality
210 DATATYPES_REC_SINGLETON_EQ
,
211 // corecursive singleton equality (not (= k1 k2)) for fresh k1, k2
212 DATATYPES_REC_SINGLETON_FORCE_DEQ
,
213 // cycle conflict for datatypes
215 //-------------------- datatypes size/height
216 // (>= (dt.size t) 0)
218 // (=> (= (dt.height t) 0) => (and (= (dt.height (sel_1 t)) 0) .... ))
219 DATATYPES_HEIGHT_ZERO
,
220 //-------------------- sygus extension
221 // a sygus symmetry breaking lemma (or ~is-C1( t1 ) V ... V ~is-Cn( tn ) )
222 // where t1 ... tn are unique shared selector chains. For details see
223 // Reynolds et al CAV 2019
224 DATATYPES_SYGUS_SYM_BREAK
,
225 // a conjecture-dependent symmetry breaking lemma, which may be used to
226 // exclude constructors for variables that irrelevant for a synthesis
228 DATATYPES_SYGUS_CDEP_SYM_BREAK
,
229 // an enumerator-specific symmetry breaking lemma, which are used e.g. for
230 // excluding certain kinds of constructors
231 DATATYPES_SYGUS_ENUM_SYM_BREAK
,
232 // a simple static symmetry breaking lemma (see Reynolds et al CAV 2019)
233 DATATYPES_SYGUS_SIMPLE_SYM_BREAK
,
234 // (dt.size t) <= N, to implement fair enumeration when sygus-fair=dt-size
235 DATATYPES_SYGUS_FAIR_SIZE
,
236 // (dt.size t) <= N => (or ~is-C1( t1 ) V ... V ~is-Cn( tn ) ) if using
238 DATATYPES_SYGUS_FAIR_SIZE_CONFLICT
,
239 // used for implementing variable agnostic enumeration
240 DATATYPES_SYGUS_VAR_AGNOSTIC
,
241 // handles case the model value for a sygus term violates the size bound
242 DATATYPES_SYGUS_SIZE_CORRECTION
,
243 // handles case the model value for a sygus term does not exist
244 DATATYPES_SYGUS_VALUE_CORRECTION
,
245 // s <= (dt.size t), where s is a term that must be less than the current
246 // size bound based on our fairness strategy. For instance, s may be
247 // (dt.size e) for (each) enumerator e when multiple enumerators are present.
248 DATATYPES_SYGUS_MT_BOUND
,
250 DATATYPES_SYGUS_MT_POS
,
251 // ---------------------------------- end datatypes theory
253 //-------------------------------------- floating point theory
254 // a lemma sent during TheoryFp::ppRewrite
256 // a lemma sent during TheoryFp::convertAndEquateTerm
258 // a lemma sent during TheoryFp::registerTerm
260 //-------------------------------------- end floating point theory
262 //-------------------------------------- quantifiers theory
263 //-------------------- types of instantiations.
264 // Notice the identifiers in this section cover all the techniques used for
265 // quantifier instantiation. The subcategories below are for specific lemmas
266 // that are not instantiation lemmas added, per technique.
267 // instantiation from E-matching
268 QUANTIFIERS_INST_E_MATCHING
,
269 // E-matching using simple trigger implementation
270 QUANTIFIERS_INST_E_MATCHING_SIMPLE
,
271 // E-matching using multi-triggers
272 QUANTIFIERS_INST_E_MATCHING_MT
,
273 // E-matching using linear implementation of multi-triggers
274 QUANTIFIERS_INST_E_MATCHING_MTL
,
275 // instantiation due to higher-order matching on top of e-matching
276 QUANTIFIERS_INST_E_MATCHING_HO
,
277 // E-matching based on variable triggers
278 QUANTIFIERS_INST_E_MATCHING_VAR_GEN
,
279 // conflicting instantiation from conflict-based instantiation
280 QUANTIFIERS_INST_CBQI_CONFLICT
,
281 // propagating instantiation from conflict-based instantiation
282 QUANTIFIERS_INST_CBQI_PROP
,
283 // instantiation from naive exhaustive instantiation in finite model finding
284 QUANTIFIERS_INST_FMF_EXH
,
285 // instantiation from finite model finding based on its model-based algorithm
286 QUANTIFIERS_INST_FMF_FMC
,
287 // instantiation from running exhaustive instantiation on a subdomain of
288 // the quantified formula in finite model finding based on its model-based
290 QUANTIFIERS_INST_FMF_FMC_EXH
,
291 // instantiations from counterexample-guided instantiation
292 QUANTIFIERS_INST_CEGQI
,
293 // instantiations from syntax-guided instantiation
294 QUANTIFIERS_INST_SYQI
,
295 // instantiations from enumerative instantiation
296 QUANTIFIERS_INST_ENUM
,
297 // instantiations from pool instantiation
298 QUANTIFIERS_INST_POOL
,
299 //-------------------- bounded integers
300 // a proxy lemma from bounded integers, used to control bounds on ground terms
301 QUANTIFIERS_BINT_PROXY
,
302 // a proxy lemma to minimize an instantiation of non-ground terms
303 QUANTIFIERS_BINT_MIN_NG
,
304 //-------------------- counterexample-guided instantiation
305 // a counterexample lemma
306 QUANTIFIERS_CEGQI_CEX
,
307 // an auxiliary lemma from counterexample lemma
308 QUANTIFIERS_CEGQI_CEX_AUX
,
309 // a reduction lemma for nested quantifier elimination
310 QUANTIFIERS_CEGQI_NESTED_QE
,
311 // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
312 // counterexample literal is G1.
313 QUANTIFIERS_CEGQI_CEX_DEP
,
315 QUANTIFIERS_CEGQI_VTS_LB_DELTA
,
316 // delta < c, for positive c
317 QUANTIFIERS_CEGQI_VTS_UB_DELTA
,
319 QUANTIFIERS_CEGQI_VTS_LB_INF
,
320 //-------------------- syntax-guided instantiation
321 // a counterexample lemma
322 QUANTIFIERS_SYQI_CEX
,
323 // evaluation unfolding for syntax-guided instantiation
324 QUANTIFIERS_SYQI_EVAL_UNFOLD
,
325 //-------------------- sygus solver
326 // preprocessing a sygus conjecture based on quantifier elimination, of the
327 // form Q <=> Q_preprocessed
328 QUANTIFIERS_SYGUS_QE_PREPROC
,
329 // G or ~G where G is the active guard for a sygus enumerator
330 QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT
,
331 // manual exclusion of a current solution
332 QUANTIFIERS_SYGUS_EXCLUDE_CURRENT
,
333 // manual exclusion of a current solution for sygus-stream
334 QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT
,
335 // ~Q where Q is a PBE conjecture with conflicting examples
336 QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA
,
337 //-------------------- dynamic splitting
338 // a dynamic split from quantifiers
340 //-------------------- miscellaneous
342 QUANTIFIERS_SKOLEMIZE
,
343 // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
344 QUANTIFIERS_REDUCE_ALPHA_EQ
,
345 // a higher-order match predicate lemma
346 QUANTIFIERS_HO_MATCH_PRED
,
347 // reduction of quantifiers that don't have triggers that cover all variables
348 QUANTIFIERS_PARTIAL_TRIGGER_REDUCE
,
349 //-------------------------------------- end quantifiers theory
351 // ---------------------------------- sep theory
352 // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
354 // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
356 // introduces a label for a heap, of the form U => L, where U is an
357 // unlabelled separation logic predicate and L is its labelled form
359 // introduces the set constraints for a label
363 // positive reduction for sep constraint
365 // negative reduction for sep constraint
367 // model-based refinement for negated star/wand
369 // sep.nil is not in the heap
371 // a symmetry breaking lemma
373 // finite witness data lemma
374 SEP_WITNESS_FINITE_DATA
,
375 // element distinctness lemma
377 // reference bound lemma
379 // ---------------------------------- end sep theory
381 // ---------------------------------- sets theory
382 //-------------------- sets core solver
383 // split when computing care graph
388 // conflict when two singleton/emptyset terms merge
391 SETS_EQ_MEM_CONFLICT
,
393 SETS_MEM_EQ_CONFLICT
,
395 SETS_PROXY_SINGLETON
,
401 //-------------------- sets cardinality solver
403 SETS_CARD_SPLIT_EMPTY
,
404 // cycle of cardinalities, hence all sets have the same
406 // two sets have the same cardinality
409 SETS_CARD_GRAPH_EMP_PARENT
,
410 SETS_CARD_GRAPH_EQ_PARENT
,
411 SETS_CARD_GRAPH_EQ_PARENT_2
,
412 SETS_CARD_GRAPH_PARENT_SINGLETON
,
413 // cardinality is at least the number of elements we already know
415 // negative members are part of the universe
416 SETS_CARD_NEGATIVE_MEMBER
,
417 // all sets have non-negative cardinality
419 // the universe is a superset of every set
420 SETS_CARD_UNIV_SUPERSET
,
421 // cardinality of the universe is at most cardinality of the type
423 //-------------------- sets relations solver
424 SETS_RELS_IDENTITY_DOWN
,
425 SETS_RELS_IDENTITY_UP
,
426 SETS_RELS_JOIN_COMPOSE
,
427 SETS_RELS_JOIN_IMAGE_DOWN
,
428 SETS_RELS_JOIN_SPLIT_1
,
429 SETS_RELS_JOIN_SPLIT_2
,
430 SETS_RELS_PRODUCE_COMPOSE
,
431 SETS_RELS_PRODUCT_SPLIT
,
432 SETS_RELS_TCLOSURE_FWD
,
433 SETS_RELS_TCLOSURE_UP
,
434 SETS_RELS_TRANSPOSE_EQ
,
435 SETS_RELS_TRANSPOSE_REV
,
436 SETS_RELS_TUPLE_REDUCTION
,
437 //-------------------------------------- end sets theory
439 //-------------------------------------- strings theory
440 //-------------------- base solver
441 // initial normalize singular
442 // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
443 // x1 ++ ... ++ xn = xi
445 // initial constant merge
446 // explain_constant(x, c) => x = c
447 // Above, explain_constant(x,c) is a basic explanation of why x must be equal
448 // to string constant c, which is computed by taking arguments of
449 // concatenation terms that are entailed to be constants. For example:
450 // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
451 STRINGS_I_CONST_MERGE
,
452 // initial constant conflict
453 // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
455 STRINGS_I_CONST_CONFLICT
,
457 // Given two concatenation terms, this is applied when we find that they are
458 // equal after e.g. removing strings that are currently empty. For example:
459 // y = "" ^ z = "" => x ++ y = z ++ x
461 // injectivity of seq.unit
462 // (seq.unit x) = (seq.unit y) => x=y, or
463 // (seq.unit x) = (seq.unit c) => x=c
465 // unit constant conflict
466 // (seq.unit x) = C => false if |C| != 1.
467 STRINGS_UNIT_CONST_CONFLICT
,
468 // injectivity of seq.unit for disequality
469 // (seq.unit x) != (seq.unit y) => x != y, or
470 // (seq.unit x) != (seq.unit c) => x != c
471 STRINGS_UNIT_INJ_DEQ
,
472 // A split due to cardinality
474 // The cardinality inference for strings, see Liang et al CAV 2014.
476 //-------------------- core solver
477 // A cycle in the empty string equivalence class, e.g.:
478 // x ++ y = "" => x = ""
479 // This is typically not applied due to length constraints implying emptiness.
481 // A cycle in the containment ordering.
482 // x = y ++ x => y = "" or
483 // x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
484 // This is typically not applied due to length constraints implying emptiness.
486 // Flat form constant
487 // x = y ^ x = z ++ c ... ^ y = z ++ d => false
488 // where c and d are distinct constants.
491 // x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
492 // Notice flat form instances are similar to normal form inferences but do
493 // not involve recursive explanations.
495 // Flat form endpoint empty
496 // x = y ^ x = z ^ y = z ++ y' => y' = ""
497 STRINGS_F_ENDPOINT_EMP
,
498 // Flat form endpoint equal
499 // x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
500 STRINGS_F_ENDPOINT_EQ
,
501 // Flat form not contained
502 // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
504 // Normal form equality conflict
505 // x = N[x] ^ y = N[y] ^ x=y => false
506 // where Rewriter::rewrite(N[x]=N[y]) = false.
508 // Given two normal forms, infers that the remainder one of them has to be
509 // empty. For example:
510 // If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
511 STRINGS_N_ENDPOINT_EMP
,
512 // Given two normal forms, infers that two components have to be the same if
513 // they have the same length. For example:
514 // If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
516 // Given two normal forms, infers that the endpoints have to be the same. For
518 // If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
519 STRINGS_N_ENDPOINT_EQ
,
520 // Given two normal forms with constant endpoints, infers a conflict if the
521 // endpoints do not agree. For example:
522 // If "abc" ++ ... = "bc" ++ ... then conflict
524 // infer empty, for example:
526 // This is inferred when we encounter an x such that x = "" rewrites to a
527 // constant. This inference is used for instance when we otherwise would have
528 // split on the emptiness of x but the rewriter tells us the emptiness of x
531 // string split constant propagation, for example:
532 // x = y, x = "abc", y = y1 ++ "b" ++ y2
533 // implies y1 = "a" ++ y1'
534 STRINGS_SSPLIT_CST_PROP
,
535 // string split variable propagation, for example:
536 // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
537 // implies x1 = y1 ++ x1'
538 // This is inspired by Zheng et al CAV 2015.
539 STRINGS_SSPLIT_VAR_PROP
,
540 // length split, for example:
541 // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
542 // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
544 // length split empty, for example:
546 // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
547 STRINGS_LEN_SPLIT_EMP
,
548 // string split constant
549 // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
550 // implies y1 = "c" ++ y1'
551 // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
553 // string split variable, for example:
554 // x = y, x = x1 ++ x2, y = y1 ++ y2
555 // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
556 // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
558 // flat form loop, for example:
559 // x = y, x = x1 ++ z, y = z ++ y2
560 // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
561 // for fresh u, u1, u2.
562 // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
565 STRINGS_FLOOP_CONFLICT
,
566 // Normal form inference
567 // x = y ^ z = y => x = z
568 // This is applied when y is the normal form of both x and z.
570 // Normal form not contained, same as FFROM_NCTN but for normal forms
572 // Length normalization
573 // x = y => len( x ) = len( y )
574 // Typically applied when y is the normal form of x.
576 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
579 STRINGS_DEQ_DISL_EMP_SPLIT
,
580 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1, we apply the
582 // x = "a" v x != "a"
583 STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT
,
584 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != "", we apply the
586 // ni = x ++ x' ++ ... ^ nj = "abc" ++ y' ++ ... ^ x != "" --->
587 // x = k1 ++ k2 ^ len(k1) = 1 ^ (k1 != "a" v x = "a" ++ k2)
588 STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT
,
589 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y), we apply the
591 // ni = x ++ x' ++ ... ^ nj = y ++ y' ++ ... ^ ni != nj ^ len(x) != len(y)
593 // len(k1) = len(x) ^ len(k2) = len(y) ^ (y = k1 ++ k3 v x = k1 ++ k2)
594 STRINGS_DEQ_DISL_STRINGS_SPLIT
,
595 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y), we apply the
598 STRINGS_DEQ_STRINGS_EQ
,
599 // When x ++ x' ++ ... != y ++ y' ++ ... and we do not know how the lengths
600 // of x and y compare, we apply the inference:
601 // len(x) = len(y) v len(x) != len(y)
603 // When px ++ x ++ ... != py ^ len(px ++ x ++ ...) = len(py), we apply the
604 // following inference that infers that the remainder of the longer normal
605 // form must be empty:
606 // ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
608 STRINGS_DEQ_NORM_EMP
,
609 // When two strings are disequal s != t and the comparison of their lengths
610 // is unknown, we apply the inference:
611 // len(s) != len(t) V len(s) = len(t)
612 STRINGS_DEQ_LENGTH_SP
,
613 //-------------------- codes solver
614 // str.to_code( v ) = rewrite( str.to_code(c) )
615 // where v is the proxy variable for c.
617 // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
619 //-------------------- regexp solver
620 // regular expression normal form conflict
621 // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
622 // where y is the normal form computed for x.
623 STRINGS_RE_NF_CONFLICT
,
624 // regular expression unfolding
625 // This is a general class of inferences of the form:
627 // where F is formula expressing the next step of checking whether x is in
630 // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
631 STRINGS_RE_UNFOLD_POS
,
632 // Same as above, for negative memberships
633 STRINGS_RE_UNFOLD_NEG
,
634 // intersection inclusion conflict
635 // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]]
636 // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
637 STRINGS_RE_INTER_INCLUDE
,
638 // intersection conflict, using regexp intersection computation
639 // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]]
640 STRINGS_RE_INTER_CONF
,
641 // intersection inference
642 // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
643 STRINGS_RE_INTER_INFER
,
644 // regular expression delta
645 // (x = "" ^ x in R) => C
646 // where "" in R holds if and only if C holds.
648 // regular expression delta conflict
649 // (x = "" ^ x in R) => false
650 // where R does not accept the empty string.
651 STRINGS_RE_DELTA_CONF
,
652 // regular expression derive ???
654 //-------------------- extended function solver
655 // Standard extended function inferences from context-dependent rewriting
656 // produced by constant substitutions. See Reynolds et al CAV 2017. These are
657 // inferences of the form:
658 // X = Y => f(X) = t when rewrite( f(Y) ) = t
659 // where X = Y is a vector of equalities, where some of Y may be constants.
661 // Same as above, for normal form substitutions.
663 // Decompositions based on extended function inferences from context-dependent
664 // rewriting produced by constant substitutions. This is like the above, but
665 // handles cases where the inferred predicate is not necessarily an equality
666 // involving f(X). For example:
667 // x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
668 // This is generally only inferred if contains( y, "B" ) is a known term in
669 // the current context.
671 // Same as above, for normal form substitutions.
673 // Extended function equality rewrite. This is an inference of the form:
675 // where P is a predicate implied by rewrite( t = s ).
676 // Typically, t is an application of an extended function and s is a constant.
677 // It is generally only inferred if P is a predicate over known terms.
679 // contain transitive
680 // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
683 // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
684 // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
685 STRINGS_CTN_DECOMPOSE
,
687 // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
688 STRINGS_CTN_NEG_EQUAL
,
690 // str.contains( x, y ) => x = w1 ++ y ++ w2
691 // where w1 and w2 are skolem variables.
693 // All reduction inferences of the form:
694 // f(x1, .., xn) = y ^ P(x1, ..., xn, y)
695 // where f is an extended function, y is the purification variable for
696 // f(x1, .., xn) and P is the reduction predicate for f
697 // (see theory_strings_preprocess).
699 //-------------------- prefix conflict
700 // prefix conflict (coarse-grained)
701 STRINGS_PREFIX_CONFLICT
,
702 //-------------------- other
703 // a lemma added during term registration for an atomic term
704 STRINGS_REGISTER_TERM_ATOMIC
,
705 // a lemma added during term registration
706 STRINGS_REGISTER_TERM
,
707 // a split during collect model info
709 //-------------------------------------- end strings theory
711 //-------------------------------------- uf theory
712 // Clause from the uf symmetry breaker
714 //-------------------- cardinality extension to UF
715 // The inferences below are described in Reynolds' thesis 2013.
716 // conflict of the form (card_T n) => (not (distinct t1 ... tn))
718 // conflict of the form (not (card_T1 n1)) ^ ... (not (card_Tk nk)) ^ (card n)
719 // where n1 + ... + nk >= n, where (card n) is a combined cardinality
722 // (not (card_T n)) => (distinct t1 ... tn)
723 UF_CARD_ENFORCE_NEGATIVE
,
724 // used to make the index terms in cardinality constraints equal
726 // conflict of the form (not (card_T1 n)) ^ (card_T2 m) where the cardinality
727 // of T2 can be assumed to be without loss of generality larger than T1 due to
728 // monotonicity reasoning (Claessen et al 2011).
729 UF_CARD_MONOTONE_COMBINED
,
730 // conflict of the form (not (card_T n)) ^ (card_T m) where n>m
731 UF_CARD_SIMPLE_CONFLICT
,
732 // equality split requested by cardinality solver
733 // (or (= t1 t2) (not (= t1 t2))
734 // to satisfy the cardinality constraints on the type of t1, t2.
736 //-------------------- end cardinality extension to UF
737 //-------------------- HO extension to UF
738 // Encodes an n-ary application as a chain of binary HO_APPLY applications
739 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
741 // A lemma corresponding to the definition of a skolem k used to convert
742 // HO_APPLY terms to APPLY_UF terms. This is of the form:
743 // (forall x1 ... xn) (@ (@ k x1) ... xn) = t
744 // where notice that t is a function whose free variables (if any) are
746 UF_HO_APP_CONV_SKOLEM
,
747 // Adds an extensionality lemma to witness that disequal functions have
748 // different applications
749 // (not (= (f sk1 .. skn) (g sk1 .. skn))
750 UF_HO_EXTENSIONALITY
,
751 //-------------------- model-construction specific part
752 // These rules are necessary to ensure that we build models properly. For more
753 // details see Section 3.3 of Barbosa et al. CADE'19.
755 // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
756 // equivalent by adding the equality as a lemma
757 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
758 UF_HO_MODEL_APP_ENCODE
,
759 // Adds an extensionality lemma to witness that disequal functions have
760 // different applications
761 // (not (= (f sk1 .. skn) (g sk1 .. skn))
762 UF_HO_MODEL_EXTENSIONALITY
,
763 //-------------------- end model-construction specific part
764 //-------------------- end HO extension to UF
765 //-------------------------------------- end uf theory
767 //-------------------------------------- unknown
772 * Converts an inference to a string. Note: This function is also used in
773 * `safe_print()`. Changing this functions name or signature will result in
774 * `safe_print()` printing "<unsupported>" instead of the proper strings for
777 * @param i The inference
778 * @return The name of the inference
780 const char* toString(InferenceId i
);
783 * Writes an inference name to a stream.
785 * @param out The stream to write to
786 * @param i The inference to write to the stream
789 std::ostream
& operator<<(std::ostream
& out
, InferenceId i
);
791 /** Make node from inference id */
792 Node
mkInferenceIdNode(InferenceId i
);
794 } // namespace theory
797 #endif /* CVC5__THEORY__INFERENCE_H */