summaryrefslogtreecommitdiff
path: root/Assignment2/src/Z3.dcl
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment2/src/Z3.dcl')
-rw-r--r--Assignment2/src/Z3.dcl13
1 files changed, 13 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)