diff options
| author | Erin van der Veen | 2018-07-06 13:40:19 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 13:40:19 +0200 |
| commit | 1b7dac92022193b4b051046d5d00fb9c1ee9ade0 (patch) | |
| tree | 08fc8e1e0fee3e3efeeafc3c4e74a7d51aa8e540 /Assignment2/src/Z3.icl | |
| parent | Reword totality constraint, add producing model to enumeration (diff) | |
| parent | Add properties to make transition probabilities remain in [0,1] (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment2/src/Z3.icl')
| -rw-r--r-- | Assignment2/src/Z3.icl | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl index cb054e1..b4b7326 100644 --- a/Assignment2/src/Z3.icl +++ b/Assignment2/src/Z3.icl @@ -1,11 +1,9 @@ implementation module Z3 -import System.Process -import Text - import StdString -import StdDebug +import System.Process +import Text :: Z3 = { handle :: ProcessHandle @@ -28,29 +26,26 @@ startZ3 w addAssert :: !Z3 !String !*World -> *World addAssert z3 s w -# (_, w) = writePipe (trace_s ("(assert " <+ s <+ ")\n")) z3.Z3.stdIn w +# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w = w addVariable :: !Z3 !String !*World -> *World addVariable z3 s w -# (_, w) = writePipe (trace_s ("(declare-const " <+ s <+ " Real)\n")) z3.Z3.stdIn w +# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w = w checkSat :: !Z3 !*World -> (!Bool, !*World) checkSat z3 w -# (_, w) = writePipe (trace_s "(check-sat)\n") z3.Z3.stdIn w +# (_, w) = writePipe "(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 w -# (_, w) = writePipe (trace_s "(get-model)\n") z3.Z3.stdIn w -# (_, w) = writePipe (trace_s "(exit)\n") z3.Z3.stdIn w +# (_, w) = writePipe "(get-model)\n" z3.Z3.stdIn w +# (_, w) = writePipe "(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 s s |