Z3
src/api/java/Model.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_sort_kind;
00021 
00025 public class Model extends Z3Object
00026 {
00035     public Expr getConstInterp(Expr a) throws Z3Exception
00036     {
00037         getContext().checkContextMatch(a);
00038         return getConstInterp(a.getFuncDecl());
00039     }
00040 
00049     public Expr getConstInterp(FuncDecl f) throws Z3Exception
00050     {
00051         getContext().checkContextMatch(f);
00052         if (f.getArity() != 0
00053                 || Native.getSortKind(getContext().nCtx(),
00054                         Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
00055                         .toInt())
00056             throw new Z3Exception(
00057                     "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
00058 
00059         long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
00060                 f.getNativeObject());
00061         if (n == 0)
00062             return null;
00063         else
00064             return Expr.create(getContext(), n);
00065     }
00066 
00076     public FuncInterp getFuncInterp(FuncDecl f) throws Z3Exception
00077     {
00078         getContext().checkContextMatch(f);
00079 
00080         Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext()
00081                 .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
00082 
00083         if (f.getArity() == 0)
00084         {
00085             long n = Native.modelGetConstInterp(getContext().nCtx(),
00086                     getNativeObject(), f.getNativeObject());
00087 
00088             if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
00089             {
00090                 if (n == 0)
00091                     return null;
00092                 else
00093                 {
00094                     if (Native.isAsArray(getContext().nCtx(), n) ^ true)
00095                         throw new Z3Exception(
00096                                 "Argument was not an array constant");
00097                     long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
00098                     return getFuncInterp(new FuncDecl(getContext(), fd));
00099                 }
00100             } else
00101             {
00102                 throw new Z3Exception(
00103                         "Constant functions do not have a function interpretation; use ConstInterp");
00104             }
00105         } else
00106         {
00107             long n = Native.modelGetFuncInterp(getContext().nCtx(),
00108                     getNativeObject(), f.getNativeObject());
00109             if (n == 0)
00110                 return null;
00111             else
00112                 return new FuncInterp(getContext(), n);
00113         }
00114     }
00115 
00119     public int getNumConsts() throws Z3Exception
00120     {
00121         return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
00122     }
00123 
00129     public FuncDecl[] getConstDecls() throws Z3Exception
00130     {
00131         int n = getNumConsts();
00132         FuncDecl[] res = new FuncDecl[n];
00133         for (int i = 0; i < n; i++)
00134             res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
00135                     .nCtx(), getNativeObject(), i));
00136         return res;
00137     }
00138 
00142     public int getNumFuncs() throws Z3Exception
00143     {
00144         return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
00145     }
00146 
00152     public FuncDecl[] getFuncDecls() throws Z3Exception
00153     {
00154         int n = getNumFuncs();
00155         FuncDecl[] res = new FuncDecl[n];
00156         for (int i = 0; i < n; i++)
00157             res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
00158                     .nCtx(), getNativeObject(), i));
00159         return res;
00160     }
00161 
00167     public FuncDecl[] getDecls() throws Z3Exception
00168     {
00169         int nFuncs = getNumFuncs();
00170         int nConsts = getNumConsts();
00171         int n = nFuncs + nConsts;
00172         FuncDecl[] res = new FuncDecl[n];
00173         for (int i = 0; i < nConsts; i++)
00174             res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
00175                     .nCtx(), getNativeObject(), i));
00176         for (int i = 0; i < nFuncs; i++)
00177             res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
00178                     getContext().nCtx(), getNativeObject(), i));
00179         return res;
00180     }
00181 
00186     @SuppressWarnings("serial")
00187     public class ModelEvaluationFailedException extends Z3Exception
00188     {
00192         public ModelEvaluationFailedException()
00193         {
00194             super();
00195         }
00196     }
00197 
00211     public Expr eval(Expr t, boolean completion) throws Z3Exception
00212     {
00213         Native.LongPtr v = new Native.LongPtr();
00214         if (Native.modelEval(getContext().nCtx(), getNativeObject(),
00215                 t.getNativeObject(), (completion) ? true : false, v) ^ true)
00216             throw new ModelEvaluationFailedException();
00217         else
00218             return Expr.create(getContext(), v.value);
00219     }
00220 
00226     public Expr evaluate(Expr t, boolean completion) throws Z3Exception
00227     {
00228         return eval(t, completion);
00229     }
00230 
00235     public int getNumSorts() throws Z3Exception
00236     {
00237         return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
00238     }
00239 
00249     public Sort[] getSorts() throws Z3Exception
00250     {
00251 
00252         int n = getNumSorts();
00253         Sort[] res = new Sort[n];
00254         for (int i = 0; i < n; i++)
00255             res[i] = Sort.create(getContext(),
00256                     Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
00257         return res;
00258     }
00259 
00269     public Expr[] getSortUniverse(Sort s) throws Z3Exception
00270     {
00271 
00272         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
00273                 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
00274         int n = nUniv.size();
00275         Expr[] res = new Expr[n];
00276         for (int i = 0; i < n; i++)
00277             res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
00278         return res;
00279     }
00280 
00286     public String toString()
00287     {
00288         try
00289         {
00290             return Native.modelToString(getContext().nCtx(), getNativeObject());
00291         } catch (Z3Exception e)
00292         {
00293             return "Z3Exception: " + e.getMessage();
00294         }
00295     }
00296 
00297     Model(Context ctx, long obj) throws Z3Exception
00298     {
00299         super(ctx, obj);
00300     }
00301 
00302     void incRef(long o) throws Z3Exception
00303     {
00304         getContext().model_DRQ().incAndClear(getContext(), o);
00305         super.incRef(o);
00306     }
00307 
00308     void decRef(long o) throws Z3Exception
00309     {
00310         getContext().model_DRQ().add(o);
00311         super.decRef(o);
00312     }
00313 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines