RetroSearch Browse

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_model.html below:

Z3: Model Class Reference

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

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

Definition at line 29 of file Model.cs.

◆ ConstInterp() [1/2]

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.

Definition at line 36 of file Model.cs.

38

Debug.Assert(a !=

null

);

Expr ConstInterp(Expr a)

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

Context Context

Access Context object

◆ ConstInterp() [2/2]

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.

51

Debug.Assert(f !=

null

);

55 throw new

Z3Exception(

"Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp."

);

57

IntPtr n = Native.Z3_model_get_const_interp(

Context

.nCtx, NativeObject, f.NativeObject);

61 return

Expr.Create(

Context

, n);

◆ Double()

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

Definition at line 244 of file Model.cs.

245 using

var r =

Eval

(t,

true

);

246 return

Native.Z3_get_numeral_double(

Context

.nCtx, r.NativeObject);

Expr Eval(Expr t, bool completion=false)

Evaluates the expression t in the current model.

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

222

Debug.Assert(t !=

null

);

224

IntPtr v = IntPtr.Zero;

225 if

(Native.Z3_model_eval(

Context

.nCtx, NativeObject, t.NativeObject, (

byte

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

byte

)0)

226 throw new

ModelEvaluationFailedException();

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

236

Debug.Assert(t !=

null

);

238 return Eval

(t, completion);

◆ FuncInterp()

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.

71

Debug.Assert(f !=

null

);

79

IntPtr n = Native.Z3_model_get_const_interp(

Context

.nCtx, NativeObject, f.NativeObject);

87 if

(Native.Z3_is_as_array(

Context

.nCtx, n) == 0)

88 throw new

Z3Exception(

"Argument was not an array constant"

);

89

IntPtr fd = Native.Z3_get_as_array_func_decl(

Context

.nCtx, n);

90 using

var decl =

new

FuncDecl(

Context

, fd);

96 throw new

Z3Exception(

"Constant functions do not have a function interpretation; use ConstInterp"

);

101

IntPtr n = Native.Z3_model_get_func_interp(

Context

.nCtx, NativeObject, f.NativeObject);

102 if

(n == IntPtr.Zero)

FuncInterp FuncInterp(FuncDecl f)

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

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

◆ SortUniverse()

The finite set of distinct values that represent the interpretation for sort s .

See also: Sorts

Parameters

Returns: An array of expressions, where each is an element of the universe of s

Definition at line 283 of file Model.cs.

285

Debug.Assert(s !=

null

);

287 using

ASTVector av =

new

ASTVector(

Context

, Native.Z3_model_get_sort_universe(

Context

.nCtx, NativeObject, s.NativeObject));

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

297 return

Native.Z3_model_to_string(

Context

.nCtx, NativeObject);

◆ ConstDecls

The function declarations of the constants in the model.

Definition at line 120 of file Model.cs.

126

FuncDecl[] res =

new

FuncDecl[n];

127 for

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

128

res[i] =

new

FuncDecl(

Context

, Native.Z3_model_get_const_decl(

Context

.nCtx, NativeObject, i));

uint NumConsts

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

◆ Consts

Enumerate constants in model.

Definition at line 136 of file Model.cs.

141 for

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

143

var f =

new

FuncDecl(

Context

, Native.Z3_model_get_const_decl(

Context

.nCtx, NativeObject, i));

144

IntPtr n = Native.Z3_model_get_const_interp(

Context

.nCtx, NativeObject, f.NativeObject);

145 if

(n == IntPtr.Zero)

continue

;

146

yield

return new

KeyValuePair<FuncDecl, Expr>(f, Expr.Create(

Context

, n));

◆ Decls

All symbols that have an interpretation in the model.

Definition at line 178 of file Model.cs.

185

uint n = nFuncs + nConsts;

186

FuncDecl[] res =

new

FuncDecl[n];

187 for

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

188

res[i] =

new

FuncDecl(

Context

, Native.Z3_model_get_const_decl(

Context

.nCtx, NativeObject, i));

189 for

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

190

res[nConsts + i] =

new

FuncDecl(

Context

, Native.Z3_model_get_func_decl(

Context

.nCtx, NativeObject, i));

uint NumFuncs

The number of function interpretations in the model.

◆ FuncDecls

The function declarations of the function interpretations in the model.

Definition at line 162 of file Model.cs.

168

FuncDecl[] res =

new

FuncDecl[n];

169 for

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

170

res[i] =

new

FuncDecl(

Context

, Native.Z3_model_get_func_decl(

Context

.nCtx, NativeObject, i));

◆ NumConsts

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

Definition at line 112 of file Model.cs.

114 get

{

return

Native.Z3_model_get_num_consts(

Context

.nCtx, NativeObject); }

◆ NumFuncs

The number of function interpretations in the model.

Definition at line 154 of file Model.cs.

156 get

{

return

Native.Z3_model_get_num_funcs(

Context

.nCtx, NativeObject); }

◆ NumSorts

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

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.

270

Sort[] res =

new

Sort[n];

271 for

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

272

res[i] = Sort.Create(

Context

, Native.Z3_model_get_sort(

Context

.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