1 /********************* */
2 /*! \file inference_id.h
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
12 ** \brief Inference enumeration.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__INFERENCE_ID_H
18 #define CVC4__THEORY__INFERENCE_ID_H
23 #include "util/safe_print.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 // simple congruence x=y => f(x)=f(y)
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)
51 // based on sign (NlSolver::checkMonomialSign)
53 // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
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)
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
,
72 // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
73 ARITH_NL_T_MONOTONICITY
,
74 // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
76 // secant refinement, the dual of the above inference
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
100 ARRAYS_READ_OVER_WRITE
,
101 ARRAYS_READ_OVER_WRITE_1
,
102 ARRAYS_READ_OVER_WRITE_CONTRA
,
104 BAG_NON_NEGATIVE_COUNT
,
105 BAG_MK_BAG_SAME_ELEMENT
,
112 BAG_INTERSECTION_MIN
,
113 BAG_DIFFERENCE_SUBTRACT
,
114 BAG_DIFFERENCE_REMOVE
,
115 BAG_DUPLICATE_REMOVAL
,
117 // (= (C t1 ... tn) (C s1 .. sn)) => (= ti si)
119 // ((_ is Ci) t) => (= t (Ci (sel_1 t) ... (sel_n t)))
121 // (or ((_ is C1) t) V ... V ((_ is Cn) t))
123 // (not ((_ is C1) t)) ^ ... [j] ... ^ (not ((_ is Cn) t)) => ((_ is Cj) t)
125 // (= t (Ci t1 ... tn)) => (= (sel_j t) rewrite((sel_j (Ci t1 ... tn))))
126 DATATYPES_COLLAPSE_SEL
,
127 // (= (Ci t1...tn) (Cj t1...tn)) => false
128 DATATYPES_CLASH_CONFLICT
,
129 // ((_ is Ci) t) ^ (= t (Cj t1 ... tn)) => false
130 DATATYPES_TESTER_CONFLICT
,
131 // ((_ is Ci) t) ^ ((_ is Cj) s) ^ (= t s) => false
132 DATATYPES_TESTER_MERGE_CONFLICT
,
133 // bisimilarity for codatatypes
135 // cycle conflict for datatypes
138 // ensures that pto is a function: (pto x y) ^ ~(pto z w) ^ x = z => y != w
140 // enforces injectiveness of pto: (pto x y) ^ (pto y w) ^ x = y => y = w
143 //-------------------------------------- base solver
144 // initial normalize singular
145 // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" =>
146 // x1 ++ ... ++ xn = xi
148 // initial constant merge
149 // explain_constant(x, c) => x = c
150 // Above, explain_constant(x,c) is a basic explanation of why x must be equal
151 // to string constant c, which is computed by taking arguments of
152 // concatenation terms that are entailed to be constants. For example:
153 // ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
154 STRINGS_I_CONST_MERGE
,
155 // initial constant conflict
156 // ( explain_constant(x, c1) ^ explain_constant(x, c2) ^ x = y) => false
158 STRINGS_I_CONST_CONFLICT
,
160 // Given two concatenation terms, this is applied when we find that they are
161 // equal after e.g. removing strings that are currently empty. For example:
162 // y = "" ^ z = "" => x ++ y = z ++ x
164 // injectivity of seq.unit
165 // (seq.unit x) = (seq.unit y) => x=y, or
166 // (seq.unit x) = (seq.unit c) => x=c
168 // unit constant conflict
169 // (seq.unit x) = C => false if |C| != 1.
170 STRINGS_UNIT_CONST_CONFLICT
,
171 // injectivity of seq.unit for disequality
172 // (seq.unit x) != (seq.unit y) => x != y, or
173 // (seq.unit x) != (seq.unit c) => x != c
174 STRINGS_UNIT_INJ_DEQ
,
175 // A split due to cardinality
177 // The cardinality inference for strings, see Liang et al CAV 2014.
179 //-------------------------------------- end base solver
180 //-------------------------------------- core solver
181 // A cycle in the empty string equivalence class, e.g.:
182 // x ++ y = "" => x = ""
183 // This is typically not applied due to length constraints implying emptiness.
185 // A cycle in the containment ordering.
186 // x = y ++ x => y = "" or
187 // x = y ++ z ^ y = x ++ w => z = "" ^ w = ""
188 // This is typically not applied due to length constraints implying emptiness.
190 // Flat form constant
191 // x = y ^ x = z ++ c ... ^ y = z ++ d => false
192 // where c and d are distinct constants.
195 // x = y ^ x = z ++ x' ... ^ y = z ++ y' ^ len(x') = len(y') => x' = y'
196 // Notice flat form instances are similar to normal form inferences but do
197 // not involve recursive explanations.
199 // Flat form endpoint empty
200 // x = y ^ x = z ^ y = z ++ y' => y' = ""
201 STRINGS_F_ENDPOINT_EMP
,
202 // Flat form endpoint equal
203 // x = y ^ x = z ++ x' ^ y = z ++ y' => x' = y'
204 STRINGS_F_ENDPOINT_EQ
,
205 // Flat form not contained
206 // x = c ^ x = y => false when rewrite( contains( y, c ) ) = false
208 // Normal form equality conflict
209 // x = N[x] ^ y = N[y] ^ x=y => false
210 // where Rewriter::rewrite(N[x]=N[y]) = false.
212 // Given two normal forms, infers that the remainder one of them has to be
213 // empty. For example:
214 // If x1 ++ x2 = y1 and x1 = y1, then x2 = ""
215 STRINGS_N_ENDPOINT_EMP
,
216 // Given two normal forms, infers that two components have to be the same if
217 // they have the same length. For example:
218 // If x1 ++ x2 = x3 ++ x4 and len(x1) = len(x3) then x1 = x3
220 // Given two normal forms, infers that the endpoints have to be the same. For
222 // If x1 ++ x2 = x3 ++ x4 ++ x5 and x1 = x3 then x2 = x4 ++ x5
223 STRINGS_N_ENDPOINT_EQ
,
224 // Given two normal forms with constant endpoints, infers a conflict if the
225 // endpoints do not agree. For example:
226 // If "abc" ++ ... = "bc" ++ ... then conflict
228 // infer empty, for example:
230 // This is inferred when we encounter an x such that x = "" rewrites to a
231 // constant. This inference is used for instance when we otherwise would have
232 // split on the emptiness of x but the rewriter tells us the emptiness of x
235 // string split constant propagation, for example:
236 // x = y, x = "abc", y = y1 ++ "b" ++ y2
237 // implies y1 = "a" ++ y1'
238 STRINGS_SSPLIT_CST_PROP
,
239 // string split variable propagation, for example:
240 // x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
241 // implies x1 = y1 ++ x1'
242 // This is inspired by Zheng et al CAV 2015.
243 STRINGS_SSPLIT_VAR_PROP
,
244 // length split, for example:
245 // len( x1 ) = len( y1 ) V len( x1 ) != len( y1 )
246 // This is inferred when e.g. x = y, x = x1 ++ x2, y = y1 ++ y2.
248 // length split empty, for example:
250 // This is inferred when, e.g. x = y, x = z ++ x1, y = y1 ++ z
251 STRINGS_LEN_SPLIT_EMP
,
252 // string split constant
253 // x = y, x = "c" ++ x2, y = y1 ++ y2, y1 != ""
254 // implies y1 = "c" ++ y1'
255 // This is a special case of F-Split in Figure 5 of Liang et al CAV 2014.
257 // string split variable, for example:
258 // x = y, x = x1 ++ x2, y = y1 ++ y2
259 // implies x1 = y1 ++ x1' V y1 = x1 ++ y1'
260 // This is rule F-Split in Figure 5 of Liang et al CAV 2014.
262 // flat form loop, for example:
263 // x = y, x = x1 ++ z, y = z ++ y2
264 // implies z = u2 ++ u1, u in ( u1 ++ u2 )*, x1 = u2 ++ u, y2 = u ++ u1
265 // for fresh u, u1, u2.
266 // This is the rule F-Loop from Figure 5 of Liang et al CAV 2014.
269 STRINGS_FLOOP_CONFLICT
,
270 // Normal form inference
271 // x = y ^ z = y => x = z
272 // This is applied when y is the normal form of both x and z.
274 // Normal form not contained, same as FFROM_NCTN but for normal forms
276 // Length normalization
277 // x = y => len( x ) = len( y )
278 // Typically applied when y is the normal form of x.
280 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != len(y), we apply the
283 STRINGS_DEQ_DISL_EMP_SPLIT
,
284 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) = 1, we apply the
286 // x = "a" v x != "a"
287 STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT
,
288 // When x ++ x' ++ ... != "abc" ++ y' ++ ... ^ len(x) != "", we apply the
290 // ni = x ++ x' ++ ... ^ nj = "abc" ++ y' ++ ... ^ x != "" --->
291 // x = k1 ++ k2 ^ len(k1) = 1 ^ (k1 != "a" v x = "a" ++ k2)
292 STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT
,
293 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) != len(y), we apply the
295 // ni = x ++ x' ++ ... ^ nj = y ++ y' ++ ... ^ ni != nj ^ len(x) != len(y)
297 // len(k1) = len(x) ^ len(k2) = len(y) ^ (y = k1 ++ k3 v x = k1 ++ k2)
298 STRINGS_DEQ_DISL_STRINGS_SPLIT
,
299 // When x ++ x' ++ ... != y ++ y' ++ ... ^ len(x) = len(y), we apply the
302 STRINGS_DEQ_STRINGS_EQ
,
303 // When x ++ x' ++ ... != y ++ y' ++ ... and we do not know how the lengths
304 // of x and y compare, we apply the inference:
305 // len(x) = len(y) v len(x) != len(y)
307 // When px ++ x ++ ... != py ^ len(px ++ x ++ ...) = len(py), we apply the
308 // following inference that infers that the remainder of the longer normal
309 // form must be empty:
310 // ni = px ++ x ++ ... ^ nj = py ^ len(ni) = len(nj) --->
312 STRINGS_DEQ_NORM_EMP
,
313 // When two strings are disequal s != t and the comparison of their lengths
314 // is unknown, we apply the inference:
315 // len(s) != len(t) V len(s) = len(t)
316 STRINGS_DEQ_LENGTH_SP
,
317 //-------------------------------------- end core solver
318 //-------------------------------------- codes solver
319 // str.to_code( v ) = rewrite( str.to_code(c) )
320 // where v is the proxy variable for c.
322 // str.code(x) = -1 V str.code(x) != str.code(y) V x = y
324 //-------------------------------------- end codes solver
325 //-------------------------------------- regexp solver
326 // regular expression normal form conflict
327 // ( x in R ^ x = y ^ rewrite((str.in_re y R)) = false ) => false
328 // where y is the normal form computed for x.
329 STRINGS_RE_NF_CONFLICT
,
330 // regular expression unfolding
331 // This is a general class of inferences of the form:
333 // where F is formula expressing the next step of checking whether x is in
336 // x = "" V x in R V ( x = x1 ++ x2 ++ x3 ^ x1 in R ^ x2 in (R)* ^ x3 in R)
337 STRINGS_RE_UNFOLD_POS
,
338 // Same as above, for negative memberships
339 STRINGS_RE_UNFOLD_NEG
,
340 // intersection inclusion conflict
341 // (x in R1 ^ ~ x in R2) => false where [[includes(R2,R1)]]
342 // Where includes(R2,R1) is a heuristic check for whether R2 includes R1.
343 STRINGS_RE_INTER_INCLUDE
,
344 // intersection conflict, using regexp intersection computation
345 // (x in R1 ^ x in R2) => false where [[intersect(R1, R2) = empty]]
346 STRINGS_RE_INTER_CONF
,
347 // intersection inference
348 // (x in R1 ^ y in R2 ^ x = y) => (x in re.inter(R1,R2))
349 STRINGS_RE_INTER_INFER
,
350 // regular expression delta
351 // (x = "" ^ x in R) => C
352 // where "" in R holds if and only if C holds.
354 // regular expression delta conflict
355 // (x = "" ^ x in R) => false
356 // where R does not accept the empty string.
357 STRINGS_RE_DELTA_CONF
,
358 // regular expression derive ???
360 //-------------------------------------- end regexp solver
361 //-------------------------------------- extended function solver
362 // Standard extended function inferences from context-dependent rewriting
363 // produced by constant substitutions. See Reynolds et al CAV 2017. These are
364 // inferences of the form:
365 // X = Y => f(X) = t when rewrite( f(Y) ) = t
366 // where X = Y is a vector of equalities, where some of Y may be constants.
368 // Same as above, for normal form substitutions.
370 // Decompositions based on extended function inferences from context-dependent
371 // rewriting produced by constant substitutions. This is like the above, but
372 // handles cases where the inferred predicate is not necessarily an equality
373 // involving f(X). For example:
374 // x = "A" ^ contains( y ++ x, "B" ) => contains( y, "B" )
375 // This is generally only inferred if contains( y, "B" ) is a known term in
376 // the current context.
378 // Same as above, for normal form substitutions.
380 // Extended function equality rewrite. This is an inference of the form:
382 // where P is a predicate implied by rewrite( t = s ).
383 // Typically, t is an application of an extended function and s is a constant.
384 // It is generally only inferred if P is a predicate over known terms.
386 // contain transitive
387 // ( str.contains( s, t ) ^ ~contains( s, r ) ) => ~contains( t, r ).
390 // str.contains( x, str.++( y1, ..., yn ) ) => str.contains( x, yi ) or
391 // ~str.contains( str.++( x1, ..., xn ), y ) => ~str.contains( xi, y )
392 STRINGS_CTN_DECOMPOSE
,
394 // ( len( x ) = len( s ) ^ ~contains( x, s ) ) => x != s
395 STRINGS_CTN_NEG_EQUAL
,
397 // str.contains( x, y ) => x = w1 ++ y ++ w2
398 // where w1 and w2 are skolem variables.
400 // All reduction inferences of the form:
401 // f(x1, .., xn) = y ^ P(x1, ..., xn, y)
402 // where f is an extended function, y is the purification variable for
403 // f(x1, .., xn) and P is the reduction predicate for f
404 // (see theory_strings_preprocess).
406 //-------------------------------------- end extended function solver
407 //-------------------------------------- prefix conflict
408 // prefix conflict (coarse-grained)
409 STRINGS_PREFIX_CONFLICT
,
410 //-------------------------------------- end prefix conflict
412 // Clause from the uf symmetry breaker
416 UF_CARD_ENFORCE_NEGATIVE
,
418 UF_CARD_MONOTONE_COMBINED
,
419 UF_CARD_SIMPLE_CONFLICT
,
421 //-------------------------------------- begin HO extension to UF
422 // Encodes an n-ary application as a chain of binary HO_APPLY applications
423 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
425 UF_HO_APP_CONV_SKOLEM
,
426 // Adds an extensionality lemma to witness that disequal functions have
427 // different applications
428 // (not (= (f sk1 .. skn) (g sk1 .. skn))
429 UF_HO_EXTENSIONALITY
,
430 //-------------------------------------- begin model-construction specific part
431 // These rules are necessary to ensure that we build models properly. For more
432 // details see Section 3.3 of Barbosa et al. CADE'19.
434 // Enforces that a regular APPLY_UF term in the model is equal to its HO_APPLY
435 // equivalent by adding the equality as a lemma
436 // (= (f t1 ... tn) (@ (@ ... (@ f t1) ...) tn))
437 UF_HO_MODEL_APP_ENCODE
,
438 // Adds an extensionality lemma to witness that disequal functions have
439 // different applications
440 // (not (= (f sk1 .. skn) (g sk1 .. skn))
441 UF_HO_MODEL_EXTENSIONALITY
,
442 //-------------------------------------- end model-construction specific part
443 //-------------------------------------- end HO extension to UF
449 * Converts an inference to a string. Note: This function is also used in
450 * `safe_print()`. Changing this functions name or signature will result in
451 * `safe_print()` printing "<unsupported>" instead of the proper strings for
454 * @param i The inference
455 * @return The name of the inference
457 const char* toString(InferenceId i
);
460 * Writes an inference name to a stream.
462 * @param out The stream to write to
463 * @param i The inference to write to the stream
466 std::ostream
& operator<<(std::ostream
& out
, InferenceId i
);
468 } // namespace theory
471 #endif /* CVC4__THEORY__INFERENCE_H */