sig
  val playout_fixpoint : bool Pervasives.ref
  val set_timeout : (unit -> bool) -> unit
  type term =
      Const of string
    | Var of string
    | Func of string * GDL.term array
  type rel_atom = string * GDL.term array
  type atom =
      Distinct of GDL.term array
    | Rel of GDL.rel_atom
    | Role of GDL.term
    | True of GDL.term
    | Does of GDL.term * GDL.term
  type literal = Pos of GDL.atom | Neg of GDL.atom | Disj of GDL.literal list
  type gdl_rule = GDL.rel_atom * GDL.rel_atom list * GDL.rel_atom list
  type def_branch = GDL.term array * GDL.rel_atom list * GDL.rel_atom list
  type gdl_defs = (string * GDL.def_branch list) list
  type clause = GDL.rel_atom * GDL.literal list
  type path = (string * int) list
  type path_set
  type request =
      Start of string * GDL.term * GDL.clause list * int * int
    | Play of string * GDL.term list
    | Stop of string * GDL.term list
  module Terms :
    sig
      type elt = term
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  val add_terms : GDL.term list -> GDL.Terms.t -> GDL.Terms.t
  val terms_of_list : GDL.term list -> GDL.Terms.t
  val atoms_of_body : GDL.literal list -> GDL.atom list
  val rel_of_atom : GDL.atom -> GDL.rel_atom
  val term_vars : GDL.term -> Aux.Strings.t
  val terms_vars : GDL.term array -> Aux.Strings.t
  val clause_vars : GDL.clause -> Aux.Strings.t
  val clauses_vars : GDL.clause list -> Aux.Strings.t
  val literals_vars : GDL.literal list -> Aux.Strings.t
  val defs_of_rules : GDL.gdl_rule list -> GDL.gdl_defs
  val rules_of_clause : GDL.clause -> GDL.gdl_rule list
  val nnf_dnf : GDL.literal list -> GDL.literal list list
  type substitution = (string * GDL.term) list
  val unify :
    GDL.substitution -> GDL.term list -> GDL.term list -> GDL.substitution
  val unify_args :
    ?sb:GDL.substitution ->
    GDL.term array -> GDL.term array -> GDL.substitution
  val match_nonblank :
    GDL.substitution -> GDL.term list -> GDL.term list -> GDL.substitution
  val mask_blank : GDL.term list -> GDL.term list -> bool
  val unify_all : GDL.substitution -> GDL.term list -> GDL.substitution
  val unify_rels :
    ?sb:GDL.substitution -> GDL.rel_atom -> GDL.rel_atom -> GDL.substitution
  val rels_unify : GDL.rel_atom -> GDL.rel_atom -> bool
  val subst : GDL.substitution -> GDL.term -> GDL.term
  val subst_consts : GDL.substitution -> GDL.term -> GDL.term
  val subst_rel : GDL.substitution -> GDL.rel_atom -> GDL.rel_atom
  val subst_rels : GDL.substitution -> GDL.rel_atom list -> GDL.rel_atom list
  val subst_literal : GDL.substitution -> GDL.literal -> GDL.literal
  val subst_literals :
    GDL.substitution -> GDL.literal list -> GDL.literal list
  val subst_clause : GDL.substitution -> GDL.clause -> GDL.clause
  val subst_consts_literals :
    GDL.substitution -> GDL.literal list -> GDL.literal list
  val subst_consts_clause : GDL.substitution -> GDL.clause -> GDL.clause
  module Tuples :
    sig
      type elt = term array
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  type graph = GDL.Tuples.t Aux.StrMap.t
  val graph_mem : string -> GDL.term array -> GDL.graph -> bool
  val merge_graphs : GDL.graph -> GDL.graph -> GDL.graph
  val build_graph : GDL.rel_atom list -> GDL.graph
  val graph_to_atoms : GDL.graph -> GDL.rel_atom list
  val gdl_rel_graph : string -> GDL.graph -> GDL.term array list
  val saturate : GDL.graph -> GDL.gdl_rule list -> GDL.graph
  val run_prolog_aggregate : bool Pervasives.ref
  val reorder_clauses : bool Pervasives.ref
  type prolog_program
  val preprocess_program : GDL.clause list -> GDL.prolog_program
  val restore_program :
    ?t_cls:GDL.clause list ->
    ?d_cls:GDL.clause list -> GDL.prolog_program -> GDL.prolog_program
  val run_prolog_atom :
    GDL.rel_atom -> GDL.prolog_program -> GDL.rel_atom list
  val run_prolog_goal :
    GDL.literal list -> GDL.prolog_program -> GDL.substitution list
  val run_prolog_check_atom : GDL.rel_atom -> GDL.prolog_program -> bool
  val run_prolog_check_goal : GDL.literal list -> GDL.prolog_program -> bool
  val optimize_goal :
    testground:GDL.prolog_program ->
    ?head_sb:GDL.substitution -> GDL.literal list -> GDL.literal list
  val optimize_program :
    testground:GDL.prolog_program -> GDL.prolog_program -> GDL.prolog_program
  val expand_definitions :
    GDL.gdl_defs -> GDL.def_branch list -> GDL.def_branch list
  val atom_of_rel : GDL.rel_atom -> GDL.atom
  val negate_bodies :
    GDL.literal list list -> (GDL.substitution * GDL.literal list) list
  val rename_clauses :
    GDL.clause list -> Aux.Strings.t Pervasives.ref * GDL.clause list
  val func_graph : string -> GDL.term list -> GDL.term array list
  val elim_pattern_args :
    string list -> GDL.clause list -> string list * GDL.clause list
  val elim_ground_distinct : GDL.clause list -> GDL.clause list
  val state_cls : GDL.term list -> GDL.clause list
  val blank : GDL.term
  val counter_n : string
  val term_str : GDL.term -> string
  val terms_str : GDL.term array -> string
  val term_to_name : ?nested:bool -> GDL.term -> string
  val state_terms : GDL.literal list -> GDL.term list
  val pos_state_terms : GDL.literal list -> GDL.term list
  val term_arities : GDL.term -> (string * int) list
  val atom_str : GDL.atom -> string
  val rel_atom_str : GDL.rel_atom -> string
  val rel_atoms_str : GDL.rel_atom list -> string
  val gdl_rule_str : GDL.gdl_rule -> string
  val gdl_rules_str : GDL.gdl_rule list -> string
  val def_str : string * GDL.def_branch list -> string
  val literal_str : GDL.literal -> string
  val literals_str : GDL.literal list -> string
  val clause_str : GDL.clause -> string
  val clauses_str : GDL.clause list -> string
  val sb_str : (string * GDL.term) list -> string
  val program_clauses : GDL.prolog_program -> GDL.clause list
  val topsort_callgraph : GDL.clause list -> string list
  val static_rels : GDL.gdl_defs -> string list * string list
  val playout_satur :
    aggregate:bool ->
    GDL.term array ->
    int ->
    GDL.gdl_rule list ->
    GDL.gdl_rule list * GDL.gdl_rule list * GDL.graph * GDL.term list *
    (GDL.term array list list * GDL.term list list * GDL.term list)
  val playout_prolog :
    aggregate:bool ->
    GDL.term array ->
    int ->
    GDL.prolog_program ->
    GDL.term array list list * GDL.term list list * GDL.term list
  val find_cycle : GDL.term option list -> GDL.term option list
  val expand_players : GDL.clause list -> GDL.clause list
  val simult_subst : GDL.path_set -> GDL.term -> GDL.term -> GDL.term
  val map_paths :
    (GDL.path -> GDL.term -> 'a) -> GDL.path_set -> GDL.term -> 'a list
  val rel_on_paths : string -> GDL.path list -> string
  val pred_on_path_subterm : GDL.path -> GDL.term -> string
  val term_paths :
    ?prefix_only:bool -> (GDL.term -> bool) -> GDL.term -> GDL.path_set
  val at_path : GDL.term -> GDL.path -> GDL.term
  val merge_terms : GDL.term -> GDL.term -> GDL.path_set * int * int
  val at_paths :
    ?fail_at_missing:bool -> GDL.path_set -> GDL.term -> GDL.term list
  val empty_path_set : GDL.path_set
  val eps_path_set : GDL.path_set
  val add_path : (string -> int) -> GDL.path -> GDL.path_set -> GDL.path_set
  val paths_union : GDL.path_set -> GDL.path_set -> GDL.path_set
  val paths_intersect : GDL.path_set -> GDL.path_set -> GDL.path_set
  val paths_to_list : GDL.path_set -> GDL.path list
  val path_str : GDL.path -> string
  val ground_vars_at_paths :
    (GDL.clause -> GDL.literal list) ->
    (GDL.path * GDL.term list) list -> GDL.clause list -> GDL.clause list
  val blank_outside_subterm :
    (string * int) list -> GDL.path -> GDL.term -> GDL.term
  val blank_outside_subterms :
    (string * int) list -> (GDL.path * GDL.term) list -> GDL.term
  val refine_leaf_paths : GDL.path_set -> GDL.term list -> GDL.path_set
  val refine_paths_avoiding :
    GDL.path_set ->
    (GDL.term -> bool) -> (GDL.term -> bool) -> GDL.term list -> GDL.path_set
  type argpaths = (GDL.path * int) list list
  val find_rel_arg :
    GDL.term list -> GDL.term array -> (GDL.path * int) list -> GDL.term
  val complete_paths_for : GDL.path_set -> GDL.argpaths -> bool
end