Data Structures | |
class | ModelEvaluationFailedException |
Public Member Functions | |
Expr | getConstInterp (Expr a) throws Z3Exception |
Expr | getConstInterp (FuncDecl f) throws Z3Exception |
FuncInterp | getFuncInterp (FuncDecl f) throws Z3Exception |
int | getNumConsts () throws Z3Exception |
FuncDecl[] | getConstDecls () throws Z3Exception |
int | getNumFuncs () throws Z3Exception |
FuncDecl[] | getFuncDecls () throws Z3Exception |
FuncDecl[] | getDecls () throws Z3Exception |
Expr | eval (Expr t, boolean completion) throws Z3Exception |
Expr | evaluate (Expr t, boolean completion) throws Z3Exception |
int | getNumSorts () throws Z3Exception |
Sort[] | getSorts () throws Z3Exception |
Expr[] | getSortUniverse (Sort s) throws Z3Exception |
String | toString () |
Package Functions | |
Model (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
A Model contains interpretations (assignments) of constants and functions.
Definition at line 25 of file Model.java.
Model | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 297 of file Model.java.
{ super(ctx, obj); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 308 of file Model.java.
{ getContext().model_DRQ().add(o); super.decRef(o); }
Expr eval | ( | Expr | t, |
boolean | completion | ||
) | throws Z3Exception [inline] |
Evaluates the expression t in the current model. This function may fail if t contains quantifiers, is partial (MODEL_PARTIAL enabled), or if t is not well-sorted. In this case a ModelEvaluationFailedException
is thrown.
t | An expression |
completion | When this flag is enabled, a model value will be assigned to any constant or function that does not have an interpretation in the model. |
Z3Exception |
Definition at line 211 of file Model.java.
Referenced by Model.evaluate().
{ Native.LongPtr v = new Native.LongPtr(); if (Native.modelEval(getContext().nCtx(), getNativeObject(), t.getNativeObject(), (completion) ? true : false, v) ^ true) throw new ModelEvaluationFailedException(); else return Expr.create(getContext(), v.value); }
Expr evaluate | ( | Expr | t, |
boolean | completion | ||
) | throws Z3Exception [inline] |
Alias for Eval
.
Z3Exception |
Definition at line 226 of file Model.java.
{ return eval(t, completion); }
FuncDecl [] getConstDecls | ( | ) | throws Z3Exception [inline] |
The function declarations of the constants in the model.
Z3Exception |
Definition at line 129 of file Model.java.
{ int n = getNumConsts(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext() .nCtx(), getNativeObject(), i)); return res; }
Expr getConstInterp | ( | Expr | a | ) | throws Z3Exception [inline] |
Retrieves the interpretation (the assignment) of a in the model.
a | A Constant |
Z3Exception |
Definition at line 35 of file Model.java.
{ getContext().checkContextMatch(a); return getConstInterp(a.getFuncDecl()); }
Expr getConstInterp | ( | FuncDecl | f | ) | throws Z3Exception [inline] |
Retrieves the interpretation (the assignment) of f in the model.
f | A function declaration of zero arity |
Z3Exception |
Definition at line 49 of file Model.java.
{ getContext().checkContextMatch(f); if (f.getArity() != 0 || Native.getSortKind(getContext().nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT .toInt()) throw new Z3Exception( "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); if (n == 0) return null; else return Expr.create(getContext(), n); }
FuncDecl [] getDecls | ( | ) | throws Z3Exception [inline] |
All symbols that have an interpretation in the model.
Z3Exception |
Definition at line 167 of file Model.java.
{ int nFuncs = getNumFuncs(); int nConsts = getNumConsts(); int n = nFuncs + nConsts; FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < nConsts; i++) res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext() .nCtx(), getNativeObject(), i)); for (int i = 0; i < nFuncs; i++) res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl( getContext().nCtx(), getNativeObject(), i)); return res; }
FuncDecl [] getFuncDecls | ( | ) | throws Z3Exception [inline] |
The function declarations of the function interpretations in the model.
Z3Exception |
Definition at line 152 of file Model.java.
{ int n = getNumFuncs(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext() .nCtx(), getNativeObject(), i)); return res; }
FuncInterp getFuncInterp | ( | FuncDecl | f | ) | throws Z3Exception [inline] |
Retrieves the interpretation (the assignment) of a non-constant f in the model.
f | A function declaration of non-zero arity |
Z3Exception |
Definition at line 76 of file Model.java.
{ getContext().checkContextMatch(f); Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext() .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject()))); if (f.getArity() == 0) { long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); if (sk == Z3_sort_kind.Z3_ARRAY_SORT) { if (n == 0) return null; else { if (Native.isAsArray(getContext().nCtx(), n) ^ true) throw new Z3Exception( "Argument was not an array constant"); long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); return getFuncInterp(new FuncDecl(getContext(), fd)); } } else { throw new Z3Exception( "Constant functions do not have a function interpretation; use ConstInterp"); } } else { long n = Native.modelGetFuncInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); if (n == 0) return null; else return new FuncInterp(getContext(), n); } }
int getNumConsts | ( | ) | throws Z3Exception [inline] |
The number of constants that have an interpretation in the model.
Definition at line 119 of file Model.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
{ return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject()); }
int getNumFuncs | ( | ) | throws Z3Exception [inline] |
The number of function interpretations in the model.
Definition at line 142 of file Model.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
{ return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject()); }
int getNumSorts | ( | ) | throws Z3Exception [inline] |
The number of uninterpreted sorts that the model has an interpretation for.
Definition at line 235 of file Model.java.
Referenced by Model.getSorts().
{ return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject()); }
Sort [] getSorts | ( | ) | throws Z3Exception [inline] |
The uninterpreted sorts that the model has an interpretation for. Z3 also provides an intepretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort.
Z3Exception |
Definition at line 249 of file Model.java.
{ int n = getNumSorts(); Sort[] res = new Sort[n]; for (int i = 0; i < n; i++) res[i] = Sort.create(getContext(), Native.modelGetSort(getContext().nCtx(), getNativeObject(), i)); return res; }
Expr [] getSortUniverse | ( | Sort | s | ) | throws Z3Exception [inline] |
The finite set of distinct values that represent the interpretation for sort s .
s | An uninterpreted sort |
Z3Exception |
Definition at line 269 of file Model.java.
{ ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse( getContext().nCtx(), getNativeObject(), s.getNativeObject())); int n = nUniv.size(); Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject()); return res; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 302 of file Model.java.
{ getContext().model_DRQ().incAndClear(getContext(), o); super.incRef(o); }
String toString | ( | ) | [inline] |
Conversion of models to strings.
Definition at line 286 of file Model.java.
{ try { return Native.modelToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }