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 // ---------------------------------- ext theory
49 // a simplification from the extended theory utility
51 // ---------------------------------- arith theory
52 //-------------------- linear core
53 // black box conflicts. It's magic.
55 // conflicting equality
57 // conflicting lower bound
59 // conflict due to trichotomy
60 ARITH_CONF_TRICHOTOMY
,
61 // conflicting upper bound
63 // conflict from simplex
65 // conflict from sum-of-infeasibility simplex
66 ARITH_CONF_SOI_SIMPLEX
,
67 // conflict when getting constraint from fact queue
68 ARITH_CONF_FACT_QUEUE
,
69 // introduces split on a disequality
71 // tighten integer inequalities to ceiling
73 // tighten integer inequalities to floor
78 ARITH_DIO_DECOMPOSITION
,
79 // unate lemma during presolve
83 // a split that occurs when the non-linear solver changes values of arithmetic
84 // variables in a model, but those variables are inconsistent with assignments
85 // from another theory
86 ARITH_SPLIT_FOR_NL_MODEL
,
87 //-------------------- preprocessing
88 // equivalence of term and its preprocessed form
89 ARITH_PP_ELIM_OPERATORS
,
90 // a lemma from arithmetic preprocessing
91 ARITH_PP_ELIM_OPERATORS_LEMMA
,
92 //-------------------- nonlinear core
93 // simple congruence x=y => f(x)=f(y)
95 // shared term value split (for naive theory combination)
96 ARITH_NL_SHARED_TERM_VALUE_SPLIT
,
97 // checkModel found a conflict with a quadratic equality
98 ARITH_NL_CM_QUADRATIC_EQ
,
99 //-------------------- nonlinear incremental linearization solver
100 // splitting on zero (NlSolver::checkSplitZero)
102 // based on sign (NlSolver::checkMonomialSign)
104 // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
106 // based on inferring bounds (NlSolver::checkMonomialInferBounds)
107 ARITH_NL_INFER_BOUNDS
,
108 // same as above, for inferences that introduce new terms
109 ARITH_NL_INFER_BOUNDS_NT
,
110 // factoring (NlSolver::checkFactoring)
112 // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
113 ARITH_NL_RES_INFER_BOUNDS
,
114 // tangent planes (NlSolver::checkTangentPlanes)
115 ARITH_NL_TANGENT_PLANE
,
116 //-------------------- nonlinear transcendental solver
117 // purification of arguments to transcendental functions
118 ARITH_NL_T_PURIFY_ARG
,
119 // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
120 ARITH_NL_T_INIT_REFINE
,
123 // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
124 ARITH_NL_T_MONOTONICITY
,
125 // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
127 // secant refinement, the dual of the above inference
129 //-------------------- nonlinear iand solver
130 // initial refinements (IAndSolver::checkInitialRefine)
131 ARITH_NL_IAND_INIT_REFINE
,
132 // value refinements (IAndSolver::checkFullRefine)
133 ARITH_NL_IAND_VALUE_REFINE
,
134 // sum refinements (IAndSolver::checkFullRefine)
135 ARITH_NL_IAND_SUM_REFINE
,
136 // bitwise refinements (IAndSolver::checkFullRefine)
137 ARITH_NL_IAND_BITWISE_REFINE
,
138 //-------------------- nonlinear pow2 solver
139 // initial refinements (Pow2Solver::checkInitialRefine)
140 ARITH_NL_POW2_INIT_REFINE
,
141 // value refinements (Pow2Solver::checkFullRefine)
142 ARITH_NL_POW2_VALUE_REFINE
,
143 // monotonicity refinements (Pow2Solver::checkFullRefine)
144 ARITH_NL_POW2_MONOTONE_REFINE
,
145 // trivial refinements (Pow2Solver::checkFullRefine)
146 ARITH_NL_POW2_TRIVIAL_CASE_REFINE
,
147 //-------------------- nonlinear cad solver
148 // conflict / infeasible subset obtained from cad
149 ARITH_NL_CAD_CONFLICT
,
150 // excludes an interval for a single variable
151 ARITH_NL_CAD_EXCLUDED_INTERVAL
,
152 //-------------------- nonlinear icp solver
153 // conflict obtained from icp
154 ARITH_NL_ICP_CONFLICT
,
155 // propagation / contraction of variable bounds from icp
156 ARITH_NL_ICP_PROPAGATION
,
157 // ---------------------------------- end arith theory
159 // ---------------------------------- arrays theory
161 ARRAYS_READ_OVER_WRITE
,
162 ARRAYS_READ_OVER_WRITE_1
,
163 ARRAYS_READ_OVER_WRITE_CONTRA
,
164 // (= (select (as const (Array T1 T2) x) y) x)
165 ARRAYS_CONST_ARRAY_DEFAULT
,
166 // an internally inferred tautological equality
168 // ---------------------------------- end arrays theory
170 // ---------------------------------- bags theory
171 BAG_NON_NEGATIVE_COUNT
,
172 BAG_MK_BAG_SAME_ELEMENT
,
179 BAG_INTERSECTION_MIN
,
180 BAG_DIFFERENCE_SUBTRACT
,
181 BAG_DIFFERENCE_REMOVE
,
182 BAG_DUPLICATE_REMOVAL
,
183 // ---------------------------------- end bags theory
185 // ---------------------------------- bitvector theory
186 BV_BITBLAST_CONFLICT
,
187 BV_BITBLAST_INTERNAL_EAGER_LEMMA
,
188 BV_BITBLAST_INTERNAL_BITBLAST_LEMMA
,
193 // ---------------------------------- end bitvector theory
195 // ---------------------------------- datatypes theory
196 // (= k t) for fresh k
198 // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
200 // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))
202 // (or ((_ is C1) t) V ... V ((_ is Cn) t))
204 // (or ((_ is Ci) t) V (not ((_ is Ci) t)))
205 DATATYPES_BINARY_SPLIT
,
206 // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
208 // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
209 DATATYPES_COLLAPSE_SEL
,
210 // (= (Ci t1...tn) (Cj t1...tn)) => false
211 DATATYPES_CLASH_CONFLICT
,
212 // ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false
213 DATATYPES_TESTER_CONFLICT
,
214 // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false
215 DATATYPES_TESTER_MERGE_CONFLICT
,
216 // bisimilarity for codatatypes
218 // corecursive singleton equality
219 DATATYPES_REC_SINGLETON_EQ
,
220 // corecursive singleton equality (not (= k1 k2)) for fresh k1, k2
221 DATATYPES_REC_SINGLETON_FORCE_DEQ
,
222 // cycle conflict for datatypes
224 //-------------------- datatypes size/height
225 // (>= (dt.size t) 0)
227 // (=> (= (dt.height t) 0) => (and (= (dt.height (sel_1 t)) 0) .... ))
228 DATATYPES_HEIGHT_ZERO
,
229 //-------------------- sygus extension
230 // a sygus symmetry breaking lemma (or ~is-C1( t1 ) V ... V ~is-Cn( tn ) )
231 // where t1 ... tn are unique shared selector chains. For details see
232 // Reynolds et al CAV 2019
233 DATATYPES_SYGUS_SYM_BREAK
,
234 // a conjecture-dependent symmetry breaking lemma, which may be used to
235 // exclude constructors for variables that irrelevant for a synthesis
237 DATATYPES_SYGUS_CDEP_SYM_BREAK
,
238 // an enumerator-specific symmetry breaking lemma, which are used e.g. for
239 // excluding certain kinds of constructors
240 DATATYPES_SYGUS_ENUM_SYM_BREAK
,
241 // a simple static symmetry breaking lemma (see Reynolds et al CAV 2019)
242 DATATYPES_SYGUS_SIMPLE_SYM_BREAK
,
243 // (dt.size t) <= N, to implement fair enumeration when sygus-fair=dt-size
244 DATATYPES_SYGUS_FAIR_SIZE
,
245 // (dt.size t) <= N => (or ~is-C1( t1 ) V ... V ~is-Cn( tn ) ) if using
247 DATATYPES_SYGUS_FAIR_SIZE_CONFLICT
,
248 // used for implementing variable agnostic enumeration
249 DATATYPES_SYGUS_VAR_AGNOSTIC
,
250 // handles case the model value for a sygus term violates the size bound
251 DATATYPES_SYGUS_SIZE_CORRECTION
,
252 // handles case the model value for a sygus term does not exist
253 DATATYPES_SYGUS_VALUE_CORRECTION
,
254 // s <= (dt.size t), where s is a term that must be less than the current
255 // size bound based on our fairness strategy. For instance, s may be
256 // (dt.size e) for (each) enumerator e when multiple enumerators are present.
257 DATATYPES_SYGUS_MT_BOUND
,
259 DATATYPES_SYGUS_MT_POS
,
260 // ---------------------------------- end datatypes theory
262 //-------------------------------------- floating point theory
263 // a lemma sent during TheoryFp::ppRewrite
265 // a lemma sent during TheoryFp::convertAndEquateTerm
267 // a lemma sent during TheoryFp::registerTerm
269 //-------------------------------------- end floating point theory
271 //-------------------------------------- quantifiers theory
272 //-------------------- types of instantiations.
273 // Notice the identifiers in this section cover all the techniques used for
274 // quantifier instantiation. The subcategories below are for specific lemmas
275 // that are not instantiation lemmas added, per technique.
276 // instantiation from E-matching
277 QUANTIFIERS_INST_E_MATCHING
,
278 // E-matching using simple trigger implementation
279 QUANTIFIERS_INST_E_MATCHING_SIMPLE
,
280 // E-matching using multi-triggers
281 QUANTIFIERS_INST_E_MATCHING_MT
,
282 // E-matching using linear implementation of multi-triggers
283 QUANTIFIERS_INST_E_MATCHING_MTL
,
284 // instantiation due to higher-order matching on top of e-matching
285 QUANTIFIERS_INST_E_MATCHING_HO
,
286 // E-matching based on variable triggers
287 QUANTIFIERS_INST_E_MATCHING_VAR_GEN
,
288 // conflicting instantiation from conflict-based instantiation
289 QUANTIFIERS_INST_CBQI_CONFLICT
,
290 // propagating instantiation from conflict-based instantiation
291 QUANTIFIERS_INST_CBQI_PROP
,
292 // instantiation from naive exhaustive instantiation in finite model finding
293 QUANTIFIERS_INST_FMF_EXH
,
294 // instantiation from finite model finding based on its model-based algorithm
295 QUANTIFIERS_INST_FMF_FMC
,
296 // instantiation from running exhaustive instantiation on a subdomain of
297 // the quantified formula in finite model finding based on its model-based
299 QUANTIFIERS_INST_FMF_FMC_EXH
,
300 // instantiations from counterexample-guided instantiation
301 QUANTIFIERS_INST_CEGQI
,
302 // instantiations from syntax-guided instantiation
303 QUANTIFIERS_INST_SYQI
,
304 // instantiations from enumerative instantiation
305 QUANTIFIERS_INST_ENUM
,
306 // instantiations from pool instantiation
307 QUANTIFIERS_INST_POOL
,
308 //-------------------- bounded integers
309 // a proxy lemma from bounded integers, used to control bounds on ground terms
310 QUANTIFIERS_BINT_PROXY
,
311 // a proxy lemma to minimize an instantiation of non-ground terms
312 QUANTIFIERS_BINT_MIN_NG
,
313 //-------------------- counterexample-guided instantiation
314 // a counterexample lemma
315 QUANTIFIERS_CEGQI_CEX
,
316 // an auxiliary lemma from counterexample lemma
317 QUANTIFIERS_CEGQI_CEX_AUX
,
318 // a reduction lemma for nested quantifier elimination
319 QUANTIFIERS_CEGQI_NESTED_QE
,
320 // G2 => G1 where G2 is a counterexample literal for a nested quantifier whose
321 // counterexample literal is G1.
322 QUANTIFIERS_CEGQI_CEX_DEP
,
324 QUANTIFIERS_CEGQI_VTS_LB_DELTA
,
325 // delta < c, for positive c
326 QUANTIFIERS_CEGQI_VTS_UB_DELTA
,
328 QUANTIFIERS_CEGQI_VTS_LB_INF
,
329 //-------------------- syntax-guided instantiation
330 // a counterexample lemma
331 QUANTIFIERS_SYQI_CEX
,
332 // evaluation unfolding for syntax-guided instantiation
333 QUANTIFIERS_SYQI_EVAL_UNFOLD
,
334 //-------------------- sygus solver
335 // preprocessing a sygus conjecture based on quantifier elimination, of the
336 // form Q <=> Q_preprocessed
337 QUANTIFIERS_SYGUS_QE_PREPROC
,
338 // G or ~G where G is the active guard for a sygus enumerator
339 QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT
,
340 // manual exclusion of a current solution
341 QUANTIFIERS_SYGUS_EXCLUDE_CURRENT
,
342 // manual exclusion of a current solution for sygus-stream
343 QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT
,
344 // Q where Q was solved by a subcall to the single invocation module
345 QUANTIFIERS_SYGUS_SI_SOLVED
,
346 // Q where Q was (trusted) solved by sampling
347 QUANTIFIERS_SYGUS_SAMPLE_TRUST_SOLVED
,
348 // Q where Q was solved by a verification subcall
349 QUANTIFIERS_SYGUS_VERIFY_SOLVED
,
350 // ~Q where Q is a PBE conjecture with conflicting examples
351 QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA
,
352 // unif+pi symmetry breaking between multiple enumerators
353 QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB
,
354 // unif+pi separation lemma
355 QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION
,
356 // unif+pi lemma for fairness of size of enumerators
357 QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE
,
358 // unif+pi lemma for removing redundant operators
359 QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS
,
360 // symmetry breaking for enumerators
361 QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB
,
362 // constraining terms to be in the domain of output
363 QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN
,
364 // condition exclusion from sygus unif
365 QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE
,
366 // refinement lemma from sygus unif
367 QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT
,
368 // symmetry breaking lemma from unsat core learning algorithm initialization
369 QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK
,
370 // candidate exclusion lemma from unsat core learning algorithm
371 QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE
,
372 // candidate exclusion lemma from repair constants algorithm
373 QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE
,
374 // a counterexample-guided inductive synthesis refinement lemma
375 QUANTIFIERS_SYGUS_CEGIS_REFINE
,
376 // a cegis refinement lemma found by sampling
377 QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE
,
378 // a lemma based on refinement lemma evaluation
379 QUANTIFIERS_SYGUS_REFINE_EVAL
,
380 // an evaluation unfolding lemma
381 QUANTIFIERS_SYGUS_EVAL_UNFOLD
,
382 // candidate exclusion lemma from programming-by-examples
383 QUANTIFIERS_SYGUS_PBE_EXCLUDE
,
384 // a lemma generated while constructing a candidate solution for PBE
385 QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL
,
386 //-------------------- dynamic splitting
387 // a dynamic split from quantifiers
389 //-------------------- induction / conjecture generation
390 // a split on a conjecture for inductive theorem proving
391 QUANTIFIERS_CONJ_GEN_SPLIT
,
392 // enumeration of ground terms for inductive theorem proving
393 QUANTIFIERS_CONJ_GEN_GT_ENUM
,
394 //-------------------- miscellaneous
396 QUANTIFIERS_SKOLEMIZE
,
397 // Q1 <=> Q2, where Q1 and Q2 are alpha equivalent
398 QUANTIFIERS_REDUCE_ALPHA_EQ
,
399 // a higher-order match predicate lemma
400 QUANTIFIERS_HO_MATCH_PRED
,
401 // purification of non-variable higher-order function
402 QUANTIFIERS_HO_PURIFY
,
403 // reduction of quantifiers that don't have triggers that cover all variables
404 QUANTIFIERS_PARTIAL_TRIGGER_REDUCE
,
405 // a purification lemma for a ground term appearing in a quantified formula,
406 // used to ensure E-matching has equality information for that term
407 QUANTIFIERS_GT_PURIFY
,
408 // when term indexing discovers disequal congruent terms in the master
410 QUANTIFIERS_TDB_DEQ_CONG
,
411 //-------------------------------------- end quantifiers theory
413 // ---------------------------------- sep theory
414 // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
416 // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
418 // introduces a label for a heap, of the form U => L, where U is an
419 // unlabelled separation logic predicate and L is its labelled form
421 // introduces the set constraints for a label
425 // positive reduction for sep constraint
427 // negative reduction for sep constraint
429 // model-based refinement for negated star/wand
431 // sep.nil is not in the heap
433 // a symmetry breaking lemma
435 // finite witness data lemma
436 SEP_WITNESS_FINITE_DATA
,
437 // element distinctness lemma
439 // reference bound lemma
441 // ---------------------------------- end sep theory
443 // ---------------------------------- sets theory
444 //-------------------- sets core solver
445 // split when computing care graph
450 // conflict when two singleton/emptyset terms merge
453 SETS_EQ_MEM_CONFLICT
,
455 SETS_MEM_EQ_CONFLICT
,
457 SETS_PROXY_SINGLETON
,
463 //-------------------- sets cardinality solver
465 SETS_CARD_SPLIT_EMPTY
,
466 // cycle of cardinalities, hence all sets have the same
468 // two sets have the same cardinality
471 SETS_CARD_GRAPH_EMP_PARENT
,
472 SETS_CARD_GRAPH_EQ_PARENT
,
473 SETS_CARD_GRAPH_EQ_PARENT_2
,
474 SETS_CARD_GRAPH_PARENT_SINGLETON
,
475 // cardinality is at least the number of elements we already know
477 // negative members are part of the universe
478 SETS_CARD_NEGATIVE_MEMBER
,
479 // all sets have non-negative cardinality
481 // the universe is a superset of every set
482 SETS_CARD_UNIV_SUPERSET
,
483 // cardinality of the universe is at most cardinality of the type
485 //-------------------- sets relations solver
486 SETS_RELS_IDENTITY_DOWN
,
487 SETS_RELS_IDENTITY_UP
,
488 SETS_RELS_JOIN_COMPOSE
,
489 SETS_RELS_JOIN_IMAGE_DOWN
,
490 SETS_RELS_JOIN_IMAGE_UP
,
491 SETS_RELS_JOIN_SPLIT_1
,
492 SETS_RELS_JOIN_SPLIT_2
,
493 SETS_RELS_PRODUCE_COMPOSE
,
494 SETS_RELS_PRODUCT_SPLIT
,
495 SETS_RELS_TCLOSURE_FWD
,
496 SETS_RELS_TCLOSURE_UP
,
497 SETS_RELS_TRANSPOSE_EQ
,
498 SETS_RELS_TRANSPOSE_REV
,
499 SETS_RELS_TUPLE_REDUCTION
,
500 //-------------------------------------- end sets theory
502 //-------------------------------------- strings theory
503 //-------------------- base solver
504 // initial normalize singular
505 // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
506 // x1 ++ ... ++ xn = xi
508 // initial constant merge
509 // explain_constant(x, c) => x = c
510 // Above, explain_constant(x,c) is a basic explanation of why x must be equal
511 // to string constant c, which is computed by taking arguments of
512 // concatenation terms that are entailed to be constants. For example:
513 // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
514 STRINGS_I_CONST_MERGE
,
515 // initial constant conflict
516 // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
518 STRINGS_I_CONST_CONFLICT
,
520 // Given two concatenation terms, this is applied when we find that they are
521 // equal after e.g. removing strings that are currently empty. For example:
522 // y = "" ^ z = "" => x ++ y = z ++ x
524 // injectivity of seq.unit
525 // (seq.unit x) = (seq.unit y) => x=y, or
526 // (seq.unit x) = (seq.unit c) => x=c
528 // unit constant conflict
529 // (seq.unit x) = C => false if |C| != 1.
530 STRINGS_UNIT_CONST_CONFLICT
,
531 // injectivity of seq.unit for disequality
532 // (seq.unit x) != (seq.unit y) => x != y, or
533 // (seq.unit x) != (seq.unit c) => x != c
534 STRINGS_UNIT_INJ_DEQ
,
535 // A split due to cardinality
537 // The cardinality inference for strings, see Liang et al CAV 2014.
539 //-------------------- core solver
540 // A cycle in the empty string equivalence class, e.g.:
541 // x ++ y = "" => x = ""
542 // This is typically not applied due to length constraints implying emptiness.
544 // A cycle in the containment ordering.
545 // x = y ++ x => y = "" or
546 // x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
547 // This is typically not applied due to length constraints implying emptiness.
549 // Flat form constant
550 // x = y ^ x = z ++ c ... ^ y = z ++ d => false
551 // where c and d are distinct constants.
554 // x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
555 // Notice flat form instances are similar to normal form inferences but do
556 // not involve recursive explanations.
558 // Flat form endpoint empty
559 // x = y ^ x = z ^ y = z ++ y' => y' = ""
560 STRINGS_F_ENDPOINT_EMP
,
561 // Flat form endpoint equal
562 // x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
563 STRINGS_F_ENDPOINT_EQ
,
564 // Flat form not contained
565 // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
567 // Normal form equality conflict
568 // x = N[x] ^ y = N[y] ^ x=y => false
569 // where Rewriter::rewrite(N[x]=N[y]) = false.
571 // Given two normal forms, infers that the remainder one of them has to be
572 // empty. For example:
573 // If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
574 STRINGS_N_ENDPOINT_EMP
,
575 // Given two normal forms, infers that two components have to be the same if
576 // they have the same length. For example:
577 // If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
579 // Given two normal forms, infers that the endpoints have to be the same. For
581 // If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
582 STRINGS_N_ENDPOINT_EQ
,
583 // Given two normal forms with constant endpoints, infers a conflict if the
584 // endpoints do not agree. For example:
585 // If "abc" ++ ... = "bc" ++ ... then conflict
587 // infer empty, for example:
589 // This is inferred when we encounter an x such that x = "" rewrites to a
590 // constant. This inference is used for instance when we otherwise would have
591 // split on the emptiness of x but the rewriter tells us the emptiness of x
594 // string split constant propagation, for example:
595 // x = y, x = "abc", y = y1 ++ "b" ++ y2
596 // implies y1 = "a" ++ y1'
597 STRINGS_SSPLIT_CST_PROP
,
598 // string split variable propagation, for example:
599 // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
600 // implies x1 = y1 ++ x1'
601 // This is inspired by Zheng et al CAV 2015.
602 STRINGS_SSPLIT_VAR_PROP
,
603 // length split, for example:
604 // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
605 // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
607 // length split empty, for example:
609 // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
610 STRINGS_LEN_SPLIT_EMP
,
611 // string split constant
612 // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
613 // implies y1 = "c" ++ y1'
614 // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
616 // string split variable, for example:
617 // x = y, x = x1 ++ x2, y = y1 ++ y2
618 // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
619 // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
621 // flat form loop, for example:
622 // x = y, x = x1 ++ z, y = z ++ y2
623 // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
624 // for fresh u, u1, u2.
625 // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
628 STRINGS_FLOOP_CONFLICT
,
629 // Normal form inference
630 // x = y ^ z = y => x = z
631 // This is applied when y is the normal form of both x and z.
633 // Normal form not contained, same as FFROM_NCTN but for normal forms
635 // Length normalization
636 // x = y => len( x ) = len( y )
637 // Typically applied when y is the normal form of x.
639 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
642 STRINGS_DEQ_DISL_EMP_SPLIT
,
643 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1, we apply the
645 // x = "a" v x != "a"
646 STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT
,
647 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != "", we apply the
649 // ni = x ++ x' ++ ... ^ nj = "abc" ++ y' ++ ... ^ x != "" --->
650 // x = k1 ++ k2 ^ len(k1) = 1 ^ (k1 != "a" v x = "a" ++ k2)
651 STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT
,
652 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y), we apply the
654 // ni = x ++ x' ++ ... ^ nj = y ++ y' ++ ... ^ ni != nj ^ len(x) != len(y)
656 // len(k1) = len(x) ^ len(k2) = len(y) ^ (y = k1 ++ k3 v x = k1 ++ k2)
657 STRINGS_DEQ_DISL_STRINGS_SPLIT
,
658 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y), we apply the
661 STRINGS_DEQ_STRINGS_EQ
,
662 // When x ++ x' ++ ... != y ++ y' ++ ... and we do not know how the lengths
663 // of x and y compare, we apply the inference:
664 // len(x) = len(y) v len(x) != len(y)
666 // When px ++ x ++ ... != py ^ len(px ++ x ++ ...) = len(py), we apply the
667 // following inference that infers that the remainder of the longer normal
668 // form must be empty:
669 // ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
671 STRINGS_DEQ_NORM_EMP
,
672 // When two strings are disequal s != t and the comparison of their lengths
673 // is unknown, we apply the inference:
674 // len(s) != len(t) V len(s) = len(t)
675 STRINGS_DEQ_LENGTH_SP
,
676 // Disequality extensionality
677 // x != y => ( seq.len(x) != seq.len(y) or
678 // ( seq.nth(x, d) != seq.nth(y, d) ^ 0 <= d < seq.len(x) ) )
679 STRINGS_DEQ_EXTENSIONALITY
,
680 //-------------------- codes solver
681 // str.to_code( v ) = rewrite( str.to_code(c) )
682 // where v is the proxy variable for c.
684 // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
686 //-------------------- sequence update solver
688 STRINGS_ARRAY_UPDATE_UNIT
,
689 // update over conatenation
690 STRINGS_ARRAY_UPDATE_CONCAT
,
692 STRINGS_ARRAY_NTH_UNIT
,
693 // nth over conatenation
694 STRINGS_ARRAY_NTH_CONCAT
,
695 //-------------------- regexp solver
696 // regular expression normal form conflict
697 // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
698 // where y is the normal form computed for x.
699 STRINGS_RE_NF_CONFLICT
,
700 // regular expression unfolding
701 // This is a general class of inferences of the form:
703 // where F is formula expressing the next step of checking whether x is in
706 // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
707 STRINGS_RE_UNFOLD_POS
,
708 // Same as above, for negative memberships
709 STRINGS_RE_UNFOLD_NEG
,
710 // intersection inclusion conflict
711 // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]]
712 // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
713 STRINGS_RE_INTER_INCLUDE
,
714 // intersection conflict, using regexp intersection computation
715 // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]]
716 STRINGS_RE_INTER_CONF
,
717 // intersection inference
718 // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
719 STRINGS_RE_INTER_INFER
,
720 // regular expression delta
721 // (x = "" ^ x in R) => C
722 // where "" in R holds if and only if C holds.
724 // regular expression delta conflict
725 // (x = "" ^ x in R) => false
726 // where R does not accept the empty string.
727 STRINGS_RE_DELTA_CONF
,
728 // regular expression derive ???
730 //-------------------- extended function solver
731 // Standard extended function inferences from context-dependent rewriting
732 // produced by constant substitutions. See Reynolds et al CAV 2017. These are
733 // inferences of the form:
734 // X = Y => f(X) = t when rewrite( f(Y) ) = t
735 // where X = Y is a vector of equalities, where some of Y may be constants.
737 // Same as above, for normal form substitutions.
739 // Decompositions based on extended function inferences from context-dependent
740 // rewriting produced by constant substitutions. This is like the above, but
741 // handles cases where the inferred predicate is not necessarily an equality
742 // involving f(X). For example:
743 // x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
744 // This is generally only inferred if contains( y, "B" ) is a known term in
745 // the current context.
747 // Same as above, for normal form substitutions.
749 // Extended function equality rewrite. This is an inference of the form:
751 // where P is a predicate implied by rewrite( t = s ).
752 // Typically, t is an application of an extended function and s is a constant.
753 // It is generally only inferred if P is a predicate over known terms.
755 // contain transitive
756 // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
759 // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
760 // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
761 STRINGS_CTN_DECOMPOSE
,
763 // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
764 STRINGS_CTN_NEG_EQUAL
,
766 // str.contains( x, y ) => x = w1 ++ y ++ w2
767 // where w1 and w2 are skolem variables.
769 // All reduction inferences of the form:
770 // f(x1, .., xn) = y ^ P(x1, ..., xn, y)
771 // where f is an extended function, y is the purification variable for
772 // f(x1, .., xn) and P is the reduction predicate for f
773 // (see theory_strings_preprocess).
775 //-------------------- prefix conflict
776 // prefix conflict (coarse-grained)
777 STRINGS_PREFIX_CONFLICT
,
778 //-------------------- other
779 // a lemma added during term registration for an atomic term
780 STRINGS_REGISTER_TERM_ATOMIC
,
781 // a lemma added during term registration
782 STRINGS_REGISTER_TERM
,
783 // a split during collect model info
785 //-------------------------------------- end strings theory
787 //-------------------------------------- uf theory
788 // Clause from the uf symmetry breaker
790 //-------------------- cardinality extension to UF
791 // The inferences below are described in Reynolds' thesis 2013.
792 // conflict of the form (card_T n) => (not (distinct t1 ... tn))
794 // conflict of the form (not (card_T1 n1)) ^ ... (not (card_Tk nk)) ^ (card n)
795 // where n1 + ... + nk >= n, where (card n) is a combined cardinality
798 // (not (card_T n)) => (distinct t1 ... tn)
799 UF_CARD_ENFORCE_NEGATIVE
,
800 // used to make the index terms in cardinality constraints equal
802 // conflict of the form (not (card_T1 n)) ^ (card_T2 m) where the cardinality
803 // of T2 can be assumed to be without loss of generality larger than T1 due to
804 // monotonicity reasoning (Claessen et al 2011).
805 UF_CARD_MONOTONE_COMBINED
,
806 // conflict of the form (not (card_T n)) ^ (card_T m) where n>m
807 UF_CARD_SIMPLE_CONFLICT
,
808 // equality split requested by cardinality solver
809 // (or (= t1 t2) (not (= t1 t2))
810 // to satisfy the cardinality constraints on the type of t1, t2.
812 //-------------------- end cardinality extension to UF
813 //-------------------- HO extension to UF
814 // Encodes an n-ary application as a chain of binary HO_APPLY applications
815 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
817 // A lemma corresponding to the definition of a skolem k used to convert
818 // HO_APPLY terms to APPLY_UF terms. This is of the form:
819 // (forall x1 ... xn) (@ (@ k x1) ... xn) = t
820 // where notice that t is a function whose free variables (if any) are
822 UF_HO_APP_CONV_SKOLEM
,
823 // Adds an extensionality lemma to witness that disequal functions have
824 // different applications
825 // (not (= (f sk1 .. skn) (g sk1 .. skn))
826 UF_HO_EXTENSIONALITY
,
827 //-------------------- model-construction specific part
828 // These rules are necessary to ensure that we build models properly. For more
829 // details see Section 3.3 of Barbosa et al. CADE'19.
831 // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
832 // equivalent by adding the equality as a lemma
833 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
834 UF_HO_MODEL_APP_ENCODE
,
835 // Adds an extensionality lemma to witness that disequal functions have
836 // different applications
837 // (not (= (f sk1 .. skn) (g sk1 .. skn))
838 UF_HO_MODEL_EXTENSIONALITY
,
839 //-------------------- end model-construction specific part
840 //-------------------- end HO extension to UF
841 //-------------------------------------- end uf theory
843 //-------------------------------------- unknown
848 * Converts an inference to a string. Note: This function is also used in
849 * `safe_print()`. Changing this functions name or signature will result in
850 * `safe_print()` printing "<unsupported>" instead of the proper strings for
853 * @param i The inference
854 * @return The name of the inference
856 const char* toString(InferenceId i
);
859 * Writes an inference name to a stream.
861 * @param out The stream to write to
862 * @param i The inference to write to the stream
865 std::ostream
& operator<<(std::ostream
& out
, InferenceId i
);
867 /** Make node from inference id */
868 Node
mkInferenceIdNode(InferenceId i
);
870 /** get an inference identifier from a node, return false if we fail */
871 bool getInferenceId(TNode n
, InferenceId
& i
);
873 } // namespace theory
876 #endif /* CVC5__THEORY__INFERENCE_H */