40 \<open>A\<close> and \<open>B\<close>, respectively. This assignment is recorded |
40 \<open>A\<close> and \<open>B\<close>, respectively. This assignment is recorded |
41 in the table that is given to the translation function and also returned |
41 in the table that is given to the translation function and also returned |
42 (appropriately updated) in the result. In the case above the |
42 (appropriately updated) in the result. In the case above the |
43 input table is empty (i.e.~@{ML Termtab.empty}) and the output table is |
43 input table is empty (i.e.~@{ML Termtab.empty}) and the output table is |
44 |
44 |
45 @{ML_response_fake [display,gray] |
45 @{ML_matchresult_fake [display,gray] |
46 "Termtab.dest table" |
46 "Termtab.dest table" |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
48 |
48 |
49 An index is also produced whenever the translation |
49 An index is also produced whenever the translation |
50 function cannot find an appropriate propositional formula for a term. |
50 function cannot find an appropriate propositional formula for a term. |
56 |
56 |
57 text \<open> |
57 text \<open> |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
58 returns @{ML "BoolVar 1" in Prop_Logic} for @{ML pform'} and the table |
59 @{ML table'} is: |
59 @{ML table'} is: |
60 |
60 |
61 @{ML_response_fake [display,gray] |
61 @{ML_matchresult_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 In the print out of the tabel, we used some pretty printing scaffolding |
65 In the print out of the tabel, we used some pretty printing scaffolding |
66 to see better which assignment the table contains. |
66 to see better which assignment the table contains. |
67 |
67 |
68 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 |
69 with the function @{ML "SAT_Solver.invoke_solver"}. For example |
69 with the function @{ML "SAT_Solver.invoke_solver"}. For example |
70 |
70 |
71 @{ML_response_fake [display,gray] |
71 @{ML_matchresult_fake [display,gray] |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
73 "SAT_Solver.SATISFIABLE assg"} |
73 "SAT_Solver.SATISFIABLE assg"} |
74 \<close> |
74 \<close> |
75 |
75 |
76 text \<open> |
76 text \<open> |
77 determines that the formula @{ML pform} is satisfiable. If we inspect |
77 determines that the formula @{ML pform} is satisfiable. If we inspect |
78 the returned function \<open>assg\<close> |
78 the returned function \<open>assg\<close> |
79 |
79 |
80 @{ML_response [display,gray] |
80 @{ML_matchresult [display,gray] |
81 "let |
81 "let |
82 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
82 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
83 in |
83 in |
84 (assg 1, assg 2, assg 3) |
84 (assg 1, assg 2, assg 3) |
85 end" |
85 end" |