Create a Quantifier. @see #mkForall(Sort[],Symbol[],Expr ,int,Pattern[],Expr<?>[],Symbol,Symbol)
(boolean universal, Sort[] sorts,
Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns,
Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID)
| 2892 | * @see #mkForall(Sort[],Symbol[],Expr<BoolSort>,int,Pattern[],Expr<?>[],Symbol,Symbol) |
| 2893 | **/ |
| 2894 | public Quantifier mkQuantifier(boolean universal, Sort[] sorts, |
| 2895 | Symbol[] names, Expr<BoolSort> body, int weight, Pattern[] patterns, |
| 2896 | Expr<?>[] noPatterns, Symbol quantifierID, Symbol skolemID) |
| 2897 | |
| 2898 | { |
| 2899 | |
| 2900 | if (universal) |
| 2901 | return mkForall(sorts, names, body, weight, patterns, noPatterns, |
| 2902 | quantifierID, skolemID); |
| 2903 | else |
| 2904 | return mkExists(sorts, names, body, weight, patterns, noPatterns, |
| 2905 | quantifierID, skolemID); |
| 2906 | } |
| 2907 | |
| 2908 | /** |
| 2909 | * Create a Quantifier |