equal
deleted
inserted
replaced
23 maxsize=8, |
23 maxsize=8, |
24 maxvars=10000, |
24 maxvars=10000, |
25 maxtime=60, |
25 maxtime=60, |
26 satsolver="auto"] |
26 satsolver="auto"] |
27 |
27 |
28 ML {* structure sat = SATFunc(structure cnf = cnf); *} |
28 ML {* structure sat = SATFunc(cnf) *} |
29 |
29 |
30 method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *} |
30 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
31 "SAT solver" |
31 "SAT solver" |
32 |
32 |
33 method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *} |
33 method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *} |
34 "SAT solver (with definitional CNF)" |
34 "SAT solver (with definitional CNF)" |
35 |
35 |
36 end |
36 end |