Public Member Functions | |
boolean | isUniversal () throws Z3Exception |
boolean | isExistential () throws Z3Exception |
int | getWeight () throws Z3Exception |
int | getNumPatterns () throws Z3Exception |
Pattern[] | getPatterns () throws Z3Exception |
int | getNumNoPatterns () throws Z3Exception |
Pattern[] | getNoPatterns () throws Z3Exception |
int | getNumBound () throws Z3Exception |
Symbol[] | getBoundVariableNames () throws Z3Exception |
Sort[] | getBoundVariableSorts () throws Z3Exception |
BoolExpr | getBody () throws Z3Exception |
Package Functions | |
Quantifier (Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception | |
Quantifier (Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception | |
Quantifier (Context ctx, long obj) throws Z3Exception | |
void | checkNativeObject (long obj) throws Z3Exception |
Quantifier expressions.
Definition at line 25 of file Quantifier.java.
Quantifier | ( | Context | ctx, |
boolean | isForall, | ||
Sort[] | sorts, | ||
Symbol[] | names, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline, package] |
Definition at line 148 of file Quantifier.java.
{ super(ctx); getContext().checkContextMatch(patterns); getContext().checkContextMatch(noPatterns); getContext().checkContextMatch(sorts); getContext().checkContextMatch(names); getContext().checkContextMatch(body); if (sorts.length != names.length) throw new Z3Exception( "Number of sorts does not match number of names"); if (noPatterns == null && quantifierID == null && skolemID == null) { setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true : false, weight, AST.arrayLength(patterns), AST .arrayToNative(patterns), AST.arrayLength(sorts), AST .arrayToNative(sorts), Symbol.arrayToNative(names), body .getNativeObject())); } else { setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), AST.arrayLength(sorts), AST.arrayToNative(sorts), Symbol.arrayToNative(names), body.getNativeObject())); } }
Quantifier | ( | Context | ctx, |
boolean | isForall, | ||
Expr[] | bound, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline, package] |
Definition at line 184 of file Quantifier.java.
{ super(ctx); getContext().checkContextMatch(noPatterns); getContext().checkContextMatch(patterns); // Context().CheckContextMatch(bound); getContext().checkContextMatch(body); if (noPatterns == null && quantifierID == null && skolemID == null) { setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), (isForall) ? true : false, weight, AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(patterns), body.getNativeObject())); } else { setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), body.getNativeObject())); } }
Quantifier | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 213 of file Quantifier.java.
{ super(ctx, obj); }
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented from Expr.
Definition at line 218 of file Quantifier.java.
{ if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST .toInt()) throw new Z3Exception("Underlying object is not a quantifier"); super.checkNativeObject(obj); }
BoolExpr getBody | ( | ) | throws Z3Exception [inline] |
The body of the quantifier.
Z3Exception |
Definition at line 142 of file Quantifier.java.
{ return new BoolExpr(getContext(), Native.getQuantifierBody(getContext() .nCtx(), getNativeObject())); }
Symbol [] getBoundVariableNames | ( | ) | throws Z3Exception [inline] |
The symbols for the bound variables.
Z3Exception |
Definition at line 112 of file Quantifier.java.
{ int n = getNumBound(); Symbol[] res = new Symbol[n]; for (int i = 0; i < n; i++) res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName( getContext().nCtx(), getNativeObject(), i)); return res; }
Sort [] getBoundVariableSorts | ( | ) | throws Z3Exception [inline] |
The sorts of the bound variables.
Z3Exception |
Definition at line 127 of file Quantifier.java.
{ int n = getNumBound(); Sort[] res = new Sort[n]; for (int i = 0; i < n; i++) res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort( getContext().nCtx(), getNativeObject(), i)); return res; }
Pattern [] getNoPatterns | ( | ) | throws Z3Exception [inline] |
The no-patterns.
Z3Exception |
Definition at line 89 of file Quantifier.java.
{ int n = getNumNoPatterns(); Pattern[] res = new Pattern[n]; for (int i = 0; i < n; i++) res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst( getContext().nCtx(), getNativeObject(), i)); return res; }
int getNumBound | ( | ) | throws Z3Exception [inline] |
The number of bound variables.
Definition at line 102 of file Quantifier.java.
Referenced by Quantifier.getBoundVariableNames(), and Quantifier.getBoundVariableSorts().
{ return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject()); }
int getNumNoPatterns | ( | ) | throws Z3Exception [inline] |
The number of no-patterns.
Definition at line 78 of file Quantifier.java.
Referenced by Quantifier.getNoPatterns().
{ return Native.getQuantifierNumNoPatterns(getContext().nCtx(), getNativeObject()); }
int getNumPatterns | ( | ) | throws Z3Exception [inline] |
The number of patterns.
Definition at line 54 of file Quantifier.java.
Referenced by Quantifier.getPatterns().
{ return Native .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject()); }
Pattern [] getPatterns | ( | ) | throws Z3Exception [inline] |
The patterns.
Z3Exception |
Definition at line 65 of file Quantifier.java.
{ int n = getNumPatterns(); Pattern[] res = new Pattern[n]; for (int i = 0; i < n; i++) res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst( getContext().nCtx(), getNativeObject(), i)); return res; }
int getWeight | ( | ) | throws Z3Exception [inline] |
The weight of the quantifier.
Definition at line 46 of file Quantifier.java.
{ return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject()); }
boolean isExistential | ( | ) | throws Z3Exception [inline] |
Indicates whether the quantifier is existential.
Definition at line 38 of file Quantifier.java.
{ return !isUniversal(); }
boolean isUniversal | ( | ) | throws Z3Exception [inline] |
Indicates whether the quantifier is universal.
Definition at line 30 of file Quantifier.java.
Referenced by Quantifier.isExistential().
{ return Native.isQuantifierForall(getContext().nCtx(), getNativeObject()); }