Tactics, Goals, Probes, and Parameters for goal-based solving
ApplyResult represents the result of applying a tactic to a goal.
NumSubgoals returns the number of subgoals in the result.
String returns the string representation of the apply result.
Subgoal returns the i-th subgoal.
Context methods (receiver omitted for clarity)
GetProbeDescr returns a description of the probe with the given name.
GetTacticDescr returns a description of the tactic with the given name.
MkGoal creates a new goal.
MkParams creates a new parameter set.
MkProbe creates a probe with the given name.
MkTactic creates a tactic with the given name.
NewSolverFromTactic creates a solver from the given tactic. The solver uses the tactic to solve goals.
ParOr creates a tactic that applies the given tactics in parallel.
ProbeConst creates a probe that always evaluates to the given value.
TacticCond creates a conditional tactic: if p then t1 else t2.
TacticFail creates a tactic that always fails.
TacticFailIf creates a tactic that fails if the probe p evaluates to false.
TacticFailIfNotDecided creates a tactic that fails if the goal is not trivially satisfiable (empty) or trivially unsatisfiable (contains false).
TacticSkip creates a tactic that always succeeds.
When creates a conditional tactic that applies t only if probe p evaluates to true.
Goal represents a set of formulas that can be solved or transformed.
Assert adds a constraint to the goal.
ConvertModel converts a model from the original goal into a model for this goal. Use this when a tactic has transformed the goal and you need a model for the original.
Depth returns the depth of the goal. It tracks how many times the goal was transformed by a tactic.
Formula returns the i-th formula in the goal.
IsDecidedSat returns true if the goal is decided to be satisfiable.
IsDecidedUnsat returns true if the goal is decided to be unsatisfiable.
IsInconsistent returns true if the goal contains the formula false.
NumExprs returns the number of expressions in the goal.
Precision returns the precision of the goal as a uint. Possible values: 0 = precise, 1 = under-approximation, 2 = over-approximation, 3 = under+over.
Reset removes all formulas from the goal.
Size returns the number of formulas in the goal.
String returns the string representation of the goal.
ToDimacsString converts the goal to a string in DIMACS format. If includeNames is true, formula names are included as comments.
Translate creates a copy of the goal in the target context.
Params represents a parameter set.
SetBool sets a Boolean parameter.
SetDouble sets a double parameter.
SetSymbol sets a symbol parameter.
SetUint sets an unsigned integer parameter.
String returns the string representation of the parameters.
Probe represents a probe for checking properties of goals.
ProbeAnd creates a probe that is the conjunction of p1 and p2.
Apply evaluates the probe on a goal.
ProbeEq creates a probe that evaluates to true if p1 == p2.
ProbeGe creates a probe that evaluates to true if p1 >= p2.
ProbeGt creates a probe that evaluates to true if p1 > p2.
ProbeLe creates a probe that evaluates to true if p1 <= p2.
ProbeLt creates a probe that evaluates to true if p1 < p2.
ProbeNot creates a probe that is the negation of p.
ProbeOr creates a probe that is the disjunction of p1 and p2.
Tactic represents a Z3 tactic for transforming goals.
AndThen creates a tactic that applies t1 and then t2.
Apply applies the tactic to a goal.
ApplyEx applies the tactic to a goal with the given parameters.
GetHelp returns help information for the tactic.
GetParamDescrs returns parameter descriptions for the tactic.
OrElse creates a tactic that applies t1, and if it fails, applies t2.
ParAndThen creates a tactic that applies t to a goal and then t2 to every subgoal produced by t, processing subgoals in parallel.
Repeat creates a tactic that applies t repeatedly (at most max times).
TryFor returns a tactic that applies t for at most ms milliseconds. If t does not terminate in ms milliseconds, then it fails.
UsingParams returns a tactic that applies t using the given parameters.