diff options
Diffstat (limited to 'src/theory/uf/tim/theory_uf_tim.h')
| -rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 9a2d252c0..4c8a1a71a 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -156,6 +156,16 @@ public: */ void explain(TNode n, Effort level) {} + /** + * Get a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n, TheoryEngine* engine) { + Unimplemented("TheoryUFTim doesn't support model generation"); + } + std::string identify() const { return std::string("TheoryUFTim"); } private: |