#include<iostream>
#include<vector>
#include<stdio.h>
#include<algorithm>
#include<cstdlib>
#include<iterator>
#include<exception>
#include<fstream>
#include <string.h>
#include <functional>
#include <cassert>
#include <sys/time.h>
using namespace std;
#include "ExpressionManager.h"
#include "HashTable_WithStandardKeys.h"
#include "ExpressionMisc.h"
#include "Project.h"
#include "Monniaux.h"

#include "Generator.hpp"
#include "Skolem.hpp"
#include "AIGBasedSkolem.hpp"


t_DAGManager *dm; //dag manager class

class pDAGNode //smart pointer for t_DAGNode*
{
	t_DAGNode* ptr;

	public:
		pDAGNode(t_DAGNode* p):ptr(p) {dm->incrementReferenceCount(ptr);}
		pDAGNode(const pDAGNode &p):ptr(p.ptr) {dm->incrementReferenceCount(ptr);}
		~pDAGNode(){ dm->decrementReferenceCount(ptr);}
		void operator=(const pDAGNode &p)
		{
			dm->incrementReferenceCount(p.ptr); 
			dm->decrementReferenceCount(ptr); 
			ptr = p.ptr;
			return;
		}
		t_DAGNode* operator->(){return ptr;}
		t_DAGNode& operator*(){return *ptr;}
};


string buildRelationalExpression(string reader, t_ExpressionManager* em, t_Expression* &expr);
string buildArithmaticExpression(string reader, t_ExpressionManager* em, t_Expression* &expr);
string buildSelectExpression(string reader,t_ExpressionManager* em,t_Expression* &expr);
string buildConcatExpression(string reader, t_ExpressionManager *em, t_Expression* &expr);
string buildBracketExpression(string reader, t_ExpressionManager *em, t_Expression* &expr);
string buildVariableExpression(string reader, t_ExpressionManager *em, t_Expression* &expr);

string buildExpression(string reader, t_ExpressionManager* em, t_Expression* &expr)
{
    //check for relational operators
    t_Expression* first;
    trimInPlace(reader);
    //assert( ! reader.empty());
    if(reader.empty())
    {
        cout<<"empty reader"<<endl;
        expr = NULL;
        return reader;
    }
    reader = buildRelationalExpression(reader, em, first);

    trimInPlace(reader);

    if (reader.empty())
    {
        expr = first;
        return reader;
    }
    string oper = reader.substr(0, 2);
    if (oper == "&&" || oper == "||")
        reader = reader.substr(2);
    else
    {
        expr = first;
        return reader;
    }

    while (oper == "&&" || oper == "||")
    {
        t_Expression* second;
        reader = buildRelationalExpression(reader, em, second);
        if (second == NULL)
            break;
        string label;
        if (oper == "&&")
        {
            label = em->m_operatorLabelLogAND;
        } else if (oper == "||")
            label = em->m_operatorLabelLogOR;

        first = em->createOneBitExpressionWithTwoOperands(label, first, second);
        trimInPlace(reader);

        if (reader.empty())
            break;
        oper = reader.substr(0, 2);
        reader = reader.substr(2);
    }

    expr = first;
    return reader;
}

string buildRelationalExpression(string reader, t_ExpressionManager* em, t_Expression* &expr)
{
    t_Expression* first;
    reader = buildArithmaticExpression(reader, em, first);

    trimInPlace(reader);

    if (reader.empty())
    {
        expr = first;
        return reader;
    }
    string oper = reader.substr(0, 2);
    string label;
    if (oper == ">=")
    {
        label = em->m_operatorLabelGreaterThanOrEqual;
        reader = reader.substr(2);
    } else if (oper == "<=")
    {
        label = em->m_operatorLabelLessThanOrEqual;
        reader = reader.substr(2);
    } else if (oper == "==")
    {
        label = em->m_operatorLabelLogicalEquality;
        reader = reader.substr(2);
    } else
    {
        oper = reader.substr(0, 1);
        if (oper == "<")
        {
            label = em->m_operatorLabelLessThan;
            reader = reader.substr(1);
        } else if (oper == ">")
        {
            label = em->m_operatorLabelGreaterThan;
            reader = reader.substr(1);
        } else //no relational operator
        {
            expr = first;
            return reader;
        }
    }

    trimInPlace(reader);

    t_Expression* second;
    reader = buildArithmaticExpression(reader, em, second);
    if (second == NULL)
    {
        expr = first;
        //cout<<"No second operand found."<<endl;
        return reader;
    }
    //    if(0)
    //    {
    //        ofstream out("ParsedExpression", ios::app);
    //        out<<"Testing: operands of "<<label<<endl;
    //        string name = "first";
    //        em->printExpressionToFileAsDAG(name, first, &out);
    //        name = "second";
    //        em->printExpressionToFileAsDAG(name, second, &out);
    //        out<<endl;
    //    }

    expr = em->createOneBitExpressionWithTwoOperands(label, first, second);

    //TypeOfExpressionTuple type_info = {TYPE_BOOL, 1};
    //vector<t_Expression*> vec_operands = t_ExpressionManager::buildVector(first,second);
    //expr = em->createExpression(label, vec_operands, type_info);

    return reader;
}

string buildArithmaticExpression(string reader, t_ExpressionManager* em, t_Expression* &expr)
{
    t_Expression* first;
    reader = buildSelectExpression(reader, em, first);

    trimInPlace(reader);
    if (reader.empty())
    {
        expr = first;
        return reader;
    }
    string oper = reader.substr(0, 1);
    if (oper == "+" || oper == "-" || oper == "*" || oper == "/" || oper == "%")
    {
        //reader = reader.substr(1);
    } else
    {
        expr = first;
        return reader;
    }

    while (oper == "+" || oper == "-" || oper == "*" || oper == "/" || oper == "%")
    {
        reader = reader.substr(1); //skip the operator
        string label;
        if (oper == "+")
            label = em->m_operatorLabelADD;
        else if (oper == "-")
            label = em->m_operatorLabelSUB;
        else if (oper == "*")
            label = em->m_operatorLabelMultiply;
        else if (oper == "/")
            label = em->m_operatorLabelDivide;
        else if (oper == "%")
            label = em->m_operatorLabelModulus;

        t_Expression* second;
        reader = buildSelectExpression(reader, em, second);
        if (second == NULL)
            break;

        vector<t_Expression*> vec_operands = t_ExpressionManager::buildVector(first, second);
        int wid = max( em->getWidth(first), em->getWidth(second) );
        //TypeOfExpressionTuple operatorType = {TYPE_UNSIGNED_INTEGER, -1};
        TypeOfExpressionTuple operatorType = {TYPE_UNSIGNED_BITVECTOR, wid};
        first = em->createExpression(label, vec_operands, operatorType);

        trimInPlace(reader);
        if (reader.empty())
            break;
        oper = reader.substr(0,1);
    }

    expr = first;
    return reader;
}

string buildSelectExpression(string reader,t_ExpressionManager* em,t_Expression* &expr)
{
    t_Expression* first;
    reader = buildConcatExpression(reader, em, first);
    trimInPlace(reader);

    if(reader.empty())
    {
        expr = first;
        return reader;
    }
    string oper = reader.substr(0, 1);
    bool foundSelect = false;
    if (oper == "[")
    {
        foundSelect = true;
    } else
    {
        expr = first;
        return reader;
    }

#ifdef OLD
    if(foundSelect)
    {
        reader = reader.substr(1);
        t_Expression* ub_expr;
        t_Expression* lb_expr;
        reader = buildConcatExpression(reader, em, ub_expr);
        trimInPlace(reader);

        assert(ub_expr != NULL);
        assert(!reader.empty() && reader[0]==':');

        reader = reader.substr(1);
        int ub = em->getConstantValuePresentInExpression(ub_expr);


        reader = buildConcatExpression(reader,em,lb_expr);
        assert(lb_expr != NULL);
        int lb = em->getConstantValuePresentInExpression(lb_expr);

        int width = ub-lb+1;
        vector<t_Expression*> operands = t_ExpressionManager::buildVector(first,lb_expr,ub_expr);
        string label = "select";

        TypeOfExpressionTuple operatorType = {TYPE_UNSIGNED_BITVECTOR, width};
        expr = em->createExpression(label,operands,operatorType);

        assert(reader[0] == ']');
        reader = reader.substr(1);

        return reader;
    }
    else
    {
        assert(false);
    }
#else
    int openidx = reader.find('[');
    int mididx = reader.find(':');
    int closeidx = reader.find(']');
    
    assert(openidx>=0 && openidx<mididx);
    assert(mididx < closeidx);
    assert(closeidx <= reader.length());
    
    string ubStr = reader.substr(openidx+1, mididx-openidx-1);
    string lbStr = reader.substr(mididx+1, closeidx-mididx-1);
    
    TypeOfExpressionTuple constIntType = {TYPE_UNSIGNED_INTEGER, -1};
    vector<t_Expression*> operands(3,NULL);
    operands[0] = first;
    operands[1] = em->createConstant(lbStr, constIntType);
    operands[2] = em->createConstant(ubStr, constIntType);
    
    assert(operands[1]!= NULL);
    assert(operands[2]!= NULL);
    
    int ub = stringToInteger(ubStr);
    int lb = stringToInteger(lbStr);
    assert(lb>=0);
    assert(ub>=lb);
    TypeOfExpressionTuple typ = {TYPE_UNSIGNED_BITVECTOR, ub-lb+1};
    string label = "select";
    expr = em->createExpression(label, operands, typ);
    
    return reader.substr(closeidx+1);   //done forget to eat away the expression just parsed
#endif
}

string buildConcatExpression(string reader, t_ExpressionManager *em, t_Expression* &expr)
{
    trimInPlace(reader);
    assert(! reader.empty());
    if(reader[0] != '{')
    {
        return buildBracketExpression(reader, em, expr);
    }
    
    vector<t_Expression*> operands;
    int width = 0;
    while(reader[0] != '}')
    {
        reader = reader.substr(1);      //eat away the '{' ',' '}'
        t_Expression *e;
        reader = buildBracketExpression(reader, em, e);
        assert(e != NULL);
        assert( ! reader.empty());      //'}' should be left in the string
        operands.push_back(e);
        width += em->getWidth(e);
        assert(reader[0] ==',' || reader[0] == '}');
    }
    
    assert(operands.empty() == false);
    {
        string label = "concat";
        TypeOfExpressionTuple type = {TYPE_UNSIGNED_BITVECTOR, width};
        expr = em-> createExpression(label, operands, type);
    }
    
    return reader.substr(1);    //eat away the '}'
}

string buildBracketExpression(string reader, t_ExpressionManager *em, t_Expression* &expr)
{
    trimInPlace(reader);
    bool negate = false;
    if (reader[0] == '!')
    {
        negate = true;
        reader = reader.substr(1);
        trimInPlace(reader);
    }

    t_Expression* first;

    if (reader[0] == '(')
    {
        //cout << "'(' found.:" << reader << endl;

        int brackCount = 1, i;
        for (i = 1; i < reader.size() && brackCount > 0; ++i)
        {
            if (reader[i] == ')')
                brackCount--;
            else if (reader[i] == '(')
                brackCount++;

            if (brackCount == 0)
                break;
        }
        //Now i is the position of corresponding ')'
        string insideBracket = reader.substr(1, i - 1);
        reader = reader.substr(i + 1);

        //cout << "InsideBracket:" << insideBracket << endl;
        insideBracket = buildExpression(insideBracket, em, first);
        trimInPlace(insideBracket);

        if (insideBracket.empty() == false)
        {
            cout << "ERROR: Incomplete expression found:"<<insideBracket << endl;
        }
        //cout << "Expression with bracket parsed. Remaining:" << reader << endl;

        trimInPlace(reader);

    } else
    {
        reader = buildVariableExpression(reader, em, first);
    }

    if (negate)
    {
        expr = em->createOneBitExpressionWithOneOperand(em->m_operatorLabelLogNOT, first);
    } else
        expr = first;

    return reader;
}

string buildVariableExpression(string reader, t_ExpressionManager *em, t_Expression* &expr)
{
    trimInPlace(reader);
    //cout << "BuildVariable:" << reader << endl;
    if (reader[0] == ')')
    {
        //cout << "Closing parenthesis found" << endl;
        expr = NULL;
        return reader;
    }
    string operand;
    int i = 0;
    static string specialChars("_$.#@");
    for (int i = 0; i < reader.size(); ++i)
    {
        char c = reader[i];
        if (isalnum(c) || specialChars.find(c)!=string::npos)
        {
            operand += c;
        } else
            break;
    }

    //const char* strPtr = operand.c_str();
    //char* end;
    //long val = strtol(strPtr, &end, 0);
    //if (end == strPtr)
    reader = reader.substr(operand.size() );
    if( ! isdigit((char)operand[0]) )
    {
        //Not a number'
        int width, ub, lb;
        string symName = operand;
        cout<<"Processing "<<operand<<endl;
        operand = extractNumberAtEnd(operand, lb);
        operand = extractNumberAtEnd(operand, ub);
        width = ub-lb+1;
        assert(width>0);
        TypeOfExpressionTuple symbolType = {TYPE_UNSIGNED_BITVECTOR, width};
        //cout << "Creating symbol:" << symName << " of size " << width << endl;
        expr = em->createSymbol(symName, symbolType);
    } else
    {
        //cout << "Creating constant:" << operand << " ";
        
        {
            if(operand.find("0b") != 0) //not starts with 0b
            {
                //integer
                int op;
                if(operand.find("0x") == 0)
                {
                    istringstream ss(operand);
                    ss>>op;
                }
                else
                {
                    op= stringToInteger(operand);
                }
                
                string bitv = integerToBinaryString(op);
                TypeOfExpressionTuple constantType = {TYPE_UNSIGNED_BITVECTOR, bitv.size()};
                expr = em->createConstant(bitv, constantType);
                //cout<<"type integer to "<<bitv.size()<<" bit bitvector"<<endl;
            }
            else{
                operand = operand.substr(2);
                TypeOfExpressionTuple constantType = {TYPE_UNSIGNED_BITVECTOR, operand.size()};
                expr = em->createConstant(operand, constantType);
                //cout<<"type bitvector"<<endl;
            }
        }
        //TypeOfExpressionTuple constantType = {TYPE_UNSIGNED_BITVECTOR, operand.size()};
        //expr = em->createConstant(operand, constantType);
    }

    //reader = reader.substr(operand.size()); //skip the operand
    //cout<<"  Remaining:"<<reader<<endl;
    return reader;
}

int main(int argc, char *argv[])
{  

  bool test_exp_manager = false;
  if(test_exp_manager)
  {
	  t_ConfigurationOptions config_options("config.txt");
  	  t_ExpressionManager *em = new t_ExpressionManager(config_options);
          BVManager* bvm = BVManager::getInstance();

	  TypeOfExpressionTuple te1= {TYPE_UNSIGNED_BITVECTOR, 2};
	  //te1.m_type=TYPE_UNSIGNED_BITVECTOR;
	  //te1.m_width=2;
	  string bv1="bv1";
	  string bv2="bv2";
	  t_Expression *e1 = em->createSymbol(bv1,te1);
	  t_Expression *e2 = em->createSymbol(bv2,te1);
	    
	 
	  TypeOfExpressionTuple tt = {TYPE_BOOL, 1};
	  string TrueString = "true";
	  t_Expression *TrueNode1 = em->createConstant(TrueString, tt);
	  t_Expression *TrueNode2 = em->createConstant(TrueString, tt);
	    
	  if(TrueNode1 == TrueNode2)
		{
		cout<<"\nTrue nodes are the same. It is "<<TrueNode1<<endl;
		}
	  else
		{
		cout<<"\nTrue nodes are the different"<<endl;
		}


	  vector<t_Expression *> v_operands;
	  v_operands.push_back(e1);
	  v_operands.push_back(e2);
	  string add="add";
	  //t_Expression *e3 = em->createExpression(add,v_operands);
	  t_Expression *e3 = em->createExpression(add,v_operands, te1);
	  vector<t_Expression *> v_e4;
	  v_e4.push_back(e2);
	  v_e4.push_back(e1);
	  //t_Expression *e4 = em->createExpression(add,v_e4);
	  t_Expression *e4 = em->createExpression(add,v_e4, te1);

	 string equal = "logeq";
	 vector<t_Expression *> v_equal;
	 v_equal.push_back(e3);
	 v_equal.push_back(e4);
	 t_Expression *e5 = em->createExpression(equal,v_equal, tt); 

	  
	  ofstream *fout1=new ofstream("testOutputToExpression");
	  //em->printExpressionToFile(e4,fout1);
	  em->printExpressionToFileAsDAG("expr", e5, cout);
	  string exprName = "testExpression";
	  em->printExpressionAsYicesExpression(e5,exprName,fout1);
	  fout1->close();
	 
	  cout<<"\nLabel of e4:"<<em->getLabelOfExpression(e4)<<endl;
	  cout<<"\nSize of e4:"<<em->getSizeOfExpression(e4)<<endl;
	  cout<<"\nWidth of e4:"<<em->getWidth(e4)<<endl;
	  t_TypeOfExpression e4Type = em->getTypeOfExpressionWithOutWidth(e4);

	  if(e4Type == TYPE_UNSIGNED_BITVECTOR)
		cout<<"\nType of e4 is TYPE_UNSIGNED_BITVECTOR\n";
	  else
		cout<<"\nWhat is type of e4?\n";

	   
	  
	  cout<<"\nLeaves of e4\n";
	  vector<t_Expression *> leavesExprInt = em->getVectorOfLeafExpressions(e4);
	  for (int i=0;i<leavesExprInt.size();i++)
	    {
	      cout<<em->getLableOfExpression(leavesExprInt[i])<<endl;
	      signed int ival=i;
	      cout<<" value given = "<<i<<endl;
	      em->setValue(leavesExprInt[i],ival);
	    }
	  cout<<"Evaluation starts:\n";
	  em->evaluateExpression(e4);
	  em->printExpressionToFileAsDAG("expr", e4, cout);//The output is not clear. Is evalaution actually happening?

	 cout<<"\nChildren of e4\n";
	 vector<t_Expression *> childrenExprInt = em->getVectorOfOperands(e4);
	  for (int i=0;i<childrenExprInt.size();i++)
	    {
	      cout<<em->getLableOfExpression(childrenExprInt[i])<<endl;      
	    }

	  
	  TypeOfExpressionTuple type_ite;
	  type_ite.m_type = TYPE_UNSIGNED_BITVECTOR;
	  type_ite.m_width = 2;
	  string cond = "cond";
	  t_Expression *e_bool = em->createSymbol(cond,type_ite);
	  vector<t_Expression *> v_ite_op;
	  v_ite_op.push_back(e_bool);
	  v_ite_op.push_back(e1);
	  v_ite_op.push_back(e1);
	  string ite = "ite";
	  t_Expression *e_ite_bv = em->createExpression(ite,v_ite_op, type_ite); // This gets simplified to e1
	  em->printExpressionToFileAsDAG("ite", e_ite_bv, cout);
	  cout<<endl;

	  // Creating constants
	  
	  TypeOfExpressionTuple tconst = {TYPE_UNSIGNED_BITVECTOR, 3};
	  string const1="111";
	  string const2="010";
	  t_Expression *c1 = em->createConstant(const1,tconst);
	  t_Expression *c2 = em->createConstant(const2,tconst);
	  vector<t_Expression *> const_operands;
	  const_operands.push_back(c1);
	  const_operands.push_back(c2);
	  string myop="multiply";
	  t_Expression *c3 = em->createExpression(myop,const_operands, tconst); 
	  em->printExpressionToFileAsDAG("c3", c3, cout);


	  TypeOfExpressionTuple tconst2 = {TYPE_UNSIGNED_BITVECTOR, 40};
	  string const4="1111111111111111111111111111111111111111";
	  string const5="0000010000000000000000000000000000000000";
	  t_Expression *c4 = em->createConstant(const4,tconst2);
	  t_Expression *c5 = em->createConstant(const5,tconst2);
	  const_operands.clear();
	  const_operands.push_back(c4);
	  const_operands.push_back(c5);
	  string myop2="add";
	  t_Expression *c6 = em->createExpression(myop2,const_operands, tconst2); // This works fine. Does 40-bit operation correctly
	  em->printExpressionToFileAsDAG("c6", c6, cout);

	  
	  //string reader = " (0b011 * x) + (0b100 * y) + (0b001 * z) + 0b010 == 0b000 ";
	  //string reader = "0b100 * y == 0b000";
	  //t_Expression *ReaderExp; 
	  //string remaining;
	  //remaining = buildExpression(reader, em, ReaderExp); 
	  //em->printExpressionToFileAsDAG("ReaderExp", ReaderExp, cout);
	  //cout<<"\nremaining = "<<remaining<<endl;

	  //t_DAGNode *ReaderDAG = (ReaderExp->m_dagExpression)->getDag();

  }//if(test_exp_manager) ends here

  // Testing the changes in NewBV.cc
  bool test_bv_manager = false;
  if(test_bv_manager)
  {  

	  t_ConfigurationOptions config_options("config.txt");
  	  t_ExpressionManager *em = new t_ExpressionManager(config_options);
          BVManager* bvm = BVManager::getInstance();


	  string mystring = "1111111111111111111111111111111111111111111111111111111111111111"; 
	  bvatom max = bvm->getBVatom(64, mystring);
	  bvatom max_square = bvm->bvmul(max, max);// error in arith_mult!!! result obtained is 0x4000000000000001[64]
	  						// should be 0x0000000000000001[64]						
	  cout<<"\nmax = "; bvm->printPrettyBVatom(max);
	  cout<<"\nmax^{2} = "; bvm->printPrettyBVatom(max_square);
	  cout<<endl;

	  string mystring2 = "11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111"; 
	  bvatom max2 = bvm->getBVatom(128, mystring2);
	  bvatom max2_square = bvm->bvmul(max2, max2);				
	  cout<<"\nmax2 = "; bvm->printPrettyBVatom(max2);
	  cout<<"\nmax2^{2} = "; bvm->printPrettyBVatom(max2_square);
	  cout<<endl;


	  string test_str = "111"; 
	  string one_str = "001";
	  string two_str = "010";
	  string six_str = "110";
	  string four_str = "100";
	  bvatom test_bv1 = bvm->getBVatom(3, test_str);
	  bvatom test_one = bvm->getBVatom(3, one_str);
	  bvatom test_two = bvm->getBVatom(3, two_str);
	  bvatom test_bv1_square = bvm->bvmul(test_bv1, test_bv1);					
	  cout<<"\ntest_bv1 = "; bvm->printPrettyBVatom(test_bv1);
	  cout<<"\ntest_bv1 = "<<bvm->printBVasBinString(test_bv1)<<endl;
	  cout<<"\ntest_bv1^{2} = "; bvm->printPrettyBVatom(test_bv1_square);
	  cout<<"\ntest_bv1^{2} = "<<bvm->printBVasBinString(test_bv1_square)<<endl;

	  cout<<endl<<"test_bv1 = "<<bvm->printBVasBinString(test_bv1)<<endl;
	  cout<<endl<<"test_one = "<<bvm->printBVasBinString(test_one)<<endl;
	  bvatom test_bv1_plus_one = bvm->bvadd(test_bv1, test_one);	
	  bvatom test_bv1_minus_one = bvm->bvsub(test_bv1, test_one);		
	  cout<<"\ntest_bv1+1 = "<<bvm->printBVasBinString(test_bv1_plus_one)<<endl; 
	  cout<<"\ntest_bv1 >> 2 = "<<bvm->printBVasBinString(bvm->right_shift(test_bv1, test_two))<<endl; 
	  cout<<"\narith_neg(test_bv1) = "<<bvm->printBVasBinString(bvm->arith_neg(test_bv1))<<endl; 
	  cout<<"\ntest_bv1-1 = "<<bvm->printBVasBinString(test_bv1_minus_one)<<endl; 
	  cout<<endl;

	  string test_str2 = "0000001100001111"; 
	  bvatom test_bv2 = bvm->getBVatom(16, test_str2);
	  //bvatom test_bv2 = bvm->concat(bvm->getZeroedBVatom(4), test_bv1);

	  cout<<endl<<"test_bv1 = "<<bvm->printBVasBinString(test_bv1)<<endl;
	  cout<<endl<<"test_bv2 = "<<bvm->printBVasBinString(test_bv2)<<endl;

	  bvatom test_six = bvm->getBVatom(3, six_str);
	  bvatom test_four = bvm->getBVatom(3, four_str);
	  bvatom test_six_shifted = bvm->bvlshift(test_six, 2);
	  bvatom test_six_multiplied = bvm->bvmul(test_six, test_four);

	  cout<<"\ntest_six = "; bvm->printPrettyBVatom(test_six);

	  cout<<"\ntest_six_shifted = "; bvm->printPrettyBVatom(test_six_shifted);
	  if(bvm->checkBVForZero(test_six_shifted) == false)
		{
		cout<<endl<<"test_six_shifted is non zero"<<endl;
		}
	  else
		{
		cout<<endl<<"test_six_shifted is zero"<<endl;
		}
	   
	  cout<<"\ntest_six_multiplied = "; bvm->printPrettyBVatom(test_six_multiplied);
	  if(bvm->checkBVForZero(test_six_multiplied) == false)
		{
		cout<<endl<<"test_six_multiplied is non zero"<<endl;
		}
	  else
		{
		cout<<endl<<"test_six_multiplied is zero"<<endl;
		}

	   if(bvm->checkBVEquality(test_six_multiplied, test_six_shifted))
		{
		cout<<endl<<"test_six_multiplied = test_six_shifted"<<endl;
		}
	  else
		{
		cout<<endl<<"test_six_multiplied != test_six_shifted"<<endl;
		}
	   
	   bool mi_test = true;
	   if(mi_test)
	   {
		   cout<<"\nTesting the changes in NewBV.cc related to multiplicative inverse\n";   	   

		   /* following four lines are for testing multInverse on 32-bit numbers */
		   string mystring = "11101111111111110101001111011111"; //inefficient when tried with algo. in 
		   bvatom result = bvm->getBVatom(32, mystring);
		   //string mystring = "101"; 	
		   //bvatom result = bvm->getBVatom(3, mystring);
		   
		   /* following four lines are for testing multInverse on 64-bit numbers */
		   //string mystring = "1000100110101011100010011010101110001001101010111000100110101011"; //inefficient when tried with algo. in 
		   //string mystring = "0000100110101011100010011010101110001001101010111000100111111111"; 
		   //string mystring = "1111111111111111111111111111111111111111111111111111111111111111"; 
		   //string mystring = "0000000000000000000000000000000000000000000000000000000000001111"; //inefficient when tried with algo. in
		   //string mystring = "0000000000000000000000000000000000000000000000000000000000000011"; //still ok when tried with algo. in	
		   //bvatom result = bvm->getBVatom(64, mystring);

		   cout<<"\nresult = ";
		   bvm->printPrettyBVatom(result);
		   cout<<endl;
		   cout<<"\n-result = ";
		   bvatom ai_result = bvm->addInverse(result);
		   bvm->printPrettyBVatom(ai_result);
		   cout<<endl;
		   cout<<"\nresult' = ";
		   bvatom mi_result = bvm->multInverse(result);
		   bvm->printPrettyBVatom(mi_result);
		   cout<<endl;
		   cout<<"\nresult' * result = ";
		   bvatom product = bvm->bvmul(result, mi_result);
		   bvm->printPrettyBVatom(product);
		   cout<<endl;	   
	   }
  }// if(test_bv_manager) ends here
   
  bool test_garbage_collector = false;
  if(test_garbage_collector)
  {

	  t_ConfigurationOptions config_options("config.txt");
  	  t_ExpressionManager *em = new t_ExpressionManager(config_options);
          BVManager* bvm = BVManager::getInstance();

	  // Testing the garbage collection part
	  cout<<"\nTesting the garbage collection part\n";

	  dm = new t_DAGManager(true, true, false, 0, 3);
	  vector<t_DAGNode*> dead_nodes;
	  vector<t_DAGNode*> root_nodes;

	  bool use_smart_pointers = false;

	  if(use_smart_pointers)
	  {
		pDAGNode x = dm->createNode("x");
		pDAGNode three = dm->createNode("3");
		
	  }	
	  else
	  {  
	  	t_DAGNode *x = dm->createNode("x");
	  	dm->incrementReferenceCount(x);

	  	t_DAGNode *three = dm->createNode("3");
	  	dm->incrementReferenceCount(three);

	  	dm->getVectorOfDeadNodes(dead_nodes);
	  	cout<<"\ndead_nodes after creation of x and three\n";
	  	for(int i=0; i<dead_nodes.size(); i++)
			{
			cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}

	  	root_nodes = dm->getVectorOfRootNodes();
	  	cout<<"\nroot_nodes after creation of x and three\n";
	  	for(int i=0; i<root_nodes.size(); i++)
			{
			cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}

	  	vector<t_DAGNode*> p1_children;
	  	p1_children.push_back(three);
	  	p1_children.push_back(x);	
	  	t_DAGNode *p1 = dm->createNode("*", p1_children);
	  	dm->incrementReferenceCount(p1);
	  	dm->decrementReferenceCount(x);
	  	dm->decrementReferenceCount(three);
	  
	  	dm->getVectorOfDeadNodes(dead_nodes);
	  	cout<<"\ndead_nodes after creation of p1\n";
	  	for(int i=0; i<dead_nodes.size(); i++)
			{
			cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  	root_nodes = dm->getVectorOfRootNodes();
	  	cout<<"\nroot_nodes after creation of p1\n";
	  	for(int i=0; i<root_nodes.size(); i++)
			{
			cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}

	  	t_DAGNode *x_clone = dm->createNode("x");
	  	dm->incrementReferenceCount(x_clone);

	  	t_DAGNode *three_clone = dm->createNode("3");
	  	dm->incrementReferenceCount(three_clone);

	  	dm->getVectorOfDeadNodes(dead_nodes);
	  	cout<<"\ndead_nodes after creation of x_clone and three_clone\n";
	  	for(int i=0; i<dead_nodes.size(); i++)
			{
			cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  	root_nodes = dm->getVectorOfRootNodes();
	  	cout<<"\nroot_nodes after creation of x_clone and three_clone\n";
	  	for(int i=0; i<root_nodes.size(); i++)
			{
			cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}  

	  	vector<t_DAGNode*> p1_clone_children;
	  	p1_clone_children.push_back(three_clone);
	  	p1_clone_children.push_back(x_clone);	
	  	t_DAGNode *p1_clone = dm->createNode("*", p1_clone_children);
	  	dm->incrementReferenceCount(p1_clone);
	  	dm->decrementReferenceCount(x_clone);
	  	dm->decrementReferenceCount(three_clone);  

	  	dm->getVectorOfDeadNodes(dead_nodes);
	  	cout<<"\ndead_nodes after creation of p1_clone\n";
	  	for(int i=0; i<dead_nodes.size(); i++)
			{
			cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  	root_nodes = dm->getVectorOfRootNodes();
	  	cout<<"\nroot_nodes after creation of p1_clone\n";
	  	for(int i=0; i<root_nodes.size(); i++)
			{
			cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}

	  	vector<t_DAGNode*> p2_children;
	  	p2_children.push_back(p1);
	  	p2_children.push_back(p1_clone);	
	  	t_DAGNode *p2 = dm->createNode("+", p2_children);
	  	dm->incrementReferenceCount(p2);
	  	dm->decrementReferenceCount(p1);
	  	dm->decrementReferenceCount(p1_clone);  

		cout<<"p2 =  " <<p2->getLabel()<<endl;
		vector<t_DAGNode*> LeafNodes = dm->getVectorOfLeafNodes(p2);
		cout<<"\nleaf nodes\n";
	  	for(int i=0; i<LeafNodes.size(); i++)
			{
			cout<<integerToString((long int)(LeafNodes[i]))<< "   " <<LeafNodes[i]->getLabel()<<endl;
			}
	  
	  	dm->getVectorOfDeadNodes(dead_nodes);
	  	cout<<"\ndead_nodes after creation of p2\n";
	  	for(int i=0; i<dead_nodes.size(); i++)
			{
			cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  	root_nodes = dm->getVectorOfRootNodes();
	  	cout<<"\nroot_nodes after creation of p2\n";
	  	for(int i=0; i<root_nodes.size(); i++)
			{
			cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}
	  	ofstream out("ref_count.txt", ios::app);
	  	dm->printDAGAsDOTFile(p2, &out);

		bool test_delete_node = false;

	  	if(test_delete_node)
	  	{
			/* The following code can be used when deleteDeadNode is public */

			/*
	
			dm->decrementReferenceCount(p2);

			dm->getVectorOfDeadNodes(dead_nodes);

			cout<<"\ndead_nodes after decrementing ref.count of p2\n";
			for(int i=0; i<dead_nodes.size(); i++)
			{
				cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  		root_nodes = dm->getVectorOfRootNodes();
	  		cout<<"\nroot_nodes after decrementing ref.count of p2\n";
	  		for(int i=0; i<root_nodes.size(); i++)
			{
				cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}
	  		dm->printDAGAsDOTFile(p2, &out);

		
			cout<<"\ndeleting p2: "<<p2<<endl;
	
			bool ret_value = dm->deleteDeadNode(p2);
	
			if(!ret_value)
				{
					cout<<"\ncould not delete\n";
					exit(1);
				}			
	

	
			dm->getVectorOfDeadNodes(dead_nodes);
			cout<<"\ndead_nodes after deleting p2\n";
			for(int i=0; i<dead_nodes.size(); i++)
			{
				cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  		root_nodes = dm->getVectorOfRootNodes();
	  		cout<<"\nroot_nodes after deleting p2\n";
	  		for(int i=0; i<root_nodes.size(); i++)
			{
				cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}
	  		//dm->printDAGAsDOTFile(p2, &out);
			dm->printDAGAsDOTFile(p1, &out);	
			dm->printDAGAsDOTFile(x, &out);	
			dm->printDAGAsDOTFile(three, &out);	*/
	
	  	}
	  	else
	  	{
			cout<<"\nm_dagnode_count = "<<dm->getCountOfAllDAGNodesInDAGManager()<<endl;
			cout<<"\nm_memory_usage = "<<dm->getMemoryUsage()<<endl;
	
			dm->decrementReferenceCount(p2);
	
			dm->getVectorOfDeadNodes(dead_nodes);
			cout<<"\ndead_nodes after decrementing ref.count of p2\n";
			for(int i=0; i<dead_nodes.size(); i++)
			{	
				cout<<integerToString((long int)(dead_nodes[i]))<< "   " <<dead_nodes[i]->getLabel()<<endl;
			}
	  		root_nodes = dm->getVectorOfRootNodes();
	  		cout<<"\nroot_nodes after decrementing ref.count of p2\n";
		  	for(int i=0; i<root_nodes.size(); i++)
			{
				cout<<integerToString((long int)(root_nodes[i]))<< "   " <<root_nodes[i]->getLabel()<<endl;
			}  

			cout<<"\nm_dagnode_count = "<<dm->getCountOfAllDAGNodesInDAGManager()<<endl;
			cout<<"\nm_memory_usage = "<<dm->getMemoryUsage()<<endl;	
	 	}
	    }//else of if(use_smart_pointers)
  }// if(test_garbage_collector) ends here

  bool test_dag_reader = false;
  if(test_dag_reader) //working
	{

	  t_ConfigurationOptions config_options("config.txt");
  	  t_ExpressionManager *em = new t_ExpressionManager(config_options);
          BVManager* bvm = BVManager::getInstance();



  	//string reader = "((0b011 * x) + (0b100 * y) + (0b001 * z) + 0b010 == 0b000) && (0b1000 * y == 0b0000) && (0b1010 * y == 0b0000)  ";
  	string reader = "0b100 * y == 0b000";
  	t_Expression *ReaderExp; 
	string remaining;
	remaining = buildExpression(reader, em, ReaderExp); 
        em->printExpressionToFileAsDAG("ReaderExp", ReaderExp, cout);
  	cout<<"\nremaining = "<<remaining<<endl;	
	}// if(test_dag_reader)  ends here


  bool conjunction_input_from_file = false;
  if(conjunction_input_from_file)
	{

	  t_ConfigurationOptions config_options("config.txt");
  	  t_ExpressionManager *em = new t_ExpressionManager(config_options);
          BVManager* bvm = BVManager::getInstance();


	if (argc != 4) {
	    cout<<"Usage: "<<argv[0]<<" infilename machinename testlayer1|testlayer2|testlayer3|testproject\n",
	    exit(-1);
	  }

        ifstream* InputFile;
	InputFile = new ifstream();
    	InputFile->open(argv[1]);

	int layer_to_test;
	if(strcmp(argv[3], "testlayer1") == 0)
	{
		layer_to_test = 1;
	}
	else if(strcmp(argv[3], "testlayer2") == 0)
	{
		layer_to_test = 2;
	}
	else if(strcmp(argv[3], "testlayer3") == 0)
	{
		layer_to_test = 3;
	}
	else if(strcmp(argv[3], "testproject") == 0)
	{
		layer_to_test = 0;
	}
	else
	{
		cout<<"Usage: "<<argv[0]<<" infilename machinename testlayer1|testlayer2|testlayer3|testproject\n",
	    	exit(-1);
	}		

	ofstream* LayerStatsFile;
	LayerStatsFile = new ofstream();

	if(layer_to_test == 1)
	{
		LayerStatsFile->open("Layer1Statitics.txt", fstream::app);	
	}
	else if(layer_to_test == 2)
	{
		LayerStatsFile->open("Layer2Statitics.txt", fstream::app);
	}
	else if(layer_to_test == 3)
	{
		LayerStatsFile->open("Layer3Statitics.txt", fstream::app);
	}
	else if(layer_to_test == 0)
	{
		LayerStatsFile->open("ProjectStatitics.txt", fstream::app);
	}
	else
	{
		cout<<"Unknown value for layer_to_test\n",
	    	exit(-1);
	}

	t_HashTable <string, int> VariableList;
	t_HashTable <string, int> WidthTable;

	string eqz_var = "eqz";
	string diseqz_var = "diseqz";
	string leq_var = "leq";	

	unsigned number_constraints;
	unsigned total_number_variables;
	unsigned total_number_eliminate;
	vector<string> total_variables;
	vector<string> variables_to_eliminate;

	set<t_Expression*> EqzChildren;
	set<t_Expression*> DiseqzChildren;
	set<t_Expression*> LeqChildren;

	t_Expression* kandNode;

	*InputFile >> number_constraints;
	*InputFile >> total_number_variables;

	unsigned sum_variable_width = 0;
	int number_equalities = 0;
	int number_disequalities = 0;
	int number_inequalities = 0;

	struct timeval start_ms, finish_ms;
        unsigned long long int duration_ms;

	for(unsigned total_var_it = 0; total_var_it < total_number_variables; total_var_it++)
		{
		string variable;
		*InputFile >> variable;
		total_variables.push_back(variable);

		addEntryToVariableList(variable, total_var_it, VariableList);
		}
	
	for(unsigned total_var_it = 0; total_var_it < total_number_variables; total_var_it++)
		{
		unsigned variable_width;
		*InputFile >> variable_width;
		string variable = total_variables[total_var_it];

		addEntryToWidthTable(variable, variable_width, WidthTable);
		}

	*InputFile >> total_number_eliminate;	

	for(unsigned var_to_elim_it = 0; var_to_elim_it < total_number_eliminate; var_to_elim_it++)
		{
		string variable;
		*InputFile >> variable;
		variables_to_eliminate.push_back(variable);

		unsigned variable_width = getWidthOfVariable(variable, WidthTable);
		assert(variable_width > 0);
		sum_variable_width = sum_variable_width + variable_width;
		}	
	
	for(unsigned constr_it = 0; constr_it < number_constraints; constr_it++)
		{
		string constraint_type;
		unsigned constraint_width;
		unsigned number_variables;
		vector<string> variables;
		vector<bvatom> coefficients_left;
		bvatom constant_left;
		vector<bvatom> coefficients_right;
		bvatom constant_right;

		*InputFile >> constraint_type;
		*InputFile >> constraint_width;
		*InputFile >> number_variables;

		//cout << endl << constraint_type;
		//cout << endl << constraint_width;
		//cout << endl << number_variables;
		
		for(unsigned var_it = 0; var_it < number_variables; var_it++)
			{
			string variable;
			*InputFile >> variable;
			//cout << endl << variable;
			variables.push_back(variable);
			}

		if(constraint_type == "=" || constraint_type == "!=")
			{
			string constant_left_str;
			*InputFile >> constant_left_str;
			//cout << endl << constant_left_str;
			bvatom constant_left = bvm->getBVatom(constant_left_str.size(), constant_left_str);
			
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string coefficient_str;
				*InputFile >> coefficient_str;
				//cout << endl << coefficient_str;
				bvatom coefficient = bvm->getBVatom(coefficient_str.size(), coefficient_str);

				coefficients_left.push_back(coefficient);
				}

			// let's create the coefficient_map
			vector< pair< string, bvatom > > coefficient_map_left;
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string variable = variables[var_it];
				bvatom coefficient = coefficients_left[var_it];
				coefficient_map_left.push_back(make_pair(variable, coefficient));
				}

			t_Expression* kaddNode = CreateKaddNodeFromConstantAndCoefficientMap(constraint_width, constant_left, coefficient_map_left, em, VariableList, bvm);
			assert(kaddNode != NULL);

			if(constraint_type == "=")
				{	
				number_equalities++;
				t_Expression* eqzNode = CreateNode(eqz_var, kaddNode, em);
				assert(eqzNode != NULL);
				EqzChildren.insert(eqzNode);
				}
			else
				{
				number_disequalities++;
				t_Expression* disEqzNode = CreateNode(diseqz_var, kaddNode, em);
				assert(disEqzNode != NULL);
				DiseqzChildren.insert(disEqzNode);
				}			
			}
		else if(constraint_type == "<=")
			{
			string constant_left_str;
			*InputFile >> constant_left_str;
			//cout << endl << constant_left_str;
			bvatom constant_left = bvm->getBVatom(constant_left_str.size(), constant_left_str);
			
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string coefficient_str;
				*InputFile >> coefficient_str;
				//cout << endl << coefficient_str;
				bvatom coefficient = bvm->getBVatom(coefficient_str.size(), coefficient_str);

				coefficients_left.push_back(coefficient);	
				}

			string constant_right_str;
			*InputFile >> constant_right_str;
			//cout << endl << constant_right_str;
			bvatom constant_right = bvm->getBVatom(constant_right_str.size(), constant_right_str);
			
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string coefficient_str;
				*InputFile >> coefficient_str;
				//cout << endl << coefficient_str;
				bvatom coefficient = bvm->getBVatom(coefficient_str.size(), coefficient_str);

				coefficients_right.push_back(coefficient);					
				}

			// let's create the coefficient_maps
			vector< pair< string, bvatom > > coefficient_map_left;
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string variable = variables[var_it];
				bvatom coefficient = coefficients_left[var_it];
				coefficient_map_left.push_back(make_pair(variable, coefficient));
				}

			t_Expression* kaddNode_left = CreateKaddNodeFromConstantAndCoefficientMap(constraint_width, constant_left, coefficient_map_left, em, VariableList, bvm);
			assert(kaddNode_left != NULL);

			vector< pair< string, bvatom > > coefficient_map_right;
			for(unsigned var_it = 0; var_it < number_variables; var_it++)
				{
				string variable = variables[var_it];
				bvatom coefficient = coefficients_right[var_it];
				coefficient_map_right.push_back(make_pair(variable, coefficient));
				}

			t_Expression* kaddNode_right = CreateKaddNodeFromConstantAndCoefficientMap(constraint_width, constant_right, coefficient_map_right, em, VariableList, bvm);
			assert(kaddNode_right != NULL);

			t_Expression* leqNode = CreateNode(leq_var, kaddNode_left, kaddNode_right, em);
			assert(leqNode != NULL);
			LeqChildren.insert(leqNode);

			number_inequalities++;			
			}
		else
			{
			cout<<"\nUnknown constraint type from input file\n";
			exit(1);
			}				
		}//for 

		*LayerStatsFile << endl << argv[1] << "\t" << total_number_variables << "\t" << total_number_eliminate << "\t" << sum_variable_width;
		*LayerStatsFile << "\t" << number_equalities << "\t" << number_disequalities << "\t" << number_inequalities;

		
		kandNode = CreateKandNode(EqzChildren, DiseqzChildren, LeqChildren, em);
		assert(kandNode != NULL);


		//cout<<endl;
		//em->printExpressionToFileAsDAG("kand", kandNode, cout);
		//cout<<endl;
		//cout<<"\nvariables_to_eliminate = ";
		//for(unsigned var_to_elim_it = 0; var_to_elim_it < total_number_eliminate; var_to_elim_it++)
		//	{
		//	cout<<variables_to_eliminate[var_to_elim_it]<<", ";
		//	}
		//cout<<endl;

		bool usebvlibrary_in_layer2 = false;
				
		t_Project *proj = t_Project::getInstance(VariableList, WidthTable, usebvlibrary_in_layer2, em, bvm);

		if(layer_to_test == 1)
		{
			cout<<"\n\nLayer1 started\n\n";

			em->printExpressionToFileAsDAG("kand before layer2", kandNode, cout);
			
			gettimeofday (&start_ms, NULL);

			t_Expression* kandAfterLayer1 = proj->Layer1(kandNode, variables_to_eliminate);

			gettimeofday (&finish_ms, NULL);

			duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
			duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;

			if(kandAfterLayer1 == NULL)
				{
				cout<<"\nkandAfterLayer1 == NULL! Error inside proj->Layer1\n";
				exit(1);
				}
			else
				{
                                em->printExpressionToFileAsDAG("kand after layer1", kandAfterLayer1, cout);
				cout<<"\nLayer1 completed in "<<duration_ms<<" milli seconds\n";
				}
			cout<<endl;

			*LayerStatsFile << "\t" << duration_ms << "\t" << argv[2] << endl;
		}
		else if(layer_to_test == 2)
		{
			cout<<"\n\nLayer2 started\n\n";
			
			em->printExpressionToFileAsDAG("kand before layer2", kandNode, cout);

			gettimeofday (&start_ms, NULL);

			t_Expression* kandAfterLayer2 = proj->Layer2(kandNode, variables_to_eliminate);

			gettimeofday (&finish_ms, NULL);

			duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
			duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;

			if(kandAfterLayer2 == NULL)
				{
				cout<<"\nkandAfterLayer2 == NULL! Error inside proj->Layer2\n";
				exit(1);
				}
			else
				{
				em->printExpressionToFileAsDAG("kand after layer2", kandAfterLayer2, cout);
				cout<<"\nLayer2 completed in "<<duration_ms<<" milli seconds\n";
				}
			cout<<endl;

			*LayerStatsFile << "\t" << duration_ms << "\t" << argv[2];

			if(usebvlibrary_in_layer2)
			{
				*LayerStatsFile << "\tbv-library\n";
			}
			else
			{
				*LayerStatsFile << "\tmachine-arithmetic\n";
			}

		}
		else if(layer_to_test == 3)
		{
			cout<<"\n\nLayer3 started\n\n";

			em->printExpressionToFileAsDAG("kand before layer3", kandNode, cout);
			
			gettimeofday (&start_ms, NULL);

			t_Expression* resultOfLayer3 = proj->Layer3(kandNode, variables_to_eliminate);

			gettimeofday (&finish_ms, NULL);

			duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
			duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;

			if(resultOfLayer3 == NULL)
				{
				cout<<"\nresultOfLayer3 == NULL! Error inside proj->Layer3\n";
				exit(1);
				}
			else
				{
                                em->printExpressionToFileAsDAG("result of layer3", resultOfLayer3, cout);
				cout<<"\nLayer3 completed in "<<duration_ms<<" milli seconds\n";
				}
			cout<<endl;

			*LayerStatsFile << "\t" << duration_ms << "\t" << argv[2] << endl;
		}
		else if(layer_to_test == 0)
		{
			cout<<"\n\nProject started\n\n";

			em->printExpressionToFileAsDAG("kand before project", kandNode, cout);

			cout<<"\nvariables_to_eliminate = ";
			for(unsigned var_to_elim_it = 0; var_to_elim_it < total_number_eliminate; var_to_elim_it++)
			{
				cout<<variables_to_eliminate[var_to_elim_it]<<", ";
			}
			cout<<endl;
			
			gettimeofday (&start_ms, NULL);

			t_Expression* resultOfProject = proj->Project(kandNode, variables_to_eliminate);

			gettimeofday (&finish_ms, NULL);

			duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
			duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;

			if(resultOfProject == NULL)
				{
				cout<<"\nresultOfProject == NULL! Error inside proj->Project\n";
				exit(1);
				}
			else
				{
                                em->printExpressionToFileAsDAG("result of project", resultOfProject, cout);
				cout<<"\nProject completed in "<<duration_ms<<" milli seconds\n";
				}
			cout<<endl;

			*LayerStatsFile << "\t" << duration_ms << "\t" << argv[2] << endl;
		}
		

		InputFile->close();
		LayerStatsFile->close();	

	}//if(conjunction_input_from_file) ends here


  bool test_layer1_using_hardcoded_case = false;
  if(test_layer1_using_hardcoded_case)
	{

	t_ConfigurationOptions config_options("config.txt");
  	t_ExpressionManager *em = new t_ExpressionManager(config_options);
        BVManager* bvm = BVManager::getInstance();


	t_HashTable <string, int> VariableList;
	t_HashTable <string, int> WidthTable;

	string x_var = "x";
	string y_var = "y";
	string z_var = "z";	
	string m_var = "m";
	string n_var = "n";
	string p_var = "p";
	string a_var = "a";
	string b_var = "b";
	string c_var = "c";	
	string zero_var = "000";	
	string one_var = "001";	
	string two_var = "010";	
	string three_var = "011";	
	string four_var = "100";	
	string five_var = "101";	
	string six_var = "110";	
	string seven_var = "111";	
	string eqz_var = "eqz";
	string diseqz_var = "diseqz";
	string leq_var = "leq";	
	string mul_var = "bvmul";	
	string one_var_four_bit = "0001";
	string one_var_one_bit = "1";	

	addEntryToVariableList(y_var, 0, VariableList);
	addEntryToVariableList(x_var, 1, VariableList);
	addEntryToVariableList(z_var, 2, VariableList);
	addEntryToVariableList(m_var, 3, VariableList);
	addEntryToVariableList(n_var, 4, VariableList);
	addEntryToVariableList(p_var, 5, VariableList);
	addEntryToVariableList(a_var, 6, VariableList);
	addEntryToVariableList(b_var, 7, VariableList);
	addEntryToVariableList(c_var, 8, VariableList);

	addEntryToWidthTable(y_var, 3, WidthTable);
	addEntryToWidthTable(x_var, 3, WidthTable);
	addEntryToWidthTable(z_var, 3, WidthTable);
	addEntryToWidthTable(m_var, 4, WidthTable);
	addEntryToWidthTable(n_var, 4, WidthTable);
	addEntryToWidthTable(p_var, 4, WidthTable);
	addEntryToWidthTable(a_var, 1, WidthTable);
	addEntryToWidthTable(b_var, 1, WidthTable);
	addEntryToWidthTable(c_var, 1, WidthTable);

	t_Project *proj = t_Project::getInstance(VariableList, WidthTable, false, em, bvm);

	//variables
	t_Expression* x = CreateSymbol(x_var, 3, em);
	t_Expression* y = CreateSymbol(y_var, 3, em);
	t_Expression* z = CreateSymbol(z_var, 3, em);

	t_Expression* m = CreateSymbol(m_var, 4, em);
	t_Expression* n = CreateSymbol(n_var, 4, em);
	t_Expression* p = CreateSymbol(p_var, 4, em);

	t_Expression* a = CreateSymbol(a_var, 1, em);
	t_Expression* b = CreateSymbol(b_var, 1, em);
	t_Expression* c = CreateSymbol(c_var, 1, em);

	//constants
	t_Expression* zero = CreateConstant(zero_var, 3, em);
	t_Expression* one = CreateConstant(one_var, 3, em);
	t_Expression* two = CreateConstant(two_var, 3, em);
	t_Expression* three = CreateConstant(three_var, 3, em);
	t_Expression* five = CreateConstant(five_var, 3, em);
	t_Expression* four = CreateConstant(four_var, 3, em);
	t_Expression* six = CreateConstant(six_var, 3, em);
	t_Expression* seven = CreateConstant(seven_var, 3, em);

	t_Expression* one_four_bit = CreateConstant(one_var_four_bit, 4, em);

	t_Expression* one_one_bit = CreateConstant(one_var_one_bit, 1, em);

	//monoms
	t_Expression *one_x = CreateTerm(mul_var, 3, one, x, em);
	t_Expression *two_x = CreateTerm(mul_var, 3, two, x, em);
	t_Expression *three_x = CreateTerm(mul_var, 3, three, x, em);
	t_Expression *four_x = CreateTerm(mul_var, 3, four, x, em);
	t_Expression *six_x = CreateTerm(mul_var, 3, six, x, em);
	t_Expression *zero_y = CreateTerm(mul_var, 3, zero, y, em);
	t_Expression *one_y = CreateTerm(mul_var, 3, one, y, em);
	t_Expression *two_y = CreateTerm(mul_var, 3, two, y, em);
	t_Expression *three_y = CreateTerm(mul_var, 3, three, y, em);
	t_Expression *five_y = CreateTerm(mul_var, 3, five, y, em);
	t_Expression *six_y = CreateTerm(mul_var, 3, six, y, em);	
	t_Expression *one_z = CreateTerm(mul_var, 3, one, z, em);
	t_Expression *three_z = CreateTerm(mul_var, 3, three, z, em);

	t_Expression *one_m = CreateTerm(mul_var, 4, one_four_bit, m, em);
	t_Expression *one_n = CreateTerm(mul_var, 4, one_four_bit, n, em);
	t_Expression *one_p = CreateTerm(mul_var, 4, one_four_bit, p, em);
	
	t_Expression *one_a = CreateTerm(mul_var, 1, one_one_bit, a, em);
	t_Expression *one_b = CreateTerm(mul_var, 1, one_one_bit, b, em);
	t_Expression *one_c = CreateTerm(mul_var, 1, one_one_bit, c, em);

	//kadds
	vector<t_Expression*> SortedChildren;
	SortedChildren.push_back(two_y);
	SortedChildren.push_back(two_x);
	t_Expression *kadd1 = CreateKaddNode(3, SortedChildren, em, VariableList, six); //kadd1: 2y+2x+6 

	SortedChildren.clear();
	SortedChildren.push_back(two_y);
	SortedChildren.push_back(four_x);
	t_Expression *kadd2 = CreateKaddNode(3, SortedChildren, em, VariableList, four); //kadd2: 2y+4x+4

  
        SortedChildren.clear();
	SortedChildren.push_back(two_y);
	SortedChildren.push_back(six_x);
	t_Expression *kadd3 = CreateKaddNode(3, SortedChildren, em, VariableList); //kadd3: 6x+2y


	SortedChildren.clear();
	SortedChildren.push_back(two_y);
	SortedChildren.push_back(one_x);
	t_Expression *kadd4 = CreateKaddNode(3, SortedChildren, em, VariableList, six); //kadd4: 2y+x+6


	SortedChildren.clear();
	SortedChildren.push_back(two_y);
	SortedChildren.push_back(four_x);
	t_Expression *kadd5 = CreateKaddNode(3, SortedChildren, em, VariableList, three); //kadd5: 2y+4x+3


	SortedChildren.clear();
	SortedChildren.push_back(one_m);
	SortedChildren.push_back(one_n);
	t_Expression *kadd6 = CreateKaddNode(4, SortedChildren, em, VariableList); //kadd6: m+n

		
	SortedChildren.clear();
	SortedChildren.push_back(one_n);
	SortedChildren.push_back(one_p);
	t_Expression *kadd7 = CreateKaddNode(4, SortedChildren, em, VariableList); //kadd7: n+p


	SortedChildren.clear();
	SortedChildren.push_back(one_a);
	SortedChildren.push_back(one_b);
	t_Expression *kadd8 = CreateKaddNode(1, SortedChildren, em, VariableList); //kadd8: a+b

		
	SortedChildren.clear();
	SortedChildren.push_back(one_b);
	SortedChildren.push_back(one_c);
	t_Expression *kadd9 = CreateKaddNode(1, SortedChildren, em, VariableList); //kadd9: b+c

	//lmes
	t_Expression *eqz1 = CreateNode(eqz_var, kadd1, em); //eqz1: 2y+2x+6 = 0 mod 8
	t_Expression *eqz2 = CreateNode(eqz_var, kadd2, em); //eqz2: 2y+4x+4 = 0 mod 8
	t_Expression *eqz3 = CreateNode(eqz_var, kadd6, em); //eqz3: m+n = 0 mod 16
	t_Expression *eqz4 = CreateNode(eqz_var, kadd8, em); //eqz3: a+b = 0 mod 1

	
	//lmds
	t_Expression *diseqz1 = CreateNode(diseqz_var, kadd3, em); //diseqz1: 6x+2y <> 0 mod 8
	t_Expression *diseqz2 = CreateNode(diseqz_var, kadd7, em); //diseqz2: n+p <> 0 mod 16
	t_Expression *diseqz3 = CreateNode(diseqz_var, kadd9, em); //diseqz2: b+c <> 0 mod 1

	
	//lmis
	t_Expression *leq1 = CreateNode(leq_var, kadd4, kadd5, em); //leq1: 2y+x+6 <= 2y+4x+3 mod 8
	

	//kand
	set<t_Expression*> EqzChildren;
	set<t_Expression*> DiseqzChildren;
	set<t_Expression*> LteChildren;

	EqzChildren.insert(eqz1);
	EqzChildren.insert(eqz2);
	EqzChildren.insert(eqz3);
	EqzChildren.insert(eqz4);
	DiseqzChildren.insert(diseqz1);
	DiseqzChildren.insert(diseqz2);
	DiseqzChildren.insert(diseqz3);
	LteChildren.insert(leq1);
	t_Expression* kand1 = CreateKandNode(EqzChildren, DiseqzChildren, LteChildren, em);
	
	bool test_print_smt = false;
	
	if(test_print_smt)
		{
		string logeq = "logeq";
		t_Expression* logeq1 = CreateNode(logeq, one_a, one_b, em);
		t_Expression* logeq2 = CreateNode(logeq, one_b, one_c, em);
		t_Expression* logeq3 = CreateNode(logeq, one_a, one_c, em);		

		string logand = "logand";
		vector<t_Expression*> logand_children;
		//logand_children.push_back(eqz1);
		//logand_children.push_back(diseqz1);
		//logand_children.push_back(leq1);
		logand_children.push_back(logeq1);
		logand_children.push_back(logeq2);
		logand_children.push_back(logeq3);
		t_Expression* and1 = CreateNode(logand, logand_children, em); 

		// unsat case
		SortedChildren.clear();
		SortedChildren.push_back(two_y);
		t_Expression *kadd_new = CreateKaddNode(3, SortedChildren, em, VariableList, one); //kadd_new: 2y+1
		t_Expression *eqz_new = CreateNode(eqz_var, kadd_new, em); //eqz_new: 2y+1 = 0 mod 8


		set<t_Expression*> ConstraintsToPrint;
		ConstraintsToPrint.insert(eqz_new);
		//ConstraintsToPrint.insert(and1);
		//ConstraintsToPrint.insert(logeq1);
		em->printExpressionsToFileInSMT(ConstraintsToPrint, "", "layer.smt");

		


		bool sat;
		t_solver solver = stp;
		map<string, string> model;
		bool model_found = obtainModelOfFormula(eqz_new, sat, solver, model, em);		
		assert(model_found);
		cout << "sat = "<<sat << endl;
		cout << "model" << endl;
		for(map<string, string>::iterator mit = model.begin(); mit != model.end(); mit++)
			{
			cout<<endl<<mit->first<<"\t"<<mit->second;
			}
		}

	bool test_evaluation = false;
	
	if(test_evaluation)
		{
		map<string, string> Model;
		Model.insert(make_pair("x", "001"));
		Model.insert(make_pair("y", "001"));

		bool result;
		bool evaluated = evaluateLMC(diseqz1, Model, result, em, bvm, WidthTable);

		assert(evaluated);

		if(result)
			cout<<"\nconstraint true\n";
		else
			cout<<"\nconstraint false\n";


		t_HashTable <unsigned long long int, pair<bool, set<t_Expression*> > > Temp_HT;	

		unsigned long long int key = 123;
		bool result_1 = true;
		set<t_Expression*> result_2;
		result_2.insert(eqz1);
		result_2.insert(leq1);

		t_HTStatusValue <pair<bool, set<t_Expression*> > > insert_result = Temp_HT.hashtable_insert(key, make_pair(result_1, result_2));
		if (insert_result.success())
            		{
                		t_HTStatusValue <pair<bool, set<t_Expression*> > > result_search = Temp_HT.hashtable_search(key);
				if(result_search.success())
    					{			
						//cout<<(result_search.getValue()).first << "\t" << (result_search.getValue()).second << endl;
						cout<<(result_search.getValue()).first << endl;
						displaySetOfExpressionsOnScreen("second", (result_search.getValue()).second, em);
					}
				else
					{
						cout<<"\nError in searching\n";		
					}
            		}
        	else
            		{
                		cout<<"\nError in insertion\n";				
            		}	
		
		exit(1);	
		}

	bool test_monniaux = true;
	if(test_monniaux)
		{
		bool usebvlibrary_in_layer2 = true;
		t_Monniaux *mon = t_Monniaux::getInstance(VariableList, WidthTable, usebvlibrary_in_layer2, em, bvm);
		t_solver solver = stp;
		vector<string> Variables;

		string logor = "logor";
		string logand = "logand";
		string lognot = "lognot";
		string leq = "leq";

		SortedChildren.clear();
		t_Expression *kadd_two = CreateKaddNode(3, SortedChildren, em, VariableList, two); //kadd_two: 2
		t_Expression *kadd_zero = CreateKaddNode(3, SortedChildren, em, VariableList, zero); //kadd_zero: 0
		t_Expression *kadd_seven = CreateKaddNode(3, SortedChildren, em, VariableList, seven); //kadd_seven: 7
		t_Expression *leq_mon1 = CreateNode(leq, kadd3, kadd_two, em); //leq_mon1:  6x+2y <= 2 mod 8
		t_Expression *leq_mon2 = CreateNode(leq, kadd_two, kadd3, em); //leq_mon2:  2 <= 6x+2y mod 8
		t_Expression *leq_mon3 = CreateNode(leq, kadd3, kadd_seven, em); //leq_mon3:  6x+2y <= 7 mod 8

		vector<t_Expression*> logand_children;
		logand_children.push_back(eqz1);
		logand_children.push_back(eqz2);
		t_Expression* logand1 = CreateNode(logand, logand_children, em);

		logand_children.clear();
		logand_children.push_back(eqz1);
		logand_children.push_back(diseqz1);
		t_Expression* logand2 = CreateNode(logand, logand_children, em);

		vector<t_Expression*> logor_children;
		logor_children.push_back(logand1);
		logor_children.push_back(logand2);
		t_Expression* logor1 = CreateNode(logor, logor_children, em);		

		t_Expression* final = logor1;
		Variables.push_back("x");

		t_Expression* result_monniaux = mon->Monniaux(final, Variables, solver);
		assert(result_monniaux != NULL);
		em->printExpressionToFileAsDAG("result_monniaux", result_monniaux, cout);

		exit(1);
		}


	int WhichCallToLayer1 = 1;
	int WhichOrderToEliminate = 2;
	
	vector<string> Variables;

	if(WhichCallToLayer1 == 1)
		{
		em->printExpressionToFileAsDAG("kand1", kand1, cout);
				
		if(WhichOrderToEliminate == 0)
			{
			Variables.push_back("x");
			Variables.push_back("y");
			Variables.push_back("z");
			Variables.push_back("n");
			Variables.push_back("b");
			}
		else if(WhichOrderToEliminate == 1)
			{
			Variables.push_back("y");
			Variables.push_back("x");
			Variables.push_back("z");
			Variables.push_back("n");
			Variables.push_back("b");
			}
		else
			{
			Variables.push_back("b");
			Variables.push_back("n");
			Variables.push_back("x");
			Variables.push_back("z");
			Variables.push_back("y");
			}

		t_Expression* kandAfterLayer1 = proj->Layer1(kand1, Variables);
		

		if(kandAfterLayer1 == NULL)
			{
			cout<<"\nkandAfterLayer1 == NULL! Error inside proj->Layer1\n";
			exit(1);
			}
		else
			{
			em->printExpressionToFileAsDAG("kand1 after layer1", kandAfterLayer1, cout);
			}

		bool test_hash_table = true;
		
		if(test_hash_table)
			{
			t_Expression* kandAfterLayer2 = proj->Layer1(kand1, Variables);
			}

		}// if(WhichCallToLayer1 == 1) ends here	

       	//delete proj;

	}// if(test_layer1_using_hardcoded_case) ends here

  bool boolean_input_from_smt_file = false;
  if(boolean_input_from_smt_file)
	{
		if (argc != 2) {
		    cout<<"Usage: "<<argv[0]<<" infilename\n",
		    exit(-1);
		  }

		string smt_filename = strdup(argv[1]);
		FILE *fp = fopen(smt_filename.c_str(), "r");
		if (fp == NULL)
		{
		    cerr << "ERROR : " << smt_filename << " Doesnot Exists " << endl;
		    exit(-1);
		}

		extern t_ExpressionManager *em;
          	BVManager* bvm = BVManager::getInstance();

		extern FILE *SMTin;
		extern int SMTparse();

		extern t_HashTable <string, int> WidthTable;
		extern vector<t_Expression*> root;
	        extern set<string> VarSetToElim;

		SMTin = fp;
		SMTparse();       
  
		set<t_Expression*> ConstraintsToPrint;
		cout<<"\nroot\n";
		for(int i = 0; i < root.size(); i++)
		{
			assert(root[i] != NULL);
			em->printExpressionToFileAsDAG("root[i]", root[i], cout);
			cout<<endl;
		
			ConstraintsToPrint.insert(root[i]);				
		}
		em->printExpressionsToFileInSMT(ConstraintsToPrint, "", "echo.smt");
		
                displaySetOfStringsOnScreen("VarSetToElim", VarSetToElim);

		
  	} // if(boolean_input_from_smt_file) ends here

  bool test_skolem_function_generator = true;
  if(test_skolem_function_generator)
	{
		#ifdef DEBUG_SKOLEM
    		cout << "Staring Project..." << endl;
		#endif

		bool input_from_command_line = true;
		if(input_from_command_line) 
		{
			// read the command-line args and set the configuration options appropriately
			cout << "Reading the command-line args and setting the configuration options appropriately..." << endl;		
			readCommandLineArguments(argc, argv); 
		}
		else
		{    
			// read the confguration file and set the configuration options appropriately
			cout << "Reading the confguration file and setting the configuration options appropriately..." << endl;
			readConfigFile(); 
		}

	    	ABC* abcObj;
		abcObj = ABC::getSingleton();
		assert(abcObj != NULL);		
    
		Abc_Frame_t* abcFrame = abcObj->getAbcFrame();
		assert(abcFrame != NULL);

		extern t_ExpressionManager *em;

		bool debug = false;

		if(use_aig_manager)
		{

			bool debug_before_skf_generation = false;
			bool debug_after_skf_generation = false;

			set<Aig_Obj_t*> Factors;
			list<string> VariablesToEliminate;
			set<Aig_Obj_t*> RHS_of_Factors;
			map<string, Aig_Obj_t*> Output_String_to_RHS_of_Factors;
			map<Aig_Obj_t*, Aig_Obj_t*> Output_Object_to_RHS_of_Factors;
			map<Aig_Obj_t*, Aig_Obj_t*> Output_Object_to_RHS_of_PrimaryOutputs;

			vector< list<string> > VariablesToEliminateForGameBenchmarks;
			char TypeOfInnerQuantifier;

			int external_skolem_total_size;
			int external_skolem_number_of_vars;
			int external_skolem_max_size;
			float external_skolem_avg_size;			

			Aig_Man_t* aig_manager;

			cout << "Reading the original factors and variables to be eliminated..." << endl;	

			if(benchmark_type == "crafted")
			{
				assert(problem_kind == "variable_elimination");

				obtainVariablesToEliminate(VariablesToEliminate);

				if(apply_tsietin_encoding_on_benchmarks)
				{
					obtainFactorsThroughTsietin(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminate);
				}
				else
				{
					obtainFactors(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminate);				 
				}
			}
			else if(benchmark_type == "generated")
			{
				assert(problem_kind == "variable_elimination");

				if(apply_tsietin_encoding_on_benchmarks)
				{
					obtainFactorsThroughTsietinAndVariablesToEliminateFromGeneratedBenchmark(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminate);					
				}
				else
				{
					obtainFactorsAndVariablesToEliminateFromGeneratedBenchmark(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminate);				 
				}
			}
			else if(benchmark_type == "hwmcc-2010" || benchmark_type == "hwmcc-2012")
			{
				assert(problem_kind == "variable_elimination" || problem_kind == "graph_decomposition" || problem_kind == "benchmark_generation");

				if(problem_kind == "variable_elimination")
				{
					obtainFactorsAndVariablesToEliminatFromHWMCCFile(abcObj, abcFrame, Factors, VariablesToEliminate, aig_manager);		
				}
				else if(problem_kind == "graph_decomposition")
				{
					obtainFactorsAndVariablesToEliminatFromHWMCCFile(abcObj, abcFrame, Factors, RHS_of_Factors, VariablesToEliminate, Output_Object_to_RHS_of_Factors, Output_Object_to_RHS_of_PrimaryOutputs, aig_manager);		
				}
				else
				{
					obtainFactorsAndVariablesToEliminatFromHWMCCFile(abcObj, abcFrame, Factors, Output_String_to_RHS_of_Factors, VariablesToEliminate, aig_manager);
				}
			}
			else if(benchmark_type == "iscas-89")
			{
				//obtainFactorsAndVariablesToEliminatFromISCASFile(abcObj, abcFrame, Factors, VariablesToEliminate, em);	
				//cout << "\nExiting after reading\n"; exit(1); // for debugging

				cout << "AIG Manager based reading is not implemented for BENCHMARK-TYPE "<< benchmark_type << endl;
				assert(false);

			}
			else if(benchmark_type == "qdimacs")
			{
				assert(problem_kind == "variable_elimination");

				obtainFactorsAndVariablesToEliminatFromQdimacsFile(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminate);	
				//Aig_ManShow(aig_manager, 0, NULL); 
				//assert(false);	
			}
			else if(benchmark_type == "game")
			{
				assert(problem_kind == "variable_elimination");

				obtainFactorsAndVariablesToEliminatFromGameQdimacsFile(abcObj, abcFrame, Factors, aig_manager, VariablesToEliminateForGameBenchmarks, TypeOfInnerQuantifier);				
	
				//Aig_ManShow(aig_manager, 0, NULL); 				
			}
			else if(benchmark_type == "external_skolem")
			{
				assert(problem_kind == "print_stats");

				readSkolemFunctionsAndGetTheirSizes(abcObj, abcFrame, aig_manager, external_skolem_total_size,  external_skolem_number_of_vars, external_skolem_max_size, external_skolem_avg_size);	
				//Aig_ManShow(aig_manager, 0, NULL); 				
			}
			else
			{
				cout << "Value of BENCHMARK-TYPE is "<< benchmark_type << endl;
				assert(false && "Invalid Value");
			}

			if(debug_before_skf_generation) // place to test new helper.cpp functions
			{

				bool test_sat_solving = false;
				bool test_interpolant_generation = false;
				bool test_incremental_sat_solving = false;
				bool test_unsatcore_generation = false;
				bool test_qbf_solving = false;
				bool test_composes = false;
				bool test_dontcare_optimization = true;
				
				if(test_dontcare_optimization)
				{
					//testDontCareOptimization(abcObj, abcFrame);

					set<Aig_Obj_t*>::iterator Factors_it = Factors.begin();
					Aig_Obj_t* alpha = *Factors_it;
					Factors_it++;
					Aig_Obj_t* beta = *Factors_it;
					string alpha_file = "alpha.v";
					string beta_file  = "beta.v";
					writeFormulaToFile(aig_manager, alpha, alpha_file);
					writeFormulaToFile(aig_manager, beta, beta_file);

					set<string> support_alpha;
					computeSupport(alpha, support_alpha, aig_manager);
					set<string> support_beta;
					computeSupport(beta, support_beta, aig_manager);

					set_union(support_alpha.begin(), support_alpha.end(), support_beta.begin(), support_beta.end(),inserter(original_variables, original_variables.begin()));

					Aig_Obj_t* optimized_alpha = performDontCareOptimization(aig_manager, alpha, beta);
					writeFormulaToFile(aig_manager, optimized_alpha, "optimized_alpha", ".v", 0, 0);
				}
				else if(test_composes)
				{
					set<Aig_Obj_t*>::iterator Factors_it = Factors.begin();
					Aig_Obj_t* alpha = *Factors_it;
					Factors_it++;
					Aig_Obj_t* beta = *Factors_it;
					string alpha_file = "alpha.v";
					string beta_file  = "beta.v";
					writeFormulaToFile(aig_manager, alpha, alpha_file);
					writeFormulaToFile(aig_manager, beta, beta_file);

					string a_string = "a";
					Aig_Obj_t* alpha_composed_beta = ReplaceLeafByExpression(beta, a_string, alpha, aig_manager);
					Aig_Obj_t* zero_composed_beta = ReplaceLeafByExpression(beta, a_string, createFalse(aig_manager), aig_manager);
					Aig_Obj_t* one_composed_beta = ReplaceLeafByExpression(beta, a_string, createTrue(aig_manager), aig_manager);

					string alpha_composed_beta_file = "alpha_composed_beta.v";
					string zero_composed_beta_file  = "zero_composed_beta.v";
					string one_composed_beta_file  = "one_composed_beta.v";
					string alpha_after_composes_file = "alpha_after_composes.v";
					string beta_after_composes_file  = "beta_after_composes.v";
					writeFormulaToFile(aig_manager, alpha_composed_beta, alpha_composed_beta_file);
					writeFormulaToFile(aig_manager, zero_composed_beta, zero_composed_beta_file);
					writeFormulaToFile(aig_manager, one_composed_beta, one_composed_beta_file);
					writeFormulaToFile(aig_manager, alpha, alpha_after_composes_file);
					writeFormulaToFile(aig_manager, beta, beta_after_composes_file);

				}
				else if(test_sat_solving)
				{
					Aig_Obj_t* and_of_factors = createAnd(Factors, aig_manager);
					assert(and_of_factors != NULL);

				
					unsigned long long int solver_ms;
					struct timeval solver_start_ms, solver_finish_ms;

					vector< vector<int> > CNF;
					vector< vector<int> > Temp_CNF;
					int top_label = getCNF(aig_manager, and_of_factors, CNF);
					vector<int> clause_1;
					clause_1.push_back(top_label);
					CNF.push_back(clause_1);
	
					int number_of_variables = LabelCount-1;
					int number_of_clauses = CNF.size();

					cout << "\nsize of dag = " << computeSize(and_of_factors, aig_manager) << endl;

					printf( "CNF: Variables = %6d. Clauses = %7d. ", number_of_variables, number_of_clauses );

					string cnf_filename = "debug.cnf";
					writeCNFToFile(CNF, Temp_CNF, number_of_variables, number_of_clauses, cnf_filename);

					map<string, int> Model;
					gettimeofday (&solver_start_ms, NULL); 	
					bool result_of_exactnesscheck = giveCNFFiletoSATSolverAndQueryForSatisfiability(cnf_filename, Model);
					gettimeofday (&solver_finish_ms, NULL);
					solver_ms = solver_finish_ms.tv_sec * 1000 + solver_finish_ms.tv_usec / 1000;
					solver_ms -= solver_start_ms.tv_sec * 1000 + solver_start_ms.tv_usec / 1000;
					cout << "\nexternal-solver finished in " << solver_ms << " milliseconds\n";
				
					Model.clear();
					//result_of_exactnesscheck = isSat(aig_manager, and_of_factors, Model);
				}
				else if(test_interpolant_generation)
				{
					set<Aig_Obj_t*>::iterator Factors_it = Factors.begin();
					Aig_Obj_t* alpha = *Factors_it;
					Factors_it++;
					Aig_Obj_t* beta = *Factors_it;
					string alpha_file = "alpha.v";
					string beta_file  = "beta.v";
					writeFormulaToFile(aig_manager, alpha, alpha_file);
					writeFormulaToFile(aig_manager, beta, beta_file);

					Aig_Obj_t* Interpolant = Interpolate(aig_manager, alpha, beta);
					writeFormulaToFile(aig_manager, Interpolant, "Interpolant", ".v", 0, 0);
				}
				else if(test_incremental_sat_solving)
				{
					int testing_inc = 2;
					if(testing_inc == 1)
					{
						sat_solver* pSat;
						pSat = sat_solver_new();

						int iVar = 1;
						int iVar0 = 2;
						int iVar1 = 3;
						int iVar2 = 4;
						int fCompl0 = 0;
						int fCompl1 = 0;
						int fCompl = 0;
					
						sat_solver_setnvars( pSat, 3 );
						sat_solver_add_and(pSat, iVar, iVar0, iVar1, fCompl0, fCompl1, fCompl );
						//sat_solver_add_const(pSat, iVar2, fCompl );
						cout << endl << sat_solver_nvars(pSat) << "\t" << sat_solver_nclauses(pSat) << endl;
						//Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
						// This function is not printing all clauses. How to debug?
					
					
						int Lit = toLitCond( iVar2,  0);
						int status = sat_solver_solve( pSat, &Lit, &Lit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
					

						if ( status == l_False )
						{
							cout << "\nFormula is unsat\n";
						}
						else if ( status == l_True )
						{
							cout << "\nFormula is sat; get the CEX\n";  

						}
						else
						{
							cout << "\nUnknown value " << status <<" returned from solver\n";
						}

						sat_solver_delete(pSat);
					}
					else if(testing_inc == 2)
					{
						sat_solver* pSat_for_exactness_check = sat_solver_new();
						set<Aig_Obj_t*>::iterator Factors_it = Factors.begin();
						Aig_Obj_t* alpha = *Factors_it;
						Factors_it++;
						Aig_Obj_t* beta = *Factors_it;
						//Factors_it++;
						//Aig_Obj_t* gamma = *Factors_it;

						string alpha_file = "alpha.v";
						string beta_file  = "beta.v";
						//string gamma_file  = "gamma.v";
						writeFormulaToFile(aig_manager, alpha, alpha_file);
						writeFormulaToFile(aig_manager, beta, beta_file);
						//writeFormulaToFile(aig_manager, gamma, gamma_file);
						
						map<string, int> Model;
						unsigned long long int cnf_time;
						int formula_size;
						unsigned long long int simplification_time;
						vector<Aig_Obj_t*> positive_assumptions_in_exactness_check;
						vector<Aig_Obj_t*> negative_assumptions_in_exactness_check;

						string a_string = "a";
						string b_string = "b";
						string c_string = "c";

						Aig_Obj_t* a_obj = Ci_name_to_Ci_object_map[a_string];
						Aig_Obj_t* b_obj = Ci_name_to_Ci_object_map[b_string];
						Aig_Obj_t* c_obj = Ci_name_to_Ci_object_map[c_string];

						//negative_assumptions_in_exactness_check.push_back(b_obj);
						
						bool result_of_exactnesscheck = isExactnessCheckSatisfiable(aig_manager, alpha, Model, cnf_time, formula_size, simplification_time, positive_assumptions_in_exactness_check, negative_assumptions_in_exactness_check, pSat_for_exactness_check, IncrementalLabelTableForExactnessCheck, IncrementalLabelCountForExactnessCheck, Ci_name_to_Ci_label_mapForExactnessCheck, Ci_label_to_Ci_name_mapForExactnessCheck);

						/* This is not working 
						//addIncrementToExactnessCheck(aig_manager, beta);
						//result_of_exactnesscheck = isExactnessCheckSatisfiable(aig_manager, createTrue(aig_manager), Model, cnf_time, formula_size, simplification_time, positive_assumptions_in_exactness_check, negative_assumptions_in_exactness_check); */
						
						//negative_assumptions_in_exactness_check.push_back(c_obj);
					
						result_of_exactnesscheck = isExactnessCheckSatisfiable(aig_manager, beta, Model, cnf_time, formula_size, simplification_time, positive_assumptions_in_exactness_check, negative_assumptions_in_exactness_check, pSat_for_exactness_check, IncrementalLabelTableForExactnessCheck, IncrementalLabelCountForExactnessCheck, Ci_name_to_Ci_label_mapForExactnessCheck, Ci_label_to_Ci_name_mapForExactnessCheck);

						//result_of_exactnesscheck = isExactnessCheckSatisfiable(aig_manager, gamma, Model, cnf_time, formula_size, simplification_time, positive_assumptions_in_exactness_check, negative_assumptions_in_exactness_check);

						sat_solver_delete(pSat_for_exactness_check);
						
					}
				}
				else if(test_unsatcore_generation)
				{
					int testing_unsat = 2;

					if(testing_unsat == 1)
					{
						Aig_Obj_t* and_of_factors = createAnd(Factors, aig_manager);
						assert(and_of_factors != NULL);
					
						string and_of_factors_file  = "and_of_factors.v";
						writeFormulaToFile(aig_manager, and_of_factors, and_of_factors_file);
					
						//unsatCore(aig_manager, and_of_factors);
					
						map<string, int> Model;
						unsigned long long int cnf_time;
						int formula_size;
						unsigned long long int simplification_time;
						bool sat_result = isSat(aig_manager, and_of_factors, Model, cnf_time, formula_size, simplification_time);
						Aig_ManShow(aig_manager, 0, NULL); 
					}
					else
					{
						Aig_Obj_t* and_of_factors = createAnd(Factors, aig_manager);
						assert(and_of_factors != NULL);

						string x1_string = "x1";
						string x4_string = "x4";
						string x5_string = "x5";
						Aig_Obj_t* x1_obj = Ci_name_to_Ci_object_map[x1_string];
						Aig_Obj_t* neg_x1_obj = createNot(x1_obj, aig_manager);
						Aig_Obj_t* x4_obj = Ci_name_to_Ci_object_map[x4_string];
						Aig_Obj_t* x5_obj = Ci_name_to_Ci_object_map[x5_string];
						Aig_Obj_t* assignment;
						assignment = createAnd(neg_x1_obj, x4_obj, aig_manager);
						assignment = createAnd(assignment, x5_obj, aig_manager);

						set<Aig_Obj_t*> positive_variables;
						positive_variables.insert(x4_obj);
						//positive_variables.insert(x5_obj);
						set<Aig_Obj_t*> negative_variables;
						negative_variables.insert(x1_obj);

						//and_of_factors = createAnd(and_of_factors, assignment, aig_manager);			
					
						string and_of_factors_file  = "and_of_factors.v";
						writeFormulaToFile(aig_manager, and_of_factors, and_of_factors_file);
					
						set<string> variables_in_unsat_core;
						unsatCore(aig_manager, and_of_factors, positive_variables, negative_variables, variables_in_unsat_core);
					
						//Aig_ManShow(aig_manager, 0, NULL); 
						
					}
				}
				else if(test_qbf_solving)
				{
					set<Aig_Obj_t*>::iterator Factors_it = Factors.begin();
					Aig_Obj_t* alpha = *Factors_it;
					Factors_it++;
					Aig_Obj_t* beta = *Factors_it;

					string alpha_file = "alpha.v";
					string beta_file  = "beta.v";
					writeFormulaToFile(aig_manager, alpha, alpha_file);
					writeFormulaToFile(aig_manager, beta, beta_file);

					isQbfSat(alpha, beta, VariablesToEliminate, aig_manager);
					Aig_ManShow(aig_manager, 0, NULL); 
				}
				
				
				cout << "\nTesting done !!";
				assert(false);
			}

			AIGBasedSkolem* AIGBasedSkolemObj = new AIGBasedSkolem(aig_manager);
			assert(AIGBasedSkolemObj != NULL);

			// set the logfile_prefix
			logfile_prefix = benchmark_name_without_extension;
			if(use_bloqqer)
			{
				logfile_prefix += "_bloqqer_";
			}
			else if(benchmark_type == "external_skolem")
			{
				logfile_prefix += "_externalskolem_";	
			}
			else if(enable_cegar)
			{
				logfile_prefix += "_cegar";

				if(use_mu_based_scheme_with_optimizations_in_cegar && unify_code_for_mu_based_scheme_in_cegar)
				{

					if(use_assumptions_in_unified_cegar)
					{
						logfile_prefix += "_optimized";
					}
					else
					{
						logfile_prefix += "_unoptimized";
					}
				
					if(use_bads_in_unified_cegar)
					{
						logfile_prefix += "_withbads";
					}
					else
					{
						logfile_prefix += "_withnegf";
					}


					if(accumulate_formulae_in_cbzero_in_cegar)
					{
						logfile_prefix += "_withaccumulate_";
					}
					else
					{
						logfile_prefix += "_noaccumulate_";
					}
				}
			}
			else
			{
				logfile_prefix += "_monolithic";	
				if(compute_quantifier_eliminated_result_using_skolem_functions)
				{
					logfile_prefix += "_compositionqe";
				}
				else
				{
					logfile_prefix += "_bddlikeqe";
				}

				if(use_interpolant_as_skolem_function)
				{
					logfile_prefix += "_interpolantskf";
				}
				else
				{
					logfile_prefix += "_cofactorskf";
				}
				
				if(skolem_function_type_in_jiang == "cofactorone")
				{
					logfile_prefix += "_cofactorone_";
				}
				else
				{
					logfile_prefix += "_bothcofactors_";
				}
			}
			

			#ifdef RECORD_KEEP
				unsigned long long int total_duration_ms;
				struct timeval total_start_ms, total_finish_ms;
				gettimeofday (&total_start_ms, NULL); 

				string record_file;
				record_file = logfile_prefix;
				record_file += "skolem_function_generation_details.txt";
				FILE* record_fp = fopen(record_file.c_str(), "a+");
				assert(record_fp != NULL);
				fprintf(record_fp, "\n\n\n\n");
				fprintf(record_fp, "benchmark type = %s\n", benchmark_type.c_str()); 
				fprintf(record_fp, "benchmark name = %s\n", benchmark_name.c_str()); 
				fprintf(record_fp, "problem = %s\n", problem_kind.c_str()); 
				fprintf(record_fp, "machine = %s\n", machine.c_str());
				fclose(record_fp);
			#endif
			
			if(time_out_enabled)
			{
				time_t elim_start_time;
				time(&elim_start_time);
				time_out_start = elim_start_time;
			}

			if(match_outputs_of_monolithic_and_factorized) // for proving correctness
			{
				cout << "match_outputs_of_monolithic_and_factorized not supported with AIG Manager" << endl;
				assert(false);				
			}
			else if(problem_kind == "benchmark_generation" && (benchmark_type == "hwmcc-2010" || benchmark_type == "hwmcc-2012"))
			{
				// to generate benchmarks of the component generation problem
				if(generate_satisfiable_benchmarks)
				{
					AIGBasedSkolemObj->satisfiableBenchmarkGeneration(Factors, Output_String_to_RHS_of_Factors, VariablesToEliminate);
				}
				else
				{
					AIGBasedSkolemObj->benchmarkGeneration(Factors, Output_String_to_RHS_of_Factors, VariablesToEliminate);
				}
			}
			else if(problem_kind == "graph_decomposition" && (benchmark_type == "hwmcc-2010" || benchmark_type == "hwmcc-2012"))
			{
				// graph decomposition on HMWMCC benchmarks

				// Skolem function generation is done inside graph decomposition
				// It can be either monolithic or factorized depending on 'disable_factorization'
				
				AIGBasedSkolemObj->graphDecomposition(Factors, RHS_of_Factors, VariablesToEliminate, Output_Object_to_RHS_of_Factors, Output_Object_to_RHS_of_PrimaryOutputs, abcObj, abcFrame);

			}
			else if(benchmark_type == "game")
			{
				assert(problem_kind == "variable_elimination");

				original_logfile_prefix = logfile_prefix;
				original_benchmark_name = benchmark_name;

				AIGBasedSkolemObj->generateSkolemFunctionsForGameBenchmarks(Factors, VariablesToEliminateForGameBenchmarks, TypeOfInnerQuantifier);
					
			}
			else if(benchmark_type == "external_skolem")
			{
				assert(problem_kind == "print_stats");

				#ifdef RECORD_KEEP
				string plot_file;
				plot_file = logfile_prefix; 
				plot_file += "skolem_function_generation_details_to_plot.txt";
				FILE* plot_fp = fopen(plot_file.c_str(), "a+");
				assert(plot_fp != NULL);
				fprintf(plot_fp, "\n%s\t%s\t%s\t%d\t%d\t%d\t%f", benchmark_type.c_str(), benchmark_name.c_str(), machine.c_str(), external_skolem_total_size,  external_skolem_number_of_vars, external_skolem_max_size, external_skolem_avg_size);
				fclose(plot_fp);
				#endif
			}
			else if(use_bloqqer) // use bloqqer
			{
				AIGBasedSkolemObj->skolemFunctionGeneratorUsingBloqqer(Factors, VariablesToEliminate);			
				
			}
			else if(disable_factorization) // use monolithic (Jiang's) approach
			{
				AIGBasedSkolemObj->monolithicSkolemFunctionGeneratorWithScopeReduction(Factors, VariablesToEliminate);			
				
			}
			else // use factorized approach
			{
				AIGBasedSkolemObj->factorizedSkolemFunctionGenerator(Factors, VariablesToEliminate);
			}

			if(time_out_enabled && timed_out)
			{
				cout << "\nTime-out from skolem-function generator\n";
			}

			if(debug_after_skf_generation) // place to test new helper.cpp functions
			{

				set<Aig_Obj_t*> Functions;
				for(int var_to_elim_index = 1; var_to_elim_index <= AIGBasedSkolemObj->number_of_vars_to_elim; var_to_elim_index++)
				{
					Functions.insert(AIGBasedSkolemObj->SkolemFunctions[var_to_elim_index]);
				}

				Aig_Obj_t* debug_dag = createAnd(Functions, aig_manager);
				assert(debug_dag != NULL);

				
				unsigned long long int solver_ms;
				struct timeval solver_start_ms, solver_finish_ms;
				
				map<string, int> Model;
				bool result_of_exactnesscheck;

				bool use_external = true;
				bool use_internal = true;

				if(use_external)
				{
					vector< vector<int> > CNF;
					vector< vector<int> > Temp_CNF;
					int top_label = getCNF(aig_manager, debug_dag, CNF);
					vector<int> clause_1;
					clause_1.push_back(top_label);
					CNF.push_back(clause_1);
	
					int number_of_variables = LabelCount-1;
					int number_of_clauses = CNF.size();

					cout << "\nsize of dag = " << computeSize(debug_dag, aig_manager) << endl;

					printf( "CNF: Variables = %6d. Clauses = %7d. ", number_of_variables, number_of_clauses );

					string cnf_filename = "debug.cnf";
					writeCNFToFile(CNF, Temp_CNF, number_of_variables, number_of_clauses, cnf_filename);

					cout << "\nexternal-solver called\n";
					gettimeofday (&solver_start_ms, NULL); 	
					result_of_exactnesscheck = giveCNFFiletoSATSolverAndQueryForSatisfiability(cnf_filename, Model);
					gettimeofday (&solver_finish_ms, NULL);
					solver_ms = solver_finish_ms.tv_sec * 1000 + solver_finish_ms.tv_usec / 1000;
					solver_ms -= solver_start_ms.tv_sec * 1000 + solver_start_ms.tv_usec / 1000;
					cout << "\nexternal-solver finished in " << solver_ms << " milliseconds\n";
					if(result_of_exactnesscheck)
						cout << "\nFormula is sat; get the CEX\n";
					else
						cout << "\nFormula is unsat\n";
				}

				if(use_internal)
				{

					cout << "\n\nPress any key to continue...\n";	
					char c = getchar();
					cout << "\nsize of dag = " << computeSize(debug_dag, aig_manager) << endl;
					cout << "\n\ninternal-solver called\n";				
					Model.clear();
					//result_of_exactnesscheck = isSat(aig_manager, debug_dag, Model);
				}
				
				
				cout << "\nTesting done !!";
				assert(false);
			}//if(debug_after_skf_generation) ends here

			// printing the statitics
			#ifdef RECORD_KEEP
				gettimeofday (&total_finish_ms, NULL);
		   		total_duration_ms = total_finish_ms.tv_sec * 1000 + total_finish_ms.tv_usec / 1000;
		   		total_duration_ms -= total_start_ms.tv_sec * 1000 + total_start_ms.tv_usec / 1000;

				if(problem_kind == "variable_elimination") // for the graph_decomposition case,
				// there are multiple calls to variable_elimination and total_time_in_compute_size is reset
				// to zero after each call
				{
					total_duration_ms = total_duration_ms - total_time_in_compute_size;
				}
				else if(problem_kind == "graph_decomposition")// for graph_decomposition; substract the cumulative time spent in size computation
				{
					total_duration_ms = total_duration_ms - cumulative_time_in_compute_size;
				}
				else
				{
					// do nothing
				}

				string order_string_to_print;
				if(order_of_elimination_of_variables == 0)
				{
					order_string_to_print = "alphabetical";	
				}
				else if(order_of_elimination_of_variables == 1)
				{
					order_string_to_print = "least-occurring-first";	
				}
				else if(order_of_elimination_of_variables == 2)
				{
					order_string_to_print = "factor-graph-based";	
				}
				else if(order_of_elimination_of_variables == 3)
				{
					order_string_to_print = "externally-supplied";	
				}

				string algorithm_string;
				if(enable_cegar)
				{
					algorithm_string = "cegar";

					if(use_mu_based_scheme_with_optimizations_in_cegar && unify_code_for_mu_based_scheme_in_cegar)
					{

						if(use_assumptions_in_unified_cegar)
						{
							algorithm_string += "_optimized";
						}
						else
						{
							algorithm_string += "_unoptimized";
						}
				
						if(use_bads_in_unified_cegar)
						{
							algorithm_string += "_withbads";
						}
						else
						{
							algorithm_string += "_withnegf";
						}


						if(accumulate_formulae_in_cbzero_in_cegar)
						{
							algorithm_string += "_withaccumulate";
						}
						else
						{
							algorithm_string += "_noaccumulate";
						}
					}
				}
				else
				{
					algorithm_string = "monolithic";	
					if(compute_quantifier_eliminated_result_using_skolem_functions)
					{
						algorithm_string += "_compositionqe";
					}
					else
					{
						algorithm_string += "_bddlikeqe";
					}

					if(use_interpolant_as_skolem_function)
					{
						algorithm_string += "_interpolantskf";
					}
					else
					{
						algorithm_string += "_cofactorskf";
					}

					if(skolem_function_type_in_jiang == "cofactorone")
					{
						algorithm_string += "_cofactorone";
					}
					else
					{
						algorithm_string += "_bothcofactors";
					}
				}
				
				record_file = logfile_prefix;
				record_file += "skolem_function_generation_details.txt";
				record_fp = fopen(record_file.c_str(), "a+");
				assert(record_fp != NULL);		
				
				
				if(problem_kind == "graph_decomposition")
				{
					fprintf(record_fp, "\n\n\ntotal-time-in-component-generation-without-size-computation-time = %llu milliseconds\nsize-computation-time = %llu\nnumber of components generated = %d\n", total_duration_ms, cumulative_time_in_compute_size, number_of_components_generated);
				}
				else if(problem_kind == "variable_elimination")
				{
					if(enable_cegar)
					{
						if(use_mu_based_scheme_in_cegar || use_mu_based_scheme_with_optimizations_in_cegar)
						{
							fprintf(record_fp, "\n\n\ntotal-time-in-evaluation-of-mu = %llu milliseconds\ntotal-time-in-interpolant-computation-in-cegar = %llu milliseconds\ntotal-time-in-dont-care-optimization-in-cegar = %llu milliseconds\ntotal-time-in-generalization-in-refinement-from-bottom-in-cegar = %llu milliseconds\ntotal-time-in-initial-abstraction-generation-without-size-computation-time = %llu milliseconds\ntotal-time-in-cegar-loops-without-size-computation-time = %llu milliseconds\ntotal-time-in-reverse-substitution-without-size-computation-time = %llu milliseconds\nsolver-used = %s\nnumber-of-cegar-iterations = %d\n\ntotal-time-without-size-computation-time = %llu milliseconds\n", total_time_in_mu_evaluation_in_cegar, total_time_in_interpolant_computation_in_cegar, total_time_in_dontcare_optimization_in_cegar, total_time_in_generalization_in_mu_based_scheme_with_optimizations_in_cegar, total_time_in_initial_abstraction_generation_in_cegar, total_time_in_cegar_loops_in_cegar, total_time_in_reverse_substitution_in_cegar, solver.c_str(), cegar_iteration_number, total_duration_ms);
						}
						else
						{
							fprintf(record_fp, "\n\n\ntotal-time-in-initial-abstraction-generation-without-size-computation-time = %llu milliseconds\ntotal-time-in-cegar-loops-without-size-computation-time = %llu milliseconds\nsolver-used = %s\nnumber-of-cegar-iterations = %d\ntotal-time-in-connection-substitution-without-size-computation-time = %llu milliseconds\ntotal-time-in-reverse-substitution-without-size-computation-time = %llu milliseconds\ntotal-time-without-size-computation-time = %llu milliseconds\nmaximum-length-of-connection = %d\nnumber-of-connections = %d\n", total_time_in_initial_abstraction_generation_in_cegar, total_time_in_cegar_loops_in_cegar, solver.c_str(), cegar_iteration_number, total_time_in_connection_substitution_in_cegar, total_time_in_reverse_substitution_in_cegar, total_duration_ms, maximum_length_of_connection_in_connection_based_scheme, number_of_connections_in_connection_based_scheme);

							fprintf(record_fp, "\n\nsizes-of-exactness-formulae-after-simplification = ");
							for(list<int>::iterator sfs_it = sizes_of_exactness_formulae_in_cegar.begin(); sfs_it != sizes_of_exactness_formulae_in_cegar.end(); sfs_it++)
							{
								fprintf(record_fp, "%d, ", *sfs_it);
							}

							unsigned long long int total_time_in_cnf_generation_in_cegar = 0;
							unsigned long long int total_time_in_aig_simplification_in_cegar = 0;
							unsigned long long int total_time_in_sat_solving_in_cegar_computed = 0;
					
							fprintf(record_fp, "\ntimes-in-simplification = ");
							for(list<unsigned long long int>::iterator sfs_it = times_in_aig_simplification_in_cegar.begin(); sfs_it != times_in_aig_simplification_in_cegar.end(); sfs_it++)
							{
								fprintf(record_fp, "%llu, ", *sfs_it);
								total_time_in_aig_simplification_in_cegar = total_time_in_aig_simplification_in_cegar + *sfs_it;
							}

							fprintf(record_fp, "\ntimes-in-cnf-generation = ");
							for(list<unsigned long long int>::iterator sfs_it = times_in_cnf_generation_in_cegar.begin(); sfs_it != times_in_cnf_generation_in_cegar.end(); sfs_it++)
							{
								fprintf(record_fp, "%llu, ", *sfs_it);
								total_time_in_cnf_generation_in_cegar = total_time_in_cnf_generation_in_cegar + *sfs_it;
							}

							fprintf(record_fp, "\ntimes-in-sat-solving = ");
							for(list<unsigned long long int>::iterator sfs_it = times_in_sat_solving_in_cegar.begin(); sfs_it != times_in_sat_solving_in_cegar.end(); sfs_it++)
							{
								fprintf(record_fp, "%llu, ", *sfs_it);
								total_time_in_sat_solving_in_cegar_computed = total_time_in_sat_solving_in_cegar_computed + *sfs_it;
							}

							fprintf(record_fp, "\ntotal_time_in_cnf_generation_in_cegar = %llu milliseconds\ntotal_time_in_aig_simplification_in_cegar = %llu milliseconds\ntotal_time_in_sat_solving_in_cegar = %llu milliseconds", total_time_in_cnf_generation_in_cegar, total_time_in_aig_simplification_in_cegar, total_time_in_sat_solving_in_cegar_computed);

							fprintf(record_fp, "\n\ntotal_time_in_exactness_checking_in_cegar = %llu milliseconds\ntotal_time_in_x_new_recompution_in_cegar = %llu milliseconds\ntotal_time_in_reevaluation_in_cegar = %llu milliseconds\nnumber_of_exactness_checking_in_cegar = %d\nnumber_of_x_new_recompution_in_cegar = %d\nnumber_of_reevaluation_in_cegar = %d ", total_time_in_exactness_checking_in_cegar, total_time_in_x_new_recompution_in_cegar, total_time_in_reevaluation_in_cegar, number_of_exactness_checking_in_cegar, number_of_x_new_recompution_in_cegar, number_of_reevaluation_in_cegar);

							fprintf(record_fp, "\n\nordering-used = %s\nbad_to_be_pulled_in_each_iteration = %s\ntotal time in ordering = %llu milliseconds\ntotal time in compute-size = %llu\ntotal time in compute-support = %llu\ntotal time in initialization of skolem function generator-without-size-computation-time = %llu", order_string_to_print.c_str(), bad_to_be_pulled_in_each_iteration.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_compute_support, total_time_in_generator_initialization);

							fprintf(record_fp, "\n\nsize_computation_time_in_initialization = %llu milliseconds\nsize_computation_time_in_initial_abstraction_generation_in_cegar = %llu milliseconds\nsize_computation_time_in_reverse_substitution_in_cegar = %llu milliseconds\nsize_computation_time_in_cegar_loops_in_cegar = %llu milliseconds\nsize_computation_time_in_connection_substitution_in_cegar = %llu milliseconds\ntotal_time_in_compute_size = %llu milliseconds", size_computation_time_in_initialization, size_computation_time_in_initial_abstraction_generation_in_cegar, size_computation_time_in_reverse_substitution_in_cegar, size_computation_time_in_cegar_loops_in_cegar, size_computation_time_in_connection_substitution_in_cegar, total_time_in_compute_size);
						}
					
					}
					else
					{
						fprintf(record_fp, "\ntotal-time-in-initial-skolem-function-generation-without-size-computation-time = %llu milliseconds\ntotal-time-in-reverse-substitution-without-size-computation-time = %llu milliseconds\ntotal-time-without-size-computation-time = %llu milliseconds\ntotal-time-in-interpolant-computation = %llu", total_time_in_initial_abstraction_generation_in_cegar, total_time_in_reverse_substitution_in_cegar, total_duration_ms, total_time_in_interpolant_computation);

						fprintf(record_fp, "\n\nalgorithm-used = %s\nordering-used = %s\ntotal time in ordering = %llu milliseconds\ntotal time in compute-size = %llu\ntotal time in compute-support = %llu\ntotal time in initialization of skolem function generator-without-size-computation-time = %llu\ntotal time in sat solving = %llu\nsolver used = %s\nnumber of cegar iterations = %d", algorithm_string.c_str(), order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_compute_support, total_time_in_generator_initialization, total_time_in_smt_solver, solver.c_str(), cegar_iteration_number);

						fprintf(record_fp, "\n\nCompose Details:\nHit_1 = %llu\nMiss_1 = %llu\nHit_2 = %llu\nMiss_2 = %llu\nLeaves = %llu\nNon-leaves = %llu\nNo-create-expr = %llu\nCreate-expr = %llu\nCreate-expr/Miss_2 = %f", first_level_cache_hits, first_level_cache_misses, second_level_cache_hits, second_level_cache_misses, leaf_cases, node_cases, no_recreation_cases, recreation_cases, (float)recreation_cases/(float)second_level_cache_misses);

						fprintf(record_fp, "\n\nsize_computation_time_in_initialization = %llu milliseconds\nsize_computation_time_in_initial_abstraction_generation_in_cegar = %llu milliseconds\nsize_computation_time_in_reverse_substitution_in_cegar = %llu milliseconds\nsize_computation_time_in_cegar_loops_in_cegar = %llu milliseconds\nsize_computation_time_in_connection_substitution_in_cegar = %llu milliseconds\ntotal_time_in_compute_size = %llu milliseconds", size_computation_time_in_initialization, size_computation_time_in_initial_abstraction_generation_in_cegar, size_computation_time_in_reverse_substitution_in_cegar, size_computation_time_in_cegar_loops_in_cegar, size_computation_time_in_connection_substitution_in_cegar, total_time_in_compute_size);
					}

					if(enable_cegar && perform_reverse_substitution)
					{
						fprintf(record_fp, "\nnumber-of-composes-in-reverse-substitution = %d", AIGBasedSkolemObj->number_of_compose_operations_for_variable);
						fprintf(record_fp, "\nfinal-skolem-function-sizes = ");
						for(list<int>::iterator sfs_it = skolem_function_sizes_after_reverse_substitution.begin(); sfs_it != skolem_function_sizes_after_reverse_substitution.end(); sfs_it++)
						{
							fprintf(record_fp, "%d, ", *sfs_it);
						}
					}
					else if(perform_reverse_substitution)
					{
						fprintf(record_fp, "\ncompose-in-reverse-substitution = %d", AIGBasedSkolemObj->number_of_compose_operations_for_variable);
						fprintf(record_fp, "\ntime-in-reverse-substitution = %llu", AIGBasedSkolemObj->ComposeTime);
						fprintf(record_fp, "\nfinal-skolem-function-sizes = ");
						for(list<int>::iterator sfs_it = skolem_function_sizes_after_reverse_substitution.begin(); sfs_it != skolem_function_sizes_after_reverse_substitution.end(); sfs_it++)
						{
							fprintf(record_fp, "%llu, ", *sfs_it);
						}
					}
					else
					{
						fprintf(record_fp, "\ncompose-in-reverse-substitution = -");
						fprintf(record_fp, "\ntime-in-reverse-substitution = -");
						fprintf(record_fp, "\nfinal-skolem-function-sizes = -");
					}
				}//else if(problem_kind == "variable_elimination") ends here
				else
				{
					// do nothing
				}

				fclose(record_fp);

				if(!use_bloqqer && benchmark_type != "game" && benchmark_type != "external_skolem")
				{
				
					string plot_file;
					plot_file = logfile_prefix; 
					plot_file += "skolem_function_generation_details_to_plot.txt";
					FILE* plot_fp = fopen(plot_file.c_str(), "a+");
					assert(plot_fp != NULL);

					if(disable_factorization)
					{
						if(time_out_enabled && timed_out)
						{
							fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated), (float)sum_of_skolem_function_sizes/(float)(number_of_variables_eliminated));
						}
						else
						{
							fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(AIGBasedSkolemObj->number_of_vars_to_elim), (float)sum_of_skolem_function_sizes/(float)(AIGBasedSkolemObj->number_of_vars_to_elim));
						}
						//fprintf(plot_fp, "\t%llu\t%llu\t-\t-\t-\t-\t-\t", total_number_of_compose_operations,  total_time_in_compose_operations);
					}
					else
					{
						if(time_out_enabled && timed_out)
						{
							if(enable_cegar)
							{
								fprintf(plot_fp, "\t-\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated));
							}
							else
							{
								fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated), (float)sum_of_skolem_function_sizes/(float)(number_of_variables_eliminated));
							}
						}
						else
						{
							fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(AIGBasedSkolemObj->number_of_vars_to_elim), (float)sum_of_skolem_function_sizes/(float)(AIGBasedSkolemObj->number_of_vars_to_elim));						
						}
					
						//fprintf(plot_fp, "\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t", total_number_of_compose_operations,  total_time_in_compose_operations, total_time_in_alpha_combined, total_time_in_delta_part, total_time_in_correction_part, total_time_in_delta_combined, total_time_in_next_factor);
					
					}

					if(time_out_enabled && timed_out)
					{
						fprintf(plot_fp, "\t%llu\t", time_out*1000);
					}
					else
					{
						fprintf(plot_fp, "\t%llu\t", total_duration_ms);
					}

				
					if(time_out_enabled && timed_out)
					{
						//fprintf(plot_fp, "-\t-\t%s\t%llu\t%llu\t%llu\t%f\t", order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(number_of_variables_eliminated));
						fprintf(plot_fp, "%d\t-\t-\t%s\t%llu\t", cegar_iteration_number, order_string_to_print.c_str(), total_time_in_ordering);
					}
					else if(!perform_reverse_substitution)
					{
						//fprintf(plot_fp, "-\t-\t%s\t%llu\t%llu\t%llu\t%f\t", order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(AIGBasedSkolemObj->number_of_vars_to_elim));
						fprintf(plot_fp, "%d\t-\t-\t%s\t%llu\t", cegar_iteration_number, order_string_to_print.c_str(), total_time_in_ordering);
					}
					else
					{
						//fprintf(plot_fp, "%llu\t%f\t%s\t%llu\t%llu\t%llu\t%f\t", AIGBasedSkolemObj->ComposeTime, (float)sum_of_skolem_function_sizes_after_reverse_substitution/(float)(AIGBasedSkolemObj->number_of_vars_to_elim), order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(AIGBasedSkolemObj->number_of_vars_to_elim));
						fprintf(plot_fp, "%d\t%llu\t%f\t%s\t%llu\t", cegar_iteration_number, total_time_in_reverse_substitution_in_cegar, (float)sum_of_skolem_function_sizes_after_reverse_substitution/(float)(AIGBasedSkolemObj->number_of_vars_to_elim), order_string_to_print.c_str(), total_time_in_ordering);
					}

				
					if(enable_cegar)
					{
						fprintf(plot_fp, "%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\n", total_time_in_mu_evaluation_in_cegar, total_time_in_interpolant_computation_in_cegar, total_time_in_dontcare_optimization_in_cegar, total_time_in_generalization_in_mu_based_scheme_with_optimizations_in_cegar, total_time_in_initial_abstraction_generation_in_cegar, total_time_in_cegar_loops_in_cegar, total_time_in_sat_solving_in_cegar, total_time_in_true_sat_solving_in_cegar, total_time_in_false_sat_solving_in_cegar);
					}
					else
					{
						fprintf(plot_fp, "%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\n", total_time_in_mu_evaluation_in_cegar, total_time_in_interpolant_computation, total_time_in_dontcare_optimization_in_cegar, total_time_in_generalization_in_mu_based_scheme_with_optimizations_in_cegar, total_time_in_initial_abstraction_generation_in_cegar, total_time_in_cegar_loops_in_cegar, total_time_in_sat_solving_in_cegar, total_time_in_true_sat_solving_in_cegar, total_time_in_false_sat_solving_in_cegar);
					}

				
					fclose(plot_fp);

				}
			#endif

			#ifdef DEBUG_SKOLEM
				string map_file_name = "Ci_id_to_Ci_name_map.txt";
				FILE* map_fp = fopen(map_file_name.c_str(), "w+");
				assert(map_fp != NULL);

				for(map<int, string>::iterator map_it = Ci_id_to_Ci_name_map.begin(); map_it != Ci_id_to_Ci_name_map.end(); map_it++)
				{
					fprintf(map_fp, "\n%d\t%s\n", map_it->first, (map_it->second).c_str());	
				}
				fclose(map_fp);

				map_file_name = "Ci_name_to_Ci_number_map.txt";
				map_fp = fopen(map_file_name.c_str(), "w+");
				assert(map_fp != NULL);

				for(map<string, int>::iterator map_it = Ci_name_to_Ci_number_map.begin(); map_it != Ci_name_to_Ci_number_map.end(); map_it++)
				{
					fprintf(map_fp, "\n%s\t%d\n", (map_it->first).c_str(), map_it->second);	
				}
				fclose(map_fp);

				map_file_name = "Ci_name_to_Ci_label_map.txt";
				map_fp = fopen(map_file_name.c_str(), "w+");
				assert(map_fp != NULL);

				for(map<string, int>::iterator map_it = Ci_name_to_Ci_label_mapForGetCNF.begin(); map_it != Ci_name_to_Ci_label_mapForGetCNF.end(); map_it++)
				{
					fprintf(map_fp, "\n%s\t%d\n", (map_it->first).c_str(), map_it->second);	
				}
				fclose(map_fp);
				//char dump_file[100];
				//strcpy(dump_file, "dump.v");
				//Aig_ManDumpVerilog( aig_manager, dump_file );

				Aig_ManShow(aig_manager, 0, NULL); 
			#endif
			
		}
		else if(!debug)
		{
			set<t_Expression*> Factors;
			list<string> VariablesToEliminate;

			cout << "Reading the original factors and variables to be eliminated..." << endl;	

			if(benchmark_type == "crafted")
			{
				obtainFactors(abcObj, abcFrame, Factors, em);
				obtainVariablesToEliminate(VariablesToEliminate); 
			}
			else if(benchmark_type == "hwmcc-2010" || benchmark_type == "hwmcc-2012")
			{
				obtainFactorsAndVariablesToEliminatFromHWMCCFile(abcObj, abcFrame, Factors, VariablesToEliminate, em);		
			}
			else if(benchmark_type == "iscas-89")
			{
				obtainFactorsAndVariablesToEliminatFromISCASFile(abcObj, abcFrame, Factors, VariablesToEliminate, em);	
				cout << "\nExiting after reading\n"; exit(1); // for debugging
			}
			else
			{
				cout << "Value of BENCHMARK-TYPE is "<< benchmark_type << endl;
				assert(false && "Invalid Value");
			}

	
			bool write_back;
			#ifdef DEBUG_SKOLEM
			write_back = true;
			#else
			write_back = false;
			#endif
			if(write_back)
			{	
				string outfile_prefix = "original_factor_";
				string outfile_extension = ".v";
				int outfile_count = 1;
				for(set<t_Expression*>::iterator factor_it = Factors.begin(); factor_it != Factors.end(); factor_it++)
				{
					char outfile_count_char[100];
					sprintf(outfile_count_char, "%d", outfile_count);
					string outfile_count_string(outfile_count_char);

					string outfile = outfile_prefix;
					outfile += outfile_count_string;
					outfile += outfile_extension;

					cout << "*factor_it = " << *factor_it << endl;
			
					writeFormulaToFile(em, *factor_it, outfile);

					outfile_count++;	
				}

				FILE *vars_to_elim_outfile = fopen("original_VariablesToEliminate.txt", "w");
				assert(vars_to_elim_outfile != NULL);
				for(list<string>::iterator list_it = VariablesToEliminate.begin(); list_it != VariablesToEliminate.end(); list_it++)
				{
					fprintf(vars_to_elim_outfile, "%s\n", (*list_it).c_str());
				}
				fclose(vars_to_elim_outfile);
			}

	

			Skolem* SkolemObj = new Skolem(em);
			assert(SkolemObj != NULL);		

			#ifdef RECORD_KEEP
				unsigned long long int total_duration_ms;
				struct timeval total_start_ms, total_finish_ms;
				gettimeofday (&total_start_ms, NULL); 

				string record_file;
				record_file = logfile_prefix; 
				record_file += "skolem_function_generation_details.txt";
				FILE* record_fp = fopen(record_file.c_str(), "a+");
				assert(record_fp != NULL);
				fprintf(record_fp, "\n\n\n\n");
				fprintf(record_fp, "Y = %s\n", benchmark_type.c_str()); 
				fprintf(record_fp, "B = %s\n", benchmark_name.c_str()); 
				fprintf(record_fp, "M = %s\n", machine.c_str());
				fclose(record_fp);

				string size_file;
				size_file = logfile_prefix; 
				size_file += "skolem_function_generation_factor_size_details.txt";
				FILE* size_fp = fopen(size_file.c_str(), "a+");
				assert(size_fp != NULL);
				fprintf(size_fp, "\n\n\n\n");
				fprintf(size_fp, "Y = %s\n", benchmark_type.c_str()); 
				fprintf(size_fp, "B = %s\n", benchmark_name.c_str()); 
				fprintf(size_fp, "M = %s\n", machine.c_str());
				fclose(size_fp);
			#endif

			if(time_out_enabled)
			{
				time_t elim_start_time;
				time(&elim_start_time);
				time_out_start = elim_start_time;
			}
			if(match_outputs_of_monolithic_and_factorized) // for proving correctness
			{
				SkolemObj->factorizedSkolemFunctionGenerator(Factors, VariablesToEliminate);
				variable_order_file_name = benchmark_name_without_extension;
				variable_order_file_name += "_factorized_order.txt";
				SkolemObj->clearAllDataStructures();

				if(apply_scope_reduction)
				{
					SkolemObj->monolithicSkolemFunctionGeneratorWithScopeReduction(Factors, VariablesToEliminate);
				}
				else
				{
					SkolemObj->monolithicSkolemFunctionGenerator(Factors, VariablesToEliminate);
				}
				assert(result_of_qe_using_factorized != NULL);
				assert(result_of_qe_using_monolithic != NULL);

				t_Expression* factorized_implies_monolithic = createAnd(result_of_qe_using_factorized, createNot(result_of_qe_using_monolithic, em), em);
				assert(factorized_implies_monolithic != NULL);
				string factorized_implies_monolithic_outfile = benchmark_name_without_extension;
				factorized_implies_monolithic_outfile += "_factorized_implies_monolithic.smt2";
				set<t_Expression*> ConstraintsToPrint;
				ConstraintsToPrint.insert(factorized_implies_monolithic);
				em->printExpressionsToFileInSMT(ConstraintsToPrint, "", factorized_implies_monolithic_outfile);

				t_Expression* monolithic_implies_factorized = createAnd(result_of_qe_using_monolithic, createNot(result_of_qe_using_factorized, em), em);
				assert(monolithic_implies_factorized != NULL);
				string monolithic_implies_factorized_outfile = benchmark_name_without_extension;
				monolithic_implies_factorized_outfile += "_monolithic_implies_factorized.smt2";
				ConstraintsToPrint.clear();
				ConstraintsToPrint.insert(monolithic_implies_factorized);
				em->printExpressionsToFileInSMT(ConstraintsToPrint, "", monolithic_implies_factorized_outfile);
				
			}
			else if(disable_factorization) // use monolithic (Jiang's) approach
			{
					if(apply_scope_reduction)
					{
						SkolemObj->monolithicSkolemFunctionGeneratorWithScopeReduction(Factors, VariablesToEliminate);
					}
					else
					{
						SkolemObj->monolithicSkolemFunctionGenerator(Factors, VariablesToEliminate);
					}
			}
			else // use factorized approach
			{
					SkolemObj->factorizedSkolemFunctionGenerator(Factors, VariablesToEliminate);
			}

			if(time_out_enabled && timed_out)
			{
					cout << "\nTime-out from skolem-function generator\n";
			}

			#ifdef RECORD_KEEP
					gettimeofday (&total_finish_ms, NULL);
		   			total_duration_ms = total_finish_ms.tv_sec * 1000 + total_finish_ms.tv_usec / 1000;
		   			total_duration_ms -= total_start_ms.tv_sec * 1000 + total_start_ms.tv_usec / 1000;


					string order_string_to_print;
					if(order_of_elimination_of_variables == 0)
					{
						order_string_to_print = "alphabetical";	
					}
					else if(order_of_elimination_of_variables == 1)
					{
						order_string_to_print = "least-occurring-first";	
					}
					else if(order_of_elimination_of_variables == 2)
					{
						order_string_to_print = "least-cost-first";	
					}
					else if(order_of_elimination_of_variables == 3)
					{
						order_string_to_print = "externally-supplied";	
					}


					string algorithm_string;
					if(disable_factorization || disable_factorization_inside_factorized_code)
					{
						algorithm_string = "monolithic";
					}
					else if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
					{
						algorithm_string = "factorized_with_qe";
					}
					else
					{
						algorithm_string = "factorized";
					}
		
					record_file = logfile_prefix; 
					record_file += "skolem_function_generation_details.txt";
					record_fp = fopen(record_file.c_str(), "a+");
					assert(record_fp != NULL);
					fprintf(record_fp, "\nT = %llu", total_duration_ms);

					if(perform_reverse_substitution)
					{
						fprintf(record_fp, "\ncompose-in-reverse-substitution = %d", SkolemObj->number_of_compose_operations_for_variable);
						fprintf(record_fp, "\ntime-in-reverse-substitution = %llu", SkolemObj->ComposeTime);
						fprintf(record_fp, "\nfinal-skolem-function-sizes = ");
						for(list<int>::iterator sfs_it = skolem_function_sizes_after_reverse_substitution.begin(); sfs_it != skolem_function_sizes_after_reverse_substitution.end(); sfs_it++)
						{
							fprintf(record_fp, "%llu, ", *sfs_it);
						}
					}
					else
					{
						fprintf(record_fp, "\ncompose-in-reverse-substitution = -");
						fprintf(record_fp, "\ntime-in-reverse-substitution = -");
						fprintf(record_fp, "\nfinal-skolem-function-sizes = -");
					}

					fprintf(record_fp, "\nalgorithm-used = %s\nordering-used = %s\ntotal time in ordering = %llu milliseconds\ntotal time in compute-size = %llu\ntotal time in compute-support = %llu\ntotal time in initialization of skolem function generator = %llu\n", algorithm_string.c_str(), order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_compute_support, total_time_in_generator_initialization);

					fprintf(record_fp, "\n\nCompose Details:\nHit_1 = %llu\nMiss_1 = %llu\nHit_2 = %llu\nMiss_2 = %llu\nLeaves = %llu\nNon-leaves = %llu\nNo-create-expr = %llu\nCreate-expr = %llu\nCreate-expr/Miss_2 = %f", first_level_cache_hits, first_level_cache_misses, second_level_cache_hits, second_level_cache_misses, leaf_cases, node_cases, no_recreation_cases, recreation_cases, (float)recreation_cases/(float)second_level_cache_misses);
					fclose(record_fp);
				
					size_file = logfile_prefix; 
					size_file += "skolem_function_generation_factor_size_details.txt";
					size_fp = fopen(size_file.c_str(), "a+");
					assert(size_fp != NULL);
					fprintf(size_fp, "\n\n");
					fprintf(size_fp, "A = %s\n", algorithm_string.c_str()); 
					fprintf(size_fp, "O = %s\n", order_string_to_print.c_str()); 
					fclose(size_fp);

					string plot_file;
					plot_file = logfile_prefix; 
					plot_file += "skolem_function_generation_details_to_plot.txt";
					FILE* plot_fp = fopen(plot_file.c_str(), "a+");
					assert(plot_fp != NULL);

					if(disable_factorization)
					{
						if(time_out_enabled && timed_out)
						{
							fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated), (float)sum_of_skolem_function_sizes/(float)(number_of_variables_eliminated));
						}
						else
						{
							fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(SkolemObj->number_of_vars_to_elim), (float)sum_of_skolem_function_sizes/(float)(SkolemObj->number_of_vars_to_elim));
						}
						fprintf(plot_fp, "\t%llu\t%llu\t-\t-\t-\t-\t-\t", total_number_of_compose_operations,  total_time_in_compose_operations);
					}
					else
					{
						if(time_out_enabled && timed_out)
						{
							if(order_of_elimination_of_variables == 2)
							{
								fprintf(plot_fp, "\t%f\t%f\t%f", (float)total_of_skyline_sizes_in_least_cost_ordering/(float)(number_of_variables_eliminated), (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated), (float)sum_of_skolem_function_sizes/(float)(number_of_variables_eliminated));
							}
							else
							{
								fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(number_of_variables_eliminated), (float)sum_of_skolem_function_sizes/(float)(number_of_variables_eliminated));
							}
						}
						else
						{
							if(order_of_elimination_of_variables == 2)
							{
								fprintf(plot_fp, "\t%f\t%f\t%f", (float)total_of_skyline_sizes_in_least_cost_ordering/(float)(SkolemObj->number_of_vars_to_elim), (float)sum_of_number_of_factors_containing_variable/(float)(SkolemObj->number_of_vars_to_elim), (float)sum_of_skolem_function_sizes/(float)(SkolemObj->number_of_vars_to_elim));
							}
							else
							{
								fprintf(plot_fp, "\t%f\t%f", (float)sum_of_number_of_factors_containing_variable/(float)(SkolemObj->number_of_vars_to_elim), (float)sum_of_skolem_function_sizes/(float)(SkolemObj->number_of_vars_to_elim));
							}
						}
					
						fprintf(plot_fp, "\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t", total_number_of_compose_operations,  total_time_in_compose_operations, total_time_in_alpha_combined, total_time_in_delta_part, total_time_in_correction_part, total_time_in_delta_combined, total_time_in_next_factor);
					
					}

					if(time_out_enabled && timed_out)
					{
						fprintf(plot_fp, "%llu\t", time_out*1000);
					}
					else
					{
						fprintf(plot_fp, "%llu\t", total_duration_ms);
					}

				

					if(time_out_enabled && timed_out)
					{
						fprintf(plot_fp, "-\t-\t%s\t%llu\t%llu\t%llu\t%f\t", order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(number_of_variables_eliminated));
					}
					else if(!perform_reverse_substitution)
					{
						fprintf(plot_fp, "-\t-\t%s\t%llu\t%llu\t%llu\t%f\t", order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(SkolemObj->number_of_vars_to_elim));
					}
					else
					{
						fprintf(plot_fp, "%llu\t%f\t%s\t%llu\t%llu\t%llu\t%f\t", SkolemObj->ComposeTime, (float)sum_of_skolem_function_sizes_after_reverse_substitution/(float)(SkolemObj->number_of_vars_to_elim), order_string_to_print.c_str(), total_time_in_ordering, total_time_in_compute_size, total_time_in_ordering+total_time_in_compute_size, (float)sum_of_numbers_of_affecting_factors/(float)(SkolemObj->number_of_vars_to_elim));
					}

					fprintf(plot_fp, "%d\t%d\t%d\t%d\n", max_factor_size, min_factor_size, max_factor_varstoelim_size, min_factor_varstoelim_size);

					fclose(plot_fp);
			#endif
		}
		else // debug case
		{
			string x = "x";
			string y = "y";
			t_Expression* x_exp = createProposition(x, em);
			t_Expression* y_exp = createProposition(y, em);
			t_Expression* x_and_y = createAnd(x_exp, y_exp, em);
			t_Expression* t_exp = createTrue(em);
			
			string outfile = "input.txt";
			writeFormulaToFile(em, x_and_y, outfile);

			unsigned long long int second_level_cache_hits = 0;
			unsigned long long int second_level_cache_misses = 0;
			
			t_HashTable<unsigned long, t_Expression*> cache;
			t_Expression* ReplacedFormula;
			//ReplacedFormula = em->ReplaceLeafByExpression(x_and_y, x, y_exp, cache, true, second_level_cache_hits, second_level_cache_misses);
			outfile = "output1.txt";
			writeFormulaToFile(em, ReplacedFormula, outfile);

			cout << "\nsecond_level_cache_hits = " << second_level_cache_hits;
			cout << "\tsecond_level_cache_misses = " << second_level_cache_misses << endl;

			cout << endl << endl;

			cache.clear();
			t_Expression* ReplacedFormula2;
			//ReplacedFormula2 = em->ReplaceLeafByExpression(ReplacedFormula, y, t_exp, cache, true, second_level_cache_hits, second_level_cache_misses);
			//ReplacedFormula2 = em->ReplaceLeafByExpression(x_and_y, x, y_exp, cache, true, second_level_cache_hits, second_level_cache_misses);
			outfile = "output2.txt";
			writeFormulaToFile(em, ReplacedFormula2, outfile);

			cout << "\nsecond_level_cache_hits = " << second_level_cache_hits;
			cout << "\tsecond_level_cache_misses = " << second_level_cache_misses << endl;

		}
	}// if(test_skolem_function_generator) ends here 
 //cout<< "\nEnd of TEST"<<endl;
 return 0;
}