Z3
Public Member Functions | Protected Member Functions
Expr Class Reference
+ Inheritance diagram for Expr:

Public Member Functions

Expr simplify () throws Z3Exception
 
Expr simplify (Params p) throws Z3Exception
 
FuncDecl getFuncDecl () throws Z3Exception
 
Z3_lbool getBoolValue () throws Z3Exception
 
int getNumArgs () throws Z3Exception
 
Expr[] getArgs () throws Z3Exception
 
void update (Expr[] args) throws Z3Exception
 
Expr substitute (Expr[] from, Expr[] to) throws Z3Exception
 
Expr substitute (Expr from, Expr to) throws Z3Exception
 
Expr substituteVars (Expr[] to) throws Z3Exception
 
Expr translate (Context ctx) throws Z3Exception
 
String toString ()
 
boolean isNumeral () throws Z3Exception
 
boolean isWellSorted () throws Z3Exception
 
Sort getSort () throws Z3Exception
 
boolean isConst () throws Z3Exception
 
boolean isIntNum () throws Z3Exception
 
boolean isRatNum () throws Z3Exception
 
boolean isAlgebraicNumber () throws Z3Exception
 
boolean isBool () throws Z3Exception
 
boolean isTrue () throws Z3Exception
 
boolean isFalse () throws Z3Exception
 
boolean isEq () throws Z3Exception
 
boolean isDistinct () throws Z3Exception
 
boolean isITE () throws Z3Exception
 
boolean isAnd () throws Z3Exception
 
boolean isOr () throws Z3Exception
 
boolean isIff () throws Z3Exception
 
boolean isXor () throws Z3Exception
 
boolean isNot () throws Z3Exception
 
boolean isImplies () throws Z3Exception
 
boolean isInt () throws Z3Exception
 
boolean isReal () throws Z3Exception
 
boolean isArithmeticNumeral () throws Z3Exception
 
boolean isLE () throws Z3Exception
 
boolean isGE () throws Z3Exception
 
boolean isLT () throws Z3Exception
 
boolean isGT () throws Z3Exception
 
boolean isAdd () throws Z3Exception
 
boolean isSub () throws Z3Exception
 
boolean isUMinus () throws Z3Exception
 
boolean isMul () throws Z3Exception
 
boolean isDiv () throws Z3Exception
 
boolean isIDiv () throws Z3Exception
 
boolean isRemainder () throws Z3Exception
 
boolean isModulus () throws Z3Exception
 
boolean isIntToReal () throws Z3Exception
 
boolean isRealToInt () throws Z3Exception
 
boolean isRealIsInt () throws Z3Exception
 
boolean isArray () throws Z3Exception
 
boolean isStore () throws Z3Exception
 
boolean isSelect () throws Z3Exception
 
boolean isConstantArray () throws Z3Exception
 
boolean isDefaultArray () throws Z3Exception
 
boolean isArrayMap () throws Z3Exception
 
boolean isAsArray () throws Z3Exception
 
boolean isSetUnion () throws Z3Exception
 
boolean isSetIntersect () throws Z3Exception
 
boolean isSetDifference () throws Z3Exception
 
boolean isSetComplement () throws Z3Exception
 
boolean isSetSubset () throws Z3Exception
 
boolean isBV () throws Z3Exception
 
boolean isBVNumeral () throws Z3Exception
 
boolean isBVBitOne () throws Z3Exception
 
boolean isBVBitZero () throws Z3Exception
 
boolean isBVUMinus () throws Z3Exception
 
boolean isBVAdd () throws Z3Exception
 
boolean isBVSub () throws Z3Exception
 
boolean isBVMul () throws Z3Exception
 
boolean isBVSDiv () throws Z3Exception
 
boolean isBVUDiv () throws Z3Exception
 
boolean isBVSRem () throws Z3Exception
 
boolean isBVURem () throws Z3Exception
 
boolean isBVSMod () throws Z3Exception
 
boolean isBVULE () throws Z3Exception
 
boolean isBVSLE () throws Z3Exception
 
boolean isBVUGE () throws Z3Exception
 
boolean isBVSGE () throws Z3Exception
 
boolean isBVULT () throws Z3Exception
 
boolean isBVSLT () throws Z3Exception
 
boolean isBVUGT () throws Z3Exception
 
boolean isBVSGT () throws Z3Exception
 
boolean isBVAND () throws Z3Exception
 
boolean isBVOR () throws Z3Exception
 
boolean isBVNOT () throws Z3Exception
 
boolean isBVXOR () throws Z3Exception
 
boolean isBVNAND () throws Z3Exception
 
boolean isBVNOR () throws Z3Exception
 
boolean isBVXNOR () throws Z3Exception
 
boolean isBVConcat () throws Z3Exception
 
boolean isBVSignExtension () throws Z3Exception
 
boolean isBVZeroExtension () throws Z3Exception
 
boolean isBVExtract () throws Z3Exception
 
boolean isBVRepeat () throws Z3Exception
 
boolean isBVReduceOR () throws Z3Exception
 
boolean isBVReduceAND () throws Z3Exception
 
boolean isBVComp () throws Z3Exception
 
boolean isBVShiftLeft () throws Z3Exception
 
boolean isBVShiftRightLogical () throws Z3Exception
 
boolean isBVShiftRightArithmetic () throws Z3Exception
 
boolean isBVRotateLeft () throws Z3Exception
 
boolean isBVRotateRight () throws Z3Exception
 
boolean isBVRotateLeftExtended () throws Z3Exception
 
boolean isBVRotateRightExtended () throws Z3Exception
 
boolean isIntToBV () throws Z3Exception
 
boolean isBVToInt () throws Z3Exception
 
boolean isBVCarry () throws Z3Exception
 
boolean isBVXOR3 () throws Z3Exception
 
boolean isLabel () throws Z3Exception
 
boolean isLabelLit () throws Z3Exception
 
boolean isOEQ () throws Z3Exception
 
boolean isProofTrue () throws Z3Exception
 
boolean isProofAsserted () throws Z3Exception
 
boolean isProofGoal () throws Z3Exception
 
boolean isProofModusPonens () throws Z3Exception
 
boolean isProofReflexivity () throws Z3Exception
 
boolean isProofSymmetry () throws Z3Exception
 
boolean isProofTransitivity () throws Z3Exception
 
boolean isProofTransitivityStar () throws Z3Exception
 
boolean isProofMonotonicity () throws Z3Exception
 
boolean isProofQuantIntro () throws Z3Exception
 
boolean isProofDistributivity () throws Z3Exception
 
boolean isProofAndElimination () throws Z3Exception
 
boolean isProofOrElimination () throws Z3Exception
 
boolean isProofRewrite () throws Z3Exception
 
boolean isProofRewriteStar () throws Z3Exception
 
boolean isProofPullQuant () throws Z3Exception
 
boolean isProofPullQuantStar () throws Z3Exception
 
boolean isProofPushQuant () throws Z3Exception
 
boolean isProofElimUnusedVars () throws Z3Exception
 
boolean isProofDER () throws Z3Exception
 
boolean isProofQuantInst () throws Z3Exception
 
boolean isProofHypothesis () throws Z3Exception
 
boolean isProofLemma () throws Z3Exception
 
boolean isProofUnitResolution () throws Z3Exception
 
boolean isProofIFFTrue () throws Z3Exception
 
boolean isProofIFFFalse () throws Z3Exception
 
boolean isProofCommutativity () throws Z3Exception
 
boolean isProofDefAxiom () throws Z3Exception
 
boolean isProofDefIntro () throws Z3Exception
 
boolean isProofApplyDef () throws Z3Exception
 
boolean isProofIFFOEQ () throws Z3Exception
 
boolean isProofNNFPos () throws Z3Exception
 
boolean isProofNNFNeg () throws Z3Exception
 
boolean isProofNNFStar () throws Z3Exception
 
boolean isProofCNFStar () throws Z3Exception
 
boolean isProofSkolemize () throws Z3Exception
 
boolean isProofModusPonensOEQ () throws Z3Exception
 
boolean isProofTheoryLemma () throws Z3Exception
 
boolean isRelation () throws Z3Exception
 
boolean isRelationStore () throws Z3Exception
 
boolean isEmptyRelation () throws Z3Exception
 
boolean isIsEmptyRelation () throws Z3Exception
 
boolean isRelationalJoin () throws Z3Exception
 
boolean isRelationUnion () throws Z3Exception
 
boolean isRelationWiden () throws Z3Exception
 
boolean isRelationProject () throws Z3Exception
 
boolean isRelationFilter () throws Z3Exception
 
boolean isRelationNegationFilter () throws Z3Exception
 
boolean isRelationRename () throws Z3Exception
 
boolean isRelationComplement () throws Z3Exception
 
boolean isRelationSelect () throws Z3Exception
 
boolean isRelationClone () throws Z3Exception
 
boolean isFiniteDomain () throws Z3Exception
 
boolean isFiniteDomainLT () throws Z3Exception
 
int getIndex () throws Z3Exception
 
- Public Member Functions inherited from AST
boolean equals (Object o)
 
int compareTo (Object other) throws Z3Exception
 
int hashCode ()
 
int getId () throws Z3Exception
 
AST translate (Context ctx) throws Z3Exception
 
Z3_ast_kind getASTKind () throws Z3Exception
 
boolean isExpr () throws Z3Exception
 
boolean isApp () throws Z3Exception
 
boolean isVar () throws Z3Exception
 
boolean isQuantifier () throws Z3Exception
 
boolean isSort () throws Z3Exception
 
boolean isFuncDecl () throws Z3Exception
 
String toString ()
 
String getSExpr () throws Z3Exception
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Protected Member Functions

 Expr (Context ctx)
 
 Expr (Context ctx, long obj) throws Z3Exception
 
- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

Expressions are terms.

Definition at line 30 of file Expr.java.

Constructor & Destructor Documentation

Expr ( Context  ctx)
inlineprotected

Constructor for Expr

Definition at line 1738 of file Expr.java.

1739  {
1740  super(ctx);
1741  {
1742  }
1743  }
Expr ( Context  ctx,
long  obj 
) throws Z3Exception
inlineprotected

Constructor for Expr

Definition at line 1748 of file Expr.java.

1749  {
1750  super(ctx, obj);
1751  {
1752  }
1753  }

Member Function Documentation

Expr [] getArgs ( ) throws Z3Exception
inline

The arguments of the expression.

Definition at line 90 of file Expr.java.

Referenced by FuncInterp.toString().

91  {
92  int n = getNumArgs();
93  Expr[] res = new Expr[n];
94  for (int i = 0; i < n; i++)
95  res[i] = Expr.create(getContext(),
96  Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
97  return res;
98  }
Expr(Context ctx)
Definition: Expr.java:1738
Z3_lbool getBoolValue ( ) throws Z3Exception
inline

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

Definition at line 73 of file Expr.java.

74  {
75  return Z3_lbool.fromInt(Native.getBoolValue(getContext().nCtx(),
76  getNativeObject()));
77  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
FuncDecl getFuncDecl ( ) throws Z3Exception
inline

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

Definition at line 63 of file Expr.java.

Referenced by Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.isBVSRem(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConst(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCNFStar(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), and Expr.isXor().

64  {
65  return new FuncDecl(getContext(), Native.getAppDecl(getContext().nCtx(),
66  getNativeObject()));
67  }
int getIndex ( ) throws Z3Exception
inline

The de-Burijn index of a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

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.

Definition at line 1727 of file Expr.java.

1728  {
1729  if (!isVar())
1730  throw new Z3Exception("Term is not a bound variable.");
1731 
1732  return Native.getIndexValue(getContext().nCtx(), getNativeObject());
1733  }
boolean isVar()
Definition: AST.java:152
int getNumArgs ( ) throws Z3Exception
inline

The number of arguments of the expression.

Definition at line 82 of file Expr.java.

Referenced by Expr.getArgs(), Expr.isConst(), and Expr.update().

83  {
84  return Native.getAppNumArgs(getContext().nCtx(), getNativeObject());
85  }
Sort getSort ( ) throws Z3Exception
inline

The Sort of the term.

Definition at line 206 of file Expr.java.

Referenced by BitVecExpr.getSortSize().

207  {
208  return Sort.create(getContext(),
209  Native.getSort(getContext().nCtx(), getNativeObject()));
210  }
boolean isAdd ( ) throws Z3Exception
inline

Indicates whether the term is addition (binary)

Definition at line 408 of file Expr.java.

409  {
411  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isAlgebraicNumber ( ) throws Z3Exception
inline

Indicates whether the term is an algebraic number

Definition at line 239 of file Expr.java.

240  {
241  return Native.isAlgebraicNumber(getContext().nCtx(), getNativeObject());
242  }
boolean isAnd ( ) throws Z3Exception
inline

Indicates whether the term is an n-ary conjunction

Definition at line 298 of file Expr.java.

299  {
301  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isArithmeticNumeral ( ) throws Z3Exception
inline

Indicates whether the term is an arithmetic numeral.

Definition at line 368 of file Expr.java.

369  {
371  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isArray ( ) throws Z3Exception
inline

Indicates whether the term is of an array sort.

Definition at line 497 of file Expr.java.

498  {
499  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Z3_sort_kind
500  .fromInt(Native.getSortKind(getContext().nCtx(),
501  Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ARRAY_SORT);
502  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isArrayMap ( ) throws Z3Exception
inline

Indicates whether the term is an array map.

It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.

Definition at line 545 of file Expr.java.

546  {
548  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isAsArray ( ) throws Z3Exception
inline

Indicates whether the term is an as-array term.

An as-array term is n array value that behaves as the function graph of the function passed as parameter.

Definition at line 555 of file Expr.java.

556  {
558  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBool ( ) throws Z3Exception
inline

Indicates whether the term has Boolean sort.

Definition at line 247 of file Expr.java.

248  {
249  return (isExpr() && Native.isEqSort(getContext().nCtx(),
250  Native.mkBoolSort(getContext().nCtx()),
251  Native.getSort(getContext().nCtx(), getNativeObject())));
252  }
boolean isExpr()
Definition: AST.java:127
boolean isBV ( ) throws Z3Exception
inline

Indicates whether the terms is of bit-vector sort.

Definition at line 603 of file Expr.java.

604  {
605  return Native.getSortKind(getContext().nCtx(),
606  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_BV_SORT
607  .toInt();
608  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isBVAdd ( ) throws Z3Exception
inline

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

Definition at line 645 of file Expr.java.

646  {
648  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVAND ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise AND

Definition at line 814 of file Expr.java.

815  {
817  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVBitOne ( ) throws Z3Exception
inline

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

Definition at line 621 of file Expr.java.

622  {
624  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVBitZero ( ) throws Z3Exception
inline

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

Definition at line 629 of file Expr.java.

630  {
632  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVCarry ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector carry

Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

Definition at line 1018 of file Expr.java.

1019  {
1021  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVComp ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector comparison

Definition at line 926 of file Expr.java.

927  {
929  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVConcat ( ) throws Z3Exception
inline

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

Definition at line 870 of file Expr.java.

871  {
873  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVExtract ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector extraction

Definition at line 894 of file Expr.java.

895  {
897  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVMul ( ) throws Z3Exception
inline

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

Definition at line 661 of file Expr.java.

662  {
664  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVNAND ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise NAND

Definition at line 846 of file Expr.java.

847  {
849  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVNOR ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise NOR

Definition at line 854 of file Expr.java.

855  {
857  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVNOT ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise NOT

Definition at line 830 of file Expr.java.

831  {
833  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVNumeral ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector numeral

Definition at line 613 of file Expr.java.

614  {
616  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVOR ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise OR

Definition at line 822 of file Expr.java.

823  {
825  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVReduceAND ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector reduce AND

Definition at line 918 of file Expr.java.

919  {
921  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVReduceOR ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector reduce OR

Definition at line 910 of file Expr.java.

911  {
913  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVRepeat ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector repetition

Definition at line 902 of file Expr.java.

903  {
905  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVRotateLeft ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector rotate left

Definition at line 958 of file Expr.java.

959  {
961  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVRotateLeftExtended ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector rotate left (extended)

Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Definition at line 976 of file Expr.java.

977  {
979  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVRotateRight ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector rotate right

Definition at line 966 of file Expr.java.

967  {
969  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVRotateRightExtended ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector rotate right (extended)

Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Definition at line 986 of file Expr.java.

987  {
989  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSDiv ( ) throws Z3Exception
inline

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

Definition at line 669 of file Expr.java.

670  {
672  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSGE ( ) throws Z3Exception
inline

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

Definition at line 774 of file Expr.java.

775  {
777  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSGT ( ) throws Z3Exception
inline

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

Definition at line 806 of file Expr.java.

807  {
809  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVShiftLeft ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector shift left

Definition at line 934 of file Expr.java.

935  {
937  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVShiftRightArithmetic ( ) throws Z3Exception
inline

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

Definition at line 950 of file Expr.java.

951  {
953  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVShiftRightLogical ( ) throws Z3Exception
inline

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

Definition at line 942 of file Expr.java.

943  {
945  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSignExtension ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector sign extension

Definition at line 878 of file Expr.java.

879  {
881  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSLE ( ) throws Z3Exception
inline

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

Definition at line 757 of file Expr.java.

758  {
760  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSLT ( ) throws Z3Exception
inline

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

Definition at line 790 of file Expr.java.

791  {
793  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSMod ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector signed modulus

Definition at line 701 of file Expr.java.

702  {
704  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSRem ( ) throws Z3Exception
inline

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

Definition at line 685 of file Expr.java.

686  {
688  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVSub ( ) throws Z3Exception
inline

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

Definition at line 653 of file Expr.java.

654  {
656  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVToInt ( ) throws Z3Exception
inline

Indicates whether the term is a coercion from bit-vector to integer

This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

Definition at line 1008 of file Expr.java.

1009  {
1011  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVUDiv ( ) throws Z3Exception
inline

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

Definition at line 677 of file Expr.java.

678  {
680  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVUGE ( ) throws Z3Exception
inline

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

Definition at line 766 of file Expr.java.

767  {
769  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVUGT ( ) throws Z3Exception
inline

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

Definition at line 798 of file Expr.java.

799  {
801  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVULE ( ) throws Z3Exception
inline

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

Definition at line 749 of file Expr.java.

750  {
752  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVULT ( ) throws Z3Exception
inline

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

Definition at line 782 of file Expr.java.

783  {
785  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVUMinus ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector unary minus

Definition at line 637 of file Expr.java.

638  {
640  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVURem ( ) throws Z3Exception
inline

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

Definition at line 693 of file Expr.java.

694  {
696  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVXNOR ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise XNOR

Definition at line 862 of file Expr.java.

863  {
865  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVXOR ( ) throws Z3Exception
inline

Indicates whether the term is a bit-wise XOR

Definition at line 838 of file Expr.java.

839  {
841  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVXOR3 ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector ternary XOR

The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)

Definition at line 1028 of file Expr.java.

1029  {
1031  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isBVZeroExtension ( ) throws Z3Exception
inline

Indicates whether the term is a bit-vector zero extension

Definition at line 886 of file Expr.java.

887  {
889  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isConst ( ) throws Z3Exception
inline

Indicates whether the term represents a constant.

Definition at line 215 of file Expr.java.

216  {
217  return isApp() && getNumArgs() == 0 && getFuncDecl().getDomainSize() == 0;
218  }
boolean isApp()
Definition: AST.java:144
FuncDecl getFuncDecl()
Definition: Expr.java:63
boolean isConstantArray ( ) throws Z3Exception
inline

Indicates whether the term is a constant array.

For example, select(const(v),i) = v holds for every v and i. The function is unary.

Definition at line 527 of file Expr.java.

528  {
530  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isDefaultArray ( ) throws Z3Exception
inline

Indicates whether the term is a default array.

For example default(const(v)) = v. The function is unary.

Definition at line 536 of file Expr.java.

537  {
539  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isDistinct ( ) throws Z3Exception
inline

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

Definition at line 282 of file Expr.java.

283  {
285  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isDiv ( ) throws Z3Exception
inline

Indicates whether the term is division (binary)

Definition at line 440 of file Expr.java.

441  {
443  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isEmptyRelation ( ) throws Z3Exception
inline

Indicates whether the term is an empty relation

Definition at line 1574 of file Expr.java.

1575  {
1577  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isEq ( ) throws Z3Exception
inline

Indicates whether the term is an equality predicate.

Definition at line 273 of file Expr.java.

274  {
276  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isFalse ( ) throws Z3Exception
inline

Indicates whether the term is the constant false.

Definition at line 265 of file Expr.java.

266  {
268  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isFiniteDomain ( ) throws Z3Exception
inline

Indicates whether the term is of an array sort.

Definition at line 1696 of file Expr.java.

1697  {
1698  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1699  .getSortKind(getContext().nCtx(),
1700  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT
1701  .toInt());
1702  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isFiniteDomainLT ( ) throws Z3Exception
inline

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

Definition at line 1707 of file Expr.java.

1708  {
1710  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isGE ( ) throws Z3Exception
inline

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

Definition at line 384 of file Expr.java.

385  {
387  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isGT ( ) throws Z3Exception
inline

Indicates whether the term is a greater-than

Definition at line 400 of file Expr.java.

401  {
403  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isIDiv ( ) throws Z3Exception
inline

Indicates whether the term is integer division (binary)

Definition at line 448 of file Expr.java.

449  {
451  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isIff ( ) throws Z3Exception
inline

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

Definition at line 315 of file Expr.java.

316  {
318  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isImplies ( ) throws Z3Exception
inline

Indicates whether the term is an implication

Definition at line 339 of file Expr.java.

340  {
342  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isInt ( ) throws Z3Exception
inline

Indicates whether the term is of integer sort.

Definition at line 347 of file Expr.java.

Referenced by Expr.isIntNum().

348  {
349  return (Native.isNumeralAst(getContext().nCtx(), getNativeObject()) && Native
350  .getSortKind(getContext().nCtx(),
351  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_INT_SORT
352  .toInt());
353  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isIntNum ( ) throws Z3Exception
inline

Indicates whether the term is an integer numeral.

Definition at line 223 of file Expr.java.

224  {
225  return isNumeral() && isInt();
226  }
boolean isNumeral()
Definition: Expr.java:188
boolean isInt()
Definition: Expr.java:347
boolean isIntToBV ( ) throws Z3Exception
inline

Indicates whether the term is a coercion from integer to bit-vector

This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

Definition at line 997 of file Expr.java.

998  {
1000  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isIntToReal ( ) throws Z3Exception
inline

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

Definition at line 472 of file Expr.java.

473  {
475  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isIsEmptyRelation ( ) throws Z3Exception
inline

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

Definition at line 1582 of file Expr.java.

1583  {
1585  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isITE ( ) throws Z3Exception
inline

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

Definition at line 290 of file Expr.java.

291  {
293  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isLabel ( ) throws Z3Exception
inline

Indicates whether the term is a label (used by the Boogie Verification condition generator).

The label has two parameters, a string and a Boolean polarity. It takes one argument, a formula.

Definition at line 1038 of file Expr.java.

1039  {
1041  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isLabelLit ( ) throws Z3Exception
inline

Indicates whether the term is a label literal (used by the Boogie Verification condition generator).

A label literal has a set of string parameters. It takes no arguments.

Definition at line 1048 of file Expr.java.

1049  {
1051  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isLE ( ) throws Z3Exception
inline

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

Definition at line 376 of file Expr.java.

377  {
379  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isLT ( ) throws Z3Exception
inline

Indicates whether the term is a less-than

Definition at line 392 of file Expr.java.

393  {
395  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isModulus ( ) throws Z3Exception
inline

Indicates whether the term is modulus (binary)

Definition at line 464 of file Expr.java.

465  {
467  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isMul ( ) throws Z3Exception
inline

Indicates whether the term is multiplication (binary)

Definition at line 432 of file Expr.java.

433  {
435  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isNot ( ) throws Z3Exception
inline

Indicates whether the term is a negation

Definition at line 331 of file Expr.java.

332  {
334  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isNumeral ( ) throws Z3Exception
inline

Indicates whether the term is a numeral

Definition at line 188 of file Expr.java.

Referenced by Expr.isIntNum(), and Expr.isRatNum().

189  {
190  return Native.isNumeralAst(getContext().nCtx(), getNativeObject());
191  }
boolean isOEQ ( ) throws Z3Exception
inline

Indicates whether the term is a binary equivalence modulo namings.

This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

Definition at line 1058 of file Expr.java.

1059  {
1060  return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_OEQ;
1061  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isOr ( ) throws Z3Exception
inline

Indicates whether the term is an n-ary disjunction

Definition at line 306 of file Expr.java.

307  {
309  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofAndElimination ( ) throws Z3Exception
inline

Indicates whether the term is a proof by elimination of AND

Given a proof for (and l_1 ... l_n), produces a proof for l_i T1: (and l_1 ... l_n) [and-elim T1]: l_i

Definition at line 1194 of file Expr.java.

1195  {
1197  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofApplyDef ( ) throws Z3Exception
inline

Indicates whether the term is a proof for application of a definition

[apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Definition at line 1424 of file Expr.java.

1425  {
1427  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofAsserted ( ) throws Z3Exception
inline

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

Definition at line 1074 of file Expr.java.

1075  {
1077  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofCNFStar ( ) throws Z3Exception
inline

Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.

A proof for (~ P Q) where Q is in conjunctive normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1501 of file Expr.java.

1502  {
1504  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofCommutativity ( ) throws Z3Exception
inline

Indicates whether the term is a proof by commutativity

[comm]: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Definition at line 1370 of file Expr.java.

1371  {
1373  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofDefAxiom ( ) throws Z3Exception
inline

Indicates whether the term is a proof for Tseitin-like axioms

Proof object used to justify Tseitin's like axioms:

(or (not (and p q)) p) (or (not (and p q)) q) (or (not (and p q r)) p) (or (not (and p q r)) q) (or (not (and p q r)) r) ... (or (and p q) (not p) (not q)) (or (not (or p q)) p q) (or (or p q) (not p)) (or (or p q) (not q)) (or (not (iff p q)) (not p) q) (or (not (iff p q)) p (not q)) (or (iff p q) (not p) (not q)) (or (iff p q) p q) (or (not (ite a b c)) (not a) b) (or (not (ite a b c)) a c) (or (ite a b c) (not a) (not b)) (or (ite a b c) a (not c)) (or (not (not a)) (not a)) (or (not a) a)

This proof object has no antecedents. Note: all axioms are propositional tautologies. Note also that 'and' and 'or' can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

Definition at line 1393 of file Expr.java.

1394  {
1396  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofDefIntro ( ) throws Z3Exception
inline

Indicates whether the term is a proof for introduction of a name

Introduces a name for a formula/term. Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type: [def-intro]: (and (or n (not e)) (or (not n) e))

or: [def-intro]: (or (not n) e) when e only occurs positively.

When e is of the form (ite cond th el): [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise: [def-intro]: (= n e)

Definition at line 1414 of file Expr.java.

1415  {
1417  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofDER ( ) throws Z3Exception
inline

Indicates whether the term is a proof for destructive equality resolution

A proof for destructive equality resolution: (iff (forall (x) (or (not (= x t)) P[x])) P[t]) if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

Definition at line 1297 of file Expr.java.

1298  {
1300  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofDistributivity ( ) throws Z3Exception
inline

Indicates whether the term is a distributivity proof object.

Given that f (= or) distributes over g (= and), produces a proof for (= (f a (g c d)) (g (f a c) (f a d))) If f and g are associative, this proof also justifies the following equality: (= (f (g a b) (g c d)) (g (f a c) (f a d) (f b c) (f b d))) where each f and g can have arbitrary number of arguments.

This proof object has no antecedents. Remark. This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

Definition at line 1184 of file Expr.java.

1185  {
1187  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofElimUnusedVars ( ) throws Z3Exception
inline

Indicates whether the term is a proof for elimination of unused variables.

A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) (forall (x_1 ... x_n) p[x_1 ... x_n]))

It is used to justify the elimination of unused variables. This proof object has no antecedents.

Definition at line 1283 of file Expr.java.

1284  {
1286  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofGoal ( ) throws Z3Exception
inline

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

Definition at line 1083 of file Expr.java.

1084  {
1086  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofHypothesis ( ) throws Z3Exception
inline

Indicates whether the term is a hypthesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1315 of file Expr.java.

1316  {
1318  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofIFFFalse ( ) throws Z3Exception
inline

Indicates whether the term is a proof by iff-false

T1: (not p) [iff-false T1]: (iff p false)

Definition at line 1356 of file Expr.java.

1357  {
1359  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofIFFOEQ ( ) throws Z3Exception
inline

Indicates whether the term is a proof iff-oeq

T1: (iff p q) [iff~ T1]: (~ p q)

Definition at line 1433 of file Expr.java.

1434  {
1436  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofIFFTrue ( ) throws Z3Exception
inline

Indicates whether the term is a proof by iff-true

T1: p [iff-true T1]: (iff p true)

Definition at line 1347 of file Expr.java.

1348  {
1350  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofLemma ( ) throws Z3Exception
inline

Indicates whether the term is a proof by lemma

T1: false [lemma T1]: (or (not l_1) ... (not l_n))

This proof object has one antecedent: a hypothetical proof for false. It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the hypotheses: l_1, ..., l_n.

Definition at line 1328 of file Expr.java.

1329  {
1331  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofModusPonens ( ) throws Z3Exception
inline

Indicates whether the term is proof via modus ponens

Given a proof for p and a proof for (implies p q), produces a proof for q. T1: p T2: (implies p q) [mp T1 T2]: q The second antecedents may also be a proof for (iff p q).

Definition at line 1094 of file Expr.java.

1095  {
1097  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofModusPonensOEQ ( ) throws Z3Exception
inline

Indicates whether the term is a proof by modus ponens for equi-satisfiability.

Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q) [mp~ T1 T2]: q

Definition at line 1525 of file Expr.java.

1526  {
1528  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofMonotonicity ( ) throws Z3Exception
inline

Indicates whether the term is a monotonicity proof object.

T1: (R t_1 s_1) ... Tn: (R t_n s_n) [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are supressed to save space.

Definition at line 1158 of file Expr.java.

1159  {
1161  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofNNFNeg ( ) throws Z3Exception
inline

Indicates whether the term is a proof for a negative NNF step

Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) and T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2' [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) (and (or r_1 r_2) (or r_1' r_2')))

Definition at line 1474 of file Expr.java.

1475  {
1477  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofNNFPos ( ) throws Z3Exception
inline

Indicates whether the term is a proof for a positive NNF step

Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1 T2: (not s_2) ~ r_2 T3: s_1 ~ r_1' T4: s_2 ~ r_2'

r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))

(b) When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are 'implies', 'iff', 'xor', 'ite'. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives 'and' and 'or'.

Definition at line 1458 of file Expr.java.

1459  {
1461  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofNNFStar ( ) throws Z3Exception
inline

Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.

A proof for (~ P Q) where Q is in negation normal form.

This proof object is only used if the parameter PROOF_MODE is 1.

This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.

Definition at line 1489 of file Expr.java.

1490  {
1492  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofOrElimination ( ) throws Z3Exception
inline

Indicates whether the term is a proof by eliminiation of not-or

Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). T1: (not (or l_1 ... l_n)) [not-or-elim T1]: (not l_i)

Definition at line 1204 of file Expr.java.

1205  {
1207  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofPullQuant ( ) throws Z3Exception
inline

Indicates whether the term is a proof for pulling quantifiers out.

A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Definition at line 1247 of file Expr.java.

1248  {
1250  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofPullQuantStar ( ) throws Z3Exception
inline

Indicates whether the term is a proof for pulling quantifiers out.

A proof for (iff P Q) where Q is in prenex normal form. This proof object is only used if the parameter PROOF_MODE is 1. This proof object has no antecedents

Definition at line 1258 of file Expr.java.

1259  {
1261  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofPushQuant ( ) throws Z3Exception
inline

Indicates whether the term is a proof for pushing quantifiers in.

A proof for: (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) ... (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) This proof object has no antecedents

Definition at line 1270 of file Expr.java.

1271  {
1273  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofQuantInst ( ) throws Z3Exception
inline

Indicates whether the term is a proof for quantifier instantiation

A proof of (or (not (forall (x) (P x))) (P a))

Definition at line 1306 of file Expr.java.

1307  {
1309  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofQuantIntro ( ) throws Z3Exception
inline

Indicates whether the term is a quant-intro proof

Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)). T1: (~ p q) [quant-intro T1]: (~ (forall (x) p) (forall (x) q))

Definition at line 1168 of file Expr.java.

1169  {
1171  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofReflexivity ( ) throws Z3Exception
inline

Indicates whether the term is a proof for (R t t), where R is a reflexive relation.

This proof object has no antecedents. The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either '~', '=' or 'iff'.

Definition at line 1106 of file Expr.java.

1107  {
1109  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofRewrite ( ) throws Z3Exception
inline

Indicates whether the term is a proof by rewriting

A proof for a local rewriting step (= t s). The head function symbol of t is interpreted.

This proof object has no antecedents. The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s). Remark: if f is bool, then = is iff.

Examples: (= (+ x 0) x) (= (+ x 1 2) (+ 3 x)) (iff (or x false) x)

Definition at line 1221 of file Expr.java.

1222  {
1224  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofRewriteStar ( ) throws Z3Exception
inline

Indicates whether the term is a proof by rewriting

A proof for rewriting an expression t into an expression s. This proof object is used if the parameter PROOF_MODE is 1. This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules. The object is also used in a few cases if the parameter PROOF_MODE is 2. The cases are: - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to Booleans (BIT2BOOL=true) - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)

Definition at line 1237 of file Expr.java.

1238  {
1240  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofSkolemize ( ) throws Z3Exception
inline

Indicates whether the term is a proof for a Skolemization step

Proof for:

(p x y)) (p (sk y) y))

This proof object has no antecedents.

Definition at line 1515 of file Expr.java.

1516  {
1518  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofSymmetry ( ) throws Z3Exception
inline

Indicates whether the term is proof by symmetricity of a relation

Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t). T1: (R t s) [symmetry T1]: (R s t) T1 is the antecedent of this proof object.

Definition at line 1117 of file Expr.java.

1118  {
1120  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofTheoryLemma ( ) throws Z3Exception
inline

Indicates whether the term is a proof for theory lemma

Generic proof for theory lemmas.

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

Definition at line 1544 of file Expr.java.

1545  {
1547  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofTransitivity ( ) throws Z3Exception
inline

Indicates whether the term is a proof by transitivity of a relation

Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof for (R t u). T1: (R t s) T2: (R s u) [trans T1 T2]: (R t u)

Definition at line 1128 of file Expr.java.

1129  {
1131  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofTransitivityStar ( ) throws Z3Exception
inline

Indicates whether the term is a proof by condensed transitivity of a relation

Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1. It combines several symmetry and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d) [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

Definition at line 1146 of file Expr.java.

1147  {
1149  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofTrue ( ) throws Z3Exception
inline

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

Definition at line 1066 of file Expr.java.

1067  {
1069  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isProofUnitResolution ( ) throws Z3Exception
inline

Indicates whether the term is a proof by unit resolution

T1: (or l_1 ... l_n l_1' ... l_m') T2: (not l_1) ... T(n+1): (not l_n) [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')

Definition at line 1338 of file Expr.java.

1339  {
1341  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRatNum ( ) throws Z3Exception
inline

Indicates whether the term is a real numeral.

Definition at line 231 of file Expr.java.

232  {
233  return isNumeral() && isReal();
234  }
boolean isReal()
Definition: Expr.java:358
boolean isNumeral()
Definition: Expr.java:188
boolean isReal ( ) throws Z3Exception
inline

Indicates whether the term is of sort real.

Definition at line 358 of file Expr.java.

Referenced by Expr.isRatNum().

359  {
360  return Native.getSortKind(getContext().nCtx(),
361  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_REAL_SORT
362  .toInt();
363  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isRealIsInt ( ) throws Z3Exception
inline

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

Definition at line 489 of file Expr.java.

490  {
492  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRealToInt ( ) throws Z3Exception
inline

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

Definition at line 480 of file Expr.java.

481  {
483  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelation ( ) throws Z3Exception
inline

Indicates whether the term is of an array sort.

Definition at line 1552 of file Expr.java.

1553  {
1554  return (Native.isApp(getContext().nCtx(), getNativeObject()) && Native
1555  .getSortKind(getContext().nCtx(),
1556  Native.getSort(getContext().nCtx(), getNativeObject())) == Z3_sort_kind.Z3_RELATION_SORT
1557  .toInt());
1558  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
boolean isRelationalJoin ( ) throws Z3Exception
inline

Indicates whether the term is a relational join

Definition at line 1590 of file Expr.java.

1591  {
1593  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationClone ( ) throws Z3Exception
inline

Indicates whether the term is a relational clone (copy)

Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind

See also
IsRelationUnion

to perform destructive updates to the first argument.

Definition at line 1688 of file Expr.java.

1689  {
1691  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationComplement ( ) throws Z3Exception
inline

Indicates whether the term is the complement of a relation

Definition at line 1665 of file Expr.java.

1666  {
1668  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationFilter ( ) throws Z3Exception
inline

Indicates whether the term is a relation filter

Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Brujin indices corresponding to the columns of the relation. So the first column in the relation has index 0.

Definition at line 1630 of file Expr.java.

1631  {
1633  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationNegationFilter ( ) throws Z3Exception
inline

Indicates whether the term is an intersection of a relation with the negation of another.

Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

Definition at line 1647 of file Expr.java.

1648  {
1650  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationProject ( ) throws Z3Exception
inline

Indicates whether the term is a projection of columns (provided as numbers in the parameters).

The function takes one argument.

Definition at line 1618 of file Expr.java.

1619  {
1621  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationRename ( ) throws Z3Exception
inline

Indicates whether the term is the renaming of a column in a relation

The function takes one argument. The parameters contain the renaming as a cycle.

Definition at line 1657 of file Expr.java.

1658  {
1660  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationSelect ( ) throws Z3Exception
inline

Indicates whether the term is a relational select

Check if a record is an element of the relation. The function takes

n+1

arguments, where the first argument is a relation, and the remaining

n

arguments correspond to a record.

Definition at line 1676 of file Expr.java.

1677  {
1679  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationStore ( ) throws Z3Exception
inline

Indicates whether the term is an relation store

Insert a record into a relation. The function takes

n+1

arguments, where the first argument is the relation and the remaining

n

elements correspond to the

n

columns of the relation.

Definition at line 1566 of file Expr.java.

1567  {
1569  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationUnion ( ) throws Z3Exception
inline

Indicates whether the term is the union or convex hull of two relations.

The function takes two arguments.

Definition at line 1599 of file Expr.java.

1600  {
1602  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRelationWiden ( ) throws Z3Exception
inline

Indicates whether the term is the widening of two relations

The function takes two arguments.

Definition at line 1608 of file Expr.java.

1609  {
1611  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isRemainder ( ) throws Z3Exception
inline

Indicates whether the term is remainder (binary)

Definition at line 456 of file Expr.java.

457  {
459  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSelect ( ) throws Z3Exception
inline

Indicates whether the term is an array select.

Definition at line 517 of file Expr.java.

518  {
520  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSetComplement ( ) throws Z3Exception
inline

Indicates whether the term is set complement

Definition at line 587 of file Expr.java.

588  {
590  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSetDifference ( ) throws Z3Exception
inline

Indicates whether the term is set difference

Definition at line 579 of file Expr.java.

580  {
582  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSetIntersect ( ) throws Z3Exception
inline

Indicates whether the term is set intersection

Definition at line 571 of file Expr.java.

572  {
574  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSetSubset ( ) throws Z3Exception
inline

Indicates whether the term is set subset

Definition at line 595 of file Expr.java.

596  {
598  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSetUnion ( ) throws Z3Exception
inline

Indicates whether the term is set union

Definition at line 563 of file Expr.java.

564  {
566  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isStore ( ) throws Z3Exception
inline

Indicates whether the term is an array store.

It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.

Definition at line 509 of file Expr.java.

510  {
512  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isSub ( ) throws Z3Exception
inline

Indicates whether the term is subtraction (binary)

Definition at line 416 of file Expr.java.

417  {
419  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isTrue ( ) throws Z3Exception
inline

Indicates whether the term is the constant true.

Definition at line 257 of file Expr.java.

258  {
260  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isUMinus ( ) throws Z3Exception
inline

Indicates whether the term is a unary minus

Definition at line 424 of file Expr.java.

425  {
427  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
boolean isWellSorted ( ) throws Z3Exception
inline

Indicates whether the term is well-sorted.

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

Definition at line 198 of file Expr.java.

199  {
200  return Native.isWellSorted(getContext().nCtx(), getNativeObject());
201  }
boolean isXor ( ) throws Z3Exception
inline

Indicates whether the term is an exclusive or

Definition at line 323 of file Expr.java.

324  {
326  }
boolean isApp()
Definition: AST.java:144
Z3_decl_kind getDeclKind()
Definition: FuncDecl.java:131
FuncDecl getFuncDecl()
Definition: Expr.java:63
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
Expr simplify ( ) throws Z3Exception
inline

Returns a simplified version of the expression

Definition at line 35 of file Expr.java.

36  {
37  return simplify(null);
38  }
Expr simplify ( Params  p) throws Z3Exception
inline

Returns a simplified version of the expression A set of parameters

Parameters
pa Params object

to configure the simplifier

See also
Context.SimplifyHelp

Definition at line 46 of file Expr.java.

47  {
48 
49  if (p == null)
50  return Expr.create(getContext(),
51  Native.simplify(getContext().nCtx(), getNativeObject()));
52  else
53  return Expr.create(
54  getContext(),
55  Native.simplifyEx(getContext().nCtx(), getNativeObject(),
56  p.getNativeObject()));
57  }
Expr(Context ctx)
Definition: Expr.java:1738
Expr substitute ( Expr[]  from,
Expr[]  to 
) throws Z3Exception
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 123 of file Expr.java.

Referenced by Expr.substitute().

124  {
125  getContext().checkContextMatch(from);
126  getContext().checkContextMatch(to);
127  if (from.length != to.length)
128  throw new Z3Exception("Argument sizes do not match");
129  return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
130  getNativeObject(), (int) from.length, Expr.arrayToNative(from),
131  Expr.arrayToNative(to)));
132  }
Expr(Context ctx)
Definition: Expr.java:1738
Expr substitute ( Expr  from,
Expr  to 
) throws Z3Exception
inline

Substitute every occurrence of from in the expression with to.

See also
Substitute(Expr[],Expr[])

Definition at line 138 of file Expr.java.

139  {
140 
141  return substitute(new Expr[] { from }, new Expr[] { to });
142  }
Expr(Context ctx)
Definition: Expr.java:1738
Expr substitute(Expr[] from, Expr[] to)
Definition: Expr.java:123
Expr substituteVars ( Expr[]  to) throws Z3Exception
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]

.

Definition at line 150 of file Expr.java.

151  {
152 
153  getContext().checkContextMatch(to);
154  return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
155  getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
156  }
Expr(Context ctx)
Definition: Expr.java:1738
String toString ( )
inline

Returns a string representation of the expression.

Definition at line 180 of file Expr.java.

181  {
182  return super.toString();
183  }
Expr translate ( Context  ctx) throws Z3Exception
inline

Translates (copies) the term to the Context ctx .

Parameters
ctxA context
Returns
A copy of the term which is associated with ctx

Definition at line 165 of file Expr.java.

166  {
167 
168  if (getContext() == ctx)
169  return this;
170  else
171  return Expr.create(
172  ctx,
173  Native.translate(getContext().nCtx(), getNativeObject(),
174  ctx.nCtx()));
175  }
Expr(Context ctx)
Definition: Expr.java:1738
void update ( Expr[]  args) throws Z3Exception
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 105 of file Expr.java.

106  {
107  getContext().checkContextMatch(args);
108  if (isApp() && args.length != getNumArgs())
109  throw new Z3Exception("Number of arguments does not match");
110  setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
111  (int) args.length, Expr.arrayToNative(args)));
112  }
boolean isApp()
Definition: AST.java:144
Expr(Context ctx)
Definition: Expr.java:1738