Z3
src/api/java/Fixedpoint.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines