Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Properties
Model Class Reference

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

+ Inheritance diagram for Model:

Data Structures

class  DecRefQueue
class  ModelEvaluationFailedException
 A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. More...

Public Member Functions

Expr ConstInterp (Expr a)
 Retrieves the interpretation (the assignment) of a in the model.
Expr ConstInterp (FuncDecl f)
 Retrieves the interpretation (the assignment) of f in the model.
FuncInterp FuncInterp (FuncDecl f)
 Retrieves the interpretation (the assignment) of a non-constant f in the model.
Expr Eval (Expr t, bool completion=false)
 Evaluates the expression t in the current model.
Expr Evaluate (Expr t, bool completion=false)
 Alias for Eval.
Expr[] SortUniverse (Sort s)
 The finite set of distinct values that represent the interpretation for sort s .
override string ToString ()
 Conversion of models to strings.

Properties

uint NumConsts [get]
 The number of constants that have an interpretation in the model.
FuncDecl[] ConstDecls [get]
 The function declarations of the constants in the model.
uint NumFuncs [get]
 The number of function interpretations in the model.
FuncDecl[] FuncDecls [get]
 The function declarations of the function interpretations in the model.
FuncDecl[] Decls [get]
 All symbols that have an interpretation in the model.
uint NumSorts [get]
 The number of uninterpreted sorts that the model has an interpretation for.
Sort[] Sorts [get]
 The uninterpreted sorts that the model has an interpretation for.

Detailed Description

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

Definition at line 29 of file Model.cs.


Member Function Documentation

Expr ConstInterp ( Expr  a) [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.

Definition at line 36 of file Model.cs.

        {
            Contract.Requires(a != null);

            Context.CheckContextMatch(a);
            return ConstInterp(a.FuncDecl);
        }
Expr ConstInterp ( FuncDecl  f) [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.

Definition at line 49 of file Model.cs.

        {
            Contract.Requires(f != null);

            Context.CheckContextMatch(f);
            if (f.Arity != 0 ||
                Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT)
                throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");

            IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
            if (n == IntPtr.Zero)
                return null;
            else
                return Expr.Create(Context, n);
        }
Expr Eval ( Expr  t,
bool  completion = false 
) [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.

Definition at line 205 of file Model.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            IntPtr v = IntPtr.Zero;
            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
                throw new ModelEvaluationFailedException();
            else
                return Expr.Create(Context, v);
        }
Expr Evaluate ( Expr  t,
bool  completion = false 
) [inline]

Alias for Eval.

Definition at line 220 of file Model.cs.

        {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<Expr>() != null);

            return Eval(t, completion);
        }
FuncInterp FuncInterp ( FuncDecl  f) [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.

Definition at line 70 of file Model.cs.

        {
            Contract.Requires(f != null);

            Context.CheckContextMatch(f);

            Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));

            if (f.Arity == 0)
            {
                IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);

                if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
                {
                    if (n == IntPtr.Zero)
                        return null;
                    else
                    {
                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
                            throw new Z3Exception("Argument was not an array constant");
                        IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
                        return FuncInterp(new FuncDecl(Context, fd));
                    }
                }
                else
                {
                    throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
                }
            }
            else
            {
                IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
                if (n == IntPtr.Zero)
                    return null;
                else
                    return new FuncInterp(Context, n);
            }
        }
Expr [] SortUniverse ( Sort  s) [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

Definition at line 263 of file Model.cs.

        {
            Contract.Requires(s != null);
            Contract.Ensures(Contract.Result<Expr[]>() != null);

            ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
            uint n = nUniv.Size;
            Expr[] res = new Expr[n];
            for (uint i = 0; i < n; i++)
                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
            return res;
        }
override string ToString ( ) [inline]

Conversion of models to strings.

Returns:
A string representation of the model.

Definition at line 280 of file Model.cs.

        {
            return Native.Z3_model_to_string(Context.nCtx, NativeObject);
        }

Property Documentation

FuncDecl [] ConstDecls [get]

The function declarations of the constants in the model.

Definition at line 121 of file Model.cs.

FuncDecl [] Decls [get]

All symbols that have an interpretation in the model.

Definition at line 163 of file Model.cs.

FuncDecl [] FuncDecls [get]

The function declarations of the function interpretations in the model.

Definition at line 146 of file Model.cs.

uint NumConsts [get]

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

Definition at line 113 of file Model.cs.

uint NumFuncs [get]

The number of function interpretations in the model.

Definition at line 138 of file Model.cs.

uint NumSorts [get]

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

Definition at line 231 of file Model.cs.

Sort [] Sorts [get]

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

Definition at line 244 of file Model.cs.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines