Skip to content

Commit

Permalink
Draft: saw-script#1828: Approach 2
Browse files Browse the repository at this point in the history
This implements the idea in
GaloisInc/saw-script#1828 (comment).
  • Loading branch information
RyanGlScott committed Mar 3, 2023
1 parent 00f1386 commit be6cea2
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion src/Data/AIG/Operations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,7 @@ import qualified Control.Monad hiding (fail)
import Control.Monad.State hiding (zipWithM, replicateM, mapM, sequence, fail)
import Data.Bits ((.|.), setBit, shiftL, testBit)
import qualified Data.Bits as Bits
import Data.Maybe (isNothing)

import qualified Data.Vector as V
import qualified Data.Vector.Generic.Mutable as MV
Expand Down Expand Up @@ -626,7 +627,13 @@ subConst g x c = addConst g x (-c)
-- of the same size as the arguments.
-- Overflow is silently discarded.
mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul g x y = assert (length x == length y) $ do
mul g x y = assert (length x == length y) $
if isNothing (asUnsigned g x)
then mul' g x y
else mul' g y x

mul' :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul' g x y = do
-- Create mutable array to store result.
let n = length y
-- Function to update bits.
Expand Down

0 comments on commit be6cea2

Please sign in to comment.