equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/sat_solver.ML |
1 (* Title: HOL/Tools/sat_solver.ML |
2 Author: Tjark Weber |
2 Author: Tjark Weber |
3 Copyright 2004-2009 |
3 Copyright 2004-2009 |
4 |
4 |
5 Interface to external SAT solvers, and (simple) built-in SAT solvers. |
5 Interface to external SAT solvers, and (simple) built-in SAT solvers. |
|
6 |
|
7 Relevant Isabelle environment settings: |
|
8 |
|
9 # MiniSat 1.14 |
|
10 #MINISAT_HOME=/usr/local/bin |
|
11 |
|
12 # zChaff |
|
13 #ZCHAFF_HOME=/usr/local/bin |
|
14 |
|
15 # BerkMin561 |
|
16 #BERKMIN_HOME=/usr/local/bin |
|
17 #BERKMIN_EXE=BerkMin561-linux |
|
18 #BERKMIN_EXE=BerkMin561-solaris |
|
19 |
|
20 # Jerusat 1.3 |
|
21 #JERUSAT_HOME=/usr/local/bin |
6 *) |
22 *) |
7 |
23 |
8 signature SAT_SOLVER = |
24 signature SAT_SOLVER = |
9 sig |
25 sig |
10 exception NOT_CONFIGURED |
26 exception NOT_CONFIGURED |