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_response_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 *} |
74 |
75 |
|
76 text {* |
75 determines that the formula @{ML pform} is satisfiable. If we inspect |
77 determines that the formula @{ML pform} is satisfiable. If we inspect |
76 the returned function @{text assg} |
78 the returned function @{text assg} |
77 |
79 |
78 @{ML_response [display,gray] |
80 @{ML_response [display,gray] |
79 "let |
81 "let |
80 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
82 val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform |
81 in |
83 in |
82 (assg 1, assg 2, assg 3) |
84 (assg 1, assg 2, assg 3) |
83 end" |
85 end" |
84 "(SOME true, SOME true, NONE)"} |
86 "(NONE, SOME true, NONE)"} |
85 |
87 |
86 we obtain a possible assignment for the variables @{text "A"} an @{text "B"} |
88 we obtain a possible assignment for the variables @{text "A"} an @{text "B"} |
87 that makes the formula satisfiable. |
89 that makes the formula satisfiable. |
88 |
90 |
89 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}. |