diff options
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); |