Remove thom groebner

src/carl/formula/model/ran/RealAlgebraicNumber.h

@@ -4,7 +4,6 @@
  * @file
  * Represent a real algebraic number (RAN) in one of several ways:
  * - Implicitly by a univariate polynomial and an interval.
- * - Implicitly by a polynomial and a sequence of signs (called Thom encoding).
  * - Explicitly by a rational number.
  * Rationale:
  * - A real number cannot always be adequately represented in finite memory, since
@@ -19,10 +18,6 @@
  *   to do relatively fast arithmetic with this representation without rounding errors.
  * - When the algebraic real is only finitely long prefer the rational number
  *   representation because it's faster.
- * - The idea of the Thom-Encoding is as follows: Take a square-free univariate polynomial p
- *   with degree n that has the algebraic real as its root, compute the first n-1 derivates of p,
- *   plug in this algebraic real into each derivate and only keep the sign.
- *   Then polynomial p with this sequence of signs uniquely represents this algebraic real.
  */
 
 #include <iostream>
@@ -36,7 +31,6 @@
 
 #include "RealAlgebraicNumberSettings.h"
 
-#include "../../../thom/ThomEncoding.h"
 #include "RealAlgebraicNumber_Interval.h"
 
 namespace carl {
@@ -62,8 +56,6 @@ class RealAlgebraicNumber {
 	bool mIsRoot = true;
   // Interval representation
 	mutable std::shared_ptr<IntervalContent> mIR;
-  // ThomEncoding
-	std::shared_ptr<ThomEncoding<Number>> mTE;
 
 	void checkForSimplification() const {
 	  //make numeric if possible
@@ -123,10 +115,7 @@ class RealAlgebraicNumber {
 		}
 	}
 
-	explicit RealAlgebraicNumber(const ThomEncoding<Number>& te, bool isRoot = true):
-		mIsRoot(isRoot),
-		mTE(std::make_shared<ThomEncoding<Number>>(te))
-	{}
+
 
 	RealAlgebraicNumber(const RealAlgebraicNumber& ran) = default;
 	RealAlgebraicNumber(RealAlgebraicNumber&& ran) = default;
@@ -160,7 +149,6 @@ class RealAlgebraicNumber {
 	bool isZero() const {
 		if (isNumeric()) return carl::isZero(mValue);
 		else if (isInterval()) return mIR->interval.isZero();
-		else if (isThom()) return mTE->isZero();
 		else return false;
 	}
 
@@ -169,7 +157,7 @@ class RealAlgebraicNumber {
 	 */
 	bool isNumeric() const {
 		checkForSimplification();
-		return !mIR && !mTE;
+		return !mIR;
 	}
 	/**
 	 * Check if the underlying representation is an implict number
@@ -180,17 +168,6 @@ class RealAlgebraicNumber {
 		return bool(mIR);
 	}
 
-	/**
-	 * Check if the underlying representation is an implicit number
-	 * that uses the Thom encoding.
-	 */
-	bool isThom() const noexcept {
-		return bool(mTE);
-	}
-	const ThomEncoding<Number>& getThomEncoding() const {
-		assert(isThom());
-		return *mTE;
-	}
 
 
 	bool isIntegral() const {
@@ -219,7 +196,7 @@ class RealAlgebraicNumber {
 	}
 
 	std::size_t getRefinementCount() const {
-		assert(!isNumeric() && !isThom());
+		assert(!isNumeric());
 		assert(isInterval());
 		return mIR->refinementCount;
 	}
@@ -257,9 +234,7 @@ class RealAlgebraicNumber {
 		else if (isInterval()) {
 			return mIR->interval.sgn();
 		}
-		else if(isThom()) {
-			return mTE->sgnReprNum();
-		}
+
 		else return Sign::ZERO;
 	}
 
@@ -268,16 +243,14 @@ class RealAlgebraicNumber {
 			return carl::sgn(p.evaluate(mValue));
 		} else if (isInterval()){
 			return mIR->sgn(p);
-		} else {
-			assert(isThom());
-			return mTE->signOnPolynomial(MultivariatePolynomial<Number>(p));
 		}
+		assert(false);
+
 	}
 
 	bool isRootOf(const UnivariatePolynomial<Number>& p) const {
 		if (isNumeric()) return p.countRealRoots(value()) == 1;
 		else if (isInterval()) return p.countRealRoots(mIR->interval) == 1;
-		else if (isThom()) return this->sgn(p) == Sign::ZERO;
 		else return false;
 	}
 
@@ -297,16 +270,6 @@ class RealAlgebraicNumber {
 				if (isNumeric()) return i.contains(mValue);
 			}
 			return i.contains(mIR->interval);
-		} else if (isThom()) {
-			if(i.lowerBoundType() != BoundType::INFTY) {
-				if(i.lowerBoundType() == BoundType::STRICT && *mTE <= i.lower()) return false;
-				if(i.lowerBoundType() == BoundType::WEAK && *mTE < i.lower()) return false;
-			}
-			if(i.upperBoundType() != BoundType::INFTY) {
-				if(i.upperBoundType() == BoundType::STRICT && *mTE >= i.upper()) return false;
-				if(i.upperBoundType() == BoundType::WEAK && *mTE > i.upper()) return false;
-			}
-			return true;
 		}
 		else return false;
 	}
@@ -368,7 +331,6 @@ template<typename Num>
 std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber<Num>& ran) {
 	if (ran.isNumeric()) return os << "(NR " << ran.value() << (ran.isRoot() ? " R" : "") << ")";
 	else if (ran.isInterval()) return os << "(IR " << ran.getInterval() << ", " << ran.getIRPolynomial() << (ran.isRoot() ? " R" : "") << ")";
-	else if (ran.isThom()) return os << "(TE " << ran.getThomEncoding() << (ran.isRoot() ? " R" : "") << ")";
 	else return os << "(RAN)"; // should never be the case
 }
 

src/carl/formula/model/ran/RealAlgebraicNumber.tpp

@@ -9,18 +9,7 @@ namespace carl {
 		CARL_LOG_FUNC("carl.ran", *this << ", " << n);
 		if (this == &n) return true;
 
-		if(this->isThom() || n.isThom()) {
-			assert(!this->isInterval() && !n.isInterval());
-			if(this->isThom() && n.isThom()) {
-				return *(this->mTE) == *(n.mTE);
-			} else if(this->isThom() && n.isNumeric()) {
-				return *(this->mTE) == n.value();
-			} else {
-				assert(this->isNumeric() && n.isThom());
-				return this->value() == *(n.mTE);
-			}
-		}
-		assert(!isThom() && !n.isThom());
+
 
 		if (isNumeric()) {
 			if (n.isNumeric()) {
@@ -74,11 +63,6 @@ namespace carl {
 				} else {
 					return value() <= n.lower();
 				}
-			} else {
-				assert(n.isThom());
-				bool res = this->value() < *(n.mTE);
-				CARL_LOG_TRACE("carl.ran", "result is " << res);
-				return res;
 			}
 		} else if(isInterval()) {
 			if (n.isNumeric()) {
@@ -90,17 +74,8 @@ namespace carl {
 				}
 			}
 		} else {
-			assert(isThom());
-			if(n.isNumeric()) {
-				bool res = *mTE < n.value();
-				CARL_LOG_TRACE("carl.ran", "result is " << res);
-				return res;
-			} else {
-				assert(n.isThom());
-				bool res =  *mTE < *(n.mTE);
-				CARL_LOG_TRACE("carl.ran", "result is " << res);
-				return res;
-			}
+			assert(false);
+
 		}
 
 		if (mIR == n.mIR) return false;

src/carl/formula/model/ran/RealAlgebraicNumberEvaluation.h

@@ -19,7 +19,6 @@
 #include "../../../core/MultivariatePolynomial.h"
 #include "../../../core/polynomialfunctions/Resultant.h"
 #include "../../../interval/IntervalEvaluation.h"
-#include "../../../thom/ThomEvaluation.h"
 #include "../../../util/SFINAE.h"
 
 namespace carl {

src/carl/formula/model/ran/RealAlgebraicNumberOperations.h

@@ -54,62 +54,45 @@ namespace carl {
 		} else if (n.isInterval()) {
 			CARL_LOG_TRACE("carl.ran", "Selecting from (-oo, " << n << ") -> " << (carl::ceil(n.lower()) - 1));
 			return RealAlgebraicNumber<Number>(carl::ceil(n.lower()) - 1, false);
-		} else {
-			assert(n.isThom());
-			RealAlgebraicNumber<Number> res(*(n.mTE) + Number(-1), false);
-			CARL_LOG_TRACE("carl.ran", "selecting sample " << res);
-			return res;
 		}
 	}
 	template<typename Number>
 	RealAlgebraicNumber<Number> sampleBetween(const RealAlgebraicNumber<Number>& lower, const RealAlgebraicNumber<Number>& upper, RANSampleHeuristic heuristic = RANSampleHeuristic::Default) {
 		CARL_LOG_FUNC("carl.ran", lower << ", " << upper);
-		if(lower.isThom() || upper.isThom()) {
-			RealAlgebraicNumber<Number> res;
-			if(lower.isThom() && upper.isThom()) {
-				res =  RealAlgebraicNumber<Number>(ThomEncoding<Number>::intermediatePoint(*(lower.mTE), *(upper.mTE)), false);
-			} else if(lower.isNumeric() && upper.isThom()) {
-				res = RealAlgebraicNumber<Number>(ThomEncoding<Number>::intermediatePoint(lower.value(), *(upper.mTE)), false);
-			} else {
-				assert(lower.isThom() && upper.isNumeric());
-				res = RealAlgebraicNumber<Number>(ThomEncoding<Number>::intermediatePoint(*(lower.mTE), upper.value()), false);
-			}
-			CARL_LOG_TRACE("carl.ran", "selecting sample " << res);
-			return res;
-		} else {
-			Interval<Number> i;
-			if (lower.isNumeric()) i.set(lower.value(), lower.value());
-			else i.set(lower.upper(), lower.upper());
-			if (upper.isNumeric()) i.setUpper(upper.value());
-			else i.setUpper(upper.lower());
-			while (i.isEmpty()) {
-				if (!lower.isNumeric()) {
-					lower.refine();
-					if (lower.isNumeric()) i.setLower(lower.value());
-					else i.setLower(lower.upper());
-				}
-				if (!upper.isNumeric()) {
-					upper.refine();
-					if (upper.isNumeric()) i.setUpper(upper.value());
-					else i.setUpper(upper.lower());
-				}
+
+		Interval<Number> i;
+		if (lower.isNumeric()) i.set(lower.value(), lower.value());
+		else i.set(lower.upper(), lower.upper());
+		if (upper.isNumeric()) i.setUpper(upper.value());
+		else i.setUpper(upper.lower());
+		while (i.isEmpty()) {
+			if (!lower.isNumeric()) {
+				lower.refine();
+				if (lower.isNumeric()) i.setLower(lower.value());
+				else i.setLower(lower.upper());
 			}
-			CARL_LOG_TRACE("carl.ran", "Selecting from (" << lower << ", " << upper << ") -> " << i.sample(false) << " (from " << i << ")");
-			switch (heuristic) {
-				case RANSampleHeuristic::Center:
-					return RealAlgebraicNumber<Number>(i.center(), false);
-				case RANSampleHeuristic::CenterInt:
-					return RealAlgebraicNumber<Number>(i.sample(false), false);
-				case RANSampleHeuristic::LeftInt:
-					return RealAlgebraicNumber<Number>(i.sampleLeft(), false);
-				case RANSampleHeuristic::RightInt:
-					return RealAlgebraicNumber<Number>(i.sampleRight(), false);
-				case RANSampleHeuristic::ZeroInt:
-					return RealAlgebraicNumber<Number>(i.sampleZero(), false);
-				case RANSampleHeuristic::InftyInt:
-					return RealAlgebraicNumber<Number>(i.sampleInfty(), false);
+			if (!upper.isNumeric()) {
+				upper.refine();
+				if (upper.isNumeric()) i.setUpper(upper.value());
+				else i.setUpper(upper.lower());
 			}
 		}
+		CARL_LOG_TRACE("carl.ran", "Selecting from (" << lower << ", " << upper << ") -> " << i.sample(false) << " (from " << i << ")");
+		switch (heuristic) {
+			case RANSampleHeuristic::Center:
+				return RealAlgebraicNumber<Number>(i.center(), false);
+			case RANSampleHeuristic::CenterInt:
+				return RealAlgebraicNumber<Number>(i.sample(false), false);
+			case RANSampleHeuristic::LeftInt:
+				return RealAlgebraicNumber<Number>(i.sampleLeft(), false);
+			case RANSampleHeuristic::RightInt:
+				return RealAlgebraicNumber<Number>(i.sampleRight(), false);
+			case RANSampleHeuristic::ZeroInt:
+				return RealAlgebraicNumber<Number>(i.sampleZero(), false);
+			case RANSampleHeuristic::InftyInt:
+				return RealAlgebraicNumber<Number>(i.sampleInfty(), false);
+		}
+
 	}
 	template<typename Number>
 	RealAlgebraicNumber<Number> sampleAbove(const RealAlgebraicNumber<Number>& n) {
@@ -120,12 +103,9 @@ namespace carl {
 		} else if (n.isInterval()) {
 			CARL_LOG_TRACE("carl.ran", "Selecting from (" << n << ", oo) -> " << (carl::floor(n.upper()) + 1));
 			return RealAlgebraicNumber<Number>(carl::floor(n.upper()) + 1, false);
-		} else {
-			assert(n.isThom());
-			RealAlgebraicNumber<Number> res(*(n.mTE) + Number(1), false);
-			CARL_LOG_TRACE("carl.ran", "selecting sample " << res);
-			return res;
 		}
+			assert(false);
+
 	}
 
 }