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.

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 0422ae06f912e1630629d12c1109c4b989cdbcc0..c4541f4e423b92eea559b94d3fea8254ca519eda 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -232,3 +232,11 @@ header = "options/bv_options.h"
   type       = "bool"
   default    = "true"
   help       = "algebraic inferences for extended functions"
+
+[[option]]
+  name       = "bvPrintConstsInBinary"
+  category   = "regular"
+  long       = "bv-print-consts-in-binary"
+  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 259f23afc7479aa3481630569ed1361266d020f1..d6ed07c12d42782aef39b86f7c076e395f9f73fc 100644 (file)
--- 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 << ")";
       }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 15dbf0df8d31f24a99caa31b9d86dc0b472bd0b3..c8b052265f48561b22a2b35ce0c31655294e8f21 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -570,6 +570,8 @@ set(regress_0_tests
   regress0/preprocess/preprocess_14.cvc
   regress0/preprocess/preprocess_15.cvc
   regress0/print_lambda.cvc
+  regress0/printer/bv_consts_bin.smt2
+  regress0/printer/bv_consts_dec.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
@@ -846,10 +848,10 @@ set(regress_0_tests
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
-  regress0/sygus/array-grammar-select.sy
-  regress0/sygus/array-grammar-store.sy
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
+  regress0/sygus/array-grammar-select.sy
+  regress0/sygus/array-grammar-store.sy
   regress0/sygus/c100.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/check-generic-red.sy

diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2
new file mode 100644 (file)
index 0000000..e5c3c28
--- /dev/null
+++ b/test/regress/regress0/printer/bv_consts_bin.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --bv-print-consts-in-binary
+; EXPECT: sat
+; EXPECT: ((x #b0001))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 4))
+(assert (= x #b0001))
+(check-sat)
+(get-value (x))

diff --git a/test/regress/regress0/printer/bv_consts_dec.smt2 b/test/regress/regress0/printer/bv_consts_dec.smt2
new file mode 100644 (file)
index 0000000..98d95e8
--- /dev/null
+++ b/test/regress/regress0/printer/bv_consts_dec.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --no-bv-print-consts-in-binary
+; EXPECT: sat
+; EXPECT: ((x (_ bv1 4)))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 4))
+(assert (= x #b0001))
+(check-sat)
+(get-value (x))