Printing FP values as binary or indexed BVs according to option (#4554)

diff --git a/NEWS b/NEWS
index 0a8ad8eaa288cf39053c3a8daf2c084c5e96b295..92cd3ee80bf4a6aa24fd1788cc8805c5f3409623 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,13 @@ Changes:
   `Result::Entailment` along with corresponding changes to the enum values.
 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
   instead of `edu.nyu.acsys.CVC4`.
+* Printing of BV constants: previously CVC4 would print BV constant
+  values as indexed symbols by default and in binary notation with the
+  option --bv-print-consts-in-binary. To be SMT-LIB compliant the
+  default behavior is now to print BV constant values in binary
+  notation and as indexed symbols with the new option
+  --bv-print-consts-as-indexed-symbols. The option
+  --bv-print-consts-in-binary has been removed.
 
 Changes since 1.6
 =================

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 5c8cd8f58f674d281b5f06aaab6c65f8a1279795..a72c7d92a6d9eb64311380f4f824b097bc1c26c2 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -286,9 +286,9 @@ header = "options/bv_options.h"
   help       = "algebraic inferences for extended functions"
 
 [[option]]
-  name       = "bvPrintConstsInBinary"
+  name       = "bvPrintConstsAsIndexedSymbols"
   category   = "regular"
-  long       = "bv-print-consts-in-binary"
+  long       = "bv-print-consts-as-indexed-symbols"
   type       = "bool"
   default    = "false"
   help       = "print bit-vector constants in binary (e.g. #b0001) instead of decimal (e.g. (_ bv1 4)), applies to SMT-LIB 2.x"

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0c0c4c3a825aaa48aee41a91e182bb2b19f5b34d..6670fa065418b721217430d159ecbf6646097037 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -146,31 +146,25 @@ void Smt2Printer::toStream(std::ostream& out,
           << n.getConst<FloatingPointSize>().significand()
           << ")";
       break;
-    case kind::CONST_BITVECTOR: {
+    case kind::CONST_BITVECTOR:
+    {
       const BitVector& bv = n.getConst<BitVector>();
-      const Integer& x = bv.getValue();
-      unsigned width = bv.getSize();
-      if (d_variant == sygus_variant || options::bvPrintConstsInBinary())
+      if (options::bvPrintConstsAsIndexedSymbols())
       {
-        out << "#b" << bv.toString();
+        out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
       }
       else
       {
-        out << "(_ ";
-        out << "bv" << x << " " << width;
-        out << ")";
+        out << "#b" << bv.toString();
       }
-
-      // //out << "#b";
-
-      // while(n-- > 0) {
-      //   out << (x.testBit(n) ? '1' : '0');
-      // }
       break;
     }
     case kind::CONST_FLOATINGPOINT:
-      out << n.getConst<FloatingPoint>();
+    {
+      out << n.getConst<FloatingPoint>().toString(
+          options::bvPrintConstsAsIndexedSymbols());
       break;
+    }
     case kind::CONST_ROUNDINGMODE:
       switch (n.getConst<RoundingMode>()) {
       case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
@@ -292,26 +286,22 @@ void Smt2Printer::toStream(std::ostream& out,
       out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      // out << "to_fp_bv "
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
           << n.getConst<FloatingPointToFPIEEEBitVector>().t.significand()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      // out << "to_fp_fp "
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
           << n.getConst<FloatingPointToFPFloatingPoint>().t.significand()
           << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_REAL_OP:
-      // out << "to_fp_real "
       out << "(_ to_fp " << n.getConst<FloatingPointToFPReal>().t.exponent()
           << ' ' << n.getConst<FloatingPointToFPReal>().t.significand() << ")";
       break;
     case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      // out << "to_fp_signed "
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
           << n.getConst<FloatingPointToFPSignedBitVector>().t.significand()

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index f5545f73c7a9e622b1c8bf77f37ba6e73c7ec499..2c2816515e3b42abdad0a35c70625a9835d285c9 100644 (file)
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -959,6 +959,41 @@ static FloatingPointLiteral constructorHelperBitVector(
     return bv;
   }
 
-
+std::string FloatingPoint::toString(bool printAsIndexed) const
+{
+  std::string str;
+  // retrive BV value
+  BitVector bv(pack());
+  unsigned largestSignificandBit =
+      t.significand() - 2;  // -1 for -inclusive, -1 for hidden
+  unsigned largestExponentBit =
+      (t.exponent() - 1) + (largestSignificandBit + 1);
+  BitVector v[3];
+  v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
+  v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
+  v[2] = bv.extract(largestSignificandBit, 0);
+  str.append("(fp ");
+  for (unsigned i = 0; i < 3; ++i)
+  {
+    if (printAsIndexed)
+    {
+      str.append("(_ bv");
+      str.append(v[i].getValue().toString());
+      str.append(" ");
+      str.append(std::to_string(v[i].getSize()));
+      str.append(")");
+    }
+    else
+    {
+      str.append("#b");
+      str.append(v[i].toString());
+    }
+    if (i < 2)
+    {
+      str.append(" ");
+    }
+  }
+  return str;
+}
 
 }/* CVC4 namespace */

diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index bac0fbd59e858e773ce4504e7d8f911fbc1eb5ee..11aa660f50401dd4c7de4b00b2979d5d182130bb 100644 (file)
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -333,6 +333,13 @@ namespace CVC4 {
       return this->fpl;
     }
 
+    /* Return string representation.
+     *
+     * If printAsIndexed is true then it prints
+     * the bit-vector components of the FP value as indexed symbols, otherwise
+     * in binary notation. */
+    std::string toString(bool printAsIndexed = false) const;
+
     // Gives the corresponding IEEE-754 transfer format
     BitVector pack (void) const;
 
@@ -526,17 +533,10 @@ namespace CVC4 {
   */
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) {
-    BitVector bv(fp.pack());
-
-    unsigned largestSignificandBit = fp.t.significand() - 2; // -1 for -inclusive, -1 for hidden
-    unsigned largestExponentBit = (fp.t.exponent() - 1) + (largestSignificandBit + 1);
-
-    return os
-      << "(fp #b" << bv.extract(largestExponentBit + 1, largestExponentBit + 1)
-      << " #b" << bv.extract(largestExponentBit, largestSignificandBit + 1)
-      << " #b" << bv.extract(largestSignificandBit, 0)
-      << ")";
+  inline std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
+  {
+    // print in binary notation
+    return os << fp.toString();
   }
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;

diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2
index e5c3c28246629d7883cc7688ddf76ce1b408b3b2..f910c2c96334f47a7d4413ecc6bef9c20aa42e95 100644 (file)
--- a/test/regress/regress0/printer/bv_consts_bin.smt2
+++ b/test/regress/regress0/printer/bv_consts_bin.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-print-consts-in-binary
+; COMMAND-LINE:
 ; EXPECT: sat
 ; EXPECT: ((x #b0001))
 (set-option :produce-models true)

diff --git a/test/regress/regress0/printer/bv_consts_dec.smt2 b/test/regress/regress0/printer/bv_consts_dec.smt2
index 98d95e8224b29d9f052f204b1eabc9bba35cf2e3..38337e8cf94a4ceacd634faf4039668f30ac5ea7 100644 (file)
--- a/test/regress/regress0/printer/bv_consts_dec.smt2
+++ b/test/regress/regress0/printer/bv_consts_dec.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-bv-print-consts-in-binary
+; COMMAND-LINE: --bv-print-consts-as-indexed-symbols
 ; EXPECT: sat
 ; EXPECT: ((x (_ bv1 4)))
 (set-option :produce-models true)

diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2
index 46652bc248a65e3e43bcd26e9ea69d68ef8bbb02..41d1ffd84371df54ec1bc12c5518f01a4c6babf9 100644 (file)
--- a/test/regress/regress0/printer/empty_symbol_name.smt2
+++ b/test/regress/regress0/printer/empty_symbol_name.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; EXPECT: ((|| (_ bv1 4)))
+; EXPECT: ((|| #b0001))
 (set-option :produce-models true)
 (set-logic QF_BV)
 (declare-const || (_ BitVec 4))

diff --git a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 b/test/regress/regress0/printer/symbol_starting_w_digit.smt2
index 6a688a16f89df1ddd608e81a700ab3230c002a56..ea13a65c2f1d2f05f730aac644991b3fbe22b612 100644 (file)
--- a/test/regress/regress0/printer/symbol_starting_w_digit.smt2
+++ b/test/regress/regress0/printer/symbol_starting_w_digit.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
-; EXPECT: ((|0_0| (_ bv1 4)))
-; EXPECT: ((x (_ bv3 4)))
+; EXPECT: ((|0_0| #b0001))
+; EXPECT: ((x #b0011))
 (set-option :produce-models true)
 (set-logic QF_BV)
 (declare-const |0_0| (_ BitVec 4))