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 | |
parent | bee3c7f6840e531bc91d990b98f2b331d1f2f82c (diff) |
Update to standard implementation of contains term (#3270)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.h | 4 |
5 files changed, 14 insertions, 48 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 104e40d8b..1713c21e2 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1245,7 +1245,8 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); nretc = Rewriter::rewrite( nretc ); //ensure that nret does not contain vars - if( !TermUtil::containsTerms( nretc, vars ) ){ + if (!expr::hasSubterm(nretc, vars)) + { //result is ( nret / pv_prop.d_coeff ) nret = nretc; }else{ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index ea90ddd66..c6427a4c4 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/instantiate.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" @@ -170,8 +171,7 @@ bool Instantiate::addInstantiation( << terms[i] << std::endl; bad_inst = true; } - else if (quantifiers::TermUtil::containsTerms( - terms[i], d_term_util->d_inst_constants[q])) + else if (expr::hasSubterm(terms[i], d_term_util->d_inst_constants[q])) { Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index f5159a630..33da46675 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1808,9 +1808,10 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo Node newBody = body; NodeBuilder<> body_split(kind::OR); NodeBuilder<> tb(kind::OR); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node trm = body[i]; - if( TermUtil::containsTerms( body[i], args ) ){ + for (const Node& trm : body) + { + if (expr::hasSubterm(trm, args)) + { tb << trm; }else{ body_split << trm; diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index ffd808ed3..48dc88537 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -489,15 +489,17 @@ Node TermUtil::rewriteVtsSymbols( Node n ) { bool TermUtil::containsVtsTerm( Node n, bool isFree ) { std::vector< Node > t; getVtsTerms( t, isFree, false ); - return containsTerms( n, t ); + return expr::hasSubterm(n, t); } bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { std::vector< Node > t; getVtsTerms( t, isFree, false ); if( !t.empty() ){ - for( unsigned i=0; i<n.size(); i++ ){ - if( containsTerms( n[i], t ) ){ + for (const Node& nc : n) + { + if (expr::hasSubterm(nc, t)) + { return true; } } @@ -508,7 +510,7 @@ bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { bool TermUtil::containsVtsInfinity( Node n, bool isFree ) { std::vector< Node > t; getVtsTerms( t, isFree, false, false ); - return containsTerms( n, t ); + return expr::hasSubterm(n, t); } Node TermUtil::ensureType( Node n, TypeNode tn ) { @@ -524,40 +526,6 @@ Node TermUtil::ensureType( Node n, TypeNode tn ) { } } -bool TermUtil::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) { - if (visited.find(n) == visited.end()) - { - if( std::find( t.begin(), t.end(), n )!=t.end() ){ - return true; - } - visited[n] = true; - if (n.hasOperator()) - { - if (containsTerms2(n.getOperator(), t, visited)) - { - return true; - } - } - for (const Node& nc : n) - { - if (containsTerms2(nc, t, visited)) - { - return true; - } - } - } - return false; -} - -bool TermUtil::containsTerms( Node n, std::vector< Node >& t ) { - if( t.empty() ){ - return false; - }else{ - std::map< Node, bool > visited; - return containsTerms2( n, t, visited ); - } -} - int TermUtil::getTermDepth( Node n ) { if (!n.hasAttribute(TermDepthAttribute()) ){ int maxDepth = -1; 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 */ |