diff options
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 7 | ||||
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 5 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 38 |
3 files changed, 34 insertions, 16 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index ed68df89c..4bfc1a4f9 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -19,6 +19,7 @@ #include "base/output.h" #include "expr/expr.h" +#include "expr/node_algorithm.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_static_learner.h" @@ -107,9 +108,11 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet switch(n.getKind()){ case ITE: - if(n.hasBoundVar()) { + if (expr::hasBoundVar(n)) + { // Unsafe with non-ground ITEs; do nothing - Debug("arith::static") << "(potentially) non-ground ITE, ignoring..." << endl; + Debug("arith::static") + << "(potentially) non-ground ITE, ignoring..." << endl; break; } diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 30debf6d7..f4e9f9d6b 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -20,6 +20,7 @@ #include <cmath> #include <set> +#include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" @@ -1199,7 +1200,7 @@ bool NonlinearExtension::solveEqualitySimple(Node eq) { Assert(!slv.isNull()); // currently do not support substitution-with-coefficients - if (veqc.isNull() && !slv.hasSubterm(uv)) + if (veqc.isNull() && !expr::hasSubterm(slv, uv)) { Trace("nl-ext-cm") << "check-model-subs : " << uv << " -> " << slv << std::endl; @@ -1454,7 +1455,7 @@ bool NonlinearExtension::simpleCheckModelLit(Node lit) // is it a valid variable? std::map<Node, std::pair<Node, Node> >::iterator bit = d_check_model_bounds.find(v); - if (!invalid_vsum.hasSubterm(v) && bit != d_check_model_bounds.end()) + if (!expr::hasSubterm(invalid_vsum, v) && bit != d_check_model_bounds.end()) { std::map<Node, Node>::iterator it = v_a.find(v); if (it != v_a.end()) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 6db246b8b..968970049 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -32,6 +32,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node.h" +#include "expr/node_algorithm.h" #include "expr/node_builder.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -1354,24 +1355,37 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - - if(right.size() > options::ppAssertMaxSubSize()){ - Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl; + if (right.size() > options::ppAssertMaxSubSize()) + { + Debug("simplify") + << "TheoryArithPrivate::solve(): did not substitute due to the " + "right hand side containing too many terms: " + << minVar << ":" << elim << endl; Debug("simplify") << right.size() << endl; - }else if(elim.hasSubterm(minVar)){ - Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl; - - }else if (!minVar.getType().isInteger() || right.isIntegral()) { - Assert(!elim.hasSubterm(minVar)); + } + else if (expr::hasSubterm(elim, minVar)) + { + Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " + "due to recursive pattern with sharing: " + << minVar << ":" << elim << endl; + } + else if (!minVar.getType().isInteger() || right.isIntegral()) + { + Assert(!expr::hasSubterm(elim, minVar)); // cannot eliminate integers here unless we know the resulting // substitution is integral - Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl; + Debug("simplify") << "TheoryArithPrivate::solve(): substitution " + << minVar << " |-> " << elim << endl; outSubstitutions.addSubstitution(minVar, elim); return Theory::PP_ASSERT_STATUS_SOLVED; - } else { - Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; - + } + else + { + Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " + "b/c it's integer: " + << minVar << ":" << minVar.getType() << " |-> " + << elim << ":" << elim.getType() << endl; } } } |