diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-16 16:38:38 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-16 16:38:38 -0800 |
commit | 78d7485639cdf0769c13606b8ad3f5e9455153f1 (patch) | |
tree | fa32eeda005c7ef774bdf9e7a210d43bc9b33ffa /src/printer/smt2 | |
parent | 60b5ac4c6488014feb4820a98e663cc5fdbad5c1 (diff) |
Add option to print BV constants in binary (#2805)
This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 259f23afc..d6ed07c12 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -22,6 +22,7 @@ #include <vector> #include "expr/node_manager_attributes.h" +#include "options/bv_options.h" #include "options/language.h" #include "options/smt_options.h" #include "printer/dagification_visitor.h" @@ -160,11 +161,14 @@ void Smt2Printer::toStream(std::ostream& out, const BitVector& bv = n.getConst<BitVector>(); const Integer& x = bv.getValue(); unsigned n = bv.getSize(); - if(d_variant == sygus_variant ){ + if (d_variant == sygus_variant || options::bvPrintConstsInBinary()) + { out << "#b" << bv.toString(); - }else{ + } + else + { out << "(_ "; - out << "bv" << x <<" " << n; + out << "bv" << x << " " << n; out << ")"; } |