diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-13 20:39:13 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-09-13 20:39:13 +0000 |
commit | 01dfa806851502267e1032483fec48e8b4373634 (patch) | |
tree | 8103a5a5a763fecfc42793bf5c3c88290bff775b /src/theory/model.h | |
parent | dce6be13f8eb90006c7ceb8d43a8a78da23ca838 (diff) |
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 2f4ebfdbf..85f5dd31b 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -37,12 +37,6 @@ class TheoryModel : public Model { friend class TheoryEngineModelBuilder; protected: - /** add term function - * This should be called on all terms that exist in the model. - * addTerm( n ) will do any model-specific processing necessary for n, - * such as contraining the interpretation of uninterpretted functions. - */ - virtual void addTerm( Node n ) {} /** substitution map for this model */ SubstitutionMap d_substitutions; public: @@ -94,6 +88,12 @@ public: public: /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); + /** add term function + * addTerm( n ) will do any model-specific processing necessary for n, + * such as contraining the interpretation of uninterpretted functions, + * and adding n to the equality engine of this model + */ + virtual void addTerm( Node n ); /** assert equality holds in the model */ void assertEquality( Node a, Node b, bool polarity ); /** assert predicate holds in the model */ |