Up  

Class type Bound.bound


class type bound = object .. end
Here all candidates are checked for exceeding the iterative deepening bound. This includes determining if the current derivation branch is incomplete, i.e. if candidates have been dropped while constructing the branch, and (based on Flags.opt_restart) backtracking to a choice point, where the branch is not incomplete.

The actual bound criterion is handled internally according to Flags.opt_iterative_deepening.

In the finite domain mode (Config.finite_domain) the bound does not correspond to Flags.opt_iterative_deepening, but to the current domain size. As the input is BS then, any the complexity of any literal will be within the bound.

Member Access

method current_bound : complexity
the current deepening bound.
method dropped_choice_point : choice_point option
the oldest choice point of an ignored literal in the current derivation branch, if any have been ignored yet. this implies that the current branch can not be extended towards a model, but backtracking before this choice point might be.

Complexity

method get_complexity : literal -> complexity
the complexity value of a literal.
method get_complexity_subst : literal -> subst -> int -> complexity
get_complexity_subst literal subst offset returns the complexity of the literal assembled by applying subst with offset to literal.
method compare_complexity : complexity -> complexity -> int
usual comparison. Amounts to a compare over ints for term depth and term weight.

Check

method exceeds : complexity -> bool
returns true, if the candidate exceeds the current deepening bound.
method exceeds_current : complexity -> choice_point -> bool
returns true, if registering this candidate would have an impact wrt. to backtracking over an incomplete branch. that is, if the dropped complexity is higher than any complexity dropped up to now, or if the drop occurs in an older choice point than any other drop yet (Bound.bound.dropped_choice_point).

This is never the case if the candidate does not exceed the deepening bound. Otherwise, the details depend on the restart strategy (Flags.opt_restart), e.g. for eager restarting only the lowest dropped complexity is of relevance.

method register : complexity -> choice_point -> bool
like Bound.bound.exceeds, and additionally registers the candidate as dropped.
method register_subst : literal -> subst -> int -> choice_point -> bool
like Bound.bound.register, but for the literal assembled by applying subst with offset to literal.
method has_min_exceeding : bool
restarting will increase the depth bound by 1.

Backtracking

method backtrack : unit
retracts information invalidated by backtracking (State).
method restart : keep_bound:bool -> unit
cleans all stored data and increases the depth bound (if keep_bound is false, which is the default). The new depth bound is the lowest complexity of the dropped candidates.

Incomplete Branches

method is_derivation_incomplete : bool
an incomplete branch is part of the derivation and has been skipped. This implies that the current derivation can not be extended towards a refutation.
method incomplete : unit
marks the derivation as incomplete, i.e. an incomplete branch is (going to be) skipped.

Representation

method complexity_to_string : complexity -> string
the deepening bound as a string.
method print_statistic : unit
string representation of the current bound, restarts, and skipped incomplete branches (ala Print.print_label).