Static Public Member Functions | |
static Quantifier | of (Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID) |
static Quantifier | of (Context ctx, boolean isForall, Expr<?>[] bound, Expr< BoolSort > body, int weight, Pattern[] patterns, Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID) |
Additional Inherited Members | |
Protected Member Functions inherited from Expr< BoolSort > | |
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 |
Indicates whether the quantifier is existential.
Definition at line 38 of file Quantifier.java.
|
inline |
Indicates whether the quantifier is universal.
Definition at line 30 of file Quantifier.java.
|
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 221 of file Quantifier.java.
|
inlinestatic |
Create a quantified expression.
ctx | Context to create the quantifier on. |
isForall | Quantifier type. |
sorts | Sorts of bound variables. |
names | Names of bound variables |
body | Body of quantifier |
weight | Weight used to indicate priority for qunatifier instantiation |
patterns | Nullable patterns |
noPatterns | Nullable noPatterns |
quantifierID | Nullable quantifierID |
skolemID | Nullable skolemID |
Definition at line 175 of file Quantifier.java.
Referenced by Context.mkExists(), and Context.mkForall().
|
inline |
Translates (copies) the quantifier to the Context
.
ctx | A context |
Z3Exception | on error |
Definition at line 156 of file Quantifier.java.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Solver.__deepcopy__(), and Quantifier.translate().