class documentation

A base decorator for the ModelBuilderCommand class from which other prover command decorators can extend.

Method __init__ No summary
Method build_model Attempt to build a model. Store the result to prevent unnecessary re-building.
Method get_model_builder Return the model builder object :return: ModelBuilder
Method model Return a string representation of the model
Method _decorate_model Modify and return the proof string :param valuation_str: str with the model builder's output :param format: str indicating the format for displaying :return: str
Instance Variable _model Undocumented
Instance Variable _result Undocumented

Inherited from TheoremToolCommandDecorator:

Method add_assumptions Add new assumptions to the assumption list.
Method assumptions List the current assumptions.
Method goal Return the goal
Method print_assumptions Print the list of the current assumptions.
Method retract_assumptions Retract assumptions from the assumption list.
Instance Variable _command Undocumented
def __init__(self, modelBuilderCommand): (source)
Parameters
modelBuilderCommandModelBuilderCommand to decorate
def build_model(self, verbose=False): (source)

Attempt to build a model. Store the result to prevent unnecessary re-building.

def get_model_builder(self): (source)

Return the model builder object :return: ModelBuilder

def model(self, format=None): (source)

Return a string representation of the model

Parameters
formatUndocumented
simplifybool simplify the proof?
Returns
str
def _decorate_model(self, valuation_str, format=None): (source)

Modify and return the proof string :param valuation_str: str with the model builder's output :param format: str indicating the format for displaying :return: str

Undocumented