Encode the DPJ rules in an SMT solver

[reprogrammer]

To be able to use an off-the-shelf SMT solver, we have to write the DPJ rules as boolean formula. Then, we can combine the constraints generated by DPJizer with the rules of DPJ and solve them using an SMT solver.