sig
type news
val make_news : Cfg.cfg -> News.news
val null_news : News.news
val set_max_literal_weight : News.news -> int -> unit
val reset_weight_limit_exceeded : News.news -> unit
val unit_table_size : News.news -> int
val delayed_clauses_size : News.news -> int
val weight_limit_exceeded : News.news -> int
val insert_unit : News.news -> Predicate.predicate -> Fact.fact -> unit
val insert_disjunction :
News.news ->
(Predicate.predicate * Fact.fact * int * Fact.fact list) list -> unit
val process_news : News.news -> int
val clear_news : News.news -> unit
module Disjunct :
sig
type disjunct
val is_wp_semantics_true : News.Disjunct.disjunct -> bool
val get_fact : News.Disjunct.disjunct -> Fact.fact
val get_predicate : News.Disjunct.disjunct -> Predicate.predicate
val get_complements : News.Disjunct.disjunct -> Fact.fact list
end
type delayed_clause
val get_disjuncts : News.delayed_clause -> News.Disjunct.disjunct list
val pick_disjunction : News.news -> News.delayed_clause
type state
val obtain_state : News.news -> News.state
val install_state : News.state -> unit
end