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

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
aA Constant
Returns
An expression if the constant has an interpretation in the model, null otherwise.

Definition at line 36 of file Model.cs.

37  {
38  Contract.Requires(a != null);
39 
40  Context.CheckContextMatch(a);
41  return ConstInterp(a.FuncDecl);
42  }
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Definition: Model.cs:36

◆ ConstInterp() [2/2]

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.

50  {
51  Contract.Requires(f != null);
52 
53  Context.CheckContextMatch(f);
54  if (f.Arity != 0 ||
55  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT)
56  throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
57 
58  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
59  if (n == IntPtr.Zero)
60  return null;
61  else
62  return Expr.Create(Context, n);
63  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

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

206  {
207  Contract.Requires(t != null);
208  Contract.Ensures(Contract.Result<Expr>() != null);
209 
210  IntPtr v = IntPtr.Zero;
211  if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
212  throw new ModelEvaluationFailedException();
213  else
214  return Expr.Create(Context, v);
215  }

◆ Evaluate()

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

Alias for Eval.

Definition at line 220 of file Model.cs.

221  {
222  Contract.Requires(t != null);
223  Contract.Ensures(Contract.Result<Expr>() != null);
224 
225  return Eval(t, completion);
226  }
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Definition: Model.cs:205

◆ FuncInterp()

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.

71  {
72  Contract.Requires(f != null);
73 
74  Context.CheckContextMatch(f);
75 
76  Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));
77 
78  if (f.Arity == 0)
79  {
80  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
81 
82  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
83  {
84  if (n == IntPtr.Zero)
85  return null;
86  else
87  {
88  if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
89  throw new Z3Exception("Argument was not an array constant");
90  IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
91  return FuncInterp(new FuncDecl(Context, fd));
92  }
93  }
94  else
95  {
96  throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
97  }
98  }
99  else
100  {
101  IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
102  if (n == IntPtr.Zero)
103  return null;
104  else
105  return new FuncInterp(Context, n);
106  }
107  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Definition: Model.cs:70

◆ SortUniverse()

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.

264  {
265  Contract.Requires(s != null);
266  Contract.Ensures(Contract.Result<Expr[]>() != null);
267 
268  ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
269  return av.ToExprArray();
270  }

◆ ToString()

override string ToString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 276 of file Model.cs.

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

Property Documentation

◆ ConstDecls

FuncDecl [] ConstDecls
get

The function declarations of the constants in the model.

Definition at line 121 of file Model.cs.

121  {
122  get
123  {
124  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
125 
126  uint n = NumConsts;
127  FuncDecl[] res = new FuncDecl[n];
128  for (uint i = 0; i < n; i++)
129  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
130  return res;
131  }
132  }
uint NumConsts
The number of constants that have an interpretation in the model.
Definition: Model.cs:113

◆ Decls

FuncDecl [] Decls
get

All symbols that have an interpretation in the model.

Definition at line 163 of file Model.cs.

163  {
164  get
165  {
166  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
167 
168  uint nFuncs = NumFuncs;
169  uint nConsts = NumConsts;
170  uint n = nFuncs + nConsts;
171  FuncDecl[] res = new FuncDecl[n];
172  for (uint i = 0; i < nConsts; i++)
173  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
174  for (uint i = 0; i < nFuncs; i++)
175  res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
176  return res;
177  }
178  }
uint NumConsts
The number of constants that have an interpretation in the model.
Definition: Model.cs:113
uint NumFuncs
The number of function interpretations in the model.
Definition: Model.cs:138

◆ FuncDecls

FuncDecl [] FuncDecls
get

The function declarations of the function interpretations in the model.

Definition at line 146 of file Model.cs.

146  {
147  get
148  {
149  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
150 
151  uint n = NumFuncs;
152  FuncDecl[] res = new FuncDecl[n];
153  for (uint i = 0; i < n; i++)
154  res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
155  return res;
156  }
157  }
uint NumFuncs
The number of function interpretations in the model.
Definition: Model.cs:138

◆ NumConsts

uint NumConsts
get

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

Definition at line 113 of file Model.cs.

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

◆ NumFuncs

uint NumFuncs
get

The number of function interpretations in the model.

Definition at line 138 of file Model.cs.

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

◆ NumSorts

uint NumSorts
get

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

Definition at line 231 of file Model.cs.

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

244  {
245  get
246  {
247  Contract.Ensures(Contract.Result<Sort[]>() != null);
248 
249  uint n = NumSorts;
250  Sort[] res = new Sort[n];
251  for (uint i = 0; i < n; i++)
252  res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
253  return res;
254  }
255  }
uint NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
Definition: Model.cs:231