Metadata-Version: 2.1
Name: tptp
Version: 0.0.3.dev2
Summary: A library for handling TPTP related input and systems
Home-page: https://github.com/leoprover/tptp
Author: Tobias Gleißner
Author-email: tobias.gleissner@fu-berlin.de
License: BSD3
Platform: UNKNOWN
Classifier: Development Status :: 2 - Pre-Alpha
Classifier: Environment :: Console
Classifier: Environment :: Web Environment
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Information Technology
Classifier: Intended Audience :: Legal Industry
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Programming Language :: Python :: 3.5
Classifier: Programming Language :: Python :: 3.6
Classifier: Programming Language :: Python :: 3.7
Classifier: Programming Language :: Python :: 3.8
Classifier: Programming Language :: Python :: 3.9
Requires-Python: >=3.5
Description-Content-Type: text/markdown
Requires-Dist: pathlib
Requires-Dist: lxml
Requires-Dist: requests
Requires-Dist: colorama

# 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](http://www.tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology) 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
```python
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
...
```


