Package nltk :: Package inference :: Module prover9 :: Class Prover9Parent
[hide private]
[frames] | no frames]

type Prover9Parent

source code

object --+
         |
        Prover9Parent
Known Subclasses:

A common class extended by both Prover9 and Mace. It contains the functionality required to convert NLTK-style expressions into Prover9-style expressions.

Instance Methods [hide private]
 
config_prover9(self, binary_location, verbose=False) source code
 
prover9_input(self, goal, assumptions)
Returns: The input string that should be provided to the prover9 binary.
source code
 
binary_locations(self)
A list of directories that should be searched for the prover9 executables.
source code
 
_find_binary(self, name, verbose=False) source code
 
_call(self, input_str, binary, args=[], verbose=False)
Call the binary with the given input.
source code
 
__init__(self, timeout=60)
Class Variables [hide private]
  _binary_location = None
A common class extended by both Prover9 and Mace.
Instance Variables [hide private]
  _timeout
The timeout value for prover9.
Method Details [hide private]

prover9_input(self, goal, assumptions)

source code 
Returns:
The input string that should be provided to the prover9 binary. This string is formed based on the goal, assumptions, and timeout value of this object.

binary_locations(self)

source code 

A list of directories that should be searched for the prover9 executables. This list is used by config_prover9 when searching for the prover9 executables.

_call(self, input_str, binary, args=[], verbose=False)

source code 

Call the binary with the given input.

Parameters:
  • input_str - A string whose contents are used as stdin.
  • binary - The location of the binary to call
  • args - A list of command-line arguments.
Returns:
A tuple (stdout, returncode)

See Also: config_prover9

__init__(self, timeout=60)
(Constructor)

 
Overrides: object.__init__
(inherited documentation)

Class Variable Details [hide private]

_binary_location

A common class extended by both Prover9 and Mace. It contains the functionality required to convert NLTK-style expressions into Prover9-style expressions.

Value:
None

Instance Variable Details [hide private]

_timeout

The timeout value for prover9. If a proof can not be found in this amount of time, then prover9 will return false. (Use 0 for no timeout.)