diff options
author | Erin van der Veen | 2018-07-06 13:08:47 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-07-06 13:08:47 +0200 |
commit | b3b88892e39ab7e754d9a3429d8db0356869e3ac (patch) | |
tree | 8c7b15a47c34afa044c03978af8c6bae736ebef0 /Assignment2/src/Z3.icl | |
parent | Change var naming, change order of commands to Z3 (diff) |
Debug smt2 statements
Diffstat (limited to 'Assignment2/src/Z3.icl')
-rw-r--r-- | Assignment2/src/Z3.icl | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl index 0bef921..2efe664 100644 --- a/Assignment2/src/Z3.icl +++ b/Assignment2/src/Z3.icl @@ -14,7 +14,7 @@ import StdDebug , stdErr :: ReadPipe } -startZ3 :: *World -> (Z3, *World) +startZ3 :: !*World -> (!Z3, !*World) startZ3 w # (err, w) = runProcessIO "z3" ["-smt2", "-in"] Nothing w # (handle, {ProcessIO | stdIn, stdOut, stdErr}) = fromOk err @@ -26,28 +26,31 @@ startZ3 w } = (z3, w) -addAssert :: Z3 String *World -> *World +addAssert :: !Z3 !String !*World -> *World addAssert z3 s w -# (_, w) = writePipe ("(assert (" <+ s <+ "))\n") z3.Z3.stdIn w +# (_, w) = writePipe (trace_s ("(assert " <+ s <+ ")\n")) z3.Z3.stdIn w = w -addVariable :: Z3 String *World -> *World +addVariable :: !Z3 !String !*World -> *World addVariable z3 s w -# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w +# (_, w) = writePipe (trace_s ("(declare-const " <+ s <+ " Real)\n")) z3.Z3.stdIn w = w -checkSat :: Z3 *World -> (Bool, *World) +checkSat :: !Z3 !*World -> (!Bool, !*World) checkSat z3 w -# (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w +# (_, w) = writePipe (trace_s "(check-sat)\n") z3.Z3.stdIn w # (out, w) = readPipeBlocking z3.Z3.stdOut w # out = fromOk out = (startsWith "sat" out, w) -getModel :: Z3 *World -> (String, *World) +getModel :: !Z3 !*World -> (!String, !*World) getModel z3 w -# (_, w) = writePipe "(get-model)\n" z3.Z3.stdIn w -# (_, w) = writePipe "(exit)\n" z3.Z3.stdIn w +# (_, w) = writePipe (trace_s "(get-model)\n") z3.Z3.stdIn w +# (_, w) = writePipe (trace_s "(exit)\n") z3.Z3.stdIn w # (_, w) = waitForProcess z3.Z3.handle w # (out, w) = readPipeNonBlocking z3.Z3.stdOut w # out = fromOk out = (out, w) + +trace_s :: String -> String +trace_s s = trace_n s s |