Embedded Files
A program to check satisfiability of formulae in the union of EUF and list theories.
It uses the congruence closure algorithm by Nelson - Oppen.
See my blog at http://lamacchinadituring.blogspot.com/ for more informations.
Screenshots of the ListSAT GUI
Page updated
Google Sites
Report abuse