In abduce, allow switching to SIM_MANDATORY not at the sim root #214
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Currently, during simulated backward chaining, it is possible for a goal to have an "opposite" match to a RHS. In this case, the
abduce
method sets the simulation mode toSIM_MANDATORY
:Note that it does this when backward chaining first begins at the root. But it is possible to have an opposite match at later steps in the backward chaining, for example to match the anti-fact RHS of a strong requirement. We want this to create a mandatory solution also.
This pull request updates the logic in
abduce
to allow the simulation mode to switch to mandatory at steps other than the simulation root. If the simulation mode isSIM_OPTIONAL
, it means that backward chaining has not previously had an opposite match, so we switch toSIM_MANDATORY
if the current match is opposite, similar to the case forSIM_ROOT
. If the simulation mode is alreadySIM_MANDATORY
and the current match is not an opposite match, thenabduce
simply continues with the backward chaining.However, if the simulation mode is already
SIM_MANDATORY
and the current match is opposite, then it means that backward chaining would have two opposite matches. We don't have a use case for this yet and it is not clear what the logic should be, so we don't allow this case.