Bitblast formula that don't contain arrays into and-inverter graphs. This uses the...

Bitblast formula that don't contain arrays into and-inverter graphs. This uses the AIG implementation provided by the ABC package.

This has some advantages:
* The AIG nodes are smaller than our ASTNodes, so it uses less memory.
* The CNFs generated by ABC are smaller, so generally solving is quicker.

Some notes:
* I haven't made the CNF converter incremental, so bitblasting to AIGs is only enabled for bit-vector problems (which STP bitblasts eagerly).
* AIG re-writing isn't enabled yet.
* From prior experience some big problems fail in CNF encoding. All of our test cases pass though.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@913 e59a4935-1847-0410-ae03-e826735625c1