Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot | |
- include directive works - no keyword : 'fof', 'cnf', ... can be used for symbols name - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted) - same thing for string But: - string not distinct by projection to real, not sure if the current state of string theory make them distinct - filtering in include is not done - the result is not printed in the TPTP way (currently SMT2 way) |