Debug smt2 statements

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