Add minimization goals (not supported by Z3)

1 files changed, 6 insertions, 4 deletions

diff --git a/Assignment2/src/Expression.icl b/Assignment2/src/Expression.icl
index 7622103..53699c0 100644
--- a/Assignment2/src/Expression.icl
+++ b/Assignment2/src/Expression.icl
@@ -1,8 +1,10 @@
 implementation module Expression
 
 from StdChar import instance == Char
-from StdOverloaded import class toString(toString)
-from StdString import instance toString {#Char}, instance toString Int, instance toString Real
+from StdOverloaded import class toString(toString), class toReal(toReal)
+from StdReal import entier, instance toReal Int, instance == Real
+from StdString import
+	instance toString {#Char}, instance toString Int, instance toString Real
 
 import Data._Array
 from Data.Func import $
@@ -46,6 +48,6 @@ where
 		(e1 - e2) -> "(- " <+ e1 <+ " " <+ e2 <+ ")"
 		(e1 * e2) -> "(* " <+ e1 <+ " " <+ e2 <+ ")"
 		(e1 / e2) -> "(/ " <+ e1 <+ " " <+ e2 <+ ")"
-		LitInt i  -> toString i
-		LitReal r -> toString r
+		LitInt i  -> toString i <+ ".0"
+		LitReal r -> if (toReal (entier r) == r) (r <+ ".0") (toString r)
 		Var v     -> v