Make first argument constant whenever possible when normalizing multi…

…plication

This tends to play better with libraries such as What4, which use a similar
convention. See the Haddocks for `mul`.

This is part of an eventual fix for GaloisInc/saw-script#1828.

src/Data/AIG/Operations.hs

@@ -627,40 +627,47 @@ subConst g x c = addConst g x (-c)
 --   of the same size as the arguments.
 --   Overflow is silently discarded.
 --
---   Because it is beneficial to have the second argument be a constant whenever
+--   Because it is beneficial to have the first argument be a constant whenever
 --   possible (see the Haddocks for `mul'`), this will flip the order of
---   arguments if the first argument is a constant.
+--   arguments if the first argument is not a constant.
+--
+--   Because multiplication is commutative, we could just as well process the
+--   arguments the other way around. We deliberately choose the convention of
+--   making the first argument be a constant whenever possible due to the fact
+--   that several downstream libraries (e.g., What4) already normalize
+--   multiplication to have constants appear as the first argument.
 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) $
   if isJust (asUnsigned g x)
-    then mul' g y x -- The first argument is constant, so swap the arguments
-    else mul' g x y
+    then mul' g x y
+    else mul' g y x -- The first argument is not a constant,
+                    -- so swap the arguments.
 
 -- | Multiply two bitvectors with the same size, with result
 --   of the same size as the arguments.
 --   Overflow is silently discarded.
 --
---   This algorithm computes partial products by adding multiples of the first
+--   This algorithm computes partial products by adding multiples of the second
 --   'BV' argument, where the coefficient is computed from different bits of the
---   second argument. Whenever the second 'BV' argument is a constant,
+--   first argument. Whenever the first 'BV' argument is a constant,
 --   bitblasting the resulting AIG will result in a network of full adders,
 --   which is very amenable to verification. As a result, it is beneficial to
---   make the second 'BV' argument a constant whenever possible. (See
+--   make the first 'BV' argument a constant whenever possible. (See
 --   https://github.com/GaloisInc/saw-script/issues/1828 for a specific example
 --   of where this can help.)
 --
 --   See 'mul' for a version of this function that flips the argument order if
---   the first argument is a constant.
+--   the first argument is not a constant.
 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
+  let n = length x
   -- Function to update bits.
   let updateBits i z | i == n = return z
       updateBits i z = do
-        z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)
+        z' <- iteM g (x ! i) (add g z (shlC g y i)) (return z)
         updateBits (i+1) z'
-  updateBits 0 $ replicate (length x) (falseLit g)
+  updateBits 0 $ replicate (length y) (falseLit g)
 
 -- | Unsigned multiply two bitvectors with size @m@ and size @n@,
 --   resulting in a vector of size @m+n@.