RetroSearch Browse

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

ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More...

Inheritance diagram for ApplyResult:

Detailed Description

ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.

Definition at line 29 of file ApplyResult.cs.

Member Function Documentation ◆ ToString() override string ToString ( ) inline

A string representation of the ApplyResult.

Definition at line 58 of file ApplyResult.cs.

60 return

Native.Z3_apply_result_to_string(

.nCtx, NativeObject);

Context Context

Access Context object

Property Documentation ◆ NumSubgoals ◆ Subgoals

Retrieves the subgoals from the ApplyResult.

Definition at line 42 of file ApplyResult.cs.

48

Goal[] res =

new

Goal[n];

49 for

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

50

res[i] =

new

Goal(

, Native.Z3_apply_result_get_subgoal(

.nCtx, NativeObject, i));

uint NumSubgoals

The number of Subgoals.

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