equal
deleted
inserted
replaced
21 ["itself"=1, |
21 ["itself"=1, |
22 minsize=1, |
22 minsize=1, |
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 no_assms="false"] |
27 |
28 |
28 ML {* structure sat = SATFunc(cnf) *} |
29 ML {* structure sat = SATFunc(cnf) *} |
29 |
30 |
30 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
31 method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} |
31 "SAT solver" |
32 "SAT solver" |