Add minimization goals (not supported by Z3)

1 files changed, 12 insertions, 2 deletions

diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index b4b7326..8494bad 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -5,6 +5,10 @@ import StdString
 import System.Process
 import Text
 
+import StdDebug
+from Data.Func import $
+trace_id x = trace x x
+
 :: Z3 =
 	{ handle :: ProcessHandle
 	, stdIn  :: WritePipe
@@ -26,12 +30,17 @@ startZ3 w
 
 addAssert :: !Z3 !String !*World -> *World
 addAssert z3 s w
-# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w
+# (_, w) = writePipe (trace_id $ "(assert " <+ s <+ ")\n") z3.Z3.stdIn w
+= w
+
+addMinimize :: !Z3 !String !*World -> *World
+addMinimize z3 s w
+# (_, w) = writePipe (trace_id $ "(minimize " <+ 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) = writePipe (trace_id $ "(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
 = w
 
 checkSat :: !Z3 !*World -> (!Bool, !*World)
@@ -39,6 +48,7 @@ checkSat z3 w
 # (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
+# out = trace_id out
 = (startsWith "sat" out, w)
 
 getModel :: !Z3 !*World -> (!String, !*World)