From bb0190a3d272e8d3207cfc358f79c647ed67acaf Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 22 Sep 2020 16:15:54 -0700
Subject: [PATCH] FP: Use Assert instead of PRECONDITION macro in converter.
 (#5119)

The FP converter (= word blaster) uses a PRECONDITION macro that is
defined in symFPU (if included) and calls traits::precondition. This is
a problem for two reasons. First, traits::precondition calls
AlwaysAssert, and PRECONDITION is called for every word-blasted node, so
this can be expensive. Second, in case of an assertion failure, we get
very generic failure messages, that don't allow to distinguish between
failures and are absolutely non-descriptive:

Check failure

b
This fixes both issues.

@martin-cs
---
 src/theory/fp/fp_converter.cpp | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index cb5ade6d9..3ddf9f595 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -141,7 +141,6 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
 #endif
 
 #ifndef CVC4_USE_SYMFPU
-#define PRECONDITION(X) Assert((X))
 #define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
 #endif
 
@@ -155,6 +154,7 @@ symbolicRoundingMode traits::RNA(void) { return symbolicRoundingMode(0x02); };
 symbolicRoundingMode traits::RTP(void) { return symbolicRoundingMode(0x04); };
 symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
 symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
+
 void traits::precondition(const bool b)
 {
   AlwaysAssert(b);
@@ -186,18 +186,19 @@ bool symbolicProposition::checkNodeType(const TNode node)
 
 symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }  // Only used within this header so could be friend'd
 symbolicProposition::symbolicProposition(bool v)
     : nodeWrapper(
           NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
+
 symbolicProposition::symbolicProposition(const symbolicProposition &old)
     : nodeWrapper(old)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 
 symbolicProposition symbolicProposition::operator!(void)const
@@ -245,7 +246,7 @@ bool symbolicRoundingMode::checkNodeType(const TNode n)
 
 symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 
 #ifdef CVC4_USE_SYMFPU
@@ -253,8 +254,8 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
     : nodeWrapper(NodeManager::currentNM()->mkConst(
           BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
 {
-  PRECONDITION((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
-  PRECONDITION(checkNodeType(*this));
+  Assert((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
+  Assert(checkNodeType(*this));
 }
 #else
 symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
@@ -268,7 +269,7 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
 symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
     : nodeWrapper(old)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 
 symbolicProposition symbolicRoundingMode::valid(void) const
@@ -333,7 +334,7 @@ Node symbolicBitVector<isSigned>::toProposition(Node node) const
 template <bool isSigned>
 symbolicBitVector<isSigned>::symbolicBitVector(const Node n) : nodeWrapper(n)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 
 template <bool isSigned>
@@ -346,7 +347,7 @@ template <bool isSigned>
 symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v)
     : nodeWrapper(NodeManager::currentNM()->mkConst(BitVector(w, v)))
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 template <bool isSigned>
 symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p)
@@ -358,13 +359,13 @@ symbolicBitVector<isSigned>::symbolicBitVector(
     const symbolicBitVector<isSigned> &old)
     : nodeWrapper(old)
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 template <bool isSigned>
 symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
     : nodeWrapper(NodeManager::currentNM()->mkConst(old))
 {
-  PRECONDITION(checkNodeType(*this));
+  Assert(checkNodeType(*this));
 }
 
 template <bool isSigned>
@@ -670,7 +671,7 @@ template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
     bwt reduction) const
 {
-  PRECONDITION(this->getWidth() > reduction);
+  Assert(this->getWidth() > reduction);
 
   NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
@@ -704,7 +705,7 @@ template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
     const symbolicBitVector<isSigned> &op) const
 {
-  PRECONDITION(this->getWidth() <= op.getWidth());
+  Assert(this->getWidth() <= op.getWidth());
   return this->extend(op.getWidth() - this->getWidth());
 }
 
@@ -721,7 +722,7 @@ template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
     bwt upper, bwt lower) const
 {
-  PRECONDITION(upper >= lower);
+  Assert(upper >= lower);
 
   NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
@@ -734,7 +735,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
 floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type)
     : FloatingPointSize(type.getConst<FloatingPointSize>())
 {
-  PRECONDITION(type.isFloatingPoint());
+  Assert(type.isFloatingPoint());
 }
 floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig)
     : FloatingPointSize(exp, sig)
-- 
2.30.2