diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 17:31:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-12 17:31:22 -0500 |
| commit | a117e2b45539a822aa480b90558c2c0da6031dd9 (patch) | |
| tree | 5006484b1794943a1f049247ebbb2a63cb82dbfb /src/theory/quantifiers/term_util.h | |
| parent | bee3c7f6840e531bc91d990b98f2b331d1f2f82c (diff) | |
Update to standard implementation of contains term (#3270)
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
| -rw-r--r-- | src/theory/quantifiers/term_util.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index b39a4e129..99ea483d9 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -219,8 +219,6 @@ public: //general utilities // TODO #1216 : promote these? private: - //helper for contains term - static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ); /** cache for getTypeValue */ std::unordered_map<TypeNode, std::unordered_map<int, Node>, @@ -244,8 +242,6 @@ public: d_type_value_offset_status; public: - /** 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 ); /** get the term depth of n */ |