diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-30 09:57:06 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 09:57:06 -0600 |
commit | 89b6c052e96cc907800650de93d2f238e19acd38 (patch) | |
tree | a634adc60388ab164d707511be0f1f52e75aef61 /src/theory/theory_model.h | |
parent | f1c8b8cda3b99353adbe424e0bf1259147001f3c (diff) |
Fixes for issue 1404 (#1409)
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index a8726f490..600f511c8 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -91,12 +91,6 @@ public: //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** add term - * This will do any model-specific processing necessary for n, - * such as constraining the interpretation of uninterpreted functions, - * and adding n to the equality engine of this model. - */ - virtual void addTerm(TNode n); /** assert equality holds in the model */ void assertEquality(TNode a, TNode b, bool polarity); /** assert predicate holds in the model */ @@ -204,6 +198,14 @@ public: Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; + /** add term internal + * + * This will do any model-specific processing necessary for n, + * such as constraining the interpretation of uninterpreted functions. + * This is called once for all terms in the equality engine, just before + * a model builder constructs this model. + */ + virtual void addTermInternal(TNode n); private: /** cache for getModelValue */ |