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.  
Public Member Functions inherited from AST  
override bool  Equals (object o) 
Object comparison.  
virtual int  CompareTo (object other) 
Object Comparison.  
override int  GetHashCode () 
The AST's hash code.  
AST  Translate (Context ctx) 
Translates (copies) the AST to the Context ctx .  
override string  ToString () 
A string representation of the AST.  
string  SExpr () 
A string representation of the AST in sexpression notation.  
Public Member Functions inherited from Z3Object  
void  Dispose () 
Disposes of the underlying native Z3 object.  
Protected Member Functions  
Expr (Context ctx)  
Constructor for Expr  
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 wellsorted.  
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 nary distinct predicate (every argument is mutually distinct).  
bool  IsITE [get] 
Indicates whether the term is a ternary ifthenelse term  
bool  IsAnd [get] 
Indicates whether the term is an nary conjunction  
bool  IsOr [get] 
Indicates whether the term is an nary disjunction  
bool  IsIff [get] 
Indicates whether the term is an ifandonlyif (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  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 lessthanorequal  
bool  IsGE [get] 
Indicates whether the term is a greaterthanorequal  
bool  IsLT [get] 
Indicates whether the term is a lessthan  
bool  IsGT [get] 
Indicates whether the term is a greaterthan  
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 asarray 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 bitvector sort.  
bool  IsBVNumeral [get] 
Indicates whether the term is a bitvector numeral  
bool  IsBVBitOne [get] 
Indicates whether the term is a onebit bitvector with value one  
bool  IsBVBitZero [get] 
Indicates whether the term is a onebit bitvector with value zero  
bool  IsBVUMinus [get] 
Indicates whether the term is a bitvector unary minus  
bool  IsBVAdd [get] 
Indicates whether the term is a bitvector addition (binary)  
bool  IsBVSub [get] 
Indicates whether the term is a bitvector subtraction (binary)  
bool  IsBVMul [get] 
Indicates whether the term is a bitvector multiplication (binary)  
bool  IsBVSDiv [get] 
Indicates whether the term is a bitvector signed division (binary)  
bool  IsBVUDiv [get] 
Indicates whether the term is a bitvector unsigned division (binary)  
bool  IsBVSRem [get] 
Indicates whether the term is a bitvector signed remainder (binary)  
bool  IsBVURem [get] 
Indicates whether the term is a bitvector unsigned remainder (binary)  
bool  IsBVSMod [get] 
Indicates whether the term is a bitvector signed modulus  
bool  IsBVULE [get] 
Indicates whether the term is an unsigned bitvector lessthanorequal  
bool  IsBVSLE [get] 
Indicates whether the term is a signed bitvector lessthanorequal  
bool  IsBVUGE [get] 
Indicates whether the term is an unsigned bitvector greaterthanorequal  
bool  IsBVSGE [get] 
Indicates whether the term is a signed bitvector greaterthanorequal  
bool  IsBVULT [get] 
Indicates whether the term is an unsigned bitvector lessthan  
bool  IsBVSLT [get] 
Indicates whether the term is a signed bitvector lessthan  
bool  IsBVUGT [get] 
Indicates whether the term is an unsigned bitvector greaterthan  
bool  IsBVSGT [get] 
Indicates whether the term is a signed bitvector greaterthan  
bool  IsBVAND [get] 
Indicates whether the term is a bitwise AND  
bool  IsBVOR [get] 
Indicates whether the term is a bitwise OR  
bool  IsBVNOT [get] 
Indicates whether the term is a bitwise NOT  
bool  IsBVXOR [get] 
Indicates whether the term is a bitwise XOR  
bool  IsBVNAND [get] 
Indicates whether the term is a bitwise NAND  
bool  IsBVNOR [get] 
Indicates whether the term is a bitwise NOR  
bool  IsBVXNOR [get] 
Indicates whether the term is a bitwise XNOR  
bool  IsBVConcat [get] 
Indicates whether the term is a bitvector concatenation (binary)  
bool  IsBVSignExtension [get] 
Indicates whether the term is a bitvector sign extension  
bool  IsBVZeroExtension [get] 
Indicates whether the term is a bitvector zero extension  
bool  IsBVExtract [get] 
Indicates whether the term is a bitvector extraction  
bool  IsBVRepeat [get] 
Indicates whether the term is a bitvector repetition  
bool  IsBVReduceOR [get] 
Indicates whether the term is a bitvector reduce OR  
bool  IsBVReduceAND [get] 
Indicates whether the term is a bitvector reduce AND  
bool  IsBVComp [get] 
Indicates whether the term is a bitvector comparison  
bool  IsBVShiftLeft [get] 
Indicates whether the term is a bitvector shift left  
bool  IsBVShiftRightLogical [get] 
Indicates whether the term is a bitvector logical shift right  
bool  IsBVShiftRightArithmetic [get] 
Indicates whether the term is a bitvector arithmetic shift left  
bool  IsBVRotateLeft [get] 
Indicates whether the term is a bitvector rotate left  
bool  IsBVRotateRight [get] 
Indicates whether the term is a bitvector rotate right  
bool  IsBVRotateLeftExtended [get] 
Indicates whether the term is a bitvector rotate left (extended)  
bool  IsBVRotateRightExtended [get] 
Indicates whether the term is a bitvector rotate right (extended)  
bool  IsIntToBV [get] 
Indicates whether the term is a coercion from integer to bitvector  
bool  IsBVToInt [get] 
Indicates whether the term is a coercion from bitvector to integer  
bool  IsBVCarry [get] 
Indicates whether the term is a bitvector carry  
bool  IsBVXOR3 [get] 
Indicates whether the term is a bitvector 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 quantintro 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 notor  
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 ifftrue  
bool  IsProofIFFFalse [get] 
Indicates whether the term is a proof by ifffalse  
bool  IsProofCommutativity [get] 
Indicates whether the term is a proof by commutativity  
bool  IsProofDefAxiom [get] 
Indicates whether the term is a proof for Tseitinlike 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 iffoeq  
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 equisatisfiability.  
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 deBurijn index of a bound variable.  
Properties inherited from AST  
uint  Id [get] 
A unique identifier for the AST (unique among all ASTs).  
Z3_ast_kind  ASTKind [get] 
The kind of the AST.  
bool  IsExpr [get] 
Indicates whether the AST is an Expr  
bool  IsVar [get] 
Indicates whether the AST is a BoundVariable  
bool  IsQuantifier [get] 
Indicates whether the AST is a Quantifier  
bool  IsSort [get] 
Indicates whether the AST is a Sort  
bool  IsFuncDecl [get] 
Indicates whether the AST is a FunctionDeclaration  
Additional Inherited Members  
Static Public Member Functions inherited from AST  
static bool  operator== (AST a, AST b) 
Comparison operator.  
static bool  operator!= (AST a, AST b) 
Comparison operator.  
Constructor for Expr
Definition at line 1481 of file Expr.cs.
Constructor for Expr
Definition at line 1485 of file Expr.cs.
Returns a simplified version of the expression.
p  A set of parameters to configure the simplifier 
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.
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 deBruijn index i
is replaced with term to[i]
.

inline 
Returns a string representation of the expression.
Definition at line 178 of file Expr.cs.
Referenced by Expr.ToString().
Translates (copies) the term to the Context ctx .
ctx  A context 

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 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 deBurijn index of a bound variable.
Bound variables are indexed by deBruijn indices. It is perhaps easiest to explain the meaning of deBruijn indices by indicating the compilation process from nondeBruijn formulas to deBruijn 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.

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

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.

get 

get 
Indicates whether the term is a proof for Tseitinlike 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).

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 defintro 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: [defintro]: (= n e)

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.

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.

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.

get 

get 

get 

get 

get 

get 

get 

get 

get 

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')))

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 toplevel 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'.

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.

get 

get 

get 

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

get 

get 

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'.

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 equisatisfiability (~ t s). Remark: if f is bool, then = is iff.
Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

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:

get 

get 

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:

get 

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.

get 

get 

get 

get 

get 

get 

get 

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.

get 

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 deBrujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.

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.

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 

get 