Module Bound (.ml)

module Bound: sig .. end

iterative deepening bound

Types

type config = Config.config

type literal = Term.literal

type choice_point = State.choice_point

type subst = Subst.subst

type complexity = int

the complexity (of a literal), i.e. the value to be checked against the deepening bound. Currently the term depth or weight (Flags.opt_iterative_deepening).

class type bound = object .. end

Here all candidates are checked for exceeding the iterative deepening bound.

Creation

val create : inc:bool -> config -> bound

creates a bound object with the initial bound given in Config.deepening_bound. if inc is true, Bound.bound.restart always increases the bound by 1, otherwise as described in Bound.bound.restart

val create_BS : config -> bound

creates a bound object specialized for the BS class (function free terms) using term depth as the complexity.

that is, all terms are known to be of term depth 2, so in essence no bound checks need to be performed at all.