A library for handling TPTP related input and systems
Project description
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 printedMySolver
- when invoked to solve the problem
absolute/path/SYN001+1.p
within a timeout of60
seconds the program/shellscriptmy-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
...
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for tptp-0.0.3.dev2-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | e282aad090f0f2c0e7288dfdb92cfd0d85b71032fa34fe8845f7dcfbc3c232da |
|
MD5 | e3dbd48fddb775b0683bd56132dbe9fb |
|
BLAKE2b-256 | bd47aa5fb605fdf261c7f1096b4ed3526b1d9052712ecebb34d67809adddfba7 |