21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Requires(a != null);
51 Contract.Requires(f != null);
56 throw new Z3Exception(
"Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
72 Contract.Requires(f != null);
89 throw new Z3Exception(
"Argument was not an array constant");
96 throw new Z3Exception(
"Constant functions do not have a function interpretation; use ConstInterp");
102 if (n == IntPtr.Zero)
112 public uint NumConsts
124 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
128 for (uint i = 0; i < n; i++)
149 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
153 for (uint i = 0; i < n; i++)
166 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
168 uint nFuncs = NumFuncs;
169 uint nConsts = NumConsts;
170 uint n = nFuncs + nConsts;
172 for (uint i = 0; i < nConsts; i++)
174 for (uint i = 0; i < nFuncs; i++)
207 Contract.Requires(t != null);
208 Contract.Ensures(Contract.Result<
Expr>() != null);
210 IntPtr v = IntPtr.Zero;
222 Contract.Requires(t != null);
223 Contract.Ensures(Contract.Result<
Expr>() != null);
225 return Eval(t, completion);
247 Contract.Ensures(Contract.Result<
Sort[]>() != null);
251 for (uint i = 0; i < n; i++)
265 Contract.Requires(s != null);
266 Contract.Ensures(Contract.Result<
Expr[]>() != null);
285 Contract.Requires(ctx != null);
290 public DecRefQueue() : base() { }
291 public DecRefQueue(uint move_limit) : base(move_limit) { }
292 internal override void IncRef(
Context ctx, IntPtr obj)
297 internal override void DecRef(
Context ctx, IntPtr obj)
303 internal override void IncRef(IntPtr o)
309 internal override void DecRef(IntPtr o)
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
static void Z3_model_inc_ref(Z3_context a0, Z3_model a1)
A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model...
static Z3_ast_vector Z3_model_get_sort_universe(Z3_context a0, Z3_model a1, Z3_sort a2)
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
static uint Z3_model_get_num_sorts(Z3_context a0, Z3_model a1)
Expr ConstInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of f in the model.
static void Z3_model_dec_ref(Z3_context a0, Z3_model a1)
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
static uint Z3_model_get_num_consts(Z3_context a0, Z3_model a1)
Expr[] SortUniverse(Sort s)
The finite set of distinct values that represent the interpretation for sort s .
static int Z3_model_eval(Z3_context a0, Z3_model a1, Z3_ast a2, int a3, [In, Out] ref Z3_ast a4)
static Z3_func_decl Z3_model_get_func_decl(Z3_context a0, Z3_model a1, uint a2)
uint Arity
The arity of the function declaration
static Z3_func_interp Z3_model_get_func_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static int Z3_is_as_array(Z3_context a0, Z3_ast a1)
static Z3_ast Z3_model_get_const_interp(Z3_context a0, Z3_model a1, Z3_func_decl a2)
static Z3_func_decl Z3_get_as_array_func_decl(Z3_context a0, Z3_ast a1)
static uint Z3_model_get_num_funcs(Z3_context a0, Z3_model a1)
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
static Z3_sort Z3_model_get_sort(Z3_context a0, Z3_model a1, uint a2)
IDecRefQueue Model_DRQ
Model DRQ
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Expr Evaluate(Expr t, bool completion=false)
Alias for Eval.
static Z3_func_decl Z3_model_get_const_decl(Z3_context a0, Z3_model a1, uint a2)
A Model contains interpretations (assignments) of constants and functions.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
static Z3_sort Z3_get_range(Z3_context a0, Z3_func_decl a1)
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
override string ToString()
Conversion of models to strings.
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
ModelEvaluationFailedException()
An exception that is thrown when model evaluation fails.
static string Z3_model_to_string(Z3_context a0, Z3_model a1)
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...