[Git][haskell-team/DHG_packages][master] what4: fix some tests
Clint Adams (@clint)
gitlab at salsa.debian.org
Wed Oct 25 17:26:09 BST 2023
Clint Adams pushed to branch master at Debian Haskell Group / DHG_packages
Commits:
5f4156ce by Clint Adams at 2023-10-25T12:25:35-04:00
what4: fix some tests
- - - - -
5 changed files:
- p/haskell-what4/debian/changelog
- p/haskell-what4/debian/control
- + p/haskell-what4/debian/patches/disable-tests-yices
- p/haskell-what4/debian/patches/series
- p/haskell-what4/debian/rules
Changes:
=====================================
p/haskell-what4/debian/changelog
=====================================
@@ -1,3 +1,10 @@
+haskell-what4 (1.5.1-2) unstable; urgency=medium
+
+ * Build-Depend on both cvc4 and cvc5 for testsuite.
+ * Disable tests requiring Yices.
+
+ -- Clint Adams <clint at debian.org> Wed, 25 Oct 2023 11:22:09 -0400
+
haskell-what4 (1.5.1-1) unstable; urgency=medium
[ Ilias Tsitsimpis ]
=====================================
p/haskell-what4/debian/control
=====================================
@@ -103,6 +103,7 @@ Build-Depends: debhelper (>= 10),
libghc-zenc-prof,
libghc-parameterized-utils-dev,
cvc4,
+ cvc5,
z3,
libghc-quickcheck2-dev (>= 2.12),
libghc-quickcheck2-prof,
@@ -180,7 +181,7 @@ X-Description: Solver-agnostic symbolic values support for issuing queries
What4 is a generic library for representing values as symbolic formulae which
may contain references to symbolic values, representing unknown variables.
It provides support for communicating with a variety of SAT and SMT solvers,
- including Z3, CVC4, Yices, Boolector, STP, and dReal.
+ including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal.
The data representation types make heavy use of GADT-style type indices
to ensure type-correct manipulation of symbolic values.
=====================================
p/haskell-what4/debian/patches/disable-tests-yices
=====================================
@@ -0,0 +1,78 @@
+--- a/test/ExprBuilderSMTLib2.hs
++++ b/test/ExprBuilderSMTLib2.hs
+@@ -1159,39 +1159,13 @@ testUnsafeSetAbstractValue2 = testCase "
+ , "compound symbolic expression"
+ ]
+
+-testResolveSymBV :: WURB.SearchStrategy -> TestTree
+-testResolveSymBV searchStrat =
+- testProperty ("test resolveSymBV (" ++ show (PP.pretty searchStrat) ++ ")") $
+- H.property $ do
+- let w = knownNat @8
+- lb <- H.forAll $ HGen.word8 $ HRange.constant 0 maxBound
+- ub <- H.forAll $ HGen.word8 $ HRange.constant lb maxBound
+-
+- rbv <- liftIO $ withYices $ \sym proc -> do
+- bv <- freshConstant sym (safeSymbol "bv") knownRepr
+- p1 <- bvUge sym bv =<< bvLit sym w (BV.mkBV w (toInteger lb))
+- p2 <- bvUle sym bv =<< bvLit sym w (BV.mkBV w (toInteger ub))
+- p3 <- andPred sym p1 p2
+- assume (solverConn proc) p3
+- WURB.resolveSymBV sym searchStrat w proc bv
+-
+- case rbv of
+- WURB.BVConcrete bv -> do
+- let bv' = fromInteger $ BV.asUnsigned bv
+- lb H.=== bv'
+- ub H.=== bv'
+- WURB.BVSymbolic bounds -> do
+- let (lb', ub') = WUBA.ubounds bounds
+- lb H.=== fromInteger lb'
+- ub H.=== fromInteger ub'
+-
+ ----------------------------------------------------------------------
+
+
+ main :: IO ()
+ main = do
+ testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"
+- let solverNames = SolverName <$> [ "cvc4", "cvc5", "yices", "z3" ]
++ let solverNames = SolverName <$> [ "cvc4", "cvc5", "z3" ]
+ solvers <- reportSolverVersions testLevel id
+ =<< (zip solverNames <$> mapM getSolverVersion solverNames)
+ let z3Tests =
+@@ -1278,17 +1252,6 @@ main = do
+
+ , testCase "CVC4 #182 test case" $ withCVC4 issue182Test
+ ]
+- let yicesTests =
+- [
+- testResolveSymBV WURB.ExponentialSearch
+- , testResolveSymBV WURB.BinarySearch
+-
+- , testCase "Yices 0-tuple" $ withYices zeroTupleTest
+- , testCase "Yices 1-tuple" $ withYices oneTupleTest
+- , testCase "Yices pair" $ withYices pairTest
+- , testCase "Yices rounding" $ withYices roundingTest
+- , testCase "Yices #182 test case" $ withYices issue182Test
+- ]
+ let cvc5Tests = cvc4Tests
+ let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
+ else fmap (ignoreTestBecause (nm <> " not present"))
+@@ -1311,5 +1274,4 @@ main = do
+ ]
+ <> (skipIfNotPresent "cvc4" cvc4Tests)
+ <> (skipIfNotPresent "cvc5" cvc5Tests)
+- <> (skipIfNotPresent "yices" yicesTests)
+ <> (skipIfNotPresent "z3" z3Tests)
+--- a/test/OnlineSolverTest.hs
++++ b/test/OnlineSolverTest.hs
+@@ -61,8 +61,6 @@ allOnlineSolvers =
+ , AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options, Just cvc4Timeout)
+ , (SolverName "CVC5"
+ , AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout)
+- , (SolverName "Yices"
+- , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)
+ , (SolverName "Boolector"
+ , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout)
+ #ifdef TEST_STP
=====================================
p/haskell-what4/debian/patches/series
=====================================
@@ -1,2 +1,3 @@
no-tasty-sugar
disable-tests-non-x86_64
+disable-tests-yices
=====================================
p/haskell-what4/debian/rules
=====================================
@@ -9,3 +9,5 @@ include /usr/share/cdbs/1/rules/debhelper.mk
include /usr/share/cdbs/1/class/hlibrary.mk
build/haskell-what4-utils:: build-ghc-stamp
+
+check-ghc-stamp: export LC_ALL := C.UTF-8
View it on GitLab: https://salsa.debian.org/haskell-team/DHG_packages/-/commit/5f4156cea631961cb8de82416f7e868f4015dfb4
--
View it on GitLab: https://salsa.debian.org/haskell-team/DHG_packages/-/commit/5f4156cea631961cb8de82416f7e868f4015dfb4
You're receiving this email because of your account on salsa.debian.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://alioth-lists.debian.net/pipermail/pkg-haskell-commits/attachments/20231025/1010cace/attachment-0001.htm>
More information about the Pkg-haskell-commits
mailing list