diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-10 11:25:19 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-10 11:25:19 -0700 |
| commit | 31a2135f4650a63fa772f001fcf191f2f7093a8d (patch) | |
| tree | 1d01c094b7df9b010f748905aeaace44f17d904a /src/theory/bv/theory_bv.h | |
| parent | aef0e5ed90b1b8913b5c8c743cbcd012d5916ba7 (diff) | |
Refactored BVAckermann preprocessing pass. (#1889)
Diffstat (limited to 'src/theory/bv/theory_bv.h')
| -rw-r--r-- | src/theory/bv/theory_bv.h | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 90bd6275c..13469d562 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -68,8 +68,6 @@ public: Node expandDefinition(LogicRequest& logicRequest, Node node) override; - void mkAckermanizationAssertions(std::vector<Node>& assertions); - void preRegisterTerm(TNode n) override; void check(Effort e) override; @@ -136,8 +134,6 @@ private: Node getBVDivByZero(Kind k, unsigned width); typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - void collectFunctionSymbols(TNode term, TNodeSet& seen); - void storeFunction(TNode func, TNode term); typedef std::unordered_set<Node, NodeHashFunction> NodeSet; NodeSet d_staticLearnCache; @@ -148,12 +144,7 @@ private: std::unordered_map<unsigned, Node> d_BVDivByZero; std::unordered_map<unsigned, Node> d_BVRemByZero; - - typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgs; typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; - // for ackermanization - FunctionToArgs d_funcToArgs; - CVC4::theory::SubstitutionMap d_funcToSkolem; context::CDO<bool> d_lemmasAdded; |