Module Dpll_literal

module Dpll_literal: sig .. end
Literals and variables.

module Variable: Id.Generator 
Variables are represented by unique identifiers.
module Variable_map: Index.Map  with type key = Variable.t
Maps keyed off variables.
module Variable_set: Index.Set  with type elt = Variable.t
Sets of variables.
module Variable_queue: Index.PriorityQueue  with type elt = Variable.t
Priorities queues of variables.
module Literal: Id.T 
Literals are unique identifiers.
module Literal_map: Index.Map  with type key = Literal.t
Maps keyed off literals.
module Literal_set: Index.Set  with type elt = Literal.t
Sets of literals.
val variable : Literal.t -> Variable.t
variable l is the variable in literal l.

val is_positive : Literal.t -> bool
is_positive l is true when l is a literal positive.

val literal : Variable.t -> Literal.t
literal v is the positive literal corresponding to variable v.

val negation : Literal.t -> Literal.t
negation l is the negation of literal l.

Hosted by the Logo* web site.
*Other names and brands may be claimed as the property of others.