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
File details
Details for the file tptp-0.0.3.dev2.tar.gz
.
File metadata
- Download URL: tptp-0.0.3.dev2.tar.gz
- Upload date:
- Size: 31.3 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/1.15.0 pkginfo/1.5.0.1 requests/2.22.0 setuptools/41.2.0 requests-toolbelt/0.9.1 tqdm/4.36.1 CPython/3.7.3
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 |
d462d7dc40118f1bfb0d63b663d467b495bd10c6a76da49e986648e78b4bd755
|
|
MD5 |
167dd84cea33cc7edcf20fef6284c0f7
|
|
BLAKE2b-256 |
463e87eda2aa3a485297769487586f6ac7b7195f95e51c358402190c86ce3d54
|
File details
Details for the file tptp-0.0.3.dev2-py3-none-any.whl
.
File metadata
- Download URL: tptp-0.0.3.dev2-py3-none-any.whl
- Upload date:
- Size: 45.2 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/1.15.0 pkginfo/1.5.0.1 requests/2.22.0 setuptools/41.2.0 requests-toolbelt/0.9.1 tqdm/4.36.1 CPython/3.7.3
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 |
e282aad090f0f2c0e7288dfdb92cfd0d85b71032fa34fe8845f7dcfbc3c232da
|
|
MD5 |
e3dbd48fddb775b0683bd56132dbe9fb
|
|
BLAKE2b-256 |
bd47aa5fb605fdf261c7f1096b4ed3526b1d9052712ecebb34d67809adddfba7
|