package msat

  1. Overview
  2. Docs
val mcsat : bool
type term
type formula
type proof
type seen =
  1. | Nope
  2. | Both
  3. | Positive
  4. | Negative
type lit = {
  1. lid : int;
  2. term : term;
  3. mutable l_level : int;
  4. mutable l_weight : float;
  5. mutable assigned : term option;
}
type var = {
  1. vid : int;
  2. pa : atom;
  3. na : atom;
  4. mutable used : int;
  5. mutable seen : seen;
  6. mutable v_level : int;
  7. mutable v_weight : float;
  8. mutable v_assignable : lit list option;
  9. mutable reason : reason option;
}
and atom = {
  1. aid : int;
  2. var : var;
  3. neg : atom;
  4. lit : formula;
  5. mutable is_true : bool;
  6. mutable watched : clause Vec.t;
}
and clause = {
  1. name : string;
  2. tag : int option;
  3. atoms : atom array;
  4. mutable cpremise : premise;
  5. mutable activity : float;
  6. mutable attached : bool;
  7. mutable visited : bool;
}
and reason =
  1. | Decision
  2. | Bcp of clause
  3. | Semantic
and premise =
  1. | Hyp
  2. | Local
  3. | Lemma of proof
  4. | History of clause list
type t =
  1. | Lit of lit
  2. | Atom of atom
val of_lit : lit -> t
val of_atom : atom -> t
type elt =
  1. | E_lit of lit
  2. | E_var of var
val nb_elt : unit -> int
val get_elt : int -> elt
val iter_elt : (elt -> unit) -> unit
val elt_of_lit : lit -> elt
val elt_of_var : var -> elt
val get_elt_id : elt -> int
val get_elt_level : elt -> int
val get_elt_weight : elt -> float
val set_elt_level : elt -> int -> unit
val set_elt_weight : elt -> float -> unit
val dummy_var : var
val dummy_atom : atom
val dummy_clause : clause
val add_term : term -> lit
val add_atom : formula -> atom
val make_boolean_var : formula -> var * Formula_intf.negated
val empty_clause : clause
val make_clause : ?tag:int -> string -> atom list -> premise -> clause
val mark : atom -> unit
val seen : atom -> bool
val clear : var -> unit
val fresh_name : unit -> string
val fresh_lname : unit -> string
val fresh_tname : unit -> string
val fresh_hname : unit -> string
val print_lit : Format.formatter -> lit -> unit
val print_atom : Format.formatter -> atom -> unit
val print_clause : Format.formatter -> clause -> unit
val pp : Format.formatter -> t -> unit
val pp_lit : Format.formatter -> lit -> unit
val pp_atom : Format.formatter -> atom -> unit
val pp_clause : Format.formatter -> clause -> unit
val pp_dimacs : Format.formatter -> clause -> unit
val pp_reason : Format.formatter -> (int * reason option) -> unit