module Prop: sig end
Propositional logic
Author(s): Harald Ruess
type t
val pp : t Pretty.printer
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
?? |
: |
t
|
|
val mk_true : t
val mk_false : t
val mk_var : Name.t -> t
val mk_poslit : Atom.t -> t
val mk_neglit : Atom.t -> t
val mk_ite : t -> t -> t -> t
val mk_conj : t list -> t
val mk_disj : t list -> t
val mk_iff : t -> t -> t
val mk_neg : t -> t
val mk_let : Name.t -> t -> t -> t
val is_true : t -> bool
val is_false : t -> bool
val is_var : t -> bool
val is_atom : t -> bool
val is_ite : t -> bool
val is_disj : t -> bool
val is_iff : t -> bool
val is_neg : t -> bool
val is_let : t -> bool
val d_var : t -> Name.t
val d_atom : t -> Atom.t
val d_disj : t -> t list
val d_iff : t -> t * t
val d_ite : t -> t * t * t
val d_neg : t -> t
val d_let : t -> Name.t * t * t
val set_verbose : bool -> unit
Parameter settings for SAT solver
val set_assertion_frequency : int -> unit
val set_remove_subsumed_clauses : bool -> unit
val set_validate : bool -> unit
val set_polarity_optimization : bool -> unit
val set_clause_relevance : int -> unit
val set_cleanup_period : int -> unit
val set_num_refinements : int -> unit
val statistics : bool Pervasives.ref
val show_explanations : bool Pervasives.ref
module Assignment: sig end
Assignments for propositional formulas over literals
including equalities and arithmetic inequalities.
val sat : Context.t -> t -> (Assignment.t * Context.t) option
might fail if already in use.