Z3
src/api/java/Quantifier.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_ast_kind;
00021 
00025 public class Quantifier extends BoolExpr
00026 {
00030     public boolean isUniversal() throws Z3Exception
00031     {
00032         return Native.isQuantifierForall(getContext().nCtx(), getNativeObject());
00033     }
00034 
00038     public boolean isExistential() throws Z3Exception
00039     {
00040         return !isUniversal();
00041     }
00042 
00046     public int getWeight() throws Z3Exception
00047     {
00048         return Native.getQuantifierWeight(getContext().nCtx(), getNativeObject());
00049     }
00050 
00054     public int getNumPatterns() throws Z3Exception
00055     {
00056         return Native
00057                 .getQuantifierNumPatterns(getContext().nCtx(), getNativeObject());
00058     }
00059 
00065     public Pattern[] getPatterns() throws Z3Exception
00066     {
00067         int n = getNumPatterns();
00068         Pattern[] res = new Pattern[n];
00069         for (int i = 0; i < n; i++)
00070             res[i] = new Pattern(getContext(), Native.getQuantifierPatternAst(
00071                     getContext().nCtx(), getNativeObject(), i));
00072         return res;
00073     }
00074 
00078     public int getNumNoPatterns() throws Z3Exception
00079     {
00080         return Native.getQuantifierNumNoPatterns(getContext().nCtx(),
00081                 getNativeObject());
00082     }
00083 
00089     public Pattern[] getNoPatterns() throws Z3Exception
00090     {
00091         int n = getNumNoPatterns();
00092         Pattern[] res = new Pattern[n];
00093         for (int i = 0; i < n; i++)
00094             res[i] = new Pattern(getContext(), Native.getQuantifierNoPatternAst(
00095                     getContext().nCtx(), getNativeObject(), i));
00096         return res;
00097     }
00098 
00102     public int getNumBound() throws Z3Exception
00103     {
00104         return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
00105     }
00106 
00112     public Symbol[] getBoundVariableNames() throws Z3Exception
00113     {
00114         int n = getNumBound();
00115         Symbol[] res = new Symbol[n];
00116         for (int i = 0; i < n; i++)
00117             res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
00118                     getContext().nCtx(), getNativeObject(), i));
00119         return res;
00120     }
00121 
00127     public Sort[] getBoundVariableSorts() throws Z3Exception
00128     {
00129         int n = getNumBound();
00130         Sort[] res = new Sort[n];
00131         for (int i = 0; i < n; i++)
00132             res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
00133                     getContext().nCtx(), getNativeObject(), i));
00134         return res;
00135     }
00136 
00142     public BoolExpr getBody() throws Z3Exception
00143     {
00144         return new BoolExpr(getContext(), Native.getQuantifierBody(getContext()
00145                 .nCtx(), getNativeObject()));
00146     }
00147 
00148     Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
00149             Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
00150             Symbol quantifierID, Symbol skolemID) throws Z3Exception
00151     {
00152         super(ctx);
00153 
00154         getContext().checkContextMatch(patterns);
00155         getContext().checkContextMatch(noPatterns);
00156         getContext().checkContextMatch(sorts);
00157         getContext().checkContextMatch(names);
00158         getContext().checkContextMatch(body);
00159 
00160         if (sorts.length != names.length)
00161             throw new Z3Exception(
00162                     "Number of sorts does not match number of names");
00163 
00164         if (noPatterns == null && quantifierID == null && skolemID == null)
00165         {
00166             setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
00167                     : false, weight, AST.arrayLength(patterns), AST
00168                     .arrayToNative(patterns), AST.arrayLength(sorts), AST
00169                     .arrayToNative(sorts), Symbol.arrayToNative(names), body
00170                     .getNativeObject()));
00171         } else
00172         {
00173             setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), 
00174                     (isForall) ? true : false, weight, AST.getNativeObject(quantifierID), 
00175                      AST.getNativeObject(skolemID), 
00176                      AST.arrayLength(patterns), AST.arrayToNative(patterns), 
00177                      AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), 
00178                      AST.arrayLength(sorts), AST.arrayToNative(sorts), 
00179                      Symbol.arrayToNative(names), 
00180                      body.getNativeObject()));
00181         }
00182     }
00183 
00184     Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body,
00185             int weight, Pattern[] patterns, Expr[] noPatterns,
00186             Symbol quantifierID, Symbol skolemID) throws Z3Exception
00187     {
00188         super(ctx);
00189 
00190         getContext().checkContextMatch(noPatterns);
00191         getContext().checkContextMatch(patterns);
00192         // Context().CheckContextMatch(bound);
00193         getContext().checkContextMatch(body);
00194 
00195         if (noPatterns == null && quantifierID == null && skolemID == null)
00196         {
00197             setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
00198                     (isForall) ? true : false, weight, AST.arrayLength(bound),
00199                     AST.arrayToNative(bound), AST.arrayLength(patterns),
00200                     AST.arrayToNative(patterns), body.getNativeObject()));
00201         } else
00202         {
00203             setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
00204                     (isForall) ? true : false, weight,
00205                     AST.getNativeObject(quantifierID),
00206                     AST.getNativeObject(skolemID), AST.arrayLength(bound),
00207                     AST.arrayToNative(bound), AST.arrayLength(patterns),
00208                     AST.arrayToNative(patterns), AST.arrayLength(noPatterns),
00209                     AST.arrayToNative(noPatterns), body.getNativeObject()));
00210         }
00211     }
00212 
00213     Quantifier(Context ctx, long obj) throws Z3Exception
00214     {
00215         super(ctx, obj);
00216     }
00217 
00218     void checkNativeObject(long obj) throws Z3Exception
00219     {
00220         if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
00221                 .toInt())
00222             throw new Z3Exception("Underlying object is not a quantifier");
00223         super.checkNativeObject(obj);
00224     }
00225 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines