Package nltk :: Package inference :: Module mace :: Class MaceCommand
[hide private]
[frames] | no frames]

type MaceCommand

source code

                    object --+    
                             |    
  prover9.Prover9CommandParent --+
                                 |
            object --+           |
                     |           |
api.TheoremToolCommand --+       |
                         |       |
api.BaseTheoremToolCommand --+   |
                             |   |
            object --+       |   |
                     |       |   |
api.TheoremToolCommand --+   |   |
                         |   |   |
   api.ModelBuilderCommand --+   |
                             |   |
   api.BaseModelBuilderCommand --+
                                 |
                                MaceCommand

A MaceCommand specific to the Mace model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats.

Instance Methods [hide private]
 
__init__(self, goal=None, assumptions=None, max_models=500, model_builder=None) source code
nltk.sem.Valuation
_convert2val(self, valuation_str)
Transform the output file into an NLTK-style Valuation.
source code
 
_decorate_model(self, valuation_str, format)
Print out a Mace4 model using any Mace4 interpformat format.
source code
 
_transform_output(self, valuation_str, format)
Transform the output file into any Mace4 interpformat format.
source code
 
_call_interpformat(self, input_str, args=[], verbose=False)
Call the interpformat binary with the given input.
source code

Inherited from prover9.Prover9CommandParent: print_assumptions

Inherited from api.BaseModelBuilderCommand: build_model, get_model_builder, model

Inherited from api.BaseTheoremToolCommand: add_assumptions, assumptions, goal, retract_assumptions

Static Methods [hide private]
 
_make_relation_set(num_entities, values)
Convert a Mace4-style relation table into a dictionary.
source code
 
_make_relation_tuple(position, values, num_entities) source code
 
_make_model_var(value)
Pick an alphabetic character as identifier for an entity in the model.
source code
Class Variables [hide private]
  _interpformat_bin = None
Instance Variables [hide private]

Inherited from api.BaseModelBuilderCommand (private): _modelbuilder

Inherited from api.BaseTheoremToolCommand (private): _result

Properties [hide private]
  valuation
valuation
Method Details [hide private]

__init__(self, goal=None, assumptions=None, max_models=500, model_builder=None)
(Constructor)

source code 
Parameters:
  • goal (logic.Expression) - Input expression to prove
  • assumptions (list of logic.Expression) - Input expressions to use as assumptions in the proof.
  • max_models (int) - The maximum number of models that Mace will try before simply returning false. (Use 0 for no maximum.)
Overrides: api.BaseTheoremToolCommand.__init__

_convert2val(self, valuation_str)

source code 

Transform the output file into an NLTK-style Valuation.

Returns: nltk.sem.Valuation
A model if one is generated; None otherwise.

_make_relation_set(num_entities, values)
Static Method

source code 

Convert a Mace4-style relation table into a dictionary.

Parameters:
  • num_entities (int) - the number of entities in the model; determines the row length in the table.
  • values (list of int) - a list of 1's and 0's that represent whether a relation holds in a Mace4 model.

_make_model_var(value)
Static Method

source code 

Pick an alphabetic character as identifier for an entity in the model.

Parameters:
  • value (int) - where to index into the list of characters

_decorate_model(self, valuation_str, format)

source code 

Print out a Mace4 model using any Mace4 interpformat format. See http://www.cs.unm.edu/~mccune/mace4/manual/ for details.

Parameters:
  • valuation_str - str with the model builder's output
  • format - str indicating the format for displaying models. Defaults to 'standard' format.
Returns:
str
Overrides: api.BaseModelBuilderCommand._decorate_model

_transform_output(self, valuation_str, format)

source code 

Transform the output file into any Mace4 interpformat format.

Parameters:
  • format (str) - Output format for displaying models.

_call_interpformat(self, input_str, args=[], verbose=False)

source code 

Call the interpformat binary with the given input.

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

See Also: config_prover9


Property Details [hide private]

valuation

valuation