write_aig: Normalize symmetry in multiplication

This bumps the `aig` submodule to bring in the changes from GaloisInc/aig#14,
which changes how `aig` performs multiplication to swap the order of arguments
if the second argument is a constant. This has two benefits:

* This ensures that `write_aig` will produce the same networks for `X * C` and
  `C * X`, where `C` is a constant and `X` is a variable.
* The algorithm that `mul` uses to compute multiplication is biased in its order
  of arguments, and having the first argument be a constant tends to produce
  networks that ABC has an easier time verifying. (The FFS example under
  `doc/tutorial/code/ffs.c` is a notable example of this.)

I have added a test case to check to see if the test case from #1828 now
produces identical AIGs regardless of the order of arguments.

Fixes #1828.

intTests/test1828/.gitignore

@@ -0,0 +1,2 @@
+left.aig
+right.aig

intTests/test1828/test.saw

@@ -0,0 +1,2 @@
+write_aig "left.aig" {{ \x -> x * 0x12345678 }};
+write_aig "right.aig" {{ \x -> 0x12345678 * x }};

intTests/test1828/test.sh

@@ -0,0 +1,9 @@
+set -e
+
+# This test case uses `write_aiger` to produce AIG files for two nearly
+# identical functions, where the only difference is the order of arguments (one
+# symbolic and one concrete) in a bitvector multiplication. If the `aig` library
+# does its job correctly, these should produce identical AIG files, so check
+# this using `diff`.
+$SAW test.saw
+diff -ru left.aig right.aig