Subproject

H1/2

Categories

Core algorithms

Overview

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.

Publications

---

Benchmarks

---

Download

Click here for the library.

Manual

After extracting the archive you will find a directory called "example". This directory provides further compile instructions. In the file "example.cpp" you can see how this interface can be used.

Status

Stable