Nice patch by Dan Liew that adds support for printing queries in the

SMTLIB format (part of his MSc project work).


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 1155 insertions, 0 deletions

diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp
new file mode 100644
index 00000000..7225704e
--- /dev/null
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -0,0 +1,249 @@
+//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <iostream>
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBLetPrinter.h"
+
+using namespace std;
+
+namespace ExprSMTLIBOptions
+{
+	llvm::cl::opt<bool> useLetExpressions("smtlib-use-let-expressions",
+			llvm::cl::desc("Enables generated SMT-LIBv2 files to use (let) expressions (default=on)"),
+			llvm::cl::init(true)
+	);
+}
+
+namespace klee
+{
+	const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
+
+
+	ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() :
+	bindings(), firstEO(), twoOrMoreEO(),
+	disablePrintedAbbreviations(false)
+	{
+	}
+
+	void ExprSMTLIBLetPrinter::generateOutput()
+	{
+		if(p==NULL || query == NULL || o ==NULL)
+		{
+			std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
+			return;
+		}
+
+		generateBindings();
+
+		if(isHumanReadable()) printNotice();
+		printOptions();
+		printSetLogic();
+		printArrayDeclarations();
+		printLetExpression();
+		printAction();
+		printExit();
+	}
+
+	void ExprSMTLIBLetPrinter::scan(const ref<Expr>& e)
+	{
+		if(isa<ConstantExpr>(e))
+			return; //we don't need to scan simple constants
+
+		if(firstEO.insert(e).second)
+		{
+			//We've not seen this expression before
+
+			if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
+			{
+
+				//Attempt to insert array and if array wasn't present before do more things
+				if(usedArrays.insert(re->updates.root).second)
+				{
+
+					//check if the array is constant
+					if( re->updates.root->isConstantArray())
+						haveConstantArray=true;
+
+					//scan the update list
+					scanUpdates(re->updates.head);
+
+				}
+
+			}
+
+			//recurse into the children
+			Expr* ep = e.get();
+			for(unsigned int i=0; i < ep->getNumKids(); i++)
+				scan(ep->getKid(i));
+		}
+		else
+		{
+			/* We must of seen the expression before. Add it to
+			 * the set of twoOrMoreOccurances. We don't need to
+			 * check if the insertion fails.
+			 */
+			twoOrMoreEO.insert(e);
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::generateBindings()
+	{
+		//Assign a number to each binding that will be used
+		unsigned int counter=0;
+		for(set<ref<Expr> >::const_iterator i=twoOrMoreEO.begin();
+				i!= twoOrMoreEO.end(); ++i)
+		{
+			bindings.insert(std::make_pair(*i,counter));
+			++counter;
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
+	{
+		map<const ref<Expr>,unsigned int>::const_iterator i= bindings.find(e);
+
+		if(disablePrintedAbbreviations || i == bindings.end())
+		{
+			/*There is no abbreviation for this expression so print it normally.
+			 * Do this by using the parent method.
+			 */
+			ExprSMTLIBPrinter::printExpression(e,expectedSort);
+		}
+		else
+		{
+			//Use binding name e.g. "?B1"
+
+			/* Handle the corner case where the expectedSort
+			 * doesn't match the sort of the abbreviation. Not really very efficient (calls bindings.find() twice),
+			 * we'll cast and call ourself again but with the correct expectedSort.
+			 */
+			if(getSort(e) != expectedSort)
+			{
+				printCastToSort(e,expectedSort);
+				return;
+			}
+
+			// No casting is needed in this depth of recursion, just print the abbreviation
+			*p << BINDING_PREFIX << i->second;
+		}
+	}
+
+	void ExprSMTLIBLetPrinter::reset()
+	{
+		//Let parent clean up first
+		ExprSMTLIBPrinter::reset();
+
+		firstEO.clear();
+		twoOrMoreEO.clear();
+		bindings.clear();
+	}
+
+	void ExprSMTLIBLetPrinter::printLetExpression()
+	{
+		*p << "(assert"; p->pushIndent(); printSeperator();
+
+		if(bindings.size() !=0 )
+		{
+			//Only print let expression if we have bindings to use.
+			*p << "(let"; p->pushIndent(); printSeperator();
+			*p << "( "; p->pushIndent();
+
+			//Print each binding
+			for(map<const ref<Expr>, unsigned int>::const_iterator i= bindings.begin();
+					i!=bindings.end(); ++i)
+			{
+				printSeperator();
+				*p << "(" << BINDING_PREFIX << i->second << " ";
+				p->pushIndent();
+
+				//Disable abbreviations so none are used here.
+				disablePrintedAbbreviations=true;
+
+				//We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
+				printExpression(i->first,getSort(i->first));
+
+				p->popIndent();
+				printSeperator();
+				*p << ")";
+			}
+
+
+			p->popIndent(); printSeperator();
+			*p << ")";
+			printSeperator();
+
+			//Re-enable printing abbreviations.
+			disablePrintedAbbreviations=false;
+
+		}
+
+		//print out Expressions with abbreviations.
+		unsigned int numberOfItems= query->constraints.size() +1; //+1 for query
+		unsigned int itemsLeft=numberOfItems;
+		vector<ref<Expr> >::const_iterator constraint=query->constraints.begin();
+
+		/* Produce nested (and () () statements. If the constraint set
+		 * is empty then we will only print the "queryAssert".
+		 */
+		for(; itemsLeft !=0; --itemsLeft)
+		{
+			if(itemsLeft >=2)
+			{
+				*p << "(and"; p->pushIndent(); printSeperator();
+				printExpression(*constraint,SORT_BOOL); //We must and together bool expressions
+				printSeperator();
+				++constraint;
+				continue;
+			}
+			else
+			{
+				// must have 1 item left (i.e. the "queryAssert")
+				if(isHumanReadable()) { *p << "; query"; p->breakLineI();}
+				printExpression(queryAssert,SORT_BOOL); //The query must be a bool expression
+
+			}
+		}
+
+		/* Produce closing brackets for nested "and statements".
+		 * Number of "nested ands" = numberOfItems -1
+		 */
+		itemsLeft= numberOfItems -1;
+		for(; itemsLeft!=0; --itemsLeft)
+		{
+			p->popIndent(); printSeperator();
+			*p << ")";
+		}
+
+
+
+		if(bindings.size() !=0)
+		{
+			//end let expression
+			p->popIndent(); printSeperator();
+			*p << ")";  printSeperator();
+		}
+
+		//end assert
+		p->popIndent(); printSeperator();
+		*p << ")";
+		p->breakLineI();
+	}
+
+	ExprSMTLIBPrinter* createSMTLIBPrinter()
+	{
+		if(ExprSMTLIBOptions::useLetExpressions)
+			return new ExprSMTLIBLetPrinter();
+		else
+			return new ExprSMTLIBPrinter();
+	}
+
+
+}
+
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
new file mode 100644
index 00000000..aa75629a
--- /dev/null
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -0,0 +1,906 @@
+//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include <iostream>
+
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBPrinter.h"
+
+using namespace std;
+
+namespace ExprSMTLIBOptions
+{
+	//Command line options
+	llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> argConstantDisplayMode
+	("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated SMT-LIBv2 files (default=dec)"),
+	llvm::cl::values( clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin","Use binary form (e.g. #b00101101)"),
+					  clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex","Use Hexadecimal form (e.g. #x2D)"),
+					  clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec","Use decimal form (e.g. (_ bv45 8) )"),
+					  clEnumValEnd
+					),
+					llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL)
+
+
+	);
+
+	llvm::cl::opt<bool> humanReadableSMTLIB("smtlib-human-readable",
+				llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"),
+				llvm::cl::init(false)
+
+
+	);
+
+}
+
+
+namespace klee
+{
+
+	ExprSMTLIBPrinter::ExprSMTLIBPrinter() :
+		usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV),
+		humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL)
+	{
+		setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
+	}
+
+	ExprSMTLIBPrinter::~ExprSMTLIBPrinter()
+	{
+		if(p!=NULL)
+			delete p;
+	}
+
+	void ExprSMTLIBPrinter::setOutput(std::ostream& output)
+	{
+		o = &output;
+		if(p!=NULL)
+			delete p;
+
+		p = new PrintContext(output);
+	}
+
+	void ExprSMTLIBPrinter::setQuery(const Query& q)
+	{
+		query = &q;
+		reset(); // clear the data structures
+		scanAll();
+		mangleQuery();
+	}
+
+	void ExprSMTLIBPrinter::reset()
+	{
+		usedArrays.clear();
+		haveConstantArray=false;
+
+		/* Clear the PRODUCE_MODELS option if it was automatically set.
+		 * We need to do this because the next query might not need the
+		 * (get-value) SMT-LIBv2 command.
+		 */
+		if(arraysToCallGetValueOn !=NULL)
+			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_DEFAULT);
+
+		arraysToCallGetValueOn=NULL;
+
+
+	}
+
+	bool ExprSMTLIBPrinter::isHumanReadable()
+	{
+		return humanReadable;
+	}
+
+	bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm)
+	{
+		if(cdm > DECIMAL)
+			return false;
+
+		this->cdm = cdm;
+		return true;
+	}
+
+	void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr>& e)
+	{
+		/* Handle simple boolean constants */
+
+		if(e->isTrue())
+		{
+			*p << "true";
+			return;
+		}
+
+		if(e->isFalse())
+		{
+			*p << "false";
+			return;
+		}
+
+		/* Handle bitvector constants */
+
+		std::string value;
+
+		/* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
+		 * from the length of the string (e.g. zero is #b00000000). LLVM
+		 * doesn't know about this so we need to pad the printed output
+		 * with the appropriate number of zeros (zeroPad)
+		 */
+		unsigned int zeroPad=0;
+
+		switch(cdm)
+		{
+			case BINARY:
+				e->toString(value,2);
+				*p << "#b";
+
+				zeroPad = e->getWidth() - value.length();
+
+				for(unsigned int count=0; count < zeroPad; count++)
+					*p << "0";
+
+				*p << value ;
+				break;
+
+			case HEX:
+				e->toString(value,16);
+				*p << "#x";
+
+				zeroPad =  (e->getWidth() / 4) - value.length();
+				for(unsigned int count=0; count < zeroPad; count++)
+					*p << "0";
+
+				*p << value ;
+				break;
+
+			case DECIMAL:
+				e->toString(value,10);
+				*p << "(_ bv" << value<< " " << e->getWidth() << ")";
+				break;
+
+			default:
+				std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant display mode" << std::endl;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
+	{
+		//check if casting might be necessary
+		if(getSort(e) != expectedSort)
+		{
+			printCastToSort(e,expectedSort);
+			return;
+		}
+
+
+		switch(e->getKind())
+		{
+			case Expr::Constant:
+				printConstant(cast<ConstantExpr>(e));
+				return; //base case
+
+			case Expr::NotOptimized:
+				//skip to child
+				printExpression(e->getKid(0),expectedSort);
+				return;
+
+			case Expr::Read:
+				printReadExpr(cast<ReadExpr>(e));
+				return;
+
+			case Expr::Extract:
+				printExtractExpr(cast<ExtractExpr>(e));
+				return;
+
+			case Expr::SExt:
+			case Expr::ZExt:
+				printCastExpr(cast<CastExpr>(e));
+				return;
+
+			case Expr::Ne:
+				printNotEqualExpr(cast<NeExpr>(e));
+				return;
+
+			case Expr::Select:
+				//the if-then-else expression.
+				printSelectExpr(cast<SelectExpr>(e),expectedSort);
+				return;
+
+			case Expr::Eq:
+				/* The "=" operator is special in that it can take any sort but we must
+				 * enforce that both arguments are the same type. We do this a lazy way
+				 * by enforcing the second argument is of the same type as the first.
+				 */
+				printSortArgsExpr(e,getSort(e->getKid(0)));
+
+				return;
+
+			case Expr::And:
+			case Expr::Or:
+			case Expr::Xor:
+			case Expr::Not:
+				/* These operators have a bitvector version and a bool version.
+				 * For these operators only (e.g. wouldn't apply to bvult) if the expected sort the
+				 * expression is T then that implies the arguments are also of type T.
+				 */
+				printLogicalOrBitVectorExpr(e,expectedSort);
+
+				return;
+
+
+			default:
+				/* The remaining operators (Add,Sub...,Ult,Ule,..)
+				 * Expect SORT_BITVECTOR arguments
+				 */
+				printSortArgsExpr(e,SORT_BITVECTOR);
+				return;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr>& e)
+	{
+		*p << "(" << getSMTLIBKeyword(e) << " ";
+		p->pushIndent();
+
+		printSeperator();
+
+		//print array with updates recursively
+		printUpdatesAndArray(e->updates.head,e->updates.root);
+
+		//print index
+		printSeperator();
+		printExpression(e->index,SORT_BITVECTOR);
+
+		p->popIndent();
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr>& e)
+	{
+		unsigned int lowIndex= e->offset;
+		unsigned int highIndex= lowIndex + e->width -1;
+
+		*p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex << ") ";
+
+		p->pushIndent(); //add indent for recursive call
+		printSeperator();
+
+		//recurse
+		printExpression(e->getKid(0),SORT_BITVECTOR);
+
+		p->popIndent(); //pop indent added for the recursive call
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr>& e)
+	{
+		/* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
+		 * instead of specifying of what bit-width we would like to extend to
+		 * we specify how many bits to add to the child expression
+		 *
+		 * e.g
+		 * ((_ sign_extend 64) (_ bv5 32))
+		 *
+		 * gives a (_ BitVec 96) instead of (_ BitVec 64)
+		 *
+		 * So we must work out how many bits we need to add.
+		 *
+		 * (e->width) is the desired number of bits
+		 * (e->src->getWidth()) is the number of bits in the child
+		 */
+		unsigned int numExtraBits= (e->width) - (e->src->getWidth());
+
+		*p << "((_ " << getSMTLIBKeyword(e) << " " <<
+				numExtraBits << ") ";
+
+		p->pushIndent(); //add indent for recursive call
+		printSeperator();
+
+		//recurse
+		printExpression(e->src,SORT_BITVECTOR);
+
+		p->popIndent(); //pop indent added for recursive call
+		printSeperator();
+
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr>& e)
+	{
+		*p << "(not (";
+		p->pushIndent();
+		*p << "=" << " ";
+		p->pushIndent();
+		printSeperator();
+
+		/* The "=" operators allows both sorts. We assume
+		 * that the second argument sort should be forced to be the same sort as the
+		 * first argument
+		 */
+		SMTLIB_SORT s = getSort(e->getKid(0));
+
+		printExpression(e->getKid(0),s);
+		printSeperator();
+		printExpression(e->getKid(1),s);
+		p->popIndent();
+		printSeperator();
+
+		*p << ")";
+		p->popIndent();
+		printSeperator();
+		*p << ")";
+	}
+
+
+	const char* ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr>& e)
+	{
+
+		switch(e->getKind())
+		{
+			case Expr::Read: return "select";
+			case Expr::Select: return "ite";
+			case Expr::Concat: return "concat";
+			case Expr::Extract: return "extract";
+			case Expr::ZExt: return "zero_extend";
+			case Expr::SExt: return "sign_extend";
+
+			case Expr::Add: return "bvadd";
+			case Expr::Sub: return "bvsub";
+			case Expr::Mul: return "bvmul";
+			case Expr::UDiv: return "bvudiv";
+			case Expr::SDiv: return "bvsdiv";
+			case Expr::URem: return "bvurem";
+			case Expr::SRem: return "bvsrem";
+
+
+			/* And, Xor, Not and Or are not handled here because there different versions
+			 * for different sorts. See printLogicalOrBitVectorExpr()
+			 */
+
+
+			case Expr::Shl: return "bvshl";
+			case Expr::LShr: return "bvlshr";
+			case Expr::AShr: return "bvashr";
+
+			case Expr::Eq: return "=";
+
+			//Not Equal does not exist directly in SMTLIBv2
+
+			case Expr::Ult: return "bvult";
+			case Expr::Ule: return "bvule";
+			case Expr::Ugt: return "bvugt";
+			case Expr::Uge: return "bvuge";
+
+			case Expr::Slt: return "bvslt";
+			case Expr::Sle: return "bvsle";
+			case Expr::Sgt: return "bvsgt";
+			case Expr::Sge: return "bvsge";
+
+			default:
+				return "<error>";
+
+		}
+	}
+
+	void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode* un, const Array* root)
+	{
+		if(un!=NULL)
+		{
+			*p << "(store ";
+			p->pushIndent();
+			printSeperator();
+
+			//recurse to get the array or update that this store operations applies to
+			printUpdatesAndArray(un->next,root);
+
+			printSeperator();
+
+			//print index
+			printExpression(un->index,SORT_BITVECTOR);
+			printSeperator();
+
+			//print value that is assigned to this index of the array
+			printExpression(un->value,SORT_BITVECTOR);
+
+			p->popIndent();
+			printSeperator();
+			*p << ")";
+		}
+		else
+		{
+			//The base case of the recursion
+			*p << root->name;
+		}
+
+	}
+
+	void ExprSMTLIBPrinter::scanAll()
+	{
+		//perform scan of all expressions
+		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
+			scan(*i);
+
+		//Scan the query too
+		scan(query->expr);
+	}
+
+	void ExprSMTLIBPrinter::generateOutput()
+	{
+		if(p==NULL || query == NULL || o ==NULL)
+		{
+			std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. Output or query bad!" << std::endl;
+			return;
+		}
+
+		if(humanReadable) printNotice();
+		printOptions();
+		printSetLogic();
+		printArrayDeclarations();
+		printConstraints();
+		printQuery();
+		printAction();
+		printExit();
+	}
+
+	void ExprSMTLIBPrinter::printSetLogic()
+	{
+		*o << "(set-logic ";
+		switch(logicToUse)
+		{
+		case QF_ABV: *o << "QF_ABV"; break;
+		case QF_AUFBV: *o << "QF_AUFBV" ; break;
+		}
+		*o << " )" << std::endl;
+	}
+
+
+	void ExprSMTLIBPrinter::printArrayDeclarations()
+	{
+		//Assume scan() has been called
+		if(humanReadable)
+			*o << "; Array declarations" << endl;
+
+		//declare arrays
+		for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
+		{
+			*o << "(declare-fun " << (*it)->name << " () "
+				 "(Array (_ BitVec " << (*it)->getDomain() << ") "
+				 "(_ BitVec " << (*it)->getRange() << ") ) )" << endl;
+		}
+
+		//Set array values for constant values
+		if(haveConstantArray)
+		{
+			if(humanReadable)
+				*o << "; Constant Array Definitions" << endl;
+
+			const Array* array;
+
+			//loop over found arrays
+			for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
+			{
+				array= *it;
+				int byteIndex=0;
+				if(array->isConstantArray())
+				{
+					/*loop over elements in the array and generate an assert statement
+					  for each one
+					 */
+					for(vector< ref<ConstantExpr> >::const_iterator ce= array->constantValues.begin();
+							ce != array->constantValues.end(); ce++, byteIndex++)
+					{
+						*p << "(assert (";
+						p->pushIndent();
+						*p <<           "= ";
+						p->pushIndent();
+						printSeperator();
+
+						*p << "(select " << array->name << " (_ bv" << byteIndex << " " << array->getDomain() << ") )";
+						printSeperator();
+						printConstant((*ce));
+
+						p->popIndent();
+						printSeperator();
+						*p << ")";
+						p->popIndent();
+						printSeperator();
+						*p << ")";
+
+						p->breakLineI();
+
+					}
+				}
+			}
+		}
+	}
+
+	void ExprSMTLIBPrinter::printConstraints()
+	{
+		if(humanReadable)
+			*o << "; Constraints" << endl;
+
+		//Generate assert statements for each constraint
+		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
+		{
+			*p << "(assert ";
+			p->pushIndent();
+			printSeperator();
+
+			//recurse into Expression
+			printExpression(*i,SORT_BOOL);
+
+			p->popIndent();
+			printSeperator();
+			*p << ")"; p->breakLineI();
+		}
+
+	}
+
+	void ExprSMTLIBPrinter::printAction()
+	{
+		//Ask solver to check for satisfiability
+		*o << "(check-sat)" << endl;
+
+		/* If we has arrays to find the values of then we'll
+		 * ask the solver for the value of each bitvector in each array
+		 */
+		if(arraysToCallGetValueOn!=NULL && !arraysToCallGetValueOn->empty())
+		{
+
+			const Array* theArray=0;
+
+			//loop over the array names
+			for(vector<const Array*>::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++)
+			{
+				theArray=*it;
+				//Loop over the array indices
+				for(unsigned int index=0; index < theArray->size; ++index)
+				{
+					*o << "(get-value ( (select " << (**it).name <<
+					     " (_ bv" << index << " " << theArray->getDomain() << ") ) ) )" << endl;
+				}
+
+			}
+
+
+		}
+	}
+
+	void ExprSMTLIBPrinter::scan(const ref<Expr>& e)
+	{
+		if(e.isNull())
+		{
+			std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" << std::endl;
+			return;
+		}
+
+		if(isa<ConstantExpr>(e))
+			return; //we don't need to scan simple constants
+
+		if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
+		{
+
+			//Attempt to insert array and if array wasn't present before do more things
+			if(usedArrays.insert(re->updates.root).second)
+			{
+
+				//check if the array is constant
+				if( re->updates.root->isConstantArray())
+					haveConstantArray=true;
+
+				//scan the update list
+				scanUpdates(re->updates.head);
+
+			}
+
+		}
+
+		//recurse into the children
+		Expr* ep = e.get();
+		for(unsigned int i=0; i < ep->getNumKids(); i++)
+			scan(ep->getKid(i));
+	}
+
+
+	void ExprSMTLIBPrinter::scanUpdates(const UpdateNode* un)
+	{
+		while(un != NULL)
+		{
+			scan(un->index);
+			scan(un->value);
+			un= un->next;
+		}
+	}
+
+
+	void ExprSMTLIBPrinter::printExit()
+	{
+		*o << "(exit)" << endl;
+	}
+
+	bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l)
+	{
+		if(l > QF_AUFBV)
+			return false;
+
+		logicToUse=l;
+		return true;
+	}
+
+	void ExprSMTLIBPrinter::printSeperator()
+	{
+		if(humanReadable)
+			p->breakLineI();
+		else
+			p->write(" ");
+	}
+
+	void ExprSMTLIBPrinter::printNotice()
+	{
+		*o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
+	}
+
+	void ExprSMTLIBPrinter::setHumanReadable(bool hr)
+	{
+		humanReadable=hr;
+	}
+
+	void ExprSMTLIBPrinter::printOptions()
+	{
+		//Print out SMTLIBv2 boolean options
+		for(std::map<SMTLIBboolOptions,bool>::const_iterator i= smtlibBoolOptions.begin(); i!= smtlibBoolOptions.end(); i++)
+		{
+			*o << "(set-option :" << getSMTLIBOptionString(i->first) <<
+			" " << ((i->second)?"true":"false") << ")" << endl;
+		}
+	}
+
+	void ExprSMTLIBPrinter::printQuery()
+	{
+		if(humanReadable)
+		{
+			*p << "; Query from solver turned into an assert";
+			p->breakLineI();
+		}
+
+		p->pushIndent();
+		*p << "(assert";
+		p->pushIndent();
+		printSeperator();
+
+		printExpression(queryAssert,SORT_BOOL);
+
+		p->popIndent();
+		printSeperator();
+		*p << ")";
+		p->popIndent();
+		p->breakLineI();
+	}
+
+	ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr>& e)
+	{
+		/* We could handle every operator in a large switch statement,
+		 * but this seems more elegant.
+		 */
+
+		if(e->getKind() == Expr::Extract)
+		{
+			/* This is a special corner case. In most cases if a node in the expression tree
+			 * is of width 1 it should be considered as SORT_BOOL. However it is possible to
+			 * perform an extract operation on a SORT_BITVECTOR and produce a SORT_BITVECTOR of length 1.
+			 * The ((_ extract i j) () ) operation in SMTLIBv2 always produces SORT_BITVECTOR
+			 */
+			return SORT_BITVECTOR;
+		}
+		else
+			return (e->getWidth() == Expr::Bool)?(SORT_BOOL):(SORT_BITVECTOR);
+	}
+
+	void ExprSMTLIBPrinter::printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
+	{
+		switch(sort)
+		{
+			case SORT_BITVECTOR:
+				if(humanReadable)
+				{
+					p->breakLineI(); *p << ";Performing implicit bool to bitvector cast"; p->breakLine();
+				}
+				//We assume the e is a bool that we need to cast to a bitvector sort.
+				*p << "(ite"; p->pushIndent(); printSeperator();
+				printExpression(e,SORT_BOOL); printSeperator();
+				*p << "(_ bv1 1)" ; printSeperator(); //printing the "true" bitvector
+				*p << "(_ bv0 1)" ; p->popIndent(); printSeperator(); //printing the "false" bitvector
+				*p << ")";
+				break;
+			case SORT_BOOL:
+			{
+				/* We make the assumption (might be wrong) that any bitvector whos unsigned decimal value is
+				 * is zero is interpreted as "false", otherwise it is true.
+				 *
+				 * This may not be the interpretation we actually want!
+				 */
+				Expr::Width bitWidth=e->getWidth();
+				if(humanReadable)
+				{
+					p->breakLineI(); *p << ";Performing implicit bitvector to bool cast"; p->breakLine();
+				}
+				*p << "(bvugt"; p->pushIndent(); printSeperator();
+				// We assume is e is a bitvector
+				printExpression(e,SORT_BITVECTOR); printSeperator();
+				*p << "(_ bv0 " << bitWidth << ")"; p->popIndent(); printSeperator(); //Zero bitvector of required width
+				*p << ")";
+
+				if(bitWidth!=Expr::Bool)
+					std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " << bitWidth << ") to bool!" << std::endl;
+
+			}
+				break;
+			default:
+				assert(0 && "Unsupported cast!");
+		}
+	}
+
+	void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
+	{
+		//This is the if-then-else expression
+
+		*p << "(" << getSMTLIBKeyword(e) << " ";
+		p->pushIndent(); //add indent for recursive call
+
+			//The condition
+			printSeperator();
+			printExpression(e->getKid(0),SORT_BOOL);
+
+			/* This operator is special in that the remaining children
+			 * can be of any sort.
+			 */
+
+			//if true
+			printSeperator();
+			printExpression(e->getKid(1),s);
+
+			//if false
+			printSeperator();
+			printExpression(e->getKid(2),s);
+
+
+		p->popIndent(); //pop indent added for recursive call
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
+	{
+		*p << "(" << getSMTLIBKeyword(e) << " ";
+		p->pushIndent(); //add indent for recursive call
+
+		//loop over children and recurse into each expecting they are of sort "s"
+		for(unsigned int i=0; i < e->getNumKids(); i++)
+		{
+			printSeperator();
+			printExpression(e->getKid(i),s);
+		}
+
+		p->popIndent(); //pop indent added for recursive call
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
+	{
+		/* For these operators it is the case that the expected sort is the same as the sorts
+		 * of the arguments.
+		 */
+
+		*p << "(";
+		switch(e->getKind())
+		{
+			case Expr::And:
+				*p << ((s==SORT_BITVECTOR)?"bvand":"and");
+				break;
+			case Expr::Not:
+				*p << ((s==SORT_BITVECTOR)?"bvnot":"not");
+				break;
+			case Expr::Or:
+				*p << ((s==SORT_BITVECTOR)?"bvor":"or");
+				break;
+
+			case Expr::Xor:
+				*p << ((s==SORT_BITVECTOR)?"bvxor":"xor");
+				break;
+			default:
+				*p << "ERROR"; // this shouldn't happen
+		}
+		*p << " ";
+
+		p->pushIndent(); //add indent for recursive call
+
+		//loop over children and recurse into each expecting they are of sort "s"
+		for(unsigned int i=0; i < e->getNumKids(); i++)
+		{
+			printSeperator();
+			printExpression(e->getKid(i),s);
+		}
+
+		p->popIndent(); //pop indent added for recursive call
+		printSeperator();
+		*p << ")";
+	}
+
+	void ExprSMTLIBPrinter::mangleQuery()
+	{
+		//Negating the query
+		queryAssert = Expr::createIsZero(query->expr);
+	}
+
+	bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value)
+	{
+		std::pair< std::map<SMTLIBboolOptions,bool>::iterator, bool> thePair;
+		bool theValue=  (value==OPTION_TRUE)?true:false;
+
+		switch(option)
+		{
+			case PRINT_SUCCESS:
+			case PRODUCE_MODELS:
+			case INTERACTIVE_MODE:
+				thePair=smtlibBoolOptions.insert(std::pair<SMTLIBboolOptions,bool>(option,theValue));
+
+				if(value== OPTION_DEFAULT)
+				{
+					//we should unset (by removing from map) this option so the solver uses its default
+					smtlibBoolOptions.erase(thePair.first);
+					return true;
+				}
+
+				if(!thePair.second)
+				{
+					//option was already present so modify instead.
+					thePair.first->second=value;
+				}
+				return true;
+			default:
+				return false;
+
+		}
+	}
+
+	void ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array*>& a)
+	{
+		arraysToCallGetValueOn = &a;
+
+		//This option must be set in order to use the SMTLIBv2 command (get-value () )
+		if(!a.empty())
+			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_TRUE);
+
+		/* There is a risk that users will ask about array values that aren't
+		 * even in the query. We should add them to the usedArrays list and hope
+		 * that the solver knows what to do when we ask for the values of arrays
+		 * that don't feature in our query!
+		 */
+		for(vector<const Array*>::const_iterator i = a.begin(); i!= a.end() ; ++i)
+		{
+			usedArrays.insert(*i);
+		}
+
+	}
+
+const char* ExprSMTLIBPrinter::getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option)
+{
+	switch(option)
+	{
+		case PRINT_SUCCESS: return "print-success";
+		case PRODUCE_MODELS: return "produce-models";
+		case INTERACTIVE_MODE: return "interactive-mode";
+		default:
+			return "unknown-option";
+	}
+}
+
+}
+
+
+