diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
commit | 5b65d0f80d56731fd7d07f491973bad14a85566e (patch) | |
tree | 4aafa4742804ff87408a1da7523d799851a028c0 /src/theory/substitutions.h | |
parent | bdaa3049467fd17d3fb95701f7946a4bf0f5206a (diff) |
* Add assertion in TheoryModel code to ensure we don't get inconsistent
substitutions for solved variables. Related to bug 418 (and might
resolve it).
* Respect phase-locking in Minisat (one phase-saving site was unguarded).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index cf751b69e..5cb8c5e2f 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -108,14 +108,27 @@ public: /** * Adds a substitution from x to t. */ - void addSubstitution(TNode x, TNode t, - bool invalidateCache = true); + void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** * Returns true iff x is in the substitution map */ - bool hasSubstitution(TNode x) - { return d_substitutions.find(x) != d_substitutions.end(); } + bool hasSubstitution(TNode x) const { + return d_substitutions.find(x) != d_substitutions.end(); + } + + /** + * Returns the substitution mapping that was given for x via + * addSubstitution(). Note that the returned value might itself + * be in the map; for the actual substitution that would be + * performed for x, use .apply(x). This getSubstitution() function + * is mainly intended for constructing assertions about what has + * already been put in the map. + */ + TNode getSubstitution(TNode x) const { + AssertArgument(hasSubstitution(x), x, "element not in this substitution map"); + return (*d_substitutions.find(x)).second; + } /** * Apply the substitutions to the node. |