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

Z3: Tactic Class Reference

Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. More...

Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.

Definition at line 31 of file Tactic.cs.

◆ Apply()

Execute the tactic over the goal.

Definition at line 58 of file Tactic.cs.

60

Debug.Assert(g !=

null

);

64 return new

ApplyResult(

, Native.Z3_tactic_apply(

.nCtx, NativeObject, g.NativeObject));

68 return new

ApplyResult(

, Native.Z3_tactic_apply_ex(

.nCtx, NativeObject, g.NativeObject, p.NativeObject));

Context Context

Access Context object

Referenced by Goal.Simplify().

◆ Help

A string containing a description of parameters accepted by the tactic.

Definition at line 36 of file Tactic.cs.

41 return

Native.Z3_tactic_get_help(

.nCtx, NativeObject);

◆ ParameterDescriptions

Retrieves parameter descriptions for Tactics.

Definition at line 49 of file Tactic.cs.

51 get

{

return new

ParamDescrs(

, Native.Z3_tactic_get_param_descrs(

.nCtx, NativeObject)); }

◆ Solver

Creates a solver that is implemented using the given tactic.

See also: Context.MkSolver(Tactic)

Definition at line 89 of file Tactic.cs.

Solver MkSolver(Symbol logic=null)

Creates a new (incremental) solver.

◆ this[Goal g]

Apply the tactic to a goal.

Definition at line 75 of file Tactic.cs.

79

Debug.Assert(g !=

null

);

ApplyResult Apply(Goal g, Params p=null)

Execute the tactic over the goal.

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