module type T = sig .. end
type
The type of numbers.
module Literal: Dl_core.L with type number = num
Literals.
type Literal.t
type
The type of the solver.
val negation : literal -> literal
The negation of the literal.
val new_solver : unit -> t
A new solver for difference logic over nums.
val fresh_variable : t -> Dl_core.Variable.t
A fresh variable for the solver.
val add_literal : t -> literal -> unit
Add an interface literal to the solver.
val conflict_detected : t -> bool
Has a conflict been detected in the solver?
val inference_possible : t -> bool
Might the solver attempt to make an inference?
val get_literal_possible : t -> bool
Does the solver have a literal to propagate?
val get_lemma_possible : t -> bool
Does the solver have a lemma to propagate?
val decision_level : t -> int
The decision level of the solver.
val increment_level : t -> unit
Increment the decision level of the solver.
val set_literal : t -> literal -> unit
Add a literal assertion to the solver.
val get_literal : t -> literal
Get a literal from the solver.
val get_lemma : t -> literal list
Get a lemma from the solver.
val infer : t -> unit
Attempt to make some inferences.
val explain_conflict : t -> literal list
Conflict clause.
val explain : t -> literal -> literal list
Clause explaining the propagated literal.
val backtrack : t -> int -> unit
Backtrack to the given decision level.
val is_true : t -> literal -> bool
Is the literal true in the current state of the solver?
val potential : t -> num Dl_core.Variable_map.t
The (negation of) the value assignment to variables in the
current model.
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.