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

Z3: FuncInterp Class Reference

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.
More...

class Entry An Entry object represents an element in the finite map used to encode a function interpretation. More...
override string ToString () A string representation of the function interpretation. More...
void Dispose () Disposes of the underlying native Z3 object. More...

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

Definition at line 29 of file FuncInterp.cs.

◆ ToString() override string ToString ( ) inline

A string representation of the function interpretation.

Definition at line 151 of file FuncInterp.cs.

158 if

(n > 1) res +=

"["

;

159

Expr[] args = e.Args;

160 for

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

162 if

(i != 0) res +=

", "

;

165 if

(n > 1) res +=

"]"

;

166

res +=

" -> "

+ e.Value +

", "

;

168

res +=

"else -> "

Else

;

Entry[] Entries

The entries in the function interpretation

Expr Else

The (symbolic) ‘else’ value of the function interpretation.

◆ Arity

The arity of the function interpretation

Definition at line 143 of file FuncInterp.cs.

145 get

{

return

Native.Z3_func_interp_get_arity(

Context

.nCtx, NativeObject); }

Context Context

Access Context object

◆ Else ◆ Entries

The entries in the function interpretation

Definition at line 115 of file FuncInterp.cs.

121

Entry[] res =

new

Entry[n];

122 for

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

123

res[i] =

new

Entry(

Context

, Native.Z3_func_interp_get_entry(

Context

.nCtx, NativeObject, i));

uint NumEntries

The number of entries in the function interpretation.

Referenced by FuncInterp.ToString().

◆ NumEntries

The number of entries in the function interpretation.

Definition at line 107 of file FuncInterp.cs.

109 get

{

return

Native.Z3_func_interp_get_num_entries(

Context

.nCtx, NativeObject); }

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