From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 18 Aug 2009 19:22:35 +0000 (+0000)
Subject: added an option for pure binary printing
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=bd7475c54df17b3f1525e4b635294be78a001036;p=francis%2Fstp.git

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 ad688f1..12bd650 100644
--- 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 2249651..3fe3b3b 100644
--- 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 b94e302..bfa8932 100644
--- 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 890a0ee..6b69cf7 100644
--- 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;