Model Class Reference

Inheritance diagram for Model:

Data Structures
class	ModelEvaluationFailedException

Public Member Functions
int	getNumConsts ()
FuncDecl<?>[]	getConstDecls ()
int	getNumFuncs ()
FuncDecl<?>[]	getFuncDecls ()
FuncDecl<?>[]	getDecls ()
int	getNumSorts ()
Sort[]	getSorts ()
String	toString ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

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

Definition at line 28 of file Model.java.

Member Function Documentation

getConstDecls()

FuncDecl<?> [] getConstDecls ( )

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

getDecls()

FuncDecl<?> [] getDecls ( )

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

getFuncDecls()

FuncDecl<?> [] getFuncDecls ( )

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

getNumConsts()

int getNumConsts ( )

inline

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

Definition at line 119 of file Model.java.

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

getNumFuncs()

int getNumFuncs ( )

inline

The number of function interpretations in the model.

Definition at line 142 of file Model.java.

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

getNumSorts()

int getNumSorts ( )

inline

The number of uninterpreted sorts that the model has an interpretation for.

Definition at line 235 of file Model.java.

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

getSorts()

Sort [] getSorts ( )

inline

The uninterpreted sorts that the model has an interpretation for. Remarks: Z3 also provides an interpretation 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(R s)

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

toString()

String toString ( )

inline

Conversion of models to strings.

Returns

A string representation of the model.

Definition at line 285 of file Model.java.

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