Public Member Functions | |
Expr | simplify () throws Z3Exception |
Expr | simplify (Params p) throws Z3Exception |
FuncDecl | getFuncDecl () throws Z3Exception |
Z3_lbool | getBoolValue () throws Z3Exception |
int | getNumArgs () throws Z3Exception |
Expr[] | getArgs () throws Z3Exception |
void | update (Expr[] args) throws Z3Exception |
Expr | substitute (Expr[] from, Expr[] to) throws Z3Exception |
Expr | substitute (Expr from, Expr to) throws Z3Exception |
Expr | substituteVars (Expr[] to) throws Z3Exception |
Expr | translate (Context ctx) throws Z3Exception |
String | toString () |
boolean | isNumeral () throws Z3Exception |
boolean | isWellSorted () throws Z3Exception |
Sort | getSort () throws Z3Exception |
boolean | isConst () throws Z3Exception |
boolean | isIntNum () throws Z3Exception |
boolean | isRatNum () throws Z3Exception |
boolean | isAlgebraicNumber () throws Z3Exception |
boolean | isBool () throws Z3Exception |
boolean | isTrue () throws Z3Exception |
boolean | isFalse () throws Z3Exception |
boolean | isEq () throws Z3Exception |
boolean | isDistinct () throws Z3Exception |
boolean | isITE () throws Z3Exception |
boolean | isAnd () throws Z3Exception |
boolean | isOr () throws Z3Exception |
boolean | isIff () throws Z3Exception |
boolean | isXor () throws Z3Exception |
boolean | isNot () throws Z3Exception |
boolean | isImplies () throws Z3Exception |
boolean | isInt () throws Z3Exception |
boolean | isReal () throws Z3Exception |
boolean | isArithmeticNumeral () throws Z3Exception |
boolean | isLE () throws Z3Exception |
boolean | isGE () throws Z3Exception |
boolean | isLT () throws Z3Exception |
boolean | isGT () throws Z3Exception |
boolean | isAdd () throws Z3Exception |
boolean | isSub () throws Z3Exception |
boolean | isUMinus () throws Z3Exception |
boolean | isMul () throws Z3Exception |
boolean | isDiv () throws Z3Exception |
boolean | isIDiv () throws Z3Exception |
boolean | isRemainder () throws Z3Exception |
boolean | isModulus () throws Z3Exception |
boolean | isIntToReal () throws Z3Exception |
boolean | isRealToInt () throws Z3Exception |
boolean | isRealIsInt () throws Z3Exception |
boolean | isArray () throws Z3Exception |
boolean | isStore () throws Z3Exception |
boolean | isSelect () throws Z3Exception |
boolean | isConstantArray () throws Z3Exception |
boolean | isDefaultArray () throws Z3Exception |
boolean | isArrayMap () throws Z3Exception |
boolean | isAsArray () throws Z3Exception |
boolean | isSetUnion () throws Z3Exception |
boolean | isSetIntersect () throws Z3Exception |
boolean | isSetDifference () throws Z3Exception |
boolean | isSetComplement () throws Z3Exception |
boolean | isSetSubset () throws Z3Exception |
boolean | isBV () throws Z3Exception |
boolean | isBVNumeral () throws Z3Exception |
boolean | isBVBitOne () throws Z3Exception |
boolean | isBVBitZero () throws Z3Exception |
boolean | isBVUMinus () throws Z3Exception |
boolean | isBVAdd () throws Z3Exception |
boolean | isBVSub () throws Z3Exception |
boolean | isBVMul () throws Z3Exception |
boolean | isBVSDiv () throws Z3Exception |
boolean | isBVUDiv () throws Z3Exception |
boolean | isBVSRem () throws Z3Exception |
boolean | isBVURem () throws Z3Exception |
boolean | isBVSMod () throws Z3Exception |
boolean | isBVULE () throws Z3Exception |
boolean | isBVSLE () throws Z3Exception |
boolean | isBVUGE () throws Z3Exception |
boolean | isBVSGE () throws Z3Exception |
boolean | isBVULT () throws Z3Exception |
boolean | isBVSLT () throws Z3Exception |
boolean | isBVUGT () throws Z3Exception |
boolean | isBVSGT () throws Z3Exception |
boolean | isBVAND () throws Z3Exception |
boolean | isBVOR () throws Z3Exception |
boolean | isBVNOT () throws Z3Exception |
boolean | isBVXOR () throws Z3Exception |
boolean | isBVNAND () throws Z3Exception |
boolean | isBVNOR () throws Z3Exception |
boolean | isBVXNOR () throws Z3Exception |
boolean | isBVConcat () throws Z3Exception |
boolean | isBVSignExtension () throws Z3Exception |
boolean | isBVZeroExtension () throws Z3Exception |
boolean | isBVExtract () throws Z3Exception |
boolean | isBVRepeat () throws Z3Exception |
boolean | isBVReduceOR () throws Z3Exception |
boolean | isBVReduceAND () throws Z3Exception |
boolean | isBVComp () throws Z3Exception |
boolean | isBVShiftLeft () throws Z3Exception |
boolean | isBVShiftRightLogical () throws Z3Exception |
boolean | isBVShiftRightArithmetic () throws Z3Exception |
boolean | isBVRotateLeft () throws Z3Exception |
boolean | isBVRotateRight () throws Z3Exception |
boolean | isBVRotateLeftExtended () throws Z3Exception |
boolean | isBVRotateRightExtended () throws Z3Exception |
boolean | isIntToBV () throws Z3Exception |
boolean | isBVToInt () throws Z3Exception |
boolean | isBVCarry () throws Z3Exception |
boolean | isBVXOR3 () throws Z3Exception |
boolean | isLabel () throws Z3Exception |
boolean | isLabelLit () throws Z3Exception |
boolean | isOEQ () throws Z3Exception |
boolean | isProofTrue () throws Z3Exception |
boolean | isProofAsserted () throws Z3Exception |
boolean | isProofGoal () throws Z3Exception |
boolean | isProofModusPonens () throws Z3Exception |
boolean | isProofReflexivity () throws Z3Exception |
boolean | isProofSymmetry () throws Z3Exception |
boolean | isProofTransitivity () throws Z3Exception |
boolean | isProofTransitivityStar () throws Z3Exception |
boolean | isProofMonotonicity () throws Z3Exception |
boolean | isProofQuantIntro () throws Z3Exception |
boolean | isProofDistributivity () throws Z3Exception |
boolean | isProofAndElimination () throws Z3Exception |
boolean | isProofOrElimination () throws Z3Exception |
boolean | isProofRewrite () throws Z3Exception |
boolean | isProofRewriteStar () throws Z3Exception |
boolean | isProofPullQuant () throws Z3Exception |
boolean | isProofPullQuantStar () throws Z3Exception |
boolean | isProofPushQuant () throws Z3Exception |
boolean | isProofElimUnusedVars () throws Z3Exception |
boolean | isProofDER () throws Z3Exception |
boolean | isProofQuantInst () throws Z3Exception |
boolean | isProofHypothesis () throws Z3Exception |
boolean | isProofLemma () throws Z3Exception |
boolean | isProofUnitResolution () throws Z3Exception |
boolean | isProofIFFTrue () throws Z3Exception |
boolean | isProofIFFFalse () throws Z3Exception |
boolean | isProofCommutativity () throws Z3Exception |
boolean | isProofDefAxiom () throws Z3Exception |
boolean | isProofDefIntro () throws Z3Exception |
boolean | isProofApplyDef () throws Z3Exception |
boolean | isProofIFFOEQ () throws Z3Exception |
boolean | isProofNNFPos () throws Z3Exception |
boolean | isProofNNFNeg () throws Z3Exception |
boolean | isProofNNFStar () throws Z3Exception |
boolean | isProofCNFStar () throws Z3Exception |
boolean | isProofSkolemize () throws Z3Exception |
boolean | isProofModusPonensOEQ () throws Z3Exception |
boolean | isProofTheoryLemma () throws Z3Exception |
boolean | isRelation () throws Z3Exception |
boolean | isRelationStore () throws Z3Exception |
boolean | isEmptyRelation () throws Z3Exception |
boolean | isIsEmptyRelation () throws Z3Exception |
boolean | isRelationalJoin () throws Z3Exception |
boolean | isRelationUnion () throws Z3Exception |
boolean | isRelationWiden () throws Z3Exception |
boolean | isRelationProject () throws Z3Exception |
boolean | isRelationFilter () throws Z3Exception |
boolean | isRelationNegationFilter () throws Z3Exception |
boolean | isRelationRename () throws Z3Exception |
boolean | isRelationComplement () throws Z3Exception |
boolean | isRelationSelect () throws Z3Exception |
boolean | isRelationClone () throws Z3Exception |
boolean | isFiniteDomain () throws Z3Exception |
boolean | isFiniteDomainLT () throws Z3Exception |
int | getIndex () throws Z3Exception |
![]() | |
boolean | equals (Object o) |
int | compareTo (Object other) throws Z3Exception |
int | hashCode () |
int | getId () throws Z3Exception |
AST | translate (Context ctx) throws Z3Exception |
Z3_ast_kind | getASTKind () throws Z3Exception |
boolean | isExpr () throws Z3Exception |
boolean | isApp () throws Z3Exception |
boolean | isVar () throws Z3Exception |
boolean | isQuantifier () throws Z3Exception |
boolean | isSort () throws Z3Exception |
boolean | isFuncDecl () throws Z3Exception |
String | toString () |
String | getSExpr () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Protected Member Functions | |
Expr (Context ctx) | |
Expr (Context ctx, long obj) throws Z3Exception | |
![]() | |
void | finalize () throws Z3Exception |
Constructor for Expr
|
inlineprotected |
Constructor for Expr
|
inline |
The arguments of the expression.
Definition at line 90 of file Expr.java.
Referenced by FuncInterp.toString().
|
inline |
|
inline |
The function declaration of the function that is applied in this expression.
Definition at line 63 of file Expr.java.
Referenced by Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.isBVSRem(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConst(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCNFStar(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), and Expr.isXor().
|
inline |
The de-Burijn index of a bound variable.
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.
The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.
Definition at line 1727 of file Expr.java.
|
inline |
The number of arguments of the expression.
Definition at line 82 of file Expr.java.
Referenced by Expr.getArgs(), Expr.isConst(), and Expr.update().
|
inline |
The Sort of the term.
Definition at line 206 of file Expr.java.
Referenced by BitVecExpr.getSortSize().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is of an array sort.
Definition at line 497 of file Expr.java.
|
inline |
Indicates whether the term is an array map.
It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.
Definition at line 545 of file Expr.java.
|
inline |
Indicates whether the term is an as-array term.
An as-array term is n array value that behaves as the function graph of the function passed as parameter.
Definition at line 555 of file Expr.java.
|
inline |
|
inline |
Indicates whether the terms is of bit-vector sort.
Definition at line 603 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a bit-vector extraction
Definition at line 894 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a bit-vector reduce AND
Definition at line 918 of file Expr.java.
|
inline |
|
inline |
|
inline |
Indicates whether the term is a bit-vector rotate left
Definition at line 958 of file Expr.java.
|
inline |
Indicates whether the term is a bit-vector rotate left (extended)
Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
Definition at line 976 of file Expr.java.
|
inline |
Indicates whether the term is a bit-vector rotate right
Definition at line 966 of file Expr.java.
|
inline |
Indicates whether the term is a bit-vector rotate right (extended)
Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
Definition at line 986 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a bit-vector sign extension
Definition at line 878 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a coercion from bit-vector to integer
This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
Definition at line 1008 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a bit-vector zero extension
Definition at line 886 of file Expr.java.
|
inline |
|
inline |
Indicates whether the term is a constant array.
For example, select(const(v),i) = v holds for every v and i. The function is unary.
Definition at line 527 of file Expr.java.
|
inline |
Indicates whether the term is a default array.
For example default(const(v)) = v. The function is unary.
Definition at line 536 of file Expr.java.
|
inline |
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
Definition at line 282 of file Expr.java.
|
inline |
|
inline |
Indicates whether the term is an empty relation
Definition at line 1574 of file Expr.java.
|
inline |
|
inline |
|
inline |
Indicates whether the term is of an array sort.
Definition at line 1696 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is an implication
Definition at line 339 of file Expr.java.
|
inline |
Indicates whether the term is of integer sort.
Definition at line 347 of file Expr.java.
Referenced by Expr.isIntNum().
|
inline |
|
inline |
Indicates whether the term is a coercion from integer to bit-vector
This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.
Definition at line 997 of file Expr.java.
|
inline |
Indicates whether the term is a coercion of integer to real (unary)
Definition at line 472 of file Expr.java.
|
inline |
Indicates whether the term is a test for the emptiness of a relation
Definition at line 1582 of file Expr.java.
|
inline |
|
inline |
|
inline |
Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
A label literal has a set of string parameters. It takes no arguments.
Definition at line 1048 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a numeral
Definition at line 188 of file Expr.java.
Referenced by Expr.isIntNum(), and Expr.isRatNum().
|
inline |
|
inline |
|
inline |
Indicates whether the term is a proof by elimination of AND
Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and l_1 ... l_n) [and-elim T1]: l_i
Definition at line 1194 of file Expr.java.
|
inline |
Indicates whether the term is a proof for application of a definition
[apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.
Definition at line 1424 of file Expr.java.
|
inline |
Indicates whether the term is a proof for a fact asserted by the user.
Definition at line 1074 of file Expr.java.
|
inline |
Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
Definition at line 1501 of file Expr.java.
|
inline |
Indicates whether the term is a proof by commutativity
[comm]: (= (f a b) (f b a))
f is a commutative operator.
This proof object has no antecedents. Remark: if f is bool, then = is iff.
Definition at line 1370 of file Expr.java.
|
inline |
Indicates whether the term is a proof for Tseitin-like axioms
Proof object used to justify Tseitin's like axioms:
(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)
This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).
Definition at line 1393 of file Expr.java.
|
inline |
Indicates whether the term is a proof for introduction of a name
Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:
When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n) e))
or: [def-intro]: (or (not n) e) when e only occurs positively.
When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))
Otherwise: [def-intro]: (= n e)
Definition at line 1414 of file Expr.java.
|
inline |
Indicates whether the term is a proof for destructive equality resolution
A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.
This proof object has no antecedents.
Several variables can be eliminated simultaneously.
Definition at line 1297 of file Expr.java.
|
inline |
Indicates whether the term is a distributivity proof object.
Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.
This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.
Definition at line 1184 of file Expr.java.
|
inline |
Indicates whether the term is a proof for elimination of unused variables.
A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))
It is used to justify the elimination of unused variables. This proof object has no antecedents.
Definition at line 1283 of file Expr.java.
|
inline |
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
Definition at line 1083 of file Expr.java.
|
inline |
Indicates whether the term is a hypthesis marker.
Mark a hypothesis in a natural deduction style proof.
Definition at line 1315 of file Expr.java.
|
inline |
Indicates whether the term is a proof by iff-false
T1: (not p) [iff-false T1]: (iff p false)
Definition at line 1356 of file Expr.java.
|
inline |
Indicates whether the term is a proof iff-oeq
T1: (iff p q) [iff~ T1]: (~ p q)
Definition at line 1433 of file Expr.java.
|
inline |
Indicates whether the term is a proof by iff-true
T1: p [iff-true T1]: (iff p true)
Definition at line 1347 of file Expr.java.
|
inline |
Indicates whether the term is a proof by lemma
T1: false [lemma T1]: (or (not l_1) ... (not l_n))
This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.
Definition at line 1328 of file Expr.java.
|
inline |
Indicates whether the term is proof via modus ponens
Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).
Definition at line 1094 of file Expr.java.
|
inline |
Indicates whether the term is a proof by modus ponens for equi-satisfiability.
Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q
Definition at line 1525 of file Expr.java.
|
inline |
Indicates whether the term is a monotonicity proof object.
T1: (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space.
Definition at line 1158 of file Expr.java.
|
inline |
Indicates whether the term is a proof for a negative NNF step
Proof for a (negative) NNF step. Examples:
T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))
Definition at line 1474 of file Expr.java.
|
inline |
Indicates whether the term is a proof for a positive NNF step
Proof for a (positive) NNF step. Example:
T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'
r_2)))
The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.
Definition at line 1458 of file Expr.java.
|
inline |
Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
A proof for (~ P Q) where Q is in negation normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
Definition at line 1489 of file Expr.java.
|
inline |
Indicates whether the term is a proof by eliminiation of not-or
Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)
Definition at line 1204 of file Expr.java.
|
inline |
Indicates whether the term is a proof for pulling quantifiers out.
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
Definition at line 1247 of file Expr.java.
|
inline |
Indicates whether the term is a proof for pulling quantifiers out.
A proof for (iff P Q) where Q is in prenex normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents
Definition at line 1258 of file Expr.java.
|
inline |
Indicates whether the term is a proof for pushing quantifiers in.
A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents
Definition at line 1270 of file Expr.java.
|
inline |
Indicates whether the term is a proof for quantifier instantiation
A proof of (or (not (forall (x) (P x))) (P a))
Definition at line 1306 of file Expr.java.
|
inline |
Indicates whether the term is a quant-intro proof
Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))
Definition at line 1168 of file Expr.java.
|
inline |
Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.
Definition at line 1106 of file Expr.java.
|
inline |
Indicates whether the term is a proof by rewriting
A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.
This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.
Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)
Definition at line 1221 of file Expr.java.
|
inline |
Indicates whether the term is a proof by rewriting
A proof for rewriting an expression t into an expression s. This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
Definition at line 1237 of file Expr.java.
|
inline |
Indicates whether the term is a proof for a Skolemization step
Proof for:
(p x y)) (p (sk y) y))
This proof object has no antecedents.
Definition at line 1515 of file Expr.java.
|
inline |
Indicates whether the term is proof by symmetricity of a relation
Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the antecedent of this proof object.
Definition at line 1117 of file Expr.java.
|
inline |
Indicates whether the term is a proof for theory lemma
Generic proof for theory lemmas.
The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
Definition at line 1544 of file Expr.java.
|
inline |
Indicates whether the term is a proof by transitivity of a relation
Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u)
Definition at line 1128 of file Expr.java.
|
inline |
Indicates whether the term is a proof by condensed transitivity of a relation
Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.
Definition at line 1146 of file Expr.java.
|
inline |
Indicates whether the term is a Proof for the expression 'true'.
Definition at line 1066 of file Expr.java.
|
inline |
Indicates whether the term is a proof by unit resolution
T1: (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
Definition at line 1338 of file Expr.java.
|
inline |
|
inline |
Indicates whether the term is of sort real.
Definition at line 358 of file Expr.java.
Referenced by Expr.isRatNum().
|
inline |
|
inline |
Indicates whether the term is a coercion of real to integer (unary)
Definition at line 480 of file Expr.java.
|
inline |
Indicates whether the term is of an array sort.
Definition at line 1552 of file Expr.java.
|
inline |
Indicates whether the term is a relational join
Definition at line 1590 of file Expr.java.
|
inline |
Indicates whether the term is a relational clone (copy)
Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind
to perform destructive updates to the first argument.
Definition at line 1688 of file Expr.java.
|
inline |
Indicates whether the term is the complement of a relation
Definition at line 1665 of file Expr.java.
|
inline |
Indicates whether the term is a relation filter
Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.
Definition at line 1630 of file Expr.java.
|
inline |
Indicates whether the term is an intersection of a relation with the negation of another.
Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function
target = filter_by_negation(pos, neg, columns)
where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.
Definition at line 1647 of file Expr.java.
|
inline |
Indicates whether the term is a projection of columns (provided as numbers in the parameters).
The function takes one argument.
Definition at line 1618 of file Expr.java.
|
inline |
Indicates whether the term is the renaming of a column in a relation
The function takes one argument. The parameters contain the renaming as a cycle.
Definition at line 1657 of file Expr.java.
|
inline |
Indicates whether the term is a relational select
Check if a record is an element of the relation. The function takes
arguments, where the first argument is a relation, and the remaining
arguments correspond to a record.
Definition at line 1676 of file Expr.java.
|
inline |
Indicates whether the term is an relation store
Insert a record into a relation. The function takes
arguments, where the first argument is the relation and the remaining
elements correspond to the
columns of the relation.
Definition at line 1566 of file Expr.java.
|
inline |
Indicates whether the term is the union or convex hull of two relations.
The function takes two arguments.
Definition at line 1599 of file Expr.java.
|
inline |
Indicates whether the term is the widening of two relations
The function takes two arguments.
Definition at line 1608 of file Expr.java.
|
inline |
|
inline |
Indicates whether the term is an array select.
Definition at line 517 of file Expr.java.
|
inline |
Indicates whether the term is set complement
Definition at line 587 of file Expr.java.
|
inline |
Indicates whether the term is set difference
Definition at line 579 of file Expr.java.
|
inline |
Indicates whether the term is set intersection
Definition at line 571 of file Expr.java.
|
inline |
Indicates whether the term is set subset
Definition at line 595 of file Expr.java.
|
inline |
Indicates whether the term is set union
Definition at line 563 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the term is a unary minus
Definition at line 424 of file Expr.java.
|
inline |
|
inline |
|
inline |
|
inline |
Returns a simplified version of the expression A set of parameters
p | a Params object |
to configure the simplifier
Definition at line 46 of file Expr.java.
|
inline |
Substitute every occurrence of from[i]
in the expression with to[i]
, for i
smaller than num_exprs
.
The result is the new expression. The arrays
and
must have size
. For every
smaller than
, we must have that sort of
must be equal to sort of
.
Definition at line 123 of file Expr.java.
Referenced by Expr.substitute().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |