/********************************************************************
  Developers: Ajith John, Supratik Chakraborty

  Last updated: July 24, 2013
*********************************************************************/

/*********************************************************************

ExpressionMisc.cpp and ExpressionMisc.h contains a set of useful functions
for operating on expressions.  

*********************************************************************/

#include <iostream>
#include "ExpressionMisc.h"
using namespace std;

// function to create unsigned bit-vector symbols
t_Expression* CreateSymbol(string &symb_name, unsigned symb_width, t_ExpressionManager *em)
{
	TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, symb_width};
	return em->createSymbol(symb_name, te);
}

// function to create unsigned bit-vector constants
// const_value should be a binary string of width const_width
t_Expression* CreateConstant(string &const_value, unsigned const_width, t_ExpressionManager *em)
{
	// ensure that const_value is a binary string
	for (int i = 0; i < const_value.size(); i++)
	{
        	if (const_value[i] != '0' && const_value[i] != '1')
        	{
        		t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! non-binary string as input in function CreateConstant in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
               		return NULL;
        	}
    	}
	
	// ensure that size of const_value is const_width
	if(const_value.size() != const_width)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! size of binary string is different from the width specified in function CreateConstant in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
               	return NULL;
	}
	// create the bv-constant 
	else
	{
		TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, const_width};
		return em->createConstant(const_value, te);
	}
}

// functions to create unsigned bit-vector terms
t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_ExpressionManager *em)
{
	assert(child1 != NULL);

	TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
	vector<t_Expression *> children;
  	children.push_back(child1);
	return em->createExpression(term_name, children, te);
}

t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_Expression* child2, t_ExpressionManager *em)
{
	assert(child1 != NULL && child2 != NULL);	

	TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
	vector<t_Expression *> children;
  	children.push_back(child1);
	children.push_back(child2);
	return em->createExpression(term_name, children, te);
}

t_Expression* CreateTerm(string &term_name, unsigned term_width, t_Expression* child1, t_Expression* child2, t_Expression* child3,t_ExpressionManager *em)
{
	assert(child1 != NULL && child2 != NULL && child3 != NULL);	
	
	TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
	vector<t_Expression *> children;
  	children.push_back(child1);
	children.push_back(child2);
	children.push_back(child3);
	return em->createExpression(term_name, children, te);
}



t_Expression* CreateTerm(string &term_name, unsigned term_width, vector<t_Expression*> &children, t_ExpressionManager *em)
{
	assert(children.size() >= 1);

	if(children.size() == 1)
	{
		//create unary term
		assert(children[0] != NULL);
		return CreateTerm(term_name, term_width, children[0], em);
	}
	else if(children.size() == 2)
	{
		//create binary term
		assert(children[0] != NULL);
		assert(children[1] != NULL);
		return CreateTerm(term_name, term_width, children[0], children[1], em);
	}
	else
	{
		assert(children[0] != NULL);
		assert(children[1] != NULL);
		t_Expression* result = CreateTerm(term_name, term_width, children[0], children[1], em);

		for(int i = 2; i < children.size(); i++)
		{
			assert(result != NULL);
			assert(children[i] != NULL);
			result = CreateTerm(term_name, term_width, result, children[i], em);
		}
	
		return result;
	}		
}

// functions to create boolean nodes
t_Expression* CreateNode(string &node_name, t_Expression* child1, t_ExpressionManager *em)
{
	assert(child1 != NULL);

	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	vector<t_Expression *> children;
  	children.push_back(child1);
	return em->createExpression(node_name, children, te);
}

t_Expression* CreateNode(string &node_name, t_Expression* child1, t_Expression* child2, t_ExpressionManager *em)
{
	assert(child1 != NULL && child2 != NULL);

	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	vector<t_Expression *> children;
  	children.push_back(child1);
	children.push_back(child2);
	return em->createExpression(node_name, children, te);
}

t_Expression* CreateNode(string &node_name, t_Expression* child1, t_Expression* child2, t_Expression* child3, t_ExpressionManager *em)
{
	assert(child1 != NULL && child2 != NULL && child3 != NULL);

	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	vector<t_Expression *> children;
  	children.push_back(child1);
	children.push_back(child2);
	children.push_back(child3);
	return em->createExpression(node_name, children, te);
}

t_Expression* CreateNode(string &node_name, vector<t_Expression*> &children, t_ExpressionManager *em)
{
	assert(node_name == "logand" || node_name == "logor");
	assert(children.size() >= 2);
	
	if(children.size() == 2)
	{
		assert(children[0] != NULL);
		assert(children[1] != NULL);
		return CreateNode(node_name, children[0], children[1], em);
	}
	else
	{
		assert(children[0] != NULL);
		assert(children[1] != NULL);
		t_Expression* result = CreateNode(node_name, children[0], children[1], em);

		for(int i = 2; i < children.size(); i++)
		{
			assert(result != NULL);
			assert(children[i] != NULL);
			result = CreateNode(node_name, result, children[i], em);
		}
	
		return result;
	}		
}


// function to create "kand" node from "eqz", "diseqz" and "leq" node sets
// note that keeping "eqz", "diseqz" and "leq" children as sets avoids duplication

// Precondition: None of the children should be NULL. This condition is not checked inside the function. 
//		 Ensure this before calling the function. 
t_Expression* CreateKandNode(set<t_Expression*> &EqzChildren, set<t_Expression*> &DiseqzChildren, set<t_Expression*> &LeqChildren, t_ExpressionManager *em)
{
	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	//concate EqzChildren, DiseqzChildren and LeqChildren to get SortedChildren
	vector<t_Expression*> SortedChildren(EqzChildren.begin(), EqzChildren.end());
	copy(DiseqzChildren.begin(), DiseqzChildren.end(), inserter(SortedChildren, SortedChildren.end()));
	copy(LeqChildren.begin(), LeqChildren.end(), inserter(SortedChildren, SortedChildren.end()));
	
	assert(SortedChildren.size() > 0);

	string term_name = "kand";
	return em->createExpression(term_name, SortedChildren, te);	
}



// function to create "kand" node from two existing "kand" nodes.
// Collects the children of the existing "kand" nodes, and creates
// a new "kand" node.
t_Expression* CreateKandNode(t_Expression* kand_1, t_Expression* kand_2, t_ExpressionManager *em)
{
	assert(kand_1 != NULL);
	assert(kand_2 != NULL);

	if(isTrue(kand_1, em)) // kand_1 == true
	{
		return kand_2;
	}
	else if(isTrue(kand_2, em)) // kand_2 == true
	{
		return kand_1;
	}
	else
	{
		set<t_Expression*> E_1, D_1, I_1;
		bool ConstraintsFound = findConstraintsFromKandNode(kand_1, E_1, D_1, I_1, em);
		assert(ConstraintsFound);

		set<t_Expression*> E_2, D_2, I_2;
		ConstraintsFound = findConstraintsFromKandNode(kand_2, E_2, D_2, I_2, em);
		assert(ConstraintsFound);

		set<t_Expression*> E, D, I;
		set_union(E_1.begin(), E_1.end(), E_2.begin(), E_2.end(),inserter(E, E.begin()));
		set_union(D_1.begin(), D_1.end(), D_2.begin(), D_2.end(),inserter(D, D.begin()));
		set_union(I_1.begin(), I_1.end(), I_2.begin(), I_2.end(),inserter(I, I.begin()));

		t_Expression* kand = CreateKandNode(E, D, I, em);
		assert(kand != NULL);
		return kand;
	}	
}


// Given a set of constraints, where each constraint is 
// eqz, diseqz, leq, not (eqz), not(diseqz), or not(leq),
// pushes the negation inside in case of not(eqz), not(diseqz), and not(leq), 
// and returns kand which is a conjunction of these constraints. 
// Returns true if the conjunction is true; returns NULL in case of errors. 
t_Expression* obtainKandNodeFromASetOfConstraints(set<t_Expression*> &Constraints, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable)
{
	set <t_Expression*> EqzChildren;
	set <t_Expression*> DiseqzChildren;
	set <t_Expression*> LeqChildren; 

	for(set<t_Expression*>::iterator it = Constraints.begin(); it != Constraints.end(); it++) // take each constraint
	{	
		t_Expression* Constraint = *it;
		assert(Constraint != NULL);

		string Label = em->getLabelOfExpression(Constraint);
		if("eqz" == Label) // equation
		{	
			EqzChildren.insert(Constraint);
		}
		else if("diseqz" == Label) // disequation
		{	
			DiseqzChildren.insert(Constraint);
		}
		else if("leq" == Label) // inequation
		{	
			LeqChildren.insert(Constraint);
		}
		else	if("lognot" == Label) // negation of LMC
		{
			// take the LMC
			t_Expression* LMC = getIthChild(Constraint, 0, em);
			assert(LMC != NULL);

			string LabelOfLMC = em->getLabelOfExpression(LMC);
			if("eqz" == LabelOfLMC) // equation t = 0
			{	
				t_Expression* NegatedConstraint = negateLME(LMC, em); // disequation t \neq 0
				assert(NegatedConstraint != NULL);

				DiseqzChildren.insert(NegatedConstraint);
			}
			else if("diseqz" == LabelOfLMC) // disequation t \neq 0
			{	
				t_Expression* NegatedConstraint = negateLMD(LMC, em); // equation t = 0
				assert(NegatedConstraint != NULL);

				EqzChildren.insert(NegatedConstraint);
			}
			else if("leq" == LabelOfLMC) // inequation t1 \leq t2
			{	
				// negation of t1 \leq t2 \equiv t1 > t2
				// t1 > t2 \equiv t1-1 >= t2 \wedge t1 \neq 0
				// t1 > t2 \equiv t1 >= t2+1 \wedge t2 \neq 2^p-1
				t_Expression* NegatedLMI_LMIPart; // This denotes t1-1 >= t2 or t1 >= t2+1
				t_Expression* NegatedLMI_LMDPart; // This denotes t1 \neq 0 or t2 \neq 2^p-1; NULL if the disequation is trivial
				
				NegatedLMI_LMIPart = negateLMI(LMC, NegatedLMI_LMDPart, em, bvm, VariableList, WidthTable);
				
				assert(NegatedLMI_LMIPart != NULL); // This part cannot be NULL
				LeqChildren.insert(NegatedLMI_LMIPart);

				if(NegatedLMI_LMDPart != NULL)
				{
					DiseqzChildren.insert(NegatedLMI_LMDPart);
				}			
			}
			else	
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! unknown negated constraint in function obtainKandNodeFromASetOfConstraints in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return NULL;
			}
		}
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unknown constraint in function obtainKandNodeFromASetOfConstraints in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return NULL;
		}
	}// for ends here

	// create the kand node
	t_Expression* KandNode;

	if(EqzChildren.empty()  && DiseqzChildren.empty() && LeqChildren.empty())
	{
		// all children are trivial; hence result is true
		KandNode = getTrue(em);
	}
	else
	{
		KandNode = CreateKandNode(EqzChildren, DiseqzChildren, LeqChildren, em);
	}
	
	// return the kand node
	assert(KandNode != NULL);	
	return KandNode;
}//function ends here




// get index of variable from VariableList
// returns -1 if the variable has no entry in VariableList
int getVariableIndex(const string &variable, t_HashTable <string, int> &VariableList)
{
	t_HTStatusValue <int> result_search = VariableList.hashtable_search(variable);
	if(result_search.success())
    	{
		return result_search.getValue();
	}
	else
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! hash table search failure in function getVariableIndex in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
	        return -1;
	}
}

// adds entry (variable, index) into VariableList
// index should be >= 0
bool addEntryToVariableList(const string &variable, int index, t_HashTable <string, int> &VariableList)
{
	if(index < 0)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! index < 0 in function addEntryToVariableList in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
	        return false;
	}
	else
	{
		t_HTStatusValue <int> insert_result = VariableList.hashtable_insert(variable, index);
		if (insert_result.success())
            	{
                	return true;
            	}
        	else
            	{
                	t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! hash table insert failure in function addEntryToVariableList in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
	       	 	return false;
            	}	
	}//else ends here
}



// check if 
// (1) children are sorted based on the indices of variables in the monoms
// (2) all coefficients are non-zero
// return true if (1) and (2) are satisfied, returns false otherwise with error message
bool checkIfChildrenOfKaddNodeAreSortedAndAllCoefficientsAreNonZero(const vector<t_Expression*> &children, t_ExpressionManager *em, t_HashTable <string, int> &VariableList)
{
	if(children.size() == 0)// no children, it is fine, take it as sorted. 
	{
		return true;
	}
	else
	{
		//note that each children[i] is a monom
		// let's get the variable node from it and coefficient node from it

		t_Expression* PreviousCoefficientNode = getIthChild(children[0], 0, em);
		assert(PreviousCoefficientNode != NULL);

		// let's get its label
		string PreviousCoefficientName = em->getLabelOfExpression(PreviousCoefficientNode);
		
		t_Expression* PreviousVariableNode = getIthChild(children[0], 1, em);
		assert(PreviousVariableNode != NULL);

		// let's get its name
		string PreviousVariableName = em->getLabelOfExpression(PreviousVariableNode);
		// let's get its variable index
		int PreviousVariableIndex = getVariableIndex(PreviousVariableName, VariableList);
		
		if(isZeroConstant(PreviousCoefficientName)) // coefficient is zero
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! zero coefficient encountered in function checkIfChildrenOfKaddNodeAreSorted  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
                	return false;
		}		
		else if(PreviousVariableIndex < 0) // unknown variable encountered
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unknown variable encountered in function checkIfChildrenOfKaddNodeAreSorted  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
                	return false;
		}
		else
		{
			for(int i = 1; i < children.size(); i++)
			{
				// let's get the variable node from it and coefficient node from it
				t_Expression* CoefficientNode = getIthChild(children[i], 0, em);
				assert(CoefficientNode != NULL);

				// let's get its label
				string CoefficientName = em->getLabelOfExpression(CoefficientNode);

				// let's get the variable index of children[i]
				t_Expression* VariableNode = getIthChild(children[i], 1, em);
				assert(VariableNode != NULL);

				// let's get its name
				string VariableName = em->getLabelOfExpression(VariableNode);
				// let's get its variable index
				int VariableIndex = getVariableIndex(VariableName, VariableList);

				if(isZeroConstant(CoefficientName)) // coefficient is zero
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! zero coefficient encountered in function checkIfChildrenOfKaddNodeAreSorted  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
                			return false;
				}
				else if(VariableIndex < 0)// unknown variable encountered
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! unknown variable encountered in function checkIfChildrenOfKaddNodeAreSorted  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
		                	return false;
				}
				else if(PreviousVariableIndex >= VariableIndex)//we need a strict ordering on variables
				// i.e. we need PreviousVariableIndex < VariableIndex
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! monoms are not sorted in function checkIfChildrenOfKaddNodeAreSorted  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;
				}

				PreviousVariableIndex = VariableIndex;
			}//for ends here
		return true;
		}//else ends here
	}//else ends here
}



// function to create "kadd" node from the constant child and sorted children (monoms).
// note that the constant child is NULL by default.
// 
// preconditions: 1) monom children should be sorted (for correctness)
//		  2) no coefficient or constant should be zero (for efficiency)
//		  both conditions are checked inside the function. NULL is returned if either is is false.
//		  3) None of the children should be NULL. This condition is not checked inside the function.
//		     Ensure this before calling the function. 
t_Expression* CreateKaddNode(unsigned term_width, vector<t_Expression*> &SortedChildren, t_ExpressionManager *em, t_HashTable <string, int> &VariableList, t_Expression* ConstantChild)
{
	bool ChildrenAreSortedAndAllCoefficientsAreNonZero = checkIfChildrenOfKaddNodeAreSortedAndAllCoefficientsAreNonZero(SortedChildren, em, VariableList);
	if(ChildrenAreSortedAndAllCoefficientsAreNonZero)
	{
		if(SortedChildren.size() == 0 && ConstantChild == NULL)
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! call to function CreateKaddNode in ExpressionMisc.cpp with no children", logFile, c_RunLevelVerbosity);
			logFile->close();
        	        return NULL;	
		}
		else
		{
			TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
			string term_name = "kadd";
			
			if(ConstantChild == NULL) // no constant
			{
				return em->createExpression(term_name, SortedChildren, te);	
			}
			else 
			{
				string ConstantName = em->getLabelOfExpression(ConstantChild);
				if(isZeroConstant(ConstantName)) // constant is there, but zero
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! call to function CreateKaddNode in ExpressionMisc.cpp with constant as zero", logFile, c_RunLevelVerbosity);
					logFile->close();
        	        		return NULL;	
				}	
				else // constant is there, and non-zero
				{
					vector<t_Expression*> FinalChildren;
					FinalChildren.push_back(ConstantChild); 
					FinalChildren.insert(FinalChildren.end(), SortedChildren.begin(), SortedChildren.end());				
					return em->createExpression(term_name, FinalChildren, te);				
				}
			}// else of if(ConstantChild == NULL)  ends here			
		}// else of if(SortedChildren.size() == 0 && ConstantChild == NULL) ends here
	}// if(ChildrenAreSorted) ends here
	else
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! ensure that children are sorted and coefficients are non-zero in function CreateKaddNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return NULL;
	}// else of if(ChildrenAreSorted) ends here
}




// function to create "kadd" node from the constant and coefficient map.
// precondition: monom children should be sorted (for correctness)
//		 this condition is checked inside the function. NULL is returned if it is false.
// note that if (1) the constant is zero and (2) the coefficient_map is empty or has only zero coefficients, 
// then "kadd" node with a single zero child is returned. 
t_Expression* CreateKaddNodeFromConstantAndCoefficientMap(unsigned term_width, bvatom constant, const vector< pair< string, bvatom > > &coefficient_map, t_ExpressionManager *em, t_HashTable <string, int> &VariableList, BVManager* bvm)
{
	vector<t_Expression*> SortedChildrenVector; // children of the "kadd" node to be created
	
	t_Expression* ConstantExp; //let's create expression for the constant part first
	if(!(bvm->checkBVForZero(constant))) //if constant = 0, avoid it
	{
		//create the constant expression and insert it into SortedChildrenvector
		string constant_string = bvm->printBVasBinString(constant);
		unsigned constant_width = constant_string.size();
		ConstantExp = CreateConstant(constant_string, constant_width, em);
		assert(ConstantExp != NULL);
		SortedChildrenVector.push_back(ConstantExp);
	}

	// let's push back the monoms into the sorted children

	if(coefficient_map.size() > 0)
	{
		string PreviousVariableName = coefficient_map[0].first;
		bvatom PreviousCoefficient = coefficient_map[0].second;
		// let's get its variable index
		int PreviousVariableIndex = getVariableIndex(PreviousVariableName, VariableList);
		
		if(PreviousVariableIndex < 0) // unknown variable encountered
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unknown variable encountered in function  CreateKaddNodeFromConstantAndCoefficientMap in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
                	return NULL;
		}
		else if(!(bvm->checkBVForZero(PreviousCoefficient))) // if coefficient is zero, avoid it
		{
			// coefficient is not zero; create the monom
			string CoefficientString = bvm->printBVasBinString(PreviousCoefficient);
			unsigned CoefficientWidth = CoefficientString.size();
			t_Expression* CoefficientExp = CreateConstant(CoefficientString, CoefficientWidth, em);
			t_Expression* VariableExp = CreateSymbol(PreviousVariableName, CoefficientWidth, em);
			assert(CoefficientExp != NULL);
			assert(VariableExp != NULL);

			string multiply_label = "bvmul";
			t_Expression* Monom = CreateTerm(multiply_label, CoefficientWidth, CoefficientExp, VariableExp, em);
			assert(Monom != NULL);

			// insert the monom into SortedChildrenvector 
			SortedChildrenVector.push_back(Monom);
		}
			
		for(int i = 1; i < coefficient_map.size(); i++)
		{
			string VariableName = coefficient_map[i].first;
			bvatom Coefficient = coefficient_map[i].second;
			// let's get its variable index
			int VariableIndex = getVariableIndex(VariableName, VariableList);

			if(VariableIndex < 0)// unknown variable encountered
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! unknown variable encountered in function createKaddNodeFromConstantAndCoefficientMap  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
		               	return NULL;
			}
			else if(PreviousVariableIndex >= VariableIndex)//we need a strict ordering on variables
			// i.e. we need PreviousVariableIndex < VariableIndex
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! monoms are not sorted in function createKaddNodeFromConstantAndCoefficientMap  in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return NULL;
			}
			else if(!(bvm->checkBVForZero(Coefficient))) // if coefficient is zero, avoid it
			{
				// coefficient is not zero; create the monom
				string CoefficientString = bvm->printBVasBinString(Coefficient);
				unsigned CoefficientWidth = CoefficientString.size();
				t_Expression* CoefficientExp = CreateConstant(CoefficientString, CoefficientWidth, em);
				t_Expression* VariableExp = CreateSymbol(VariableName, CoefficientWidth, em);
				assert(CoefficientExp != NULL);
				assert(VariableExp != NULL);				

				string multiply_label = "bvmul";
				t_Expression* Monom = CreateTerm(multiply_label, CoefficientWidth, CoefficientExp, VariableExp, em);
				assert(Monom != NULL);

				// insert the monom into SortedChildrenvector 
				SortedChildrenVector.push_back(Monom);
			}//else if(!(bvm->checkBVForZero(Coefficient))) ends here
			PreviousVariableIndex = VariableIndex;
		}//for ends here
	}// if(coefficient_map.size() > 0) ends here	

	//now we have the sorted children
	if(SortedChildrenVector.size() == 0)
	{
		// we need to create "kadd" node with a single child which is 0

		string ZeroString = getZeroBinaryStringOfGivenLength(term_width);
		t_Expression* ZeroExp = CreateConstant(ZeroString, term_width, em);
		assert(ZeroExp != NULL);
		SortedChildrenVector.push_back(ZeroExp);
		
		TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
		string term_name = "kadd";

		return em->createExpression(term_name, SortedChildrenVector, te);	
	}
	else
	{
		TypeOfExpressionTuple te = {TYPE_UNSIGNED_BITVECTOR, term_width};
		string term_name = "kadd";
		return em->createExpression(term_name, SortedChildrenVector, te);	
	}
}//function ends here



// functions to create boolean constants
t_Expression* getTrue(t_ExpressionManager *em)
{
	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	string const_value = "true";
	return em->createConstant(const_value, te);
}

t_Expression* getFalse(t_ExpressionManager *em)
{
	TypeOfExpressionTuple te = {TYPE_BOOL, 1};
	string const_value = "false";
	return em->createConstant(const_value, te);
}

// finds the number of child nodes in the parameter degree
// returns false in case of errors; false otherwise
bool Degree(t_Expression* exp, t_ExpressionManager *em, unsigned int &degree)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function Degree in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		degree = 0;
                return false;
	}
	else
	{
		degree = (em->getVectorOfOperands(exp)).size();
		return true;
	}
}


// returns i^{th} child node of exp
// returns NULL in case of errors
t_Expression* getIthChild(t_Expression* exp, unsigned int i, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function getIthChild in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return NULL;
	}
	else
	{
		vector<t_Expression*> operands = em->getVectorOfOperands(exp);
		
		if(i >= operands.size())
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! i >= operands.size() in function getIthChild in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
                	return NULL;
		}
		else
		{
			return operands[i];
		}
	}
}

// functions to check if expression is a constant
bool isTrue(t_Expression* exp, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function isTrue in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return false;
	}
	else if(TYPE_BOOL == em->getTypeOfExpressionWithOutWidth(exp) && CONSTANT == em->getTypeOfValueStoredInExpressionLabel(exp) && "true" == em->getLabelOfExpression(exp))
	{
		return true;
	}
	else
	{
		return false;
	}		
}


bool isFalse(t_Expression* exp, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function isFalse in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return false;
	}
	else if(TYPE_BOOL == em->getTypeOfExpressionWithOutWidth(exp) && CONSTANT == em->getTypeOfValueStoredInExpressionLabel(exp) && "false" == em->getLabelOfExpression(exp))
	{
		return true;
	}
	else
	{
		return false;
	}		
}


bool isBVConstant(t_Expression* exp, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function isBVConstant in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return false;
	}
	else if(TYPE_UNSIGNED_BITVECTOR == em->getTypeOfExpressionWithOutWidth(exp) && CONSTANT == em->getTypeOfValueStoredInExpressionLabel(exp))
	{
		return true;
	}
	else
	{
		return false;
	}		
}


bool isBooleanConstant(t_Expression* exp, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function isBooleanConstant in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return false;
	}
	else if(TYPE_BOOL == em->getTypeOfExpressionWithOutWidth(exp) && CONSTANT == em->getTypeOfValueStoredInExpressionLabel(exp))
	{
		return true;
	}
	else
	{
		return false;
	}				
}

bool isBVVariable(t_Expression* exp, t_ExpressionManager *em)
{
	if(exp == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! exp is NULL in function isBVVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
                return false;
	}
	else if(TYPE_UNSIGNED_BITVECTOR == em->getTypeOfExpressionWithOutWidth(exp) && SYMBOL == em->getTypeOfValueStoredInExpressionLabel(exp))
	{
		return true;
	}
	else
	{
		return false;
	}		
}



// get width of variable from WidthTable
// returns -1 if the variable has no entry in WidthTable
int getWidthOfVariable(const string &variable, t_HashTable <string, int> &WidthTable)
{
	t_HTStatusValue <int> result_search = WidthTable.hashtable_search(variable);
	if(result_search.success())
    	{
		return result_search.getValue();
	}
	else
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! hash table search failure in function getWidthOfVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
	        return -1;
	}
}

// adds entry (variable, width) into WidthTable
// width should be >= 1
bool addEntryToWidthTable(const string &variable, int width, t_HashTable <string, int> &WidthTable)
{
	if(width <= 0)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! width <= 0 in function addEntryToWidthTable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
	        return false;
	}
	else
	{
		t_HTStatusValue <int> insert_result = WidthTable.hashtable_insert(variable, width);
		if (insert_result.success())
            	{
                	return true;
            	}
        	else
            	{
                	t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! hash table insert failure in function addEntryToWidthTable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
	       	 	return false;
            	}	
	}//else ends here
}




// Given a "kand" node, obtain the equations in E, disequations in D, and inequations in I
bool findConstraintsFromKandNode(t_Expression* kandNode, set<t_Expression*> &E, set<t_Expression*> &D, set<t_Expression*> &I, t_ExpressionManager *em)
{
	if(kandNode == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! kandNode is NULL in function findConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("kand" != em->getLabelOfExpression(kandNode))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		vector <t_Expression*> Children = em->getVectorOfOperands(kandNode);

		for(int i = 0; i < Children.size(); i++)// take each child
		{
			t_Expression* Child = Children[i];

			assert(Child != NULL);

			if("eqz" == em->getLabelOfExpression(Child))//if child is equation
			{			
				E.insert(Child);

			}//if child is equation ends here
			else if("diseqz" == em->getLabelOfExpression(Child))// if child is disequation
			{
				D.insert(Child);
			
			}//if child is disequation ends here
			else if("leq" == em->getLabelOfExpression(Child))// if child is inequation
			{
				I.insert(Child);
				
			}//if child is inequation ends here
			else
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function findConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}

		}// for each child ends here

		return true;
	}// else of if (!kandNode) ends here
}// function ends here



// returns true if the eqzNode is trivial i.e. true, false otherwise
bool	equationIsTrivial(t_Expression *eqzNode, t_ExpressionManager *em)
{
	assert(eqzNode != NULL);
	assert("eqz" == em->getLabelOfExpression(eqzNode));

	t_Expression* kaddNode = getIthChild(eqzNode, 0, em);

	assert(kaddNode != NULL);
	
	if(kaddIsZeroConstant(kaddNode, em)) // kaddNode is zero, i.e. eqzNode is 0 = 0
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the eqzNode is false, true otherwise
bool equationIsFalse(t_Expression *eqzNode, t_ExpressionManager *em)
{
	assert(eqzNode != NULL);
	assert("eqz" == em->getLabelOfExpression(eqzNode));

	t_Expression* kaddNode = getIthChild(eqzNode, 0, em);

	assert(kaddNode != NULL);
	
	if(kaddIsNonZeroConstant(kaddNode, em)) // kaddNode is non-zero constant, eg: eqzNode is 2 = 0
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the diseqzNode is trivial i.e. true, false otherwise
bool disequationIsTrivial(t_Expression *diseqzNode, t_ExpressionManager *em)
{
	assert(diseqzNode != NULL);
	assert("diseqz" == em->getLabelOfExpression(diseqzNode));

	t_Expression* kaddNode = getIthChild(diseqzNode, 0, em);

	assert(kaddNode != NULL);
	
	if(kaddIsNonZeroConstant(kaddNode, em)) // kaddNode is non-zero constant, eg: diseqzNode is not(7 = 0)
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the diseqzNode is false, false otherwise
bool disequationIsFalse(t_Expression *diseqzNode, t_ExpressionManager *em)
{
	assert(diseqzNode != NULL);
	assert("diseqz" == em->getLabelOfExpression(diseqzNode));

	t_Expression* kaddNode = getIthChild(diseqzNode, 0, em);

	assert(kaddNode != NULL);
	
	if(kaddIsZeroConstant(kaddNode, em)) // kaddNode is zero constant, i.e. diseqzNode is not(0 = 0)
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the leqNode is trivial i.e. true, false otherwise
bool inequationIsTrivial(t_Expression *leqNode, t_ExpressionManager *em, BVManager* bvm)
{
	assert(leqNode != NULL);
	assert("leq" == em->getLabelOfExpression(leqNode));

	vector <t_Expression*> ChildrenOfLeqNode = em->getVectorOfOperands(leqNode); 

	assert(ChildrenOfLeqNode.size() == 2);

	t_Expression* lhsKaddNode = ChildrenOfLeqNode[0];
	t_Expression* rhsKaddNode = ChildrenOfLeqNode[1];

	assert(lhsKaddNode != NULL);
	assert(rhsKaddNode != NULL);
	
	if(kaddIsZeroConstant(lhsKaddNode, em)) // lhsKaddNode is zero constant, i.e. inequation is like 0 <= t
		{
		return true;
		}
	else if(kaddIsMaximumConstant(rhsKaddNode, em)) // rhsKaddNode is maximum constant, i.e. inequation is like t <= 2^{p}-1
		{
		return true;
		}
	else if(firstKaddIsLteSecondKadd(lhsKaddNode, rhsKaddNode, em, bvm)) // eg: inequation is like 6 <= 7
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the leqNode is false, false otherwise
bool inequationIsFalse(t_Expression *leqNode, t_ExpressionManager *em, BVManager* bvm)
{
	assert(leqNode != NULL);
	assert("leq" == em->getLabelOfExpression(leqNode));

	vector <t_Expression*> ChildrenOfLeqNode = em->getVectorOfOperands(leqNode); 

	assert(ChildrenOfLeqNode.size() == 2);

	t_Expression* lhsKaddNode = ChildrenOfLeqNode[0];
	t_Expression* rhsKaddNode = ChildrenOfLeqNode[1];

	assert(lhsKaddNode != NULL);
	assert(rhsKaddNode != NULL);
	
	if(firstKaddIsGtSecondKadd(lhsKaddNode, rhsKaddNode, em, bvm)) // eg: inequation is like 7 <= 6
		{
		return true;
		}
	else
		{
		return false;
		}
}



// returns true if the kaddNode is zero constant, false otherwise
bool kaddIsZeroConstant(t_Expression *kaddNode, t_ExpressionManager *em)
{
	assert(kaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(kaddNode));

	vector <t_Expression*> ChildrenOfKaddNode = em->getVectorOfOperands(kaddNode); 
	if(ChildrenOfKaddNode.size() != 1)
	{
		return false;
	}
	else
	{
		assert(ChildrenOfKaddNode[0] != NULL);		

		if(!isBVConstant(ChildrenOfKaddNode[0], em))
		{
			return false;
		}
		else
		{
			string ConstantString = em->getLabelOfExpression(ChildrenOfKaddNode[0]);
			// recall that Coefficient is a (zero-padded) binary string starting with "0b"; 			
			ConstantString = ConstantString.substr(2); //we need characters from position 2 to end
			
			if(isZeroConstant(ConstantString))	
			{
				return true;
			}
			else
			{
				return false;
			}// else of if(isZeroConstant(ConstantString))	 ends here
		}// else of f(!isBVConstant(ChildrenOfKaddNode[0], em)) ends here
	}//else of if(ChildrenOfKaddNode.size() != 1) ends here

}
	


// returns true if the kaddNode is a non-zero constant, false otherwise
bool kaddIsNonZeroConstant(t_Expression *kaddNode, t_ExpressionManager *em)
{
	assert(kaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(kaddNode));

	vector <t_Expression*> ChildrenOfKaddNode = em->getVectorOfOperands(kaddNode); 
	if(ChildrenOfKaddNode.size() != 1)
	{
		return false;
	}
	else
	{
		assert(ChildrenOfKaddNode[0] != NULL);		
		
		if(!isBVConstant(ChildrenOfKaddNode[0], em))
		{
			return false;
		}
		else
		{
			string ConstantString = em->getLabelOfExpression(ChildrenOfKaddNode[0]);
			// recall that Coefficient is a (zero-padded) binary string starting with "0b"; 			
			ConstantString = ConstantString.substr(2); //we need characters from position 2 to end
			
			if(isZeroConstant(ConstantString))	
			{
				return false;
			}
			else
			{
				return true;
			}// else of if(isZeroConstant(ConstantString))	 ends here
		}// else of f(!isBVConstant(ChildrenOfKaddNode[0], em)) ends here
	}//else of if(ChildrenOfKaddNode.size() != 1) ends here

}



// returns true if the kaddNode is the maximum constant 2^{p}-1, false otherwise
bool kaddIsMaximumConstant(t_Expression *kaddNode, t_ExpressionManager *em)
{
	assert(kaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(kaddNode));

	vector <t_Expression*> ChildrenOfKaddNode = em->getVectorOfOperands(kaddNode); 
	if(ChildrenOfKaddNode.size() != 1)
	{
		return false;
	}
	else
	{
		assert(ChildrenOfKaddNode[0] != NULL);
		
		if(!isBVConstant(ChildrenOfKaddNode[0], em))
		{
			return false;
		}
		else
		{
			string ConstantString = em->getLabelOfExpression(ChildrenOfKaddNode[0]);
			// recall that Coefficient is a (zero-padded) binary string starting with "0b"; 			
			ConstantString = ConstantString.substr(2); //we need characters from position 2 to end
			
			if(isMaximumConstant(ConstantString))	
			{
				return true;
			}
			else
			{
				return false;
			}// else of if(isMaximumConstant(ConstantString))	 ends here
		}// else of f(!isBVConstant(ChildrenOfKaddNode[0], em)) ends here
	}//else of if(ChildrenOfKaddNode.size() != 1) ends here

}



// returns true if 
// (1) both the firstKaddNode and the secondKaddNode are constants and
// (2) the firstKaddNode is less than or equal to the secondKaddNode
// returns false otherwise
bool firstKaddIsLteSecondKadd(t_Expression *firstKaddNode, t_Expression *secondKaddNode, t_ExpressionManager *em, BVManager* bvm)
{
	assert(firstKaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(firstKaddNode));

	assert(secondKaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(secondKaddNode));

	vector <t_Expression*> ChildrenOfFirstKaddNode = em->getVectorOfOperands(firstKaddNode); 
	vector <t_Expression*> ChildrenOfSecondKaddNode = em->getVectorOfOperands(secondKaddNode); 

	if(ChildrenOfFirstKaddNode.size() != 1 || ChildrenOfSecondKaddNode.size() != 1)
	{
		return false;
	}
	else
	{

		assert(ChildrenOfFirstKaddNode[0] != NULL);
		assert(ChildrenOfSecondKaddNode[0] != NULL);

		if(!isBVConstant(ChildrenOfFirstKaddNode[0], em) || !isBVConstant(ChildrenOfSecondKaddNode[0], em))
		{
			return false;
		}
		else
		{
			string FirstConstantString = em->getLabelOfExpression(ChildrenOfFirstKaddNode[0]);
			FirstConstantString = FirstConstantString.substr(2); //we need characters from position 2 to end
			bvatom FirstConstant = bvm->getBVatom(FirstConstantString.size(), FirstConstantString);

			string SecondConstantString = em->getLabelOfExpression(ChildrenOfSecondKaddNode[0]);
			SecondConstantString = SecondConstantString.substr(2); //we need characters from position 2 to end
			bvatom SecondConstant = bvm->getBVatom(SecondConstantString.size(), SecondConstantString);		
			
			if(bvm->checkBVGreaterThan(SecondConstant, FirstConstant) || bvm->checkBVEquality(SecondConstant, FirstConstant))	
			{
				return true;
			}
			else
			{
				return false;
			}//if SecondConstant >= FirstConstant ends here
		}//if both first and second kadd's are constants ends here
	}//if both first and second kadd's have single child ends here
}//function ends here


// returns true if 
// (1) both the firstKaddNode and the secondKaddNode are constants and
// (2) the firstKaddNode is greater than the secondKaddNode
// returns false otherwise
bool firstKaddIsGtSecondKadd(t_Expression *firstKaddNode, t_Expression *secondKaddNode, t_ExpressionManager *em, BVManager* bvm)
{
	assert(firstKaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(firstKaddNode));

	assert(secondKaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(secondKaddNode));

	vector <t_Expression*> ChildrenOfFirstKaddNode = em->getVectorOfOperands(firstKaddNode); 
	vector <t_Expression*> ChildrenOfSecondKaddNode = em->getVectorOfOperands(secondKaddNode); 

	if(ChildrenOfFirstKaddNode.size() != 1 || ChildrenOfSecondKaddNode.size() != 1)
	{
		return false;
	}
	else
	{

		assert(ChildrenOfFirstKaddNode[0] != NULL);
		assert(ChildrenOfSecondKaddNode[0] != NULL);

		if(!isBVConstant(ChildrenOfFirstKaddNode[0], em) || !isBVConstant(ChildrenOfSecondKaddNode[0], em))
		{
			return false;
		}
		else
		{
			string FirstConstantString = em->getLabelOfExpression(ChildrenOfFirstKaddNode[0]);
			FirstConstantString = FirstConstantString.substr(2); //we need characters from position 2 to end
			bvatom FirstConstant = bvm->getBVatom(FirstConstantString.size(), FirstConstantString);

			string SecondConstantString = em->getLabelOfExpression(ChildrenOfSecondKaddNode[0]);
			SecondConstantString = SecondConstantString.substr(2); //we need characters from position 2 to end
			bvatom SecondConstant = bvm->getBVatom(SecondConstantString.size(), SecondConstantString);		
			
			if(bvm->checkBVGreaterThan(FirstConstant, SecondConstant))	
			{
				return true;
			}
			else
			{
				return false;
			}//if FirstConstant > SecondConstant ends here
		}//if both first and second kadd's are constants ends here
	}//if both first and second kadd's have single child ends here
}//function ends here
	



// Given a "kadd" node, this function finds the monom i.e. bvmul node with the variable. 
// Sets "MonomWithVariable" to NULL if the "kadd" node is free of the variable. 
// Returns false in case of errors; true otherwise. 
bool findMonomOfKaddNodeWithGivenVariable(t_Expression* kaddNode, const string &variable, t_Expression* &MonomWithVariable, t_ExpressionManager *em,  t_HashTable <string, int> &VariableList)
{
	if(kaddNode == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! kaddNode is NULL in function findMonomOfKaddNodeWithGivenVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("kadd" != em->getLabelOfExpression(kaddNode))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findMonomOfKaddNodeWithGivenVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		vector <t_Expression*> Children = em->getVectorOfOperands(kaddNode); 
		// the first child can be a constant; remove it from Children if so
		if(Children.size() == 0)
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! kaddNode with no children in function findMonomOfKaddNodeWithGivenVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else
		{
			assert(Children[0] != NULL);
			
			if(isBVConstant(Children[0], em)) //constant child exists	
			{
				if(Children.size() == 1) //we have only one child which is a constant
				{
					MonomWithVariable = NULL;
					return true;
				}
				else
				{
					Children.erase (Children.begin());				
				}
			}
			// Now Children is a vector of monoms; do binary search on it. 
			
			int VariableIndex = getVariableIndex(variable, VariableList); 

			assert(VariableIndex >= 0);

			int MonomLocation;
			bool SearchDone = binarySearch(Children, 0, Children.size()-1, VariableIndex, MonomLocation, em, VariableList);
			if(!SearchDone)
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! error in searching in function findMonomOfKaddNodeWithGivenVariable in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}
			else
			{
				if(MonomLocation < 0)
				{
					MonomWithVariable = NULL;
				}
				else
				{
					MonomWithVariable = Children[MonomLocation];
				}

				return true;
			}// else of if(!SearchDone) ends here
			
		}// else of if(Children.size() == 0) ends here

	}// else of if("kadd" != em->getLabelOfExpression(kaddNode)) ends here
}//function ends here



// Given a vector of monoms in "Children", find the location of the monom containing
// the variable with index "key" in "MonomLocation". If there's no child with the variable, then set
// "MonomLocation" to -1. Returns false in case of errors; true otherwise. 
bool binarySearch(const vector <t_Expression*> &Children, int first, int last, int key, int &MonomLocation, t_ExpressionManager *em, t_HashTable <string, int> &VariableList)
{
	while (first <= last) 
	{
		int mid = (first + last) / 2;  // compute mid point
		
		// get the variable of monom at location "mid" in "Children"
		string VariableOfMidMonom;
		bool VariableFound = findVariableOfMonom(Children[mid], VariableOfMidMonom, em);
		if(!VariableFound)	
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! error in finding variable in function binarySearch in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else
		{
			// get index of this variable
			int IndexOfVariableOfMidMonom = getVariableIndex(VariableOfMidMonom, VariableList);

			assert(IndexOfVariableOfMidMonom >= 0);

			if (key > IndexOfVariableOfMidMonom) 
			{
				first = mid + 1;  // repeat search in top half
			}
			else if (key < IndexOfVariableOfMidMonom)
			{
				last = mid - 1; // repeat search in bottom half
			}
			else
			{
				MonomLocation = mid;     // found it. return position /////
				return true;
			}
		}
	}//while ends here

	MonomLocation = -1; // failed to find key
	return true;   

}



// Given a monom, i.e. "bvmul" node, this function finds the variable of the monom. 
// Returns false in case of errors; true otherwise. 
bool findVariableOfMonom(t_Expression* monom, string &VariableOfMonom, t_ExpressionManager *em)
{
	if(monom == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! monom is NULL in function findVariableOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("bvmul" != em->getLabelOfExpression(monom))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findVariableOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		t_Expression* VariableNode = getIthChild(monom, 1, em);// get the second child

		assert(VariableNode != NULL);

		if(isBVVariable(VariableNode, em))
		{
			VariableOfMonom = em->getLabelOfExpression(VariableNode);
			return true;
		}
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! second child of bvmul node is not variable in function findVariableOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

	}// else of else if("bvmul" != em->getLabelOfExpression(monom)) ends here
}//function ends here



// Given a monom, i.e. "bvmul" node, this function finds the coefficient of the monom as a bvatom.
// Returns false in case of errors; true otherwise. 
bool findCoefficientOfMonom(t_Expression* monom, bvatom &CoefficientOfMonom, t_ExpressionManager *em, BVManager* bvm)
{
	if(monom == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! monom is NULL in function findCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("bvmul" != em->getLabelOfExpression(monom))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		t_Expression* ConstantNode = getIthChild(monom, 0, em);// get the first child

		assert(ConstantNode != NULL);

		if(isBVConstant(ConstantNode, em))
		{
			string Coefficient = em->getLabelOfExpression(ConstantNode);
			// recall that Coefficient is a (zero-padded) binary string starting with "0b";
			// hence the following code will suffice to create the bvatom

			Coefficient = Coefficient.substr(2); //we need characters from position 2 to end
			CoefficientOfMonom = bvm->getBVatom(Coefficient.size(), Coefficient);
			return true;
		}
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! first child of bvmul node is not constant in function findCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

	}// else of else if("bvmul" != em->getLabelOfExpression(monom)) ends here
}//function ends here



// Given a monom, i.e. "bvmul" node, this function finds the variable and the 
// coefficient of the variable in the monom. Returns false in case of errors; true otherwise. 
bool findVariableAndCoefficientOfMonom(t_Expression* monom, string &VariableOfMonom, bvatom &CoefficientOfMonom, t_ExpressionManager *em, BVManager* bvm)
{
	if(monom == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! monom is NULL in function findVariableAndCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("bvmul" != em->getLabelOfExpression(monom))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findVariableAndCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		vector <t_Expression*> Children = em->getVectorOfOperands(monom); 

		if(Children.size() != 2)
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! number of children of bvmul node is not two in function findVariableAndCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

		t_Expression* ConstantNode = Children[0];// get the first child
		t_Expression* VariableNode = Children[1];// get the second child

		assert(ConstantNode != NULL);
		assert(VariableNode != NULL);

		if(!isBVConstant(ConstantNode, em))
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! first child of bvmul node is not constant in function findVariableAndCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else if(!isBVVariable(VariableNode, em))
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! second child of bvmul node is not variable in function findVariableAndCoefficientOfMonom in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else
		{
			VariableOfMonom = em->getLabelOfExpression(VariableNode);
			
			string Coefficient = em->getLabelOfExpression(ConstantNode);
			// recall that Coefficient is a (zero-padded) binary string starting with "0b"; 
			// hence the following code will suffice to create the bvatom

			Coefficient = Coefficient.substr(2); //we need characters from position 2 to end
			CoefficientOfMonom = bvm->getBVatom(Coefficient.size(), Coefficient);
			return true;

		}// else of else if(!isBVVariable(VariableNode, em)) ends here

	}// else of else if("bvmul" != em->getLabelOfExpression(monom)) ends here

}//function ends here




// Given a "kadd" node c_0 + c_1.x_1 + ... +c_n.x_n and variables_to_exclude as say {x_i, x_{i+1}}, this 
// function returns Constant = c_0 and CoefficientMap = vector < (x_1, c_1), ... ,(x_{i-1}, c_{i-1}), (x_{i+2}, c_{i+2}), ..., (x_n, c_n) >
// i.e. CoefficientMap has all coefficients and variables except those in variables_to_exclude. 
// Returns false in case of errors; true otherwise. 
bool getKaddNodeAsCoefficientMapExcludingGivenVariables(t_Expression* kaddNode, const set<string> &variables_to_exclude, bvatom &Constant, vector< pair< string, bvatom > > &CoefficientMap, t_ExpressionManager *em, BVManager* bvm)
{
	if(kaddNode == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! kaddNode is NULL in function getKaddNodeAsCoefficientMapExcludingGivenVariables in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("kadd" != em->getLabelOfExpression(kaddNode))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function getKaddNodeAsCoefficientMapExcludingGivenVariables in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		vector <t_Expression*> Children = em->getVectorOfOperands(kaddNode); 
		
		if(Children.size() == 0)
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! kaddNode with no children in function getKaddNodeAsCoefficientMapExcludingGivenVariables in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else
		{	
			// the first child can be a constant. check it, process it.
			int index = 0;

			assert(Children[index] != NULL);

			if(isBVConstant(Children[index], em))	
			{
				// obtain the label of Children[0] as bvatom: this is the constant on LHS i.e. c_0
				string ConstantString = em->getLabelOfExpression(Children[index]);
				ConstantString = ConstantString.substr(2); //we need characters from position 2 to end: avoiding the initial "0b"
				Constant = bvm->getBVatom(ConstantString.size(), ConstantString);
				// We have c_0 now
				index++; //first child is processed now				

			}// if(isBVConstant(Children[index], em)) ends here
			else // no constant part. we need to set Constant to zero
			{
				int WidthOfKaddNode = em->getWidth(kaddNode);
				string ZeroString = getZeroBinaryStringOfGivenLength(WidthOfKaddNode);

				Constant = bvm->getBVatom(WidthOfKaddNode, ZeroString);
			}

			// Now Children[index ... size-1] is a vector of monoms

			CoefficientMap.clear();// Let's clear the map any way to begin with

			for(; index < Children.size(); index++)
			{
				t_Expression* Child = Children[index];

				assert(Child != NULL);
				
				// find the variable and the coefficient of monom
				string VariableOfMonom;
				bvatom CoefficientOfMonom;
				findVariableAndCoefficientOfMonom(Child, VariableOfMonom, CoefficientOfMonom, em, bvm);

				//if variable of monom \notin variables_to_exclude, then only enter it into the map
				if(variables_to_exclude.find(VariableOfMonom) == variables_to_exclude.end())
				{
					CoefficientMap.push_back(make_pair(VariableOfMonom, CoefficientOfMonom));
				}
			}// for loop ends here

			return true;
				
		}//else of if(Children.size() == 0) ends here

	}//else of if("kadd" != em->getLabelOfExpression(kaddNode)) ends here	

}//function ends here



// function to bvmul each coefficient in coefficient map source_map by multiplier, 
// and return the new coefficient map in destination_map
bool scalarMultiplication(const vector< pair< string, bvatom > > &source_map, bvatom multiplier, vector< pair< string, bvatom > > &destination_map, BVManager* bvm)
{
	int source_map_size = source_map.size();
	for(int i = 0; i < source_map_size; i++)
		{
			string variable = source_map[i].first;
			bvatom coefficient = source_map[i].second;
			bvatom multiplied_coefficient = bvm->bvmul(multiplier, coefficient);

			destination_map.push_back(make_pair(variable, multiplied_coefficient));
			// note that this may create zero coefficients; they will be avoided 
			// while creating the "kadd" node
		}	
	
	return true;	
}



// function to find the additive inverse of each coefficient in coefficient map source_map, 
// and return the new coefficient map involving the additive inverses in destination_map
bool additiveInverse(const vector< pair< string, bvatom > > &source_map, vector< pair< string, bvatom > > &destination_map, BVManager* bvm)
{
	int source_map_size = source_map.size();
	for(int i = 0; i < source_map_size; i++)
		{
			string variable = source_map[i].first;
			bvatom coefficient = source_map[i].second;
			bvatom inversed_coefficient = bvm->addInverse(coefficient);

			destination_map.push_back(make_pair(variable, inversed_coefficient));
		}	
	
	return true;	
}



// function to left shift each coefficient in coefficient map source_map by shift, 
// and return the new coefficient map in destination_map
bool leftShift(const vector< pair< string, bvatom > > &source_map, int shift, vector< pair< string, bvatom > > &destination_map, BVManager* bvm)
{
	int source_map_size = source_map.size();
	for(int i = 0; i < source_map_size; i++)
		{
			string variable = source_map[i].first;
			bvatom coefficient = source_map[i].second;
			bvatom shifted_coefficient = bvm->bvlshift(coefficient, shift);

			destination_map.push_back(make_pair(variable, shifted_coefficient));
			// note that this may create zero coefficients; they will be avoided 
			// while creating the "kadd" node
		}	
	
	return true;	
}



// function to add two coefficient maps, and return the result in destination_map
bool addition(const vector< pair< string, bvatom > > &first_source_map, const vector< pair< string, bvatom > > &second_source_map, vector< pair< string, bvatom > > &destination_map, BVManager* bvm, t_HashTable <string, int> &VariableList)
{
	int i = 0;
	int j = 0;
	int first_map_size = first_source_map.size();
	int second_map_size = second_source_map.size();
	
	while(i < first_map_size && j < second_map_size)
		{
			// recall that the maps are sorted
			string first_variable = first_source_map[i].first;
			bvatom first_coefficient = first_source_map[i].second;

			string second_variable = second_source_map[j].first;
			bvatom second_coefficient = second_source_map[j].second;

			int first_index = getVariableIndex(first_variable, VariableList); 			
			int second_index = getVariableIndex(second_variable, VariableList); 

			if(first_index < second_index)//first_variable lower in the order, pop it
			{
				destination_map.push_back(make_pair(first_variable, first_coefficient));		
				i++;
			}
			else if(second_index < first_index)//second_variable lower in the order, pop it
			{
				destination_map.push_back(make_pair(second_variable, second_coefficient));		
				j++;
			}
			else //both variables same in the order, add them, pop both
			{
				bvatom added_coefficient = bvm->bvadd(first_coefficient, second_coefficient);
				destination_map.push_back(make_pair(first_variable, added_coefficient));
				// note that this may create zero coefficients; they will be avoided 
				// while creating the "kadd" node		
				i++;
				j++;
			}
		}//while ends here

	while(i < first_map_size)//just copy
		{
			string variable = first_source_map[i].first;
			bvatom coefficient = first_source_map[i].second;
			destination_map.push_back(make_pair(variable, coefficient));		
			i++;
		}	

	while(j < second_map_size)//just copy
		{
			string variable = second_source_map[j].first;
			bvatom coefficient = second_source_map[j].second;
			destination_map.push_back(make_pair(variable, coefficient));		
			j++;
		}	
	
	return true;	
}




// displays the coefficient map on screen
bool displayCoefficientMapOnScreen(const bvatom &Constant, const vector< pair< string, bvatom > > &CoefficientMap, BVManager* bvm)
{
	cout << endl <<"Constant = " << bvm->printBVasBinString(Constant) << endl;

	cout << endl << "CoefficientMap" << endl;
	
	for(int i = 0; i < CoefficientMap.size(); i++)
	{
		cout << CoefficientMap[i].first << "\t" << bvm->printBVasBinString(CoefficientMap[i].second) << endl;
	}	
	
	return true;
}




// displays a set of expressions on screen
bool displaySetOfExpressionsOnScreen(const string &WhoAmI, const set<t_Expression*> &ExpressionSet, t_ExpressionManager *em)
{
	cout << endl << WhoAmI << endl;
	
	for(set<t_Expression*>::iterator it = ExpressionSet.begin(); it != ExpressionSet.end(); it++)
	{
		em->printExpressionToFileAsDAG("*it ", *it, cout);
	}	
	
	return true;
}



// displays a set of strings on screen
bool displaySetOfStringsOnScreen(const string &WhoAmI, const set<string> &StringSet)
{
	cout << endl << WhoAmI << endl;
	
	for(set<string>::iterator it = StringSet.begin(); it != StringSet.end(); it++)
	{
		cout << *it << endl;
	}	
	
	return true;
}



// displays a vector of strings on screen
bool displayVectorOfStringsOnScreen(const string &WhoAmI, const vector<string> &StringVector)
{
	cout << endl << WhoAmI << endl;
	
	for(int i = 0; i < StringVector.size(); i++)
	{
		cout << StringVector[i] << endl;
	}	
	
	return true;
}


// Given a constraint (equation/disequation/inequation) and a variable, 
// Returns true if the constraint is free of variable; false otherwise. 
bool constraintFreeOfVariable(t_Expression* Constraint, const string &variable, t_ExpressionManager *em, t_HashTable <string, int> &VariableList)
{

	assert(Constraint != NULL);
	
	string ConstraintLabel = em->getLabelOfExpression(Constraint);
	assert("eqz" == ConstraintLabel || "diseqz" == ConstraintLabel || "leq" == ConstraintLabel);


	if("eqz" == ConstraintLabel || "diseqz" == ConstraintLabel)
	//if Constraint  is equation or disequation
	{			
		// get the kadd node
		t_Expression* kaddNode = getIthChild(Constraint, 0, em);

		assert(kaddNode != NULL);

		t_Expression* MonomWithVariable;
		bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, em, VariableList);

		assert(MonomFound);

		if(MonomWithVariable == NULL) 
		//kaddNode is free of variable, i.e. (dis)equation is free of variable
		{
			return true;
		}
		else 
		//kaddNode contains variable, i.e. (dis)equation contains variable
		{
			return false;
		}

	} //if Constraint is equation or disequation ends here
	else// if Constraint is inequation
	{
		// get the kadd nodes
		t_Expression* LHSOfLeqNode = getIthChild(Constraint, 0, em);// get the first child
		t_Expression* RHSOfLeqNode = getIthChild(Constraint, 1, em);// get the second child

		assert(LHSOfLeqNode != NULL);
		assert(RHSOfLeqNode != NULL);

		t_Expression* MonomWithVariableOnLHS;
		bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, em, VariableList);

		assert(LHSMonomFound);
	
		if(MonomWithVariableOnLHS != NULL) 
		//lhs contains variable, i.e. inequation contains variable
		{
			return false;
		}
		else 
		//lhs is free of variable
		{
			t_Expression* MonomWithVariableOnRHS;
			bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, em, VariableList);

			assert(RHSMonomFound);
			
			if(MonomWithVariableOnRHS != NULL) 
			//rhs contains variable, i.e. inequation contains variable
			{
				return false;
			}
			else 
			// rhs is also free of variable, i.e. inequation is free of variable
			{
				return true;
			}
		}//lhs is free of variable ends here
				
	}//if Constraint is inequation ends here
	
}



// Given a constraint (equation/disequation/inequation), this function finds the support of the constraint.
// Returns false in case of errors; true otherwise.
bool findSupportOfConstraint(t_Expression* Constraint, set<string> &SupportOfConstraint, t_ExpressionManager *em)
{

	assert(Constraint != NULL);
	
	string ConstraintLabel = em->getLabelOfExpression(Constraint);
	assert("eqz" == ConstraintLabel || "diseqz" == ConstraintLabel || "leq" == ConstraintLabel);

	SupportOfConstraint.clear();

	if("eqz" == ConstraintLabel || "diseqz" == ConstraintLabel)
	//if Constraint  is equation or disequation
	{			
		// get the kadd node
		t_Expression* kaddNode = getIthChild(Constraint, 0, em);
		assert(kaddNode != NULL);
		
		// support of equation or disequation = support of kadd node below it
		bool SupportOfKaddNodeFound = findSupportOfKaddNode(kaddNode, SupportOfConstraint, em);
		assert(SupportOfKaddNodeFound);

	} //if Constraint is equation or disequation ends here
	else// if Constraint is inequation
	{
		// get the kadd nodes
		t_Expression* LHSOfLeqNode = getIthChild(Constraint, 0, em);// get the first child
		t_Expression* RHSOfLeqNode = getIthChild(Constraint, 1, em);// get the second child
		assert(LHSOfLeqNode != NULL);
		assert(RHSOfLeqNode != NULL);

		// support of inequation = union of supports of kadd node children 
		set<string> SupportOfLHS;
		bool SupportOfLHSFound = findSupportOfKaddNode(LHSOfLeqNode, SupportOfLHS, em);
		assert(SupportOfLHSFound);

		set<string> SupportOfRHS;
		bool SupportOfRHSFound = findSupportOfKaddNode(RHSOfLeqNode, SupportOfRHS, em);
		assert(SupportOfRHSFound);
				
		set_union(SupportOfLHS.begin(), SupportOfLHS.end(), SupportOfRHS.begin(), SupportOfRHS.end(),inserter(SupportOfConstraint, SupportOfConstraint.begin()));

	}//if Constraint is inequation ends here

	return true;	
}




// Given a kadd node, this function finds the support of the kadd node.
// Returns false in case of errors; true otherwise.
bool findSupportOfKaddNode(t_Expression* kaddNode, set<string> &SupportOfKaddNode, t_ExpressionManager *em)
{
	assert(kaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(kaddNode));
	
	SupportOfKaddNode.clear();

	vector <t_Expression*> Children = em->getVectorOfOperands(kaddNode); 

	assert(Children.size() > 0);
	assert(Children[0] != NULL);
		
	if(isBVConstant(Children[0], em)) //constant child exists	
	{
		if(Children.size() == 1) //we have only one child which is a constant
		{
			return true;
		}
		else
		{
			Children.erase (Children.begin());				
		}
	}

	int children_size = Children.size();
	for(int i = 0; i < children_size; i++)
	{
		assert(Children[i] != NULL);
		t_Expression* monom = Children[i];

		string VariableOfMonom;		
		bool VariableFound = findVariableOfMonom(monom, VariableOfMonom, em);
		assert(VariableFound);

		SupportOfKaddNode.insert(VariableOfMonom);
	}
	
	return true;
}//function ends here





// Given a "kand" node and a variable, 
// obtain the equations with the variable in E_x, equations without the variable in E_neg_x,
//	      disequations with the variable in D_x, disequations without the variable in D_neg_x,
//	      inequations with the variable in I_x, inequations without the variable in I_neg_x
bool findFreeAndBoundConstraintsFromKandNode(t_Expression* kandNode, const string &variable, set<t_Expression*> &E_x, set<t_Expression*> &D_x, set<t_Expression*> &I_x, set<t_Expression*> &E_neg_x, set<t_Expression*> &D_neg_x, set<t_Expression*> &I_neg_x, t_ExpressionManager *em, t_HashTable <string, int> &VariableList)
{
	if(kandNode == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! kandNode is NULL in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else if("kand" != em->getLabelOfExpression(kandNode))
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unexpected node encountered in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else
	{
		vector <t_Expression*> Children = em->getVectorOfOperands(kandNode);

		for(int i = 0; i < Children.size(); i++)// take each child
		{
			t_Expression* Child = Children[i];

			assert(Child != NULL);

			if("eqz" == em->getLabelOfExpression(Child))//if child is equation
			{			
				// get the kadd node
				t_Expression* kaddNode = getIthChild(Child, 0, em);

				assert(kaddNode != NULL);

				t_Expression* MonomWithVariable;
				bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, em, VariableList);

				if(!MonomFound)
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;
				}
				else if(MonomWithVariable == NULL) 
				//kaddNode is free of variable, i.e. Child is free of variable
				{
					//insert Child into E_neg_x
					E_neg_x.insert(Child);
				}
				else 
				//kaddNode contains variable, i.e. Child contains variable
				{
					//insert Child into E_x
					E_x.insert(Child);
				}

			}//if child is equation ends here
			else if("diseqz" == em->getLabelOfExpression(Child))// if child is disequation
			{
				// get the kadd node
				t_Expression* kaddNode = getIthChild(Child, 0, em);

				assert(kaddNode != NULL);

				t_Expression* MonomWithVariable;
				bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, em, VariableList);

				if(!MonomFound)
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;
				}
				else if(MonomWithVariable == NULL) 
				//kaddNode is free of variable, i.e. Child is free of variable
				{
					//insert Child into D_neg_x
					D_neg_x.insert(Child);
				}
				else 
				//kaddNode contains variable, i.e. Child contains variable
				{
					//insert Child into D_x
					D_x.insert(Child);
				}
			
			}//if child is disequation ends here
			else if("leq" == em->getLabelOfExpression(Child))// if child is inequation
			{
				// get the kadd nodes
				t_Expression* LHSOfLeqNode = getIthChild(Child, 0, em);// get the first child
				t_Expression* RHSOfLeqNode = getIthChild(Child, 1, em);// get the second child

				assert(LHSOfLeqNode != NULL);
				assert(RHSOfLeqNode != NULL);

				t_Expression* MonomWithVariableOnLHS;
				bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, em, VariableList);

				if(!LHSMonomFound)
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;
				}
				else if(MonomWithVariableOnLHS != NULL) 
				//lhs contains variable, i.e. Child contains variable
				{
					//insert Child into I_x
					I_x.insert(Child);
				}
				else 
				//lhs is free of variable
				{
					t_Expression* MonomWithVariableOnRHS;
					bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, em, VariableList);

					if(!RHSMonomFound)
					{
						t_Logger* logManager = t_Logger::getInstance();
						ofstream *logFile = new ofstream();
						logFile->open("ExpressionMisc.log");
						logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
						logFile->close();
						return false;
					}
					else if(MonomWithVariableOnRHS != NULL) 
					//rhs contains variable, i.e. Child contains variable
					{
						//insert Child into I_x
						I_x.insert(Child);
					}
					else 
					// rhs is also free of variable, i.e. Child is free of variable
					{
						I_neg_x.insert(Child);
					}
				}
				
			}//if child is inequation ends here
			else
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function findFreeAndBoundConstraintsFromKandNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}

		}// for each child ends here

		return true;
	}// else of if (!kandNode) ends here
}// function ends here





// Given a set of constraints and variable, 
// obtain the equations with variable in E_x, equations without variable in E_neg_x,
//	      disequations with variable in D_x, disequations without variable in D_neg_x,
//	      inequations with variable in I_x, inequations without variable in I_neg_x
bool findFreeAndBoundConstraintsFromSet(const set<t_Expression*> &Constraints, const string &variable, set<t_Expression*> &E_x, set<t_Expression*> &D_x, set<t_Expression*> &I_x, set<t_Expression*> &E_neg_x, set<t_Expression*> &D_neg_x, set<t_Expression*> &I_neg_x, t_ExpressionManager *em, t_HashTable <string, int> &VariableList)
{
	
	for(set<t_Expression*>::iterator it = Constraints.begin(); it != Constraints.end(); it++) // take each constraint
	{	
		t_Expression* Constraint = *it;

		assert(Constraint != NULL);

		if("eqz" == em->getLabelOfExpression(Constraint))//if constraint is equation
		{			
			// get the kadd node
			t_Expression* kaddNode = getIthChild(Constraint, 0, em);

			assert(kaddNode != NULL);

			t_Expression* MonomWithVariable;
			bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, em, VariableList);

			if(!MonomFound)
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromSet in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}
			else if(MonomWithVariable == NULL) 
			//kaddNode is free of variable, i.e. Constraint is free of variable
			{
				//insert Constraint into E_neg_x
				E_neg_x.insert(Constraint);
			}
			else 
			//kaddNode contains variable, i.e. Constraint contains variable
			{
				//insert Constraint into E_x
				E_x.insert(Constraint);
			}

		}//if constraint is equation ends here
		else if("diseqz" == em->getLabelOfExpression(Constraint))// if constraint is disequation
		{
			// get the kadd node
			t_Expression* kaddNode = getIthChild(Constraint, 0, em);

			assert(kaddNode != NULL);

			t_Expression* MonomWithVariable;
			bool MonomFound = findMonomOfKaddNodeWithGivenVariable(kaddNode, variable, MonomWithVariable, em, VariableList);

			if(!MonomFound)
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromSet in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}
			else if(MonomWithVariable == NULL) 
			//kaddNode is free of variable, i.e. Constraint is free of variable
			{
				//insert Constraint into D_neg_x
				D_neg_x.insert(Constraint);
			}
			else 
			//kaddNode contains variable, i.e. Constraint contains variable
			{
				//insert Child into D_x
				D_x.insert(Constraint);
			}
			
		}//if constraint is disequation ends here
		else if("leq" == em->getLabelOfExpression(Constraint))// if constraint is inequation
		{
			// get the kadd nodes
			t_Expression* LHSOfLeqNode = getIthChild(Constraint, 0, em);// get the first child
			t_Expression* RHSOfLeqNode = getIthChild(Constraint, 1, em);// get the second child

			assert(LHSOfLeqNode != NULL);
			assert(RHSOfLeqNode != NULL);

			t_Expression* MonomWithVariableOnLHS;
			bool LHSMonomFound = findMonomOfKaddNodeWithGivenVariable(LHSOfLeqNode, variable, MonomWithVariableOnLHS, em, VariableList);

			if(!LHSMonomFound)
			{
				t_Logger* logManager = t_Logger::getInstance();
				ofstream *logFile = new ofstream();
				logFile->open("ExpressionMisc.log");
				logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromSet in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
				logFile->close();
				return false;
			}
			else if(MonomWithVariableOnLHS != NULL) 
			//lhs contains variable, i.e. Constraint contains variable
			{
				//insert Constraint into I_x
				I_x.insert(Constraint);
			}
			else 
			//lhs is free of variable
			{
				t_Expression* MonomWithVariableOnRHS;
				bool RHSMonomFound = findMonomOfKaddNodeWithGivenVariable(RHSOfLeqNode, variable, MonomWithVariableOnRHS, em, VariableList);

				if(!RHSMonomFound)
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!! monom finding error in function findFreeAndBoundConstraintsFromSet in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;
				}
				else if(MonomWithVariableOnRHS != NULL) 
				//rhs contains variable, i.e. Constraint contains variable
				{
					//insert Constraint into I_x
					I_x.insert(Constraint);
				}
				else 
				// rhs is also free of variable, i.e. Constraint is free of variable
				{
					I_neg_x.insert(Constraint);
				}
			}
				
		}//if constraint is inequation ends here
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function findFreeAndBoundConstraintsFromSet in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

	}// for each constraint ends here

	return true;
}// function ends here





// Version of findFreeAndBoundConstraintsFromKandNode which works for multiple variables.
// i.e. Given a "kand" node and a set of variables X, 
// obtain the equations with variables in X in E_X, equations without variables in X in E_neg_X,
//	      disequations with variables in X in D_X, disequations without variables in X in D_neg_X,
//	      inequations with variables in X in I_X, inequations without variables in X in I_neg_X. 
// Also, common_variables_in_kandNode = X \intersection support of kand node.
bool findFreeAndBoundConstraintsFromKandNodeForMultipleVariables(t_Expression* kandNode, const set<string> &variables, set<t_Expression*> &E_X, set<t_Expression*> &D_X, set<t_Expression*> &I_X, set<t_Expression*> &E_neg_X, set<t_Expression*> &D_neg_X, set<t_Expression*> &I_neg_X, set<string> &common_variables_in_kandNode,  t_ExpressionManager *em)
{
	assert(kandNode != NULL);
	assert("kand" == em->getLabelOfExpression(kandNode));

	common_variables_in_kandNode.clear();
	
	vector <t_Expression*> Children = em->getVectorOfOperands(kandNode);

	for(int i = 0; i < Children.size(); i++)// take each child
	{
		t_Expression* Constraint = Children[i];
		assert(Constraint != NULL);

		set<string> SupportOfConstraint;
		bool SupportFound = findSupportOfConstraint(Constraint, SupportOfConstraint, em);	
		assert(SupportFound);

		set<string> CommonVariables;
		set_intersection(variables.begin(), variables.end(), SupportOfConstraint.begin(), SupportOfConstraint.end(),inserter(CommonVariables, CommonVariables.begin()));

		set_union(common_variables_in_kandNode.begin(), common_variables_in_kandNode.end(), CommonVariables.begin(), CommonVariables.end(),inserter(common_variables_in_kandNode, common_variables_in_kandNode.begin()));		

		if("eqz" == em->getLabelOfExpression(Constraint))//if constraint is equation
		{			
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				E_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				E_X.insert(Constraint);
			}

		}//if constraint is equation ends here
		else if("diseqz" == em->getLabelOfExpression(Constraint))// if constraint is disequation
		{
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				D_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				D_X.insert(Constraint);
			}
			
		}//if constraint is disequation ends here
		else if("leq" == em->getLabelOfExpression(Constraint))// if constraint is inequation
		{
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				I_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				I_X.insert(Constraint);
			}
				
		}//if constraint is inequation ends here
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function findFreeAndBoundConstraintsFromKandNodeForMultipleVariables in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

	}// for each child ends here

	return true;
}// function ends here





// Version of findFreeAndBoundConstraintsFromSet which works for multiple variables.
// i.e. Given a set of constraints and a set of variables X, 
// obtain the equations with variables in X in E_X, equations without variables in X in E_neg_X,
//	      disequations with variables in X in D_X, disequations without variables in X in D_neg_X,
//	      inequations with variables in X in I_X, inequations without variables in X in I_neg_X
bool findFreeAndBoundConstraintsFromSetForMultipleVariables(const set<t_Expression*> &Constraints, const set<string> &variables, set<t_Expression*> &E_X, set<t_Expression*> &D_X, set<t_Expression*> &I_X, set<t_Expression*> &E_neg_X, set<t_Expression*> &D_neg_X, set<t_Expression*> &I_neg_X, t_ExpressionManager *em)
{
	
	for(set<t_Expression*>::iterator it = Constraints.begin(); it != Constraints.end(); it++) // take each constraint
	{	
		t_Expression* Constraint = *it;
		assert(Constraint != NULL);

		set<string> SupportOfConstraint;
		bool SupportFound = findSupportOfConstraint(Constraint, SupportOfConstraint, em);	
		assert(SupportFound);

		set<string> CommonVariables;
		set_intersection(variables.begin(), variables.end(), SupportOfConstraint.begin(), SupportOfConstraint.end(),inserter(CommonVariables, CommonVariables.begin()));		

		if("eqz" == em->getLabelOfExpression(Constraint))//if constraint is equation
		{			
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				E_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				E_X.insert(Constraint);
			}

		}//if constraint is equation ends here
		else if("diseqz" == em->getLabelOfExpression(Constraint))// if constraint is disequation
		{
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				D_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				D_X.insert(Constraint);
			}
			
		}//if constraint is disequation ends here
		else if("leq" == em->getLabelOfExpression(Constraint))// if constraint is inequation
		{
			if(CommonVariables.empty()) // support(Constraint) \intersection variables = empty
			{
				I_neg_X.insert(Constraint);
			}
			else // support(Constraint) \intersection variables != empty
			{
				I_X.insert(Constraint);
			}
				
		}//if constraint is inequation ends here
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unexpected node encountered as child of kand node in function findFreeAndBoundConstraintsFromSetForMultipleVariables in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}

	}// for each constraint ends here

	return true;
}// function ends here



// Given \exists X. alpha_kand where alpha_kand is a kand node and X is a vector of variables, 
// this function expresses it as free_kand \wedge \exists Y. bound_kand, where 
// free_kand, bound_kand are either true or kand nodes and Y is a vector of variables s.t. Y \subseteq X. 
bool scopeReduction(t_Expression* alpha_kand, const vector<string> &X, t_Expression* &free_kand, vector<string> &Y, t_Expression* &bound_kand, t_ExpressionManager *em)
{	
	assert(alpha_kand != NULL);
	assert("kand" == em->getLabelOfExpression(alpha_kand));
	
	set<t_Expression*> E_X, E_neg_X;
	set<t_Expression*> D_X, D_neg_X;
	set<t_Expression*> I_X, I_neg_X;

	set<string> variables_common_between_X_and_alpha_kand;
	set<string> variables(X.begin(), X.end());

	bool ConstraintsFound = findFreeAndBoundConstraintsFromKandNodeForMultipleVariables(alpha_kand, variables, E_X, D_X, I_X, E_neg_X, D_neg_X, I_neg_X, variables_common_between_X_and_alpha_kand, em);
	assert(ConstraintsFound);

	// create free_kand and bound_kand
	
	if(E_neg_X.empty()  && D_neg_X.empty() && I_neg_X.empty())
	{
		free_kand = getTrue(em);		
	}
	else
	{
		free_kand = CreateKandNode(E_neg_X, D_neg_X, I_neg_X, em);
	}
	assert(free_kand != NULL);

	if(E_X.empty()  && D_X.empty() && I_X.empty())
	{
		bound_kand = getTrue(em);
	}
	else
	{
		bound_kand = CreateKandNode(E_X, D_X, I_X, em);
	}
	assert(bound_kand != NULL);

	copy(variables_common_between_X_and_alpha_kand.begin(), variables_common_between_X_and_alpha_kand.end(), inserter(Y, Y.end()));	

	return true;
}


// Function to evaluate a kadd node using the map "Model" between variables and values.
// Note that each value is a binary string of size same as the width of corresponding variable.
// Sets result to the evaluated value.
// Returns false in case of errors; true otherwise.
bool evaluateKaddNode(t_Expression* kaddNode, map<string, string> &Model, bvatom &result, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &WidthTable)
{
	assert(kaddNode != NULL);
	assert("kadd" == em->getLabelOfExpression(kaddNode));

	bvatom ConstantOfKaddNode; //this is c_0
	vector< pair< string, bvatom > > CoefficientMapOfKaddNode; 
	// this is vector < x_1-->c_1,..., x_n-->c_n >

	set<string> variables_to_exclude;
	bool CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(kaddNode, variables_to_exclude, ConstantOfKaddNode, CoefficientMapOfKaddNode, em, bvm);
					
	if(!CoefficientMapFound)// error in finding coefficient map; propogate it
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! error in finding coefficient map in function evaluateKaddNode in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
	else // constant part and coefficient map of kadd node found correctly
	{
		// suppose Model is < x_1-->v_1,...,x_m-->v_m >
		// result should be c_0 + c_1.v_1 + ... + c_n.v_n

		result = ConstantOfKaddNode; // result initialized to c_0
		
		int map_size = CoefficientMapOfKaddNode.size();
		for(int i = 0; i < map_size; i++)
		{
			string variable = CoefficientMapOfKaddNode[i].first; // x_i
			bvatom coefficient = CoefficientMapOfKaddNode[i].second; // c_i

			int variable_width = getWidthOfVariable(variable, WidthTable); // width of x_i

			// let's obtain v_i 
			map<string, string>::iterator model_it = Model.find(variable);
			assert(model_it != Model.end()); // Model should contain v_i
			string value_string = model_it->second; 
			assert(variable_width == value_string.size()); // length of v_i should be same as width of x_i
			bvatom value = bvm->getBVatom(variable_width, value_string); // v_i

			result = bvm->bvadd(result, bvm->bvmul(coefficient, value)); // result = result + c_i * v_i
		}
		return true;		
	}
}// function ends here




// Function to evaluate an "eqz", "diseqz", or "leq" node using the map "Model" between variables and values.
// Note that each value is a binary string of size same as the width of corresponding variable.
// Sets result to true if the node evaluates to true; to false if the node evaluates to false.
// Returns false in case of errors; true otherwise.
bool evaluateLMC(t_Expression* constraintNode, map<string, string> &Model, bool &result, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &WidthTable)
{
	assert(constraintNode != NULL);
	
	if("eqz" == em->getLabelOfExpression(constraintNode)) // if constraint is eqz
	{
		t_Expression* kaddNode = getIthChild(constraintNode, 0, em); // get the kadd node 
		
		bvatom result_kaddnode;
		// evaluate the kadd node using Model
		bool result_kaddnode_found = evaluateKaddNode(kaddNode, Model, result_kaddnode, em, bvm, WidthTable);
		assert(result_kaddnode_found);

		if(bvm->checkBVForZero(result_kaddnode)) // result of evaluating the kadd node == 0; hence eqz node evaluates to true
		{
			result = true;
		}
		else // result of evaluating the kadd node != 0; hence eqz node evaluates to true
		{
			result = false;
		}
		
		return true;
	}
	else if("diseqz" == em->getLabelOfExpression(constraintNode)) // if constraint is diseqz
	{
		t_Expression* kaddNode = getIthChild(constraintNode, 0, em); // get the kadd node 
		
		bvatom result_kaddnode;
		// evaluate the kadd node using Model
		bool result_kaddnode_found = evaluateKaddNode(kaddNode, Model, result_kaddnode, em, bvm, WidthTable);
		assert(result_kaddnode_found);

		if(bvm->checkBVForZero(result_kaddnode)) // result of evaluating the kadd node == 0; hence eqz node evaluates to false
		{
			result = false;
		}
		else // result of evaluating the kadd node != 0; hence eqz node evaluates to true
		{
			result = true;
		}

		return true;
	}
	else if("leq" == em->getLabelOfExpression(constraintNode)) // if constraint is leq
	{
		t_Expression* lhs = getIthChild(constraintNode, 0, em); // get the lhs
		t_Expression* rhs = getIthChild(constraintNode, 1, em); // get the rhs
		
		bvatom result_lhs;
		// evaluate lhs using Model
		bool result_lhs_found = evaluateKaddNode(lhs, Model, result_lhs, em, bvm, WidthTable);
		assert(result_lhs_found);

		bvatom result_rhs;
		// evaluate rhs using Model
		bool result_rhs_found = evaluateKaddNode(rhs, Model, result_rhs, em, bvm, WidthTable);
		assert(result_rhs_found);

		if(bvm->checkBVGreaterThan(result_lhs, result_rhs)) // result of evaluating lhs > result of evaluating rhs; hence leq node evaluates to false
		{
			result = false;
		}
		else // result of evaluating lhs <= result of evaluating rhs; hence leq node evaluates to true
		{
			result = true;
		}

		return true;
	}
	else
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unknown operator in function evaluateLMC in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
}
	


// This function checks if F is satisfiable. 
// If F is satisfiable, then, sat is set to true and model of F is obtained.
// Otherwise, if F is unsatisfiable, then, sat is set to false.
// Returns false in case of errors; true otherwise
bool obtainModelOfFormula(t_Expression* F, bool &sat, t_solver solver, map<string, string> &model, t_ExpressionManager *em, const string &smt_file_name)
{
	model.clear(); //let's initialize model to empty

	if(solver == stp)
	{
		assert(F != NULL);
		
		// Let us obtain F in SMTLIB 2.0 format
		set<t_Expression*> ConstraintsToPrint;
		ConstraintsToPrint.insert(F);
		em->printExpressionsToFileInSMT(ConstraintsToPrint, "", smt_file_name);	

		// Let's call stp now
		string model_file_name = "model_";
		int location_of_dot = smt_file_name.find_last_of(".");
		assert(location_of_dot != string::npos);
	       	model_file_name += smt_file_name.substr(0, location_of_dot);
		model_file_name += ".txt";
		
		string command = "stp -p --SMTLIB2 ";
		command += smt_file_name;
		command += " > ";
		command += model_file_name;

		cout<<endl<<"command = "<<command<<endl;
		system(command.c_str()); //call to stp

		// read stp model file
		string result_of_check;
		bool stp_model_read = readSTPModelFile(model_file_name, result_of_check, model);
		assert(stp_model_read);
		if(result_of_check == "sat")
		{
			sat = true;
			return true;
		}
		else if(result_of_check == "unsat")
		{
			sat = false;
			return true;
		}
		else if(result_of_check == "unknown")
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unknown returned from stp in function obtainModelOfFormula in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
		else
		{
			t_Logger* logManager = t_Logger::getInstance();
			ofstream *logFile = new ofstream();
			logFile->open("ExpressionMisc.log");
			logManager->LOG("ERROR!! unexpected location reached in function obtainModelOfFormula in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
			logFile->close();
			return false;
		}
	}
	else
	{
		t_Logger* logManager = t_Logger::getInstance();
		ofstream *logFile = new ofstream();
		logFile->open("ExpressionMisc.log");
		logManager->LOG("ERROR!! unidentified solver in function obtainModelOfFormula in ExpressionMisc.cpp", logFile, c_RunLevelVerbosity);
		logFile->close();
		return false;
	}
}// function ends here



// This function reads the stp model in the file model_file_name
// If the file contains "sat" then, result_of_check is set to "sat" and model is read.
// o/w if the file contains "unsat" then, result_of_check is set to "unsat".
// o/w if the file contains "unknown" then, result_of_check is set to "unknown".
// Returns false in case of errors; true otherwise
bool readSTPModelFile(const string &model_file_name, string &result_of_check, map<string, string> &model)
{
	ifstream *model_file = new ifstream();
  	model_file->open(model_file_name.c_str()); // open the model_file
	assert(model_file->is_open());

	// Let us read the model_file
	result_of_check = "unknown";  //initialization

	// these denote the presently read word, word read prior to it, and that was read prior to the prior one
  	string word = "", prev_word = "", prev_prev_word = ""; 
	while(!model_file->eof()) //read until end of file
    	{
      		prev_prev_word = prev_word;
      		prev_word = word;
      		*model_file>>word;
      		
      		if(word == "")
		{
			break;	
		}
		else if(word == "sat" || word == "unsat" || word == "unknown")
		{
			result_of_check = word;
		}
		else if(prev_word=="=") // the pattern variable = value encountered
		{
			// prev_prev_word has variable; prev_word has =; word has value
			
			int start_pos = word.find("b"); 
			if(start_pos != string::npos) // value is binary
			{
				word  = word.substr(start_pos+1); // avoid 0b at the beginning
			}
			else
			{
				start_pos = word.find("x");
				if(start_pos != string::npos) // value is hex
				{
					word  = word.substr(start_pos+1); // avoid 0x at the beginning
					word = hexStringToBinaryString(word); // convert to binary
				}
				else
				{
					t_Logger* logManager = t_Logger::getInstance();
					ofstream *logFile = new ofstream();
					logFile->open("ExpressionMisc.log");
					logManager->LOG("ERROR!!unexpected value encountered in function readSTPModelFile in ExpressionMisc.cpp ", logFile, c_RunLevelVerbosity);
					logFile->close();
					return false;	
				}// else of if(start_pos != string::npos) ends here
			}// else of if(start_pos != string::npos) ends here

			model.insert(make_pair(prev_prev_word, word));
		}// else if(prev_word=="=") ends here
	}// while ends here
	model_file->close();
	return true; 
}


// Given an eqz node, this function returns the negation of this node (a diseqz node)
t_Expression* negateLME(t_Expression *eqzNode, t_ExpressionManager *em)
{
	assert(eqzNode != NULL);
	assert("eqz" == em->getLabelOfExpression(eqzNode));

	t_Expression* kaddNode = getIthChild(eqzNode, 0, em); // get the "kadd" node
	assert(kaddNode != NULL);

	// create the diseqz node
	string disequation_label = "diseqz";
	t_Expression* diseqzNode = CreateNode(disequation_label, kaddNode, em);
	assert(diseqzNode != NULL);

	return diseqzNode;	
}


// Given a diseqz node, this function returns the negation of this node (an eqz node)
t_Expression* negateLMD(t_Expression *diseqzNode, t_ExpressionManager *em)
{
	assert(diseqzNode != NULL);
	assert("diseqz" == em->getLabelOfExpression(diseqzNode));

	t_Expression* kaddNode = getIthChild(diseqzNode, 0, em); // get the "kadd" node
	assert(kaddNode != NULL);

	// create the eqz node
	string equation_label = "eqz";
	t_Expression* eqzNode = CreateNode(equation_label, kaddNode, em);
	assert(eqzNode != NULL);

	return eqzNode;	
}


// Given an leq node t1 <= t2, this function returns the negation of this node.
// Note that negation of t1 \leq t2 \equiv t1 > t2
// t1 > t2 \equiv (t1-1 >= t2) \wedge (t1 \neq 0)
// t1 > t2 \equiv (t1 >= t2+1) \wedge (t2 \neq 2^p-1)
// If t1 is a constant and t1 \neq 0, then, (t1-1 >= t2) is returned and NegatedLMI_LMDPart is set to NULL
// O/w, if t2 is a constant and t2 \neq 2^p-1, then, (t1 >= t2+1) is returned and NegatedLMI_LMDPart is set to NULL
// O/w, (t1 >= t2+1) is returned and NegatedLMI_LMDPart is set to (t2 \neq 2^p-1)
t_Expression* negateLMI(t_Expression *leqNode, t_Expression* &NegatedLMI_LMDPart, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable)
{
	assert(leqNode != NULL);
	assert("leq" == em->getLabelOfExpression(leqNode));

	// get t1 and t2
	vector <t_Expression*> ChildrenOfLeqNode = em->getVectorOfOperands(leqNode); 
	assert(ChildrenOfLeqNode.size() == 2);

	t_Expression* t1 = ChildrenOfLeqNode[0];
	t_Expression* t2 = ChildrenOfLeqNode[1];

	assert(t1 != NULL);
	assert(t2 != NULL);
	assert("kadd" == em->getLabelOfExpression(t1));
	assert("kadd" == em->getLabelOfExpression(t2));

	string inequation_label = "leq";
	string disequation_label = "diseqz";

	bvatom ConstantOft1; 
	vector< pair< string, bvatom > > CoefficientMapOft1; 

	set<string> variables_to_exclude;
	bool CoefficientMapOft1Found = getKaddNodeAsCoefficientMapExcludingGivenVariables(t1, variables_to_exclude, ConstantOft1, CoefficientMapOft1, em,  bvm);
	assert(CoefficientMapOft1Found);

	if(CoefficientMapOft1.size() == 0) //t1 is a constant
	{
		// we need to express t1 > t2
		
		assert(!(bvm->checkBVForZero(ConstantOft1))); // t1 != 0 (t1=0 implies that 0 > t2 i.e. false)
		
		unsigned int p = ConstantOft1.bv_width;
		string OneString = getOneBinaryStringOfGivenLength(p);
		bvatom ConstantOft1MinusOne = bvm->bvsub(ConstantOft1, bvm->getBVatom(p, OneString)); // we got t1-1

		// Let's create kadd node for t1-1
		t_Expression *t1MinusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1MinusOne, CoefficientMapOft1, em, VariableList, bvm); 
		assert(t1MinusOne != NULL);

		// Let's create t1-1 >= t2, i.e. t2 <= t1-1
		t_Expression* NegatedLMI_LMIPart = CreateNode(inequation_label, t2, t1MinusOne, em);
		assert(NegatedLMI_LMIPart != NULL);

		NegatedLMI_LMDPart = NULL;
		return NegatedLMI_LMIPart;
	}
	else // t1 is not a constant
	{
		// recall that we need to express t1 > t2

		bvatom ConstantOft2; 
		vector< pair< string, bvatom > > CoefficientMapOft2; 

		bool CoefficientMapOft2Found = getKaddNodeAsCoefficientMapExcludingGivenVariables(t2, variables_to_exclude, ConstantOft2, CoefficientMapOft2, em,  bvm);
		assert(CoefficientMapOft2Found);

		if(CoefficientMapOft2.size() == 0) //t2 is a constant
		{
			unsigned int p = ConstantOft2.bv_width;
			string OneString = getOneBinaryStringOfGivenLength(p);
			bvatom ConstantOft2PlusOne = bvm->bvadd(ConstantOft2, bvm->getBVatom(p, OneString)); // we got t2+1
			assert(!(bvm->checkBVForZero(ConstantOft2PlusOne))); // t2+1 != 0 (t2+1 = 0 implies that t2 = 2^p-1, i.e. t1 > 2^p-1)

			// Let's create kadd node for t2+1
			t_Expression *t2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2PlusOne, CoefficientMapOft2, em, VariableList, bvm); 
			assert(t2PlusOne != NULL);

			// Let's create t1 >= t2+1, i.e. t2+1 <= t1
			t_Expression* NegatedLMI_LMIPart = CreateNode(inequation_label, t2PlusOne, t1, em);
			assert(NegatedLMI_LMIPart != NULL);

			NegatedLMI_LMDPart = NULL;
			return NegatedLMI_LMIPart;
		}
		else // both t1 and t2 are not constants	
		{
			unsigned int p = ConstantOft2.bv_width;
			string OneString = getOneBinaryStringOfGivenLength(p);
			bvatom ConstantOft2PlusOne = bvm->bvadd(ConstantOft2, bvm->getBVatom(p, OneString)); // we have constant part of t2+1

			// Let's create kadd node for t2+1
			t_Expression *t2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2PlusOne, CoefficientMapOft2, em, VariableList, bvm); 
			assert(t2PlusOne != NULL);

			// Let's create t1 >= t2+1, i.e. t2+1 <= t1
			t_Expression* NegatedLMI_LMIPart = CreateNode(inequation_label, t2PlusOne, t1, em);
			assert(NegatedLMI_LMIPart != NULL);

			NegatedLMI_LMDPart = CreateNode(disequation_label, t2PlusOne, em);
			return NegatedLMI_LMIPart;
		}// both t1 and t2 are not constants ends here	
	}//else of if t1 is not a constant ends here
}//function ends here



// Given an eqz node t = 0, this function returns the equivalent LeqNode t <= 0
t_Expression* obtainEquivalentLeqNodeFromEqzNode(t_Expression *eqzNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList)
{
	assert(eqzNode != NULL);
	assert("eqz" == em->getLabelOfExpression(eqzNode));

	t_Expression* t = getIthChild(eqzNode, 0, em);
	assert(t != NULL);
	assert("kadd" == em->getLabelOfExpression(t));

	int p = em->getWidth(t);
	vector< pair< string, bvatom > > CoefficientMapOfZero;  
	string ZeroString = getZeroBinaryStringOfGivenLength(p);
	bvatom ConstantOfZero = bvm->getBVatom(p, ZeroString); 
	t_Expression *Zero = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfZero, CoefficientMapOfZero, em, VariableList, bvm);
	assert(Zero != NULL);	

	string inequation_label = "leq";
	t_Expression* LeqNode = CreateNode(inequation_label, t, Zero, em);
	assert(LeqNode != NULL);
	
	return LeqNode;
}



// Given a diseqz node t \neq 0, this function returns the equivalent LeqNode 1 <= t
t_Expression* obtainEquivalentLeqNodeFromDiseqzNode(t_Expression *diseqzNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList)
{
	assert(diseqzNode != NULL);
	assert("diseqz" == em->getLabelOfExpression(diseqzNode));

	t_Expression* t = getIthChild(diseqzNode, 0, em);
	assert(t != NULL);
	assert("kadd" == em->getLabelOfExpression(t));

	int p = em->getWidth(t);
	vector< pair< string, bvatom > > CoefficientMapOfOne;  
	string OneString = getOneBinaryStringOfGivenLength(p);
	bvatom ConstantOfOne = bvm->getBVatom(p, OneString); 
	t_Expression *One = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOfOne, CoefficientMapOfOne, em, VariableList, bvm);
	assert(One != NULL);	

	string inequation_label = "leq";
	t_Expression* LeqNode = CreateNode(inequation_label, One, t, em);
	assert(LeqNode != NULL);
	
	return LeqNode;
}




// Given a kand node, this function returns an equivalent simplified kand node.
// The simplifications applied are: 
// (a) t <= 0 ---> t = 0
// (b) 2^{p}-1 <= t ---> t = 2^{p}-1
// (c) t_1 <= t_2 \wedge t_2 <= t_1 ---> t_1 = t_2
t_Expression* simplifyKandBySynthesisOfLMEsFromLMIs(t_Expression *kandNode, t_ExpressionManager *em, BVManager *bvm, t_HashTable <string, int> &VariableList)
{
	// ensure that what we have is kandNode
	assert(kandNode != NULL);
	assert("kand" == em->getLabelOfExpression(kandNode));
	
	// disintegrate kandNode into E, D, I
	set<t_Expression*> E, D, I;
	bool ConstraintsFound = findConstraintsFromKandNode(kandNode, E, D, I, em);
	assert(ConstraintsFound);
	assert(!(E.empty() && D.empty() && I.empty()));

	if(I.empty()) // I is empty; no simplifications possible; hence return the original kandNode 
	{
		return kandNode;
	}
	else // I is non-empty
	{
		// Try to synthesize LMEs from LMIs using the aforementioned rules
		set<t_Expression*> E_from_I, Remaining_I;
		bool SynthesisDone = SynthesizeLMEsFromLMIs(I, E_from_I, Remaining_I, em, bvm, VariableList);
		assert(SynthesisDone);
		// We have I = E_from_I \union Remaining_I

		if(E_from_I.empty()) // No LMEs were synthesized from I; hence return the original kandNode
		{
			return kandNode;
		}
		else // LMEs were synthesized from I
		{
			set<t_Expression*> E_new, D_new, I_new;
			set_union(E.begin(), E.end(), E_from_I.begin(), E_from_I.end(),inserter(E_new, E_new.begin())); // E_new <-- E \union E_from_I
			D_new = D; 
			I_new = Remaining_I;

			assert(!(E_new.empty() && D_new.empty() && I_new.empty()));
			t_Expression* RecreatedKandNode = CreateKandNode(E_new, D_new, I_new, em);
			assert(RecreatedKandNode != NULL);
			return RecreatedKandNode;
		}// LMEs were synthesized from I ends here
	} // I is non-empty ends here
} // function ends here



// This function generates E_from_I and Remaining_I from I 
// s.t. I = E_from_I \union Remaining_I using the rules
// (a) t <= 0 ---> t = 0
// (b) 2^{p}-1 <= t ---> t = 2^{p}-1
// (c) t_1 <= t_2 \wedge t_2 <= t_1 ---> t_1 = t_2
// returns true always
bool SynthesizeLMEsFromLMIs(const set<t_Expression*> &I, set<t_Expression*> &E_from_I, set<t_Expression*> &Remaining_I, t_ExpressionManager *em, BVManager *bvm, t_HashTable <string, int> &VariableList)
{
	vector<t_Expression*> I_Vector(I.begin(), I.end());
	vector<t_Expression*> Recreated_I_Vector;
	
	for(int i = 0; i < I_Vector.size(); i++)
	{
		t_Expression* inequation = I_Vector[i]; // take each inequation
		assert(inequation != NULL);
		assert("leq" == em->getLabelOfExpression(inequation));

		// let us see if inequation is of the form t <= 0 or 2^{p}-1 <= t
		// if yes, apply rules (a) or (b)
		t_Expression* equation_from_inequation = obtainEquivalentEqzNodeFromLeqNode(inequation, em, bvm, VariableList);
		if(equation_from_inequation != NULL) // inequation is of the form t <= 0 or 2^{p}-1 <= t
		{
			assert("eqz" == em->getLabelOfExpression(equation_from_inequation));
			E_from_I.insert(equation_from_inequation);
		}
		else // inequation is NOT of the form t <= 0 or 2^{p}-1 <= t
		{
			Recreated_I_Vector.push_back(inequation);
		}		
	}// for ends here

	// We have I = Recreated_I_Vector \union E_from_I here
	
	// Let's now check for applicability of rule (c) on inequations in Recreated_I_Vector
	set<t_Expression*> AlreadyDone;
	while(true)
    	{
      		bool fixpoint_reached = true;
		
		for(int i = 0; i < Recreated_I_Vector.size(); i++)
		{
			t_Expression* inequation_1 = Recreated_I_Vector[i]; // take each inequation
			assert(inequation_1 != NULL);
			assert("leq" == em->getLabelOfExpression(inequation_1));

			if(AlreadyDone.find(inequation_1) != AlreadyDone.end()) // We have already checked if there exists a pair for inequation_1
			{
				continue;
			}
			else
			{
				for(int j = i+1; j < Recreated_I_Vector.size(); j++)
				{
		      			t_Expression* inequation_2 = Recreated_I_Vector[j]; // take the inequation to pair with
					assert(inequation_2 != NULL);
					assert("leq" == em->getLabelOfExpression(inequation_2));

					// let us see if inequation_1, inequation_2 are of the form t_1 <= t_2, t_2 <= t_1
					// if yes, apply rule (c)
					t_Expression* equation_from_inequations = obtainEquivalentEqzNodeFromPairOfLeqNodes(inequation_1, inequation_2, em, bvm, VariableList);
					if(equation_from_inequations != NULL) // inequations are of the form t_1 <= t_2, t_2 <= t_1
					{
						assert("eqz" == em->getLabelOfExpression(equation_from_inequations));
						E_from_I.insert(equation_from_inequations);				

						// Note that it is important to erase position j first. 
						// since j > i, if position i is erased first, 
						// it will change the position of inequation at position j
						assert(j > i);
						// erase inequation_2 from Recreated_I_Vector
						Recreated_I_Vector.erase(Recreated_I_Vector.begin()+j);

						// erase inequation_1 from Recreated_I_Vector
						assert(i < Recreated_I_Vector.size());
						assert(inequation_1 == Recreated_I_Vector[i]);

						Recreated_I_Vector.erase(Recreated_I_Vector.begin()+i);						

                  				fixpoint_reached = false;
						break;
					}
				}// for..j ends here
			} // else ends here
			
			if(!fixpoint_reached) // Recreated_I_Vector is changed. Restart the for..i loop
        		{
            			break;
			}
			else //No matching inequation found for inequation_1
			{
				AlreadyDone.insert(inequation_1);
			}
		}// for..i ends here
	     
      		if(fixpoint_reached)
		{
	  		break;
		}
	}// while(true) ends here

	// We have I = Recreated_I_Vector \union E_from_I here

	// Let's create set from Recreated_I_Vector
	Remaining_I.clear();
	copy(Recreated_I_Vector.begin(), Recreated_I_Vector.end(), inserter(Remaining_I, Remaining_I.end()));
	return true;
}



// Given an leq node t_1 <= t_2, this function 
// (a) Checks if t_2 is 0. If yes, returns t_1 = 0
// (b) Checks if t_1 is 2^{p}-1. If yes, returns t_2 = 2^{p}-1 i.e. t_2 + 1 = 0
// (c) Otherwise returns NULL
t_Expression* obtainEquivalentEqzNodeFromLeqNode(t_Expression *LeqNode, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList)
{
	// LeqNode: t_1 <= t_2
	
	assert(LeqNode != NULL);
	assert("leq" == em->getLabelOfExpression(LeqNode));

	t_Expression* t_1 = getIthChild(LeqNode, 0, em);	
	assert(t_1 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_1));

	t_Expression* t_2 = getIthChild(LeqNode, 1, em);	
	assert(t_2 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_2));

	if(kaddIsZeroConstant(t_2, em)) // t_2 == 0
	{
		// return t_1 = 0
		string equation_label = "eqz";
		t_Expression* EqzNode = CreateNode(equation_label, t_1, em);
		assert(EqzNode != NULL);							
		return EqzNode;
	}
	else if(kaddIsMaximumConstant(t_1, em)) // t_1 == 2^{p}-1
	{
		// return t_2 + 1 = 0

		// Let us create kadd node for t_2 + 1
		// Let's obtain coefficient map and constant of t_2
		set<string> variables_to_exclude;// no variables to exclude
		bvatom ConstantOft2; 
		vector< pair< string, bvatom > > CoefficientMapOft2; 
		bool CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(t_2, variables_to_exclude, ConstantOft2, CoefficientMapOft2, em, bvm);
		assert(CoefficientMapFound);	

		// Now, let's obtain coefficient map and constant of t_2+1
		int p = em->getWidth(t_2);
		string OneString = getOneBinaryStringOfGivenLength(p);
		bvatom ConstantOft2PlusOne = bvm->bvadd(ConstantOft2, bvm->getBVatom(p, OneString));
		
		// let's now create kadd node for t_2 + 1
		t_Expression *t2PlusOne = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft2PlusOne, CoefficientMapOft2, em, VariableList, bvm);// note that coefficient map of t2+1 is the same as coefficient map of t2
		assert(t2PlusOne != NULL);

		// let's create the equation
		string equation_label = "eqz";
		t_Expression* EqzNode = CreateNode(equation_label, t2PlusOne, em);
		assert(EqzNode != NULL);							
		return EqzNode;
	}
	else
	{
		return NULL;
	}
}



// Given leq nodes t_1 <= t_2 and t_3 <= t_4, this function 
// (a) Checks if t_3 is the same as t2 and t_4 is the same as t1. If yes, returns t_1 = t_2 i.e., t_1 - t_2 = 0
// (b) Otherwise returns NULL
t_Expression* obtainEquivalentEqzNodeFromPairOfLeqNodes(t_Expression *LeqNode_1, t_Expression *LeqNode_2, t_ExpressionManager *em, BVManager* bvm, t_HashTable <string, int> &VariableList)
{

	// LeqNode_1: t_1 <= t_2

	assert(LeqNode_1 != NULL);
	assert("leq" == em->getLabelOfExpression(LeqNode_1));

	t_Expression* t_1 = getIthChild(LeqNode_1, 0, em);	
	assert(t_1 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_1));

	t_Expression* t_2 = getIthChild(LeqNode_1, 1, em);	
	assert(t_2 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_2));


	// LeqNode_2: t_3 <= t_4

	assert(LeqNode_2 != NULL);
	assert("leq" == em->getLabelOfExpression(LeqNode_2));

	t_Expression* t_3 = getIthChild(LeqNode_2, 0, em);	
	assert(t_3 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_3));

	t_Expression* t_4 = getIthChild(LeqNode_2, 1, em);	
	assert(t_4 != NULL);
	assert("kadd" == em->getLabelOfExpression(t_4));

	if(t_3 == t_2 && t_4 == t_1) // i.e. we have t_1 <= t_2 \wedge t_2 <= t_1
	{
		// return t_1 - t_2 = 0

		// Let us create kadd node for t_1 - t_2
		int p = em->getWidth(t_1);
		set<string> variables_to_exclude;// no variables to exclude
		bool CoefficientMapFound;

		// Let's obtain coefficient map and constant of t_1
		bvatom ConstantOft1; 
		vector< pair< string, bvatom > > CoefficientMapOft1; 
		CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(t_1, variables_to_exclude, ConstantOft1, CoefficientMapOft1, em, bvm);
		assert(CoefficientMapFound);

		// Let's obtain coefficient map and constant of t_2
		bvatom ConstantOft2; 
		vector< pair< string, bvatom > > CoefficientMapOft2; 
		CoefficientMapFound = getKaddNodeAsCoefficientMapExcludingGivenVariables(t_2, variables_to_exclude, ConstantOft2, CoefficientMapOft2, em, bvm);
		assert(CoefficientMapFound);	

		// now, let's obtain coefficient map and constant of -t_2 from those of t_2
		bvatom ConstantOfMinust2; 
		vector< pair< string, bvatom > > CoefficientMapOfMinust2; 
		ConstantOfMinust2 = bvm->addInverse(ConstantOft2);
		additiveInverse(CoefficientMapOft2, CoefficientMapOfMinust2, bvm);
		
		// now, let's obtain coefficient map and constant of t_1-t_2 from those of t_1 and -t_2
		bvatom ConstantOft1Minust2; 
		vector< pair< string, bvatom > > CoefficientMapOft1Minust2; 
		ConstantOft1Minust2 = bvm->bvadd(ConstantOft1, ConstantOfMinust2);
		addition(CoefficientMapOft1, CoefficientMapOfMinust2, CoefficientMapOft1Minust2, bvm, VariableList);

		// let's now create kadd node for t_1 - t_2
		t_Expression *t1Minust2 = CreateKaddNodeFromConstantAndCoefficientMap(p, ConstantOft1Minust2, CoefficientMapOft1Minust2, em, VariableList, bvm);
		assert(t1Minust2 != NULL);

		// let's create the equation
		string equation_label = "eqz";
		t_Expression* EqzNode = CreateNode(equation_label, t1Minust2, em);
		assert(EqzNode != NULL);							
		return EqzNode;
	}
	else
	{
		return NULL;
	}
}