This commit merges into trunk the branch branches/arithmetic/integers2 from r2650 to r2779.

- This excludes revision 2777.  This revision had some strange performance implications and was delaying the merge.
- This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts.
- The DioSolver can be disabled at command line using --disable-dio-solver.
- This includes a number of changes to the arithmetic normal form.
- The Integer class features a number of new number theoretic function.
- This commit includes a few rather loud warning. I will do my best to take care of them today.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index f05ebaf17..d7f0e13a5 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -91,15 +91,18 @@ public:
   }
 
   BitVector operator ~() const {
+    //is this right? it looks like a no-op?
     return BitVector(d_size, d_value);
   }
 
   BitVector concat (const BitVector& other) const {
-    return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
+    return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
+    //return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
   }
 
   BitVector extract(unsigned high, unsigned low) const {
-    return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
+    return BitVector(high - low + 1, d_value.extractBitRange(high - low + 1, low));
+    //return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
   }
 
   size_t hash() const {