PDKIND: Add engine

[stepanhen]

Implement PDKIND Engine in Golem Solver

Overview

This pull request integrates the PDKIND (Property Directed K-Induction) algorithm into the Golem solver. The PDKIND algorithm is detailed in the IEEE paper.

PDKIND algorithm consists of 3 main methods:

• Reachable(k, F) - Checks reachability of formula F from initial states in k or fewer steps.
• Push() - Tries to construct an inductive strengthening of a property P or invalidate P.
• Solve() - Iteratively calls the Push() procedure to get strengthening of P or invalidate P, if there is no more strengthening, then the system is SAFE. If P is invalid, the system is UNSAFE.

In the paper, there were also mentioned two data structures that are needed for the methods mentioned above to run effectively. In this implementation, they are called:

• RFrame - Vector of formulas, where R[i] represents states that are i steps from initial states.
• InductionFrame - List of tuples (lemma, counterexample) where lemma holds for n steps and refutes counterexample.

The Reachable() method and RFrame were wrapped in a ReachabilityChecker class so that each instance of this class can construct and reuse its RFrame using the Reachable() method.

Validity witnesses were also implemented in this engine.

[blishko]

Implement PDKIND Engine in Golem Solver

Please move this description from the comment to the proper description of the PR.