Static Public Member Functions | |
static Quantifier | of (Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
static Quantifier | of (Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
Additional Inherited Members | |
![]() | |
Expr (Context ctx, long obj) | |
Quantifier expressions.
Definition at line 25 of file Quantifier.java.
|
inline |
|
inline |
The symbols for the bound variables.
Z3Exception |
Definition at line 112 of file Quantifier.java.
|
inline |
The sorts of the bound variables.
Z3Exception |
Definition at line 127 of file Quantifier.java.
|
inline |
|
inline |
The number of bound variables.
Definition at line 102 of file Quantifier.java.
Referenced by Quantifier.getBoundVariableNames(), and Quantifier.getBoundVariableSorts().
|
inline |
The number of no-patterns.
Definition at line 78 of file Quantifier.java.
Referenced by Quantifier.getNoPatterns().
|
inline |
The number of patterns.
Definition at line 54 of file Quantifier.java.
Referenced by Quantifier.getPatterns().
|
inline |
|
inline |
The weight of the quantifier.
Definition at line 46 of file Quantifier.java.
|
inline |
|
inline |
Indicates whether the quantifier is universal.
Definition at line 30 of file Quantifier.java.
Referenced by Quantifier.isExistential().
|
inlinestatic |
Create a quantified expression.
patterns | Nullable patterns |
noPatterns | Nullable noPatterns |
quantifierID | Nullable quantifierID |
skolemID | Nullable skolemID |
Definition at line 156 of file Quantifier.java.
Referenced by Context.mkExists(), and Context.mkForall().
|
inlinestatic |
ctx | Context to create the quantifier on. |
isForall | Quantifier type. |
bound | Bound variables. |
body | Body of the quantifier. |
weight | Weight. |
patterns | Nullable array of patterns. |
noPatterns | Nullable array of noPatterns. |
quantifierID | Nullable quantifier identifier. |
skolemID | Nullable skolem identifier. |
Definition at line 202 of file Quantifier.java.