diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 03:01:41 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 03:01:41 +0000 |
commit | a81ea9670349abe03da96cf45fbaa115c4098325 (patch) | |
tree | 7bb03f748aaaddee5da8d3a9a17c416659d0fb73 /src/theory/substitutions.h | |
parent | e116ffc5c17be0b4a4a3b92ec43edd07c7c59c82 (diff) |
Adding constant propagation code - needs more testing - off by default
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 */ |