Model Class Reference

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 ()
Package Functions
	Model (Context ctx, long obj) throws Z3Exception
void	incRef (long o) throws Z3Exception
void	decRef (long o) throws Z3Exception

---

Detailed Description

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

Definition at line 25 of file Model.java.

---

Constructor & Destructor Documentation

Model	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 297 of file Model.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

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.

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

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.

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