Revert "Simplify bvult by extracting sum common when sound. (#232)"

This reverts commit 5a6864ace5.

what4/doc/arithdomain.cry

@@ -306,20 +306,6 @@ slt a b = (sbounds a).1 <$ (sbounds b).0
 sle : {n} (fin n, n >= 1) => Dom n -> Dom n -> Bit
 sle a b = (sbounds a).1 <=$ (sbounds b).0
 
-ult_sum_common_equiv : {n} (fin n) => Dom n -> Dom n -> Dom n -> Bit
-ult_sum_common_equiv a b c =
-  if al == ah /\ bl == bh /\ al == bl
-    then True
-    else if ~(carry cl c.sz)
-      then check_same_wrap_interval cl ch
-      else check_same_wrap_interval cl mask`{n} /\ check_same_wrap_interval 0 ch
-  where
-    (cl, ch) = (c.lo, c.lo + c.sz)
-    (al, ah) = ubounds a
-    (bl, bh) = ubounds b
-    check_same_wrap_interval lo hi =
-      ~(carry ah hi) /\ ~(carry bh hi) \/ carry al lo /\ carry bl lo
-
 // A bitmask indicating which bits cannot be determined
 // given the interval information in the given domain
 unknowns : {n} (fin n, n >= 1) => Dom n -> [n]
@@ -474,13 +460,6 @@ correct_ule : {n} (fin n, n >= 1) => Dom n -> Dom n -> [n] -> [n] -> Bit
 correct_ule a b x y =
   ule a b ==> mem a x ==> mem b y ==> x <= y
 
-correct_ult_sum_common_equiv :
-  {n} (fin n, n >= 1) => Dom n -> Dom n -> Dom n -> [n] -> [n] -> [n] -> Bit
-correct_ult_sum_common_equiv a b c x y z =
-  ult_sum_common_equiv a b c ==>
-  mem a x ==> mem b y ==> mem c z ==>
-  (x + z < y + z <==> x < y)
-
 correct_bnot : {n} (fin n) => Dom n -> [n] -> Bit
 correct_bnot a x =
   mem a x <==> mem (bnot a) (~ x)
@@ -526,7 +505,6 @@ property o1 = correct_slt`{16}
 property o2 = correct_sle`{16}
 property o3 = correct_ult`{16}
 property o4 = correct_ule`{16}
-property o5 = correct_ult_sum_common_equiv`{4}
 
 ////////////////////////////////////////////////////////////
 // Operations preserve singletons

what4/src/What4/Expr/Builder.hs

@@ -2400,14 +2400,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where
     | x == y =
       return $! falsePred sym
 
-    | sr <- SR.SemiRingBVRepr SR.BVArithRepr (bvWidth x)
-    , (z, x', y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y)
-    , not (WSum.isZero sr z)
-    , BVD.isUltSumCommonEquiv (WSum.sumAbsValue x') (WSum.sumAbsValue y') (WSum.sumAbsValue z) = do
-      xr <- semiRingSum sym x'
-      yr <- semiRingSum sym y'
-      bvUlt sym xr yr
-
     | otherwise = do
         ut <- CFG.getOpt (sbUnaryThreshold sym)
         let ?unaryThreshold = fromInteger ut

what4/src/What4/Utils/BVDomain.hs

@@ -51,7 +51,6 @@ module What4.Utils.BVDomain
   , domainsOverlap
   , ubounds
   , sbounds
-  , isUltSumCommonEquiv
   , A.arithDomainData
   , B.bitbounds
     -- * Operations
@@ -426,11 +425,6 @@ ubounds a = A.ubounds (asArithDomain a)
 sbounds :: (1 <= w) => NatRepr w -> BVDomain w -> (Integer, Integer)
 sbounds w a = A.sbounds w (asArithDomain a)
 
--- | Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)
-isUltSumCommonEquiv :: BVDomain w -> BVDomain w -> BVDomain w -> Bool
-isUltSumCommonEquiv a b c =
-  A.isUltSumCommonEquiv (asArithDomain a) (asArithDomain b) (asArithDomain c)
-
 --------------------------------------------------------------------------------
 -- Operations
 

what4/src/What4/Utils/BVDomain/Arith.hs

@@ -11,7 +11,6 @@ domains.
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
@@ -31,7 +30,6 @@ module What4.Utils.BVDomain.Arith
   , eq
   , slt
   , ult
-  , isUltSumCommonEquiv
   , domainsOverlap
   , arithDomainData
   , bitbounds
@@ -96,7 +94,6 @@ module What4.Utils.BVDomain.Arith
   , correct_eq
   , correct_ult
   , correct_slt
-  , correct_isUltSumCommonEquiv
   , correct_unknowns
   , correct_bitbounds
   ) where
@@ -279,46 +276,6 @@ ult a b
     (a_min, a_max) = ubounds a
     (b_min, b_max) = ubounds b
 
--- | Check if @(bvult (bvadd a c) (bvadd b c))@ is equivalent to @(bvult a b)@.
--- 
--- This is true if and only if for all natural values @i_a@, @i_b@, @i_c@ in
--- @a@, @b@, @c@, either both @i_a + i_c@ and @i_b + i_c@ are less than @2^w@,
--- or both are not. We prove this by contradiction. If @i_a = i_b@, then the
--- property is trivial. Assume that @i_a < i_b@. Then @i_a + i_c < i_b + i_c@.
--- If exactly one of the additions is less than @2^w@, it must be the case that
--- @i_a + i_c < 2^w@ and @0 <= i_b + i_c - 2^w < 2^w@. Since @i_b < 2^w@, it
--- follows that @i_b + i_c < 2^w + i_c@, that @i_b + i_c - 2^w < i_c@, and that
--- @i_b + i_c - 2^w < i_a + i_c@. Thus, for these values of @i_a@, @i_b@, @i_c@,
--- @(bvult a b)@ is true, but @(bvult (bvadd a c) (bvadd b c))@ is false, which
--- is a contradiction.
---
--- We check this property by case analysis on whether @c@ is a single
--- non-wrapping interval, or it wraps around and is a union of two non-wrapping
--- intervals. For a non-wrapping (sub)interval @c'@ of @c@, there are four
--- possible cases:
--- 1. @a@ and @b@ contain a single value.
--- 2. @(bvadd a c')@ and @(bvadd b c')@ do not wrap around for any values in
---    @a@, @b@, @c'@.
--- 3. @(bvadd a c')@ and @(bvadd b c')@ wrap around for all values in @a@, @b@,
---    @c'@.
---
--- This is used to simplify @bvult@.
-isUltSumCommonEquiv :: Domain w -> Domain w -> Domain w -> Bool
-isUltSumCommonEquiv a b c = if al == ah && bl == bh && al == bl
-  then True
-  else if cl + cw == ch
-    then checkSameWrapInterval cl ch
-    else checkSameWrapInterval cl mask && checkSameWrapInterval 0 ch
-  where
-    (mask, cl, cw) = case c of
-      BVDInterval mask' cl' cw' -> (mask', cl', cw')
-      BVDAny mask' -> (mask', 0, mask')
-    ch = (cl + cw) .&. mask
-    (al, ah) = ubounds a
-    (bl, bh) = ubounds b
-    checkSameWrapInterval lo hi =
-      ah + hi <= mask && bh + hi <= mask || mask < al + lo && mask < bl + lo
-
 --------------------------------------------------------------------------------
 -- Operations
 
@@ -858,18 +815,6 @@ correct_slt n (a,x) (b,y) =
       Just False -> toSigned n x >= toSigned n y
       Nothing    -> True
 
-correct_isUltSumCommonEquiv ::
-  (1 <= n) =>
-  NatRepr n ->
-  (Domain n, Integer) ->
-  (Domain n, Integer) ->
-  (Domain n, Integer) ->
-  Property
-correct_isUltSumCommonEquiv n (a, x) (b, y) (c, z) =
-  member a x ==> member b y ==> member c z ==>
-    isUltSumCommonEquiv a b c ==>
-      ((toUnsigned n (x + z) < toUnsigned n (y + z)) == (toUnsigned n x < toUnsigned n y))
-
 correct_unknowns :: (1 <= n) => Domain n -> Integer -> Integer -> Property
 correct_unknowns a x y = member a x ==> member a y ==> ((x .|. u) == (y .|. u)) && (u .|. mask == mask)
   where

what4/test/BVDomTests.hs

@@ -182,9 +182,6 @@ arithDomainTests = testGroup "Arith Domain"
   , genTest "correct_slt" $
       do SW n <- genWidth
          A.correct_slt n <$> A.genPair n <*> A.genPair n
-  , genTest "correct_isUltSumCommonEquiv" $
-      do SW n <- genWidth
-         A.correct_isUltSumCommonEquiv n <$> A.genPair n <*> A.genPair n <*> A.genPair n
   , genTest "correct_unknowns" $
       do SW n <- genWidth
          a <- A.genDomain n