diff --git a/src/LogicIR/Backend/QuickCheck.hs b/src/LogicIR/Backend/QuickCheck.hs
index ffe475bc3b56403e3af65af63452e77f2ab5db6d..8fa73faadbe2109f1af51e32acc972a0a65a137f 100644
--- a/src/LogicIR/Backend/QuickCheck.hs
+++ b/src/LogicIR/Backend/QuickCheck.hs
@@ -62,17 +62,14 @@ check e1 e2 = do
-- be evaluated - i.e. there's still a variable in the LExpr - an error will be thrown.
checkLExpr :: LExpr -> IO (LConst, Model)
checkLExpr e = do
- primitivesModel <- generateModel $ primitives
+ --putStrLn $ (show $ findPrimitives quantFreeE)
+ primitivesModel <- generateModel $ findPrimitives quantFreeE
let primFreeE = applyModel primitivesModel quantFreeE
(finalE, arrayModel) <- repeatedApplyAndExpandModel (primFreeE, empty)
let model = arrayModel ++ primitivesModel
let result = eval finalE
return $ (result, model)
- where quantFreeE = replaceQuantifiers e
- vars = findPrimitives quantFreeE
- primitives = filter sPrim vars
- sPrim (LVar (Var (TPrim _) _)) = True
- sPrim _ = False
+ where quantFreeE = replaceQuantifiers e
-- applies substitution of arrays until a "pure" LExpr is the result, or no
-- more substitutions can be applied. If the latter is the case, an error
@@ -114,7 +111,7 @@ applyModel model = foldLExpr algebra
var v = substitute (LVar v) model
quant _ _ e1 e2 = error "applyModel expects a quantifier-free LExpr."
arr v e = substitute (LArray v e) model
- snull v = LIsnull v
+ snull v = substitute (LIsnull v) model
len v = LLen v
-- Substitutes an LExpr if a valid substitute can be found in the given list.
@@ -131,6 +128,11 @@ generateModelEntry e@(LVar (Var (TPrim t) _)) = do
generateValue t >>= \v -> return (e, v)
generateModelEntry e@(LArray (Var (TArray (TPrim t)) _) _) = do
generateValue t >>= \v -> return (e, v)
+generateModelEntry e@(LIsnull (Var (TArray _) _)) = do
+ generateValue PBool >>= \v -> return (e, v)
+generateModelEntry e = do
+ error $ "Cannot generate model entry for " ++ show e
+ return (e, e)
-- Generates a random LExpr of a certain Primitive type.
generateValue :: Primitive -> IO LExpr
@@ -151,7 +153,7 @@ toLExpr PInt32 v = LConst $ CInt $ v
-- Returns a list with all Vars in the LExpr.
findPrimitives :: LExpr -> [LExpr]
-findPrimitives expr = nub $ foldLExpr algebra expr
+findPrimitives expr = filter isPrim $ nub $ foldLExpr algebra expr
where algebra :: LExprAlgebra [LExpr]
algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
cnst _ = []
@@ -161,8 +163,10 @@ findPrimitives expr = nub $ foldLExpr algebra expr
var v = [LVar v]
quant _ _ e1 e2 = error "findPrimitives expects a quantifier-free LExpr."
arr v e = e
- snull v = [LVar v]
+ snull v = [LIsnull v]
len v = [LVar v]
+ isPrim (LVar (Var (TArray _) _)) = False
+ isPrim _ = True
-- Returns a list with all LArrays in the LExpr.
findArrays :: LExpr -> [LExpr]
diff --git a/src/LogicIR/Backend/Rewrite.hs b/src/LogicIR/Backend/Rewrite.hs
index e426f9a43d7915f67c648cf61c091a7d07921818..7762ed55f3e4d6c0a72370e0e0e2fde176ab6ff2 100644
--- a/src/LogicIR/Backend/Rewrite.hs
+++ b/src/LogicIR/Backend/Rewrite.hs
@@ -29,8 +29,8 @@ replaceQuantifiersAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
replaceQuantifier :: QOp -> Var -> LExpr -> LExpr -> LExpr
replaceQuantifier op var domain e = LBinop e1 combiner e2
where prime (Var t name) = Var t (name ++ "'")
- e1 = LBinop domain LAnd e
- e2 = replace var (prime var) (LBinop domain LAnd e)
+ e1 = LBinop domain LImpl e
+ e2 = replace var (prime var) (LBinop domain LImpl e)
combiner = if op == QAll then LAnd else LOr
-- Returns an LExpr where all occurences of vOld in the given LExpr are
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index d274afafc28048b57ad39a59dbe52c02fe383f75..a60393be0aacaa44b40f3827f4f8c00c89beab2a 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -19,15 +19,16 @@ evalPossible = foldLExpr evalPossibleAlgebra
evalPossibleAlgebra :: LExprAlgebra Bool
evalPossibleAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
- where cnst _ = True
- uni _ c = c
- bin le _ re = le && re
- iff ge e1 e2 = ge && e1 && e2
- var v = False
- quant _ _ a1 a2 = a1 && a2
- arr v a = False
- snull v = True -- This possibly needs to be changed. See evalAlgebra
- len v = True -- This possibly needs to be changed. See evalAlgebra
+ where cnst _ = True
+ uni _ c = c
+ bin le _ re = le && re
+ iff ge e1 e2 = ge && e1 && e2
+ var v = False
+ quant _ _ a1 a2 = a1 && a2
+ arr v a = False
+ snull (Var (TPrim _) _) = True -- Primitive type is never null.
+ snull (Var (TArray _) _) = False
+ len v = True -- This possibly needs to be changed. See evalAlgebra
evalAlgebra :: LExprAlgebra LConst
evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
@@ -43,9 +44,11 @@ evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
iff ge e1 e2 = if ge == (CBool True) then e1 else e2
-- This possibly needs to be changed.
- snull v = CBool False -- error "Null checks cannot yet be evaluated."
len v = CInt 10 -- error "Array length cannot yet be evaluated."
+ snull (Var (TPrim _) _) = CBool False -- Primitive type is never null.
+ snull (Var (TArray _) _) = error "You can't call eval on an LExpr that has an (LIsnull someArrayVar) that wasn't converted to a boolean first."
+
-- Things that should never happen.
quant _ _ e1 e2 = error "Quantifiers cannot be evaluated and should be replaced using LogicIR.Rewrite.replaceQuantifiers."
arr v a = error "You can't call eval on an LExpr that contains uninstantiated arrays."
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 535992e7ce3650293ca33054ec835c2e37156fa8..45825994928747be31b3f64cd3b6cc5cb4d75f94 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -245,3 +245,8 @@ testSpec method1@(_, name1) method2@(_, name2) n = do
let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
postAns <- testEquality n lExpr1 lExpr2
return $ preAns && postAns
+
+-- The legendary 16th test that causes an endless loop in Z3 and that gives
+-- incorrect test results in the case of QuickCheck.
+test16 = testSpec (edslSrc, "sorted1") (edslSrc, "sorted4") 10000
+ where edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
diff --git a/test/TIRQuickCheck.hs b/test/TIRQuickCheck.hs
index 5336c4321d4513f802beaac5e219a02b88c4e2c2..da62964c83d522829fa4427c7094ba99499272b2 100644
--- a/test/TIRQuickCheck.hs
+++ b/test/TIRQuickCheck.hs
@@ -8,27 +8,27 @@ import SimpleFormulaChecker
edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
-testEquiv :: Bool -> String -> String -> Assertion
-testEquiv b s s' =
- unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s') 100000) @?= b
-(.==) = testEquiv True
-(.!=) = testEquiv False
+testEquiv :: Bool -> String -> String -> Int -> Assertion
+testEquiv b s s' n =
+ unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s') n) @?= b
+eq s s' n = testEquiv True s s' n
+neq s s' n = testEquiv False s s' n
quickCheckTests =
- [ "swap_spec1" .== "swap_spec1"
- , "swap_spec1" .!= "swap_spec2"
- , "getMax_spec1" .!= "getMax_spec2"
- , "test1" .!= "test2"
- , "blob1" .== "blob1"
- , "test1_" .!= "test2"
- , "null1" .!= "null2"
- , "swap_spec1" .!= "swap_spec3"
- , "swap_spec1" .!= "swap_spec4"
- , "null3" .!= "test2"
- , "sorted1" .!= "test2"
- , "sorted1" .!= "sorted2"
- , "sorted1".!= "sorted3"
- , "test2" .!= "sorted3"
- , "sorted3" .!= "sorted4"
- , "sorted1" .== "sorted4"
- ]
+ [ (eq "swap_spec1" "swap_spec1" 10)
+ , (neq "swap_spec1" "swap_spec2" 10)
+ , (neq "getMax_spec1" "getMax_spec2" 1000)
+ , (neq "test1" "test2" 10)
+ , (eq "blob1" "blob1" 10)
+ , (neq "test1_" "test2" 10)
+ , (neq "null1" "null2" 10)
+ , (neq "swap_spec1" "swap_spec3" 10)
+ , (neq "swap_spec1" "swap_spec4" 100)
+ , (neq "null3" "test2" 10)
+ , (neq "sorted1" "test2" 10)
+ , (neq "sorted1" "sorted2" 1000)
+ , (neq "sorted1" "sorted3" 1000)
+ , (neq "test2" "sorted3" 10)
+ , (neq "sorted3" "sorted4" 1000)
+ , (eq "sorted1" "sorted4" 1000)
+ ]
\ No newline at end of file