implemented some of the z3 backend

src/LogicIR/Backend/Z3.hs

@@ -10,16 +10,38 @@ lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
 
 lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
 lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
-    flConst = undefined
-    flVar = undefined
-    flNot = undefined
-    flBinop = undefined
-    flComp = undefined
+    flConst b = mkBool b
+    flVar (Var t n) = do symbol <- mkStringSymbol n
+                         case t of
+                              TPrim PInt -> mkIntVar symbol
+                              TPrim PBool -> mkBoolVar symbol
+                              _ -> error $ show n
+    flNot a = a >>= mkNot
+    flBinop a' o b' = do a <- a'
+                         b <- b'
+                         case o of
+                            LAnd -> mkAnd [a, b]
+                            LOr -> mkOr [a, b]
+                            LImpl -> mkImplies a b
+                            LBicond -> undefined
+    flComp a' o b' = do a <- a'
+                        b <- b'
+                        case o of
+                            CEqual -> mkEq a b
+                            CNEqual -> mkEq a b >>= mkNot
+                            CLess -> mkLt a b
+                            CGreater -> mkGt a b
+                            CLeq -> mkLe a b
+                            CGeq -> mkGe a b
     flQuant = undefined
     flArray = undefined
     flNil = undefined
-    fnConst = undefined
+    fnConst n = mkInteger (fromIntegral n)
     fnUnop = undefined
-    fnBinop = undefined
+    fnBinop a' o b' = do a <- a'
+                         b <- b'
+                         case o of
+                            NAdd -> mkAdd [a, b]
+                            _ -> undefined
     fnIf = undefined
     fnLen = undefined
\ No newline at end of file

src/SimpleFormulaChecker.hs

@@ -15,6 +15,8 @@ import LogicIR.Frontend.Java
 import LogicIR.Backend.Z3
 import LogicIR.Backend.Pretty
 
+import Control.Monad.Trans (liftIO)
+
 import Debug.Trace
 
 {-
@@ -113,7 +115,12 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
     let (e1, e2) = (extractCond m1 name, extractCond m2 name)
     putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
     let lexpr = javaExpToLExpr e1 env1 decls1
-    putStrLn $ show lexpr ++ "\n\n" ++ prettyLExpr lexpr
+    putStrLn $ "LogicIR.Expr:\n" ++ show lexpr ++ "\n\nLogicIR.Pretty:\n" ++ prettyLExpr lexpr
+    putStrLn "\nZ3 AST:"
+    evalZ3 $ do asd <- lExprToZ3Ast lexpr
+                zprint astToString asd
+                return asd
+    putStrLn "\nZ3 Result:"
     {--- get postconditions
     let (post1, post2) = (extractCond m1 "post", extractCond m2 "post")
     putStrLn $ "post1:\n" ++ prettyPrint post1 ++ "\npost2:\n" ++ prettyPrint post2 ++ "\n"-}
@@ -149,4 +156,4 @@ edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
 testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
 
-blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec1")
+blub = compareSpec (edslSrc, "simple1") (edslSrc, "simple1")
\ No newline at end of file

src/z3_tests/equivalence.py

@@ -55,6 +55,7 @@ def neq_forall2():
 	solve(ast)
 
 def neq_forall3():
+	return
 	print "3"
 	x = Int('x')
 	ast1 = ForAll(x, x*x>=x, patterns = [x])
@@ -66,6 +67,22 @@ def neq_forall3():
 # A <=> B means A => B and B => A, so if we prove (A & ~B), A => B doesn't hold so A != B
 # - joao
 
+def python_is_super_hot():
+	print "SUPER HOT"
+	IntArray = ArraySort(IntSort(), IntSort())
+	ArrayRef = Datatype('ArrayRef')
+	ArrayRef.declare('NotNull', ('Value', IntArray))
+	ArrayRef.declare('Null')
+	ArrayRef = ArrayRef.create()
+
+	print ArrayRef.Null
+	print ArrayRef.NotNull
+	nullArr = Array('null', IntSort(), IntSort())
+	arr = Array('a', IntSort(), IntSort())
+	solve (arr == nullArr)
+
+help_simplify()
+
 eq()
 print ""
 neq()
@@ -74,4 +91,6 @@ neq_forall()
 print ""
 neq_forall2()
 print ""
-neq_forall3()
+neq_forall3()
\ No newline at end of file
+print ""
+python_is_super_hot()
\ No newline at end of file