summaryrefslogtreecommitdiff
path: root/Assignment2/src/Z3.icl
diff options
context:
space:
mode:
authorCamil Staps2018-07-06 20:30:57 +0200
committerCamil Staps2018-07-06 20:30:57 +0200
commitf3ddb0cfc208f3ce35d1005bbf8a22e8f3cdd779 (patch)
tree8dab04e1992d1d62cfd9f76ec481c8ae3874fa5c /Assignment2/src/Z3.icl
parentShortcommings of our own tool (diff)
Prevent division by zero in Z3
Diffstat (limited to 'Assignment2/src/Z3.icl')
-rw-r--r--Assignment2/src/Z3.icl10
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