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 :` |
|||

` ` |
`rhs_struc :` |
`(*` | optional tuples in _opt_R-relations | `*)` |

` ` |
`emb_rels :` |
`(*` | tau_e-relations, other tau_h | `*)` |

` ` |
`rule_s :` |
`(*` | map of `rhs` elements to `lhs` elems | `*)` |

` ` |
`pre :` |
`(*` | 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 :` |
`(*` | The original rule specification, if any. | `*)` |

` ` |
`lhs_vars :` |
`(*` | Free variables of the condition. | `*)` |

` ` |
`match_formula :` |
`(*` | gets instantiated in the model | `*)` |

` ` |
`rhs_vars :` |
`(*` | replace the matched variables | `*)` |

` ` |
`add_tuples :` |
`(*` | gets added | `*)` |

` ` |
`del_tuples :` |
`(*` | gets removed | `*)` |

` ` |
`rlmap :` |
`(*` | 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`

`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(emb`e`

)

where emb`e`

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`

`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.