added an option for pure binary printing

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@137 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index ad688f1cda5297800c95e19ba4e6034f8943179f..12bd650c557b2994483583271e0f8db642ab7d8c 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -39,6 +39,7 @@ bool check_counterexample = false;
 //on the counterexample returned by SAT solver
 bool construct_counterexample = true;
 bool print_counterexample = false;
+bool print_binary = false;
 //if this option is true then print the way dawson wants using a
 //different printer. do not use this printer.
 bool print_arrayval_declaredorder = false;
@@ -497,7 +498,7 @@ void ASTNode::PL_Print1(ostream& os, int indentation, bool letize) const
                case BITVECTOR:
                        os << "BITVECTOR(";
                        unsigned char * str;
-                       str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
+                       str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());                  
                        os << str << ")";
                        CONSTANTBV::BitVector_Dispose(str);
                        break;

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 2249651e4abda5c895366f5fdd72abfca4c47f75..3fe3b3bf18a470bcee02cd5e2edaeba12e34522c 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -743,7 +743,18 @@ private:
                unsigned char *res;
                const char *prefix;
 
-               if (_value_width % 4 == 0)
+               if(print_binary) {
+                 res = CONSTANTBV::BitVector_to_Bin(_bvconst);
+                 if (c_friendly)
+                       {
+                               prefix = "0b";
+                       }
+                       else
+                       {
+                               prefix = "0bin";
+                       }
+               }
+               else if (_value_width % 4 == 0)
                {
                        res = CONSTANTBV::BitVector_to_Hex(_bvconst);
                        if (c_friendly)

diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h
index b94e302ea208d1727a77aade61bc99d32846c938..bfa89327acb435f2cbd1befb16a3ff1c1e8dfd15 100644 (file)
--- a/src/AST/ASTUtil.h
+++ b/src/AST/ASTUtil.h
@@ -56,6 +56,7 @@ namespace BEEV {
   //on the counterexample returned by SAT solver
   extern bool construct_counterexample;
   extern bool print_counterexample;
+  extern bool print_binary;
   //if this option is true then print the way dawson wants using a
   //different printer. do not use this printer.
   extern bool print_arrayval_declaredorder;

diff --git a/src/parser/main.cpp b/src/parser/main.cpp
index 890a0eebd3b19b8cfe8345971ede737c404faacf..6b69cf7f18403c773dd08eb86ead05f2cc0c21db 100644 (file)
--- a/src/parser/main.cpp
+++ b/src/parser/main.cpp
@@ -86,6 +86,8 @@ int main(int argc, char ** argv) {
   helpstring +=  "-c  : construct counterexample\n";
   helpstring +=  "-d  : check counterexample\n";
   helpstring +=  "-p  : print counterexample\n";
+  helpstring +=  "-y  : print counterexample in binary\n";
+  helpstring +=  "-b  : STP input read back\n";
   helpstring +=  "-x  : flatten nested XORs\n";
   helpstring +=  "-h  : help\n";
   helpstring +=  "-m  : use the SMTLIB parser\n";
@@ -134,6 +136,9 @@ int main(int argc, char ** argv) {
       case 'p':
        BEEV::print_counterexample = true;
        break;
+      case 'y':
+       BEEV::print_binary = true;
+       break;
       case 'q':
        BEEV::print_arrayval_declaredorder = true;
        break;