From 80b0795702e71d54ed7c17ba809eebde628eb516 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 5 Jun 2020 09:54:51 -0300 Subject: [PATCH] Printing FP values as binary or indexed BVs according to option (#4554) --- NEWS | 7 ++++ src/options/bv_options.toml | 4 +- src/printer/smt2/smt2_printer.cpp | 28 +++++--------- src/util/floatingpoint.cpp | 37 ++++++++++++++++++- src/util/floatingpoint.h.in | 22 +++++------ .../regress0/printer/bv_consts_bin.smt2 | 2 +- .../regress0/printer/bv_consts_dec.smt2 | 2 +- .../regress0/printer/empty_symbol_name.smt2 | 2 +- .../printer/symbol_starting_w_digit.smt2 | 4 +- 9 files changed, 70 insertions(+), 38 deletions(-) diff --git a/NEWS b/NEWS index 0a8ad8eaa..92cd3ee80 100644 --- 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 5c8cd8f58..a72c7d92a 100644 --- 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 0c0c4c3a8..6670fa065 100644 --- 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().significand() << ")"; break; - case kind::CONST_BITVECTOR: { + case kind::CONST_BITVECTOR: + { const BitVector& bv = n.getConst(); - 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(); + { + out << n.getConst().toString( + options::bvPrintConstsAsIndexedSymbols()); break; + } case kind::CONST_ROUNDINGMODE: switch (n.getConst()) { case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break; @@ -292,26 +286,22 @@ void Smt2Printer::toStream(std::ostream& out, out << "(_ int2bv " << n.getConst().d_size << ")"; break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: - // out << "to_fp_bv " out << "(_ to_fp " << n.getConst().t.exponent() << ' ' << n.getConst().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: - // out << "to_fp_fp " out << "(_ to_fp " << n.getConst().t.exponent() << ' ' << n.getConst().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_REAL_OP: - // out << "to_fp_real " out << "(_ to_fp " << n.getConst().t.exponent() << ' ' << n.getConst().t.significand() << ")"; break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: - // out << "to_fp_signed " out << "(_ to_fp " << n.getConst().t.exponent() << ' ' << n.getConst().t.significand() diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index f5545f73c..2c2816515 100644 --- 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 bac0fbd59..11aa660f5 100644 --- 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 e5c3c2824..f910c2c96 100644 --- 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 98d95e822..38337e8cf 100644 --- 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 46652bc24..41d1ffd84 100644 --- 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 6a688a16f..ea13a65c2 100644 --- 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)) -- 2.30.2