00001 00018 package com.microsoft.z3; 00019 00020 import com.microsoft.z3.enumerations.Z3_lbool; 00021 00025 public class Fixedpoint extends Z3Object 00026 { 00027 00031 public String getHelp() throws Z3Exception 00032 { 00033 return Native.fixedpointGetHelp(getContext().nCtx(), getNativeObject()); 00034 } 00035 00041 public void setParameters(Params value) throws Z3Exception 00042 { 00043 00044 getContext().checkContextMatch(value); 00045 Native.fixedpointSetParams(getContext().nCtx(), getNativeObject(), 00046 value.getNativeObject()); 00047 } 00048 00054 public ParamDescrs getParameterDescriptions() throws Z3Exception 00055 { 00056 return new ParamDescrs(getContext(), Native.fixedpointGetParamDescrs( 00057 getContext().nCtx(), getNativeObject())); 00058 } 00059 00065 public void add(BoolExpr ... constraints) throws Z3Exception 00066 { 00067 getContext().checkContextMatch(constraints); 00068 for (BoolExpr a : constraints) 00069 { 00070 Native.fixedpointAssert(getContext().nCtx(), getNativeObject(), 00071 a.getNativeObject()); 00072 } 00073 } 00074 00080 public void registerRelation(FuncDecl f) throws Z3Exception 00081 { 00082 00083 getContext().checkContextMatch(f); 00084 Native.fixedpointRegisterRelation(getContext().nCtx(), getNativeObject(), 00085 f.getNativeObject()); 00086 } 00087 00093 public void addRule(BoolExpr rule, Symbol name) throws Z3Exception 00094 { 00095 00096 getContext().checkContextMatch(rule); 00097 Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(), 00098 rule.getNativeObject(), AST.getNativeObject(name)); 00099 } 00100 00106 public void addFact(FuncDecl pred, int ... args) throws Z3Exception 00107 { 00108 getContext().checkContextMatch(pred); 00109 Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(), 00110 pred.getNativeObject(), (int) args.length, args); 00111 } 00112 00122 public Status query(BoolExpr query) throws Z3Exception 00123 { 00124 00125 getContext().checkContextMatch(query); 00126 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(), 00127 getNativeObject(), query.getNativeObject())); 00128 switch (r) 00129 { 00130 case Z3_L_TRUE: 00131 return Status.SATISFIABLE; 00132 case Z3_L_FALSE: 00133 return Status.UNSATISFIABLE; 00134 default: 00135 return Status.UNKNOWN; 00136 } 00137 } 00138 00147 public Status query(FuncDecl[] relations) throws Z3Exception 00148 { 00149 00150 getContext().checkContextMatch(relations); 00151 Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext() 00152 .nCtx(), getNativeObject(), AST.arrayLength(relations), AST 00153 .arrayToNative(relations))); 00154 switch (r) 00155 { 00156 case Z3_L_TRUE: 00157 return Status.SATISFIABLE; 00158 case Z3_L_FALSE: 00159 return Status.UNSATISFIABLE; 00160 default: 00161 return Status.UNKNOWN; 00162 } 00163 } 00164 00168 public void push() throws Z3Exception 00169 { 00170 Native.fixedpointPush(getContext().nCtx(), getNativeObject()); 00171 } 00172 00178 public void pop() throws Z3Exception 00179 { 00180 Native.fixedpointPop(getContext().nCtx(), getNativeObject()); 00181 } 00182 00188 public void updateRule(BoolExpr rule, Symbol name) throws Z3Exception 00189 { 00190 00191 getContext().checkContextMatch(rule); 00192 Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(), 00193 rule.getNativeObject(), AST.getNativeObject(name)); 00194 } 00195 00202 public Expr getAnswer() throws Z3Exception 00203 { 00204 long ans = Native.fixedpointGetAnswer(getContext().nCtx(), getNativeObject()); 00205 return (ans == 0) ? null : Expr.create(getContext(), ans); 00206 } 00207 00211 public String getReasonUnknown() throws Z3Exception 00212 { 00213 00214 return Native.fixedpointGetReasonUnknown(getContext().nCtx(), 00215 getNativeObject()); 00216 } 00217 00221 public int getNumLevels(FuncDecl predicate) throws Z3Exception 00222 { 00223 return Native.fixedpointGetNumLevels(getContext().nCtx(), getNativeObject(), 00224 predicate.getNativeObject()); 00225 } 00226 00232 public Expr getCoverDelta(int level, FuncDecl predicate) throws Z3Exception 00233 { 00234 long res = Native.fixedpointGetCoverDelta(getContext().nCtx(), 00235 getNativeObject(), level, predicate.getNativeObject()); 00236 return (res == 0) ? null : Expr.create(getContext(), res); 00237 } 00238 00243 public void addCover(int level, FuncDecl predicate, Expr property) 00244 throws Z3Exception 00245 { 00246 Native.fixedpointAddCover(getContext().nCtx(), getNativeObject(), level, 00247 predicate.getNativeObject(), property.getNativeObject()); 00248 } 00249 00253 public String toString() 00254 { 00255 try 00256 { 00257 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), 00258 0, null); 00259 } catch (Z3Exception e) 00260 { 00261 return "Z3Exception: " + e.getMessage(); 00262 } 00263 } 00264 00269 public void setPredicateRepresentation(FuncDecl f, Symbol[] kinds) throws Z3Exception 00270 { 00271 00272 Native.fixedpointSetPredicateRepresentation(getContext().nCtx(), 00273 getNativeObject(), f.getNativeObject(), AST.arrayLength(kinds), 00274 Symbol.arrayToNative(kinds)); 00275 00276 } 00277 00281 public String toString(BoolExpr[] queries) throws Z3Exception 00282 { 00283 00284 return Native.fixedpointToString(getContext().nCtx(), getNativeObject(), 00285 AST.arrayLength(queries), AST.arrayToNative(queries)); 00286 } 00287 00293 public BoolExpr[] getRules() throws Z3Exception 00294 { 00295 00296 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules( 00297 getContext().nCtx(), getNativeObject())); 00298 int n = v.size(); 00299 BoolExpr[] res = new BoolExpr[n]; 00300 for (int i = 0; i < n; i++) 00301 res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); 00302 return res; 00303 } 00304 00310 public BoolExpr[] getAssertions() throws Z3Exception 00311 { 00312 00313 ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions( 00314 getContext().nCtx(), getNativeObject())); 00315 int n = v.size(); 00316 BoolExpr[] res = new BoolExpr[n]; 00317 for (int i = 0; i < n; i++) 00318 res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject()); 00319 return res; 00320 } 00321 00322 Fixedpoint(Context ctx, long obj) throws Z3Exception 00323 { 00324 super(ctx, obj); 00325 } 00326 00327 Fixedpoint(Context ctx) throws Z3Exception 00328 { 00329 super(ctx, Native.mkFixedpoint(ctx.nCtx())); 00330 } 00331 00332 void incRef(long o) throws Z3Exception 00333 { 00334 getContext().fixedpoint_DRQ().incAndClear(getContext(), o); 00335 super.incRef(o); 00336 } 00337 00338 void decRef(long o) throws Z3Exception 00339 { 00340 getContext().fixedpoint_DRQ().add(o); 00341 super.decRef(o); 00342 } 00343 }