equal
deleted
inserted
replaced
63 val trace = Attrib.setup_config_bool @{binding sat_trace} (K false); |
63 val trace = Attrib.setup_config_bool @{binding sat_trace} (K false); |
64 |
64 |
65 fun cond_tracing ctxt msg = |
65 fun cond_tracing ctxt msg = |
66 if Config.get ctxt trace then tracing (msg ()) else (); |
66 if Config.get ctxt trace then tracing (msg ()) else (); |
67 |
67 |
68 val solver = Attrib.setup_config_string @{binding sat_solver} (K "zchaff_with_proofs"); |
68 val solver = Attrib.setup_config_string @{binding sat_solver} (K "dpll_p"); |
69 (*see HOL/Tools/sat_solver.ML for possible values*) |
69 (*see HOL/Tools/sat_solver.ML for possible values*) |
70 |
70 |
71 val counter = Unsynchronized.ref 0; |
71 val counter = Unsynchronized.ref 0; |
72 |
72 |
73 val resolution_thm = |
73 val resolution_thm = |