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)
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.
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.
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.
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.
NumExprs returns the number of expressions in the goal.
Reset removes all formulas from the goal.
Size returns the number of formulas in the goal.
String returns the string representation of the goal.
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.
GetHelp returns help information for the tactic.
OrElse creates a tactic that applies t1, and if it fails, applies t2.
Repeat creates a tactic that applies t repeatedly (at most max times).