Module AbstractSyntax.Rule

type rule = {
  1. id : int;
  2. lhs : Predicate.predicate;
  3. e_rhs : (Predicate.predicate * int) list;
    (*

    represents the extensionnal predicates of the rule. The int represents the position in the rule

    *)
  4. i_rhs : (Predicate.predicate * int) list;
    (*

    represents the intensionnal predicates of the rule. The int represents the position in the rule

    *)
  5. i_rhs_num : int;
    (*

    stores the number of intensional predicates occurring in the rule

    *)
  6. rhs_num : int;
    (*

    stores the number of predicates occurring in the rule body

    *)
}
val pp : ?with_position:bool -> ?with_id:bool -> ?with_arity:bool -> Predicate.PredIdTable.table -> ConstGen.Table.table -> Stdlib.Format.formatter -> rule -> unit
val proto_rule_to_rule : Proto_Rule.t -> Predicate.PredIds.t -> rule
module Rules : Stdlib.Set.S with type elt = rule
module RuleMap : Stdlib.Map.S with type key = rule
val extend_head_id_map_to_rules : Predicate.pred_id -> rule -> Rules.t Predicate.PredIdMap.t -> Rules.t Predicate.PredIdMap.t
val set_new_id : int -> rule -> rule

set_new_id id rule returns a rule similar to rule except that its id is id

set_new_id_from_gen returns pair (rule',from_gen') wherer rule' is a rule similar to rule excepts that it has a new id generated from from_gen generator, and the latter has been updated to from_gen'.

val get_variables_in_rule : rule -> Predicate.TermSet.t

get_variables_in_rule rule returns the set of variables in the rule rule

val get_subgoal : rule -> int -> Predicate.predicate * int

get_subgoal rule i returns the predicate at the position i in the body of the rule rule