We introduce an option to solv linear systems in BMC without first converting them to a transition system.
The idea for the implementation is the following.
We unroll the CHC system and keep track if we can reach node V in level L. We collect all such reachable nodes in a frontier and in each step compute the next frontier. Before a node is included in the next frontier, we check if it can truly be reached. We introduce only one version of the node, even if it can reached by multiple paths. Furthermore, we include the conditions that of a node V has been reached in level L, then one of the successors of V has to be reached in level L+1. Similarly, we include the conditions that if node V has been reached in level L+1, then one of its predecessors must have been reached in level L.
The experiments did not show an improvement over the TS version, so we hide this implementation behind --experimental flag.
We introduce an option to solv linear systems in BMC without first converting them to a transition system. The idea for the implementation is the following. We unroll the CHC system and keep track if we can reach node V in level L. We collect all such reachable nodes in a frontier and in each step compute the next frontier. Before a node is included in the next frontier, we check if it can truly be reached. We introduce only one version of the node, even if it can reached by multiple paths. Furthermore, we include the conditions that of a node V has been reached in level L, then one of the successors of V has to be reached in level L+1. Similarly, we include the conditions that if node V has been reached in level L+1, then one of its predecessors must have been reached in level L.
The experiments did not show an improvement over the TS version, so we hide this implementation behind
--experimentalflag.