Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-09-18 | SMT-LIBv2 compliance regarding outputting "unknown". | Morgan Deters | |
Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.) | |||
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) |