Filling up the active container at the start under SOS is not doing full clause inter-reductions even if enabled.
We might want to do it for consistency, efficiency, and stronger invariants (e.g., "can't have two alpha-equivalent clauses in the forward subsumption index when FSub enabled, ...)
However, this is not a one-line fix, because forwardSimplify normally puts clause replacements into _newClauses from which travel to _unprocessed from which they normally go to _passive. So this long clause dispatch would need to be duplicated for the sake of addInputSOSClause or parametrized.
Filling up the active container at the start under SOS is not doing full clause inter-reductions even if enabled.
We might want to do it for consistency, efficiency, and stronger invariants (e.g., "can't have two alpha-equivalent clauses in the forward subsumption index when FSub enabled, ...)
However, this is not a one-line fix, because
forwardSimplify
normally puts clause replacements into_newClauses
from which travel to_unprocessed
from which they normally go to_passive
. So this long clause dispatch would need to be duplicated for the sake ofaddInputSOSClause
or parametrized.