summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS7
-rw-r--r--src/options/bv_options.toml4
-rw-r--r--src/printer/smt2/smt2_printer.cpp28
-rw-r--r--src/util/floatingpoint.cpp37
-rw-r--r--src/util/floatingpoint.h.in22
-rw-r--r--test/regress/regress0/printer/bv_consts_bin.smt22
-rw-r--r--test/regress/regress0/printer/bv_consts_dec.smt22
-rw-r--r--test/regress/regress0/printer/empty_symbol_name.smt22
-rw-r--r--test/regress/regress0/printer/symbol_starting_w_digit.smt24
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<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 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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback