Module Clause

module Clause: sig .. end

Clauses




The clauses are hashconsed within a context (an application of Clause.Make). Now clauses also have a trail, that is, a set of boolean literals that it depends upon as a conditional guard.
val stat_clause_create : Logtk.Util.stat
module type S = Clause_intf.S
type 'c sets = {
   c_set : 'c CCVector.ro_vector; (*
main set of clauses
*)
   c_sos : 'c CCVector.ro_vector; (*
set of support
*)
}
Bundle of clause sets

Clauses that depend on a Context


module Make: 
functor (Ctx : Ctx.S) -> S with module Ctx = Ctx