diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-16 16:46:05 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-16 18:46:05 -0500 |
commit | 7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (patch) | |
tree | d9f2e91a52406edf66967faccad550631cd9e4a5 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
parent | 4e62cdade61514f268b96e78e2f82ad12dfcad07 (diff) |
Move node algorithms to separate file (#2311)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 4799de09d..37451b776 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -14,14 +14,15 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" using namespace std; using namespace CVC4::kind; @@ -774,9 +775,11 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ } } }else if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( n[i].getKind()==BOUND_VARIABLE ){ - if (!n[1 - i].hasSubterm(n[i])) + for (unsigned i = 0; i < 2; i++) + { + if (n[i].getKind() == BOUND_VARIABLE) + { + if (!expr::hasSubterm(n[1 - i], n[i])) { return true; } @@ -874,8 +877,9 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { - return !s.hasSubterm(v) && s.getType().isSubtypeOf(v.getType()); +bool QuantifiersRewriter::isVariableElim(Node v, Node s) +{ + return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); } void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, @@ -1112,7 +1116,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Trace("var-elim-quant") << "Variable eliminate based on bit-vector inversion : " << var << " -> " << slv << std::endl; - Assert(!slv.hasSubterm(var)); + Assert(!expr::hasSubterm(slv, var)); Assert(slv.getType().isSubtypeOf(var.getType())); vars.push_back(var); subs.push_back(slv); |