Package com.microsoft.z3

Class Expr<R extends Sort>

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Expr<R>

All Implemented Interfaces:

Comparable<AST>

Direct Known Subclasses:

ArithExpr, ArrayExpr, BitVecExpr, BoolExpr, DatatypeExpr, FiniteDomainExpr, FPExpr, FPRMExpr, ReExpr, SeqExpr

public class Expr<R extends Sort>
extends AST

Expressions are terms.

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	Expr(Context ctx, long obj)	Constructor for Expr

Method Summary

Modifier and Type	Method	Description
<S extends R> Expr<S>	distillSort(Class<S> newSort)	Downcast sort of this expression.
Expr<?>[]	getArgs()	The arguments of the expression.
Z3_lbool	getBoolValue()	Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).
FuncDecl<R>	getFuncDecl()	The function declaration of the function that is applied in this expression.
int	getIndex()	The de-Bruijn index of a bound variable.
int	getNumArgs()	The number of arguments of the expression.
R	getSort()	The Sort of the term.
String	getString()	Retrieve string corresponding to string constant.
boolean	isAdd()	Indicates whether the term is addition (binary)
boolean	isAlgebraicNumber()	Indicates whether the term is an algebraic number
boolean	isAnd()	Indicates whether the term is an n-ary conjunction
boolean	isArithmeticNumeral()	Indicates whether the term is an arithmetic numeral.
boolean	isArray()	Indicates whether the term is of an array sort.
boolean	isArrayMap()	Indicates whether the term is an array map.
boolean	isAsArray()	Indicates whether the term is an as-array term.
boolean	isBool()	Indicates whether the term has Boolean sort.
boolean	isBV()	Indicates whether the terms is of bit-vector sort.
boolean	isBVAdd()	Indicates whether the term is a bit-vector addition (binary)
boolean	isBVAND()	Indicates whether the term is a bit-wise AND
boolean	isBVBitOne()	Indicates whether the term is a one-bit bit-vector with value one
boolean	isBVBitZero()	Indicates whether the term is a one-bit bit-vector with value zero
boolean	isBVCarry()	Indicates whether the term is a bit-vector carry Remarks: Compute the * carry bit in a full-adder.
boolean	isBVComp()	Indicates whether the term is a bit-vector comparison
boolean	isBVConcat()	Indicates whether the term is a bit-vector concatenation (binary)
boolean	isBVExtract()	Indicates whether the term is a bit-vector extraction
boolean	isBVMul()	Indicates whether the term is a bit-vector multiplication (binary)
boolean	isBVNAND()	Indicates whether the term is a bit-wise NAND
boolean	isBVNOR()	Indicates whether the term is a bit-wise NOR
boolean	isBVNOT()	Indicates whether the term is a bit-wise NOT
boolean	isBVNumeral()	Indicates whether the term is a bit-vector numeral
boolean	isBVOR()	Indicates whether the term is a bit-wise OR
boolean	isBVReduceAND()	Indicates whether the term is a bit-vector reduce AND
boolean	isBVReduceOR()	Indicates whether the term is a bit-vector reduce OR
boolean	isBVRepeat()	Indicates whether the term is a bit-vector repetition
boolean	isBVRotateLeft()	Indicates whether the term is a bit-vector rotate left
boolean	isBVRotateLeftExtended()	Indicates whether the term is a bit-vector rotate left (extended) Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.
boolean	isBVRotateRight()	Indicates whether the term is a bit-vector rotate right
boolean	isBVRotateRightExtended()	Indicates whether the term is a bit-vector rotate right (extended) Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.
boolean	isBVSDiv()	Indicates whether the term is a bit-vector signed division (binary)
boolean	isBVSGE()	Indicates whether the term is a signed bit-vector greater-than-or-equal
boolean	isBVSGT()	Indicates whether the term is a signed bit-vector greater-than
boolean	isBVShiftLeft()	Indicates whether the term is a bit-vector shift left
boolean	isBVShiftRightArithmetic()	Indicates whether the term is a bit-vector arithmetic shift left
boolean	isBVShiftRightLogical()	Indicates whether the term is a bit-vector logical shift right
boolean	isBVSignExtension()	Indicates whether the term is a bit-vector sign extension
boolean	isBVSLE()	Indicates whether the term is a signed bit-vector less-than-or-equal
boolean	isBVSLT()	Indicates whether the term is a signed bit-vector less-than
boolean	isBVSMod()	Indicates whether the term is a bit-vector signed modulus
boolean	isBVSRem()	Indicates whether the term is a bit-vector signed remainder (binary)
boolean	isBVSub()	Indicates whether the term is a bit-vector subtraction (binary)
boolean	isBVToInt()	Indicates whether the term is a coercion from bit-vector to integer Remarks: This function is not supported by the decision procedures.
boolean	isBVUDiv()	Indicates whether the term is a bit-vector unsigned division (binary)
boolean	isBVUGE()	Indicates whether the term is an unsigned bit-vector greater-than-or-equal
boolean	isBVUGT()	Indicates whether the term is an unsigned bit-vector greater-than
boolean	isBVULE()	Indicates whether the term is an unsigned bit-vector less-than-or-equal
boolean	isBVULT()	Indicates whether the term is an unsigned bit-vector less-than
boolean	isBVUMinus()	Indicates whether the term is a bit-vector unary minus
boolean	isBVURem()	Indicates whether the term is a bit-vector unsigned remainder (binary)
boolean	isBVXNOR()	Indicates whether the term is a bit-wise XNOR
boolean	isBVXOR()	Indicates whether the term is a bit-wise XOR
boolean	isBVXOR3()	Indicates whether the term is a bit-vector ternary XOR Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor * l1 l2) l3)
boolean	isBVZeroExtension()	Indicates whether the term is a bit-vector zero extension
boolean	isConcat()	Check whether expression is a concatenation
boolean	isConst()	Indicates whether the term represents a constant.
boolean	isConstantArray()	Indicates whether the term is a constant array.
boolean	isDefaultArray()	Indicates whether the term is a default array.
boolean	isDistinct()	Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
boolean	isDiv()	Indicates whether the term is division (binary)
boolean	isEmptyRelation()	Indicates whether the term is an empty relation
boolean	isEq()	Indicates whether the term is an equality predicate.
boolean	isFalse()	Indicates whether the term is the constant false.
boolean	isFiniteDomain()	Indicates whether the term is of an array sort.
boolean	isFiniteDomainLT()	Indicates whether the term is a less than predicate over a finite domain.
boolean	isGE()	Indicates whether the term is a greater-than-or-equal
boolean	isGT()	Indicates whether the term is a greater-than
boolean	isIDiv()	Indicates whether the term is integer division (binary)
boolean	isIff()	Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
boolean	isImplies()	Indicates whether the term is an implication
boolean	isInt()	Indicates whether the term is of integer sort.
boolean	isIntNum()	Indicates whether the term is an integer numeral.
boolean	isIntToBV()	Indicates whether the term is a coercion from integer to bit-vector Remarks: This function is not supported by the decision procedures.
boolean	isIntToReal()	Indicates whether the term is a coercion of integer to real (unary)
boolean	isIsEmptyRelation()	Indicates whether the term is a test for the emptiness of a relation
boolean	isITE()	Indicates whether the term is a ternary if-then-else term
boolean	isLabel()	Indicates whether the term is a label (used by the Boogie Verification condition generator).
boolean	isLabelLit()	Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
boolean	isLE()	Indicates whether the term is a less-than-or-equal
boolean	isLT()	Indicates whether the term is a less-than
boolean	isModulus()	Indicates whether the term is modulus (binary)
boolean	isMul()	Indicates whether the term is multiplication (binary)
boolean	isNot()	Indicates whether the term is a negation
boolean	isNumeral()	Indicates whether the term is a numeral
boolean	isOEQ()	Indicates whether the term is a binary equivalence modulo namings.
boolean	isOr()	Indicates whether the term is an n-ary disjunction
boolean	isProofAndElimination()	Indicates whether the term is a proof by elimination of AND Remarks: * Given a proof for (and l_1 ...
boolean	isProofApplyDef()	Indicates whether the term is a proof for application of a definition Remarks: [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.
boolean	isProofAsserted()	Indicates whether the term is a proof for a fact asserted by the user.
boolean	isProofCommutativity()	Indicates whether the term is a proof by commutativity Remarks: [comm]: (= (f a b) (f b a)) f is a commutative operator.
boolean	isProofDefAxiom()	Indicates whether the term is a proof for Tseitin-like axioms Remarks: 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) ...
boolean	isProofDefIntro()	Indicates whether the term is a proof for introduction of a name Remarks: Introduces a name for a formula/term.
boolean	isProofDER()	Indicates whether the term is a proof for destructive equality resolution Remarks: A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.
boolean	isProofDistributivity()	Indicates whether the term is a distributivity proof object.
boolean	isProofElimUnusedVars()	Indicates whether the term is a proof for elimination of unused variables.
boolean	isProofGoal()	Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
boolean	isProofHypothesis()	Indicates whether the term is a hypothesis marker.
boolean	isProofIFFFalse()	Indicates whether the term is a proof by iff-false Remarks: T1: (not p) [iff-false T1]: (iff p false)
boolean	isProofIFFOEQ()	Indicates whether the term is a proof iff-oeq Remarks: T1: (iff p q) [iff~ T1]: (~ p q)
boolean	isProofIFFTrue()	Indicates whether the term is a proof by iff-true Remarks: T1: p [iff-true T1]: (iff p true)
boolean	isProofLemma()	Indicates whether the term is a proof by lemma Remarks: T1: false [lemma T1]: (or (not l_1) ...
boolean	isProofModusPonens()	Indicates whether the term is proof via modus ponens Remarks: Given a proof for p and a proof for (implies p q), produces a proof for q.
boolean	isProofModusPonensOEQ()	Indicates whether the term is a proof by modus ponens for equi-satisfiability.
boolean	isProofMonotonicity()	Indicates whether the term is a monotonicity proof object.
boolean	isProofNNFNeg()	Indicates whether the term is a proof for a negative NNF step Remarks: Proof for a (negative) NNF step.
boolean	isProofNNFPos()	Indicates whether the term is a proof for a positive NNF step Remarks: Proof for a (positive) NNF step.
boolean	isProofOrElimination()	Indicates whether the term is a proof by elimination of not-or Remarks: * Given a proof for (not (or l_1 ...
boolean	isProofPullQuant()	Indicates whether the term is a proof for pulling quantifiers out.
boolean	isProofPushQuant()	Indicates whether the term is a proof for pushing quantifiers in.
boolean	isProofQuantInst()	Indicates whether the term is a proof for quantifier instantiation Remarks: A proof of (or (not (forall (x) (P x))) (P a))
boolean	isProofQuantIntro()	Indicates whether the term is a quant-intro proof Remarks: Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).
boolean	isProofReflexivity()	Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
boolean	isProofRewrite()	Indicates whether the term is a proof by rewriting Remarks: A proof for a local rewriting step (= t s).
boolean	isProofRewriteStar()	Indicates whether the term is a proof by rewriting Remarks: A proof for rewriting an expression t into an expression s.
boolean	isProofSkolemize()	Indicates whether the term is a proof for a Skolemization step Remarks: Proof for: [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x (p x y)) (p (sk y) y)) This proof object has no antecedents.
boolean	isProofSymmetry()	Indicates whether the term is proof by symmetricity of a relation Remarks: Given an symmetric relation R and a proof for (R t s), produces * a proof for (R s t).
boolean	isProofTheoryLemma()	Indicates whether the term is a proof for theory lemma Remarks: Generic proof for theory lemmas.
boolean	isProofTransitivity()	Indicates whether the term is a proof by transitivity of a relation Remarks: Given a transitive relation R, and proofs for (R t s) and (R s * u), produces a proof for (R t u).
boolean	isProofTransitivityStar()	Indicates whether the term is a proof by condensed transitivity of a relation Remarks: Condensed transitivity proof.
boolean	isProofTrue()	Indicates whether the term is a Proof for the expression 'true'.
boolean	isProofUnitResolution()	Indicates whether the term is a proof by unit resolution Remarks: T1: * (or l_1 ...
boolean	isRatNum()	Indicates whether the term is a real numeral.
boolean	isReal()	Indicates whether the term is of sort real.
boolean	isRealIsInt()	Indicates whether the term is a check that tests whether a real is integral (unary)
boolean	isRealToInt()	Indicates whether the term is a coercion of real to integer (unary)
boolean	isRelation()	Indicates whether the term is of an array sort.
boolean	isRelationalJoin()	Indicates whether the term is a relational join
boolean	isRelationClone()	Indicates whether the term is a relational clone (copy) Remarks: Create a fresh copy (clone) of a relation.
boolean	isRelationComplement()	Indicates whether the term is the complement of a relation
boolean	isRelationFilter()	Indicates whether the term is a relation filter Remarks: Filter (restrict) a relation with respect to a predicate.
boolean	isRelationNegationFilter()	Indicates whether the term is an intersection of a relation with the negation of another.
boolean	isRelationProject()	Indicates whether the term is a projection of columns (provided as numbers in the parameters).
boolean	isRelationRename()	Indicates whether the term is the renaming of a column in a relation Remarks: The function takes one argument.
boolean	isRelationSelect()	Indicates whether the term is a relational select Remarks: Check if a record is an element of the relation.
boolean	isRelationStore()	Indicates whether the term is an relation store Remarks: Insert a record into a relation.
boolean	isRelationUnion()	Indicates whether the term is the union or convex hull of two relations.
boolean	isRelationWiden()	Indicates whether the term is the widening of two relations Remarks: The function takes two arguments.
boolean	isRemainder()	Indicates whether the term is remainder (binary)
boolean	isSelect()	Indicates whether the term is an array select.
boolean	isSetComplement()	Indicates whether the term is set complement
boolean	isSetDifference()	Indicates whether the term is set difference
boolean	isSetIntersect()	Indicates whether the term is set intersection
boolean	isSetSubset()	Indicates whether the term is set subset
boolean	isSetUnion()	Indicates whether the term is set union
boolean	isStore()	Indicates whether the term is an array store.
boolean	isString()	Check whether expression is a string constant.
boolean	isSub()	Indicates whether the term is subtraction (binary)
boolean	isTrue()	Indicates whether the term is the constant true.
boolean	isUMinus()	Indicates whether the term is a unary minus
boolean	isWellSorted()	Indicates whether the term is well-sorted.
boolean	isXor()	Indicates whether the term is an exclusive or
Expr<R>	simplify()	Returns a simplified version of the expression
Expr<R>	simplify(Params p)	Returns a simplified version of the expression A set of parameters
Expr<R>	substitute(Expr<?>[] from, Expr<?>[] to)	Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
Expr<R>	substitute(Expr<?> from, Expr<?> to)	Substitute every occurrence of from in the expression with to.
Expr<R>	substituteVars(Expr<?>[] to)	Substitute the free variables in the expression with the expressions in to Remarks: For every i smaller than * num_exprs, the variable with de-Bruijn index i * is replaced with term to[i].
String	toString()	Returns a string representation of the expression.
Expr<R>	translate(Context ctx)	Translates (copies) the term to the Context ctx.
Expr<R>	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.

Methods inherited from class com.microsoft.z3.AST

compareTo, equals, getASTKind, getId, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Details

Expr

protected Expr(Context ctx,
 long obj)

Constructor for Expr

Throws:

Z3Exception - on error

Method Details

simplify

public Expr<R> simplify()

Returns a simplified version of the expression

Returns:

Expr

Throws:

Z3Exception - on error

simplify

public Expr<R> simplify(Params p)

Returns a simplified version of the expression A set of parameters

Parameters:

p - a Params object to configure the simplifier

Returns:

an Expr

Throws:

Z3Exception - on error

See Also:

• Context.SimplifyHelp()

getFuncDecl

public FuncDecl<R> getFuncDecl()

The function declaration of the function that is applied in this expression.

Returns:

a FuncDecl

Throws:

Z3Exception - on error

getBoolValue

public Z3_lbool getBoolValue()

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).

Returns:

a Z3_lbool

Throws:

Z3Exception - on error

getNumArgs

public int getNumArgs()

The number of arguments of the expression.

Returns:

an int

Throws:

Z3Exception - on error

getArgs

public Expr<?>[] getArgs()

The arguments of the expression.

Returns:

an Expr[]

Throws:

Z3Exception - on error

update

public Expr<R> 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.

Parameters:

args - arguments

Throws:

Z3Exception - on error

substitute

public Expr<R> substitute(Expr<?>[] from,
 Expr<?>[] to)

Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs. Remarks: 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].

Returns:

an Expr

Throws:

Z3Exception - on error

substitute

public Expr<R> substitute(Expr<?> from,
 Expr<?> to)

Substitute every occurrence of from in the expression with to.

Returns:

an Expr

Throws:

Z3Exception - on error

See Also:

• substitute(Expr[],Expr[])

substituteVars

public Expr<R> substituteVars(Expr<?>[] to)

Substitute the free variables in the expression with the expressions in to Remarks: For every i smaller than * num_exprs, the variable with de-Bruijn index i * is replaced with term to[i].

Returns:

an Expr

Throws:

Z3Exception - on error

Z3Exception - on error

translate

public Expr<R> translate(Context ctx)

Translates (copies) the term to the Context ctx.

Overrides:

translate in class AST

Parameters:

ctx - A context

Returns:

A copy of the term which is associated with ctx

Throws:

Z3Exception - on error

toString

public String toString()

Returns a string representation of the expression.

Overrides:

toString in class AST

isNumeral

public boolean isNumeral()

Indicates whether the term is a numeral

Returns:

a boolean

Throws:

Z3Exception - on error

isWellSorted

public boolean isWellSorted()

Indicates whether the term is well-sorted.

Returns:

True if the term is well-sorted, false otherwise.

Throws:

Z3Exception - on error

getSort

public R getSort()

The Sort of the term.

Returns:

a sort

Throws:

Z3Exception - on error

isConst

public boolean isConst()

Indicates whether the term represents a constant.

Returns:

a boolean

Throws:

Z3Exception - on error

isIntNum

public boolean isIntNum()

Indicates whether the term is an integer numeral.

Returns:

a boolean

Throws:

Z3Exception - on error

isRatNum

public boolean isRatNum()

Indicates whether the term is a real numeral.

Returns:

a boolean

Throws:

Z3Exception - on error

isAlgebraicNumber

public boolean isAlgebraicNumber()

Indicates whether the term is an algebraic number

Returns:

a boolean

Throws:

Z3Exception - on error

isBool

public boolean isBool()

Indicates whether the term has Boolean sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isTrue

public boolean isTrue()

Indicates whether the term is the constant true.

Returns:

a boolean

Throws:

Z3Exception - on error

isFalse

public boolean isFalse()

Indicates whether the term is the constant false.

Returns:

a boolean

Throws:

Z3Exception - on error

isEq

public boolean isEq()

Indicates whether the term is an equality predicate.

Returns:

a boolean

Throws:

Z3Exception - on error

isDistinct

public boolean isDistinct()

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).

Returns:

a boolean

Throws:

Z3Exception - on error

isITE

public boolean isITE()

Indicates whether the term is a ternary if-then-else term

Returns:

a boolean

Throws:

Z3Exception - on error

isAnd

public boolean isAnd()

Indicates whether the term is an n-ary conjunction

Returns:

a boolean

Throws:

Z3Exception - on error

isOr

public boolean isOr()

Indicates whether the term is an n-ary disjunction

Returns:

a boolean

Throws:

Z3Exception - on error

isIff

public boolean isIff()

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isXor

public boolean isXor()

Indicates whether the term is an exclusive or

Returns:

a boolean

Throws:

Z3Exception - on error

isNot

public boolean isNot()

Indicates whether the term is a negation

Returns:

a boolean

Throws:

Z3Exception - on error

isImplies

public boolean isImplies()

Indicates whether the term is an implication

Returns:

a boolean

Throws:

Z3Exception - on error

isInt

public boolean isInt()

Indicates whether the term is of integer sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isReal

public boolean isReal()

Indicates whether the term is of sort real.

Returns:

a boolean

Throws:

Z3Exception - on error

isArithmeticNumeral

public boolean isArithmeticNumeral()

Indicates whether the term is an arithmetic numeral.

Returns:

a boolean

Throws:

Z3Exception - on error

isLE

public boolean isLE()

Indicates whether the term is a less-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isGE

public boolean isGE()

Indicates whether the term is a greater-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isLT

public boolean isLT()

Indicates whether the term is a less-than

Returns:

a boolean

Throws:

Z3Exception - on error

isGT

public boolean isGT()

Indicates whether the term is a greater-than

Returns:

a boolean

Throws:

Z3Exception - on error

isAdd

public boolean isAdd()

Indicates whether the term is addition (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isSub

public boolean isSub()

Indicates whether the term is subtraction (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isUMinus

public boolean isUMinus()

Indicates whether the term is a unary minus

Returns:

a boolean

Throws:

Z3Exception - on error

isMul

public boolean isMul()

Indicates whether the term is multiplication (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isDiv

public boolean isDiv()

Indicates whether the term is division (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isIDiv

public boolean isIDiv()

Indicates whether the term is integer division (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isRemainder

public boolean isRemainder()

Indicates whether the term is remainder (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isModulus

public boolean isModulus()

Indicates whether the term is modulus (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isIntToReal

public boolean isIntToReal()

Indicates whether the term is a coercion of integer to real (unary)

Returns:

a boolean

Throws:

Z3Exception - on error

isRealToInt

public boolean isRealToInt()

Indicates whether the term is a coercion of real to integer (unary)

Returns:

a boolean

Throws:

Z3Exception - on error

isRealIsInt

public boolean isRealIsInt()

Indicates whether the term is a check that tests whether a real is integral (unary)

Returns:

a boolean

Throws:

Z3Exception - on error

isArray

public boolean isArray()

Indicates whether the term is of an array sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isStore

public boolean isStore()

Indicates whether the term is an array store. Remarks: It satisfies * select(store(a,i,v),j) = if i = j then v else select(a,j). Array store * takes at least 3 arguments.

Returns:

a boolean

Throws:

Z3Exception - on error

isSelect

public boolean isSelect()

Indicates whether the term is an array select.

Returns:

a boolean

Throws:

Z3Exception - on error

isConstantArray

public boolean isConstantArray()

Indicates whether the term is a constant array. Remarks: For example, * select(const(v),i) = v holds for every v and i. The function is * unary.

Returns:

a boolean

Throws:

Z3Exception - on error

isDefaultArray

public boolean isDefaultArray()

Indicates whether the term is a default array. Remarks: For example default(const(v)) = v. The function is unary.

Returns:

a boolean

Throws:

Z3Exception - on error

isArrayMap

public boolean isArrayMap()

Indicates whether the term is an array map. Remarks: It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.

Returns:

a boolean

Throws:

Z3Exception - on error

isAsArray

public boolean isAsArray()

Indicates whether the term is an as-array term. Remarks: An as-array term * is n array value that behaves as the function graph of the function * passed as parameter.

Returns:

a boolean

Throws:

Z3Exception - on error

isSetUnion

public boolean isSetUnion()

Indicates whether the term is set union

Returns:

a boolean

Throws:

Z3Exception - on error

isSetIntersect

public boolean isSetIntersect()

Indicates whether the term is set intersection

Returns:

a boolean

Throws:

Z3Exception - on error

isSetDifference

public boolean isSetDifference()

Indicates whether the term is set difference

Returns:

a boolean

Throws:

Z3Exception - on error

isSetComplement

public boolean isSetComplement()

Indicates whether the term is set complement

Returns:

a boolean

Throws:

Z3Exception - on error

isSetSubset

public boolean isSetSubset()

Indicates whether the term is set subset

Returns:

a boolean

Throws:

Z3Exception - on error

isBV

public boolean isBV()

Indicates whether the terms is of bit-vector sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isBVNumeral

public boolean isBVNumeral()

Indicates whether the term is a bit-vector numeral

Returns:

a boolean

Throws:

Z3Exception - on error

isBVBitOne

public boolean isBVBitOne()

Indicates whether the term is a one-bit bit-vector with value one

Returns:

a boolean

Throws:

Z3Exception - on error

isBVBitZero

public boolean isBVBitZero()

Indicates whether the term is a one-bit bit-vector with value zero

Returns:

a boolean

Throws:

Z3Exception - on error

isBVUMinus

public boolean isBVUMinus()

Indicates whether the term is a bit-vector unary minus

Returns:

a boolean

Throws:

Z3Exception - on error

isBVAdd

public boolean isBVAdd()

Indicates whether the term is a bit-vector addition (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSub

public boolean isBVSub()

Indicates whether the term is a bit-vector subtraction (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVMul

public boolean isBVMul()

Indicates whether the term is a bit-vector multiplication (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSDiv

public boolean isBVSDiv()

Indicates whether the term is a bit-vector signed division (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVUDiv

public boolean isBVUDiv()

Indicates whether the term is a bit-vector unsigned division (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSRem

public boolean isBVSRem()

Indicates whether the term is a bit-vector signed remainder (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVURem

public boolean isBVURem()

Indicates whether the term is a bit-vector unsigned remainder (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSMod

public boolean isBVSMod()

Indicates whether the term is a bit-vector signed modulus

Returns:

a boolean

Throws:

Z3Exception - on error

isBVULE

public boolean isBVULE()

Indicates whether the term is an unsigned bit-vector less-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSLE

public boolean isBVSLE()

Indicates whether the term is a signed bit-vector less-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isBVUGE

public boolean isBVUGE()

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSGE

public boolean isBVSGE()

Indicates whether the term is a signed bit-vector greater-than-or-equal

Returns:

a boolean

Throws:

Z3Exception - on error

isBVULT

public boolean isBVULT()

Indicates whether the term is an unsigned bit-vector less-than

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSLT

public boolean isBVSLT()

Indicates whether the term is a signed bit-vector less-than

Returns:

a boolean

Throws:

Z3Exception - on error

isBVUGT

public boolean isBVUGT()

Indicates whether the term is an unsigned bit-vector greater-than

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSGT

public boolean isBVSGT()

Indicates whether the term is a signed bit-vector greater-than

Returns:

a boolean

Throws:

Z3Exception - on error

isBVAND

public boolean isBVAND()

Indicates whether the term is a bit-wise AND

Returns:

a boolean

Throws:

Z3Exception - on error

isBVOR

public boolean isBVOR()

Indicates whether the term is a bit-wise OR

Returns:

a boolean

Throws:

Z3Exception - on error

isBVNOT

public boolean isBVNOT()

Indicates whether the term is a bit-wise NOT

Returns:

a boolean

Throws:

Z3Exception - on error

isBVXOR

public boolean isBVXOR()

Indicates whether the term is a bit-wise XOR

Returns:

a boolean

Throws:

Z3Exception - on error

isBVNAND

public boolean isBVNAND()

Indicates whether the term is a bit-wise NAND

Returns:

a boolean

Throws:

Z3Exception - on error

isBVNOR

public boolean isBVNOR()

Indicates whether the term is a bit-wise NOR

Returns:

a boolean

Throws:

Z3Exception - on error

isBVXNOR

public boolean isBVXNOR()

Indicates whether the term is a bit-wise XNOR

Returns:

a boolean

Throws:

Z3Exception - on error

isBVConcat

public boolean isBVConcat()

Indicates whether the term is a bit-vector concatenation (binary)

Returns:

a boolean

Throws:

Z3Exception - on error

isBVSignExtension

public boolean isBVSignExtension()

Indicates whether the term is a bit-vector sign extension

Returns:

a boolean

Throws:

Z3Exception - on error

isBVZeroExtension

public boolean isBVZeroExtension()

Indicates whether the term is a bit-vector zero extension

Returns:

a boolean

Throws:

Z3Exception - on error

isBVExtract

public boolean isBVExtract()

Indicates whether the term is a bit-vector extraction

Returns:

a boolean

Throws:

Z3Exception - on error

isBVRepeat

public boolean isBVRepeat()

Indicates whether the term is a bit-vector repetition

Returns:

a boolean

Throws:

Z3Exception - on error

isBVReduceOR

public boolean isBVReduceOR()

Indicates whether the term is a bit-vector reduce OR

Returns:

a boolean

Throws:

Z3Exception - on error

isBVReduceAND

public boolean isBVReduceAND()

Indicates whether the term is a bit-vector reduce AND

Returns:

a boolean

Throws:

Z3Exception - on error

isBVComp

public boolean isBVComp()

Indicates whether the term is a bit-vector comparison

Returns:

a boolean

Throws:

Z3Exception - on error

isBVShiftLeft

public boolean isBVShiftLeft()

Indicates whether the term is a bit-vector shift left

Returns:

a boolean

Throws:

Z3Exception - on error

isBVShiftRightLogical

public boolean isBVShiftRightLogical()

Indicates whether the term is a bit-vector logical shift right

Returns:

a boolean

Throws:

Z3Exception - on error

isBVShiftRightArithmetic

public boolean isBVShiftRightArithmetic()

Indicates whether the term is a bit-vector arithmetic shift left

Returns:

a boolean

Throws:

Z3Exception - on error

isBVRotateLeft

public boolean isBVRotateLeft()

Indicates whether the term is a bit-vector rotate left

Returns:

a boolean

Throws:

Z3Exception - on error

isBVRotateRight

public boolean isBVRotateRight()

Indicates whether the term is a bit-vector rotate right

Returns:

a boolean

Throws:

Z3Exception - on error

isBVRotateLeftExtended

public boolean isBVRotateLeftExtended()

Indicates whether the term is a bit-vector rotate left (extended) Remarks: Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Returns:

a boolean

Throws:

Z3Exception - on error

isBVRotateRightExtended

public boolean isBVRotateRightExtended()

Indicates whether the term is a bit-vector rotate right (extended) Remarks: Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Returns:

a boolean

Throws:

Z3Exception - on error

isIntToBV

public boolean isIntToBV()

Indicates whether the term is a coercion from integer to bit-vector Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Returns:

a boolean

Throws:

Z3Exception - on error

isBVToInt

public boolean isBVToInt()

Indicates whether the term is a coercion from bit-vector to integer Remarks: This function is not supported by the decision procedures. Only * the most rudimentary simplification rules are applied to this * function.

Returns:

a boolean

Throws:

Z3Exception - on error

isBVCarry

public boolean isBVCarry()

Indicates whether the term is a bit-vector carry Remarks: 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)))

Returns:

a boolean

Throws:

Z3Exception - on error

isBVXOR3

public boolean isBVXOR3()

Indicates whether the term is a bit-vector ternary XOR Remarks: The * meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor * l1 l2) l3)

Returns:

a boolean

Throws:

Z3Exception - on error

isLabel

public boolean isLabel()

Indicates whether the term is a label (used by the Boogie Verification condition generator). Remarks: The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.

Returns:

a boolean

Throws:

Z3Exception - on error

isLabelLit

public boolean isLabelLit()

Indicates whether the term is a label literal (used by the Boogie Verification condition generator). Remarks: A label literal has a set of string parameters. It takes no arguments.

Returns:

a boolean

Throws:

Z3Exception - on error

isString

public boolean isString()

Check whether expression is a string constant.

Returns:

a boolean

getString

public String getString()

Retrieve string corresponding to string constant. Remark: the expression should be a string constant, (isString() should return true).

Returns:

a string

Throws:

Z3Exception - on error

isConcat

public boolean isConcat()

Check whether expression is a concatenation

Returns:

a boolean

isOEQ

public boolean isOEQ()

Indicates whether the term is a binary equivalence modulo namings. Remarks: This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofTrue

public boolean isProofTrue()

Indicates whether the term is a Proof for the expression 'true'.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofAsserted

public boolean isProofAsserted()

Indicates whether the term is a proof for a fact asserted by the user.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofGoal

public boolean isProofGoal()

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofModusPonens

public boolean isProofModusPonens()

Indicates whether the term is proof via modus ponens Remarks: Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).

Returns:

a boolean

Throws:

Z3Exception - on error

isProofReflexivity

public boolean isProofReflexivity()

Indicates whether the term is a proof for (R t t), where R is a reflexive relation. Remarks: 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'.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofSymmetry

public boolean isProofSymmetry()

Indicates whether the term is proof by symmetricity of a relation Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofTransitivity

public boolean isProofTransitivity()

Indicates whether the term is a proof by transitivity of a relation Remarks: 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)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofTransitivityStar

public boolean isProofTransitivityStar()

Indicates whether the term is a proof by condensed transitivity of a relation Remarks: Condensed transitivity proof. 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofMonotonicity

public boolean isProofMonotonicity()

Indicates whether the term is a monotonicity proof object. Remarks: 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 suppressed to save space.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofQuantIntro

public boolean isProofQuantIntro()

Indicates whether the term is a quant-intro proof Remarks: Given a proof * for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: * (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))

Returns:

a boolean

Throws:

Z3Exception - on error

isProofDistributivity

public boolean isProofDistributivity()

Indicates whether the term is a distributivity proof object. Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofAndElimination

public boolean isProofAndElimination()

Indicates whether the term is a proof by elimination of AND Remarks: * Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and * l_1 ... l_n) [and-elim T1]: l_i

Returns:

a boolean

Throws:

Z3Exception - on error

isProofOrElimination

public boolean isProofOrElimination()

Indicates whether the term is a proof by elimination of not-or Remarks: * 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)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofRewrite

public boolean isProofRewrite()

Indicates whether the term is a proof by rewriting Remarks: 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)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofRewriteStar

public boolean isProofRewriteStar()

Indicates whether the term is a proof by rewriting Remarks: A proof for rewriting an expression t into an expression s. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is used in a few cases . The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofPullQuant

public boolean isProofPullQuant()

Indicates whether the term is a proof for pulling quantifiers out. Remarks: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofPushQuant

public boolean isProofPushQuant()

Indicates whether the term is a proof for pushing quantifiers in. Remarks: 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

Returns:

a boolean

Throws:

Z3Exception - on error

isProofElimUnusedVars

public boolean isProofElimUnusedVars()

Indicates whether the term is a proof for elimination of unused variables. Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofDER

public boolean isProofDER()

Indicates whether the term is a proof for destructive equality resolution Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofQuantInst

public boolean isProofQuantInst()

Indicates whether the term is a proof for quantifier instantiation Remarks: A proof of (or (not (forall (x) (P x))) (P a))

Returns:

a boolean

Throws:

Z3Exception - on error

isProofHypothesis

public boolean isProofHypothesis()

Indicates whether the term is a hypothesis marker. Remarks: Mark a hypothesis in a natural deduction style proof.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofLemma

public boolean isProofLemma()

Indicates whether the term is a proof by lemma Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofUnitResolution

public boolean isProofUnitResolution()

Indicates whether the term is a proof by unit resolution Remarks: T1: * (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... R(n+1): (not l_n) * [unit-resolution T1 ... R(n+1)]: (or l_1' ... l_m')

Returns:

a boolean

Throws:

Z3Exception - on error

isProofIFFTrue

public boolean isProofIFFTrue()

Indicates whether the term is a proof by iff-true Remarks: T1: p [iff-true T1]: (iff p true)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofIFFFalse

public boolean isProofIFFFalse()

Indicates whether the term is a proof by iff-false Remarks: T1: (not p) [iff-false T1]: (iff p false)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofCommutativity

public boolean isProofCommutativity()

Indicates whether the term is a proof by commutativity Remarks: [comm]: (= (f a b) (f b a)) f is a commutative operator. This proof object has no antecedents. Remark: if f is bool, then = is iff.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofDefAxiom

public boolean isProofDefAxiom()

Indicates whether the term is a proof for Tseitin-like axioms Remarks: 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).

Returns:

a boolean

Throws:

Z3Exception - on error

isProofDefIntro

public boolean isProofDefIntro()

Indicates whether the term is a proof for introduction of a name Remarks: 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)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofApplyDef

public boolean isProofApplyDef()

Indicates whether the term is a proof for application of a definition Remarks: [apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofIFFOEQ

public boolean isProofIFFOEQ()

Indicates whether the term is a proof iff-oeq Remarks: T1: (iff p q) [iff~ T1]: (~ p q)

Returns:

a boolean

Throws:

Z3Exception - on error

isProofNNFPos

public boolean isProofNNFPos()

Indicates whether the term is a proof for a positive NNF step Remarks: 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 R) q) (forall (x R) 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'.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofNNFNeg

public boolean isProofNNFNeg()

Indicates whether the term is a proof for a negative NNF step Remarks: 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')))

Returns:

a boolean

Throws:

Z3Exception - on error

isProofSkolemize

public boolean isProofSkolemize()

Indicates whether the term is a proof for a Skolemization step Remarks: Proof for: [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) [sk]: (~ (exists x (p x y)) (p (sk y) y)) This proof object has no antecedents.

Returns:

a boolean

Throws:

Z3Exception - on error

isProofModusPonensOEQ

public boolean isProofModusPonensOEQ()

Indicates whether the term is a proof by modus ponens for equi-satisfiability. Remarks: Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q

Returns:

a boolean

Throws:

Z3Exception - on error

isProofTheoryLemma

public boolean isProofTheoryLemma()

Indicates whether the term is a proof for theory lemma Remarks: Generic proof for theory lemmas. The theory lemma function comes with one or more parameters. The first parameter indicates the name of the theory. For the theory of arithmetic, additional parameters provide hints for checking the theory lemma. The hints for arithmetic are: - farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. - triangle-eq - Indicates a lemma related to the equivalence: (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelation

public boolean isRelation()

Indicates whether the term is of an array sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationStore

public boolean isRelationStore()

Indicates whether the term is an relation store Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isEmptyRelation

public boolean isEmptyRelation()

Indicates whether the term is an empty relation

Returns:

a boolean

Throws:

Z3Exception - on error

isIsEmptyRelation

public boolean isIsEmptyRelation()

Indicates whether the term is a test for the emptiness of a relation

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationalJoin

public boolean isRelationalJoin()

Indicates whether the term is a relational join

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationUnion

public boolean isRelationUnion()

Indicates whether the term is the union or convex hull of two relations. Remarks: The function takes two arguments.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationWiden

public boolean isRelationWiden()

Indicates whether the term is the widening of two relations Remarks: The function takes two arguments.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationProject

public boolean isRelationProject()

Indicates whether the term is a projection of columns (provided as numbers in the parameters). Remarks: The function takes one argument.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationFilter

public boolean isRelationFilter()

Indicates whether the term is a relation filter Remarks: Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationNegationFilter

public boolean isRelationNegationFilter()

Indicates whether the term is an intersection of a relation with the negation of another. Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationRename

public boolean isRelationRename()

Indicates whether the term is the renaming of a column in a relation Remarks: The function takes one argument. The parameters contain the renaming as a cycle.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationComplement

public boolean isRelationComplement()

Indicates whether the term is the complement of a relation

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationSelect

public boolean isRelationSelect()

Indicates whether the term is a relational select Remarks: 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.

Returns:

a boolean

Throws:

Z3Exception - on error

isRelationClone

public boolean isRelationClone()

Indicates whether the term is a relational clone (copy) Remarks: 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 isRelationUnion to perform destructive updates to the first argument.

Returns:

a boolean

Throws:

Z3Exception - on error

See Also:

• isRelationUnion()

isFiniteDomain

public boolean isFiniteDomain()

Indicates whether the term is of an array sort.

Returns:

a boolean

Throws:

Z3Exception - on error

isFiniteDomainLT

public boolean isFiniteDomainLT()

Indicates whether the term is a less than predicate over a finite domain.

Returns:

a boolean

Throws:

Z3Exception - on error

getIndex

public int getIndex()

The de-Bruijn index of a bound variable. Remarks: 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.

Returns:

an int

Throws:

Z3Exception - on error

distillSort

public <S extends R> Expr<S> distillSort(Class<S> newSort)

Downcast sort of this expression. Expr<ArithSort> mixedExpr = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2)); Expr<RealSort> realExpr = mixedExpr.distillSort(RealSort.class)

Throws:

Z3Exception - if sort is not compatible with expr.