Inheritance diagram for Model:

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 ()

Public Member Functions inherited from Z3Object
void	dispose () throws Z3Exception

Public Member Functions inherited from IDisposable
void	dispose () throws Z3Exception

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize () throws Z3Exception

Detailed Description

A Model contains interpretations (assignments) of constants and functions.

Definition at line 25 of file Model.java.

Member Function Documentation

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.

Parameters

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.

Returns: The evaluation of t in the model.

Exceptions

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.

Exceptions

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.

Exceptions

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.

Parameters

a	A Constant

Returns: An expression if the constant has an interpretation in the model, null otherwise.

Exceptions

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.

Parameters

f	A function declaration of zero arity

Returns: An expression if the function has an interpretation in the model, null otherwise.

Exceptions

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.

Exceptions

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.

Exceptions

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.

Parameters

f	A function declaration of non-zero arity

Returns: A FunctionInterpretation if the function has an interpretation in the model, null otherwise.

Exceptions

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.

See also: NumSorts, SortUniverse

Exceptions

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 .

See also: Sorts

Parameters

s	An uninterpreted sort

Returns: An array of expressions, where each is an element of the universe of s

Exceptions

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;
     }

String toString ( )

inline

Conversion of models to strings.

Returns: A string representation of the model.

Definition at line 286 of file Model.java.

     {
         try
         {
             return Native.modelToString(getContext().nCtx(), getNativeObject());
         } catch (Z3Exception e)
         {
             return "Z3Exception: " + e.getMessage();
         }
     }

Data Structures

Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation