equal
deleted
inserted
replaced
60 |
60 |
61 @{ML_response_fake [display,gray] |
61 @{ML_response_fake [display,gray] |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
63 "(\<forall>x. P x, 1)"} |
63 "(\<forall>x. P x, 1)"} |
64 |
64 |
65 We used some pretty printing scaffolding to see better what the output is. |
65 In the print out of the tabel, we used some pretty printing scaffolding |
|
66 to see better which assignment the table contains. |
66 |
67 |
67 Having produced a propositional formula, you can now call the SAT solvers |
68 Having produced a propositional formula, you can now call the SAT solvers |
68 with the function @{ML "SatSolver.invoke_solver"}. For example |
69 with the function @{ML "SatSolver.invoke_solver"}. For example |
69 |
70 |
70 @{ML_response_fake [display,gray] |
71 @{ML_response_fake [display,gray] |
102 lemma "True" |
103 lemma "True" |
103 apply(tactic {* sat.sat_tac 1 *}) |
104 apply(tactic {* sat.sat_tac 1 *}) |
104 done |
105 done |
105 |
106 |
106 text {* |
107 text {* |
107 However, for proving anything more exciting you have to use a SAT solver |
108 However, for proving anything more exciting using @{ML "sat_tac" in sat} you |
108 that can produce a proof. The internal one is not usuable for this. |
109 have to use a SAT solver that can produce a proof. The internal |
|
110 one is not usuable for this. |
109 |
111 |
110 \begin{readmore} |
112 \begin{readmore} |
111 The interface for the external SAT solvers is implemented |
113 The interface for the external SAT solvers is implemented |
112 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
114 in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple |
113 SAT solver based on the DPLL algorithm. The tactics for SAT solvers are |
115 SAT solver based on the DPLL algorithm. The tactics for SAT solvers are |