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.

Require Literal.is_valid l
Ensure Literal.is_valid (negation l)
Ensure Dpll_literal.is_positive (negation l) = not (Dpll_literal.is_positive l)
Ensure Dpll_literal.variable (negation l) = Dpll_literal.variable l

Hosted by the

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