Skip to main content
Join the official 2019 Python Developers SurveyStart the survey!

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 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
...

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for tptp, version 0.0.3.dev2
Filename, size File type Python version Upload date Hashes
Filename, size tptp-0.0.3.dev2-py3-none-any.whl (45.2 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size tptp-0.0.3.dev2.tar.gz (31.3 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page