Inheritance diagram for Model:

Data Structures
class	ModelEvaluationFailedException

Public Member Functions
Expr	getConstInterp (Expr a)

Expr	getConstInterp (FuncDecl f)

FuncInterp	getFuncInterp (FuncDecl f)

int	getNumConsts ()

FuncDecl[]	getConstDecls ()

int	getNumFuncs ()

FuncDecl[]	getFuncDecls ()

FuncDecl[]	getDecls ()

Expr	eval (Expr t, boolean completion)

Expr	evaluate (Expr t, boolean completion)

int	getNumSorts ()

Sort[]	getSorts ()

Expr[]	getSortUniverse (Sort s)

String	toString ()

Public Member Functions inherited from Z3Object
void	dispose ()

Public Member Functions inherited from IDisposable
void	dispose ()

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

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
	)

inline

Evaluates the expression

t

in the current model. Remarks: 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
	)

inline

Alias for

Eval

.

Exceptions

Z3Exception

Definition at line 226 of file Model.java.

     {
         return eval(t, completion);
     }

FuncDecl [] getConstDecls ( )

inline

The function declarations of the constants in the model.

Exceptions

Z3Exception

Definition at line 130 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 )

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 36 of file Model.java.

     {
         getContext().checkContextMatch(a);
         return getConstInterp(a.getFuncDecl());
     }

Expr getConstInterp ( FuncDecl f )

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

inline

All symbols that have an interpretation in the model.

Exceptions

Z3Exception

Definition at line 168 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 ( )

inline

The function declarations of the function interpretations in the model.

Exceptions

Z3Exception

Definition at line 153 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 )

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

inline

The number of constants that have an interpretation in the model.

Definition at line 120 of file Model.java.

Referenced by Model.getConstDecls(), and Model.getDecls().

     {
         return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
     }

int getNumFuncs ( )

inline

The number of function interpretations in the model.

Definition at line 143 of file Model.java.

Referenced by Model.getDecls(), and Model.getFuncDecls().

     {
         return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
     }

int getNumSorts ( )

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

inline

The uninterpreted sorts that the model has an interpretation for. Remarks: 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: getNumSorts; getSortUniverse

Exceptions

Z3Exception

Definition at line 251 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 )

inline

The finite set of distinct values that represent the interpretation for sort

s

.

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 271 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 288 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