module GDL:`sig`

..`end`

`val playout_fixpoint : ``bool Pervasives.ref`

`val set_timeout : ``(unit -> bool) -> unit`

`type `

term =

`|` |
`Const of ` |

`|` |
`Var of ` |

`|` |
`Func of ` |

type`rel_atom =`

`string * term array`

`type `

atom =

`|` |
`Distinct of ` |

`|` |
`Rel of ` |

`|` |
`Role of ` |

`|` |
`True of ` |

`|` |
`Does of ` |

`type `

literal =

`|` |
`Pos of ` |

`|` |
`Neg of ` |

`|` |
`Disj of ` |

type`gdl_rule =`

`rel_atom * rel_atom list * rel_atom list`

Positive and negative literals separated, disjunctions expanded-out.

Collect rules by relations.

type`def_branch =`

`term array * rel_atom list * rel_atom list`

type`gdl_defs =`

`(string * def_branch list) list`

type`clause =`

`rel_atom * literal list`

type`path =`

`(string * int) list`

`type `

path_set

`type `

request =

`|` |
`Start of ` |
`(*` | prepare game: match id, role, game, startclock, playclock | `*)` |

`|` |
`Play of ` |
`(*` | request a move: match id, actions on previous step | `*)` |

`|` |
`Stop of ` |
`(*` | game ends here: match id, actions on previous step | `*)` |

module Terms:`Set.S`

`with type elt = term`

`val add_terms : ``term list -> Terms.t -> Terms.t`

`val terms_of_list : ``term list -> Terms.t`

`val atoms_of_body : ``literal list -> atom list`

`val rel_of_atom : ``atom -> rel_atom`

`val term_vars : ``term -> Aux.Strings.t`

`val terms_vars : ``term array -> Aux.Strings.t`

`val clause_vars : ``clause -> Aux.Strings.t`

`val clauses_vars : ``clause list -> Aux.Strings.t`

`val literals_vars : ``literal list -> Aux.Strings.t`

`val defs_of_rules : ``gdl_rule list -> gdl_defs`

`val rules_of_clause : ``clause -> gdl_rule list`

`val nnf_dnf : ``literal list -> literal list list`

type`substitution =`

`(string * term) list`

`val unify : ``substitution -> term list -> term list -> substitution`

`val unify_args : ``?sb:substitution -> term array -> term array -> substitution`

Match terms on the left to ground terms on the right, ignoring

`Const "_BLANK_"`

on the right.`val match_nonblank : ``substitution -> term list -> term list -> substitution`

Check for equality modulo ground terms on the right.

`val mask_blank : ``term list -> term list -> bool`

`val unify_all : ``substitution -> term list -> substitution`

`val unify_rels : ``?sb:substitution -> rel_atom -> rel_atom -> substitution`

`val rels_unify : ``rel_atom -> rel_atom -> bool`

`val subst : ``substitution -> term -> term`

`val subst_consts : ``substitution -> term -> term`

`val subst_rel : ``substitution -> rel_atom -> rel_atom`

`val subst_rels : ``substitution -> rel_atom list -> rel_atom list`

`val subst_literal : ``substitution -> literal -> literal`

`val subst_literals : ``substitution -> literal list -> literal list`

`val subst_clause : ``substitution -> clause -> clause`

`val subst_consts_literals : ``substitution -> literal list -> literal list`

`val subst_consts_clause : ``substitution -> clause -> clause`

module Tuples:`Set.S`

`with type elt = term array`

type`graph =`

`Tuples.t Aux.StrMap.t`

`val graph_mem : ``string -> term array -> graph -> bool`

`val merge_graphs : ``graph -> graph -> graph`

`val build_graph : ``rel_atom list -> graph`

`val graph_to_atoms : ``graph -> rel_atom list`

`val gdl_rel_graph : ``string -> graph -> term array list`

Saturation currently exposed for testing purposes.

`val saturate : ``graph -> gdl_rule list -> graph`

`val run_prolog_aggregate : ``bool Pervasives.ref`

The interpreter can reinterpret "does" atoms as "legal" atoms for
aggregate playout. For random playout, remember to compute legal
moves, select randomly one for each player and add "does" atoms to
the program.

`val reorder_clauses : ``bool Pervasives.ref`

`type `

prolog_program

`val preprocess_program : ``clause list -> prolog_program`

`val restore_program : ``?t_cls:clause list ->`

?d_cls:clause list -> prolog_program -> prolog_program

`val run_prolog_atom : ``rel_atom -> prolog_program -> rel_atom list`

Compute all implied instantiations of the given atom, return
sorted unique instances.

Compute all variable substitutions that satisfy the given
conjunction of literals. The substitutions are not unique (there
is as many of them as there are different proofs of the goal).

`val run_prolog_goal : ``literal list -> prolog_program -> substitution list`

Just check if the atom / conjunction of literals is
satisfiable. Should be faster than checking non-emptiness of

`run_prolog_goal`

result.`val run_prolog_check_atom : ``rel_atom -> prolog_program -> bool`

`val run_prolog_check_goal : ``literal list -> prolog_program -> bool`

`val optimize_goal : ``testground:prolog_program ->`

?head_sb:substitution -> literal list -> literal list

`val optimize_program : ``testground:prolog_program -> prolog_program -> prolog_program`

`val expand_definitions : ``gdl_defs -> def_branch list -> def_branch list`

Expand branches of a definition inlining the provided
definitions. Iterate expansion to support nesting of
definitions.

`val atom_of_rel : ``rel_atom -> atom`

Remember that

`rel_of_atom`

inverts polarity of "distinct" --
invert back after using `atom_of_rel`

if needed.`val negate_bodies : ``literal list list -> (substitution * literal list) list`

Form clause bodies whose disjunction is equivalent to the
negation of disjunction of given clause bodies. Keep the
substitution so that the heads of corresponding clauses can be
substituted too.

`val rename_clauses : ``clause list -> Aux.Strings.t Pervasives.ref * clause list`

Rename clauses so that they have disjoint variables. Return a cell
storing all variables.

`val func_graph : ``string -> term list -> term array list`

`val elim_pattern_args : ``string list -> clause list -> string list * clause list`

Eliminate arguments of relations that are defined by non-wildcard
pattern matching (i.e. do not have a variable in any of the
defining clauses). Return the new clauses, and also the new
relation set.

`val elim_ground_distinct : ``clause list -> clause list`

`val state_cls : ``term list -> clause list`

`val blank : ``term`

`val counter_n : ``string`

`val term_str : ``term -> string`

`val terms_str : ``term array -> string`

`val term_to_name : ``?nested:bool -> term -> string`

`val state_terms : ``literal list -> term list`

`val pos_state_terms : ``literal list -> term list`

`val term_arities : ``term -> (string * int) list`

`val atom_str : ``atom -> string`

`val rel_atom_str : ``rel_atom -> string`

`val rel_atoms_str : ``rel_atom list -> string`

`val gdl_rule_str : ``gdl_rule -> string`

`val gdl_rules_str : ``gdl_rule list -> string`

`val def_str : ``string * def_branch list -> string`

`val literal_str : ``literal -> string`

`val literals_str : ``literal list -> string`

`val clause_str : ``clause -> string`

`val clauses_str : ``clause list -> string`

`val sb_str : ``(string * term) list -> string`

`val program_clauses : ``prolog_program -> clause list`

`val topsort_callgraph : ``clause list -> string list`

Aggregate and random playout, player-denoting variable elimination.

`val static_rels : ``gdl_defs -> string list * string list`

Partition relations into static (not depending, even indirectly,
on "true") and remaining ones.

`val playout_satur : ``aggregate:bool ->`

term array ->

int ->

gdl_rule list ->

gdl_rule list * gdl_rule list * graph * term list *

(term array list list * term list list * term list)

Besides the aggregate or random playout, also return the
separation of rules into static and dynamic. Note that the list of
playout states is one longer than that of playout actions.

When `aggregate_drop_negative`

is true, to keep monotonicity,
besides removing negative literals from "legal" clauses, we also
add old terms to the state. (Only when `~aggregate:true`

.)

`~aggregate:true`

performs an aggregate ply, `~aggregate:false`

performs a random ply. Aggregate playouts are "deprecated",
especially for uses other than generating all possible state
terms.

`val playout_prolog : ``aggregate:bool ->`

term array ->

int ->

prolog_program ->

term array list list * term list list * term list

`val find_cycle : ``term option list -> term option list`

`val expand_players : ``clause list -> clause list`

`val simult_subst : ``path_set -> term -> term -> term`

`simult_subst ps s t`

substitutes `s`

at all `t`

paths that belong
to the set `ps`

, returns $t`ps \ot s`

$.`val map_paths : ``(path -> term -> 'a) -> path_set -> term -> 'a list`

Find the list of results of a function applied to paths from the
given set that are in the term, and to subterms at these paths.

`val rel_on_paths : ``string -> path list -> string`

Toss relations hold between subterms of GDL state terms: generate
Toss relation name.

`val pred_on_path_subterm : ``path -> term -> string`

Some Toss predicates are generated from a path and an expected
subterm at that path.

`val term_paths : ``?prefix_only:bool -> (term -> bool) -> term -> path_set`

All paths in a term pointing to subterms that satisfy a
predicate. With

`~prefix_only:true`

, paths that contain a path
that has been included, are not included.`val at_path : ``term -> path -> term`

Find the subterm at given path, if the term does not have the
path, raise

`Not_found`

; `at_path p t`

is $t \tpos p$.`val merge_terms : ``term -> term -> path_set * int * int`

The set of paths that merges two terms, the cardinality of this
set, and the size of the largest common subtree.

`val at_paths : ``?fail_at_missing:bool -> path_set -> term -> term list`

Find the list of subterms at paths from the given set, if the term
does not have some of the paths, ignore them if

`~fail_at_missing:false`

,
raise `Not_found`

if `~fail_at_missing:true`

.`val empty_path_set : ``path_set`

`val eps_path_set : ``path_set`

Add path to a set. First argument gives term arities.

`val add_path : ``(string -> int) -> path -> path_set -> path_set`

`val paths_union : ``path_set -> path_set -> path_set`

`val paths_intersect : ``path_set -> path_set -> path_set`

`val paths_to_list : ``path_set -> path list`

List the paths in a set.

`val path_str : ``path -> string`

`val ground_vars_at_paths : ``(clause -> literal list) ->`

(path * term list) list -> clause list -> clause list

`ground_vars_at_paths prepare_lits ps_sterms clauses`

expands
subterms that have occurrences at paths in `ps_sterms`

in some
state term of a clause (from which pre-processed literals are
extracted by `prepare_lits`

), by substituting their variables with
corresponding subterms of terms provided in `ps_sterms`

.`val blank_outside_subterm : ``(string * int) list -> path -> term -> term`

`val blank_outside_subterms : ``(string * int) list -> (path * term) list -> term`

`val refine_leaf_paths : ``path_set -> term list -> path_set`

If some path points only to bigger than one (i.e. non-leaf)
subterms in the given set of terms, then expand/split it to longer
paths that together cover all leafs the original path covered.

`val refine_paths_avoiding : ``path_set ->`

(term -> bool) -> (term -> bool) -> term list -> path_set

`refine_paths_avoiding paths avoid_later avoid_now terms`

splits
paths in the set until, if possible, none of subterms at the paths
meets the predicate `avoid_later`

; it does not descend subterms
for which `avoid_now`

holds. Also removes paths not present
in terms.type`argpaths =`

`(path * int) list list`

The integers should be all-distinct and from 0 to N-1.

`val find_rel_arg : ``term list -> term array -> (path * int) list -> term`

`val complete_paths_for : ``path_set -> argpaths -> bool`

Check whether each of argpaths covers some tree in c_paths
completely.