Update elimCmd to take different eliminate args and add test cases fo…

…r horn clause elimination described in ICFP2017
ucsd-progsys · Feb 2, 2024 · b02c053 · b02c053
1 parent 07321ac
commit b02c053
Showing 1 changed file with 21 additions and 11 deletions.
diff --git a/tests/test.hs b/tests/test.hs
@@ -70,14 +70,24 @@ unitTests
       testGroup "native-pos" <$> dirTests nativeCmd "tests/pos"    skipNativePos  ExitSuccess
     , testGroup "native-neg" <$> dirTests nativeCmd "tests/neg"    ["float.fq"]   (ExitFailure 1)
     , testGroup "elim-crash" <$> dirTests nativeCmd "tests/crash"  []             (ExitFailure 1)
-    , testGroup "elim-pos1"  <$> dirTests elimCmd   "tests/pos"    []             ExitSuccess
-    , testGroup "elim-pos2"  <$> dirTests elimCmd   "tests/elim"   []             ExitSuccess
-    , testGroup "elim-neg"   <$> dirTests elimCmd   "tests/neg"    ["float.fq"]   (ExitFailure 1)
-    , testGroup "elim-crash" <$> dirTests elimCmd   "tests/crash"  []             (ExitFailure 1)
-    , testGroup "proof"      <$> dirTests elimCmd   "tests/proof"     []          ExitSuccess
-    , testGroup "rankN"      <$> dirTests elimCmd   "tests/rankNTypes" []         ExitSuccess
-    , testGroup "horn-pos-el" <$> dirTests elimCmd   "tests/horn/pos"  []          ExitSuccess
-    , testGroup "horn-neg-el" <$> dirTests elimCmd   "tests/horn/neg"  []          (ExitFailure 1)
+    , testGroup "elim-pos1"  <$> dirTests (elimCmd "some")   "tests/pos"    []             ExitSuccess
+    , testGroup "elim-pos2"  <$> dirTests (elimCmd "some")   "tests/elim"   []             ExitSuccess
+    , testGroup "elim-neg"   <$> dirTests (elimCmd "some")   "tests/neg"    ["float.fq"]   (ExitFailure 1)
+    , testGroup "elim-crash" <$> dirTests (elimCmd "some")   "tests/crash"  []             (ExitFailure 1)
+    , testGroup "proof"      <$> dirTests (elimCmd "some")   "tests/proof"     []          ExitSuccess
+    , testGroup "rankN"      <$> dirTests (elimCmd "some")   "tests/rankNTypes" []         ExitSuccess
+    , testGroup "horn-pos-el" <$> dirTests (elimCmd "some")   "tests/horn/pos"  []          ExitSuccess
+    , testGroup "horn-neg-el" <$> dirTests (elimCmd "some")   "tests/horn/neg"  []          (ExitFailure 1)
+
+    , testGroup "elim-pos1"  <$> dirTests (elimCmd "horn")   "tests/pos"    []             ExitSuccess
+    , testGroup "elim-pos2"  <$> dirTests (elimCmd "horn")   "tests/elim"   []             ExitSuccess
+    , testGroup "elim-neg"   <$> dirTests (elimCmd "horn")   "tests/neg"    ["float.fq"]   (ExitFailure 1)
+    , testGroup "elim-crash" <$> dirTests (elimCmd "horn")   "tests/crash"  []             (ExitFailure 1)
+    , testGroup "proof"      <$> dirTests (elimCmd "horn")   "tests/proof"     []          ExitSuccess
+    , testGroup "rankN"      <$> dirTests (elimCmd "horn")   "tests/rankNTypes" []         ExitSuccess
+    , testGroup "horn-pos-el" <$> dirTests (elimCmd "horn")   "tests/horn/pos"  ["ebind02.smt2", "ebind03.smt2"]          ExitSuccess
+    , testGroup "horn-neg-el" <$> dirTests (elimCmd "horn")   "tests/horn/neg"  []          (ExitFailure 1)
+
     , testGroup "horn-pos-na" <$> dirTests nativeCmd "tests/horn/pos"  []          ExitSuccess
     , testGroup "horn-neg-na" <$> dirTests nativeCmd "tests/horn/neg"  []          (ExitFailure 1)
 
@@ -156,9 +166,9 @@ nativeCmd :: TestCmd
 nativeCmd (LO opts) bin dir file =
   printf "cd %s && %s %s %s" dir bin opts file
 
-elimCmd :: TestCmd
-elimCmd (LO opts) bin dir file =
-  printf "cd %s && %s --eliminate=some %s %s" dir bin opts file
+elimCmd :: String -> TestCmd
+elimCmd cmd (LO opts) bin dir file =
+  printf "cd %s && %s --eliminate=%s %s %s" dir bin cmd opts file
 
 ----------------------------------------------------------------------------------------
 -- Generic Helpers