Module Datalog.Program

type program = {
  1. rules : Rule.Rules.t Predicate.PredMap.t;
  2. edb : ASPred.PredIds.t;
  3. edb_facts : Predicate.FactSet.t Predicate.PredMap.t;
  4. idb : ASPred.PredIds.t;
  5. pred_table : ASPred.PredIdTable.table;
  6. const_table : Datalog_AbstractSyntax.ConstGen.Table.table;
  7. rule_id_gen : UtilsLib.IdGenerator.IntIdGen.t;
  8. abstract_rules : ASRule.Rules.t;
}
val empty : program
val make_program : ASProg.program -> program
val temp_facts : Rule.rule -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> ((ASPred.predicate * Predicate.FactSet.elt list) -> Rule.rule -> 'a -> 'a) -> 'a -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> 'a
val p_semantics_for_predicate : Predicate.PredMap.key -> program -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> Rule.FactArray.row Predicate.PredMap.t -> Predicate.PremiseSet.t Predicate.PredicateMap.t -> Predicate.FactSet.t * Predicate.PremiseSet.t Predicate.PredicateMap.t
val seminaive : program -> Rule.FactArray.row Predicate.PredMap.t * Predicate.PremiseSet.t Predicate.PredicateMap.t
val to_abstract : program -> ASProg.program
val extend : program -> ASProg.modifier -> program

add_rule i r p adds a ASRule.rule to a Datalog.Program with the assumption that it will not change the nature of any predicate (that is making it change from extensional to intensional). If i is set to true, then the rule concerns an intensional predicate. If it is set to false then it concerns an extensional predicate and the rhs of the rule should be empty.

val add_rule : intensional:bool -> ASRule.rule -> program -> program
val remove_rule : int -> ASPred.pred_id -> program -> program

remove_rule id pred_id p returns the program p from which the rule with id id has been removed. It is assumed that the head of this rule is the predicate symbol of id pred_id.

IMPORTANT: This function only deals with rules introducing intensional predicate, because it is used when a constant is given several interpretations in a lexicon.

val get_fresh_rule_id : program -> int * program

get_fresh_rule_id prog returns a pair (i,prog') where i is a frech rule identifier and prog' only differs from prog by stating this rule identifier is now available

val get_fresh_cst_id : string -> program -> Datalog_AbstractSyntax.ConstGen.id * program

get_fresh_cst_id name prog returns a pair (id,prog') where id is constant identifier associated to name and prog' only differs from prog by stating this identifier is now available and is associated with name.

val add_pred_sym : string -> program -> ASPred.pred_id * program

add_pred_sym name p returns a pair (p_id,p') where p_id is a predicate id for the predicate symbol name and p' is p with recording the relation between name and p_id. If name is already a predicate symbol of p, then p_id is its id and p' is p. p' differs from p only with the association between name and p_id.

val build_forest : ?query:Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate -> Predicate.PremiseSet.t Predicate.PredicateMap.t -> program -> int Containers.SharedForest.SharedForest.forest list
val pp_edb : Stdlib.Format.formatter -> program -> unit