1
2signature minisatProve = sig
3  exception SAT_cex of Thm.thm
4  val GEN_SAT : satConfig.sat_config -> Thm.thm
5  val SAT_PROVE : Term.term -> Thm.thm
6  val SAT_ORACLE : Term.term -> Thm.thm
7  val ZSAT_PROVE : Term.term -> Thm.thm
8  val ZSAT_ORACLE : Term.term -> Thm.thm
9end
10