Module TranslateFormula

module TranslateFormula: sig .. end
Translating formulas from GDL to Toss.

val no_root_predicates : bool Pervasives.ref
Whether to add root predicates. Note that not adding root predicates no_root_predicates := true will violate correctness of some translations.
type transl_data = {
   f_paths :GDL.path_set; (*fluent paths*)
   c_paths :GDL.path_set; (*coordinate paths*)
   all_paths :GDL.path_set; (*sum of f_paths and c_paths*)
   root_reps :GDL.term list; (*root terms*)
   counters :string list;
   num_functions :(string * Formula.real_expr) list;
   defined_rels :string list;
   argpaths :(string * (GDL.path list array, GDL.argpaths) Aux.choice) list; (*Left argpaths are coordinating relation argument paths, Right argpaths is fact relation argument partition.*)
   term_arities :(string * int) list;
val blank_out : transl_data -> GDL.term -> GDL.term
val var_of_term : transl_data -> GDL.term -> Formula.const_or_fo_var
val empty_transl_data : transl_data
val separate_disj : string list ->
GDL.literal list list ->
(GDL.literal list * GDL.literal list * GDL.literal list) list
Exposed for testing purposes only.
val translate : ?counter_guard:bool ->
?ctx_terms:GDL.term list ->
transl_data -> GDL.literal list list -> Formula.formula
Translate a disjunction of conjunctions of literals (and disjs of lits). counter_guard is set to false, do not introduce "gdl__counter(gdl__counter)" atom.

ctx_terms is additional state terms for translating a formula with a broader context (e.g. the update condition in the context of rewrite rule application).

val build_defrels : transl_data ->
GDL.clause list -> (string * (string list * Formula.formula)) list