functor
(E : Expr_intf.S) (Th : sig
type term = E.Term.t
type formula = E.Formula.t
type proof = E.proof
type level
val dummy : level
val current_level : unit -> level
val assume :
(term, formula, proof) Plugin_intf.slice ->
(formula, proof) Plugin_intf.res
val if_sat :
(term, formula, proof) Plugin_intf.slice ->
(formula, proof) Plugin_intf.res
val backtrack : level -> unit
val assign : term -> term
val iter_assignable :
(term -> unit) -> formula -> unit
val eval : formula -> term Plugin_intf.eval_res
end) (Dummy : sig end) ->
sig
module St :
sig
val mcsat : bool
type term = E.Term.t
type formula = E.Formula.t
type proof = E.proof
type seen = Nope | Both | Positive | Negative
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 used : int;
mutable seen : seen;
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
and premise = Hyp | Local | 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 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
end
module Proof :
sig
module St :
sig
val mcsat : bool
type term = St.term
type formula = St.formula
type proof = St.proof
type seen = St.seen = Nope | Both | Positive | Negative
type lit =
St.lit = {
lid : int;
term : term;
mutable l_level : int;
mutable l_weight : float;
mutable assigned : term option;
}
type var =
St.var = {
vid : int;
pa : atom;
na : atom;
mutable used : int;
mutable seen : seen;
mutable v_level : int;
mutable v_weight : float;
mutable v_assignable : lit list option;
mutable reason : reason option;
}
and atom =
St.atom = {
aid : int;
var : var;
neg : atom;
lit : formula;
mutable is_true : bool;
mutable watched : clause Vec.t;
}
and clause =
St.clause = {
name : string;
tag : int option;
atoms : atom array;
mutable cpremise : premise;
mutable activity : float;
mutable attached : bool;
mutable visited : bool;
}
and reason = St.reason = Decision | Bcp of clause | Semantic
and premise =
St.premise =
Hyp
| Local
| Lemma of proof
| History of clause list
type t = St.t = Lit of lit | Atom of atom
val of_lit : lit -> t
val of_atom : atom -> t
type elt = St.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 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
end
exception Insuficient_hyps
type atom = St.atom
type lemma = St.proof
type clause = St.clause
type proof
and proof_node = { conclusion : clause; step : step; }
and step =
Hypothesis
| Assumption
| Lemma of lemma
| Duplicate of proof * atom list
| Resolution of proof * proof * atom
val to_list : clause -> atom list
val merge : atom list -> atom list -> atom list
val resolve : atom list -> atom list * atom list
val prove : clause -> proof
val prove_unsat : clause -> proof
val prove_atom : atom -> proof option
val parents : step -> proof list
val is_leaf : step -> bool
val expl : step -> string
val expand : proof -> proof_node
val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
val unsat_core : proof -> clause list
val check : proof -> unit
val print_clause : Format.formatter -> clause -> unit
module H :
sig
type key = clause
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
type atom = St.formula
type res =
Sat of (St.term, St.formula) Solver_intf.sat_state
| Unsat of (St.clause, Proof.proof) Solver_intf.unsat_state
exception UndecidedLit
val assume : ?tag:int -> atom list list -> unit
val solve : ?assumptions:atom list -> unit -> res
val new_lit : St.term -> unit
val new_atom : atom -> unit
val unsat_core : Proof.proof -> St.clause list
val true_at_level0 : atom -> bool
val get_tag : St.clause -> int option
val export_dimacs : Format.formatter -> unit -> unit
val export_icnf : Format.formatter -> unit -> unit
end