Expressions are terms. More...
Public Member Functions | |
Expr | Simplify (Params p=null) |
Returns a simplified version of the expression. More... | |
void | Update (Expr[] args) |
Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments. More... | |
Expr | Substitute (Expr[] from, Expr[] to) |
Substitute every occurrence of from[i] in the expression with to[i] , for i smaller than num_exprs . More... | |
Expr | Substitute (Expr from, Expr to) |
Substitute every occurrence of from in the expression with to . More... | |
Expr | SubstituteVars (Expr[] to) |
Substitute the free variables in the expression with the expressions in to More... | |
new Expr | Translate (Context ctx) |
Translates (copies) the term to the Context ctx . More... | |
override string | ToString () |
Returns a string representation of the expression. More... | |
![]() | |
override bool | Equals (object o) |
Object comparison. More... | |
virtual int | CompareTo (object other) |
Object Comparison. More... | |
override int | GetHashCode () |
The AST's hash code. More... | |
AST | Translate (Context ctx) |
Translates (copies) the AST to the Context ctx . More... | |
override string | ToString () |
A string representation of the AST. More... | |
string | SExpr () |
A string representation of the AST in s-expression notation. More... | |
![]() | |
void | Dispose () |
Disposes of the underlying native Z3 object. More... | |
Protected Member Functions | |
Expr (Context ctx, IntPtr obj) | |
Constructor for Expr More... | |
Properties | |
FuncDecl | FuncDecl [get] |
The function declaration of the function that is applied in this expression. More... | |
Z3_lbool | BoolValue [get] |
Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF). More... | |
uint | NumArgs [get] |
The number of arguments of the expression. More... | |
Expr [] | Args [get] |
The arguments of the expression. More... | |
bool | IsNumeral [get] |
Indicates whether the term is a numeral More... | |
bool | IsWellSorted [get] |
Indicates whether the term is well-sorted. More... | |
Sort | Sort [get] |
The Sort of the term. More... | |
bool | IsConst [get] |
Indicates whether the term represents a constant. More... | |
bool | IsIntNum [get] |
Indicates whether the term is an integer numeral. More... | |
bool | IsRatNum [get] |
Indicates whether the term is a real numeral. More... | |
bool | IsAlgebraicNumber [get] |
Indicates whether the term is an algebraic number More... | |
bool | IsBool [get] |
Indicates whether the term has Boolean sort. More... | |
bool | IsTrue [get] |
Indicates whether the term is the constant true. More... | |
bool | IsFalse [get] |
Indicates whether the term is the constant false. More... | |
bool | IsEq [get] |
Indicates whether the term is an equality predicate. More... | |
bool | IsDistinct [get] |
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). More... | |
bool | IsITE [get] |
Indicates whether the term is a ternary if-then-else term More... | |
bool | IsAnd [get] |
Indicates whether the term is an n-ary conjunction More... | |
bool | IsOr [get] |
Indicates whether the term is an n-ary disjunction More... | |
bool | IsIff [get] |
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) More... | |
bool | IsXor [get] |
Indicates whether the term is an exclusive or More... | |
bool | IsNot [get] |
Indicates whether the term is a negation More... | |
bool | IsImplies [get] |
Indicates whether the term is an implication More... | |
bool | IsInterpolant [get] |
Indicates whether the term is marked for interpolation. More... | |
bool | IsInt [get] |
Indicates whether the term is of integer sort. More... | |
bool | IsReal [get] |
Indicates whether the term is of sort real. More... | |
bool | IsArithmeticNumeral [get] |
Indicates whether the term is an arithmetic numeral. More... | |
bool | IsLE [get] |
Indicates whether the term is a less-than-or-equal More... | |
bool | IsGE [get] |
Indicates whether the term is a greater-than-or-equal More... | |
bool | IsLT [get] |
Indicates whether the term is a less-than More... | |
bool | IsGT [get] |
Indicates whether the term is a greater-than More... | |
bool | IsAdd [get] |
Indicates whether the term is addition (binary) More... | |
bool | IsSub [get] |
Indicates whether the term is subtraction (binary) More... | |
bool | IsUMinus [get] |
Indicates whether the term is a unary minus More... | |
bool | IsMul [get] |
Indicates whether the term is multiplication (binary) More... | |
bool | IsDiv [get] |
Indicates whether the term is division (binary) More... | |
bool | IsIDiv [get] |
Indicates whether the term is integer division (binary) More... | |
bool | IsRemainder [get] |
Indicates whether the term is remainder (binary) More... | |
bool | IsModulus [get] |
Indicates whether the term is modulus (binary) More... | |
bool | IsIntToReal [get] |
Indicates whether the term is a coercion of integer to real (unary) More... | |
bool | IsRealToInt [get] |
Indicates whether the term is a coercion of real to integer (unary) More... | |
bool | IsRealIsInt [get] |
Indicates whether the term is a check that tests whether a real is integral (unary) More... | |
bool | IsArray [get] |
Indicates whether the term is of an array sort. More... | |
bool | IsStore [get] |
Indicates whether the term is an array store. More... | |
bool | IsSelect [get] |
Indicates whether the term is an array select. More... | |
bool | IsConstantArray [get] |
Indicates whether the term is a constant array. More... | |
bool | IsDefaultArray [get] |
Indicates whether the term is a default array. More... | |
bool | IsArrayMap [get] |
Indicates whether the term is an array map. More... | |
bool | IsAsArray [get] |
Indicates whether the term is an as-array term. More... | |
bool | IsSetUnion [get] |
Indicates whether the term is set union More... | |
bool | IsSetIntersect [get] |
Indicates whether the term is set intersection More... | |
bool | IsSetDifference [get] |
Indicates whether the term is set difference More... | |
bool | IsSetComplement [get] |
Indicates whether the term is set complement More... | |
bool | IsSetSubset [get] |
Indicates whether the term is set subset More... | |
bool | IsBV [get] |
Indicates whether the terms is of bit-vector sort. More... | |
bool | IsBVNumeral [get] |
Indicates whether the term is a bit-vector numeral More... | |
bool | IsBVBitOne [get] |
Indicates whether the term is a one-bit bit-vector with value one More... | |
bool | IsBVBitZero [get] |
Indicates whether the term is a one-bit bit-vector with value zero More... | |
bool | IsBVUMinus [get] |
Indicates whether the term is a bit-vector unary minus More... | |
bool | IsBVAdd [get] |
Indicates whether the term is a bit-vector addition (binary) More... | |
bool | IsBVSub [get] |
Indicates whether the term is a bit-vector subtraction (binary) More... | |
bool | IsBVMul [get] |
Indicates whether the term is a bit-vector multiplication (binary) More... | |
bool | IsBVSDiv [get] |
Indicates whether the term is a bit-vector signed division (binary) More... | |
bool | IsBVUDiv [get] |
Indicates whether the term is a bit-vector unsigned division (binary) More... | |
bool | IsBVSRem [get] |
Indicates whether the term is a bit-vector signed remainder (binary) More... | |
bool | IsBVURem [get] |
Indicates whether the term is a bit-vector unsigned remainder (binary) More... | |
bool | IsBVSMod [get] |
Indicates whether the term is a bit-vector signed modulus More... | |
bool | IsBVULE [get] |
Indicates whether the term is an unsigned bit-vector less-than-or-equal More... | |
bool | IsBVSLE [get] |
Indicates whether the term is a signed bit-vector less-than-or-equal More... | |
bool | IsBVUGE [get] |
Indicates whether the term is an unsigned bit-vector greater-than-or-equal More... | |
bool | IsBVSGE [get] |
Indicates whether the term is a signed bit-vector greater-than-or-equal More... | |
bool | IsBVULT [get] |
Indicates whether the term is an unsigned bit-vector less-than More... | |
bool | IsBVSLT [get] |
Indicates whether the term is a signed bit-vector less-than More... | |
bool | IsBVUGT [get] |
Indicates whether the term is an unsigned bit-vector greater-than More... | |
bool | IsBVSGT [get] |
Indicates whether the term is a signed bit-vector greater-than More... | |
bool | IsBVAND [get] |
Indicates whether the term is a bit-wise AND More... | |
bool | IsBVOR [get] |
Indicates whether the term is a bit-wise OR More... | |
bool | IsBVNOT [get] |
Indicates whether the term is a bit-wise NOT More... | |
bool | IsBVXOR [get] |
Indicates whether the term is a bit-wise XOR More... | |
bool | IsBVNAND [get] |
Indicates whether the term is a bit-wise NAND More... | |
bool | IsBVNOR [get] |
Indicates whether the term is a bit-wise NOR More... | |
bool | IsBVXNOR [get] |
Indicates whether the term is a bit-wise XNOR More... | |
bool | IsBVConcat [get] |
Indicates whether the term is a bit-vector concatenation (binary) More... | |
bool | IsBVSignExtension [get] |
Indicates whether the term is a bit-vector sign extension More... | |
bool | IsBVZeroExtension [get] |
Indicates whether the term is a bit-vector zero extension More... | |
bool | IsBVExtract [get] |
Indicates whether the term is a bit-vector extraction More... | |
bool | IsBVRepeat [get] |
Indicates whether the term is a bit-vector repetition More... | |
bool | IsBVReduceOR [get] |
Indicates whether the term is a bit-vector reduce OR More... | |
bool | IsBVReduceAND [get] |
Indicates whether the term is a bit-vector reduce AND More... | |
bool | IsBVComp [get] |
Indicates whether the term is a bit-vector comparison More... | |
bool | IsBVShiftLeft [get] |
Indicates whether the term is a bit-vector shift left More... | |
bool | IsBVShiftRightLogical [get] |
Indicates whether the term is a bit-vector logical shift right More... | |
bool | IsBVShiftRightArithmetic [get] |
Indicates whether the term is a bit-vector arithmetic shift left More... | |
bool | IsBVRotateLeft [get] |
Indicates whether the term is a bit-vector rotate left More... | |
bool | IsBVRotateRight [get] |
Indicates whether the term is a bit-vector rotate right More... | |
bool | IsBVRotateLeftExtended [get] |
Indicates whether the term is a bit-vector rotate left (extended) More... | |
bool | IsBVRotateRightExtended [get] |
Indicates whether the term is a bit-vector rotate right (extended) More... | |
bool | IsIntToBV [get] |
Indicates whether the term is a coercion from integer to bit-vector More... | |
bool | IsBVToInt [get] |
Indicates whether the term is a coercion from bit-vector to integer More... | |
bool | IsBVCarry [get] |
Indicates whether the term is a bit-vector carry More... | |
bool | IsBVXOR3 [get] |
Indicates whether the term is a bit-vector ternary XOR More... | |
bool | IsLabel [get] |
Indicates whether the term is a label (used by the Boogie Verification condition generator). More... | |
bool | IsLabelLit [get] |
Indicates whether the term is a label literal (used by the Boogie Verification condition generator). More... | |
bool | IsOEQ [get] |
Indicates whether the term is a binary equivalence modulo namings. More... | |
bool | IsProofTrue [get] |
Indicates whether the term is a Proof for the expression 'true'. More... | |
bool | IsProofAsserted [get] |
Indicates whether the term is a proof for a fact asserted by the user. More... | |
bool | IsProofGoal [get] |
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. More... | |
bool | IsProofModusPonens [get] |
Indicates whether the term is proof via modus ponens More... | |
bool | IsProofReflexivity [get] |
Indicates whether the term is a proof for (R t t), where R is a reflexive relation. More... | |
bool | IsProofSymmetry [get] |
Indicates whether the term is proof by symmetricity of a relation More... | |
bool | IsProofTransitivity [get] |
Indicates whether the term is a proof by transitivity of a relation More... | |
bool | IsProofTransitivityStar [get] |
Indicates whether the term is a proof by condensed transitivity of a relation More... | |
bool | IsProofMonotonicity [get] |
Indicates whether the term is a monotonicity proof object. More... | |
bool | IsProofQuantIntro [get] |
Indicates whether the term is a quant-intro proof More... | |
bool | IsProofDistributivity [get] |
Indicates whether the term is a distributivity proof object. More... | |
bool | IsProofAndElimination [get] |
Indicates whether the term is a proof by elimination of AND More... | |
bool | IsProofOrElimination [get] |
Indicates whether the term is a proof by eliminiation of not-or More... | |
bool | IsProofRewrite [get] |
Indicates whether the term is a proof by rewriting More... | |
bool | IsProofRewriteStar [get] |
Indicates whether the term is a proof by rewriting More... | |
bool | IsProofPullQuant [get] |
Indicates whether the term is a proof for pulling quantifiers out. More... | |
bool | IsProofPullQuantStar [get] |
Indicates whether the term is a proof for pulling quantifiers out. More... | |
bool | IsProofPushQuant [get] |
Indicates whether the term is a proof for pushing quantifiers in. More... | |
bool | IsProofElimUnusedVars [get] |
Indicates whether the term is a proof for elimination of unused variables. More... | |
bool | IsProofDER [get] |
Indicates whether the term is a proof for destructive equality resolution More... | |
bool | IsProofQuantInst [get] |
Indicates whether the term is a proof for quantifier instantiation More... | |
bool | IsProofHypothesis [get] |
Indicates whether the term is a hypthesis marker. More... | |
bool | IsProofLemma [get] |
Indicates whether the term is a proof by lemma More... | |
bool | IsProofUnitResolution [get] |
Indicates whether the term is a proof by unit resolution More... | |
bool | IsProofIFFTrue [get] |
Indicates whether the term is a proof by iff-true More... | |
bool | IsProofIFFFalse [get] |
Indicates whether the term is a proof by iff-false More... | |
bool | IsProofCommutativity [get] |
Indicates whether the term is a proof by commutativity More... | |
bool | IsProofDefAxiom [get] |
Indicates whether the term is a proof for Tseitin-like axioms More... | |
bool | IsProofDefIntro [get] |
Indicates whether the term is a proof for introduction of a name More... | |
bool | IsProofApplyDef [get] |
Indicates whether the term is a proof for application of a definition More... | |
bool | IsProofIFFOEQ [get] |
Indicates whether the term is a proof iff-oeq More... | |
bool | IsProofNNFPos [get] |
Indicates whether the term is a proof for a positive NNF step More... | |
bool | IsProofNNFNeg [get] |
Indicates whether the term is a proof for a negative NNF step More... | |
bool | IsProofNNFStar [get] |
Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. More... | |
bool | IsProofCNFStar [get] |
Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. More... | |
bool | IsProofSkolemize [get] |
Indicates whether the term is a proof for a Skolemization step More... | |
bool | IsProofModusPonensOEQ [get] |
Indicates whether the term is a proof by modus ponens for equi-satisfiability. More... | |
bool | IsProofTheoryLemma [get] |
Indicates whether the term is a proof for theory lemma More... | |
bool | IsRelation [get] |
Indicates whether the term is of relation sort. More... | |
bool | IsRelationStore [get] |
Indicates whether the term is an relation store More... | |
bool | IsEmptyRelation [get] |
Indicates whether the term is an empty relation More... | |
bool | IsIsEmptyRelation [get] |
Indicates whether the term is a test for the emptiness of a relation More... | |
bool | IsRelationalJoin [get] |
Indicates whether the term is a relational join More... | |
bool | IsRelationUnion [get] |
Indicates whether the term is the union or convex hull of two relations. More... | |
bool | IsRelationWiden [get] |
Indicates whether the term is the widening of two relations More... | |
bool | IsRelationProject [get] |
Indicates whether the term is a projection of columns (provided as numbers in the parameters). More... | |
bool | IsRelationFilter [get] |
Indicates whether the term is a relation filter More... | |
bool | IsRelationNegationFilter [get] |
Indicates whether the term is an intersection of a relation with the negation of another. More... | |
bool | IsRelationRename [get] |
Indicates whether the term is the renaming of a column in a relation More... | |
bool | IsRelationComplement [get] |
Indicates whether the term is the complement of a relation More... | |
bool | IsRelationSelect [get] |
Indicates whether the term is a relational select More... | |
bool | IsRelationClone [get] |
Indicates whether the term is a relational clone (copy) More... | |
bool | IsFiniteDomain [get] |
Indicates whether the term is of an array sort. More... | |
bool | IsFiniteDomainLT [get] |
Indicates whether the term is a less than predicate over a finite domain. More... | |
bool | IsFP [get] |
Indicates whether the terms is of floating-point sort. More... | |
bool | IsFPRM [get] |
Indicates whether the terms is of floating-point rounding mode sort. More... | |
bool | IsFPNumeral [get] |
Indicates whether the term is a floating-point numeral More... | |
bool | IsFPRMNumeral [get] |
Indicates whether the term is a floating-point rounding mode numeral More... | |
bool | IsFPRMRoundNearestTiesToEven [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |
bool | IsFPRMRoundNearestTiesToAway [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |
bool | IsFPRMRoundTowardNegative [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |
bool | IsFPRMRoundTowardPositive [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |
bool | IsFPRMRoundTowardZero [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |
bool | IsFPRMExprRNE [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven More... | |
bool | IsFPRMExprRNA [get] |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway More... | |
bool | IsFPRMExprRTN [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative More... | |
bool | IsFPRMExprRTP [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive More... | |
bool | IsFPRMExprRTZ [get] |
Indicates whether the term is the floating-point rounding numeral roundTowardZero More... | |
bool | IsFPRMExpr [get] |
Indicates whether the term is a floating-point rounding mode numeral More... | |
bool | IsFPPlusInfinity [get] |
Indicates whether the term is a floating-point +oo More... | |
bool | IsFPMinusInfinity [get] |
Indicates whether the term is a floating-point -oo More... | |
bool | IsFPNaN [get] |
Indicates whether the term is a floating-point NaN More... | |
bool | IsFPPlusZero [get] |
bool | IsFPMinusZero [get] |
Indicates whether the term is a floating-point -zero More... | |
bool | IsFPAdd [get] |
Indicates whether the term is a floating-point addition term More... | |
bool | IsFPSub [get] |
Indicates whether the term is a floating-point subtraction term More... | |
bool | IsFPNeg [get] |
Indicates whether the term is a floating-point negation term More... | |
bool | IsFPMul [get] |
Indicates whether the term is a floating-point multiplication term More... | |
bool | IsFPDiv [get] |
Indicates whether the term is a floating-point divison term More... | |
bool | IsFPRem [get] |
Indicates whether the term is a floating-point remainder term More... | |
bool | IsFPAbs [get] |
Indicates whether the term is a floating-point term absolute value term More... | |
bool | IsFPMin [get] |
Indicates whether the term is a floating-point minimum term More... | |
bool | IsFPMax [get] |
Indicates whether the term is a floating-point maximum term More... | |
bool | IsFPFMA [get] |
Indicates whether the term is a floating-point fused multiply-add term More... | |
bool | IsFPSqrt [get] |
Indicates whether the term is a floating-point square root term More... | |
bool | IsFPRoundToIntegral [get] |
Indicates whether the term is a floating-point roundToIntegral term More... | |
bool | IsFPEq [get] |
Indicates whether the term is a floating-point equality term More... | |
bool | IsFPLt [get] |
Indicates whether the term is a floating-point less-than term More... | |
bool | IsFPGt [get] |
Indicates whether the term is a floating-point greater-than term More... | |
bool | IsFPLe [get] |
Indicates whether the term is a floating-point less-than or equal term More... | |
bool | IsFPGe [get] |
Indicates whether the term is a floating-point greater-than or erqual term More... | |
bool | IsFPisNaN [get] |
Indicates whether the term is a floating-point isNaN predicate term More... | |
bool | IsFPisInf [get] |
Indicates whether the term is a floating-point isInf predicate term More... | |
bool | IsFPisZero [get] |
Indicates whether the term is a floating-point isZero predicate term More... | |
bool | IsFPisNormal [get] |
Indicates whether the term is a floating-point isNormal term More... | |
bool | IsFPisSubnormal [get] |
Indicates whether the term is a floating-point isSubnormal predicate term More... | |
bool | IsFPisNegative [get] |
Indicates whether the term is a floating-point isNegative predicate term More... | |
bool | IsFPisPositive [get] |
Indicates whether the term is a floating-point isPositive predicate term More... | |
bool | IsFPFP [get] |
Indicates whether the term is a floating-point constructor term More... | |
bool | IsFPToFp [get] |
Indicates whether the term is a floating-point conversion term More... | |
bool | IsFPToFpUnsigned [get] |
Indicates whether the term is a floating-point conversion from unsigned bit-vector term More... | |
bool | IsFPToUBV [get] |
Indicates whether the term is a floating-point conversion to unsigned bit-vector term More... | |
bool | IsFPToSBV [get] |
Indicates whether the term is a floating-point conversion to signed bit-vector term More... | |
bool | IsFPToReal [get] |
Indicates whether the term is a floating-point conversion to real term More... | |
bool | IsFPToIEEEBV [get] |
Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term More... | |
uint | Index [get] |
The de-Burijn index of a bound variable. More... | |
![]() | |
uint | Id [get] |
A unique identifier for the AST (unique among all ASTs). More... | |
Z3_ast_kind | ASTKind [get] |
The kind of the AST. More... | |
bool | IsExpr [get] |
Indicates whether the AST is an Expr More... | |
bool | IsApp [get] |
Indicates whether the AST is an application More... | |
bool | IsVar [get] |
Indicates whether the AST is a BoundVariable More... | |
bool | IsQuantifier [get] |
Indicates whether the AST is a Quantifier More... | |
bool | IsSort [get] |
Indicates whether the AST is a Sort More... | |
bool | IsFuncDecl [get] |
Indicates whether the AST is a FunctionDeclaration More... | |
Additional Inherited Members | |
![]() | |
static bool | operator== (AST a, AST b) |
Comparison operator. More... | |
static bool | operator!= (AST a, AST b) |
Comparison operator. More... | |
Constructor for Expr
Returns a simplified version of the expression.
p | A set of parameters to configure the simplifier |
Definition at line 36 of file Expr.cs.
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 from
and to
must have size num_exprs
. For every i
smaller than num_exprs
, we must have that sort of from[i]
must be equal to sort of to[i]
.
Substitute every occurrence of from
in the expression with to
.
Definition at line 134 of file Expr.cs.
Substitute the free variables in the expression with the expressions in to
For every i
smaller than num_exprs
, the variable with de-Bruijn index i
is replaced with term to[i]
.
|
inline |
|
inline |
Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments.
Definition at line 96 of file Expr.cs.
|
get |
The arguments of the expression.
Definition at line 79 of file Expr.cs.
|
get |
The function declaration of the function that is applied in this expression.
Definition at line 50 of file Expr.cs.
Referenced by Model.ConstInterp().
|
get |
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 1746 of file Expr.cs.
|
get |
Indicates whether the term is addition (binary)
Definition at line 379 of file Expr.cs.
|
get |
|
get |
Indicates whether the term is an n-ary conjunction
Definition at line 297 of file Expr.cs.
|
get |
Indicates whether the term is an arithmetic numeral.
Definition at line 354 of file Expr.cs.
|
get |
Indicates whether the term is of an array sort.
Definition at line 437 of file Expr.cs.
|
get |
Indicates whether the term is an array map.
It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.
Definition at line 474 of file Expr.cs.
|
get |
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 481 of file Expr.cs.
|
get |
|
get |
Indicates whether the terms is of bit-vector sort.
Definition at line 516 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector addition (binary)
Definition at line 543 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise AND
Definition at line 648 of file Expr.cs.
|
get |
Indicates whether the term is a one-bit bit-vector with value one
Definition at line 528 of file Expr.cs.
|
get |
Indicates whether the term is a one-bit bit-vector with value zero
Definition at line 533 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector carry
Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))
Definition at line 776 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector comparison
Definition at line 718 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector concatenation (binary)
Definition at line 683 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector extraction
Definition at line 698 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector multiplication (binary)
Definition at line 553 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise NAND
Definition at line 668 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise NOR
Definition at line 673 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise NOT
Definition at line 658 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector numeral
Definition at line 523 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise OR
Definition at line 653 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector reduce AND
Definition at line 713 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector reduce OR
Definition at line 708 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector repetition
Definition at line 703 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector rotate left
Definition at line 738 of file Expr.cs.
|
get |
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 749 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector rotate right
Definition at line 743 of file Expr.cs.
|
get |
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 755 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector signed division (binary)
Definition at line 558 of file Expr.cs.
|
get |
Indicates whether the term is a signed bit-vector greater-than-or-equal
Definition at line 623 of file Expr.cs.
|
get |
Indicates whether the term is a signed bit-vector greater-than
Definition at line 643 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector shift left
Definition at line 723 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector arithmetic shift left
Definition at line 733 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector logical shift right
Definition at line 728 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector sign extension
Definition at line 688 of file Expr.cs.
|
get |
Indicates whether the term is a signed bit-vector less-than-or-equal
Definition at line 613 of file Expr.cs.
|
get |
Indicates whether the term is a signed bit-vector less-than
Definition at line 633 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector signed modulus
Definition at line 578 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector signed remainder (binary)
Definition at line 568 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector subtraction (binary)
Definition at line 548 of file Expr.cs.
|
get |
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 769 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector unsigned division (binary)
Definition at line 563 of file Expr.cs.
|
get |
Indicates whether the term is an unsigned bit-vector greater-than-or-equal
Definition at line 618 of file Expr.cs.
|
get |
Indicates whether the term is an unsigned bit-vector greater-than
Definition at line 638 of file Expr.cs.
|
get |
Indicates whether the term is an unsigned bit-vector less-than-or-equal
Definition at line 608 of file Expr.cs.
|
get |
Indicates whether the term is an unsigned bit-vector less-than
Definition at line 628 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector unary minus
Definition at line 538 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector unsigned remainder (binary)
Definition at line 573 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise XNOR
Definition at line 678 of file Expr.cs.
|
get |
Indicates whether the term is a bit-wise XOR
Definition at line 663 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector ternary XOR
The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)
Definition at line 782 of file Expr.cs.
|
get |
Indicates whether the term is a bit-vector zero extension
Definition at line 693 of file Expr.cs.
|
get |
Indicates whether the term represents a constant.
Definition at line 217 of file Expr.cs.
|
get |
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 462 of file Expr.cs.
|
get |
Indicates whether the term is a default array.
For example default(const(v)) = v. The function is unary.
Definition at line 468 of file Expr.cs.
|
get |
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
Definition at line 287 of file Expr.cs.
|
get |
Indicates whether the term is division (binary)
Definition at line 399 of file Expr.cs.
|
get |
Indicates whether the term is an empty relation
Definition at line 1335 of file Expr.cs.
|
get |
Indicates whether the term is an equality predicate.
Definition at line 282 of file Expr.cs.
|
get |
Indicates whether the term is the constant false.
Definition at line 277 of file Expr.cs.
|
get |
Indicates whether the term is of an array sort.
Definition at line 1435 of file Expr.cs.
|
get |
Indicates whether the term is a less than predicate over a finite domain.
Definition at line 1446 of file Expr.cs.
|
get |
Indicates whether the terms is of floating-point sort.
Definition at line 1454 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point term absolute value term
Definition at line 1599 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point addition term
Definition at line 1568 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point divison term
Definition at line 1589 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point equality term
Definition at line 1629 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point fused multiply-add term
Definition at line 1614 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point constructor term
Definition at line 1689 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point greater-than or erqual term
Definition at line 1649 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point greater-than term
Definition at line 1639 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isInf predicate term
Definition at line 1659 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isNaN predicate term
Definition at line 1654 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isNegative predicate term
Definition at line 1679 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isNormal term
Definition at line 1669 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isPositive predicate term
Definition at line 1684 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isSubnormal predicate term
Definition at line 1674 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point isZero predicate term
Definition at line 1664 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point less-than or equal term
Definition at line 1644 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point less-than term
Definition at line 1634 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point maximum term
Definition at line 1609 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point minimum term
Definition at line 1604 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point -oo
Definition at line 1548 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point -zero
Definition at line 1563 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point multiplication term
Definition at line 1584 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point NaN
Definition at line 1553 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point negation term
Definition at line 1579 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point numeral
Definition at line 1469 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point +oo
Definition at line 1543 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point +zero
Definition at line 1558 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point remainder term
Definition at line 1594 of file Expr.cs.
|
get |
Indicates whether the terms is of floating-point rounding mode sort.
Definition at line 1462 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point rounding mode numeral
Definition at line 1529 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition at line 1509 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition at line 1504 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition at line 1514 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition at line 1519 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition at line 1524 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point rounding mode numeral
Definition at line 1474 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition at line 1484 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition at line 1479 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition at line 1489 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition at line 1494 of file Expr.cs.
|
get |
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition at line 1499 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point roundToIntegral term
Definition at line 1624 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point square root term
Definition at line 1619 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point subtraction term
Definition at line 1574 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion term
Definition at line 1694 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion from unsigned bit-vector term
Definition at line 1699 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term
Definition at line 1720 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion to real term
Definition at line 1714 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion to signed bit-vector term
Definition at line 1709 of file Expr.cs.
|
get |
Indicates whether the term is a floating-point conversion to unsigned bit-vector term
Definition at line 1704 of file Expr.cs.
|
get |
Indicates whether the term is a greater-than-or-equal
Definition at line 364 of file Expr.cs.
|
get |
Indicates whether the term is a greater-than
Definition at line 374 of file Expr.cs.
|
get |
Indicates whether the term is integer division (binary)
Definition at line 404 of file Expr.cs.
|
get |
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
Definition at line 307 of file Expr.cs.
|
get |
Indicates whether the term is an implication
Definition at line 322 of file Expr.cs.
|
get |
Indicates whether the term is of integer sort.
Definition at line 339 of file Expr.cs.
|
get |
Indicates whether the term is marked for interpolation.
Definition at line 331 of file Expr.cs.
|
get |
Indicates whether the term is an integer numeral.
Definition at line 227 of file Expr.cs.
|
get |
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 762 of file Expr.cs.
|
get |
Indicates whether the term is a coercion of integer to real (unary)
Definition at line 419 of file Expr.cs.
|
get |
Indicates whether the term is a test for the emptiness of a relation
Definition at line 1340 of file Expr.cs.
|
get |
Indicates whether the term is a ternary if-then-else term
Definition at line 292 of file Expr.cs.
|
get |
Indicates whether the term is a label (used by the Boogie Verification condition generator).
The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.
Definition at line 791 of file Expr.cs.
|
get |
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 797 of file Expr.cs.
|
get |
Indicates whether the term is a less-than-or-equal
Definition at line 359 of file Expr.cs.
|
get |
Indicates whether the term is a less-than
Definition at line 369 of file Expr.cs.
|
get |
Indicates whether the term is modulus (binary)
Definition at line 414 of file Expr.cs.
|
get |
Indicates whether the term is multiplication (binary)
Definition at line 394 of file Expr.cs.
|
get |
Indicates whether the term is a negation
Definition at line 317 of file Expr.cs.
|
get |
|
get |
Indicates whether the term is a binary equivalence modulo namings.
This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.
Definition at line 806 of file Expr.cs.
|
get |
Indicates whether the term is an n-ary disjunction
Definition at line 302 of file Expr.cs.
|
get |
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)
Definition at line 937 of file Expr.cs.
|
get |
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 1178 of file Expr.cs.
|
get |
Indicates whether the term is a proof for a fact asserted by the user.
Definition at line 816 of file Expr.cs.
|
get |
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 1262 of file Expr.cs.
|
get |
Indicates whether the term is a proof by commutativity
f is a commutative operator.
This proof object has no antecedents. Remark: if f is bool, then = is iff.
Definition at line 1109 of file Expr.cs.
|
get |
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 1145 of file Expr.cs.
|
get |
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:
or:
when e only occurs positively.
When e is of the form (ite cond th el):
Otherwise: [def-intro]: (= n e)
Definition at line 1168 of file Expr.cs.
|
get |
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 1039 of file Expr.cs.
|
get |
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 927 of file Expr.cs.
|
get |
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 1025 of file Expr.cs.
|
get |
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
Definition at line 821 of file Expr.cs.
|
get |
Indicates whether the term is a hypthesis marker.
Mark a hypothesis in a natural deduction style proof.
Definition at line 1053 of file Expr.cs.
|
get |
Indicates whether the term is a proof by iff-false
T1: (not p) [iff-false T1]: (iff p false)
Definition at line 1096 of file Expr.cs.
|
get |
Indicates whether the term is a proof iff-oeq
T1: (iff p q) [iff~ T1]: (~ p q)
Definition at line 1187 of file Expr.cs.
|
get |
Indicates whether the term is a proof by iff-true
T1: p [iff-true T1]: (iff p true)
Definition at line 1087 of file Expr.cs.
|
get |
Indicates whether the term is a proof by lemma
T1: false
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 1066 of file Expr.cs.
|
get |
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)
The second antecedents may also be a proof for (iff p q).
Definition at line 832 of file Expr.cs.
|
get |
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)
Definition at line 1286 of file Expr.cs.
|
get |
Indicates whether the term is a monotonicity proof object.
T1: (R t_1 s_1) ... Tn: (R t_n 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 899 of file Expr.cs.
|
get |
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
and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ 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'
(and (or r_1 r_2) (or r_1' r_2')))
Definition at line 1240 of file Expr.cs.
|
get |
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'
(and (or r_1 r_2') (or r_1' 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
(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 1215 of file Expr.cs.
|
get |
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 1252 of file Expr.cs.
|
get |
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 947 of file Expr.cs.
|
get |
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 990 of file Expr.cs.
|
get |
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 1000 of file Expr.cs.
|
get |
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 1013 of file Expr.cs.
|
get |
Indicates whether the term is a proof for quantifier instantiation
A proof of (or (not (forall (x) (P x))) (P a))
Definition at line 1047 of file Expr.cs.
|
get |
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)
Definition at line 909 of file Expr.cs.
|
get |
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 841 of file Expr.cs.
|
get |
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 966 of file Expr.cs.
|
get |
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:
Definition at line 982 of file Expr.cs.
|
get |
Indicates whether the term is a proof for a Skolemization step
Proof for:
This proof object has no antecedents.
Definition at line 1275 of file Expr.cs.
|
get |
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 852 of file Expr.cs.
|
get |
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:
Definition at line 1305 of file Expr.cs.
|
get |
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 864 of file Expr.cs.
|
get |
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 885 of file Expr.cs.
|
get |
Indicates whether the term is a Proof for the expression 'true'.
Definition at line 811 of file Expr.cs.
|
get |
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 1078 of file Expr.cs.
|
get |
Indicates whether the term is a real numeral.
Definition at line 237 of file Expr.cs.
|
get |
Indicates whether the term is of sort real.
Definition at line 347 of file Expr.cs.
|
get |
Indicates whether the term is a check that tests whether a real is integral (unary)
Definition at line 429 of file Expr.cs.
|
get |
Indicates whether the term is a coercion of real to integer (unary)
Definition at line 424 of file Expr.cs.
|
get |
Indicates whether the term is of relation sort.
Definition at line 1313 of file Expr.cs.
|
get |
Indicates whether the term is a relational join
Definition at line 1345 of file Expr.cs.
|
get |
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 1427 of file Expr.cs.
|
get |
Indicates whether the term is the complement of a relation
Definition at line 1405 of file Expr.cs.
|
get |
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 1375 of file Expr.cs.
|
get |
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 1391 of file Expr.cs.
|
get |
Indicates whether the term is a projection of columns (provided as numbers in the parameters).
The function takes one argument.
Definition at line 1363 of file Expr.cs.
|
get |
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 1400 of file Expr.cs.
|
get |
Indicates whether the term is a relational select
Check if a record is an element of the relation. The function takes n+1
arguments, where the first argument is a relation, and the remaining n
arguments correspond to a record.
Definition at line 1415 of file Expr.cs.
|
get |
Indicates whether the term is an relation store
Insert a record into a relation. The function takes n+1
arguments, where the first argument is the relation and the remaining n
elements correspond to the n
columns of the relation.
Definition at line 1330 of file Expr.cs.
|
get |
Indicates whether the term is the union or convex hull of two relations.
The function takes two arguments.
Definition at line 1351 of file Expr.cs.
|
get |
Indicates whether the term is the widening of two relations
The function takes two arguments.
Definition at line 1357 of file Expr.cs.
|
get |
Indicates whether the term is remainder (binary)
Definition at line 409 of file Expr.cs.
|
get |
Indicates whether the term is an array select.
Definition at line 456 of file Expr.cs.
|
get |
Indicates whether the term is set complement
Definition at line 503 of file Expr.cs.
|
get |
Indicates whether the term is set difference
Definition at line 498 of file Expr.cs.
|
get |
Indicates whether the term is set intersection
Definition at line 493 of file Expr.cs.
|
get |
Indicates whether the term is set subset
Definition at line 508 of file Expr.cs.
|
get |
Indicates whether the term is set union
Definition at line 488 of file Expr.cs.
|
get |
Indicates whether the term is an array store.
It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.
Definition at line 451 of file Expr.cs.
|
get |
Indicates whether the term is subtraction (binary)
Definition at line 384 of file Expr.cs.
|
get |
Indicates whether the term is the constant true.
Definition at line 272 of file Expr.cs.
|
get |
Indicates whether the term is a unary minus
Definition at line 389 of file Expr.cs.
|
get |
|
get |
Indicates whether the term is an exclusive or
Definition at line 312 of file Expr.cs.
|
get |