diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 504ecd667..91ad0135b 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -145,6 +145,8 @@ public: * subsRep is whether subs contains only representatives */ TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ); + /** same as above, but without substitution */ + TNode evaluateTerm( TNode n ); /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); public: |