Mira-Craig

| Beteiligte Mitarbeiter | Beschreibung |

Die statisch gelinkte Library libcraigsolver.a stellt eine Schnittstelle zur Verfügung mit Hilfe derer Craigsche Interpolanten und sogenannte UNSAT Cores berechnet werden können. Die berechneten Interpolanten können in Konjunktiver Normalen Form (KNF) zurückgegeben werden, dazu wird die eigentliche Interpolante Tseitin-kodiert. Der in dieser Library enthaltene SAT Solver ist MiraXT.