* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 4e4088bb0..f270dacb4 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -148,7 +148,7 @@ public:
         }
       }else{
         d_nonbasic.insert(x_j);
-        d_coeffs.insert(make_pair(x_j,a_sj));
+        d_coeffs.insert(std::make_pair(x_j,a_sj));
       }
     }
   }
@@ -289,7 +289,7 @@ public:
     d_activeRows.erase(basic);
     d_activeBasicVars.erase(basic);
 
-    d_inactiveRows.insert(make_pair(basic, row));
+    d_inactiveRows.insert(std::make_pair(basic, row));
   }
 
   void reinjectBasic(TNode basic){
@@ -299,7 +299,7 @@ public:
 
     d_inactiveRows.erase(basic);
     d_activeBasicVars.insert(basic);
-    d_activeRows.insert(make_pair(basic, row));
+    d_activeRows.insert(std::make_pair(basic, row));
 
     updateRow(row);
   }