diff options
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index bde7dfdbc..5a478a250 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -68,8 +68,11 @@ private: /** Has the cache been invalidated? */ bool d_cacheInvalidated; + /** Whether to keep substitutions in solved form */ + bool d_solvedForm; + /** Internal method that performs substitution */ - Node internalSubstitute(TNode t); + Node internalSubstitute(TNode t, NodeCache& cache); /** Helper class to invalidate cache on user pop */ class CacheInvalidator : public context::ContextNotifyObj { @@ -98,13 +101,15 @@ private: public: - SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) : + SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) : d_context(context), d_substitutions(context), d_substitutionCache(), d_substituteUnderQuantifiers(substituteUnderQuantifiers), d_cacheInvalidated(false), - d_cacheInvalidator(context, d_cacheInvalidated) { + d_solvedForm(solvedForm), + d_cacheInvalidator(context, d_cacheInvalidated) + { } /** @@ -113,6 +118,11 @@ public: void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** + * Merge subMap into current set of substitutions + */ + void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true); + + /** * Returns true iff x is in the substitution map */ bool hasSubstitution(TNode x) const { @@ -170,13 +180,13 @@ 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, @@ -188,6 +198,8 @@ public: bool rewrite = true); */ + bool isSolvedForm() const { return d_solvedForm; } + /** * Print to the output stream */ |