* (2) SCOPE, which closes the scope of assumptions.
* The core rules additionally correspond to generic operations that are done
* internally on nodes, e.g. calling Rewriter::rewrite.
+ *
+ * Rules with prefix MACRO_ are those that can be defined in terms of other
+ * rules. These exist for convienience. We provide their definition in the line
+ * "Macro:".
*/
enum class PfRule : uint32_t
{
// where F' and G' are the result of each side of the equation above. Here,
// original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
MACRO_SR_PRED_TRANSFORM,
-
//================================================= Processing rules
// ======== Remove Term Formulas Axiom
// Children: none
// the quantifiers rewriter involves constructing new bound variables that are
// not guaranteed to be consistent on each call.
THEORY_REWRITE,
- // The rules in this section have the signature of a "trusted rule":
+ // The remaining rules in this section have the signature of a "trusted rule":
//
// Children: none
// Arguments: (F)
// ---------------------
// Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
// where
- // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
- // r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
+ // r_t = (skolem (suf t1 (str.len s1)))),
+ // r_s = (skolem (suf s1 (str.len t1)))).
//
// or the reverse form of the above:
//
// ---------------------
// Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
// where
- // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
- // s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
- // (str.len t2))))).
+ // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))),
+ // r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))).
//
// Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
// (pre x n) is shorthand for (str.substr x 0 n).
// ---------------------
// Conclusion: (= t1 (str.++ c r))
// where
- // r = (witness ((z String)) (= z (suf t1 1))).
+ // r = (skolem (suf t1 1)).
//
// or the reverse form of the above:
//
// ---------------------
// Conclusion: (= t2 (str.++ r c))
// where
- // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
+ // r = (skolem (pre t2 (- (str.len t2) 1))).
CONCAT_CSPLIT,
// ======== Concat length propagate
// Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
// ---------------------
// Conclusion: (= t1 (str.++ s1 r_t))
// where
- // r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
+ // r_t = (skolem (suf t1 (str.len s1)))
//
// or the reverse form of the above:
//
// ---------------------
// Conclusion: (= t2 (str.++ r_t s2))
// where
- // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
- // s2))))).
+ // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))).
CONCAT_LPROP,
// ======== Concat constant propagate
// Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
// w3 is (pre w2 p),
// w4 is (suf w2 p),
// p = Word::overlap((suf w2 1), w1),
- // r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
+ // r = (skolem (suf t1 (str.len w3))).
// In other words, w4 is the largest suffix of (suf w2 1) that can contain a
// prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
//
// w3 is (suf w2 (- (str.len w2) p)),
// w4 is (pre w2 (- (str.len w2) p)),
// p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
- // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
+ // r = (skolem (pre t2 (- (str.len t2) (str.len w3)))).
// In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
// that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
// be contained in t2.
// ---------------------
// Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
// where
- // w1 is (witness ((z String)) (= z (pre t n)))
- // w2 is (witness ((z String)) (= z (suf t n)))
+ // w1 is (skolem (pre t n))
+ // w2 is (skolem (suf t n))
STRING_DECOMPOSE,
// ======== Length positive
// Children: none
// Arguments: (t)
// ---------------------
- // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
+ // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
STRING_LENGTH_POS,
// ======== Length non-empty
// Children: (P1:(not (= t "")))
// Conclusion: (and R (= t w))
// where w = strings::StringsPreprocess::reduce(t, R, ...).
// In other words, R is the reduction predicate for extended term t, and w is
- // (witness ((z T)) (= z t))
+ // (skolem t)
// Notice that the free variables of R are w and the free variables of t.
STRING_REDUCTION,
// ======== Eager Reduction
// Children: none
- // Arguments: (t, id?)
+ // Arguments: (t)
// ---------------------
// Conclusion: R
- // where R = strings::TermRegistry::eagerReduce(t, id).
+ // where R = strings::TermRegistry::eagerReduce(t).
STRING_EAGER_REDUCTION,
//======================== Regular expressions
// ======== Regular expression intersection
// ---------------------
// Conclusion: (<= i greatestIntLessThan(c)})
INT_TIGHT_UB,
-
// ======== Tightening Strict Integer Lower Bounds
// Children: (P:(> i c))
// where i has integer type.
// ---------------------
// Conclusion: (>= i leastIntGreaterThan(c)})
INT_TIGHT_LB,
-
// ======== Trichotomy of the reals
// Children: (A B)
// Arguments: (C)
// note that "not" here denotes arithmetic negation, flipping
// >= to <, etc.
ARITH_TRICHOTOMY,
-
// ======== Arithmetic operator elimination
// Children: none
// Arguments: (t)
// ---------------------
// Conclusion: arith::OperatorElim::getAxiomFor(t)
ARITH_OP_ELIM_AXIOM,
-
// ======== Int Trust
// Children: (P1 ... Pn)
// Arguments: (Q)
// Conclusion: (and (>= real.pi l) (<= real.pi u))
// Where l (u) is a valid lower (upper) bound on pi.
ARITH_TRANS_PI,
-
//======== Exp at negative values
// Children: none
// Arguments: (t)
// exponential function is the following:
// e^x = \sum_{n=0}^{\infty} x^n / n!
ARITH_TRANS_EXP_APPROX_BELOW,
-
//======== Sine is always between -1 and 1
// Children: none
// Arguments: (t)
projects / cvc5.git / commitdiff