Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

2 files changed, 66 insertions, 0 deletions

diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl
new file mode 100644
index 0000000..0329987
--- /dev/null
+++ b/Assignment2/src/Z3.dcl
@@ -0,0 +1,13 @@
+definition module Z3
+
+from System.Process import :: ProcessHandle, :: ProcessIO
+
+:: Z3
+
+startZ3 :: *World -> (Z3, *World)
+addAssert :: Z3 String *World -> *World
+addVariable :: Z3 String *World -> *World
+checkSat :: Z3 *World -> (Bool, *World)
+
+// Note: getModel terminates z3
+getModel :: Z3 *World -> (String, *World)
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
new file mode 100644
index 0000000..0bef921
--- /dev/null
+++ b/Assignment2/src/Z3.icl
@@ -0,0 +1,53 @@
+implementation module Z3
+
+import System.Process
+import Text
+
+import StdString
+
+import StdDebug
+
+:: Z3 =
+	{ handle :: ProcessHandle
+	, stdIn  :: WritePipe
+	, stdOut :: ReadPipe
+	, stdErr :: ReadPipe
+	}
+
+startZ3 :: *World -> (Z3, *World)
+startZ3 w
+# (err, w) = runProcessIO "z3" ["-smt2", "-in"] Nothing w
+# (handle, {ProcessIO | stdIn, stdOut, stdErr}) = fromOk err
+# z3 = { Z3 |
+		handle = handle,
+		stdIn  = stdIn,
+		stdOut = stdOut,
+		stdErr = stdErr
+	}
+= (z3, w)
+
+addAssert :: Z3 String *World -> *World
+addAssert z3 s w
+# (_, w) = writePipe ("(assert (" <+ s <+ "))\n") z3.Z3.stdIn w
+= w
+
+addVariable :: Z3 String *World -> *World
+addVariable z3 s w
+# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
+= w
+
+checkSat :: Z3 *World -> (Bool, *World)
+checkSat z3 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 "(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)