summaryrefslogtreecommitdiff
path: root/Assignment2/src/Z3.icl
diff options
context:
space:
mode:
authorCamil Staps2018-07-06 13:27:35 +0200
committerCamil Staps2018-07-06 13:27:35 +0200
commit0a8bd9594f346c0d8fbfea1de729f1ca5a8005b6 (patch)
treef2539018b9163dec0ec4c980447397dd36fcfebf /Assignment2/src/Z3.icl
parentGet model if satisfiable (diff)
Cleanup
Diffstat (limited to 'Assignment2/src/Z3.icl')
-rw-r--r--Assignment2/src/Z3.icl19
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