class ParallelProverBuilderCommand(BaseProverCommand, BaseModelBuilderCommand): (source)
Constructor: ParallelProverBuilderCommand(prover, modelbuilder, goal, assumptions)
This command stores both a prover and a model builder and when either prove() or build_model() is called, then both theorem tools are run in parallel. Whichever finishes first, the prover or the model builder, is the result that will be used.
Because the theorem prover result is the opposite of the model builder result, we will treat self._result as meaning "proof found/no model found".
Method | __init__ |
No summary |
Method | build |
Attempt to build a model. Store the result to prevent unnecessary re-building. |
Method | prove |
Perform the actual proof. Store the result to prevent unnecessary re-proving. |
Method | _run |
Undocumented |
Instance Variable | _result |
A holder for the result, to prevent unnecessary re-proving |
Inherited from BaseProverCommand
:
Method | decorate |
Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str |
Method | get |
Return the prover object :return: Prover |
Method | proof |
Return the proof string :param simplify: bool simplify the proof? :return: str |
Instance Variable | _proof |
Undocumented |
Instance Variable | _prover |
The theorem tool to execute with the assumptions |
Inherited from BaseModelBuilderCommand
(via BaseProverCommand
):
Method | get |
Return the model builder object :return: ModelBuilder |
Method | model |
Return a string representation of the model |
Method | _decorate |
No summary |
Instance Variable | _model |
Undocumented |
Instance Variable | _modelbuilder |
The theorem tool to execute with the assumptions |
Inherited from BaseTheoremToolCommand
(via BaseProverCommand
, BaseModelBuilderCommand
):
Method | add |
Add new assumptions to the assumption list. |
Method | assumptions |
List the current assumptions. |
Method | goal |
Return the goal |
Method | print |
Print the list of the current assumptions. |
Method | retract |
Retract assumptions from the assumption list. |
Instance Variable | _assumptions |
Undocumented |
Instance Variable | _goal |
Undocumented |
Parameters | |
prover:Prover | The theorem tool to execute with the assumptions |
modelbuilder | Undocumented |
goal | Undocumented |
assumptions | Undocumented |
See Also | |
BaseTheoremToolCommand |