diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-28 18:33:38 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-28 18:38:38 -0400 |
| commit | feef8c2243734f8e6703164ee4d9a5980b7b1eb6 (patch) | |
| tree | 9316b7c189b3c860e6e39f92ea2c1e8a29cd1620 /src/theory/substitutions.h | |
| parent | 5746fcdf2fe4c5472a817d18f1a536f6f4c31085 (diff) | |
rm old unused code
Diffstat (limited to 'src/theory/substitutions.h')
| -rw-r--r-- | src/theory/substitutions.h | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 5a478a250..8572a6abd 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -95,10 +95,6 @@ private: */ CacheInvalidator d_cacheInvalidator; - // Helper list and method for simplifyLHS methods - // std::vector<std::pair<Node, Node> > d_worklist; - // void processWorklist(std::vector<std::pair<Node, Node> >& equalities, bool rewrite); - public: SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : @@ -186,18 +182,6 @@ public: // Simplify right-hand sides of current map with lhs -> rhs void simplifyRHS(TNode lhs, TNode rhs); - /* - // Simplify left-hand sides of current map using the given substitutions - void simplifyLHS(const SubstitutionMap& subMap, - std::vector<std::pair<Node,Node> >& equalities, - bool rewrite = true); - - // Simplify left-hand sides of current map with lhs -> rhs and then add lhs -> rhs to the substitutions set - void simplifyLHS(TNode lhs, TNode rhs, - std::vector<std::pair<Node,Node> >& equalities, - bool rewrite = true); - */ - bool isSolvedForm() const { return d_solvedForm; } /** |