Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_native_model.html below:

Z3: NativeModel Class Reference

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

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

Definition at line 36 of file NativeModel.cs.

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.

(Native.Z3_get_arity(ntvContext.nCtx, f) != 0)

Z3Exception(

);

Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);

Retrieves the interpretation (the assignment) of a in the model.

Parameters

Returns

An expression if the constant has an interpretation in the model, null otherwise.

Disposes of the underlying native Z3 object.

Definition at line 368 of file NativeModel.cs.

(NativeObject != IntPtr.Zero)

Native.Z3_model_dec_ref(ntvContext.nCtx, NativeObject);

NativeObject = IntPtr.Zero;

GC.SuppressFinalize(

);

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

Definition at line 232 of file NativeModel.cs.

var r =

(t,

);

Native.Z3_get_numeral_double(ntvContext.nCtx, r);

Z3_ast Eval(Z3_ast t, bool completion=false)

Evaluates the expression t in the current model.

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;

(Native.Z3_model_eval(ntvContext.nCtx, NativeObject, t, (

)(completion ? 1 : 0), ref v) == (

)0)

ModelEvaluationFailedException();

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

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.

(Native.Z3_get_arity(ntvContext.nCtx, f) == 0)

IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f);

(Native.Z3_is_as_array(ntvContext.nCtx, n) == 0)

Z3Exception(

);

var fd = Native.Z3_get_as_array_func_decl(ntvContext.nCtx, n);

NativeFuncInterp(ntvContext,

, f, fd);

Z3Exception(

);

IntPtr n = Native.Z3_model_get_func_interp(ntvContext.nCtx, NativeObject, f);

NativeFuncInterp(ntvContext,

, f, n);

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

Conversion of models to strings.

Returns

A string representation of the model.

Definition at line 339 of file NativeModel.cs.

Native.Z3_model_to_string(ntvContext.nCtx, NativeObject);

Convert the interpretation of t into a sequence of array updates

Parameters

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 =

(t,

);

var updates =

Dictionary<Z3_ast, Z3_ast>();

result =

ArrayValue();

result.Else = ntvContext.GetAppArg(r, 0);

result.Updates = updates.ToArray();

result.Domain = updates.Keys.ToArray();

result.Range = updates.Values.ToArray();

Debug.Assert(ntvContext.

(r) == 3);

updates[ntvContext.GetAppArg(r, 1)] = ntvContext.GetAppArg(r, 2);

r = ntvContext.GetAppArg(r, 0);

Z3_ast_kind GetAstKind(Z3_ast ast)

Get the AST kind from IntPtr

uint GetNumArgs(Z3_app app)

Return number of arguments for app

Z3_decl_kind GetDeclKind(Z3_func_decl decl)

Get the Decl kind from IntPtr

Z3_func_decl GetAppDecl(Z3_ast ast)

Get App Decl from IntPtr

Z3_ast_kind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

Z3_decl_kind

The different kinds of interpreted function kinds.

System.IntPtr Z3_func_decl

The function declarations of the constants in the model.

Definition at line 113 of file NativeModel.cs.

(uint i = 0; i < n; i++)

res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);

uint NumConsts

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

Enumerate constants in model.

Definition at line 130 of file NativeModel.cs.

(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);

(n == IntPtr.Zero)

;

yield

KeyValuePair<Z3_func_decl, Z3_ast>(f, n);

All symbols that have an interpretation in the model.

Definition at line 172 of file NativeModel.cs.

uint n = nFuncs + nConsts;

(uint i = 0; i < nConsts; i++)

res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i);

(uint i = 0; i < nFuncs; i++)

res[nConsts + i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i);

uint NumFuncs

The number of function interpretations in the model.

The function declarations of the function interpretations in the model.

Definition at line 156 of file NativeModel.cs.

(uint i = 0; i < n; i++)

res[i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i);

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

Definition at line 104 of file NativeModel.cs.

{

Native.Z3_model_get_num_consts(ntvContext.nCtx, NativeObject); }

The number of function interpretations in the model.

Definition at line 148 of file NativeModel.cs.

{

Native.Z3_model_get_num_funcs(ntvContext.nCtx, NativeObject); }

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

Definition at line 309 of file NativeModel.cs.

{

{

Native.Z3_model_get_num_sorts(ntvContext.nCtx, NativeObject); } }

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.

(uint i = 0; i < n; i++)

res[i] = Native.Z3_model_get_sort(ntvContext.nCtx, NativeObject, i);

uint NumSorts

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

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4