16 is based on the DPLL algorithm.\smallskip |
16 is based on the DPLL algorithm.\smallskip |
17 |
17 |
18 The SAT solvers expect a propositional formula as input and produce |
18 The SAT solvers expect a propositional formula as input and produce |
19 a result indicating that the formula is either satisfiable, unsatisfiable or |
19 a result indicating that the formula is either satisfiable, unsatisfiable or |
20 unknown. The type of the propositional formula is |
20 unknown. The type of the propositional formula is |
21 @{ML_type "PropLogic.prop_formula"} with the usual constructors such |
21 @{ML_type "Prop_Logic.prop_formula"} with the usual constructors such |
22 as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on. |
22 as @{ML And in Prop_Logic}, @{ML Or in Prop_Logic} and so on. |
23 |
23 |
24 The function @{ML PropLogic.prop_formula_of_term} translates an Isabelle |
24 The function @{ML Prop_Logic.prop_formula_of_term} translates an Isabelle |
25 term into a propositional formula. Let |
25 term into a propositional formula. Let |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
26 us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. |
27 The function will return a propositional formula and a table. Suppose |
27 The function will return a propositional formula and a table. Suppose |
28 *} |
28 *} |
29 |
29 |
30 ML{*val (pform, table) = |
30 ML{*val (pform, table) = |
31 PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
31 Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"} Termtab.empty*} |
32 |
32 |
33 text {* |
33 text {* |
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 PropLogic} |
36 @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} |
37 |
37 |
38 |
38 |
39 where indices are assigned for the variables |
39 where indices are assigned for the variables |
40 @{text "A"} and @{text "B"}, respectively. This assignment is recorded |
40 @{text "A"} and @{text "B"}, 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 |
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 *} |
52 *} |
53 |
53 |
54 ML{*val (pform', table') = |
54 ML{*val (pform', table') = |
55 PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
55 Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty*} |
56 |
56 |
57 text {* |
57 text {* |
58 returns @{ML "BoolVar 1" in PropLogic} 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_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)"} |