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

Inheritance diagram for NativeModel:

Data Structures
class	ArrayValue
	An array value obtained by untangling a model assignment. More...

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

Public Member Functions
Z3_ast	ConstInterp (Z3_ast a)
	Retrieves the interpretation (the assignment) of a in the model. More...

Z3_ast	ConstFuncInterp (Z3_func_decl f)
	Retrieves the interpretation (the assignment) of f in the model. More...

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

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

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

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

bool	TryGetArrayValue (Z3_ast t, out ArrayValue result)
	Convert the interpretation of t into a sequence of array updates More...

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

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

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

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

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

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

Z3_func_decl[]	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...

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

Detailed Description

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

Definition at line 36 of file NativeModel.cs.

Member Function Documentation

◆ ConstFuncInterp()

Z3_ast ConstFuncInterp ( Z3_func_decl 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 51 of file NativeModel.cs.

         {
             if (Native.Z3_get_arity(ntvContext.nCtx, f) != 0)
                 throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
  
             return Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
         }

◆ ConstInterp()

Z3_ast ConstInterp ( Z3_ast a )

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.

◆ Dispose()

void Dispose ( )

inline

Disposes of the underlying native Z3 object.

Definition at line 368 of file NativeModel.cs.

         {
             if (NativeObject != IntPtr.Zero)
             {
                 Native.Z3_model_dec_ref(ntvContext.nCtx, NativeObject);
                 NativeObject = IntPtr.Zero;
             }
             GC.SuppressFinalize(this);
         }

◆ Double()

double Double ( Z3_ast t )

inline

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

Definition at line 232 of file NativeModel.cs.

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

◆ Eval()

Z3_ast Eval	(	Z3_ast	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 214 of file NativeModel.cs.

         {
  
             IntPtr v = IntPtr.Zero;
             if (Native.Z3_model_eval(ntvContext.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0)
                 throw new ModelEvaluationFailedException();
             else
                 return v;
         }

Referenced by NativeModel.Double(), and NativeModel.TryGetArrayValue().

◆ Evaluate()

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

Alias for Eval.

◆ FuncInterp()

NativeFuncInterp FuncInterp ( Z3_func_decl 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 64 of file NativeModel.cs.

         {
             Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ntvContext.nCtx, Native.Z3_get_range(ntvContext.nCtx, f));
  
             if (Native.Z3_get_arity(ntvContext.nCtx, f) == 0)
             {
                 IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);
  
                 if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
                 {
                     if (n == IntPtr.Zero)
                         return null;
                     else
                     {
                         if (Native.Z3_is_as_array(ntvContext.nCtx, n) == 0)
                             throw new Z3Exception("Argument was not an array constant");
                         var fd = Native.Z3_get_as_array_func_decl(ntvContext.nCtx, n);
                         return new NativeFuncInterp(ntvContext, this, f, fd);
                     }
                 }
                 else
                 {
                     throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
                 }
             }
             else
             {
                 IntPtr n = Native.Z3_model_get_func_interp(ntvContext.nCtx, NativeObject, f);
                 if (n == IntPtr.Zero)
                     return null;
                 else
                     return new NativeFuncInterp(ntvContext, this, f, n);
             }
         }

◆ ToString()

override string ToString ( )

inline

Conversion of models to strings.

Returns: A string representation of the model.

Definition at line 339 of file NativeModel.cs.

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

◆ TryGetArrayValue()

bool TryGetArrayValue	(	Z3_ast	t,
		out ArrayValue	result
	)

inline

Convert the interpretation of t into a sequence of array updates

Parameters

t
result

Returns: null if the argument does evaluate to a sequence of stores to an array

Definition at line 272 of file NativeModel.cs.

         {
             var r = Eval(t, true);
             // check that r is a sequence of store over a constant default array.
             var updates = new Dictionary<Z3_ast, Z3_ast>();
             result = null;
             while (true)
             {
                 if (ntvContext.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST)
                     return false;
                 Z3_func_decl f = ntvContext.GetAppDecl(r);
                 var kind = ntvContext.GetDeclKind(f);
                 if (kind == Z3_decl_kind.Z3_OP_CONST_ARRAY)
                 {
                     result = new ArrayValue();
                     result.Else = ntvContext.GetAppArg(r, 0);
                     result.Updates = updates.ToArray();
                     result.Domain = updates.Keys.ToArray();
                     result.Range = updates.Values.ToArray();
                     return true;
                 }
                 else if (kind == Z3_decl_kind.Z3_OP_STORE)
                 {
                     Debug.Assert(ntvContext.GetNumArgs(r) == 3);
                     updates[ntvContext.GetAppArg(r, 1)] = ntvContext.GetAppArg(r, 2);
                     r = ntvContext.GetAppArg(r, 0);
                 }
                 else
                 {
                     return false;
                 }
             }
         }

Property Documentation

◆ ConstDecls

Z3_func_decl [] ConstDecls

get

The function declarations of the constants in the model.

Definition at line 113 of file NativeModel.cs.

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

◆ Consts

IEnumerable<KeyValuePair<Z3_func_decl, Z3_ast> > Consts

get

Enumerate constants in model.

Definition at line 130 of file NativeModel.cs.

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

◆ Decls

Z3_func_decl [] Decls

get

All symbols that have an interpretation in the model.

Definition at line 172 of file NativeModel.cs.

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

◆ FuncDecls

Z3_func_decl [] FuncDecls

get

The function declarations of the function interpretations in the model.

Definition at line 156 of file NativeModel.cs.

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

◆ NumConsts

uint NumConsts

get

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

Definition at line 104 of file NativeModel.cs.

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

◆ NumFuncs

uint NumFuncs

get

The number of function interpretations in the model.

Definition at line 148 of file NativeModel.cs.

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

◆ NumSorts

uint NumSorts

get

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

Definition at line 309 of file NativeModel.cs.

309 { get { return Native.Z3_model_get_num_sorts(ntvContext.nCtx, NativeObject); } }

◆ Sorts

Z3_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

Definition at line 321 of file NativeModel.cs.

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

Data Structures

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ ConstFuncInterp()

◆ ConstInterp()

◆ Dispose()

◆ Double()

◆ Eval()

◆ Evaluate()

◆ FuncInterp()

◆ ToString()

◆ TryGetArrayValue()

Property Documentation

◆ ConstDecls

◆ Consts

◆ Decls

◆ FuncDecls

◆ NumConsts

◆ NumFuncs

◆ NumSorts

◆ Sorts