Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Package Functions
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:
tAn expression
completionWhen 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:
aA 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:
fA 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:
fA 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:
sAn 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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines