msat 0.3 · OCaml Package

val mcsat : bool

type term = Fsmt.Term.t

type formula = Fsmt.Formula.t

type proof = Fsmt.proof

type lit = {

lid : int;
term : term;
mutable l_level : int;
mutable l_weight : float;
mutable assigned : term option;

}

type var = {

vid : int;
pa : atom;
na : atom;
mutable seen : bool;
mutable v_level : int;
mutable v_weight : float;
mutable reason : reason option;

}

and atom = {

aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
mutable watched : clause Vec.t;

}

and clause = {

name : string;
tag : int option;
atoms : atom Vec.t;
learnt : bool;
c_level : int;
mutable cpremise : premise;
mutable activity : float;
mutable removed : bool;

}

and reason =

| Decision
| Bcp of clause
| Semantic of int

and premise =

| Lemma of proof
| History of clause list

type t = (lit, atom) Either.t

val of_lit : lit -> t

val of_atom : atom -> t

type elt = (lit, var) Either.t

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 * bool

val empty_clause : clause

val make_clause : 
  ?tag:int ->
  string ->
  atom list ->
  int ->
  bool ->
  premise ->
  int ->
  clause

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_lit : Format.formatter -> lit -> unit

val pp_atom : Format.formatter -> atom -> unit

val pp_clause : Format.formatter -> clause -> unit

package msat