Package nltk :: Package inference :: Module mace :: Class MaceCommand

type MaceCommand

                    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]

type MaceCommand

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

_convert2val(self, valuation_str)

_make_relation_set(num_entities, values) Static Method

_make_model_var(value) Static Method

_decorate_model(self, valuation_str, format)

_transform_output(self, valuation_str, format)

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

valuation

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

_make_relation_set(num_entities, values)
Static Method

_make_model_var(value)
Static Method

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