Analysis: fix bugs 75/17275/2
Calixte DENIZET [Wed, 30 Sep 2015 17:47:32 +0000 (19:47 +0200)]
Change-Id: I43a658fce22f4c873eb52ac6b9b333497b1c4f33

scilab/modules/ast/includes/analysis/gvn/SymbolicList.hxx
scilab/modules/ast/src/cpp/analysis/FunctionBlock.cpp
scilab/modules/ast/src/cpp/analysis/IndexAnalyzer.cpp
scilab/modules/ast/src/cpp/analysis/InferenceConstraints.cpp
scilab/modules/ast/src/cpp/analysis/MultivariatePolynomial.cpp

index 8ac5212..5fa66a5 100644 (file)
@@ -30,14 +30,14 @@ class SymbolicList
 
     union Value
     {
-       GVN::Value * gvnVal;
-       double dval;
+        GVN::Value * gvnVal;
+        double dval;
 
-       Value() { }
-       Value(GVN::Value * val) : gvnVal(val) { }
-       Value(double val) : dval(val) { }
+        Value() { }
+        Value(GVN::Value * val) : gvnVal(val) { }
+        Value(double val) : dval(val) { }
     };
-    
+
     Value start;
     Value step;
     Value end;
@@ -73,99 +73,97 @@ public:
     SymbolicList(SymbolicList && sl) : symbolic(sl.symbolic), start(sl.start), step(sl.step), end(sl.end) { }
 
     inline SymbolicList & operator=(SymbolicList && sl)
-       {
-           symbolic = sl.symbolic;
-           start = sl.start;
-           step = sl.step;
-           end = sl.end;
+    {
+        symbolic = sl.symbolic;
+        start = sl.start;
+        step = sl.step;
+        end = sl.end;
 
-           return *this;
-       }
+        return *this;
+    }
 
     inline bool isSymbolic() const
-       {
-           return symbolic;
-       }
+    {
+        return symbolic;
+    }
 
     inline void setStart(GVN::Value * val)
-       {
-           start.gvnVal = val;
-       }
+    {
+        start.gvnVal = val;
+    }
 
     inline void setStep(GVN::Value * val)
-       {
-           step.gvnVal = val;
-       }
+    {
+        step.gvnVal = val;
+    }
 
     inline void setEnd(GVN::Value * val)
-       {
-           end.gvnVal = val;
-       }
-    
+    {
+        end.gvnVal = val;
+    }
+
     inline GVN::Value * getStart() const
-       {
-           return start.gvnVal;
-       }
+    {
+        return start.gvnVal;
+    }
 
     inline GVN::Value * getStep() const
-       {
-           return step.gvnVal;
-       }
+    {
+        return step.gvnVal;
+    }
 
     inline GVN::Value * getEnd() const
-       {
-           return end.gvnVal;
-       }
+    {
+        return end.gvnVal;
+    }
 
     inline double getStart(double) const
-       {
-           return start.dval;
-       }
-    
+    {
+        return start.dval;
+    }
+
     inline double getStep(double) const
-       {
-           return step.dval;
-       }
+    {
+        return step.dval;
+    }
 
     inline double getEnd(double) const
-       {
-           return end.dval;
-       }
-    
+    {
+        return end.dval;
+    }
+
     bool getType(GVN & gvn, TIType & type) const;
     void evalDollar(GVN & gvn, const GVN::Value * dollarVal);
     bool checkAsIndex(const GVN::Value * dim);
-   
+
     static bool get(AnalysisVisitor & visitor, ast::ListExp & le, SymbolicList & sl);
-    
+
     /**
      * \brief Overload of the << operator
      */
     friend inline std::wostream & operator<<(std::wostream & out, const SymbolicList & sl)
     {
-       if (sl.symbolic)
-       {
-           out << *sl.start.gvnVal->poly << L" : " << *sl.step.gvnVal->poly << L" : " << *sl.end.gvnVal->poly;
-       }
-       else
-       {
-           out << sl.start.dval << L" : " << sl.step.dval << L" : " << sl.end.dval;
-       }
+        if (sl.symbolic)
+        {
+            out << *sl.start.gvnVal->poly << L" : " << *sl.step.gvnVal->poly << L" : " << *sl.end.gvnVal->poly;
+        }
+        else
+        {
+            out << sl.start.dval << L" : " << sl.step.dval << L" : " << sl.end.dval;
+        }
         return out;
     }
 
-private:
-
     inline static GVN::Value * evalDollar(GVN & gvn, const GVN::Value * value, const GVN::Value * dollar, const GVN::Value * dollarVal)
-       {
-           if (value->poly->contains(dollar->value))
-           {
-               const MultivariatePolynomial & mp = value->poly->eval(std::pair<unsigned long long, const MultivariatePolynomial *>(dollar->value, dollarVal->poly));
-               return gvn.getValue(mp);
-           }
-
-           return nullptr;
-       }
+    {
+        if (value->poly->contains(dollar->value))
+        {
+            const MultivariatePolynomial & mp = value->poly->eval(std::pair<unsigned long long, const MultivariatePolynomial *>(dollar->value, dollarVal->poly));
+            return gvn.getValue(mp);
+        }
+
+        return nullptr;
+    }
 };
 
 } // namespace analysis
index 7ee083b..7e7b3c0 100644 (file)
@@ -303,7 +303,7 @@ std::wostream & operator<<(std::wostream & out, const FunctionBlock & fblock)
         }
     }
 
-    ast::PrettyPrintVisitor dv(out);
+    ast::PrettyPrintVisitor dv(out, true, true);
     fblock.exp->accept(dv);
 
     return out;
index bd8ecc9..7707eb3 100644 (file)
@@ -311,6 +311,27 @@ bool AnalysisVisitor::getDimension(SymbolicDimension & dim, ast::Exp & arg, bool
                 return true;
             }
 
+            if (GVN::Value * const v = _res.getConstant().getGVNValue())
+            {
+                if (GVN::Value * const dollar = getGVN().getExistingValue(symbol::Symbol(L"$")))
+                {
+                    if (GVN::Value * const w = SymbolicList::evalDollar(getGVN(), v, dollar, dim.getValue()))
+                    {
+                        bool b = getCM().check(ConstraintManager::GREATER, dim.getValue(), w);
+                        if (b)
+                        {
+                            safe = getCM().check(ConstraintManager::STRICT_POSITIVE, w);
+                        }
+                        else
+                        {
+                            safe = false;
+                        }
+                        out = SymbolicDimension(getGVN(), 1);
+                        return true;
+                    }
+                }
+            }
+
             // To use with find
             // e.g. a(find(a > 0)): find(a > 0) return a matrix where the max index is rc(a) so the extraction is safe
             if (_res.getType().ismatrix() && _res.getType().type != TIType::BOOLEAN)
index 6909c6d..bd01aaf 100644 (file)
 
 namespace analysis
 {
-    InferenceConstraint::Result SameDimsConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
-    {
-        const GVN::Value & R1 = *values[0];
-        const GVN::Value & C1 = *values[1];
-        const GVN::Value & R2 = *values[2];
-        const GVN::Value & C2 = *values[3];
+InferenceConstraint::Result SameDimsConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & R1 = *values[0];
+    const GVN::Value & C1 = *values[1];
+    const GVN::Value & R2 = *values[2];
+    const GVN::Value & C2 = *values[3];
 
-        if (R1.value == R2.value)
+    if (R1.value == R2.value)
+    {
+        if (C1.value == C2.value)
         {
-            if (C1.value == C2.value)
-            {
-                return Result::RESULT_TRUE;
-            }
+            return Result::RESULT_TRUE;
+        }
 
-            MultivariatePolynomial mp = *C1.poly - *C2.poly;
-            if (mp.constant != 0 && mp.isCoeffPositive(false))
-            {
-                return Result::RESULT_FALSE;
-            }
+        MultivariatePolynomial mp = *C1.poly - *C2.poly;
+        if (mp.constant != 0 && mp.isCoeffPositive(false))
+        {
+            return Result::RESULT_FALSE;
         }
-        else
+    }
+    else
+    {
+        MultivariatePolynomial mp = *R1.poly - *R2.poly;
+        if (mp.constant > 0 && mp.isCoeffPositive(false))
         {
-            MultivariatePolynomial mp = *R1.poly - *R2.poly;
-            if (mp.constant > 0 && mp.isCoeffPositive(false))
-            {
-                return Result::RESULT_FALSE;
-            }
+            return Result::RESULT_FALSE;
         }
-        return Result::RESULT_DUNNO;
     }
+    return Result::RESULT_DUNNO;
+}
 
-    MPolyConstraintSet SameDimsConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(2);
-        const GVN::Value & R1 = *values[0];
-        const GVN::Value & C1 = *values[1];
-        const GVN::Value & R2 = *values[2];
-        const GVN::Value & C2 = *values[3];
+MPolyConstraintSet SameDimsConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(2);
+    const GVN::Value & R1 = *values[0];
+    const GVN::Value & C1 = *values[1];
+    const GVN::Value & R2 = *values[2];
+    const GVN::Value & C2 = *values[3];
 
-        set.add(*R1.poly - *R2.poly, MPolyConstraint::Kind::EQ0);
-        set.add(*C1.poly - *C2.poly, MPolyConstraint::Kind::EQ0);
+    set.add(*R1.poly - *R2.poly, MPolyConstraint::Kind::EQ0);
+    set.add(*C1.poly - *C2.poly, MPolyConstraint::Kind::EQ0);
 
-        return set;
-    }
+    return set;
+}
 
-    void SameDimsConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        GVN::Value & R1 = *values[0];
-        GVN::Value & C1 = *values[1];
-        GVN::Value & R2 = *values[2];
-        GVN::Value & C2 = *values[3];
+void SameDimsConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
+{
+    GVN::Value & R1 = *values[0];
+    GVN::Value & C1 = *values[1];
+    GVN::Value & R2 = *values[2];
+    GVN::Value & C2 = *values[3];
 
-        applyEquality(R1, R2);
-        applyEquality(C1, C2);
-    }
+    applyEquality(R1, R2);
+    applyEquality(C1, C2);
+}
 
-    InferenceConstraint::Result EqualConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
-    {
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+InferenceConstraint::Result EqualConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
 
-        if (x.value == y.value)
-        {
-            return Result::RESULT_TRUE;
-        }
-        else
+    if (x.value == y.value)
+    {
+        return Result::RESULT_TRUE;
+    }
+    else
+    {
+        MultivariatePolynomial mp = *x.poly - *y.poly;
+        if (mp.constant > 0 && mp.isCoeffPositive(false))
         {
-            MultivariatePolynomial mp = *x.poly - *y.poly;
-            if (mp.constant > 0 && mp.isCoeffPositive(false))
-            {
-                return Result::RESULT_FALSE;
-            }
+            return Result::RESULT_FALSE;
         }
-        return Result::RESULT_DUNNO;
     }
+    return Result::RESULT_DUNNO;
+}
 
-    void EqualConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        GVN::Value & x = *values[0];
-        GVN::Value & y = *values[1];
+void EqualConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
+{
+    GVN::Value & x = *values[0];
+    GVN::Value & y = *values[1];
 
-        applyEquality(x, y);
-    }
+    applyEquality(x, y);
+}
 
-    MPolyConstraintSet EqualConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+MPolyConstraintSet EqualConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
 
-        set.add(*x.poly - *y.poly, MPolyConstraint::Kind::EQ0);
+    set.add(*x.poly - *y.poly, MPolyConstraint::Kind::EQ0);
 
-        return set;
-    }
+    return set;
+}
 
-    InferenceConstraint::Result MPolyConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
-    {
-        const std::vector<const MultivariatePolynomial *> & args = InferenceConstraint::getArgs(values);
-        MultivariatePolynomial mp;// = poly.eval();
+InferenceConstraint::Result MPolyConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const std::vector<const MultivariatePolynomial *> & args = InferenceConstraint::getArgs(values);
+    MultivariatePolynomial mp;
 
-        if (poly.containsVarsGEq(args.size()))
-        {
-            mp = poly.eval(args);
-        }
-        else
-        {
-            mp = poly.translateVariables(gvn.getCurrentValue() + 1, args.size()).eval(args);
-        }
+    if (poly.containsVarsGEq(args.size()))
+    {
+        mp = poly.translateVariables(gvn.getCurrentValue() + 1, args.size()).eval(args);
+    }
+    else
+    {
+        mp = poly.eval(args);
+    }
 
-        switch (kind)
-        {
+    switch (kind)
+    {
         case EQ0:
         {
             if (mp.isConstant(0))
@@ -183,279 +183,279 @@ namespace analysis
                 return Result::RESULT_DUNNO;
             }
         }
-        }
     }
+}
 
-    MPolyConstraintSet MPolyConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        set.add(poly.eval(InferenceConstraint::getArgs(values)), kind);
+MPolyConstraintSet MPolyConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    set.add(poly.eval(InferenceConstraint::getArgs(values)), kind);
 
-        return set;
-    }
+    return set;
+}
 
-    void MPolyConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
+void MPolyConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const
+{
+    if (kind == EQ0)
     {
-        if (kind == EQ0)
+        if (poly.constant == 0 && poly.polynomial.size() == 2)
         {
-            if (poly.constant == 0 && poly.polynomial.size() == 2)
-            {
-                const MultivariateMonomial & m1 = *poly.polynomial.begin();
-                const MultivariateMonomial & m2 = *std::next(poly.polynomial.begin());
+            const MultivariateMonomial & m1 = *poly.polynomial.begin();
+            const MultivariateMonomial & m2 = *std::next(poly.polynomial.begin());
 
-                if (((m1.coeff == 1 && m2.coeff == -1) || (m1.coeff == -1 && m2.coeff == 1)) && (m1.monomial.size() == 1 && m2.monomial.size() == 1))
-                {
-                    // We have a polynomial P such as P(X,Y)=X-Y
-                    GVN::Value & x = *values[m1.monomial.begin()->var];
-                    GVN::Value & y = *values[m2.monomial.begin()->var];
+            if (((m1.coeff == 1 && m2.coeff == -1) || (m1.coeff == -1 && m2.coeff == 1)) && (m1.monomial.size() == 1 && m2.monomial.size() == 1))
+            {
+                // We have a polynomial P such as P(X,Y)=X-Y
+                GVN::Value & x = *values[m1.monomial.begin()->var];
+                GVN::Value & y = *values[m2.monomial.begin()->var];
 
-                    applyEquality(x, y);
-                }
+                applyEquality(x, y);
             }
         }
     }
+}
 
-    InferenceConstraint::Result MPolyConstraintSet::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+InferenceConstraint::Result MPolyConstraintSet::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    for (const auto & constraint : constraints)
     {
-        for (const auto & constraint : constraints)
+        Result res = constraint.check(gvn, values);
+        if (res != Result::RESULT_TRUE)
         {
-            Result res = constraint.check(gvn, values);
-            if (res != Result::RESULT_TRUE)
-            {
-                return res;
-            }
+            return res;
         }
-        return Result::RESULT_TRUE;
     }
+    return Result::RESULT_TRUE;
+}
 
-    MPolyConstraintSet MPolyConstraintSet::getMPConstraints(const std::vector<GVN::Value *> & values) const
+MPolyConstraintSet MPolyConstraintSet::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(constraints.size());
+    const std::vector<const MultivariatePolynomial *> args = InferenceConstraint::getArgs(values);
+    for (const auto & constraint : constraints)
     {
-        MPolyConstraintSet set(constraints.size());
-        const std::vector<const MultivariatePolynomial *> args = InferenceConstraint::getArgs(values);
-        for (const auto & constraint : constraints)
-        {
-            set.add(constraint.poly.eval(args), constraint.kind);
-        }
-        return set;
+        set.add(constraint.poly.eval(args), constraint.kind);
     }
+    return set;
+}
 
-    void MPolyConstraintSet::applyConstraints(const std::vector<GVN::Value *> & values) const
+void MPolyConstraintSet::applyConstraints(const std::vector<GVN::Value *> & values) const
+{
+    for (const auto & mpc : constraints)
     {
-        for (const auto & mpc : constraints)
-        {
-            mpc.applyConstraints(values);
-        }
+        mpc.applyConstraints(values);
     }
+}
 
-    InferenceConstraint::Result PositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+InferenceConstraint::Result PositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & x = *values[0];
+
+    if (x.poly->isCoeffPositive())
+    {
+        return Result::RESULT_TRUE;
+    }
+    else if (x.poly->isConstant() && x.poly->constant < 0)
     {
-        const GVN::Value & x = *values[0];
+        return Result::RESULT_FALSE;
+    }
 
-        if (x.poly->isCoeffPositive())
-        {
-            return Result::RESULT_TRUE;
-        }
-        else if (x.poly->isConstant() && x.poly->constant < 0)
-        {
-            return Result::RESULT_FALSE;
-        }
+    return Result::RESULT_DUNNO;
+}
 
-        return Result::RESULT_DUNNO;
-    }
+void PositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
 
-    void PositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+MPolyConstraintSet PositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    const GVN::Value & x = *values[0];
 
-    MPolyConstraintSet PositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        const GVN::Value & x = *values[0];
+    set.add(*x.poly, MPolyConstraint::Kind::GEQ0);
 
-        set.add(*x.poly, MPolyConstraint::Kind::GEQ0);
+    return set;
+}
 
-        return set;
-    }
+InferenceConstraint::Result StrictPositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & x = *values[0];
 
-    InferenceConstraint::Result StrictPositiveConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+    if (x.poly->isCoeffStrictPositive())
     {
-        const GVN::Value & x = *values[0];
+        return Result::RESULT_TRUE;
+    }
+    else if (x.poly->isConstant() && x.poly->constant <= 0)
+    {
+        return Result::RESULT_FALSE;
+    }
 
-        if (x.poly->isCoeffStrictPositive())
-        {
-            return Result::RESULT_TRUE;
-        }
-        else if (x.poly->isConstant() && x.poly->constant <= 0)
-        {
-            return Result::RESULT_FALSE;
-        }
+    return Result::RESULT_DUNNO;
+}
 
-        return Result::RESULT_DUNNO;
-    }
+void StrictPositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
 
-    void StrictPositiveConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+MPolyConstraintSet StrictPositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    const GVN::Value & x = *values[0];
 
-    MPolyConstraintSet StrictPositiveConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        const GVN::Value & x = *values[0];
+    set.add(*x.poly, MPolyConstraint::Kind::GT0);
+
+    return set;
+}
 
-        set.add(*x.poly, MPolyConstraint::Kind::GT0);
+InferenceConstraint::Result StrictGreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
 
-        return set;
+    if (x.value == y.value)
+    {
+        return Result::RESULT_FALSE;
     }
-    
-    InferenceConstraint::Result StrictGreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+
+    MultivariatePolynomial mp = *x.poly - *y.poly;
+    if (mp.constant > 0 && mp.isCoeffPositive(false))
     {
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+        return Result::RESULT_TRUE;
+    }
+    else if (mp.constant < 0 && mp.isCoeffNegative(false))
+    {
+        return Result::RESULT_FALSE;
+    }
 
-        if (x.value == y.value)
-        {
-            return Result::RESULT_FALSE;
-        }
+    return Result::RESULT_DUNNO;
+}
 
-        MultivariatePolynomial mp = *x.poly - *y.poly;
-        if (mp.constant > 0 && mp.isCoeffPositive(false))
-        {
-            return Result::RESULT_TRUE;
-        }
-        else if (mp.constant < 0 && mp.isCoeffNegative(false))
-        {
-            return Result::RESULT_FALSE;
-        }
+void StrictGreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
 
-        return Result::RESULT_DUNNO;
-    }
+MPolyConstraintSet StrictGreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
 
-    void StrictGreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+    set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GT0);
 
-    MPolyConstraintSet StrictGreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+    return set;
+}
 
-        set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GT0);
+InferenceConstraint::Result GreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
 
-        return set;
+    if (x.value == y.value)
+    {
+        return Result::RESULT_TRUE;
     }
 
-    InferenceConstraint::Result GreaterConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+    MultivariatePolynomial mp = *x.poly - *y.poly;
+    if (mp.isCoeffPositive(true))
     {
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+        return Result::RESULT_TRUE;
+    }
+    else if (mp.constant < 0 && mp.isCoeffNegative(false))
+    {
+        return Result::RESULT_FALSE;
+    }
 
-        if (x.value == y.value)
-        {
-            return Result::RESULT_TRUE;
-        }
+    return Result::RESULT_DUNNO;
+}
 
-        MultivariatePolynomial mp = *x.poly - *y.poly;
-        if (mp.isCoeffPositive(true))
+void GreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+
+MPolyConstraintSet GreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(1);
+    const GVN::Value & x = *values[0];
+    const GVN::Value & y = *values[1];
+
+    set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GEQ0);
+
+    return set;
+}
+
+InferenceConstraint::Result ValidIndexConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & index = *values[0];
+    const GVN::Value & max = *values[1];
+    if (index.poly->constant > 0 && index.poly->isCoeffPositive(false))
+    {
+        // the index is geq than 1
+        MultivariatePolynomial mp = *max.poly - *index.poly;
+        if (mp.isCoeffPositive())
         {
+            // max - index >= 0
             return Result::RESULT_TRUE;
         }
-        else if (mp.constant < 0 && mp.isCoeffNegative(false))
+        else if (mp.isConstant() && mp.constant < 0)
         {
             return Result::RESULT_FALSE;
         }
-
-        return Result::RESULT_DUNNO;
     }
+    else if (index.poly->isConstant() && index.poly->constant < 1)
+    {
+        return Result::RESULT_FALSE;
+    }
+
+    return Result::RESULT_DUNNO;
+}
 
-    void GreaterConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+void ValidIndexConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
 
-    MPolyConstraintSet GreaterConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(1);
-        const GVN::Value & x = *values[0];
-        const GVN::Value & y = *values[1];
+MPolyConstraintSet ValidIndexConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(2);
+    const GVN::Value & index = *values[0];
+    const GVN::Value & max = *values[1];
 
-        set.add(*x.poly - *y.poly, MPolyConstraint::Kind::GEQ0);
+    set.add(*max.poly - *index.poly, MPolyConstraint::Kind::GEQ0);
+    set.add(*index.poly - 1, MPolyConstraint::Kind::GEQ0);
 
-        return set;
-    }
+    return set;
+}
+
+InferenceConstraint::Result ValidRangeConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+{
+    const GVN::Value & index_min = *values[0];
+    const GVN::Value & index_max = *values[1];
+    const GVN::Value & min = *values[2];
+    const GVN::Value & max = *values[3];
 
-    InferenceConstraint::Result ValidIndexConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
+    MultivariatePolynomial mp_min = *index_min.poly - *min.poly;
+    if (mp_min.isCoeffPositive())
     {
-        const GVN::Value & index = *values[0];
-        const GVN::Value & max = *values[1];
-        if (index.poly->constant > 0 && index.poly->isCoeffPositive(false))
+        MultivariatePolynomial mp_max = *max.poly - *index_max.poly;
+        if (mp_max.isCoeffPositive())
         {
-            // the index is geq than 1
-            MultivariatePolynomial mp = *max.poly - *index.poly;
-            if (mp.isCoeffPositive())
-            {
-                // max - index >= 0
-                return Result::RESULT_TRUE;
-            }
-            else if (mp.isConstant() && mp.constant < 0)
-            {
-                return Result::RESULT_FALSE;
-            }
+            return Result::RESULT_TRUE;
         }
-        else if (index.poly->isConstant() && index.poly->constant < 1)
+        else if (mp_max.isConstant() && mp_max.constant < 0)
         {
             return Result::RESULT_FALSE;
         }
-
-        return Result::RESULT_DUNNO;
     }
-
-    void ValidIndexConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
-
-    MPolyConstraintSet ValidIndexConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+    else if (mp_min.isConstant() && mp_min.constant < 0)
     {
-        MPolyConstraintSet set(2);
-        const GVN::Value & index = *values[0];
-        const GVN::Value & max = *values[1];
-
-        set.add(*max.poly - *index.poly, MPolyConstraint::Kind::GEQ0);
-        set.add(*index.poly - 1, MPolyConstraint::Kind::GEQ0);
-
-        return set;
+        return Result::RESULT_FALSE;
     }
 
-    InferenceConstraint::Result ValidRangeConstraint::check(GVN & gvn, const std::vector<GVN::Value *> & values) const
-    {
-        const GVN::Value & index_min = *values[0];
-       const GVN::Value & index_max = *values[1];
-        const GVN::Value & min = *values[2];
-       const GVN::Value & max = *values[3];
-
-       MultivariatePolynomial mp_min = *index_min.poly - *min.poly;
-       if (mp_min.isCoeffPositive())
-       {
-           MultivariatePolynomial mp_max = *max.poly - *index_max.poly;
-           if (mp_max.isCoeffPositive())
-           {
-               return Result::RESULT_TRUE;
-           }
-           else if (mp_max.isConstant() && mp_max.constant < 0)
-            {
-                return Result::RESULT_FALSE;
-            }
-       }
-       else if (mp_min.isConstant() && mp_min.constant < 0)
-       {
-           return Result::RESULT_FALSE;
-       }
-       
-        return Result::RESULT_DUNNO;
-    }
+    return Result::RESULT_DUNNO;
+}
 
-    void ValidRangeConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
+void ValidRangeConstraint::applyConstraints(const std::vector<GVN::Value *> & values) const { }
 
-    MPolyConstraintSet ValidRangeConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
-    {
-        MPolyConstraintSet set(4);
-       const GVN::Value & index_min = *values[0];
-       const GVN::Value & index_max = *values[1];
-        const GVN::Value & min = *values[2];
-       const GVN::Value & max = *values[3];
+MPolyConstraintSet ValidRangeConstraint::getMPConstraints(const std::vector<GVN::Value *> & values) const
+{
+    MPolyConstraintSet set(4);
+    const GVN::Value & index_min = *values[0];
+    const GVN::Value & index_max = *values[1];
+    const GVN::Value & min = *values[2];
+    const GVN::Value & max = *values[3];
 
-        set.add(*index_min.poly - *min.poly, MPolyConstraint::Kind::GEQ0);
-        set.add(*max.poly - *index_max.poly, MPolyConstraint::Kind::GEQ0);
+    set.add(*index_min.poly - *min.poly, MPolyConstraint::Kind::GEQ0);
+    set.add(*max.poly - *index_max.poly, MPolyConstraint::Kind::GEQ0);
 
-        return set;
-    }
+    return set;
+}
 }
index 6f07562..ab564f2 100644 (file)
 namespace analysis
 {
 
-    MultivariatePolynomial MultivariatePolynomial::getInvalid()
-    {
-        return MultivariatePolynomial(0, false);
-    }
-
-    bool MultivariatePolynomial::isValid() const
-    {
-        return valid;
-    }
+MultivariatePolynomial MultivariatePolynomial::getInvalid()
+{
+    return MultivariatePolynomial(0, false);
+}
 
-    bool MultivariatePolynomial::isInvalid() const
-    {
-        return !valid;
-    }
+bool MultivariatePolynomial::isValid() const
+{
+    return valid;
+}
 
-    void MultivariatePolynomial::invalid()
-    {
-        constant = 0;
-       valid = false;
-        polynomial.clear();
-    }
+bool MultivariatePolynomial::isInvalid() const
+{
+    return !valid;
+}
 
-    bool MultivariatePolynomial::contains(const uint64_t var) const
-       {
-           for (const auto & m : polynomial)
-           {
-               if (m.contains(var))
-               {
-                   return true;
-               }
-           }
+void MultivariatePolynomial::invalid()
+{
+    constant = 0;
+    valid = false;
+    polynomial.clear();
+}
 
-           return false;
-       }
-    
-    bool MultivariatePolynomial::checkVariable(const uint64_t max) const
+bool MultivariatePolynomial::contains(const uint64_t var) const
+{
+    for (const auto & m : polynomial)
     {
-        for (const auto & m : polynomial)
+        if (m.contains(var))
         {
-            if (!m.checkVariable(max))
-            {
-                return false;
-            }
+            return true;
         }
-        return true;
     }
 
-    bool MultivariatePolynomial::containsVarsGEq(const uint64_t min) const
+    return false;
+}
+
+bool MultivariatePolynomial::checkVariable(const uint64_t max) const
+{
+    for (const auto & m : polynomial)
     {
-        for (const auto & m : polynomial)
+        if (!m.checkVariable(max))
         {
-           if (m.monomial.lower_bound(min) != m.monomial.end())
-           {
-               return true;
-           }
+            return false;
         }
-
-       return false;
     }
-    
-    MultivariatePolynomial MultivariatePolynomial::translateVariables(const uint64_t t, const uint64_t min) const
+    return true;
+}
+
+bool MultivariatePolynomial::containsVarsGEq(const uint64_t min) const
+{
+    for (const auto & m : polynomial)
     {
-       MultivariatePolynomial mp;
-        for (const auto & m : polynomial)
+        if (m.monomial.lower_bound(min) != m.monomial.end())
         {
-           MultivariateMonomial mm(m);
-           MultivariateMonomial::Monomial::iterator i = mm.monomial.lower_bound(min);
-           if (i != mm.monomial.end())
-           {
-               // We don't modify the order in the set, so we can const_cast
-               for (MultivariateMonomial::Monomial::iterator j = std::prev(mm.monomial.end()); j != i; --j)
-               {
-                   const_cast<VarExp &>(*j).var += t;
-               }
-               const_cast<VarExp &>(*i).var += t;
-           }
-           mp.add(mm);
+            return true;
         }
-
-       return mp;
     }
 
-    MultivariatePolynomial & MultivariatePolynomial::add(const MultivariateMonomial & m, const int64_t coeff)
+    return false;
+}
+
+MultivariatePolynomial MultivariatePolynomial::translateVariables(const uint64_t t, const uint64_t min) const
+{
+    MultivariatePolynomial mp(polynomial.size(), constant);
+    for (const auto & m : polynomial)
     {
-        const int64_t c = m.coeff * coeff;
-        if (c)
+        MultivariateMonomial mm(m);
+        MultivariateMonomial::Monomial::iterator i = mm.monomial.lower_bound(min);
+        if (i != mm.monomial.end())
         {
-            Polynomial::iterator i = polynomial.find(m);
-            if (i == polynomial.end())
+            // We don't modify the order in the set, so we can const_cast
+            for (MultivariateMonomial::Monomial::iterator j = std::prev(mm.monomial.end()); j != i; --j)
             {
-                Polynomial::iterator j = polynomial.insert(m).first;
-                j->coeff = c;
-            }
-            else
-            {
-                if (i->coeff == -c)
-                {
-                    polynomial.erase(i);
-                }
-                else
-                {
-                    i->coeff += c;
-                }
+                const_cast<VarExp &>(*j).var += t;
             }
+            const_cast<VarExp &>(*i).var += t;
         }
-        return *this;
+        mp.add(mm);
     }
 
-    void MultivariatePolynomial::sub(const MultivariateMonomial & m)
+    return mp;
+}
+
+MultivariatePolynomial & MultivariatePolynomial::add(const MultivariateMonomial & m, const int64_t coeff)
+{
+    const int64_t c = m.coeff * coeff;
+    if (c)
     {
         Polynomial::iterator i = polynomial.find(m);
         if (i == polynomial.end())
         {
-            if (m.coeff)
-            {
-                polynomial.insert(m).first->coeff = -m.coeff;
-            }
+            Polynomial::iterator j = polynomial.insert(m).first;
+            j->coeff = c;
         }
         else
         {
-            if (i->coeff == m.coeff)
+            if (i->coeff == -c)
             {
                 polynomial.erase(i);
             }
             else
             {
-                i->coeff -= m.coeff;
+                i->coeff += c;
             }
         }
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator+(const MultivariateMonomial & R) const
+void MultivariatePolynomial::sub(const MultivariateMonomial & m)
+{
+    Polynomial::iterator i = polynomial.find(m);
+    if (i == polynomial.end())
     {
-        if (isValid())
+        if (m.coeff)
         {
-            MultivariatePolynomial res(*this);
-            res.add(R);
-            return res;
+            polynomial.insert(m).first->coeff = -m.coeff;
         }
-        return getInvalid();
     }
-
-    MultivariatePolynomial & MultivariatePolynomial::operator+=(const MultivariateMonomial & R)
+    else
     {
-        if (isValid())
+        if (i->coeff == m.coeff)
+        {
+            polynomial.erase(i);
+        }
+        else
         {
-            add(R);
+            i->coeff -= m.coeff;
         }
-        return *this;
     }
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator+(const int64_t R) const
+MultivariatePolynomial MultivariatePolynomial::operator+(const MultivariateMonomial & R) const
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            MultivariatePolynomial res(*this);
-            res.constant += R;
-            return res;
-        }
-        return *this;
+        MultivariatePolynomial res(*this);
+        res.add(R);
+        return res;
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator+=(const int64_t R)
+MultivariatePolynomial & MultivariatePolynomial::operator+=(const MultivariateMonomial & R)
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            constant += R;
-        }
-        return *this;
+        add(R);
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator-(const MultivariateMonomial & R) const
+MultivariatePolynomial MultivariatePolynomial::operator+(const int64_t R) const
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            MultivariatePolynomial res(*this);
-            res.sub(R);
-            return res;
-        }
-        return *this;
+        MultivariatePolynomial res(*this);
+        res.constant += R;
+        return res;
     }
+    return *this;
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator-=(const MultivariateMonomial & R)
+MultivariatePolynomial & MultivariatePolynomial::operator+=(const int64_t R)
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            sub(R);
-        }
-        return *this;
+        constant += R;
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator-(const int64_t R) const
+MultivariatePolynomial MultivariatePolynomial::operator-(const MultivariateMonomial & R) const
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            MultivariatePolynomial res(*this);
-            res.constant -= R;
-            return res;
-        }
-        return *this;
+        MultivariatePolynomial res(*this);
+        res.sub(R);
+        return res;
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator-() const
+MultivariatePolynomial & MultivariatePolynomial::operator-=(const MultivariateMonomial & R)
+{
+    if (isValid())
     {
-        if (isValid())
-        {
-            MultivariatePolynomial res(*this);
-            res.constant = -res.constant;
-            for (auto & m : res.polynomial)
-            {
-                m.coeff = -m.coeff;
-            }
-            return res;
-        }
-        return *this;
+        sub(R);
     }
+    return *this;
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator-=(const int64_t R)
+MultivariatePolynomial MultivariatePolynomial::operator-(const int64_t R) const
+{
+    if (isValid())
     {
-        if (isValid())
+        MultivariatePolynomial res(*this);
+        res.constant -= R;
+        return res;
+    }
+    return *this;
+}
+
+MultivariatePolynomial MultivariatePolynomial::operator-() const
+{
+    if (isValid())
+    {
+        MultivariatePolynomial res(*this);
+        res.constant = -res.constant;
+        for (auto & m : res.polynomial)
         {
-            constant -= R;
+            m.coeff = -m.coeff;
         }
-        return *this;
+        return res;
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator+(const MultivariatePolynomial & R) const
+MultivariatePolynomial & MultivariatePolynomial::operator-=(const int64_t R)
+{
+    if (isValid())
     {
-        if (isValid() && R.isValid())
+        constant -= R;
+    }
+    return *this;
+}
+
+MultivariatePolynomial MultivariatePolynomial::operator+(const MultivariatePolynomial & R) const
+{
+    if (isValid() && R.isValid())
+    {
+        MultivariatePolynomial res(*this);
+        res.constant += R.constant;
+        for (const auto & m : R.polynomial)
         {
-            MultivariatePolynomial res(*this);
-            res.constant += R.constant;
-            for (const auto & m : R.polynomial)
-            {
-                res.add(m);
-            }
-            return res;
+            res.add(m);
         }
-        return getInvalid();
+        return res;
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator+=(const MultivariatePolynomial & R)
+MultivariatePolynomial & MultivariatePolynomial::operator+=(const MultivariatePolynomial & R)
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        constant += R.constant;
+        for (const auto & m : R.polynomial)
         {
-            constant += R.constant;
-            for (const auto & m : R.polynomial)
-            {
-                add(m);
-            }
+            add(m);
         }
-        else
+    }
+    else
+    {
+        invalid();
+    }
+
+    return *this;
+}
+
+MultivariatePolynomial MultivariatePolynomial::operator-(const MultivariatePolynomial & R) const
+{
+    if (isValid() && R.isValid())
+    {
+        MultivariatePolynomial res(*this);
+        res.constant -= R.constant;
+        for (const auto & m : R.polynomial)
         {
-            invalid();
+            res.sub(m);
         }
-
-        return *this;
+        return res;
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator-(const MultivariatePolynomial & R) const
+MultivariatePolynomial & MultivariatePolynomial::operator-=(const MultivariatePolynomial & R)
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        constant -= R.constant;
+        for (const auto & m : R.polynomial)
         {
-            MultivariatePolynomial res(*this);
-            res.constant -= R.constant;
-            for (const auto & m : R.polynomial)
-            {
-                res.sub(m);
-            }
-            return res;
+            sub(m);
         }
-        return getInvalid();
     }
+    else
+    {
+        invalid();
+    }
+    return *this;
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator-=(const MultivariatePolynomial & R)
+MultivariatePolynomial MultivariatePolynomial::operator*(const MultivariatePolynomial & R) const
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        if (R.isConstant())
         {
-            constant -= R.constant;
-            for (const auto & m : R.polynomial)
-            {
-                sub(m);
-            }
+            return *this * R.constant;
         }
-        else
+        else if (isConstant())
         {
-            invalid();
+            return R * constant;
         }
-        return *this;
-    }
-
-    MultivariatePolynomial MultivariatePolynomial::operator*(const MultivariatePolynomial & R) const
-    {
-        if (isValid() && R.isValid())
+        else
         {
-            if (R.isConstant())
+            MultivariatePolynomial res(static_cast<unsigned int>((polynomial.size() + 1) * (R.polynomial.size() + 1) - 1), constant * R.constant);
+            for (const auto & mR : R.polynomial)
             {
-                return *this * R.constant;
+                res.add(mR, constant);
             }
-            else if (isConstant())
-            {
-                return R * constant;
-            }
-            else
+            for (const auto & mL : polynomial)
             {
-                MultivariatePolynomial res(static_cast<unsigned int>((polynomial.size() + 1) * (R.polynomial.size() + 1) - 1), constant * R.constant);
+                res.add(mL, R.constant);
                 for (const auto & mR : R.polynomial)
                 {
-                    res.add(mR, constant);
-                }
-                for (const auto & mL : polynomial)
-                {
-                    res.add(mL, R.constant);
-                    for (const auto & mR : R.polynomial)
-                    {
-                        res.add(mL * mR);
-                    }
-                }
-                return res;
-            }
-        }
-        return getInvalid();
-    }
-
-    MultivariatePolynomial MultivariatePolynomial::operator/(const MultivariatePolynomial & R) const
-    {
-        if (isValid() && R.isValid())
-        {
-            if (R.isConstant())
-            {
-                if (R.constant != 1)
-                {
-                    return *this / R.constant;
-                }
-                else
-                {
-                    return *this;
+                    res.add(mL * mR);
                 }
             }
+            return res;
         }
-        return getInvalid();
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator/=(const MultivariatePolynomial & R)
+MultivariatePolynomial MultivariatePolynomial::operator/(const MultivariatePolynomial & R) const
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        if (R.isConstant())
         {
-            if (R.polynomial.empty())
+            if (R.constant != 1)
             {
-                constant /= R.constant;
-                for (auto & m : polynomial)
-                {
-                    m.coeff /= R.constant;
-                }
+                return *this / R.constant;
             }
             else
             {
-                MultivariatePolynomial res(*this / R);
-                polynomial = res.polynomial;
-                constant = res.constant;
+                return *this;
             }
         }
-        else
-        {
-            invalid();
-        }
-        return *this;
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator*=(const MultivariatePolynomial & R)
+MultivariatePolynomial & MultivariatePolynomial::operator/=(const MultivariatePolynomial & R)
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        if (R.polynomial.empty())
         {
-            if (R.polynomial.empty())
+            constant /= R.constant;
+            for (auto & m : polynomial)
             {
-                constant *= R.constant;
-                for (auto & m : polynomial)
-                {
-                    m.coeff *= R.constant;
-                }
-            }
-            else
-            {
-                MultivariatePolynomial res(*this * R);
-                polynomial = res.polynomial;
-                constant = res.constant;
+                m.coeff /= R.constant;
             }
         }
         else
         {
-            invalid();
+            MultivariatePolynomial res(*this / R);
+            polynomial = res.polynomial;
+            constant = res.constant;
         }
-        return *this;
     }
+    else
+    {
+        invalid();
+    }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator*(const MultivariateMonomial & R) const
+MultivariatePolynomial & MultivariatePolynomial::operator*=(const MultivariatePolynomial & R)
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid())
+        if (R.polynomial.empty())
         {
-            MultivariatePolynomial res(static_cast<unsigned int>(polynomial.size() + 1), int64_t(0));
-            res.add(constant * R);
-            for (const auto & mL : polynomial)
+            constant *= R.constant;
+            for (auto & m : polynomial)
             {
-                res.add(mL * R);
+                m.coeff *= R.constant;
             }
-            return res;
         }
         else
         {
-            return getInvalid();
-        }
-    }
-
-    MultivariatePolynomial & MultivariatePolynomial::operator*=(const MultivariateMonomial & R)
-    {
-        if (isValid())
-        {
-            MultivariatePolynomial res = *this * R;
+            MultivariatePolynomial res(*this * R);
             polynomial = res.polynomial;
             constant = res.constant;
         }
-        return *this;
     }
+    else
+    {
+        invalid();
+    }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator*(const int64_t R) const
+MultivariatePolynomial MultivariatePolynomial::operator*(const MultivariateMonomial & R) const
+{
+    if (isValid())
     {
-        if (isValid())
+        MultivariatePolynomial res(static_cast<unsigned int>(polynomial.size() + 1), int64_t(0));
+        res.add(constant * R);
+        for (const auto & mL : polynomial)
         {
-            if (R)
-            {
-                if (R == 1)
-                {
-                    return *this;
-                }
-                else
-                {
-                    MultivariatePolynomial res(*this);
-                    res.constant *= R;
-                    for (auto & m : res.polynomial)
-                    {
-                        m.coeff *= R;
-                    }
-                    return res;
-                }
-            }
-            else
-            {
-                return MultivariatePolynomial(int64_t(0));
-            }
+            res.add(mL * R);
         }
+        return res;
+    }
+    else
+    {
         return getInvalid();
     }
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator*=(const int64_t R)
+MultivariatePolynomial & MultivariatePolynomial::operator*=(const MultivariateMonomial & R)
+{
+    if (isValid())
     {
-        if (isValid())
+        MultivariatePolynomial res = *this * R;
+        polynomial = res.polynomial;
+        constant = res.constant;
+    }
+    return *this;
+}
+
+MultivariatePolynomial MultivariatePolynomial::operator*(const int64_t R) const
+{
+    if (isValid())
+    {
+        if (R)
         {
-            if (R == 0)
+            if (R == 1)
             {
-                constant = 0;
-                polynomial.clear();
+                return *this;
             }
-            else if (R != 1)
+            else
             {
-                constant *= R;
-                for (auto & m : polynomial)
+                MultivariatePolynomial res(*this);
+                res.constant *= R;
+                for (auto & m : res.polynomial)
                 {
                     m.coeff *= R;
                 }
+                return res;
             }
         }
-        return *this;
+        else
+        {
+            return MultivariatePolynomial(int64_t(0));
+        }
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator/(const int64_t R) const
+MultivariatePolynomial & MultivariatePolynomial::operator*=(const int64_t R)
+{
+    if (isValid())
     {
-        if (isValid())
+        if (R == 0)
+        {
+            constant = 0;
+            polynomial.clear();
+        }
+        else if (R != 1)
         {
-            if (R != 1)
+            constant *= R;
+            for (auto & m : polynomial)
             {
-                MultivariatePolynomial res(*this);
-                res.constant /= R;
-                for (auto & m : res.polynomial)
-                {
-                    m.coeff /= R;
-                }
-                return res;
+                m.coeff *= R;
             }
         }
-        return *this;
     }
+    return *this;
+}
 
-    MultivariatePolynomial & MultivariatePolynomial::operator/=(const int64_t R)
+MultivariatePolynomial MultivariatePolynomial::operator/(const int64_t R) const
+{
+    if (isValid())
     {
-        if (isValid())
+        if (R != 1)
         {
-            if (R != 1)
+            MultivariatePolynomial res(*this);
+            res.constant /= R;
+            for (auto & m : res.polynomial)
             {
-                constant /= R;
-                for (auto & m : polynomial)
-                {
-                    m.coeff /= R;
-                }
+                m.coeff /= R;
             }
+            return res;
         }
-        return *this;
     }
+    return *this;
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator^(unsigned int R) const
+MultivariatePolynomial & MultivariatePolynomial::operator/=(const int64_t R)
+{
+    if (isValid())
     {
-        if (isValid())
+        if (R != 1)
         {
-            if (R == 0)
-            {
-                return MultivariatePolynomial(int64_t(1));
-            }
-            else if (R == 1)
+            constant /= R;
+            for (auto & m : polynomial)
             {
-                return *this;
+                m.coeff /= R;
             }
-            else
+        }
+    }
+    return *this;
+}
+
+MultivariatePolynomial MultivariatePolynomial::operator^(unsigned int R) const
+{
+    if (isValid())
+    {
+        if (R == 0)
+        {
+            return MultivariatePolynomial(int64_t(1));
+        }
+        else if (R == 1)
+        {
+            return *this;
+        }
+        else
+        {
+            if (constant == 0)
             {
-                if (constant == 0)
+                if (polynomial.empty())
                 {
-                    if (polynomial.empty())
-                    {
-                        return MultivariatePolynomial(int64_t(0));
-                    }
-                    else if (polynomial.size() == 1)
-                    {
-                        const MultivariateMonomial & m = *polynomial.begin();
-                        MultivariatePolynomial res;
-                        res.polynomial.emplace(m ^ R);
-
-                        return res;
-                    }
+                    return MultivariatePolynomial(int64_t(0));
                 }
-
-                if (polynomial.empty())
+                else if (polynomial.size() == 1)
                 {
-                    return MultivariatePolynomial(tools::powui(constant, R));
+                    const MultivariateMonomial & m = *polynomial.begin();
+                    MultivariatePolynomial res;
+                    res.polynomial.emplace(m ^ R);
+
+                    return res;
                 }
+            }
+
+            if (polynomial.empty())
+            {
+                return MultivariatePolynomial(tools::powui(constant, R));
+            }
 
-                MultivariatePolynomial p = *this;
-                MultivariatePolynomial y = (R & 1) ? *this : MultivariatePolynomial(int64_t(1));
+            MultivariatePolynomial p = *this;
+            MultivariatePolynomial y = (R & 1) ? *this : MultivariatePolynomial(int64_t(1));
 
-                while (R >>= 1)
+            while (R >>= 1)
+            {
+                p *= p;
+                if (R & 1)
                 {
-                    p *= p;
-                    if (R & 1)
-                    {
-                        y *= p;
-                    }
+                    y *= p;
                 }
-
-                return y;
             }
+
+            return y;
         }
-        return getInvalid();
     }
+    return getInvalid();
+}
 
-    MultivariatePolynomial MultivariatePolynomial::operator^(const MultivariatePolynomial & R) const
+MultivariatePolynomial MultivariatePolynomial::operator^(const MultivariatePolynomial & R) const
+{
+    if (isValid() && R.isValid())
     {
-        if (isValid() && R.isValid())
+        if (R.isConstant() && R.constant == (unsigned int)R.constant)
         {
-            if (R.isConstant() && R.constant == (unsigned int)R.constant)
-            {
-                return (*this) ^ ((unsigned int)R.constant);
-            }
+            return (*this) ^ ((unsigned int)R.constant);
         }
-        return getInvalid();
     }
+    return getInvalid();
+}
 
-    bool MultivariatePolynomial::isDivisibleBy(const int64_t n) const
+bool MultivariatePolynomial::isDivisibleBy(const int64_t n) const
+{
+    if (constant % n == 0)
     {
-        if (constant % n == 0)
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff % n != 0)
             {
-                if (m.coeff % n != 0)
-                {
-                   return false;
-                }
+                return false;
             }
-            return true;
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    bool MultivariatePolynomial::isDivisibleBy(const MultivariatePolynomial & mp) const
+bool MultivariatePolynomial::isDivisibleBy(const MultivariatePolynomial & mp) const
+{
+    if (mp.polynomial.empty())
     {
-       if (mp.polynomial.empty())
-       {
-           return isDivisibleBy(mp.constant);
-       }
-
-       return false;
+        return isDivisibleBy(mp.constant);
     }
-    
-    bool MultivariatePolynomial::isPositive() const
+
+    return false;
+}
+
+bool MultivariatePolynomial::isPositive() const
+{
+    if (constant >= 0)
     {
-        if (constant >= 0)
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff >= 0)
             {
-                if (m.coeff >= 0)
+                for (const auto & ve : m.monomial)
                 {
-                    for (const auto & ve : m.monomial)
+                    if (ve.exp % 2) // exp is odd
                     {
-                        if (ve.exp % 2) // exp is odd
-                        {
-                            return false;
-                        }
+                        return false;
                     }
                 }
-                else
-                {
-                    return false;
-                }
             }
-            return true;
+            else
+            {
+                return false;
+            }
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    bool MultivariatePolynomial::isCoeffStrictPositive(const bool checkConstant) const
+bool MultivariatePolynomial::isCoeffStrictPositive(const bool checkConstant) const
+{
+    if (!checkConstant || (constant > 0))
     {
-        if (!checkConstant || (constant > 0))
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff <= 0)
             {
-                if (m.coeff <= 0)
-                {
-                    return false;
-                }
+                return false;
             }
-            return true;
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    bool MultivariatePolynomial::isCoeffPositive(const bool checkConstant) const
+bool MultivariatePolynomial::isCoeffPositive(const bool checkConstant) const
+{
+    if (!checkConstant || (constant >= 0))
     {
-        if (!checkConstant || (constant >= 0))
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff < 0)
             {
-                if (m.coeff < 0)
-                {
-                    return false;
-                }
+                return false;
             }
-            return true;
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    bool MultivariatePolynomial::isCoeffStrictNegative(const bool checkConstant) const
+bool MultivariatePolynomial::isCoeffStrictNegative(const bool checkConstant) const
+{
+    if (!checkConstant || (constant < 0))
     {
-        if (!checkConstant || (constant < 0))
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff >= 0)
             {
-                if (m.coeff >= 0)
-                {
-                    return false;
-                }
+                return false;
             }
-            return true;
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    bool MultivariatePolynomial::isCoeffNegative(const bool checkConstant) const
+bool MultivariatePolynomial::isCoeffNegative(const bool checkConstant) const
+{
+    if (!checkConstant || (constant <= 0))
     {
-        if (!checkConstant || (constant <= 0))
+        for (const auto & m : polynomial)
         {
-            for (const auto & m : polynomial)
+            if (m.coeff > 0)
             {
-                if (m.coeff > 0)
-                {
-                    return false;
-                }
+                return false;
             }
-            return true;
         }
-        return false;
+        return true;
     }
+    return false;
+}
 
-    const std::wstring MultivariatePolynomial::print(const std::map<uint64_t, std::wstring> & vars) const
+const std::wstring MultivariatePolynomial::print(const std::map<uint64_t, std::wstring> & vars) const
+{
+    std::wostringstream wos;
+    wos << constant;
+    std::set<MultivariateMonomial, MultivariateMonomial::Compare> s(polynomial.begin(), polynomial.end());
+    for (const auto & m : s)
     {
-        std::wostringstream wos;
-        wos << constant;
-        std::set<MultivariateMonomial, MultivariateMonomial::Compare> s(polynomial.begin(), polynomial.end());
-        for (const auto & m : s)
-        {
-            wos << L" + " << m.print(vars);
-        }
-        return wos.str();
+        wos << L" + " << m.print(vars);
     }
+    return wos.str();
+}
 
-    std::wostream & operator<<(std::wostream & out, const MultivariatePolynomial & p)
+std::wostream & operator<<(std::wostream & out, const MultivariatePolynomial & p)
+{
+    const std::map<uint64_t, std::wstring> vars;
+    out << p.constant;
+    std::set<MultivariateMonomial, MultivariateMonomial::Compare> s(p.polynomial.begin(), p.polynomial.end());
+    for (const auto & m : s)
     {
-        const std::map<uint64_t, std::wstring> vars;
-        out << p.constant;
-        std::set<MultivariateMonomial, MultivariateMonomial::Compare> s(p.polynomial.begin(), p.polynomial.end());
-        for (const auto & m : s)
-        {
-            out << L" + " << m.print(vars);
-        }
-        return out;
+        out << L" + " << m.print(vars);
     }
+    return out;
+}
 
-    bool MultivariatePolynomial::isDiffConstant(const MultivariatePolynomial & R) const
-    {
-        return polynomial == R.polynomial;
-    }
+bool MultivariatePolynomial::isDiffConstant(const MultivariatePolynomial & R) const
+{
+    return polynomial == R.polynomial;
+}
+
+bool MultivariatePolynomial::isConstant() const
+{
+    return polynomial.empty();
+}
+
+bool MultivariatePolynomial::isConstant(const int64_t val) const
+{
+    return isConstant() && constant == val;
+}
 
-    bool MultivariatePolynomial::isConstant() const
+bool MultivariatePolynomial::getCommonCoeff(int64_t & common) const
+{
+    if (constant != 0)
     {
-        return polynomial.empty();
+        return false;
     }
-
-    bool MultivariatePolynomial::isConstant(const int64_t val) const
+    if (polynomial.empty())
     {
-        return isConstant() && constant == val;
+        common = constant;
+        return true;
     }
 
-    bool MultivariatePolynomial::getCommonCoeff(int64_t & common) const
+    common = polynomial.begin()->coeff;
+    for (Polynomial::const_iterator i = std::next(polynomial.begin()), e = polynomial.end(); i != e; ++i)
     {
-        if (constant != 0)
+        if (i->coeff != common)
         {
             return false;
         }
-        if (polynomial.empty())
-        {
-            common = constant;
-            return true;
-        }
-
-        common = polynomial.begin()->coeff;
-        for (Polynomial::const_iterator i = std::next(polynomial.begin()), e = polynomial.end(); i != e; ++i)
-        {
-            if (i->coeff != common)
-            {
-                return false;
-            }
-        }
-        return true;
     }
+    return true;
+}
 
-    bool MultivariatePolynomial::operator==(const MultivariatePolynomial & R) const
-    {
-        return constant == R.constant && polynomial == R.polynomial;
-    }
+bool MultivariatePolynomial::operator==(const MultivariatePolynomial & R) const
+{
+    return constant == R.constant && polynomial == R.polynomial;
+}
 
-    bool MultivariatePolynomial::operator!=(const MultivariatePolynomial & R) const
-    {
-        return !(*this == R);
-    }
+bool MultivariatePolynomial::operator!=(const MultivariatePolynomial & R) const
+{
+    return !(*this == R);
+}
 
-    bool MultivariatePolynomial::operator==(const int64_t R) const
-    {
-        return polynomial.empty() && constant == R;
-    }
+bool MultivariatePolynomial::operator==(const int64_t R) const
+{
+    return polynomial.empty() && constant == R;
+}
 
-    bool MultivariatePolynomial::operator!=(const int64_t R) const
-    {
-        return !(*this == R);
-    }
+bool MultivariatePolynomial::operator!=(const int64_t R) const
+{
+    return !(*this == R);
+}
 
-    bool operator==(const int64_t L, const MultivariatePolynomial & R)
-    {
-        return R == L;
-    }
+bool operator==(const int64_t L, const MultivariatePolynomial & R)
+{
+    return R == L;
+}
 
-    bool operator!=(const int64_t L, const MultivariatePolynomial & R)
-    {
-        return R != L;
-    }
+bool operator!=(const int64_t L, const MultivariatePolynomial & R)
+{
+    return R != L;
+}
 
-    std::size_t MultivariatePolynomial::hash() const
+std::size_t MultivariatePolynomial::hash() const
+{
+    std::size_t h = std::hash<int64_t>()(constant);
+    for (const auto & m : polynomial)
     {
-        std::size_t h = std::hash<int64_t>()(constant);
-        for (const auto & m : polynomial)
-        {
-            // since the order of the monomials is not always the same
-            // we must use a commutative operation to combine the monomial's hashes
-            h += tools::hash_combine(std::hash<int64_t>()(m.coeff), MultivariateMonomial::Hash()(m));
-        }
-
-        return h;
+        // since the order of the monomials is not always the same
+        // we must use a commutative operation to combine the monomial's hashes
+        h += tools::hash_combine(std::hash<int64_t>()(m.coeff), MultivariateMonomial::Hash()(m));
     }
 
-    bool MultivariatePolynomial::__isValid(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values)
+    return h;
+}
+
+bool MultivariatePolynomial::__isValid(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values)
+{
+    for (const auto & p : values)
     {
-        for (const auto & p : values)
+        if (p.second->isInvalid())
         {
-            if (p.second->isInvalid())
-            {
-                return false;
-            }
+            return false;
         }
-        return true;
     }
+    return true;
+}
 
-    bool MultivariatePolynomial::__isValid(const std::vector<const MultivariatePolynomial *> & values)
+bool MultivariatePolynomial::__isValid(const std::vector<const MultivariatePolynomial *> & values)
+{
+    for (const auto & v : values)
     {
-        for (const auto & v : values)
+        if (v->isInvalid())
         {
-            if (v->isInvalid())
-            {
-                return false;
-            }
+            return false;
         }
-        return true;
-    }
-
-    bool MultivariatePolynomial::__isValid(const std::pair<uint64_t, const MultivariatePolynomial *> & values)
-    {
-       return values.second->isValid();
     }
+    return true;
+}
 
-    bool MultivariatePolynomial::__contains(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-        return values.find(val) != values.end();
-    }
+bool MultivariatePolynomial::__isValid(const std::pair<uint64_t, const MultivariatePolynomial *> & values)
+{
+    return values.second->isValid();
+}
 
-    bool MultivariatePolynomial::__contains(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-        return val < values.size();
-    }
+bool MultivariatePolynomial::__contains(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return values.find(val) != values.end();
+}
 
-    bool MultivariatePolynomial::__contains(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-        return values.first == val;
-    }
+bool MultivariatePolynomial::__contains(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return val < values.size();
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__get(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-        const auto i = values.find(val);
-        if (i != values.end())
-        {
-            return i->second;
-        }
-        return nullptr;
-    }
+bool MultivariatePolynomial::__contains(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return values.first == val;
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+const MultivariatePolynomial * MultivariatePolynomial::__get(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    const auto i = values.find(val);
+    if (i != values.end())
     {
-       return values.find(val)->second;
+        return i->second;
     }
+    return nullptr;
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__get(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-       if (val < values.size())
-       {
-           return values[val];
-       }
-       return nullptr;
-    }
+const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::unordered_map<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return values.find(val)->second;
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
+const MultivariatePolynomial * MultivariatePolynomial::__get(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    if (val < values.size())
     {
         return values[val];
     }
+    return nullptr;
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__get(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
-    {
-       if (values.first == val)
-       {
-           return values.second;
-       }
-        return nullptr;
-    }
+const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::vector<const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return values[val];
+}
 
-    const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+const MultivariatePolynomial * MultivariatePolynomial::__get(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    if (values.first == val)
     {
-       return values.second;
+        return values.second;
     }
+    return nullptr;
+}
+
+const MultivariatePolynomial * MultivariatePolynomial::__getSafe(const std::pair<uint64_t, const MultivariatePolynomial *> & values, const uint64_t val)
+{
+    return values.second;
+}
 
 } // namespace analysis