Implement tranformation from a general linear CHC system into a transition system

[blishko]

This PR implements the translation from a general linear CHC system to a transition system. The implementation follows the algorithm described in the paper Horn2VMT: Translating Horn Reachability into Transition Systems https://www.osti.gov/servlets/purl/1783647

The idea is to use additional variable(s) to represent location in the graph induced by the CHC system and define a single transition relation with disjuncts representing each transition in the original system.

The solution to the transition system can be translated to a witness for the CHC system as follows:

1. From a TS error trace we can identify which locations were visited and which edges were used for each step of the trace. (The implementation currently identifies only locations. If there exists multiple edges between the source and target location, we bail out. The proper way is to check which disjunct of the transition relation was responsible for the step).
2. For an invariant we computed a projected invariant for each location by enabling the location and disabling all others. However, this can still leave unrelated variables in the formula. It is not yet clear to me what approach is best to deal with these variables. Currently, the implementation tries to find equivalent formula only over allowed variables using simplification techniques.

The transformation is enabled for BMC and IMC engines. For KIND, this approach does not work at the moment, because the transformation yields a safety property that is never k-inductive on its own. (The property says that error location is never reached). I think that for KIND a different way how to extend the algorithm to linear CHC systems is more appropriate. The transformation could work for PD-KIND which automatically strengthens the property.

[BritikovKI]

Btw, do you have the results for BMC or IMC with translation? Just to check the correctness in comparison with Z3 jic