diff options
Diffstat (limited to 'src/theory/substitutions.h')
| -rw-r--r-- | src/theory/substitutions.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index ee2a15f6f..32ed35074 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -91,6 +91,10 @@ 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) : @@ -158,10 +162,27 @@ public: // should best interact with cache invalidation on context // pops. + // Simplify right-hand sides of current map using the given substitutions + void simplifyRHS(const SubstitutionMap& subMap); + + // 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); + /** * Print to the output stream */ void print(std::ostream& out) const; + void debugPrint() const; };/* class SubstitutionMap */ |