31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty\<close> |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty\<close> |
32 |
32 |
33 text \<open> |
33 text \<open> |
34 then the resulting propositional formula @{ML pform} is |
34 then the resulting propositional formula @{ML pform} is |
35 |
35 |
36 @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} |
36 @{ML [display] \<open>Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)\<close> in Prop_Logic} |
37 |
37 |
38 |
38 |
39 where indices are assigned for the variables |
39 where indices are assigned for the variables |
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_matchresult_fake [display,gray] |
45 @{ML_matchresult_fake [display,gray] |
46 "Termtab.dest table" |
46 \<open>Termtab.dest table\<close> |
47 "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"} |
47 \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>} |
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. |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
51 Attempting to translate @{term "\<forall>x::nat. P x"} |
52 \<close> |
52 \<close> |
53 |
53 |
54 ML %grayML\<open>val (pform', table') = |
54 ML %grayML\<open>val (pform', table') = |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close> |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close> |
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 \<open>BoolVar 1\<close> in Prop_Logic} for @{ML pform'} and the table |
59 @{ML table'} is: |
59 @{ML table'} is: |
60 |
60 |
61 @{ML_matchresult_fake [display,gray] |
61 @{ML_matchresult_fake [display,gray] |
62 "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')" |
62 \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close> |
63 "(\<forall>x. P x, 1)"} |
63 \<open>(\<forall>x. P x, 1)\<close>} |
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 \<open>SAT_Solver.invoke_solver\<close>}. For example |
70 |
70 |
71 @{ML_matchresult_fake [display,gray] |
71 @{ML_matchresult_fake [display,gray] |
72 "SAT_Solver.invoke_solver \"minisat\" pform" |
72 \<open>SAT_Solver.invoke_solver "minisat" pform\<close> |
73 "SAT_Solver.SATISFIABLE assg"} |
73 \<open>SAT_Solver.SATISFIABLE assg\<close>} |
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_matchresult [display,gray] |
80 @{ML_matchresult [display,gray] |
81 "let |
81 \<open>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\<close> |
86 "(NONE, SOME true, NONE)"} |
86 \<open>(NONE, SOME true, NONE)\<close>} |
87 |
87 |
88 we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close> |
88 we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close> |
89 that makes the formula satisfiable. |
89 that makes the formula satisfiable. |
90 |
90 |
91 Note that we invoked the SAT solver with the string @{text [quotes] auto}. |
91 Note that we invoked the SAT solver with the string @{text [quotes] auto}. |