msat 0.4 · OCaml Package

val mcsat : bool

type term

type formula = F.t

type proof = F.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 v_assignable : lit list option;
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 array;
mutable cpremise : premise;
mutable activity : float;
mutable attached : bool;
mutable visited : bool;

}

and reason =

| Decision
| Bcp of clause
| Semantic of int

and premise =

| Hyp
| Lemma of proof
| History of clause list

type t =

| Lit of lit
| Atom of atom

val of_lit : lit -> t

val of_atom : atom -> t

type elt =

| E_lit of lit
| 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 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