Translation of formulas to the syntax of Prover9 and Mace4.
Deprecated: use LogicUS.FOL.Prover9Mace4, which builds the whole input file with readable symbol names and
reads Mace4 models back. This module is kept for compatibility.
Like ffol2P9M4Str, but it receives and returns the renaming tables, so that several formulas can share them.
The record holds, for variables (vi, vdic), predicates (pi, pdic), functions (fi, fdic) and constants
(ci, cdic), the next free index and the dictionary from each original symbol to its index. The symbols are written
as A, B, ... (variables), P0, P1, ... (predicates), f0, f1, ... (functions) and c0, c1, ... (constants).
Start with every index at 0 and every dictionary empty. (Deprecated: use LogicUS.FOL.Prover9Mace4.)
It translates a set of formulas to Prover9/Mace4 syntax, one per line, with the same renaming as ffol2P9M4Str. (Deprecated.)
Like sfol2P9M4Str, but it receives and returns the renaming tables, so several sets can share them. (Deprecated.)
It translates a formula to Prover9/Mace4 syntax keeping the symbol names between quotes. (Deprecated.)
It translates a set of formulas to Prover9/Mace4 syntax keeping the symbol names between quotes. (Deprecated.)
It translates a formula to Prover9/Mace4 syntax, renaming predicates, functions, constants and variables to P0, f0, c0, A, B... (Deprecated.)