diff options
author | Camil Staps | 2018-07-06 20:30:57 +0200 |
---|---|---|
committer | Camil Staps | 2018-07-06 20:30:57 +0200 |
commit | f3ddb0cfc208f3ce35d1005bbf8a22e8f3cdd779 (patch) | |
tree | 8dab04e1992d1d62cfd9f76ec481c8ae3874fa5c /Assignment2/src/Z3.icl | |
parent | Shortcommings of our own tool (diff) |
Prevent division by zero in Z3
Diffstat (limited to 'Assignment2/src/Z3.icl')
-rw-r--r-- | Assignment2/src/Z3.icl | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl index ca869a1..4db349e 100644 --- a/Assignment2/src/Z3.icl +++ b/Assignment2/src/Z3.icl @@ -1,5 +1,7 @@ implementation module Z3 +import StdList +import StdMisc import StdString import System.Process @@ -43,13 +45,17 @@ addVariable z3 type s w # (_, w) = writePipe (trace_id $ "(declare-const " <+ s <+ " " <+ type <+ ")\n") z3.Z3.stdIn w = w -checkSat :: !Z3 !*World -> (!Bool, !*World) +checkSat :: !Z3 !*World -> (!Satisfaction, !*World) checkSat z3 w # (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w # (out, w) = readPipeBlocking z3.Z3.stdOut w # out = fromOk out # out = trace_id out -= (endsWith "sat\n" out, w) += (case last $ init $ split "\n" out of + "sat" -> Sat + "unsat" -> Unsat + "unknown" -> Unknown + _ -> abort "Z3 failed\n", w) getModel :: !Z3 !*World -> (!String, !*World) getModel z3 w |