equal
deleted
inserted
replaced
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_response [display,gray] |
46 \<open>Termtab.dest table\<close> |
46 \<open>Termtab.dest table\<close> |
47 \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>} |
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. |
56 |
56 |
57 text \<open> |
57 text \<open> |
58 returns @{ML \<open>BoolVar 1\<close> 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_response [display,gray] |
62 \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close> |
62 \<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\<close> |
63 \<open>(\<forall>x. P x, 1)\<close>} |
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 |