# Module DiscreteRule

module DiscreteRule: sig .. end
Discrete structure rewriting rules construction and rewriting.

val approximate_monotonic : bool Pervasives.ref
If true, ignore what happens on RHSes of rules when assessing if fluents are positive / negative (only check whether their LHS+precondition occurrences are negative/positive).
val prune_indef_vars : bool Pervasives.ref
type matching = (string * int) list
Single match of a rule, and a set of matches.
type matchings = Assignments.assignment_set
type struc_rule = {
    lhs_struc :Structure.structure;    rhs_struc :Structure.structure; (* optional tuples in _opt_R-relations *)    emb_rels :string list; (* tau_e-relations, other tau_h *)    rule_s :(int * int) list; (* map of rhs elements to lhs elems *)    pre :Formula.formula * (string * bool) list; (* precondition *)
}
Specification of a discrete rewriting rule, as in modelling document. rhs_struc must have all emb_rels in its signature.
type var_tuples = string array list
type rule = {
    struc_rule :struc_rule option; (* The original rule specification, if any. *)    lhs_vars :string list; (* Free variables of the condition. *)    match_formula :Formula.formula; (* gets instantiated in the model *)    rhs_vars :string list; (* replace the matched variables *)    add_tuples :(string * var_tuples) list; (* gets added *)    del_tuples :(string * var_tuples) list; (* gets removed *)    rlmap :(string * string) list option; (* rule_s on variables; None means that the correspondence is 1-1 without renaming. *)
}
The formula-based rewrite rule representation. In general does not check for injectivity (distinctness of matched elements). The structure-based representation is used to generate this representation.
val empty_rule : rule
Empty rule.
val fluents : rule list -> Aux.Strings.t * Aux.Strings.t * Aux.Strings.t
Fluents are relations that are changed by rules. Distinguish two subclasses of fluents: positive fluents occur only positively on RHSes (are only added) and only negatively on LHSes and in preconditions, and negative fluents only negatively on RHSes (are only deleted) and only positively on LHSes and in preconditions. (Call the remaining fluents indefinite.) See Heuristic.
val fluents_make : ?only_pos:bool -> (string -> int -> 'a) -> rule -> 'a list
val fluent_preconds : rule list ->       (string -> int) ->       Aux.Strings.t ->       Aux.Strings.t ->       Aux.Strings.t -> (string * (string list * Formula.formula)) list
A fluent precondition is an approximation to the condition on a structure for the positive/negative fluent to appear/disappear at a position. We are only interested in expanding preconditions of positive and negative fluents.
val map_to_formulas : (Formula.formula -> Formula.formula) ->       rule -> rule
Map and fold over formulas in a rule. The add and delete tuples, and the lhs_vars denoting variables of a rule matching, are not affected.
val fold_over_formulas : (Formula.formula -> 'a -> 'a) -> rule -> 'a -> 'a
val map_to_structures : (Structure.structure -> Structure.structure) ->       rule -> rule
val orig_rel_of : string -> string
val special_rel_of : string -> string option

## Embedding and rewriting.

val find_matchings : Structure.structure -> rule -> matchings
Find all embeddings of a rule. Does not guarantee that rewriting will succeed for all of them.
val choose_match : Structure.structure ->       rule -> matchings -> matching
Choose an arbitrary embedding of a rule from the matchings returned by DiscreteRule.find_matchings for the same structure and rewrite rule. Does not guarantee that rewriting the matching will succeed. Raises Not_found for the empty matchings set.
val enumerate_matchings : Structure.structure ->       rule -> matchings -> matching list
Enumerate matchings returned by DiscreteRule.find_matchings for the same structure and rewrite rule.
val rewrite_single : Structure.structure ->       matching -> rule -> Structure.structure
Rewrite the model using the rule at the given matching.

Rewriting introduces the following form of trace:

_new_R(tup) = +R(tup) = R(tup) and not R_old(tup) _del_R(tup) = -R(tup) = not R(tup) and R_old(tup) _right_e(embe)

where embe is the model element corresponding to a RHS rule element e, or, when LHS and RHS structures have the same number of elements, e is a LHS structure element due to rule optimization during rule compilation.

val compile_rule : (string * int) list ->       (string * (string list * Formula.formula)) list ->       struc_rule -> rule
Translate a rule specification into a processed form. Note that when a relation is in $\tau_h$, and is present in the LHS but not in the RHS, it is still not removed by a rewrite.

Translate a formula-based rule specification into a processed form.

val compile_formula_rule : (string * int) list ->       (string * (string list * Formula.formula)) list ->       Formula.formula ->       (string list * (string * string list) list) option ->       ((string * string option) list * (string * string list) list) option ->       (Formula.formula * (string * bool) list) option -> rule
val changeable_rels : rule list -> string list
Relations that can explicitly change state by rewriting (i.e. not as a result of erasure). (A "symmetric difference" of rule sides.)
val translate_from_precond : precond:Formula.formula ->       add:(string * string array) list ->       ?del:(string * string array) list ->       nondistinct:string array list ->       emb_rels:string list ->       signat:(string * int) list ->       struc_elems:string list -> struc_rule
Build a rule by translating the "add" list into the RHS structure directly, and separating out from a precondition the LHS structure over the struc_vars variables. Only and all the emb_rels relations are embedded (usually the fluents). (Not all rules can be generated using this function.) Caution: simplifies the precondition.

The partition of embedded relations into positive and negative tuples (literals) is extracted from the precondition. If the partition does not cover all tuples, fail.

nondistinct_pairs connects elements that are potentially not distinct, thus weakening the "embedding" requirement into "homomorphism" requirement for matching a rule.

val matching_str : matching -> string

## Printing.

val rule_str : rule -> string
val rule_obj_str : rule -> string
Alternative syntax for testing.
val fprint_full : bool -> Format.formatter -> rule -> unit
val fprint_rule : Format.formatter -> rule -> unit
val fprint_rule : Format.formatter -> rule -> unit
val print_rule : rule -> unit
val sprint_rule : rule -> string
val is_alpha_identity : struc_rule -> bool
val build_rule_s : ?rule_s:(string * string) list ->       Structure.structure -> Structure.structure -> (int * int) list
val compare_diff : ?cmp_funs:(float -> float -> bool) ->       struc_rule -> struc_rule -> bool * string
Compare two rules and explain the first difference met. Preconditions are compared for structural equality.