diff options
author | Tim King <taking@cs.nyu.edu> | 2014-02-19 15:50:34 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-02-19 15:50:34 -0500 |
commit | efbc146839e98272d18fcfae0b62f07c4025449d (patch) | |
tree | 2c72a5b253939d6a28d5c5ddfe02b4f8e2bb9644 /src/theory/arith | |
parent | eb5debabce433774a0dbfd46745efb8fcf38b8ab (diff) | |
parent | cca221de7d29e86fd770af3aca0efc0d877dff26 (diff) |
Merge branch '1.3.x'
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.h | 2 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 12 |
4 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 92cd50864..39c2d859b 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -141,6 +141,10 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){ Assert(eq.getNode().getKind() == kind::EQUAL); SumPair sp = eq.toSumPair(); + if(sp.isNonlinear()){ + return; + } + uint32_t length = sp.maxLength(); if(length > d_maxInputCoefficientLength){ d_maxInputCoefficientLength = length; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index f19291c98..5039f826c 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -191,6 +191,8 @@ public: * orig can either be of the form (= p c) or (and ub lb). * where ub is either (leq p c) or (not (> p [- c 1])), and * where lb is either (geq p c) or (not (< p [+ c 1])) + * + * If eq cannot be used, this constraint is dropped. */ void pushInputConstraint(const Comparison& eq, Node reason); diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 7cd202e53..4edc55cca 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -1084,6 +1084,17 @@ Node Polynomial::makeAbsCondition(Variable v, Polynomial p){ return absCnd; } +bool Polynomial::isNonlinear() const { + + for(iterator i=begin(), iend =end(); i != iend; ++i){ + Monomial m = *i; + if(m.isNonlinear()){ + return true; + } + } + return false; +} + } //namespace arith } //namespace theory } //namespace CVC4 diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 1dddb5a5b..cd5f047b5 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -708,6 +708,11 @@ public: return integralCoefficient() && integralVariables(); } + /** Returns true if the VarList is a product of at least 2 Variables.*/ + bool isNonlinear() const { + return getVarList().size() >= 2; + } + /** * Given a sorted list of monomials, this function transforms this * into a strictly sorted list of monomials that does not contain zero. @@ -933,6 +938,9 @@ public: return true; } + /** Returns true if the polynomial contains a non-linear monomial.*/ + bool isNonlinear() const; + /** * Selects a minimal monomial in the polynomial by the absolute value of * the coefficient. @@ -1165,6 +1173,10 @@ public: return getConstant().isZero() && isConstant(); } + bool isNonlinear() const{ + return getPolynomial().isNonlinear(); + } + /** * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant(). * The SumPair must be integral. |