tptp 0.0.3.dev2

Description:

tptp 0.0.3.dev2

A TPTP python package
Installation

install python >= 3.5
clone this repository

Usage
Run locally:
List all solvers
python3 -m tptp local list-solvers

Run Leo III.
$ python3 -m tptp local run --solver-name leo3 --problem problems/SYN001+1.p --timeout 60

Run cvc4
$ python3 -m tptp local run --solver-name cvc4 --problem problems/SYN001+1.p --timeout 60

Run System-on-TPTP:
List all solvers
$ python3 -m tptp system-on-tptp list-solvers

Run Leo III.
$ python3 -m tptp system-on-tptp request --solver-name "Leo-III---1.4" --solver-command "run_Leo-III %s %d" --problem "problems/SYN001+1.p"

Test the competition mode
$ python3 -m tptp competition competition-test/definition.py

Run with more output. Good for error tracking.
$ python3 -m tptp competition competition-test/definition.py --verbose

Making a solver TPTP ready
SZS Status, SZS Ontology
A solver can be used by this libary if it supports the SZS Ontology as its result on the stdout.
The solution status should be reported exactly once, in a line starting % SZS status" (the leading '%' makes the line into a TPTP language comment).
For instance, a SAT-solver started for problem SYN001+1 should output the line
% SZS status Satisfiable for SYN001+1

as part of its output if it proves the problem is satisfiable.
Consequently:

if your solver proves the problem is unsatisfiable, the line % SZS status Unsatisfiable for SYN001+1.
if your solver gaves up the prove, the line % SZS status GaveUp for SYN001+1.
a full list of possible values for the SZS Status can be found at the SZS Ontology definition.

Any prove or prove-model should additionally be printed on the stdout in the following form.
% SZS output start CNFRefutation for SYN001+1
...
% SZS output end CNFRefutation for SYN001+1

Test your solver
To test your solve add it to our test competition, which can be found at
competition-test/definition.py

Here you add your solver to the SOLVERS constant
SOLVERS = (
...
{
'type': 'local',
'name': 'my-solver',
'pretty-name': 'MySolver'
'command': 'my-solver-binary-or-shell-script %s -t %d',
},
...
)

This will ensure that your solver

is called my-solver and is pretty printed MySolver
when invoked to solve the problem absolute/path/SYN001+1.p within a timeout of 60 seconds the
program/shellscript my-solver-binary-or-shell-script "absolute/path/SYN001+1.p" -t 60 is called
your problem should output an SZS Status from the SZS Ontology (see above)

Running our test competition should now list your solver.
$ python3 -m tptp competition competition-test/definition.py
...
% Satisfiable for Sat1.cnf expecting Satisfiable with MySolver -t 60s which is correct
...