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.