Module IcSet

module IcSet: sig .. end

Creating and analyzing sets of compiled input clauses.

Notes:

Terms in different input clauses may be shared. Up to now variables are only modified, by Term.renumber_variables_term. Their number and external contexts are used to represent bindings.

If client programs modify terms (e.g. by calling Term.renumber_variables_term or once variable attributes are introduced), they must copy the clause contents.

Clauses as argument in term representation are assumed to have their variable numbers between 0 and Term.max_vars - 1.

See also notes for module Ic.

type clauses = Ic.clause list

val make_eval_plain_clauses : Cfg.cfg ->
       Predicate.predicate_table ->
       Term.symbol_table -> NegativeUnits.store -> Term.term list -> clauses

val negative_units_to_store : NegativeUnits.store -> clauses -> clauses

val stratify : clauses -> clauses list

stratify clauses partitions clauses in strata. The result is a list of lists of clauses, corresponding to the strata, lowest first.

val sort_clauses : clauses -> clauses

sort_clauses clauses sorts the clause set according to a heuristics that should allows earlier detection of refutations (branch closings)

val make_eval_inc_clauses : clauses -> Predicate.predicate list -> clauses

val idb_predicates : clauses -> Predicate.predicate list

idb_predicates clauses returns a list of those predicates in clauses which appear in the head of a clause in clauses.

val select_relevant_clauses : clauses -> Predicate.predicate -> clauses

relevant_clauses clauses goal_predicate selects those clauses from clauses which are relevant for computing goal_predicate. This also includes clauses with fail head, whose nonbuiltin body predicates are all among the relevant predicates.

val split_clauses : clauses -> clauses list * clauses * clauses

split_clauses clauses partitions clauses into several sets.

The first result is a list of lists of nonrecursive clauses. (We say a clause is recursive iff one of its head predicates is so). Each sublist contains a group of clauses, such that evaluation of a group in higher list position only depends on evaluation of groups in lower positions.

The second result is a list of the recursive clauses.

The third result is a list of the clauses with false head.

clauses must not include a clause with disjunctive head (for now?).