ATP.Prover

Models of automated theorem provers.

Documentation

data Vendor

The implementation of a theorem prover, supported by atp.

Constructors

E

Vampire

Instances

Bounded Vendor

Defined in ATP.Prover

Methods

minBound :: Vendor

maxBound :: Vendor

Enum Vendor

Defined in ATP.Prover

Methods

succ :: Vendor -> Vendor

pred :: Vendor -> Vendor

toEnum :: Int -> Vendor

fromEnum :: Vendor -> Int

enumFrom :: Vendor -> [Vendor]

enumFromThen :: Vendor -> Vendor -> [Vendor]

enumFromTo :: Vendor -> Vendor -> [Vendor]

enumFromThenTo :: Vendor -> Vendor -> Vendor -> [Vendor]

Eq Vendor

Defined in ATP.Prover

Methods

(==) :: Vendor -> Vendor -> Bool

(/=) :: Vendor -> Vendor -> Bool

Ord Vendor

Defined in ATP.Prover

Methods

compare :: Vendor -> Vendor -> Ordering

(<) :: Vendor -> Vendor -> Bool

(<=) :: Vendor -> Vendor -> Bool

(>) :: Vendor -> Vendor -> Bool

(>=) :: Vendor -> Vendor -> Bool

max :: Vendor -> Vendor -> Vendor

min :: Vendor -> Vendor -> Vendor

Show Vendor

Defined in ATP.Prover

Methods

showsPrec :: Int -> Vendor -> ShowS

show :: Vendor -> String

showList :: [Vendor] -> ShowS

data Prover

The automated theorem prover.

Constructors

Prover

Fields

• vendor :: Vendor
• executable :: FilePath

Instances

Eq Prover

Defined in ATP.Prover

Methods

(==) :: Prover -> Prover -> Bool

(/=) :: Prover -> Prover -> Bool

Ord Prover

Defined in ATP.Prover

Methods

compare :: Prover -> Prover -> Ordering

(<) :: Prover -> Prover -> Bool

(<=) :: Prover -> Prover -> Bool

(>) :: Prover -> Prover -> Bool

(>=) :: Prover -> Prover -> Bool

max :: Prover -> Prover -> Prover

min :: Prover -> Prover -> Prover

Show Prover

Defined in ATP.Prover

Methods

showsPrec :: Int -> Prover -> ShowS

show :: Prover -> String

showList :: [Prover] -> ShowS

type TimeLimit = Int

The time limit allocated to the prover, in seconds.

type MemoryLimit = Int

The memory limit allocated to the prover, in Mb.

proverArguments :: Vendor -> TimeLimit -> MemoryLimit -> [String]

Build the list of command line arguments for the given prover.

proverOutput

Arguments

:: Vendor

-> ExitCode

-> Text

Standard out

-> Text

Standard error

-> Partial Text

Interpret the output of the theorem prover from its exit code and the contents of the returned stdout and stderr.

vampire :: Prover

The Vampire theorem prover.

eprover :: Prover

The E theorem prover.

defaultProver :: Prover

The default prover used by refute and prove.

>>> defaultProver
Prover {vendor = E, executable = "eprover"}