Merged QF_UFBV support from experimental branch

1 files changed, 7 insertions, 9 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0bbcba9b0..7f0494dc1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -122,8 +122,8 @@ private:
   Node getBVDivByZero(Kind k, unsigned width);
 
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
-  void collectNumerators(TNode term, TNodeSet& seen);
-  
+  void collectFunctionSymbols(TNode term, TNodeSet& seen);
+  void storeFunction(TNode func, TNode term);
   typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
   
@@ -134,14 +134,12 @@ private:
   __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
   __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
 
-  /**
-   * Maps from bit-vector width to numerators
-   * of uninterpreted function symbol
-   */
-  typedef __gnu_cxx::hash_map<unsigned, TNodeSet > WidthToNumerators;
 
-  WidthToNumerators d_BVDivByZeroAckerman;
-  WidthToNumerators d_BVRemByZeroAckerman;
+  typedef __gnu_cxx::hash_map<Node, NodeSet, NodeHashFunction>  FunctionToArgs;
+  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>  NodeToNode;
+  // for ackermanization
+  FunctionToArgs d_funcToArgs;
+  CVC4::theory::SubstitutionMap d_funcToSkolem;
 
   context::CDO<bool> d_lemmasAdded;