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

Z3: Goal Class Reference

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More...

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Definition at line 31 of file Goal.cs.

Alias for Assert.

Definition at line 96 of file Goal.cs.

void Assert(params BoolExpr[] constraints)

Adds the constraints to the given goal.

Goal to BoolExpr conversion.

Returns

A string representation of the Goal.

Definition at line 237 of file Goal.cs.

BoolExpr MkTrue()

The true Term.

BoolExpr MkAnd(params BoolExpr[] t)

Create an expression representing t[0] and t[1] and ....

uint Size

The number of formulas in the goal.

BoolExpr[] Formulas

The formulas in the goal.

Context Context

Access Context object

Adds the constraints to the given goal.

Definition at line 80 of file Goal.cs.

Debug.Assert(constraints !=

);

Debug.Assert(constraints.All(c => c !=

));

.CheckContextMatch<BoolExpr>(constraints);

(BoolExpr c

constraints)

Debug.Assert(c !=

);

Native.Z3_goal_assert(

.nCtx, NativeObject, c.NativeObject);

Referenced by Goal.Add(), and Goal.Translate().

Convert a model for the goal into a model of the original goal from which this goal was derived.

Returns

A model for g

Definition at line 181 of file Goal.cs.

(

, Native.Z3_goal_convert_model(

.nCtx, NativeObject, m.NativeObject));

(

, Native.Z3_goal_convert_model(

.nCtx, NativeObject, IntPtr.Zero));

Erases all formulas from the given goal.

Definition at line 123 of file Goal.cs.

Native.Z3_goal_reset(

.nCtx, NativeObject);

Simplifies the goal.

Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 204 of file Goal.cs.

ApplyResult res = t.

(

, p);

(res.NumSubgoals == 0)

Z3Exception(

);

res.Subgoals[0];

Tactic MkTactic(string name)

Creates a new Tactic.

ApplyResult Apply(Goal g, Params p=null)

Execute the tactic over the goal.

Goal to DIMACS formatted string conversion.

Returns

A string representation of the Goal.

Definition at line 228 of file Goal.cs.

Native.Z3_goal_to_dimacs_string(

.nCtx, NativeObject, (

)(include_names ? 1 : 0));

Goal to string conversion.

Returns

A string representation of the Goal.

Definition at line 219 of file Goal.cs.

Native.Z3_goal_to_string(

.nCtx, NativeObject);

Translates (copies) the Goal to the target Context ctx .

Definition at line 193 of file Goal.cs.

Debug.Assert(ctx !=

);

Goal(ctx, Native.Z3_goal_translate(

.nCtx, NativeObject, ctx.nCtx));

The depth of the goal.

This tracks how many transformations were applied to it.

Definition at line 115 of file Goal.cs.

{

Native.Z3_goal_depth(

.nCtx, NativeObject); }

The formulas in the goal.

Definition at line 139 of file Goal.cs.

BoolExpr[] res =

BoolExpr[n];

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

res[i] = (BoolExpr)Expr.Create(

, Native.Z3_goal_formula(

.nCtx, NativeObject, i));

Referenced by Goal.AsBoolExpr().

Indicates whether the goal contains ‘false’.

Definition at line 104 of file Goal.cs.

{

Native.Z3_goal_inconsistent(

.nCtx, NativeObject) != 0; }

Indicates whether the goal is empty, and it is precise or the product of an under approximation.

Definition at line 163 of file Goal.cs.

{

Native.Z3_goal_is_decided_sat(

.nCtx, NativeObject) != 0; }

Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximation.

Definition at line 171 of file Goal.cs.

{

Native.Z3_goal_is_decided_unsat(

.nCtx, NativeObject) != 0; }

Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).

Definition at line 72 of file Goal.cs.

Z3_goal_prec Precision

The precision of the goal.

Z3_goal_prec

Z3 custom error handler (See Z3_set_error_handler).

Indicates whether the goal is an over-approximation.

Definition at line 64 of file Goal.cs.

Indicates whether the goal is precise.

Definition at line 49 of file Goal.cs.

Indicates whether the goal is an under-approximation.

Definition at line 56 of file Goal.cs.

The number of formulas, subformulas and terms in the goal.

Definition at line 155 of file Goal.cs.

{

Native.Z3_goal_num_exprs(

.nCtx, NativeObject); }

The precision of the goal.

Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Definition at line 41 of file Goal.cs.

The number of formulas in the goal.

Definition at line 131 of file Goal.cs.

{

Native.Z3_goal_size(

.nCtx, NativeObject); }

Referenced by Goal.AsBoolExpr().

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