ProgTutorial/Recipes/Sat.thy
changeset 562 daf404920ab9
parent 556 3c214b215f7e
child 565 cecd7a941885
equal deleted inserted replaced
561:aec7073d4645 562:daf404920ab9
    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}.