diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
| -rw-r--r-- | src/theory/bv/theory_bv.h | 16 |
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; |