kind2-mc/kind2 — pull request #101 by kevinclancy (2014-07-01 22:26:13+00:00)
Title: stateless stream reconstruction

a stream whose identifier occurrences do not occur under the pre operator is called stateless, because we do not need to store its value at one instance for use at later instances.

a stateless stream is eliminated as a pre-processing step by substituting the expression on the right-hand side of its definition for all occurrences of its identifier in other stream definitions. Stateless streams therefore do not occur in the results produced by the SMT solver. However, models of stateless streams can help the user understand the counterexamples that kind2 provides. Furthermore, the user is not aware of the preprocessing the kind2 does. Therefore, kind2 needs to rebuild stateless streams after a counterexample has been produced, which is what this modification accomplishes.

In addition, a few helper functions were added to the lib module. They are standard library functions in F#, and I felt that they were useful for accomplishing this task.