Previous  Up  Next

Module News


module News: sig .. end
Storing and processing of newly derived facts (similar to a SOS).
type news
The type of news objects.
val make_news : Cfg.cfg -> news
Create a news object.
val null_news : news
An unusable news object to initialize typed fields.
val set_max_literal_weight : news -> int -> unit
val reset_weight_limit_exceeded : news -> unit
val unit_table_size : news -> int
val delayed_clauses_size : news -> int
val weight_limit_exceeded : news -> int
Is > 0 iff an inferred clause has been discarded since it exceeded the weight limit. The returned amount is the difference from the weight of the lightest such discarded clause to the limit.
val insert_unit : news -> Predicate.predicate -> Fact.fact -> unit
Insert a fact into a news object.
val insert_disjunction : news ->
       (Predicate.predicate * Fact.fact * int * Fact.fact list) list -> unit
Insert a disjunction into a news object. The disjunction is represented as a list of length > 1 of quadruples. A quadruple contains: the predicate, the atom, the weight of the atom, and a list of terms used for complement splitting.
val process_news : news -> int
process_news news processes facts in news. Processed facts are removed from news.

The number of actually new facts is returned, i.e. processed facts that are not subsumed by previously derived facts.

The precise meaning of process_news depends on the particular strategy. 


val clear_news : news -> unit
Remove all unit facts from news. To be called in place of process_news when the facts should be thrown away (e.g. after branch closing) , but the news object should be used again (e.g. for alternative branches).
module Disjunct: sig .. end
type delayed_clause 
val get_disjuncts : delayed_clause -> Disjunct.disjunct list
val pick_disjunction : news -> delayed_clause
Raises Not_found if no disjunction that is not subsumed by a unit in the extent is found.
type state 
val obtain_state : news -> state
val install_state : state -> unit