diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:00 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:06 -0600 |
| commit | 0615601703a1ac19d485e2b530a748c797b544ed (patch) | |
| tree | 19834cce797501d5586aed222349933c9af16b4a /src/theory/quantifiers/term_database.h | |
| parent | 2ba8bb701ce289ba60afec01b653b0930cc59298 (diff) | |
Simplify fmc model construction, add regression. Improve FMF debug assertions.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 86b0efbf3..0c4e94517 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -397,12 +397,15 @@ private: //helper for contains term static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited ); static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); + static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ); //general utilities public: /** simple check for whether n contains t as subterm */ static bool containsTerm( Node n, Node t ); /** simple check for contains term, true if contains at least one term in t */ static bool containsTerms( Node n, std::vector< Node >& t ); + /** contains uninterpreted constant */ + static bool containsUninterpretedConstant( Node n ); /** simple negate */ static Node simpleNegate( Node n ); /** is assoc */ |