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 }