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