Mira-Craig

| project staff | description |

The statically linked library libcraigsolver.a provides an interface to a SAT solver that can generate Craig interpolants and can also compute UNSAT cores. The computed Craig interpolants can be obtained in conjunctive normal form (CNF), i.e. the solver performs a so-called Tseitin-transformation to the computed Craig interpolant. The underlying SAT solver used in this library is MiraXT.