Expressions are terms. More...
Public Member Functions | |
Expr | Simplify (Params p=null) |
Returns a simplified version of the expression. | |
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. | |
Expr | Substitute (Expr[] from, Expr[] to) |
Substitute every occurrence of from[i] in the expression with to[i] , for i smaller than num_exprs . | |
Expr | Substitute (Expr from, Expr to) |
Substitute every occurrence of from in the expression with to . | |
Expr | SubstituteVars (Expr[] to) |
Substitute the free variables in the expression with the expressions in to | |
new Expr | Translate (Context ctx) |
Translates (copies) the term to the Context ctx . | |
override string | ToString () |
Returns a string representation of the expression. | |
Protected Member Functions | |
internal | Expr (Context ctx) |
Constructor for Expr. | |
internal | Expr (Context ctx, IntPtr obj) |
Constructor for Expr. | |
Properties | |
FuncDecl | FuncDecl [get] |
The function declaration of the function that is applied in this expression. | |
Z3_lbool | BoolValue [get] |
Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF). | |
uint | NumArgs [get] |
The number of arguments of the expression. | |
Expr[] | Args [get] |
The arguments of the expression. | |
bool | IsNumeral [get] |
Indicates whether the term is a numeral. | |
bool | IsWellSorted [get] |
Indicates whether the term is well-sorted. | |
Sort | Sort [get] |
The Sort of the term. | |
bool | IsConst [get] |
Indicates whether the term represents a constant. | |
bool | IsIntNum [get] |
Indicates whether the term is an integer numeral. | |
bool | IsRatNum [get] |
Indicates whether the term is a real numeral. | |
bool | IsAlgebraicNumber [get] |
Indicates whether the term is an algebraic number. | |
bool | IsBool [get] |
Indicates whether the term has Boolean sort. | |
bool | IsTrue [get] |
Indicates whether the term is the constant true. | |
bool | IsFalse [get] |
Indicates whether the term is the constant false. | |
bool | IsEq [get] |
Indicates whether the term is an equality predicate. | |
bool | IsDistinct [get] |
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct). | |
bool | IsITE [get] |
Indicates whether the term is a ternary if-then-else term. | |
bool | IsAnd [get] |
Indicates whether the term is an n-ary conjunction. | |
bool | IsOr [get] |
Indicates whether the term is an n-ary disjunction. | |
bool | IsIff [get] |
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary) | |
bool | IsXor [get] |
Indicates whether the term is an exclusive or. | |
bool | IsNot [get] |
Indicates whether the term is a negation. | |
bool | IsImplies [get] |
Indicates whether the term is an implication. | |
bool | IsInterpolant [get] |
Indicates whether the term is marked for interpolation. | |
bool | IsInt [get] |
Indicates whether the term is of integer sort. | |
bool | IsReal [get] |
Indicates whether the term is of sort real. | |
bool | IsArithmeticNumeral [get] |
Indicates whether the term is an arithmetic numeral. | |
bool | IsLE [get] |
Indicates whether the term is a less-than-or-equal. | |
bool | IsGE [get] |
Indicates whether the term is a greater-than-or-equal. | |
bool | IsLT [get] |
Indicates whether the term is a less-than. | |
bool | IsGT [get] |
Indicates whether the term is a greater-than. | |
bool | IsAdd [get] |
Indicates whether the term is addition (binary) | |
bool | IsSub [get] |
Indicates whether the term is subtraction (binary) | |
bool | IsUMinus [get] |
Indicates whether the term is a unary minus. | |
bool | IsMul [get] |
Indicates whether the term is multiplication (binary) | |
bool | IsDiv [get] |
Indicates whether the term is division (binary) | |
bool | IsIDiv [get] |
Indicates whether the term is integer division (binary) | |
bool | IsRemainder [get] |
Indicates whether the term is remainder (binary) | |
bool | IsModulus [get] |
Indicates whether the term is modulus (binary) | |
bool | IsIntToReal [get] |
Indicates whether the term is a coercion of integer to real (unary) | |
bool | IsRealToInt [get] |
Indicates whether the term is a coercion of real to integer (unary) | |
bool | IsRealIsInt [get] |
Indicates whether the term is a check that tests whether a real is integral (unary) | |
bool | IsArray [get] |
Indicates whether the term is of an array sort. | |
bool | IsStore [get] |
Indicates whether the term is an array store. | |
bool | IsSelect [get] |
Indicates whether the term is an array select. | |
bool | IsConstantArray [get] |
Indicates whether the term is a constant array. | |
bool | IsDefaultArray [get] |
Indicates whether the term is a default array. | |
bool | IsArrayMap [get] |
Indicates whether the term is an array map. | |
bool | IsAsArray [get] |
Indicates whether the term is an as-array term. | |
bool | IsSetUnion [get] |
Indicates whether the term is set union. | |
bool | IsSetIntersect [get] |
Indicates whether the term is set intersection. | |
bool | IsSetDifference [get] |
Indicates whether the term is set difference. | |
bool | IsSetComplement [get] |
Indicates whether the term is set complement. | |
bool | IsSetSubset [get] |
Indicates whether the term is set subset. | |
bool | IsBV [get] |
Indicates whether the terms is of bit-vector sort. | |
bool | IsBVNumeral [get] |
Indicates whether the term is a bit-vector numeral. | |
bool | IsBVBitOne [get] |
Indicates whether the term is a one-bit bit-vector with value one. | |
bool | IsBVBitZero [get] |
Indicates whether the term is a one-bit bit-vector with value zero. | |
bool | IsBVUMinus [get] |
Indicates whether the term is a bit-vector unary minus. | |
bool | IsBVAdd [get] |
Indicates whether the term is a bit-vector addition (binary) | |
bool | IsBVSub [get] |
Indicates whether the term is a bit-vector subtraction (binary) | |
bool | IsBVMul [get] |
Indicates whether the term is a bit-vector multiplication (binary) | |
bool | IsBVSDiv [get] |
Indicates whether the term is a bit-vector signed division (binary) | |
bool | IsBVUDiv [get] |
Indicates whether the term is a bit-vector unsigned division (binary) | |
bool | IsBVSRem [get] |
Indicates whether the term is a bit-vector signed remainder (binary) | |
bool | IsBVURem [get] |
Indicates whether the term is a bit-vector unsigned remainder (binary) | |
bool | IsBVSMod [get] |
Indicates whether the term is a bit-vector signed modulus. | |
bool | IsBVULE [get] |
Indicates whether the term is an unsigned bit-vector less-than-or-equal. | |
bool | IsBVSLE [get] |
Indicates whether the term is a signed bit-vector less-than-or-equal. | |
bool | IsBVUGE [get] |
Indicates whether the term is an unsigned bit-vector greater-than-or-equal. | |
bool | IsBVSGE [get] |
Indicates whether the term is a signed bit-vector greater-than-or-equal. | |
bool | IsBVULT [get] |
Indicates whether the term is an unsigned bit-vector less-than. | |
bool | IsBVSLT [get] |
Indicates whether the term is a signed bit-vector less-than. | |
bool | IsBVUGT [get] |
Indicates whether the term is an unsigned bit-vector greater-than. | |
bool | IsBVSGT [get] |
Indicates whether the term is a signed bit-vector greater-than. | |
bool | IsBVAND [get] |
Indicates whether the term is a bit-wise AND. | |
bool | IsBVOR [get] |
Indicates whether the term is a bit-wise OR. | |
bool | IsBVNOT [get] |
Indicates whether the term is a bit-wise NOT. | |
bool | IsBVXOR [get] |
Indicates whether the term is a bit-wise XOR. | |
bool | IsBVNAND [get] |
Indicates whether the term is a bit-wise NAND. | |
bool | IsBVNOR [get] |
Indicates whether the term is a bit-wise NOR. | |
bool | IsBVXNOR [get] |
Indicates whether the term is a bit-wise XNOR. | |
bool | IsBVConcat [get] |
Indicates whether the term is a bit-vector concatenation (binary) | |
bool | IsBVSignExtension [get] |
Indicates whether the term is a bit-vector sign extension. | |
bool | IsBVZeroExtension [get] |
Indicates whether the term is a bit-vector zero extension. | |
bool | IsBVExtract [get] |
Indicates whether the term is a bit-vector extraction. | |
bool | IsBVRepeat [get] |
Indicates whether the term is a bit-vector repetition. | |
bool | IsBVReduceOR [get] |
Indicates whether the term is a bit-vector reduce OR. | |
bool | IsBVReduceAND [get] |
Indicates whether the term is a bit-vector reduce AND. | |
bool | IsBVComp [get] |
Indicates whether the term is a bit-vector comparison. | |
bool | IsBVShiftLeft [get] |
Indicates whether the term is a bit-vector shift left. | |
bool | IsBVShiftRightLogical [get] |
Indicates whether the term is a bit-vector logical shift right. | |
bool | IsBVShiftRightArithmetic [get] |
Indicates whether the term is a bit-vector arithmetic shift left. | |
bool | IsBVRotateLeft [get] |
Indicates whether the term is a bit-vector rotate left. | |
bool | IsBVRotateRight [get] |
Indicates whether the term is a bit-vector rotate right. | |
bool | IsBVRotateLeftExtended [get] |
Indicates whether the term is a bit-vector rotate left (extended) | |
bool | IsBVRotateRightExtended [get] |
Indicates whether the term is a bit-vector rotate right (extended) | |
bool | IsIntToBV [get] |
Indicates whether the term is a coercion from integer to bit-vector. | |
bool | IsBVToInt [get] |
Indicates whether the term is a coercion from bit-vector to integer. | |
bool | IsBVCarry [get] |
Indicates whether the term is a bit-vector carry. | |
bool | IsBVXOR3 [get] |
Indicates whether the term is a bit-vector ternary XOR. | |
bool | IsLabel [get] |
Indicates whether the term is a label (used by the Boogie Verification condition generator). | |
bool | IsLabelLit [get] |
Indicates whether the term is a label literal (used by the Boogie Verification condition generator). | |
bool | IsOEQ [get] |
Indicates whether the term is a binary equivalence modulo namings. | |
bool | IsProofTrue [get] |
Indicates whether the term is a Proof for the expression 'true'. | |
bool | IsProofAsserted [get] |
Indicates whether the term is a proof for a fact asserted by the user. | |
bool | IsProofGoal [get] |
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user. | |
bool | IsProofModusPonens [get] |
Indicates whether the term is proof via modus ponens. | |
bool | IsProofReflexivity [get] |
Indicates whether the term is a proof for (R t t), where R is a reflexive relation. | |
bool | IsProofSymmetry [get] |
Indicates whether the term is proof by symmetricity of a relation. | |
bool | IsProofTransitivity [get] |
Indicates whether the term is a proof by transitivity of a relation. | |
bool | IsProofTransitivityStar [get] |
Indicates whether the term is a proof by condensed transitivity of a relation. | |
bool | IsProofMonotonicity [get] |
Indicates whether the term is a monotonicity proof object. | |
bool | IsProofQuantIntro [get] |
Indicates whether the term is a quant-intro proof. | |
bool | IsProofDistributivity [get] |
Indicates whether the term is a distributivity proof object. | |
bool | IsProofAndElimination [get] |
Indicates whether the term is a proof by elimination of AND. | |
bool | IsProofOrElimination [get] |
Indicates whether the term is a proof by eliminiation of not-or. | |
bool | IsProofRewrite [get] |
Indicates whether the term is a proof by rewriting. | |
bool | IsProofRewriteStar [get] |
Indicates whether the term is a proof by rewriting. | |
bool | IsProofPullQuant [get] |
Indicates whether the term is a proof for pulling quantifiers out. | |
bool | IsProofPullQuantStar [get] |
Indicates whether the term is a proof for pulling quantifiers out. | |
bool | IsProofPushQuant [get] |
Indicates whether the term is a proof for pushing quantifiers in. | |
bool | IsProofElimUnusedVars [get] |
Indicates whether the term is a proof for elimination of unused variables. | |
bool | IsProofDER [get] |
Indicates whether the term is a proof for destructive equality resolution. | |
bool | IsProofQuantInst [get] |
Indicates whether the term is a proof for quantifier instantiation. | |
bool | IsProofHypothesis [get] |
Indicates whether the term is a hypthesis marker. | |
bool | IsProofLemma [get] |
Indicates whether the term is a proof by lemma. | |
bool | IsProofUnitResolution [get] |
Indicates whether the term is a proof by unit resolution. | |
bool | IsProofIFFTrue [get] |
Indicates whether the term is a proof by iff-true. | |
bool | IsProofIFFFalse [get] |
Indicates whether the term is a proof by iff-false. | |
bool | IsProofCommutativity [get] |
Indicates whether the term is a proof by commutativity. | |
bool | IsProofDefAxiom [get] |
Indicates whether the term is a proof for Tseitin-like axioms. | |
bool | IsProofDefIntro [get] |
Indicates whether the term is a proof for introduction of a name. | |
bool | IsProofApplyDef [get] |
Indicates whether the term is a proof for application of a definition. | |
bool | IsProofIFFOEQ [get] |
Indicates whether the term is a proof iff-oeq. | |
bool | IsProofNNFPos [get] |
Indicates whether the term is a proof for a positive NNF step. | |
bool | IsProofNNFNeg [get] |
Indicates whether the term is a proof for a negative NNF step. | |
bool | IsProofNNFStar [get] |
Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form. | |
bool | IsProofCNFStar [get] |
Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form. | |
bool | IsProofSkolemize [get] |
Indicates whether the term is a proof for a Skolemization step. | |
bool | IsProofModusPonensOEQ [get] |
Indicates whether the term is a proof by modus ponens for equi-satisfiability. | |
bool | IsProofTheoryLemma [get] |
Indicates whether the term is a proof for theory lemma. | |
bool | IsRelation [get] |
Indicates whether the term is of an array sort. | |
bool | IsRelationStore [get] |
Indicates whether the term is an relation store. | |
bool | IsEmptyRelation [get] |
Indicates whether the term is an empty relation. | |
bool | IsIsEmptyRelation [get] |
Indicates whether the term is a test for the emptiness of a relation. | |
bool | IsRelationalJoin [get] |
Indicates whether the term is a relational join. | |
bool | IsRelationUnion [get] |
Indicates whether the term is the union or convex hull of two relations. | |
bool | IsRelationWiden [get] |
Indicates whether the term is the widening of two relations. | |
bool | IsRelationProject [get] |
Indicates whether the term is a projection of columns (provided as numbers in the parameters). | |
bool | IsRelationFilter [get] |
Indicates whether the term is a relation filter. | |
bool | IsRelationNegationFilter [get] |
Indicates whether the term is an intersection of a relation with the negation of another. | |
bool | IsRelationRename [get] |
Indicates whether the term is the renaming of a column in a relation. | |
bool | IsRelationComplement [get] |
Indicates whether the term is the complement of a relation. | |
bool | IsRelationSelect [get] |
Indicates whether the term is a relational select. | |
bool | IsRelationClone [get] |
Indicates whether the term is a relational clone (copy) | |
bool | IsFiniteDomain [get] |
Indicates whether the term is of an array sort. | |
bool | IsFiniteDomainLT [get] |
Indicates whether the term is a less than predicate over a finite domain. | |
uint | Index [get] |
The de-Burijn index of a bound variable. |
Constructor for Expr.
Definition at line 1492 of file Expr.cs.
: base(ctx) { Contract.Requires(ctx != null); }
Constructor for Expr.
Definition at line 1496 of file Expr.cs.
: base(ctx, obj) { Contract.Requires(ctx != null); }
Returns a simplified version of the expression.
p | A set of parameters to configure the simplifier |
Expr Substitute | ( | Expr[] | from, |
Expr[] | to | ||
) | [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 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]
.
Definition at line 115 of file Expr.cs.
{ Contract.Requires(from != null); Contract.Requires(to != null); Contract.Requires(Contract.ForAll(from, f => f != null)); Contract.Requires(Contract.ForAll(to, t => t != null)); Contract.Ensures(Contract.Result<Expr>() != null); Context.CheckContextMatch(from); Context.CheckContextMatch(to); if (from.Length != to.Length) throw new Z3Exception("Argument sizes do not match"); return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to))); }
Expr Substitute | ( | Expr | from, |
Expr | to | ||
) | [inline] |
Substitute every occurrence of from
in the expression with to
.
Definition at line 134 of file Expr.cs.
{ Contract.Requires(from != null); Contract.Requires(to != null); Contract.Ensures(Contract.Result<Expr>() != null); return Substitute(new Expr[] { from }, new Expr[] { to }); }
Expr SubstituteVars | ( | Expr[] | to | ) | [inline] |
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]
.
override string ToString | ( | ) | [inline] |
Returns a string representation of the expression.
Reimplemented from AST.
Definition at line 178 of file Expr.cs.
Referenced by Expr.ToString().
{
return base.ToString();
}
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.
{ Contract.Requires(args != null); Contract.Requires(Contract.ForAll(args, a => a != null)); Context.CheckContextMatch(args); if (IsApp && args.Length != NumArgs) throw new Z3Exception("Number of arguments does not match"); NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args)); }
The function declaration of the function that is applied in this expression.
Definition at line 50 of file Expr.cs.
Referenced by Model.ConstInterp().
uint Index [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.
abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
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.
bool IsAdd [get] |
bool IsAlgebraicNumber [get] |
bool IsAnd [get] |
bool IsArithmeticNumeral [get] |
bool IsArray [get] |
bool IsArrayMap [get] |
bool IsAsArray [get] |
bool IsBool [get] |
bool IsBV [get] |
bool IsBVAdd [get] |
bool IsBVAND [get] |
bool IsBVBitOne [get] |
bool IsBVBitZero [get] |
bool IsBVCarry [get] |
bool IsBVComp [get] |
bool IsBVConcat [get] |
bool IsBVExtract [get] |
bool IsBVMul [get] |
bool IsBVNAND [get] |
bool IsBVNOR [get] |
bool IsBVNOT [get] |
bool IsBVNumeral [get] |
bool IsBVOR [get] |
bool IsBVReduceAND [get] |
bool IsBVReduceOR [get] |
bool IsBVRepeat [get] |
bool IsBVRotateLeft [get] |
bool IsBVRotateLeftExtended [get] |
bool IsBVRotateRight [get] |
bool IsBVRotateRightExtended [get] |
bool IsBVSDiv [get] |
bool IsBVSGE [get] |
bool IsBVSGT [get] |
bool IsBVShiftLeft [get] |
bool IsBVShiftRightArithmetic [get] |
bool IsBVShiftRightLogical [get] |
bool IsBVSignExtension [get] |
bool IsBVSLE [get] |
bool IsBVSLT [get] |
bool IsBVSMod [get] |
bool IsBVSRem [get] |
bool IsBVSub [get] |
bool IsBVToInt [get] |
bool IsBVUDiv [get] |
bool IsBVUGE [get] |
bool IsBVUGT [get] |
bool IsBVULE [get] |
bool IsBVULT [get] |
bool IsBVUMinus [get] |
bool IsBVURem [get] |
bool IsBVXNOR [get] |
bool IsBVXOR [get] |
bool IsBVXOR3 [get] |
bool IsBVZeroExtension [get] |
bool IsConst [get] |
bool IsConstantArray [get] |
bool IsDefaultArray [get] |
bool IsDistinct [get] |
bool IsDiv [get] |
bool IsEmptyRelation [get] |
bool IsEq [get] |
bool IsFalse [get] |
bool IsFiniteDomain [get] |
bool IsFiniteDomainLT [get] |
bool IsGE [get] |
bool IsGT [get] |
bool IsIDiv [get] |
bool IsIff [get] |
bool IsImplies [get] |
bool IsInt [get] |
bool IsInterpolant [get] |
bool IsIntNum [get] |
bool IsIntToBV [get] |
bool IsIntToReal [get] |
bool IsIsEmptyRelation [get] |
bool IsITE [get] |
bool IsLabel [get] |
bool IsLabelLit [get] |
bool IsLE [get] |
bool IsModulus [get] |
bool IsMul [get] |
bool IsNumeral [get] |
bool IsOEQ [get] |
bool IsOr [get] |
bool IsProofAndElimination [get] |
bool IsProofApplyDef [get] |
bool IsProofAsserted [get] |
bool IsProofCNFStar [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.
bool IsProofCommutativity [get] |
bool IsProofDefAxiom [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).
bool IsProofDefIntro [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: [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)
bool IsProofDER [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.
bool IsProofDistributivity [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.
bool IsProofElimUnusedVars [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.
bool IsProofGoal [get] |
bool IsProofHypothesis [get] |
bool IsProofIFFFalse [get] |
bool IsProofIFFOEQ [get] |
bool IsProofIFFTrue [get] |
bool IsProofLemma [get] |
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.
bool IsProofModusPonens [get] |
bool IsProofModusPonensOEQ [get] |
bool IsProofMonotonicity [get] |
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.
bool IsProofNNFNeg [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 [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')))
bool IsProofNNFPos [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' [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_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 [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'.
bool IsProofNNFStar [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.
bool IsProofOrElimination [get] |
bool IsProofPullQuant [get] |
bool IsProofPullQuantStar [get] |
bool IsProofPushQuant [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
bool IsProofQuantInst [get] |
bool IsProofQuantIntro [get] |
bool IsProofReflexivity [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'.
bool IsProofRewrite [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)
bool IsProofRewriteStar [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:
bool IsProofSkolemize [get] |
bool IsProofSymmetry [get] |
bool IsProofTheoryLemma [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:
bool IsProofTransitivity [get] |
bool IsProofTransitivityStar [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.
bool IsProofTrue [get] |
bool IsProofUnitResolution [get] |
bool IsRatNum [get] |
bool IsReal [get] |
bool IsRealIsInt [get] |
bool IsRealToInt [get] |
bool IsRelation [get] |
bool IsRelationalJoin [get] |
bool IsRelationClone [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.
bool IsRelationComplement [get] |
bool IsRelationFilter [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.
bool IsRelationNegationFilter [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.
bool IsRelationProject [get] |
bool IsRelationRename [get] |
bool IsRelationSelect [get] |
bool IsRelationStore [get] |
bool IsRelationUnion [get] |
bool IsRelationWiden [get] |
bool IsRemainder [get] |
bool IsSelect [get] |
bool IsSetComplement [get] |
bool IsSetDifference [get] |
bool IsSetIntersect [get] |
bool IsSetSubset [get] |
bool IsSetUnion [get] |
bool IsStore [get] |
bool IsSub [get] |
bool IsTrue [get] |
bool IsUMinus [get] |
bool IsWellSorted [get] |
bool IsXor [get] |
uint NumArgs [get] |