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

Inheritance diagram for Model:

Data Structures
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. More...

Expr	ConstInterp (FuncDecl f)
	Retrieves the interpretation (the assignment) of f in the model. More...

FuncInterp	FuncInterp (FuncDecl f)
	Retrieves the interpretation (the assignment) of a non-constant f in the model. More...

Expr	Eval (Expr t, bool completion=false)
	Evaluates the expression t in the current model. More...

Expr	Evaluate (Expr t, bool completion=false)
	Alias for `Eval`. More...

double	Double (Expr t)
	Evaluate expression to a double, assuming it is a numeral already. More...

Expr[]	SortUniverse (Sort s)
	The finite set of distinct values that represent the interpretation for sort s . More...

override string	ToString ()
	Conversion of models to strings. More...

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
uint	NumConsts `[get]`
	The number of constants that have an interpretation in the model. More...

FuncDecl[]	ConstDecls `[get]`
	The function declarations of the constants in the model. More...

IEnumerable< KeyValuePair< FuncDecl, Expr > >	Consts `[get]`
	Enumerate constants in model. More...

uint	NumFuncs `[get]`
	The number of function interpretations in the model. More...

FuncDecl[]	FuncDecls `[get]`
	The function declarations of the function interpretations in the model. More...

FuncDecl[]	Decls `[get]`
	All symbols that have an interpretation in the model. More...

uint	NumSorts `[get]`
	The number of uninterpreted sorts that the model has an interpretation for. More...

Sort[]	Sorts `[get]`
	The uninterpreted sorts that the model has an interpretation for. More...

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object More...

Detailed Description

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

Definition at line 29 of file Model.cs.

Member Function Documentation

◆ ConstInterp() [1/2]

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

Definition at line 36 of file Model.cs.

         {
             Debug.Assert(a != null);
  
             Context.CheckContextMatch(a);
             return ConstInterp(a.FuncDecl);
         }

◆ ConstInterp() [2/2]

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

Definition at line 49 of file Model.cs.

         {
             Debug.Assert(f != null);
  
             Context.CheckContextMatch(f);
             if (f.Arity != 0) 
                 throw new Z3Exception("Non-zero arity functions 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);
         }

◆ Double()

double Double ( Expr t )

inline

Evaluate expression to a double, assuming it is a numeral already.

Definition at line 244 of file Model.cs.

                                      {
             using var r = Eval(t, true);
             return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
         }

◆ Eval()

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

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.

Definition at line 220 of file Model.cs.

         {
             Debug.Assert(t != null);
  
             IntPtr v = IntPtr.Zero;
             if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0)
                 throw new ModelEvaluationFailedException();
             else
                 return Expr.Create(Context, v);
         }

Referenced by Model.Double(), and Model.Evaluate().

◆ Evaluate()

Expr Evaluate	(	Expr	t,
		bool	completion = `false`
	)

inline

Alias for Eval.

Definition at line 234 of file Model.cs.

         {
             Debug.Assert(t != null);
  
             return Eval(t, completion);
         }

◆ FuncInterp()

FuncInterp FuncInterp ( 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.

Definition at line 69 of file Model.cs.

         {
             Debug.Assert(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);
                         using var decl = new FuncDecl(Context, fd);
                         return FuncInterp(decl);
                     }
                 }
                 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);
             }
         }

◆ SortUniverse()

Expr [] SortUniverse ( Sort s )

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

Definition at line 283 of file Model.cs.

         {
             Debug.Assert(s != null);
  
             using ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));            
             return av.ToExprArray();
         }

◆ ToString()

override string ToString ( )

inline

Conversion of models to strings.

Returns: A string representation of the model.

Definition at line 295 of file Model.cs.

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

Property Documentation

◆ ConstDecls

FuncDecl [] ConstDecls

get

The function declarations of the constants in the model.

Definition at line 120 of file Model.cs.

         {
             get
             {
  
                 uint n = NumConsts;
                 FuncDecl[] res = new FuncDecl[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

◆ Consts

IEnumerable<KeyValuePair<FuncDecl, Expr> > Consts

get

Enumerate constants in model.

Definition at line 136 of file Model.cs.

         {
             get
             {
                 uint nc = NumConsts;
                 for (uint i = 0; i < nc; ++i)
                 {
                     var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
                     IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
                     if (n == IntPtr.Zero) continue;
                     yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
                 }
             }
         }

◆ Decls

FuncDecl [] Decls

get

All symbols that have an interpretation in the model.

Definition at line 178 of file Model.cs.

         {
             get
             {
  
                 uint nFuncs = NumFuncs;
                 uint nConsts = NumConsts;
                 uint n = nFuncs + nConsts;
                 FuncDecl[] res = new FuncDecl[n];
                 for (uint i = 0; i < nConsts; i++)
                     res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
                 for (uint i = 0; i < nFuncs; i++)
                     res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));                
                 return res;
             }
         }

◆ FuncDecls

FuncDecl [] FuncDecls

get

The function declarations of the function interpretations in the model.

Definition at line 162 of file Model.cs.

         {
             get
             {
  
                 uint n = NumFuncs;
                 FuncDecl[] res = new FuncDecl[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

◆ NumConsts

uint NumConsts

get

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

Definition at line 112 of file Model.cs.

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

◆ NumFuncs

uint NumFuncs

get

The number of function interpretations in the model.

Definition at line 154 of file Model.cs.

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

◆ NumSorts

uint NumSorts

get

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

Definition at line 252 of file Model.cs.

252 { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }

◆ Sorts

Sort [] Sorts

get

The uninterpreted sorts that the model has an interpretation for.

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: NumSorts, SortUniverse

Definition at line 264 of file Model.cs.

         {
             get
             {
  
                 uint n = NumSorts;
                 Sort[] res = new Sort[n];
                 for (uint i = 0; i < n; i++)
                     res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
                 return res;
             }
         }

Data Structures

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ ConstInterp() [1/2]

◆ ConstInterp() [2/2]

◆ Double()

◆ Eval()

◆ Evaluate()

◆ FuncInterp()

◆ SortUniverse()

◆ ToString()

Property Documentation

◆ ConstDecls

◆ Consts

◆ Decls

◆ FuncDecls

◆ NumConsts

◆ NumFuncs

◆ NumSorts

◆ Sorts