/* 
 * File:   Skolem.cpp
 * Author: Ajith John
 * 
 * Created on 27 December, 2013
 */

#include "Skolem.hpp"
#include "Graph.hpp"


/**
 * Initializes pub_em
 * @param em
 */
Skolem::Skolem(t_ExpressionManager* em)
{
	if (Skolem_instance != NULL) 
	{
    		cerr << "Error in Skolem::Skolem: Attempt to create multiple copies of Skolem" << endl;
    		cerr << "There should be only one copy of Skolem" << endl;
    		assert(0);
  	}

	pub_em = em;	
}



Skolem::~Skolem()
{
}


Skolem* Skolem::Skolem_instance = NULL;


Skolem* Skolem::getInstance(t_ExpressionManager* em)
{
	if(Skolem_instance == NULL)
	{
		try
		{
			Skolem_instance = new Skolem(em);
		}
		catch(bad_alloc&) 
		{
		      cerr << "Memory allocation failure in Skolem::getInstance" << endl;
      		      assert(0);
    		}
  	}

	return Skolem_instance;
}


void Skolem::initializeFactorizedSkolemFunctionGenerator(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	// Let's first 1) Remove variables which are not occuring in the factors
	// from the set of variables to be eliminated, and
	// 2) Insert the factors into FactorMatrix

	set<string> support;
	set<string> VariablesToEliminate_Set(VariablesToEliminate.begin(), VariablesToEliminate.end());
	set<string> Final_VariablesToEliminate_Set;

	number_of_factors = Factors.size();
	// insert factors into FactorMatrix[1...number_of_factors]
	int factor_index = 1; // varies from 1 to number_of_factors
	
	#ifdef DETAILED_RECORD_KEEP
	string support_file_name = benchmark_name_without_extension;
	support_file_name += "_support.txt";
	FILE* support_fp = fopen(support_file_name.c_str(), "w");
	assert(support_fp != NULL);
	printSet(VariablesToEliminate_Set, "Original_VariablesToEliminate_Set", support_fp);
	#endif

	map<string, int> VarsToElim_To_Factors_Map;

	for(set<t_Expression*>::iterator factor_it = Factors.begin(); factor_it != Factors.end(); factor_it++)
	{
		t_Expression* factor = *factor_it;
		assert(factor != NULL);		

		set<string> support_factor;
		computeSupport(factor, support_factor);
		int support_size = support_factor.size();
		original_factor_support_sizes.insert(make_pair(factor_index, support_size));

		copy(support_factor.begin(), support_factor.end(), inserter(support, support.end()));

		set<string> varstoelim_in_support_factor;
		set_intersection(support_factor.begin(), support_factor.end(), VariablesToEliminate_Set.begin(), VariablesToEliminate_Set.end(), inserter(varstoelim_in_support_factor, varstoelim_in_support_factor.begin()));
		int varstoelim_in_support_factor_size = varstoelim_in_support_factor.size();
		original_factor_varstoelim_sizes.insert(make_pair(factor_index, varstoelim_in_support_factor_size)); 
						
		int factor_size = computeSize(factor);
		original_factor_sizes.insert(make_pair(factor_index, factor_size));	

		copy(varstoelim_in_support_factor.begin(), varstoelim_in_support_factor.end(), inserter(Final_VariablesToEliminate_Set, Final_VariablesToEliminate_Set.end()));

		for(set<string>::iterator varstoelim_it = varstoelim_in_support_factor.begin(); varstoelim_it != varstoelim_in_support_factor.end(); varstoelim_it++)
		{
			string variable_to_eliminate = *varstoelim_it;
			map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.find(variable_to_eliminate);
			if(VarsToElim_To_Factors_Map_it == VarsToElim_To_Factors_Map.end()) 
			// variable_to_eliminate occuring for the first time
			{
				VarsToElim_To_Factors_Map.insert(make_pair(variable_to_eliminate, 1));
			}
			else
			{
				(VarsToElim_To_Factors_Map_it->second)++;
			}
		} 
		
		#ifdef DETAILED_RECORD_KEEP
		fprintf(support_fp,"\nfactor_%d\n",factor_index);
		cout << endl;
		printSet(support_factor, "support_factor", support_fp);
		cout << endl;
		printSet(varstoelim_in_support_factor, "varstoelim_in_support_factor", support_fp);
		cout << endl;		
		#endif	
		
		// Following line commented on 21-jan-2014
		//if(use_uninterpreted_functions && varstoelim_in_support_factor_size >= threshold_varstoelim_for_using_uninterpreted_functions)
		if(use_uninterpreted_functions || use_uninterpreted_functions_only_to_abstract_factors)
		{
			string name_of_function = "factor";
			t_Expression* abstracted_factor = createAbstraction(name_of_function, 1, factor_index, support_factor, pub_em);
			assert(abstracted_factor != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));

			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, abstracted_factor, false);

			#ifdef RECORD_KEEP
			int abstracted_factor_size = computeSize(abstracted_factor);
			abstracted_factor_sizes.insert(make_pair(factor_index, abstracted_factor_size));			
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nfactor_" << factor_index << " of size " << factor_size << " abstracted to factor of size " << abstracted_factor_size << endl;
			#endif
		}
		else
		{
			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index,factor,false);

			#ifdef RECORD_KEEP
			abstracted_factor_sizes.insert(make_pair(factor_index, factor_size));
			#endif
		}

		if(order_of_elimination_of_variables == 2)
		{	

			#ifdef DETAILED_RECORD_KEEP
			// create the order file
			string order_file_name = benchmark_name_without_extension;
			order_file_name += "_factorized_order.txt";
			FILE* order_fp = fopen(order_file_name.c_str(), "w+");
			assert(order_fp != NULL);
			fclose(order_fp);
			#endif

	
			// initialize the factor graph
			factor_graph_factors_to_vars_map.insert(make_pair(factor_index, varstoelim_in_support_factor));

			for(set<string>::iterator varstoelim_it = varstoelim_in_support_factor.begin(); varstoelim_it != varstoelim_in_support_factor.end(); varstoelim_it++)
			{
				string variable_to_eliminate = *varstoelim_it;
				map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.find(variable_to_eliminate);
				if(factor_graph_vars_to_factors_map_it == factor_graph_vars_to_factors_map.end()) 
				// variable_to_eliminate occuring for the first time
				{
					set<int> factors_with_variable;
					factors_with_variable.insert(factor_index);
					factor_graph_vars_to_factors_map.insert(make_pair(variable_to_eliminate, factors_with_variable));
				}
				else
				{
					(factor_graph_vars_to_factors_map_it->second).insert(factor_index);
				}
			} 

			factor_to_costs_map.insert(make_pair(factor_index, factor_size));
		}
						
		factor_index++;
	}

	original_support_size = support.size();	
	
	#ifdef DETAILED_RECORD_KEEP
	printSet(support, "support", support_fp);
	printSet(Final_VariablesToEliminate_Set, "Final_VariablesToEliminate_Set", support_fp);
	fclose(support_fp);
	#endif

        if(order_of_elimination_of_variables == 1 || order_of_elimination_of_variables == 0 || order_of_elimination_of_variables == 3)
	{

		if(order_of_elimination_of_variables == 1)
		{
			map<int, set<string> > Factors_To_VarsToElim_Map;
			for(map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.begin(); VarsToElim_To_Factors_Map_it != VarsToElim_To_Factors_Map.end(); VarsToElim_To_Factors_Map_it++)
			{
				string variable_to_eliminate = VarsToElim_To_Factors_Map_it->first;
				int number_of_factors_with_variable_to_eliminate = VarsToElim_To_Factors_Map_it->second;
				cout << endl << variable_to_eliminate << "\t" << number_of_factors_with_variable_to_eliminate << endl;

				map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.find(number_of_factors_with_variable_to_eliminate);
				if(Factors_To_VarsToElim_Map_it == Factors_To_VarsToElim_Map.end())
				{
					set<string> variables_with_factor_count;
					variables_with_factor_count.insert(variable_to_eliminate);
					Factors_To_VarsToElim_Map.insert(make_pair(number_of_factors_with_variable_to_eliminate, variables_with_factor_count));
				}
				else
				{
					(Factors_To_VarsToElim_Map_it->second).insert(variable_to_eliminate);
				}
			}

			VariablesToEliminate.clear();
			for(map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.begin(); Factors_To_VarsToElim_Map_it != Factors_To_VarsToElim_Map.end(); Factors_To_VarsToElim_Map_it++)
			{
				cout << endl << "factor_count = " << Factors_To_VarsToElim_Map_it->first <<"\tvariables = ";
				set<string> variables_with_factor_count = Factors_To_VarsToElim_Map_it->second;
				for(set<string>::iterator variable_it = variables_with_factor_count.begin(); variable_it != variables_with_factor_count.end(); variable_it++)
				{
					cout << *variable_it << ", ";
					VariablesToEliminate.push_back(*variable_it);
				}
			}			
		}
		else if(order_of_elimination_of_variables == 3) // from external file
		{
			// we should read the order from the given file
			list<string> OrderOfVariableEliminationFromFile;
			obtainOrderOfVariableEliminationFromFile(OrderOfVariableEliminationFromFile);

			#ifdef DEBUG_SKOLEM 
			cout << endl << "OrderOfVariableEliminationFromFile" << endl;
			showList(OrderOfVariableEliminationFromFile);
			#endif

			VariablesToEliminate.clear();

			for(list<string>::iterator var_order_it = OrderOfVariableEliminationFromFile.begin(); var_order_it != OrderOfVariableEliminationFromFile.end(); var_order_it++)
			{
				string var_from_order_file = *var_order_it;
				if(Final_VariablesToEliminate_Set.find(var_from_order_file) != Final_VariablesToEliminate_Set.end()) // this is a var to elim
				{
					VariablesToEliminate.push_back(var_from_order_file);
				}
			}

			cout << endl << "VariablesToEliminate" << endl;
			showList(VariablesToEliminate);
		}
		else
		{
			VariablesToEliminate.clear();
			copy(Final_VariablesToEliminate_Set.begin(), Final_VariablesToEliminate_Set.end(), inserter(VariablesToEliminate, VariablesToEliminate.end()));
		}

		number_of_vars_to_elim = VariablesToEliminate.size();

		#ifdef DETAILED_RECORD_KEEP
		string order_file_name = benchmark_name_without_extension;
		order_file_name += "_factorized_non_greedy_order.txt";
		FILE* order_fp = fopen(order_file_name.c_str(), "w+");
		assert(order_fp != NULL);
		printList(VariablesToEliminate, order_fp);
		fclose(order_fp);
		#endif


		#ifdef DEBUG_SKOLEM
		cout << "number_of_factors = " << number_of_factors << endl;
		cout << "number_of_vars_to_elim = " << number_of_vars_to_elim << endl;
		#endif	

		// create the var_name_to_var_index_map and var_index_to_var_name_map
		int var_index = 1;
		for(list<string>::iterator list_it = VariablesToEliminate.begin(); list_it != VariablesToEliminate.end(); list_it++)
		{
			insertIntoVarNameToVarIndexMap(var_name_to_var_index_map, *list_it, var_index);
			insertIntoVarIndexToVarNameMap(var_index_to_var_name_map, var_index, *list_it);

			#ifdef DEBUG_SKOLEM
			cout << "(" << *list_it << ", " << var_index << ") inserted into maps "<< endl;
			#endif	

			var_index++;
		}


		if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{
			bad_set = createFalse(pub_em);				
		}
		else // else of if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{
	
			// Let's compute the skylines
			UnionOfSkylines.clear();
		
			bool use_dynamic_pgming_based_skyline_computation = false;
			if(use_dynamic_pgming_based_skyline_computation && optimization_lemmas_on)
			{
				obtainSkylineUsingLemmas();

				for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
				{
					map<int, set<int> >::iterator Skylines_it = Skylines.find(var_to_elim_index);
					assert(Skylines_it != Skylines.end());

					set<int> Skyline_for_var_to_elim_index;
					Skyline_for_var_to_elim_index = Skylines_it->second;

					#ifdef DEBUG_SKOLEM
					showSet(Skyline_for_var_to_elim_index, "Skyline_for_var_to_elim_index");
					#endif

					copy(Skyline_for_var_to_elim_index.begin(), Skyline_for_var_to_elim_index.end(), inserter(UnionOfSkylines, UnionOfSkylines.end()));
				}
			}
			else
			{
				for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
				{
					// Let's compute the skyline for each variable
					#ifdef DEBUG_SKOLEM
					cout << "\nComputing skyline for variable_" << var_to_elim_index << endl;
					#endif

					set<int> Skyline_for_var_to_elim_index;
					if(optimization_lemmas_on)
					{
						obtainSkylineOfVariableUsingLemmas(var_to_elim_index, Skyline_for_var_to_elim_index);
					}
					else
					{
						initializeSkylineVariablesTrivially(var_to_elim_index, Skyline_for_var_to_elim_index);
					}
					Skylines.insert(make_pair(var_to_elim_index, Skyline_for_var_to_elim_index));

					#ifdef DEBUG_SKOLEM
					showSet(Skyline_for_var_to_elim_index, "Skyline_for_var_to_elim_index");
					#endif

					copy(Skyline_for_var_to_elim_index.begin(), Skyline_for_var_to_elim_index.end(), inserter(UnionOfSkylines, UnionOfSkylines.end()));
				}
			}
			#ifdef DEBUG_SKOLEM
			showSet(UnionOfSkylines, "UnionOfSkylines");
			#endif
		}// else of if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation) ends here

	}// if(order_of_elimination_of_variables == 1 || order_of_elimination_of_variables == 0 || order_of_elimination_of_variables == 3) ends here
	else // if(order_of_elimination_of_variables == 2)
	{

		if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{
			bad_set = createFalse(pub_em);				
		}
		else // else of if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{

			number_of_vars_to_elim = Final_VariablesToEliminate_Set.size();

			#ifdef DEBUG_SKOLEM
			cout << "number_of_factors = " << number_of_factors << endl;
			cout << "number_of_vars_to_elim = " << number_of_vars_to_elim << endl;
			#endif	
		

			// initializing the datastructurs for least-cost-first ordering
			// note that factor graph is already created

			factor_graph_factors_to_topvars_map.clear(); // no top-vars decided so far, since ordering is undefined
			topvars.clear();

			ordered_vars_to_elim.clear(); // ordering is undefined
		
			int eqclass_number = 1;
			for(set<string>::iterator varstoelim_it = Final_VariablesToEliminate_Set.begin(); varstoelim_it != Final_VariablesToEliminate_Set.end(); varstoelim_it++)
			{
				string vartoelim = *varstoelim_it;

				unordered_vars_to_elim.insert(vartoelim);

				set<string> eqclass;
				eqclass.insert(vartoelim);

				factor_graph_vars_to_sccnos_map.insert(make_pair(vartoelim, eqclass_number));
				vars_to_eqclassnos_map.insert(make_pair(vartoelim, eqclass_number));
			
				factor_graph_sccnos_to_sccs_map.insert(make_pair(eqclass_number, eqclass));
				eqclassnos_to_eqclasses_map.insert(make_pair(eqclass_number, eqclass));

				eqclass_number++;
			}
		
			skolemfunctions_to_costs_map.clear();
			deltas_to_costs_map.clear();

			findStronglyConnectedComponentsInFactorGraph();
			// this computes factor_graph_vars_to_sccnos_map and factor_graph_sccnos_to_sccs_map

			#ifdef DEBUG_SKOLEM
			showDataStructuresForLeastCostOrdering();
			#endif
		}
		
	}

	if(print_factor_graph)
	{
		if(true)
		{
			printFactorGraphAsData(Final_VariablesToEliminate_Set);
		}
		else
		{
			printFactorGraph(Final_VariablesToEliminate_Set);
		}
	}

	#ifdef RECORD_KEEP
		string record_file = "skolem_function_generation_details.txt";
		FILE* record_fp = fopen(record_file.c_str(), "a+");
		assert(record_fp != NULL);

		fprintf(record_fp, "F = %d\n", number_of_factors); 
		fprintf(record_fp, "E = %d\n", number_of_vars_to_elim); 

		// print details of original factors
		fprintf(record_fp, "V = %d\n\n", original_support_size);

		fprintf(record_fp, "N_f = ");

		unsigned long long int total_of_factor_sizes = 0;
		unsigned long long int total_of_abstracted_factor_sizes = 0;
		unsigned long long int total_of_factor_support_sizes = 0;
		unsigned long long int total_of_factor_varstoelim_sizes = 0;
		unsigned long long int total_of_skyline_sizes = 0;
		
		for(map<int, int>::iterator original_factor_sizes_it = original_factor_sizes.begin(); original_factor_sizes_it != original_factor_sizes.end(); original_factor_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_sizes_it->second);
			total_of_factor_sizes = total_of_factor_sizes + original_factor_sizes_it->second;

			if(max_factor_size == -1)
			{
				max_factor_size = original_factor_sizes_it->second;
				min_factor_size = original_factor_sizes_it->second;
			}
			else if(original_factor_sizes_it->second > max_factor_size)
			{
				max_factor_size = original_factor_sizes_it->second;
			}
			else if(original_factor_sizes_it->second < min_factor_size)
			{
				min_factor_size = original_factor_sizes_it->second;
			}			
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "A_f = ");
		for(map<int, int>::iterator abstracted_factor_sizes_it = abstracted_factor_sizes.begin(); abstracted_factor_sizes_it != abstracted_factor_sizes.end(); abstracted_factor_sizes_it++)
		{
			fprintf(record_fp, "%d, ", abstracted_factor_sizes_it->second);
			total_of_abstracted_factor_sizes = total_of_abstracted_factor_sizes + abstracted_factor_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "V_f = ");
		for(map<int, int>::iterator original_factor_support_sizes_it = original_factor_support_sizes.begin(); original_factor_support_sizes_it != original_factor_support_sizes.end(); original_factor_support_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_support_sizes_it->second);
			total_of_factor_support_sizes = total_of_factor_support_sizes + original_factor_support_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "E_f = ");
		for(map<int, int>::iterator original_factor_varstoelim_sizes_it = original_factor_varstoelim_sizes.begin(); original_factor_varstoelim_sizes_it != original_factor_varstoelim_sizes.end(); original_factor_varstoelim_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_varstoelim_sizes_it->second);
			total_of_factor_varstoelim_sizes = total_of_factor_varstoelim_sizes + original_factor_varstoelim_sizes_it->second;


			if(max_factor_varstoelim_size == -1)
			{
				max_factor_varstoelim_size = original_factor_varstoelim_sizes_it->second;
				min_factor_varstoelim_size = original_factor_varstoelim_sizes_it->second;
			}
			else if(original_factor_varstoelim_sizes_it->second > max_factor_varstoelim_size)
			{
				max_factor_varstoelim_size = original_factor_varstoelim_sizes_it->second;
			}
			else if(original_factor_varstoelim_sizes_it->second < min_factor_varstoelim_size)
			{
				min_factor_varstoelim_size = original_factor_varstoelim_sizes_it->second;
			}

		} 

		if(!perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{
			fprintf(record_fp, "\n\n");

			fprintf(record_fp, "S_v = ");
			for(map<int, set<int> >::iterator Skylines_it = Skylines.begin(); Skylines_it != Skylines.end(); Skylines_it++)
			{
				int skyline_size = (Skylines_it->second).size();
				fprintf(record_fp, "%d, ", skyline_size);
				total_of_skyline_sizes = total_of_skyline_sizes + skyline_size;
			} 
		}

		fprintf(record_fp, "\n\n");

		number_of_compose_operations_for_variable = 0;
		ComposeTime = 0;
				
		if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
		{
			#ifdef RECORD_KEEP
				fprintf(record_fp, "v\tF_v\tT_v\tN_v\tF_v\tOB_v\tB_v\tcmp_v\tcmp_T\tS_T\tF_T\tOB_T\tB_T\tN_T\n\n");
			#endif
		}
		else
		{
			#ifdef DETAILED_RECORD_KEEP
				fprintf(record_fp, "v\tF_v\tT_v\tN_v\tA_v\t#O_v\tDP_v\tCP_v\tDC_v\tC_v\tR_T\tS_T\tA_T\tD_T\tCP_T\tC_T\tN_T\tOr_T\n\n");
			#else
				fprintf(record_fp, "v\tF_v\tT_v\tN_v\tC_v\n\n");
			#endif
		}

		fclose(record_fp);


		string 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", benchmark_type.c_str(), benchmark_name.c_str(), machine.c_str());
		if(disable_factorization || disable_factorization_inside_factorized_code)
		{
			if(use_uninterpreted_functions)
			{
				fprintf(plot_fp, "\tmonolithic_hierarchial");
			}
			else
			{
				fprintf(plot_fp, "\tmonolithic_inlined");
			}
		}
		else
		{
			if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
			{
				fprintf(plot_fp, "\tfactorized_with_qe");
			}
			else if(use_uninterpreted_functions)
			{
				fprintf(plot_fp, "\tfactorized_hierarchial");
			}
			else
			{
				fprintf(plot_fp, "\tfactorized_inlined");
			}

		}
		fprintf(plot_fp, "\t%d\t%d\t%d\t%d\t%d", number_of_factors, number_of_factors, number_of_vars_to_elim, number_of_vars_to_elim, original_support_size);

		t_Expression* conjunction_of_factors = createAnd(Factors, pub_em);
		assert(conjunction_of_factors != NULL);
		int size_of_conjunction_of_factors = computeSize(conjunction_of_factors);		
		fprintf(plot_fp, "\t%d", size_of_conjunction_of_factors);

		float avg_of_factor_sizes = (float)total_of_factor_sizes/(float)number_of_factors;
		float avg_of_abstracted_factor_sizes = (float)total_of_abstracted_factor_sizes/(float)number_of_factors;
		float avg_of_factor_support_sizes = (float)total_of_factor_support_sizes/(float)number_of_factors;
		float avg_of_factor_varstoelim_sizes = (float)total_of_factor_varstoelim_sizes/(float)number_of_factors;
		float avg_of_skyline_sizes = (float)total_of_skyline_sizes/(float)number_of_vars_to_elim;

		if(order_of_elimination_of_variables == 2)
		{
				fprintf(plot_fp, "\t%f\t%f\t%f\t%f", avg_of_factor_sizes, avg_of_abstracted_factor_sizes, avg_of_factor_support_sizes, avg_of_factor_varstoelim_sizes);
		}
		else
		{
			fprintf(plot_fp, "\t%f\t%f\t%f\t%f\t%f", avg_of_factor_sizes, avg_of_abstracted_factor_sizes, avg_of_factor_support_sizes, avg_of_factor_varstoelim_sizes, avg_of_skyline_sizes);
		}

		fclose(plot_fp);
	#endif		
}


void Skolem::factorizedSkolemFunctionGenerator(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	initializeFactorizedSkolemFunctionGenerator(Factors, VariablesToEliminate);

	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	cout << "\ninitializeFactorizedSkolemFunctionGenerator finished in " << step_ms << " milliseconds\n";

	total_time_in_generator_initialization = step_ms;
	#endif

	cout << "\n#factors = " << number_of_factors << "\t#variables_to_eliminate = " << number_of_vars_to_elim << endl;

	if(perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
	{
		assert(order_of_elimination_of_variables != 2); //this is not yet implemented
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}		

			if(maximum_index_to_eliminate != -1) // to stop computation in between
			{
				if(var_to_elim_index > maximum_index_to_eliminate)
				{
					cout << "\nLet us stop here...\n";
					return;
				}			
			}

			#ifdef DEBUG_SKOLEM
			cout << "\ncomputing skolem_function_" << var_to_elim_index << endl;
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\ncomputing skolem_function_" << var_to_elim_index << "\n";
			#endif

			#ifdef RECORD_KEEP
			unsigned long long int duration_ms;
			struct timeval start_ms, finish_ms;
			gettimeofday (&start_ms, NULL); 
			#endif

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_start_ms, NULL); 	
			#endif

			findFactorsWithVariable(var_to_elim_index);// find the set of factors containing the variable			

			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_finish_ms, NULL);
			step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			cout << "\nfindFactorsWithVariable finished in " << step_ms << " milliseconds\n";
		
			cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() << endl;

			FactorFindingTime = step_ms;
			#endif

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_start_ms, NULL); 	
			#endif
		
			t_Expression* cofactor_one_of_bad_set = NULL;
			t_Expression* skolem_function = computeSkolemFunctionUsingBadSet(var_to_elim_index, cofactor_one_of_bad_set);

			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}

			assert(skolem_function != NULL);
			assert(cofactor_one_of_bad_set != NULL);

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_finish_ms, NULL);
			step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			cout << "\ncomputeSkolemFunctionUsingBadSet finished in " << step_ms << " milliseconds\n";
			#endif

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_start_ms, NULL); 	
			#endif
			
			if(use_bad_in_perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
			{
				updateBadSet(var_to_elim_index, cofactor_one_of_bad_set);
			}
			else
			{
				#ifdef RECORD_KEEP
				DeltaCombinedSize = -1;
				#endif
			}

			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_finish_ms, NULL);
			step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			cout << "\nupdateBadSet finished in " << step_ms << " milliseconds\n";
			DeltaCombGenTime = step_ms;
			#endif
			
			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_start_ms, NULL); 	
			#endif
		
			if(var_to_elim_index != number_of_vars_to_elim) // We need to update the factor matrix
			{	
				#ifdef DEBUG_SKOLEM
				cout << "\nupdating factors\n";
				#endif

				if(use_bad_in_perform_cofactor_based_quantifier_elimination_along_with_skolem_function_generation)
				{
					updateFactorsWithoutComposition(var_to_elim_index);
				}
				else
				{
					t_Expression* quantifier_eliminated_result = computeQuantifierEliminatedResultUsingCofactors(var_to_elim_index);
					assert(quantifier_eliminated_result != NULL);

					updateFactorsUsingQuantifierEliminatedResult(var_to_elim_index, quantifier_eliminated_result);
				
				}
			}

			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_finish_ms, NULL);
			step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			cout << "\nupdateFactors finished in " << step_ms << " milliseconds\n";
			NextFactorGenTime = step_ms;
			#endif

			#ifdef DEBUG_SKOLEM
			cout << "\nclearing variable-specific data-structures\n";
			#endif

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_start_ms, NULL); 	
			#endif
		
			clearVariableSpecificDataStructures();

			#ifdef DETAILED_RECORD_KEEP
			gettimeofday (&step_finish_ms, NULL);
			step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			cout << "\nclearVariableSpecificDataStructures finished in " << step_ms << " milliseconds\n";
			#endif

			#ifdef RECORD_KEEP
			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;
			SkolemFunctionGenTime = duration_ms;

			SkolemFunctionSize = computeSize(skolem_function);	
		   	#endif

			string var_to_elim = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
			cout << "\nskolem_function_" << var_to_elim_index << ", i.e., skolem function for " << var_to_elim << " computed\n";

			#ifdef RECORD_KEEP
			string record_file = "skolem_function_generation_details.txt";
			FILE* record_fp = fopen(record_file.c_str(), "a+");
			assert(record_fp != NULL);

			total_of_skyline_sizes_in_least_cost_ordering = 0;
			sum_of_number_of_factors_containing_variable = sum_of_number_of_factors_containing_variable + NumberOfFactors;
			sum_of_skolem_function_sizes = sum_of_skolem_function_sizes + SkolemFunctionSize;
			total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
			total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
			total_time_in_alpha_combined = total_time_in_alpha_combined + AlphaCombGenTime;
			total_time_in_delta_part = total_time_in_delta_part + DeltaPartGenTime;
			total_time_in_delta_combined = total_time_in_delta_combined + DeltaCombGenTime;
			total_time_in_next_factor = total_time_in_next_factor + NextFactorGenTime;
			total_time_in_correction_part = 0;
			number_of_variables_eliminated = var_to_elim_index;
			sum_of_numbers_of_affecting_factors = 0;

			fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\t", var_to_elim.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, AlphaPartSize);

			if(print_factor_graph)
			{
				string fg_file_name = benchmark_name_without_extension;
				if(disable_factorization || disable_factorization_inside_factorized_code)
				{
					fg_file_name += "_monolithic";
				}
				else
				{
					fg_file_name += "_factorized";
				}
				fg_file_name += "_factor_graph.dat";
				FILE* fg_fp = fopen(fg_file_name.c_str(), "a+");
				assert(fg_fp != NULL);			
				for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
				{
					fprintf(fg_fp, "%d\t%d\n", *affect_it, var_to_elim_index);			
				}				
				fclose(fg_fp);
			}
		
			fprintf(record_fp, "%d\t%d\t%d\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu", DeltaPartSize, DeltaCombinedSize, number_of_compose_operations_for_variable, ComposeTime, FactorFindingTime, AlphaCombGenTime, DeltaPartGenTime, DeltaCombGenTime, NextFactorGenTime);

			fprintf(record_fp, "\n\n");

			number_of_compose_operations_for_variable = 0;
			ComposeTime = 0;
		
			fclose(record_fp);
			#endif	

		}//for ends here
		
	}
	else
	{

		if(order_of_elimination_of_variables == 2)
		{
			int var_to_elim_index = 1; 

			while(!unordered_vars_to_elim.empty())
			{
				assert(var_to_elim_index <= number_of_vars_to_elim);

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}		

				if(maximum_index_to_eliminate != -1) // to stop computation in between
				{
					if(var_to_elim_index > maximum_index_to_eliminate)
					{
						cout << "\nLet us stop here...\n";
						return;
					}			
				}

				#ifdef RECORD_KEEP
				unsigned long long int duration_ms;
				struct timeval start_ms, finish_ms;
				gettimeofday (&start_ms, NULL); 
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				string var_to_elim;
				unsigned long long int var_to_elim_cost;
				getNextVariableToEliminate(var_to_elim, var_to_elim_cost, var_to_elim_index-1);

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\ngetNextVariableToEliminate finished in " << step_ms << " milliseconds\n";		
				cout << "\nvar_to_elim = " << var_to_elim << "\tvar_to_elim_cost = " << var_to_elim_cost << endl;

				total_time_in_ordering = total_time_in_ordering + step_ms;
				total_time_in_ordering_for_the_variable = step_ms;
				#endif

				#ifdef DEBUG_SKOLEM
				cout << "\nvar_to_elim = " << var_to_elim << endl;
				cout << "\nvar_to_elim_cost = " << var_to_elim_cost << endl;
				#endif
			
				insertIntoVarNameToVarIndexMap(var_name_to_var_index_map, var_to_elim, var_to_elim_index);
				insertIntoVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index, var_to_elim);

				#ifdef DEBUG_SKOLEM
				cout << "(" << var_to_elim << ", " << var_to_elim_index << ") inserted into maps "<< endl;
				#endif	

				#ifdef DETAILED_RECORD_KEEP
				string order_file_name = benchmark_name_without_extension;
				order_file_name += "_factorized_order.txt";
				FILE* order_fp = fopen(order_file_name.c_str(), "a+");
				assert(order_fp != NULL);
				fprintf(order_fp, "%s\n", var_to_elim.c_str());
				fclose(order_fp);
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				ordered_vars_to_elim.push_back(var_to_elim);
				unordered_vars_to_elim.erase(var_to_elim);
				updateTopVariablesOfFactors(var_to_elim);

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			
				total_time_in_ordering = total_time_in_ordering + step_ms;
				total_time_in_ordering_for_the_variable = total_time_in_ordering_for_the_variable + step_ms;
				#endif

				set<int> SkylineVariables = computeSkylineInLeastCostFirst(var_to_elim, true);

				#ifdef DEBUG_SKOLEM
				showSet(SkylineVariables, "SkylineVariables");
				#endif

				Skylines.insert(make_pair(var_to_elim_index, SkylineVariables));

				#ifdef DEBUG_SKOLEM
				cout << "\ncomputing skolem_function_" << var_to_elim_index << endl;
				#endif

				#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
				cout << "\ncomputing skolem_function_" << var_to_elim_index << "\n";
				#endif
			

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				if(apply_scope_reduction)
				{
					findTopFactorsWithVariable(var_to_elim_index);// find the set of top factors containing the variable
				}
				else
				{
					findFactorsWithVariable(var_to_elim_index);// find the set of factors containing the variable
				}

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nfindFactorsWithVariable finished in " << step_ms << " milliseconds\n";
		
				cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() << endl;

				FactorFindingTime = step_ms;
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				t_Expression* alpha_combined_or_gamma_combined = NULL;
				t_Expression* skolem_function = computeSkolemFunction(var_to_elim_index, alpha_combined_or_gamma_combined);

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\ncomputeSkolemFunction finished in " << step_ms << " milliseconds\n";
				#endif

				assert(skolem_function != NULL);
				int skolem_function_size = computeSize(skolem_function);
				skolemfunctions_to_costs_map.insert(make_pair(var_to_elim_index, skolem_function_size));

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif	

				bool delta_var_to_elim_needed = checkIfDeltaIsNeeded(var_to_elim);

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
			
				total_time_in_ordering = total_time_in_ordering + step_ms;
				total_time_in_ordering_for_the_variable = total_time_in_ordering_for_the_variable + step_ms;
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				#ifdef DEBUG_SKOLEM
				cout << "\ndelta_var_to_elim_needed = " << delta_var_to_elim_needed << "\n";
				#endif

				#ifdef RECORD_KEEP
				DeltaCombinedSize = -1;
				#endif

				if(delta_var_to_elim_needed) // var_to_elim_index is 
				// in the skyline of some variable
				{
					#ifdef DEBUG_SKOLEM
					cout << "\ncomputing delta_combined_" << var_to_elim_index << "\n";
					#endif

					#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
					cout << "\ncomputing delta_combined_" << var_to_elim_index << "\n";
					#endif

					// delta-combined for var_to_elim_index will be needed later on;
					// let's find and store it right now
					if(compute_delta_combined_as_individual_factors)
					{	
						map<int, t_Expression*> factor_wise_delta_combined;

						if(disable_factorization_inside_factorized_code)
						{
							assert(skolem_function != NULL);
						 	computeDeltaCombined(var_to_elim_index, skolem_function, factor_wise_delta_combined);					
						}
						else if(use_local_skolem_function_in_delta_combined_computation)
						{
							assert(alpha_combined_or_gamma_combined != NULL);
						 	computeDeltaCombined(var_to_elim_index, alpha_combined_or_gamma_combined, factor_wise_delta_combined);
						}
						else
						{
							cout << "\nThis part is not implemented\n";
							assert(false);
						}

						if(checkTimeOut()) // check for time-out
						{
							cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
							timed_out = true; // timed_out flag set
							return;
						}

						FactorWiseDeltaCombinedMatrix.insert(make_pair(var_to_elim_index, factor_wise_delta_combined)); 
						insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, var_to_elim_index, var_to_elim_index, false);

					
						int delta_cost;
						delta_cost = computeCostOfFactorWiseDeltaCombined(factor_wise_delta_combined);
						deltas_to_costs_map.insert(make_pair(var_to_elim_index, delta_cost));

						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						cout << "\nsize of delta_combined is " << delta_cost << endl;
						#endif

						#ifdef RECORD_KEEP
						DeltaCombinedSize = -1;
						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						DeltaCombinedSize = delta_cost;
						#endif
						#endif
					}
					else
					{
						t_Expression* delta_combined;

						if(disable_factorization_inside_factorized_code)
						{
							assert(skolem_function != NULL);
							delta_combined = computeDeltaCombined(var_to_elim_index, skolem_function);
						}
						else if(use_local_skolem_function_in_delta_combined_computation)
						{
							assert(alpha_combined_or_gamma_combined != NULL);
						 	delta_combined = computeDeltaCombined(var_to_elim_index, alpha_combined_or_gamma_combined);
						}
						else
						{
							delta_combined = computeDeltaCombined(var_to_elim_index);
						}

						if(checkTimeOut()) // check for time-out
						{
							cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
							timed_out = true; // timed_out flag set
							return;
						}

						insertIntoOneDimensionalMatrix(DeltaCombinedMatrix, number_of_vars_to_elim, var_to_elim_index, delta_combined, false);
						insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, var_to_elim_index, var_to_elim_index, false);

						assert(delta_combined != NULL);
						int delta_cost = computeSize(delta_combined);
						deltas_to_costs_map.insert(make_pair(var_to_elim_index, delta_cost));

						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						cout << "\nsize of delta_combined is " << delta_cost << endl;
						#endif

						#ifdef RECORD_KEEP
						DeltaCombinedSize = -1;
						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						DeltaCombinedSize = delta_cost;
						#endif
						#endif
					}
			
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\ncomputeDeltaCombined finished in " << step_ms << " milliseconds\n";
				DeltaCombGenTime = step_ms;		
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				if(!apply_scope_reduction)
				{
					if(var_to_elim_index != number_of_vars_to_elim) // We need to update the factor matrix
					{	
						#ifdef DEBUG_SKOLEM
						cout << "\nupdating factors\n";
						#endif

						updateFactors(var_to_elim_index);
					}
				}

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nupdateFactors finished in " << step_ms << " milliseconds\n";
				NextFactorGenTime = step_ms;
				#endif

				#ifdef DEBUG_SKOLEM
				cout << "\nclearing variable-specific data-structures\n";
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				clearVariableSpecificDataStructures();

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nclearVariableSpecificDataStructures finished in " << step_ms << " milliseconds\n";
				#endif

				#ifdef RECORD_KEEP
				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;
				SkolemFunctionGenTime = duration_ms;

				SkolemFunctionSize = skolem_function_size;	
		   		#endif

				cout << "\nskolem_function_" << var_to_elim_index << ", i.e., skolem function for " << var_to_elim << " computed\n";

				#ifdef RECORD_KEEP
				string record_file = "skolem_function_generation_details.txt";
				FILE* record_fp = fopen(record_file.c_str(), "a+");
				assert(record_fp != NULL);

				total_of_skyline_sizes_in_least_cost_ordering = total_of_skyline_sizes_in_least_cost_ordering + SkylineVariables.size();
				sum_of_number_of_factors_containing_variable = sum_of_number_of_factors_containing_variable + NumberOfFactors;
				sum_of_skolem_function_sizes = sum_of_skolem_function_sizes + SkolemFunctionSize;
				total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
				total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
				total_time_in_alpha_combined = total_time_in_alpha_combined + AlphaCombGenTime;
				total_time_in_delta_part = total_time_in_delta_part + DeltaPartGenTime;
				total_time_in_delta_combined = total_time_in_delta_combined + DeltaCombGenTime;
				total_time_in_next_factor = total_time_in_next_factor + NextFactorGenTime;
				total_time_in_correction_part = total_time_in_correction_part + CorrectionPartGenTime;
				number_of_variables_eliminated = var_to_elim_index;
				sum_of_numbers_of_affecting_factors = sum_of_numbers_of_affecting_factors + FactorsAffectingSkolemFunction.size();

				#ifdef DETAILED_RECORD_KEEP
				fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\t", var_to_elim.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, AlphaPartSize);

				if(print_factor_graph)
				{
					string fg_file_name = benchmark_name_without_extension;
					if(disable_factorization || disable_factorization_inside_factorized_code)
					{
						fg_file_name += "_monolithic";
					}
					else
					{
						fg_file_name += "_factorized";
					}
					fg_file_name += "_factor_graph.dat";
					FILE* fg_fp = fopen(fg_file_name.c_str(), "a+");
					assert(fg_fp != NULL);			
					for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
					{
						fprintf(fg_fp, "%d\t%d\n", *affect_it, var_to_elim_index);			
					}				
					fclose(fg_fp);
				}
		
				string 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\nv = %s", var_to_elim.c_str());
				fprintf(size_fp, "\nS_v = ");
				for(set<int>::iterator skyline_it = Skylines[var_to_elim_index].begin(); skyline_it != Skylines[var_to_elim_index].end(); skyline_it++)
				{
					fprintf(size_fp, "%d,", *skyline_it);			
				}
		
				fprintf(size_fp, "\nF_v = ");

				for(set<int>::iterator factor_it = PreviousFactorsWithVariable.begin(); factor_it != PreviousFactorsWithVariable.end(); factor_it++)
				{
					fprintf(size_fp, "%d,", *factor_it);			
				}
				
				fprintf(size_fp, "\nX_v = ");		
				PreviousFactorsWithVariable.clear();

				for(list<int>::iterator size_it = sizes_of_factors_affecting_variable.begin(); size_it != sizes_of_factors_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}		
			
				fprintf(size_fp, "\nO_v = ");	
				sizes_of_factors_affecting_variable.clear();

				for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
				{
					fprintf(size_fp, "%d,", *affect_it);			
				}	

				fprintf(size_fp, "\n/\\_v = ");
				for(list<int>::iterator size_it = sizes_of_conflict_conjuncts_affecting_variable.begin(); size_it != sizes_of_conflict_conjuncts_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}
				sizes_of_conflict_conjuncts_affecting_variable.clear();

				fprintf(size_fp, "\n1_v = ");
				for(list<int>::iterator size_it = sizes_of_cofactors_affecting_variable.begin(); size_it != sizes_of_cofactors_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}
				sizes_of_cofactors_affecting_variable.clear();
				fprintf(size_fp, "\nA_v = %d\nN_v = %d", AlphaPartSize, SkolemFunctionSize);
			
				fclose(size_fp);


				fprintf(record_fp, "%d", FactorsAffectingSkolemFunction.size());			
				
				FactorsAffectingSkolemFunction.clear();

				fprintf(record_fp, "\t%d\t%d\t%d\t%d\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu", DeltaPartSize, CorrectionPartSize, DeltaCombinedSize, number_of_compose_operations_for_variable, ComposeTime, FactorFindingTime, AlphaCombGenTime, DeltaPartGenTime, CorrectionPartGenTime, DeltaCombGenTime, NextFactorGenTime);

				fprintf(record_fp, "\t");
				fprintf(record_fp, "%llu", total_time_in_ordering_for_the_variable);
			

				fprintf(record_fp, "\n\n");
				#else
				fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\n\n", var_to_elim.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable);
				#endif

				number_of_compose_operations_for_variable = 0;
				ComposeTime = 0;
		
				fclose(record_fp);
				#endif			

				var_to_elim_index++;

				#ifdef DEBUG_SKOLEM
				showDataStructuresForLeastCostOrdering();
				#endif
			}//while ends here
		}
		else
		{
			// compute the skolem functions, i.e. fill the SkolemFunctions matrix
			for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
			{
				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}		

				if(maximum_index_to_eliminate != -1) // to stop computation in between
				{
					if(var_to_elim_index > maximum_index_to_eliminate)
					{
						cout << "\nLet us stop here...\n";
						return;
					}			
				}

				#ifdef DEBUG_SKOLEM
				cout << "\ncomputing skolem_function_" << var_to_elim_index << endl;
				#endif

				#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
				cout << "\ncomputing skolem_function_" << var_to_elim_index << "\n";
				#endif

				#ifdef RECORD_KEEP
				unsigned long long int duration_ms;
				struct timeval start_ms, finish_ms;
				gettimeofday (&start_ms, NULL); 
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				if(apply_scope_reduction)
				{
					findTopFactorsWithVariable(var_to_elim_index);// find the set of top factors containing the variable
				}
				else
				{
					findFactorsWithVariable(var_to_elim_index);// find the set of factors containing the variable
				}

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nfindFactorsWithVariable finished in " << step_ms << " milliseconds\n";
		
				cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() << endl;

				FactorFindingTime = step_ms;
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				t_Expression* alpha_combined_or_gamma_combined = NULL;
				t_Expression* skolem_function = computeSkolemFunction(var_to_elim_index, alpha_combined_or_gamma_combined);

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\ncomputeSkolemFunction finished in " << step_ms << " milliseconds\n";
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif

				assert(skolem_function != NULL);

				#ifdef RECORD_KEEP
				DeltaCombinedSize = -1;
				#endif

				if(UnionOfSkylines.find(var_to_elim_index) != UnionOfSkylines.end()) // var_to_elim_index is 
				// in the skyline of some variable
				{
					#ifdef DEBUG_SKOLEM
					cout << "\ncomputing delta_combined_" << var_to_elim_index << "\n";
					#endif

					#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
					cout << "\ncomputing delta_combined_" << var_to_elim_index << "\n";
					#endif

					// delta-combined for var_to_elim_index will be needed later on;
					// let's find and store it right now
					if(compute_delta_combined_as_individual_factors)
					{	
						map<int, t_Expression*> factor_wise_delta_combined;

						if(disable_factorization_inside_factorized_code)
						{
							assert(skolem_function != NULL);
						 	computeDeltaCombined(var_to_elim_index, skolem_function, factor_wise_delta_combined);					
						}
						else if(use_local_skolem_function_in_delta_combined_computation)
						{
							assert(alpha_combined_or_gamma_combined != NULL);
						 	computeDeltaCombined(var_to_elim_index, alpha_combined_or_gamma_combined, factor_wise_delta_combined);
						}
						else
						{
							cout << "\nThis part is not implemented\n";
							assert(false);
						}

						if(checkTimeOut()) // check for time-out
						{
							cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
							timed_out = true; // timed_out flag set
							return;
						}

						FactorWiseDeltaCombinedMatrix.insert(make_pair(var_to_elim_index, factor_wise_delta_combined)); 
						insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, var_to_elim_index, var_to_elim_index, false);

					
						int delta_cost;
						delta_cost = computeCostOfFactorWiseDeltaCombined(factor_wise_delta_combined);
						deltas_to_costs_map.insert(make_pair(var_to_elim_index, delta_cost));

						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						cout << "\nsize of delta_combined is " << delta_cost << endl;
						#endif

						#ifdef RECORD_KEEP
						DeltaCombinedSize = -1;
						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						DeltaCombinedSize = delta_cost;
						#endif
						#endif
					}
					else
					{
						t_Expression* delta_combined;

						if(disable_factorization_inside_factorized_code)
						{
							assert(skolem_function != NULL);
						 	delta_combined = computeDeltaCombined(var_to_elim_index, skolem_function);		
						}
						else if(use_local_skolem_function_in_delta_combined_computation)
						{
							assert(alpha_combined_or_gamma_combined != NULL);
						 	delta_combined = computeDeltaCombined(var_to_elim_index, alpha_combined_or_gamma_combined);
						}
						else
						{
							delta_combined = computeDeltaCombined(var_to_elim_index);
						}

						if(checkTimeOut()) // check for time-out
						{
							cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
							timed_out = true; // timed_out flag set
							return;
						}

						insertIntoOneDimensionalMatrix(DeltaCombinedMatrix, number_of_vars_to_elim, var_to_elim_index, delta_combined, false);
						insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, var_to_elim_index, var_to_elim_index, false);

						assert(delta_combined != NULL);
						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						cout << "\nsize of delta_combined is " << computeSize(delta_combined) << endl;
						#endif

						#ifdef RECORD_KEEP
						DeltaCombinedSize = -1;
						#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
						DeltaCombinedSize = computeSize(delta_combined);
						#endif
						#endif
					}
			
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\ncomputeDeltaCombined finished in " << step_ms << " milliseconds\n";
				DeltaCombGenTime = step_ms;		
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				if(!apply_scope_reduction) // no need to update factors when apply_scope_reduction is true
				{
					if(var_to_elim_index != number_of_vars_to_elim) // We need to update the factor matrix
					{
						#ifdef DEBUG_SKOLEM
						cout << "\nupdating factors\n";
						#endif

						updateFactors(var_to_elim_index);
					}
				}

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::factorizedSkolemFunctionGenerator\n";
					timed_out = true; // timed_out flag set
					return;
				}

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nupdateFactors finished in " << step_ms << " milliseconds\n";
				NextFactorGenTime = step_ms;
				#endif

				#ifdef DEBUG_SKOLEM
				cout << "\nclearing variable-specific data-structures\n";
				#endif

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_start_ms, NULL); 	
				#endif
		
				clearVariableSpecificDataStructures();

				#ifdef DETAILED_RECORD_KEEP
				gettimeofday (&step_finish_ms, NULL);
			   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
			   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
				cout << "\nclearVariableSpecificDataStructures finished in " << step_ms << " milliseconds\n";
				#endif

				#ifdef RECORD_KEEP
				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;
				SkolemFunctionGenTime = duration_ms;

				int skolem_function_size = computeSize(skolem_function);
				SkolemFunctionSize = skolem_function_size;	
		   		#endif

				string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
				cout << "\nskolem_function_" << var_to_elim_index << ", i.e., skolem function for " << var_to_elim_name << " computed\n";

				#ifdef RECORD_KEEP
				string record_file = "skolem_function_generation_details.txt";
				FILE* record_fp = fopen(record_file.c_str(), "a+");
				assert(record_fp != NULL);

				sum_of_number_of_factors_containing_variable = sum_of_number_of_factors_containing_variable + NumberOfFactors;
				sum_of_skolem_function_sizes = sum_of_skolem_function_sizes + SkolemFunctionSize;
				total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
				total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
				total_time_in_alpha_combined = total_time_in_alpha_combined + AlphaCombGenTime;
				total_time_in_delta_part = total_time_in_delta_part + DeltaPartGenTime;
				total_time_in_delta_combined = total_time_in_delta_combined + DeltaCombGenTime;
				total_time_in_next_factor = total_time_in_next_factor + NextFactorGenTime;
				total_time_in_correction_part = total_time_in_correction_part + CorrectionPartGenTime;
				number_of_variables_eliminated = var_to_elim_index;
				sum_of_numbers_of_affecting_factors = sum_of_numbers_of_affecting_factors + FactorsAffectingSkolemFunction.size();

				#ifdef DETAILED_RECORD_KEEP
				fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\t", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, AlphaPartSize);


				if(print_factor_graph)
				{
					string fg_file_name = benchmark_name_without_extension;
					if(disable_factorization || disable_factorization_inside_factorized_code)
					{
						fg_file_name += "_monolithic";
					}
					else
					{
						fg_file_name += "_factorized";
					}
					fg_file_name += "_factor_graph.dat";
					FILE* fg_fp = fopen(fg_file_name.c_str(), "a+");
					assert(fg_fp != NULL);			
					for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
					{
						fprintf(fg_fp, "%d\t%d\n", *affect_it, var_to_elim_index);			
					}
					fprintf(fg_fp, "\n");
					fclose(fg_fp);
				}

				string 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\nv = %s", var_to_elim_name.c_str());
				fprintf(size_fp, "\nS_v = ");
				for(set<int>::iterator skyline_it = Skylines[var_to_elim_index].begin(); skyline_it != Skylines[var_to_elim_index].end(); skyline_it++)
				{
					fprintf(size_fp, "%d,", *skyline_it);			
				}
		
				fprintf(size_fp, "\nF_v = ");

				for(set<int>::iterator factor_it = PreviousFactorsWithVariable.begin(); factor_it != PreviousFactorsWithVariable.end(); factor_it++)
				{
					fprintf(size_fp, "%d,", *factor_it);			
				}
				
				fprintf(size_fp, "\nX_v = ");		
				PreviousFactorsWithVariable.clear();

				for(list<int>::iterator size_it = sizes_of_factors_affecting_variable.begin(); size_it != sizes_of_factors_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}		
			
				fprintf(size_fp, "\nO_v = ");	
				sizes_of_factors_affecting_variable.clear();

				for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
				{
					fprintf(size_fp, "%d,", *affect_it);			
				}	

				fprintf(size_fp, "\n/\\_v = ");
				for(list<int>::iterator size_it = sizes_of_conflict_conjuncts_affecting_variable.begin(); size_it != sizes_of_conflict_conjuncts_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}
				sizes_of_conflict_conjuncts_affecting_variable.clear();

				fprintf(size_fp, "\n1_v = ");
				for(list<int>::iterator size_it = sizes_of_cofactors_affecting_variable.begin(); size_it != sizes_of_cofactors_affecting_variable.end(); size_it++)
				{
					fprintf(size_fp, "%d,", *size_it);			
				}
				sizes_of_cofactors_affecting_variable.clear();
				fprintf(size_fp, "\nA_v = %d\nN_v = %d", AlphaPartSize, SkolemFunctionSize);
			
				fclose(size_fp);
			
				fprintf(record_fp, "%d", FactorsAffectingSkolemFunction.size());			
						
				FactorsAffectingSkolemFunction.clear();


				fprintf(record_fp, "\t%d\t%d\t%d\t%d\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu\t%llu", DeltaPartSize, CorrectionPartSize, DeltaCombinedSize, number_of_compose_operations_for_variable, ComposeTime, FactorFindingTime, AlphaCombGenTime, DeltaPartGenTime, CorrectionPartGenTime, DeltaCombGenTime, NextFactorGenTime);


				fprintf(record_fp, "\t");
				fprintf(record_fp, "-");
			

				fprintf(record_fp, "\n\n");
				#else
				fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\n\n", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable);
				#endif

				number_of_compose_operations_for_variable = 0;
				ComposeTime = 0;
		
				fclose(record_fp);
				#endif						
			}// for ends here
		}// if(order_of_elimination_of_variables != 2)
	}


	if(use_uninterpreted_functions && false) // write the AbstractedTounabstractedFunctionsMap
	{
		string final_qe_result_file = benchmark_name_without_extension;
		final_qe_result_file += "_output.v";
		writeAbstractedTounabstractedFunctionsMap(pub_em, AbstractedTounabstractedFunctionsMap, final_qe_result_file);
	}

	if(perform_reverse_substitution)
	{
		performReverseSubstitutionOfSkolemFunctions();
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			#ifdef RECORD_KEEP
			int final_skolem_function_size = computeSize(final_skolem_function);
			skolem_function_sizes_after_reverse_substitution.push_back(final_skolem_function_size);
			sum_of_skolem_function_sizes_after_reverse_substitution = sum_of_skolem_function_sizes_after_reverse_substitution + final_skolem_function_size;
			#endif

			#ifdef PRINT_SKOLEM_FUNCTIONS
			string skolem_function_file_name = benchmark_name_without_extension;
			skolem_function_file_name += "_skolem_function_after_reverse_substitution";
			writeFormulaToFile(pub_em, final_skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
			#endif
		}
	}

	if(match_outputs_of_monolithic_and_factorized)
	{
		t_Expression* ConjunctionOfFactors = createAnd(Factors, pub_em);
		assert(ConjunctionOfFactors != NULL);
		t_Expression* ConjunctionOfFactors_with_var_substituted = ConjunctionOfFactors;
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
			
			t_HashTable<unsigned long, t_Expression*> cache;
			ConjunctionOfFactors_with_var_substituted = pub_em->ReplaceLeafByExpression(ConjunctionOfFactors_with_var_substituted, var_to_elim_name, final_skolem_function, cache, false, 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);

			assert(ConjunctionOfFactors_with_var_substituted != NULL);			

		}//for ends here
	
		result_of_qe_using_factorized = ConjunctionOfFactors_with_var_substituted;		
	}
}




void Skolem::findFactorsWithVariable(int var_to_elim_index)
{
	#ifdef DEBUG_SKOLEM
	cout << "\nfinding factors with variable_" << var_to_elim_index << endl;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	/*
	string support_file_name = benchmark_name_without_extension;
	support_file_name += "_support.txt";
	FILE* support_fp = fopen(support_file_name.c_str(), "a+");
	assert(support_fp != NULL);
	fprintf(support_fp, "\nsizes of factors : ");	*/
	#endif

	FactorsWithVariable.clear();

	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index, factor_index);	
		#endif

		#ifdef DETAILED_RECORD_KEEP
		//fprintf(support_fp, "%d,", computeSize(factor));	
		#endif
		
		if(!formulaFreeOfVariable(factor, var_to_elim_index))
		{
			FactorsWithVariable.insert(factor_index);

			#ifdef DETAILED_RECORD_KEEP
			int factor_size = computeSize(factor);
			sizes_of_factors_with_variable.push_back(factor_size);
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nfactor_ " << factor_index << " of size " << factor_size << " encountered with variable_" << var_to_elim_index << endl;
			#endif
		}
	}

	#ifdef DETAILED_RECORD_KEEP
	/*
	fprintf(support_fp, "\nsizes of factors with variable : ");	
	for(list<int>::iterator size_it = sizes_of_factors_with_variable.begin(); size_it != sizes_of_factors_with_variable.end(); size_it++)
	{
		fprintf(support_fp, "%d,", *size_it);			
	}
	fclose(support_fp);*/
	#endif

	#ifdef DEBUG_SKOLEM
	showSet(FactorsWithVariable, "FactorsWithVariable");
	#endif
}


t_Expression* Skolem::computeSkolemFunction(int var_to_elim_index, t_Expression* &alpha_combined_or_gamma_combined)
{
	// if permissive of zeroes, then
	// 	skolem_function = alpha_combined_{var_to_elim_index} \vee delta_part, where
	// 	delta_part = \bigvee {prev_index = var_to_elim_index-1 downto prev_index = 1}. delta_combined_{prev_index} with
	//	variable at var_to_elim_index set to 0 and 
	// 	variables at prev_index+1 downto var_to_elim_index-1 substituted by their skolem functions
	// else if permissive of ones, then
	//	skolem_function = alpha_combined_or_gamma_combined{var_to_elim_index} \wedge delta_part, where
	// 	delta_part = \bigwedge {prev_index = var_to_elim_index-1 downto prev_index = 1}. \neg delta_combined_{prev_index} with
	//	variable at var_to_elim_index set to 1 and 
	// 	variables at prev_index+1 downto var_to_elim_index-1 substituted by their skolem functions

	#ifdef RECORD_KEEP
	unsigned long long int alpha_duration_ms, skyline_duration_ms, delta_duration_ms, correction_duration_ms;
	struct timeval start_ms, finish_ms;
	#endif

	t_Expression* alpha_combined;

	if(permissive_of_ones)
	{
		
		#ifdef RECORD_KEEP
		gettimeofday (&start_ms, NULL); 
		#endif

		// computing alpha_combined_or_gamma_combined{var_to_elim_index}
		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing alpha_combined_or_gamma_combined_" << var_to_elim_index << "\n";
		#endif
		
		alpha_combined_or_gamma_combined = computeAlphaCombinedOrGammaCombined(var_to_elim_index);
		assert(alpha_combined_or_gamma_combined != NULL);

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::computeSkolemFunction\n";
			timed_out = true; // timed_out flag set
			return NULL;
		}

		#ifdef DEBUG_SKOLEM
		cout << "\nalpha_combined_or_gamma_combined_" << var_to_elim_index << " computed\n";
		#endif

		#ifdef RECORD_KEEP
		gettimeofday (&finish_ms, NULL);
		alpha_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
		alpha_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
		AlphaCombGenTime = alpha_duration_ms;
		#endif

		#ifdef DETAILED_RECORD_KEEP
		cout << "\ncomputeAlphaCombinedOrGammaCombined finished in " << alpha_duration_ms << "milli seconds\n";
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nsize of alpha_combined_or_gamma_combined is " << computeSize(alpha_combined_or_gamma_combined) << endl;
		#endif

		#ifdef RECORD_KEEP
		//AlphaPartSize = -1;
		AlphaPartSize = computeSize(alpha_combined_or_gamma_combined);
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		AlphaPartSize = computeSize(alpha_combined_or_gamma_combined); //there's time spent in this.Use this only when needed
		#endif
		#endif

	}	
	else
	{

		#ifdef RECORD_KEEP
		gettimeofday (&start_ms, NULL); 
		#endif

		// computing alpha_combined_{var_to_elim_index}
		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing alpha_combined_" << var_to_elim_index << "\n";
		#endif
		
		alpha_combined = computeAlphaCombined(var_to_elim_index);
		assert(alpha_combined != NULL);

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::computeSkolemFunction\n";
			timed_out = true; // timed_out flag set
			return NULL;
		}

		#ifdef DEBUG_SKOLEM
		cout << "\nalpha_combined_" << var_to_elim_index << " computed\n";
		#endif

		#ifdef RECORD_KEEP
		gettimeofday (&finish_ms, NULL);
		alpha_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
		alpha_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
		AlphaCombGenTime = alpha_duration_ms;
		#endif

		#ifdef DETAILED_RECORD_KEEP
		cout << "\ncomputeAlphaCombined finished in " << alpha_duration_ms << "milli seconds\n";
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nsize of alpha_combined is " << computeSize(alpha_combined) << endl;
		#endif

	}
		
	// computing delta_part
	t_Expression* delta_part;
	set<t_Expression*> delta_part_components; // delta_part = disjunction of delta_part_components

	// while considering the delta_part_components, we need to consider only
	// the skyline variables

	#ifdef RECORD_KEEP
	gettimeofday (&start_ms, NULL); 
	#endif

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing skyline_" << var_to_elim_index << "\n";
	#endif

	// Let's compute the skyline first
	set<int> SkylineVariables = Skylines[var_to_elim_index];

	#ifdef DEBUG_SKOLEM
	cout << "\nskyline_" << var_to_elim_index << " computed\n";
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&finish_ms, NULL);
	skyline_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
	skyline_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
	SkylineGenTime = skyline_duration_ms;
	#endif

	#ifdef DEBUG_SKOLEM
	showSet(SkylineVariables, "SkylineVariables");
	#endif

	#ifdef RECORD_KEEP
	SkylineSize = SkylineVariables.size();
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&start_ms, NULL); 
	#endif
		
	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing delta_part_" << var_to_elim_index << "\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\ncomputing delta_part_" << var_to_elim_index << "\n";
	#endif

	for(set<int>::iterator variable_it = SkylineVariables.begin(); variable_it != SkylineVariables.end(); variable_it++)
	{
		int prev_index = *variable_it;
		assert(prev_index >= 1 && prev_index < var_to_elim_index);			
			
		// We need to take delta_combined at prev_index, and replace 
		// variables at prev_index+1 to var_to_elim_index-1 by their skolem functions
		// and variable at var_to_elim_index by 0 to obtain delta_part_component at prev_index

		// computing delta_part_component

		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing delta_part_component_" << prev_index << "\n";
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\ncomputing delta_part_component_" << prev_index << "\n";
		#endif

		t_Expression* delta_part_component;
		delta_part_component = computeDeltaCombinedWithSubstitutions(prev_index, var_to_elim_index); 
		assert(delta_part_component != NULL);

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::computeSkolemFunction\n";
			timed_out = true; // timed_out flag set
			return NULL;
		}


		if(permissive_of_ones && !use_local_skolem_function_in_delta_combined_computation)
		{
			delta_part_component = createNot(delta_part_component, pub_em);
			assert(delta_part_component != NULL);
		}

		#ifdef DEBUG_SKOLEM
		cout << "\ndelta_part_component_" << prev_index << " computed\n";
		writeFormulaToFile(pub_em, delta_part_component, "delta_part_component", ".v", prev_index, var_to_elim_index);
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\ndelta_part_component_" << prev_index << " computed\n";
		cout << "\nsize of delta_part_component_" << prev_index << " is: " << computeSize(delta_part_component) << endl;
		#endif

		delta_part_components.insert(delta_part_component);
	}

	//cout << "\ncomputing delta_part\n";

	if(delta_part_components.empty())
	{
		delta_part = NULL;

		#ifdef DEBUG_SKOLEM
		cout << "\ndelta_part is empty\n";
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\ndelta_part is empty\n";
		#endif

		#ifdef RECORD_KEEP
		DeltaPartSize = -1;
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		DeltaPartSize = 0;
		#endif
		#endif

	}
	else
	{
		if(permissive_of_ones)
		{
			// obtain conjunction of delta_part_components
			delta_part = createAnd(delta_part_components, pub_em);		
		}
		else
		{
			// obtain disjunction of delta_part_components
			delta_part = createOr(delta_part_components, pub_em);			
		}

		assert(delta_part != NULL);

		#ifdef DEBUG_SKOLEM
		cout << "\ndelta_part computed\n";
		writeFormulaToFile(pub_em, delta_part, "delta_part", ".v", var_to_elim_index, 0);
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nsize of delta_part is " << computeSize(delta_part) << endl;
		#endif

		#ifdef RECORD_KEEP
		DeltaPartSize = -1;
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		DeltaPartSize = computeSize(delta_part);
		#endif
		#endif
	}

	#ifdef DEBUG_SKOLEM
	cout << "\ndelta_part_" << var_to_elim_index << " computed\n";
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&finish_ms, NULL);
	delta_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
	delta_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
	DeltaPartGenTime = delta_duration_ms;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	cout << "\ncomputing delta part finished in " << delta_duration_ms << "milli seconds\n";
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&start_ms, NULL); 
	#endif
		
	#ifdef RECORD_KEEP
	CorrectionPartSize = -1;
	#endif

	if(!disable_factorization_inside_factorized_code && apply_correction_factor)
	{

		// we need to disjoin the correction-part with the delta-part if var_to_elim_index != 1
		if(var_to_elim_index != 1)
		{
			if(permissive_of_ones)
			{
		
				// computing correction_part{var_to_elim_index}
				#ifdef DEBUG_SKOLEM
				cout << "\ncomputing correction_part_" << var_to_elim_index << "\n";
				#endif
		
				t_Expression* correction_part = computeCorrectionPart(var_to_elim_index);
				assert(correction_part != NULL);

				if(checkTimeOut()) // check for time-out
				{
					cout << "\nWarning!!Time-out inside the function Skolem::computeSkolemFunction\n";
					timed_out = true; // timed_out flag set
					return NULL;
				}

				#ifdef DEBUG_SKOLEM
				cout << "\ncorrection_part_" << var_to_elim_index << " computed\n";
				#endif

				if(delta_part == NULL)
				{
					delta_part  = correction_part;	
				}
				else
				{
					delta_part = createOr(delta_part, correction_part, pub_em);
				}
				assert(delta_part != NULL);

				#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
				CorrectionPartSize = computeSize(correction_part);
				#endif			
			}	
			else
			{
				cout << "\nCorrection-part computation is not implemented for permissive of zeroes\n";
				assert(false);
			}
		}//if(var_to_elim_index != 1)
	}//if(apply_correction_factor)

	#ifdef RECORD_KEEP
	gettimeofday (&finish_ms, NULL);
	correction_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
	correction_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
	CorrectionPartGenTime = correction_duration_ms;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	cout << "\ncomputing correction part finished in " << correction_duration_ms << "milli seconds\n";
	#endif

        //computing skolem_function

	t_Expression* skolem_function;	
	if(delta_part == NULL)
	{
		if(permissive_of_ones)
		{
			// skolem_function = alpha_combined_or_gamma_combined_{var_to_elim_index}
			skolem_function = alpha_combined_or_gamma_combined;
		}
		else
		{
			// skolem_function = alpha_combined_{var_to_elim_index}
			skolem_function = alpha_combined;
		}
	}
	else
	{
		if(permissive_of_ones)
		{			
			// skolem_function = alpha_combined_or_gamma_combined_{var_to_elim_index} \vee delta_part
			skolem_function = createAnd(alpha_combined_or_gamma_combined, delta_part, pub_em);	
		}
		else
		{
			// skolem_function = alpha_combined_{var_to_elim_index} \vee delta_part	
			skolem_function = createOr(alpha_combined, delta_part, pub_em);			
		}

		assert(skolem_function != NULL);
	}

	if(use_uninterpreted_functions) // abstract the skolem_function
	{
		set<string> support_skolem_function;
		computeSupport(skolem_function, support_skolem_function);
		string name_of_function = "skolem";
		t_Expression* abstracted_skolem_function = createAbstraction(name_of_function, var_to_elim_index, 0, support_skolem_function, pub_em);
		assert(abstracted_skolem_function != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_skolem_function, skolem_function));
		skolem_function = abstracted_skolem_function;
	}

	#ifdef DEBUG_SKOLEM
	cout << "\nskolem_function computed\n";		
	//cout << endl << skolem_function << " inserted in SkolemFunctions[" << var_to_elim_index << "]"<< "\n";
	#endif

	#ifdef PRINT_SKOLEM_FUNCTIONS
	string skolem_function_file_name = benchmark_name_without_extension;
	skolem_function_file_name += "_skolem_function";
	writeFormulaToFile(pub_em, skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
	#endif

	// Enter into matrix
	insertIntoOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index, skolem_function, false);
		
	return skolem_function;		
}



t_Expression* Skolem::computeDeltaCombinedWithSubstitutions(int delta_combined_index, int var_to_elim_index)
{
	// sanity checks
	assert(delta_combined_index >= 1);
	assert(var_to_elim_index > delta_combined_index);

	// obtain delta_combined at delta_combined_index with
	// skolem functions substituted for variables from delta_combined_index+1 to var_to_elim_index-1
	
	t_Expression* delta_combined_with_skolem_functions_substituted;
	if(compute_delta_combined_as_individual_factors)
	{
		delta_combined_with_skolem_functions_substituted = computeDeltaCombinedWithSkolemFunctionsSubstitutedKeepingFactorsIndividual(delta_combined_index, var_to_elim_index-1);
	}	
	else
	{
		delta_combined_with_skolem_functions_substituted = computeDeltaCombinedWithSkolemFunctionsSubstituted(delta_combined_index, var_to_elim_index-1);
	}
	assert(delta_combined_with_skolem_functions_substituted != NULL);

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nsize of input to replaceVariableByConstant is: " << computeSize(delta_combined_with_skolem_functions_substituted) << endl;
	#endif

	t_Expression* delta_combined_with_substitutions;	
	if(permissive_of_ones)
	{
		// replace var_to_elim_index in delta_combined_with_skolem_functions_substituted by one
		if(reuse_same_cache_for_computations)
		{
			delta_combined_with_substitutions = replaceVariableByConstant(delta_combined_with_skolem_functions_substituted, var_to_elim_index, 1, pub_cofactor_one_cache);
		}
		else
		{
			delta_combined_with_substitutions = replaceVariableByConstant(delta_combined_with_skolem_functions_substituted, var_to_elim_index, 1);
		}
		
	}	
	else
	{
		// replace var_to_elim_index in delta_combined_with_skolem_functions_substituted by zero
		if(reuse_same_cache_for_computations)
		{
			delta_combined_with_substitutions = replaceVariableByConstant(delta_combined_with_skolem_functions_substituted, var_to_elim_index, 0, pub_cofactor_zero_cache);
		}
		else
		{
			delta_combined_with_substitutions = replaceVariableByConstant(delta_combined_with_skolem_functions_substituted, var_to_elim_index, 0);
		}
	}
	assert(delta_combined_with_substitutions != NULL);

	int size_of_delta_combined_with_substitutions = computeSize(delta_combined_with_substitutions);
	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nsize of result of replaceVariableByConstant is: " << size_of_delta_combined_with_substitutions << endl;
	#endif
	sizes_of_cofactors_affecting_variable.push_back(size_of_delta_combined_with_substitutions);

	if(use_uninterpreted_functions) // abstract the delta_part
	{
		set<string> support_delta_part;
		computeSupport(delta_combined_with_substitutions, support_delta_part);
		string name_of_function = "delta_part";
		t_Expression* abstracted_delta_part = createAbstraction(name_of_function, delta_combined_index, var_to_elim_index, support_delta_part, pub_em);
		assert(abstracted_delta_part != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_delta_part, delta_combined_with_substitutions));
		delta_combined_with_substitutions = abstracted_delta_part;
	}


	return delta_combined_with_substitutions;
}



t_Expression* Skolem::computeDeltaCombinedWithSkolemFunctionsSubstituted(int delta_combined_index, int subst_index)
{
	// sanity checks
	assert(delta_combined_index >= 1);
	assert(subst_index >= delta_combined_index);

	// obtain the existing delta-combined with substitutions
	t_Expression* delta_combined_with_substitutions;
	delta_combined_with_substitutions = searchOneDimensionalMatrix(DeltaCombinedMatrix, number_of_vars_to_elim, delta_combined_index);
	assert(delta_combined_with_substitutions != NULL);
	int index_upto_which_already_substituted = searchOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, delta_combined_index);
	
	assert(index_upto_which_already_substituted >= delta_combined_index);	

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nindex_upto_which_already_substituted = " << index_upto_which_already_substituted << endl;
	int number_of_variables_substituted = 0;
	#endif

	t_Expression* delta_combined_with_substitutions_new = delta_combined_with_substitutions;

	for(int current_subst_index = index_upto_which_already_substituted + 1; current_subst_index <= subst_index; current_subst_index++)
	{
		assert(current_subst_index > delta_combined_index);

		t_Expression* skolem_function;
		skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, current_subst_index);
		assert(skolem_function != NULL);

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nReplacing variable_" << current_subst_index << " by its skolem function\n";
		number_of_variables_substituted++;
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nsize of delta_combined_with_substitutions is: " << computeSize(delta_combined_with_substitutions) << endl;
		cout << "\nsize of skolem_function is: " << computeSize(skolem_function) << endl;
		#endif

		delta_combined_with_substitutions_new = replaceVariableByFormula(delta_combined_with_substitutions, current_subst_index, skolem_function);
		assert(delta_combined_with_substitutions_new != NULL);

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nsize of result of replaceVariableByFormula is: " << computeSize(delta_combined_with_substitutions_new) << endl;
		#endif

		delta_combined_with_substitutions = delta_combined_with_substitutions_new;
	}

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nnumber of variables to be substituted = " << number_of_variables_substituted << endl;
	#endif
	
	insertIntoOneDimensionalMatrix(DeltaCombinedMatrix, number_of_vars_to_elim, delta_combined_index, delta_combined_with_substitutions_new, true);	
	insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, delta_combined_index, subst_index, true);
	
	return delta_combined_with_substitutions_new;
}




t_Expression* Skolem::computeAlphaCombined(int var_to_elim_index)
{
	// Let us compute alpha_combined_{var_to_elim_index}
	// Suppose i = var_to_elim_index

	// i.e. we need to compute alpha_combined_{i}
	// alpha_combined_{i} = disjunction of alpha_combined_components
	set<t_Expression*> alpha_combined_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing components of alpha_combined\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\ncomputing components of alpha_combined\n";
	#endif

	#ifdef RECORD_KEEP
	int number_of_factors_containing_var_to_elim_index = FactorsWithVariable.size();
	#endif

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index
		// Each alpha_combined_component_i_j is the conjunction of
		// alpha_i_j and all_agree_with_i_j				
				
		t_Expression* alpha_i_j;
		alpha_i_j = computeAlpha(var_to_elim_index, factor_index); 
		assert(alpha_i_j != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, alpha_i_j, "alpha", ".v", var_to_elim_index, factor_index);
		#endif

		// all_agree_with_i_j = conjunction of all_agree_with_components
		t_Expression* all_agree_with_i_j;
		set<t_Expression*> all_agree_with_components; 

		#ifdef DEBUG_SKOLEM
		cout << "\nCreating all_agree_with_i_j" << endl;
		#endif
				
		for(set<int>::iterator agree_it = FactorsWithVariable.begin(); agree_it != FactorsWithVariable.end(); agree_it++)
		{
			int agree_index = *agree_it;

			#ifdef DEBUG_SKOLEM
			cout << "\nagree_index = " << agree_index << endl;
			#endif

			// Suppose k = agree_index

			if(factor_index == agree_index) // j == k; no need to consider
			{
				#ifdef DEBUG_SKOLEM
				cout << "\nfactor_index == agree_index; no need to consider" << endl;
				#endif

				continue;
			}

			#ifdef DEBUG_SKOLEM
			cout << "\nfactor_index != agree_index" << endl;
			#endif

			t_Expression* alpha_i_k;
			alpha_i_k = computeAlpha(var_to_elim_index, agree_index); 
			assert(alpha_i_k != NULL);
						
			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, alpha_i_k, "alpha", ".v", var_to_elim_index, agree_index);
			#endif

			t_Expression* gamma_i_k;
			gamma_i_k = computeGamma(var_to_elim_index, agree_index); 
			assert(gamma_i_k != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, gamma_i_k, "gamma", ".v", var_to_elim_index, agree_index);
			#endif

			t_Expression* all_agree_with_component = createOr(alpha_i_k, gamma_i_k, pub_em);
			assert(all_agree_with_component != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, all_agree_with_component, "all_agree_with_component", ".v", var_to_elim_index, agree_index);
			#endif

			all_agree_with_components.insert(all_agree_with_component);						
		} // for each agree factor ends here

		// computing all_agree_with_i_j
		// recall that all_agree_with_i_j = conjunction of all_agree_with_components
		if(all_agree_with_components.size() == 0)
		{
			all_agree_with_i_j = NULL;
		
			#ifdef DEBUG_SKOLEM
			cout << "\nall_agree_with_i_j = NULL" << endl;
			#endif
		}
		else
		{
			all_agree_with_i_j = createAnd(all_agree_with_components, pub_em);
			assert(all_agree_with_i_j != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, all_agree_with_i_j, "all_agree_with_i_j", ".v", var_to_elim_index, factor_index);
			#endif
		}

			
		// recall that alpha_combined_component_i_j is the conjunction of
		// alpha_i_j and all_agree_with_i_j
	
		t_Expression* alpha_combined_component;
		if(all_agree_with_i_j == NULL)
		{
			alpha_combined_component = alpha_i_j;
		}
		else
		{
			alpha_combined_component = createAnd(alpha_i_j, all_agree_with_i_j, pub_em);
			assert(alpha_combined_component != NULL);
		}

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, alpha_combined_component, "alpha_combined_component", ".v", var_to_elim_index, factor_index);		
		cout << "\nalpha_combined_component[" << var_to_elim_index << ", " << factor_index << "] obtained\n";			
		#endif
				
		alpha_combined_components.insert(alpha_combined_component);						
	}// for each factor ends here

	// recall that alpha_combined = disjunction of alpha_combined_components
	t_Expression* alpha_combined;				
	if(alpha_combined_components.size() == 0) // we should return false in this case (as per defn. of alpha)
	{
		alpha_combined = createFalse(pub_em); 
		assert(alpha_combined != NULL);
	}
	else
	{
		alpha_combined = createOr(alpha_combined_components, pub_em);
		assert(alpha_combined != NULL);
	}

	if(use_uninterpreted_functions) // abstract the alpha_combined
	{
		set<string> support_alpha_combined;
		computeSupport(alpha_combined, support_alpha_combined);
		string name_of_function = "alpha_combined";
		t_Expression* abstracted_alpha_combined = createAbstraction(name_of_function, var_to_elim_index, 0, support_alpha_combined, pub_em);
		assert(abstracted_alpha_combined != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_alpha_combined, alpha_combined));
		alpha_combined = abstracted_alpha_combined;
	}


	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, alpha_combined, "alpha_combined", ".v", var_to_elim_index, 0);				
	#endif

	#ifdef RECORD_KEEP
	NumberOfFactors = number_of_factors_containing_var_to_elim_index;
	#endif

	return alpha_combined;		
} // function ends here




t_Expression* Skolem::computeDeltaCombined(int var_to_elim_index)
{
	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	// Let us compute delta_combined_{var_to_elim_index}
	// Suppose i = var_to_elim_index
	// i.e. we need to compute delta_combined_{i}

	t_Expression* pairwise_conflicts;		

	// delta_combined_{i} = pairwise_conflicts_{i} \vee factorwise_conflicts_{i}, where

	// pairwise_conflicts_{i} = disjunction of pairwise_conflicts_components, where
	// each pairwise_conflicts_component_j_k = alpha_i_j \wedge beta_i_k
	// s.t. (j \neq k) \wedge (var_i \in support(factor_i_j)) \wedge (var_i \in support(factor_i_k))
	set<t_Expression*> pairwise_conflicts_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing components of pairwise_conflicts\n";
	#endif

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index
		
		t_Expression* alpha_i_j;
		alpha_i_j = computeAlpha(var_to_elim_index, factor_index); 
		assert(alpha_i_j != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, alpha_i_j, "alpha", ".v", var_to_elim_index, factor_index);
		#endif
			
		for(set<int>::iterator clash_it = FactorsWithVariable.begin(); clash_it != FactorsWithVariable.end(); clash_it++)
		{
			int clash_index = *clash_it;
			
			#ifdef DEBUG_SKOLEM
			cout << "\nclash_index = " << clash_index << endl;
			#endif

			// Suppose k = clash_index

			if(factor_index == clash_index) // j == k; no need to consider
			{
				#ifdef DEBUG_SKOLEM
				cout << "\nfactor_index == clash_index; no need to consider" << endl;
				#endif
				continue;
			}

			#ifdef DEBUG_SKOLEM
			cout << "\nfactor_index != clash_index" << endl;
			#endif

			
			t_Expression* beta_i_k;
			beta_i_k = computeBeta(var_to_elim_index, clash_index); 
			assert(beta_i_k != NULL);
				
			#ifdef DEBUG_SKOLEM		
			writeFormulaToFile(pub_em, beta_i_k, "beta", ".v", var_to_elim_index, clash_index);
			#endif

			t_Expression* pairwise_conflicts_component_j_k = createAnd(alpha_i_j, beta_i_k, pub_em);
			assert(pairwise_conflicts_component_j_k != NULL);

			#ifdef DEBUG_SKOLEM	
			writeFormulaToFile(pub_em, pairwise_conflicts_component_j_k, "pairwise_conflicts_component", ".v", factor_index, clash_index);
			#endif

			pairwise_conflicts_components.insert(pairwise_conflicts_component_j_k);						
				
		} // for each clashing factor ends here
	}// for each factor ends here

	// recall that pairwise_conflicts = disjunction of pairwise_conflicts_components				
	if(pairwise_conflicts_components.size() == 0) 
	{
		pairwise_conflicts = NULL;

		#ifdef DEBUG_SKOLEM	
		cout << "\npairwise_conflicts = NULL\n";
		#endif
	}
	else
	{
		pairwise_conflicts = createOr(pairwise_conflicts_components, pub_em);
		assert(pairwise_conflicts != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, pairwise_conflicts, "pairwise_conflicts", ".v", var_to_elim_index, 0);
		#endif
	}


	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	cout << "\ncomputing pair-wise conflicts finished in " << step_ms << " milliseconds\n";
	#endif

	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	// Let's now compute factorwise conflicts
	t_Expression* factorwise_conflicts = NULL;

	if(optimization_lemmas_on)
	{
		// factorwise_conflicts_{i} = disjunction of factorwise_conflicts_components, where
		// each factorwise_conflicts_component_i_j = delta_i_j s.t. (var_i \in support(factor_i_j))
		set<t_Expression*> factorwise_conflicts_components; 

		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing components of factorwise_conflicts\n";
		#endif

		for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
		{
			int factor_index = *factor_it;

			#ifdef DEBUG_SKOLEM
			cout << "\nfactor_index = " << factor_index << endl;
			#endif
			
			// Suppose j = factor_index
			t_Expression* delta_i_j;
			delta_i_j = computeDelta(var_to_elim_index, factor_index); 
			assert(delta_i_j != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, delta_i_j, "delta", ".v", var_to_elim_index, factor_index);
			#endif
				
			factorwise_conflicts_components.insert(delta_i_j);						
				
		}// for each factor ends here

		// recall that factorwise_conflicts = disjunction of factorwise_conflicts_components				
		if(factorwise_conflicts_components.size() == 0) 
		{
			factorwise_conflicts = NULL;

			#ifdef DEBUG_SKOLEM
			cout << "\nfactorwise_conflicts = NULL\n";
			#endif
		}
		else
		{
			factorwise_conflicts = createOr(factorwise_conflicts_components, pub_em);
			assert(factorwise_conflicts != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, factorwise_conflicts, "factorwise_conflicts", ".v", var_to_elim_index, 0);
			#endif
		}
	} // if(optimization_lemmas_on) ends here


	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	cout << "\ncomputing factor-wise conflicts finished in " << step_ms << " milliseconds\n";
	#endif
		
	// recall that delta_combined_{i} = pairwise_conflicts_{i} \vee factorwise_conflicts_{i}
	t_Expression* delta_combined;
	if(pairwise_conflicts == NULL && factorwise_conflicts == NULL)
	{
		delta_combined = createFalse(pub_em);
		assert(delta_combined != NULL);
	}
	else if(pairwise_conflicts == NULL)
	{
		delta_combined = factorwise_conflicts;
	}
	else if(factorwise_conflicts == NULL)
	{
		delta_combined = pairwise_conflicts;
	}
	else
	{
		delta_combined = createOr(factorwise_conflicts, pairwise_conflicts, pub_em);
		assert(delta_combined != NULL);
	}


	if(use_uninterpreted_functions) // abstract the delta_combined
	{
		set<string> support_delta_combined;
		computeSupport(delta_combined, support_delta_combined);
		string name_of_function = "delta_combined";
		t_Expression* abstracted_delta_combined = createAbstraction(name_of_function, var_to_elim_index, 0, support_delta_combined, pub_em);
		assert(abstracted_delta_combined != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_delta_combined, delta_combined));
		delta_combined = abstracted_delta_combined;
	}

	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, delta_combined, "delta_combined", ".v", var_to_elim_index, 0);	
	#endif

	return delta_combined;	
} // function ends here




void Skolem::updateFactors(int var_to_elim_index)
{
	assert(var_to_elim_index < number_of_vars_to_elim);

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// obtain the existing factor
		t_Expression* previous_factor;
		previous_factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(previous_factor != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, previous_factor, "factor", ".v", var_to_elim_index, factor_index);	
		#endif

		t_Expression* factor;

		if(local_skolem_function_for_updating_factors == 0) //use alpha as the local skolem function
		{
			t_Expression* alpha;
			alpha = computeAlpha(var_to_elim_index, factor_index); 
			assert(alpha != NULL);

			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, alpha);
			assert(factor != NULL);
		}
		else if(local_skolem_function_for_updating_factors == 1) //use cofactor-1 as the local skolem function
		{
			t_Expression* cofactor_1;
			cofactor_1 = computeCofactorOne(var_to_elim_index, factor_index); 
			assert(cofactor_1 != NULL);

			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, cofactor_1);
			assert(factor != NULL);	
			
		}
		else
		{
			cout << "local_skolem_function_for_updating_factors is " << local_skolem_function_for_updating_factors << endl;
        		assert(false && "invalid option");
		}

		if(use_uninterpreted_functions) // abstract the factor
		{
			set<string> support_factor;
			computeSupport(factor, support_factor);
			string name_of_function = "factor";
			t_Expression* abstracted_factor = createAbstraction(name_of_function, var_to_elim_index+1, factor_index, support_factor, pub_em);
			assert(abstracted_factor != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));
			factor = abstracted_factor;
		}


		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index+1, factor_index);	
		#endif

		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, factor, true);

		int size_of_new_factor = computeSize(factor);

		if(order_of_elimination_of_variables == 2)
		{
			factor_to_costs_map[factor_index] = size_of_new_factor;
		}

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nfactor_" << factor_index << " updated to formula of size " << size_of_new_factor << endl;
		#endif		
	}	
}


t_Expression* Skolem::computeAlpha(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* alpha;
	alpha = searchOneDimensionalMatrix(AlphaMatrix, number_of_factors, factor_index);
	if(alpha != NULL)
	{
		return alpha;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeAlpha(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// alpha_i_j = (factor_i_j with var_i = true) \wedge (\neg factor_i_j with var_i = false)

		// compute cofactor_1 = factor_i_j with var_i = true
		t_Expression* cofactor_1 = computeCofactorOne(var_to_elim_index, factor_index); 
		assert(cofactor_1 != NULL);

		// compute neg_cofactor_0 = not(factor_i_j with var_i = false)
		t_Expression* neg_cofactor_0 = computeNegatedCofactorZero(var_to_elim_index, factor_index); 
		assert(neg_cofactor_0 != NULL);

		alpha = createAnd(cofactor_1, neg_cofactor_0, pub_em); 
		assert(alpha != NULL);

		
		if(use_uninterpreted_functions) // abstract the alpha
		{
			set<string> support_alpha;
			computeSupport(alpha, support_alpha);
			string name_of_function = "alpha";
			t_Expression* abstracted_alpha = createAbstraction(name_of_function, var_to_elim_index, factor_index, support_alpha, pub_em);
			assert(abstracted_alpha != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_alpha, alpha));
			alpha = abstracted_alpha;
		}

		// Enter into matrix
		insertIntoOneDimensionalMatrix(AlphaMatrix, number_of_factors, factor_index, alpha, false);

		//cout << endl << alpha << " inserted in AlphaMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return alpha;	
	}	
}



t_Expression* Skolem::computeBeta(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* beta;
	beta = searchOneDimensionalMatrix(BetaMatrix, number_of_factors, factor_index);
	if(beta != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeBeta. BetaMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << beta << "\n";
		return beta;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeBeta(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// beta_i_j = (factor_i_j with var_i = false) \wedge (\neg factor_i_j with var_i = true)

		// compute cofactor_0 = factor_i_j with var_i = false
		t_Expression* cofactor_0 = computeCofactorZero(var_to_elim_index, factor_index); 
		assert(cofactor_0 != NULL);

		// compute neg_cofactor_1 = not(factor_i_j with var_i = true)
		t_Expression* neg_cofactor_1 = computeNegatedCofactorOne(var_to_elim_index, factor_index); 
		assert(neg_cofactor_1 != NULL);

		beta = createAnd(cofactor_0, neg_cofactor_1, pub_em); 
		assert(beta != NULL);
		
		
		if(use_uninterpreted_functions) // abstract the beta
		{
			set<string> support_beta;
			computeSupport(beta, support_beta);
			string name_of_function = "beta";
			t_Expression* abstracted_beta = createAbstraction(name_of_function, var_to_elim_index, factor_index, support_beta, pub_em);
			assert(abstracted_beta != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_beta, beta));
			beta = abstracted_beta;
		}


		// Enter into matrix
		insertIntoOneDimensionalMatrix(BetaMatrix, number_of_factors, factor_index, beta, false);

		//cout << endl << beta << " inserted in BetaMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return beta;	
	}	
}



t_Expression* Skolem::computeGamma(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* gamma;
	gamma = searchOneDimensionalMatrix(GammaMatrix, number_of_factors, factor_index);
	if(gamma != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeGamma. GammaMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << gamma << "\n";
		return gamma;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeGamma(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// gamma_i_j = (factor_i_j with var_i = false) \wedge (factor_i_j with var_i = true)

		// compute cofactor_0 = factor_i_j with var_i = false
		t_Expression* cofactor_0 = computeCofactorZero(var_to_elim_index, factor_index); 
		assert(cofactor_0 != NULL);

		// compute cofactor_1 = factor_i_j with var_i = true
		t_Expression* cofactor_1 = computeCofactorOne(var_to_elim_index, factor_index); 
		assert(cofactor_1 != NULL);

		gamma = createAnd(cofactor_0, cofactor_1, pub_em); 
		assert(gamma != NULL);
		
		
		if(use_uninterpreted_functions) // abstract the gamma
		{
			set<string> support_gamma;
			computeSupport(gamma, support_gamma);
			string name_of_function = "gamma";
			t_Expression* abstracted_gamma = createAbstraction(name_of_function, var_to_elim_index, factor_index, support_gamma, pub_em);
			assert(abstracted_gamma != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_gamma, gamma));
			gamma = abstracted_gamma;
		}


		// Enter into matrix
		insertIntoOneDimensionalMatrix(GammaMatrix, number_of_factors, factor_index, gamma, false);

		//cout << endl << gamma << " inserted in GammaMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return gamma;	
	}	
}



t_Expression* Skolem::computeDelta(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* delta;
	delta = searchOneDimensionalMatrix(DeltaMatrix, number_of_factors, factor_index);
	if(delta != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeDelta. DeltaMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << delta << "\n";
		return delta;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeDelta(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// delta_i_j = (\neg factor_i_j with var_i = false) \wedge (\neg factor_i_j with var_i = true)

		// compute negated_cofactor_0 = not(factor_i_j with var_i = false)
		t_Expression* negated_cofactor_0 = computeNegatedCofactorZero(var_to_elim_index, factor_index); 
		assert(negated_cofactor_0 != NULL);

		// compute negated_cofactor_1 = not(factor_i_j with var_i = true)
		t_Expression* negated_cofactor_1 = computeNegatedCofactorOne(var_to_elim_index, factor_index); 
		assert(negated_cofactor_1 != NULL);

		delta = createAnd(negated_cofactor_0, negated_cofactor_1, pub_em); 
		assert(delta != NULL);
		
		
		if(use_uninterpreted_functions) // abstract the delta
		{
			set<string> support_delta;
			computeSupport(delta, support_delta);
			string name_of_function = "delta";
			t_Expression* abstracted_delta = createAbstraction(name_of_function, var_to_elim_index, factor_index, support_delta, pub_em);
			assert(abstracted_delta != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_delta, delta));
			delta = abstracted_delta;
		}


		// Enter into matrix
		insertIntoOneDimensionalMatrix(DeltaMatrix, number_of_factors, factor_index, delta, false);

		//cout << endl << delta << " inserted in DeltaMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return delta;	
	}	
}



t_Expression* Skolem::computeCofactorOne(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* cofactor_1;
	cofactor_1 = searchOneDimensionalMatrix(CofactorOneMatrix, number_of_factors, factor_index);
	if(cofactor_1 != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeCofactorOne. CofactorOneMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << cofactor_1 << "\n";
		return cofactor_1;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeCofactorOne(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// compute cofactor_1 = factor_i_j with var_i = true
		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);

		if(reuse_same_cache_for_computations)
		{
			cofactor_1 = replaceVariableByConstant(factor, var_to_elim_index, 1, pub_cofactor_one_cache);	
		}
		else
		{
			cofactor_1 = replaceVariableByConstant(factor, var_to_elim_index, 1);
		}
		assert(cofactor_1 != NULL);

		// Enter into matrix
		insertIntoOneDimensionalMatrix(CofactorOneMatrix, number_of_factors, factor_index, cofactor_1, false);
		
		//cout << endl << cofactor_1 << " inserted in CofactorOneMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";

		return cofactor_1;	
	}	
}


t_Expression* Skolem::computeNegatedCofactorOne(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* neg_cofactor_1;
	neg_cofactor_1 = searchOneDimensionalMatrix(NegatedCofactorOneMatrix, number_of_factors, factor_index);
	if(neg_cofactor_1 != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeNegatedCofactorOne. NegatedCofactorOneMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << neg_cofactor_1 << "\n";
		return neg_cofactor_1;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeNegatedCofactorOne(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// compute cofactor_1 
		t_Expression* cofactor_1 = computeCofactorOne(var_to_elim_index, factor_index);
		assert(cofactor_1 != NULL);

		neg_cofactor_1 = createNot(cofactor_1, pub_em);
		assert(neg_cofactor_1 != NULL);

		// Enter into matrix
		insertIntoOneDimensionalMatrix(NegatedCofactorOneMatrix, number_of_factors, factor_index, neg_cofactor_1, false);

		//cout << endl << neg_cofactor_1 << " inserted in NegatedCofactorOneMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return neg_cofactor_1;	
	}	
}


t_Expression* Skolem::computeCofactorZero(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* cofactor_0;
	cofactor_0 = searchOneDimensionalMatrix(CofactorZeroMatrix, number_of_factors, factor_index);
	if(cofactor_0 != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeCofactorZero. CofactorZeroMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << cofactor_0 << "\n";
		return cofactor_0;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeCofactorZero(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// compute cofactor_0 = factor_i_j with var_i = false
		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);

		if(reuse_same_cache_for_computations)
		{
			cofactor_0 = replaceVariableByConstant(factor, var_to_elim_index, 0, pub_cofactor_zero_cache);	
		}
		else
		{
			cofactor_0 = replaceVariableByConstant(factor, var_to_elim_index, 0);
		}
		assert(cofactor_0 != NULL);

		// Enter into matrix
		insertIntoOneDimensionalMatrix(CofactorZeroMatrix, number_of_factors, factor_index, cofactor_0, false);

		//cout << endl << cofactor_0 << " inserted in CofactorZeroMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return cofactor_0;	
	}	
}




t_Expression* Skolem::computeNegatedCofactorZero(int var_to_elim_index, int factor_index)
{
	// check if entry already exists in the matrix
	t_Expression* neg_cofactor_0;
	neg_cofactor_0 = searchOneDimensionalMatrix(NegatedCofactorZeroMatrix, number_of_factors, factor_index);
	if(neg_cofactor_0 != NULL)
	{
		// hash table hit
		//cout << "\nhash table hit in Skolem::computeNegatedCofactorZero. NegatedCofactorZeroMatrix[" << var_to_elim_index << ", " << factor_index << "] = " << neg_cofactor_0 << "\n";
		return neg_cofactor_0;
	}
	else
	{
		// hash table miss
		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nhash table miss in Skolem::computeNegatedCofactorZero(" << var_to_elim_index <<", "<< factor_index <<")\n";
		#endif
		// compute cofactor_0 
		t_Expression* cofactor_0 = computeCofactorZero(var_to_elim_index, factor_index);
		assert(cofactor_0 != NULL);

		neg_cofactor_0 = createNot(cofactor_0, pub_em);
		assert(neg_cofactor_0 != NULL);

		// Enter into matrix
		insertIntoOneDimensionalMatrix(NegatedCofactorZeroMatrix, number_of_factors, factor_index, neg_cofactor_0, false);

		//cout << endl << neg_cofactor_0 << " inserted in NegatedCofactorZeroMatrix[" << var_to_elim_index << ", " << factor_index << "]"<< "\n";
		
		return neg_cofactor_0;	
	}	
}



bool Skolem::formulaFreeOfVariable(t_Expression* formula, int var_index)
{
	#ifdef DEBUG_SKOLEM
	cout << "\nchecking if formula is free of variable_" << var_index << endl;
	#endif

	// sanity checks
	assert(formula != NULL);
	assert(var_index >= 1);

	// obtain the adress of the variable object
	string var_string = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_index);

	set<string> support;
	computeSupport(formula, support);
	if(support.find(var_string) == support.end()) // formula is free of var_string
	{
		return true;
	}
	else
	{
		return false;
	}
}



t_Expression* Skolem::replaceVariableByConstant(t_Expression* OriginalFormula, int var_index_to_replace, int constant_to_substitute)
{

	#ifdef RECORD_KEEP
	number_of_compose_operations_for_variable++;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	// sanity checks
	assert(OriginalFormula != NULL);
	assert(var_index_to_replace >= 1);
	assert(constant_to_substitute == 0 || constant_to_substitute == 1);

	t_Expression* ReplacedFormula;
	t_Expression* FormulaToSubstitute;

	if(constant_to_substitute == 0) // replace by zero
	{
		FormulaToSubstitute = createFalse(pub_em);
	}
	else // replace by one
	{
		FormulaToSubstitute = createTrue(pub_em);
	}
	assert(FormulaToSubstitute != NULL);

	string var_to_replace = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_index_to_replace);
	t_HashTable<unsigned long, t_Expression*> cache;

	if(use_second_level_cache_in_compose)
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, true, 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);
	}
	else
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, false, 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);
	}

	assert(ReplacedFormula != NULL);
	
	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;

	ComposeTime += step_ms;
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nreplaceVariableByConstant finished in " << step_ms << " milliseconds\n";
	#endif	

	return ReplacedFormula;	
}



t_Expression* Skolem::replaceVariableByConstant(t_Expression* OriginalFormula, int var_index_to_replace, int constant_to_substitute, t_HashTable<unsigned long, t_Expression*> &cache)
{
	#ifdef RECORD_KEEP
	number_of_compose_operations_for_variable++;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 

	unsigned long long int old_first_level_cache_misses = first_level_cache_misses;	
	unsigned long long int old_recreation_cases = recreation_cases;
	#endif

	// sanity checks
	assert(OriginalFormula != NULL);
	assert(var_index_to_replace >= 1);
	assert(constant_to_substitute == 0 || constant_to_substitute == 1);

	t_Expression* ReplacedFormula;
	t_Expression* FormulaToSubstitute;

	if(constant_to_substitute == 0) // replace by zero
	{
		FormulaToSubstitute = createFalse(pub_em);
	}
	else // replace by one
	{
		FormulaToSubstitute = createTrue(pub_em);
	}
	assert(FormulaToSubstitute != NULL);

	string var_to_replace = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_index_to_replace);

	if(use_second_level_cache_in_compose)
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, true, 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);
	}
	else
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, false, 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);
	}
	
	assert(ReplacedFormula != NULL);
	
	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;

	ComposeTime += step_ms;

	unsigned long long int my_first_level_cache_misses = first_level_cache_misses - old_first_level_cache_misses;	
	unsigned long long int my_recreation_cases = recreation_cases - old_recreation_cases;

	// Note that finding size is costly, i.e. why below line is commented
	//cout << "\ncompose-constant: dag-size = " << computeSize(OriginalFormula) << ", time = " << step_ms << " m.s., misses = " << my_first_level_cache_misses << " create-expr = " << my_recreation_cases << " @ ( " << (float)my_recreation_cases/(float)my_first_level_cache_misses << ")\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nreplaceVariableByConstant finished in " << step_ms << " milliseconds\n";		
	#endif

	return ReplacedFormula;	
}


t_Expression* Skolem::replaceVariableByFormula(t_Expression* OriginalFormula, int var_index_to_replace, t_Expression* FormulaToSubstitute)
{

	#ifdef RECORD_KEEP
	number_of_compose_operations_for_variable++;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	

	unsigned long long int old_first_level_cache_misses = first_level_cache_misses;	
	unsigned long long int old_recreation_cases = recreation_cases;
	#endif

	// sanity checks
	assert(OriginalFormula != NULL);
	assert(var_index_to_replace >= 1);
	assert(FormulaToSubstitute != NULL);

	t_Expression* ReplacedFormula;

	string var_to_replace = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_index_to_replace);
	t_HashTable<unsigned long, t_Expression*> cache;

	if(use_second_level_cache_in_compose)
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, true, 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);
	}
	else
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, false, 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);
	}
	
	assert(ReplacedFormula != NULL);
	
	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;

	ComposeTime += step_ms;

	unsigned long long int my_first_level_cache_misses = first_level_cache_misses - old_first_level_cache_misses;	
	unsigned long long int my_recreation_cases = recreation_cases - old_recreation_cases;

	// Note that finding size is costly, i.e. why below line is commented
	//cout << "\ncompose-constant: dag-size = " << computeSize(OriginalFormula) << ", time = " << step_ms << " m.s., misses = " << my_first_level_cache_misses << " create-expr = " << my_recreation_cases << " @ ( " << (float)my_recreation_cases/(float)my_first_level_cache_misses << ")\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nreplaceVariableByFormula finished in " << step_ms << " milliseconds\n";		
	#endif

	return ReplacedFormula;	
}



t_Expression* Skolem::replaceVariableByFormula(t_Expression* OriginalFormula, int var_index_to_replace, t_Expression* FormulaToSubstitute, t_HashTable<unsigned long, t_Expression*> &cache)
{
	#ifdef RECORD_KEEP
	number_of_compose_operations_for_variable++;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	

	unsigned long long int old_first_level_cache_misses = first_level_cache_misses;	
	unsigned long long int old_recreation_cases = recreation_cases;
	#endif

	// sanity checks
	assert(OriginalFormula != NULL);
	assert(var_index_to_replace >= 1);
	assert(FormulaToSubstitute != NULL);

	t_Expression* ReplacedFormula;

	string var_to_replace = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_index_to_replace);
	
	if(use_second_level_cache_in_compose)
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, true, 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);
	}
	else
	{
		ReplacedFormula = pub_em->ReplaceLeafByExpression(OriginalFormula, var_to_replace, FormulaToSubstitute, cache, false, 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);
	}
	
	assert(ReplacedFormula != NULL);
	
	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;

	ComposeTime += step_ms;

	unsigned long long int my_first_level_cache_misses = first_level_cache_misses - old_first_level_cache_misses;	
	unsigned long long int my_recreation_cases = recreation_cases - old_recreation_cases;

	// Note that finding size is costly, i.e. why below line is commented
	//cout << "\ncompose-constant: dag-size = " << computeSize(OriginalFormula) << ", time = " << step_ms << " m.s., misses = " << my_first_level_cache_misses << " create-expr = " << my_recreation_cases << " @ ( " << (float)my_recreation_cases/(float)my_first_level_cache_misses << ")\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nreplaceVariableByFormula finished in " << step_ms << " milliseconds\n";		
	#endif

	return ReplacedFormula;	
}



void Skolem::initializeSkylineVariablesTrivially(int var_to_elim_index, set<int> &SkylineVariables)
{
	SkylineVariables.clear();	

	assert(var_to_elim_index >= 1);

	for(int prev_index = var_to_elim_index-1; prev_index >= 1; prev_index--)
	{
		SkylineVariables.insert(prev_index);
	}	
}




void Skolem::obtainSkylineOfVariableUsingLemmas(int var_to_elim_index, set<int> &SkylineVariables)
{
	SkylineVariables.clear();	

	assert(var_to_elim_index >= 1);

	if(var_to_elim_index == 1) // first variable to be eliminated; skyline empty
	{
		return;
	}
	
	set< pair<int, int> > Edges; // each entry is (factor_index, index of variable in the support of factor s.t. index <= var_to_elim_index)
	set<int> FactorIndices; // indices of the factors in graph
	set<int> VariableIndices; // indices of the variables in graph
	
	map<int, int> FactorToMinVariableMap; // factor_index ---> index of variable with the minimum index in the support of factor
	
	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// Suppose j = factor_index
		// first let us obtain factor_1_j
			
		t_Expression* factor_1_j = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor_1_j != NULL);

		set<string> support;
		computeSupport(factor_1_j, support);

		int min_variable_index = INT_MAX;

		for(set<string>::iterator support_it = support.begin(); support_it != support.end(); support_it++)
		{
			string variable = *support_it;
			int variable_index = searchVarNameToVarIndexMap(var_name_to_var_index_map, variable);
			
			if(variable_index >= 1 && variable_index <= var_to_elim_index) // this is a variable to be considered
			// as 1) it is a variable to be eliminated and 2) its index <= index of present variable to be eliminated
			{
				Edges.insert(make_pair(factor_index, variable_index));
				FactorIndices.insert(factor_index);
				VariableIndices.insert(variable_index);

				if(variable_index < min_variable_index)
				{
					min_variable_index = variable_index;
				}
			}
		}

		if(min_variable_index != INT_MAX)
		{
			FactorToMinVariableMap.insert(make_pair(factor_index, min_variable_index));
		}
		
	}//for each factor ends here

	// Let's create the factor_index <---> factor_node_index and 
	// variable_index ---> variable_node_index maps

	int number_of_factors_in_graph = FactorIndices.size();
	int number_of_variables_in_graph = VariableIndices.size();
	int number_of_nodes_in_graph = number_of_factors_in_graph + number_of_variables_in_graph;

	if(number_of_nodes_in_graph == 0) // no factor with the variable to be eliminated
	{
		// SkylineVariables is empty
		return;
	}

	map<int, int> FactorIndexToFactorNodeIndexMap;
	map<int, int> FactorNodeIndexToFactorIndexMap;
	map<int, int> VariableIndexToVariableNodeIndexMap;
	
	int node_index = 0;

	for(set<int>::iterator factor_it = FactorIndices.begin(); factor_it != FactorIndices.end(); factor_it++)
	{
		int factor_index = *factor_it;
		FactorIndexToFactorNodeIndexMap.insert(make_pair(factor_index, node_index));
		FactorNodeIndexToFactorIndexMap.insert(make_pair(node_index, factor_index));

		node_index++;
	} 

	for(set<int>::iterator variable_it = VariableIndices.begin(); variable_it != VariableIndices.end(); variable_it++)
	{
		int variable_index = *variable_it;
		VariableIndexToVariableNodeIndexMap.insert(make_pair(variable_index, node_index));
		
		node_index++;
	} 
	
	// Let's create the graph now

	Graph G(number_of_nodes_in_graph);	

	for(set< pair<int, int> >::iterator edge_it = Edges.begin(); edge_it != Edges.end(); edge_it++)
	{
		int factor_index = edge_it->first;
		int variable_index = edge_it->second;

		int factor_node_index = FactorIndexToFactorNodeIndexMap[factor_index];
		int variable_node_index = VariableIndexToVariableNodeIndexMap[variable_index];

		G.addEdge(factor_node_index, variable_node_index);
		G.addEdge(variable_node_index, factor_node_index);		
	}

	
	// Let's do the DFS now

	int var_to_elim_node_index = VariableIndexToVariableNodeIndexMap[var_to_elim_index];

	list<int> relatives;
	G.DFS(var_to_elim_node_index, relatives);  

	for(list<int>::iterator relatives_it = relatives.begin(); relatives_it != relatives.end(); relatives_it++)
	{
		int relative = *relatives_it;

		if(relative < number_of_factors_in_graph) // relative is a factor
		{
			int factor_index = FactorNodeIndexToFactorIndexMap[relative];
			int min_variable_index = FactorToMinVariableMap[factor_index];

			if(min_variable_index != var_to_elim_index)
			{
				assert(min_variable_index < var_to_elim_index);
				SkylineVariables.insert(min_variable_index);	
			}
		}
	}
	
}// function ends here



void Skolem::computeSupport(t_Expression* formula, set<string> &support)
{
	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	assert(formula != NULL);

	static t_HashTable<unsigned long int, set<string> > cache;
	#ifdef DETAILED_RECORD_KEEP
	static unsigned long long int cache_hits = 0;
	static unsigned long long int cache_misses = 0;
	#endif
	unsigned long int formulaID = formula->getID();
	t_HashTable<unsigned long int, set<string> >::iterator cache_it = cache.find(formulaID);
	if (cache_it != cache.end())
	{
		#ifdef DETAILED_RECORD_KEEP
		cache_hits++;
		#endif
		support = cache_it.getValue();		
	}
	else
	{

		#ifdef DETAILED_RECORD_KEEP
		cache_misses++;
		#endif

		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing support" << endl;
		#endif	
	
		vector<t_Expression*> Leaves = pub_em->getVectorOfLeafExpressions2(formula);

		for(vector<t_Expression*>::iterator leaf_it = Leaves.begin(); leaf_it != Leaves.end(); leaf_it++)
		{
			t_Expression* Leaf = *leaf_it;
			assert(Leaf != NULL);

			if(pub_em->getTypeOfValueStoredInExpressionLabel(Leaf) == SYMBOL)
			{
				string Leaf_name = pub_em->getLabelOfExpression(Leaf);
				support.insert(Leaf_name);			
			}
		}

		cache[formulaID] = support;
	}

	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;

	//cout << "\nTime to find support of dag with size " << computeSize(formula) << " is: " << step_ms << "milli seconds\n";
	total_time_in_compute_support = total_time_in_compute_support + step_ms;
	#endif

}// function ends here



void Skolem::clearVariableSpecificDataStructures()
{
	#ifdef DETAILED_RECORD_KEEP
	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		PreviousFactorsWithVariable.insert(*factor_it);			
	}
	#endif

	FactorsWithVariable.clear();

	CofactorOneMatrix.clear();
	CofactorZeroMatrix.clear();
	NegatedCofactorOneMatrix.clear();
	NegatedCofactorZeroMatrix.clear();

	AlphaMatrix.clear();
	BetaMatrix.clear();
	GammaMatrix.clear();
	DeltaMatrix.clear();

	pub_cofactor_zero_cache.clear();
	pub_cofactor_one_cache.clear();	

}



void Skolem::obtainSkylineUsingLemmas()
{
	map<int, set<string> > Supports;
	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// Suppose j = factor_index
		// first let us obtain factor_j
			
		t_Expression* factor_j = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor_j != NULL);

		set<string> support;
		computeSupport(factor_j, support);
		
		Supports.insert(make_pair(factor_index, support));

		#ifdef DEBUG_SKOLEM 
		cout << "\nfactor_index = " << factor_index << endl;
		showSet(support, "support");
		#endif
	}	

	
	map<int, set<int> > NeighboursOfFactor;	
	map<int, set<int> > ReachableFactorsFromVariable;
	map<int, int> MinVariableOfFactor;

	for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
	{
		#ifdef DEBUG_SKOLEM 
		cout << "\nvar_to_elim_index = " << var_to_elim_index << endl;
		#endif

		set<int> Neighbours;
		set<int> ReachableFactors;

		for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
		{
			bool factor_free_of_variable;
			set<string> support_factor = Supports[factor_index];
			
			string var_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
			if(support_factor.find(var_name) != support_factor.end())
			{
				factor_free_of_variable = false;
			}
			else
			{
				factor_free_of_variable = true;
			}

			if(factor_free_of_variable)
			{
				continue;
			}

			Neighbours.insert(factor_index);

			if(MinVariableOfFactor.find(factor_index) == MinVariableOfFactor.end())
			{
				MinVariableOfFactor.insert(make_pair(factor_index, var_to_elim_index));
			}

			ReachableFactors.insert(factor_index);
			
			map<int, set<int> >::iterator NeighboursOfFactor_it = NeighboursOfFactor.find(factor_index);
			if(NeighboursOfFactor_it != NeighboursOfFactor.end())
			{
				set<int> NeighboursOfThisFactor = NeighboursOfFactor_it->second;
				for(set<int>::iterator neighbour_it = NeighboursOfThisFactor.begin(); neighbour_it != NeighboursOfThisFactor.end(); neighbour_it++)
				{
					int NeighbourOfThisFactor = *neighbour_it;
					map<int, set<int> >::iterator Reachable_it = ReachableFactorsFromVariable.find(NeighbourOfThisFactor);
					if(Reachable_it != ReachableFactorsFromVariable.end())
					{
						set<int> ReachableFactorsFromNeighbour = Reachable_it->second;
						copy(ReachableFactorsFromNeighbour.begin(), ReachableFactorsFromNeighbour.end(), inserter(ReachableFactors, ReachableFactors.end()));
					}
				}
			}			
		}// for each factor ends here

		#ifdef DEBUG_SKOLEM 
		showSet(Neighbours, "Neighbours");
		showSet(ReachableFactors, "ReachableFactors");
		#endif

		ReachableFactorsFromVariable.insert(make_pair(var_to_elim_index, ReachableFactors));

		for(set<int>::iterator Neighbours_it = Neighbours.begin(); Neighbours_it != Neighbours.end(); Neighbours_it++)
		{
			int factor = *Neighbours_it;
			
			map<int, set<int> >::iterator NeighboursOfFactor_it = NeighboursOfFactor.find(factor);
			if(NeighboursOfFactor_it == NeighboursOfFactor.end())
			{
				set<int> Neighbours_of_factor;
				Neighbours_of_factor.insert(var_to_elim_index);
				NeighboursOfFactor.insert(make_pair(factor, Neighbours_of_factor));
			}
			else
			{
				set<int> Neighbours_of_factor = NeighboursOfFactor_it->second;
				Neighbours_of_factor.insert(var_to_elim_index);
				NeighboursOfFactor.insert(make_pair(factor, Neighbours_of_factor));
			}
		}		
		
	}// for each variable ends here	

	// Let's construct the skylines
	for(map<int, set<int> >::iterator reachable_it = ReachableFactorsFromVariable.begin(); reachable_it != ReachableFactorsFromVariable.end(); reachable_it++)
	{
		int variable_index = reachable_it->first;
		set<int> reachable_factors = reachable_it->second;
		set<int> skyline_for_variable;
	
		for(set<int>::iterator reachable_factors_it = reachable_factors.begin(); reachable_factors_it != reachable_factors.end(); reachable_factors_it++)
		{
			int factor = *reachable_factors_it;
			map<int, int>::iterator min_variable_it = MinVariableOfFactor.find(factor);
			assert(min_variable_it != MinVariableOfFactor.end());
			skyline_for_variable.insert(min_variable_it->second);
		}

		#ifdef DEBUG_SKOLEM 
		cout << "\nvariable_index = " << variable_index << endl;
		showSet(reachable_factors, "reachable_factors");
		showSet(skyline_for_variable, "skyline_for_variable");
		#endif

		Skylines.insert(make_pair(variable_index, skyline_for_variable));		
	}
}//end of function

void Skolem::initializeMonolithicSkolemFunctionGenerator(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	// 1) Remove variables which are not occuring in the factors
	// from the set of variables to be eliminated, and
	// 2) Insert the conjunction of factors into FactorMatrix
	// 3) Decide the order of variable elimination

	set<string> support;
	set<string> VariablesToEliminate_Set(VariablesToEliminate.begin(), VariablesToEliminate.end());
	set<string> Final_VariablesToEliminate_Set;
	map<string, int> VarsToElim_To_Factors_Map;
	int factor_index = 1;
	
	#ifdef DETAILED_RECORD_KEEP
	string support_file_name = benchmark_name_without_extension;
	support_file_name += "_support.txt";
	FILE* support_fp = fopen(support_file_name.c_str(), "w");
	assert(support_fp != NULL);
	printSet(VariablesToEliminate_Set, "Original_VariablesToEliminate_Set", support_fp);
	#endif	

	for(set<t_Expression*>::iterator factor_it = Factors.begin(); factor_it != Factors.end(); factor_it++)
	{
		t_Expression* factor = *factor_it;		

		set<string> support_factor;
		computeSupport(factor, support_factor);
		copy(support_factor.begin(), support_factor.end(), inserter(support, support.end()));

		set<string> varstoelim_in_support_factor;
		set_intersection(support_factor.begin(), support_factor.end(), VariablesToEliminate_Set.begin(), VariablesToEliminate_Set.end(), inserter(varstoelim_in_support_factor, varstoelim_in_support_factor.begin()));
		copy(varstoelim_in_support_factor.begin(), varstoelim_in_support_factor.end(), inserter(Final_VariablesToEliminate_Set, Final_VariablesToEliminate_Set.end()));

		for(set<string>::iterator varstoelim_it = varstoelim_in_support_factor.begin(); varstoelim_it != varstoelim_in_support_factor.end(); varstoelim_it++)
		{
			string variable_to_eliminate = *varstoelim_it;
			map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.find(variable_to_eliminate);
			if(VarsToElim_To_Factors_Map_it == VarsToElim_To_Factors_Map.end()) 
			// variable_to_eliminate occuring for the first time
			{
				VarsToElim_To_Factors_Map.insert(make_pair(variable_to_eliminate, 1));
			}
			else
			{
				(VarsToElim_To_Factors_Map_it->second)++;
			}
		} 
		
		#ifdef DETAILED_RECORD_KEEP
		fprintf(support_fp,"\nfactor_%d\n",factor_index);
		cout << endl;
		printSet(support_factor, "support_factor", support_fp);
		cout << endl;
		printSet(varstoelim_in_support_factor, "varstoelim_in_support_factor", support_fp);
		cout << endl;		
		#endif	

		factor_index++;		
	}

	#ifdef DETAILED_RECORD_KEEP
	printSet(support, "support", support_fp);
	printSet(Final_VariablesToEliminate_Set, "Final_VariablesToEliminate_Set", support_fp);
	fclose(support_fp);
	#endif
	
	if(order_of_elimination_of_variables == 2)
	{
		// we should read the order from the given file
		list<string> OrderOfVariableEliminationFromFile;
		obtainOrderOfVariableEliminationFromFile(OrderOfVariableEliminationFromFile);

		#ifdef DEBUG_SKOLEM 
		cout << endl << "OrderOfVariableEliminationFromFile" << endl;
		showList(OrderOfVariableEliminationFromFile);
		#endif

		VariablesToEliminate.clear();

		for(list<string>::iterator var_order_it = OrderOfVariableEliminationFromFile.begin(); var_order_it != OrderOfVariableEliminationFromFile.end(); var_order_it++)
		{
			string var_from_order_file = *var_order_it;
			if(Final_VariablesToEliminate_Set.find(var_from_order_file) != Final_VariablesToEliminate_Set.end()) // this is a var to elim
			{
				VariablesToEliminate.push_back(var_from_order_file);
			}
		}

		cout << endl << "VariablesToEliminate" << endl;
		showList(VariablesToEliminate);
		
	}	
	else if(order_of_elimination_of_variables == 1)
	{
		map<int, set<string> > Factors_To_VarsToElim_Map;
		for(map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.begin(); VarsToElim_To_Factors_Map_it != VarsToElim_To_Factors_Map.end(); VarsToElim_To_Factors_Map_it++)
		{
			string variable_to_eliminate = VarsToElim_To_Factors_Map_it->first;
			int number_of_factors = VarsToElim_To_Factors_Map_it->second;
			cout << endl << variable_to_eliminate << "\t" << number_of_factors << endl;

			map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.find(number_of_factors);
			if(Factors_To_VarsToElim_Map_it == Factors_To_VarsToElim_Map.end())
			{
				set<string> variables_with_factor_count;
				variables_with_factor_count.insert(variable_to_eliminate);
				Factors_To_VarsToElim_Map.insert(make_pair(number_of_factors, variables_with_factor_count));
			}
			else
			{
				(Factors_To_VarsToElim_Map_it->second).insert(variable_to_eliminate);
			}
		}

		VariablesToEliminate.clear();
		for(map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.begin(); Factors_To_VarsToElim_Map_it != Factors_To_VarsToElim_Map.end(); Factors_To_VarsToElim_Map_it++)
		{
			cout << endl << "factor_count = " << Factors_To_VarsToElim_Map_it->first <<"\tvariables = ";
			set<string> variables_with_factor_count = Factors_To_VarsToElim_Map_it->second;
			for(set<string>::iterator variable_it = variables_with_factor_count.begin(); variable_it != variables_with_factor_count.end(); variable_it++)
			{
				cout << *variable_it << ", ";
				VariablesToEliminate.push_back(*variable_it);
			}
		}			
	}
	else
	{
		VariablesToEliminate.clear();
		copy(Final_VariablesToEliminate_Set.begin(), Final_VariablesToEliminate_Set.end(), inserter(VariablesToEliminate, VariablesToEliminate.end()));
	}

	number_of_vars_to_elim = VariablesToEliminate.size();

	#ifdef DETAILED_RECORD_KEEP
	string order_file_name = benchmark_name_without_extension;
	order_file_name += "_monolithic_order.txt";
	FILE* order_fp = fopen(order_file_name.c_str(), "w+");
	assert(order_fp != NULL);
	printList(VariablesToEliminate, order_fp);
	fclose(order_fp);
	#endif
	
	// create the var_name_to_var_index_map and var_index_to_var_name_map
	int var_index = 1;
	for(list<string>::iterator list_it = VariablesToEliminate.begin(); list_it != VariablesToEliminate.end(); list_it++)
	{
		insertIntoVarNameToVarIndexMap(var_name_to_var_index_map, *list_it, var_index);
		insertIntoVarIndexToVarNameMap(var_index_to_var_name_map, var_index, *list_it);

		#ifdef DEBUG_SKOLEM
		cout << "(" << *list_it << ", " << var_index << ") inserted into maps "<< endl;
		#endif	

		var_index++;
	}

	t_Expression* factor = createAnd(Factors, pub_em);
	assert(factor != NULL);

	number_of_factors = 1;
	original_support_size = support.size();	
	original_factor_support_sizes.insert(make_pair(1, original_support_size));
	original_factor_varstoelim_sizes.insert(make_pair(1, number_of_vars_to_elim));

	#ifdef DEBUG_SKOLEM
	cout << "number_of_factors = " << number_of_factors << endl;
	cout << "number_of_vars_to_elim = " << number_of_vars_to_elim << endl;
	#endif	

	int size_of_transition_relation;

	// Following line commented on 21-jan-2014
	//if(use_uninterpreted_functions && number_of_vars_to_elim >= threshold_varstoelim_for_using_uninterpreted_functions)
	if(use_uninterpreted_functions)
	{
		string name_of_function = "factor";
		t_Expression* abstracted_factor = createAbstraction(name_of_function, 1, 0, support, pub_em);
		assert(abstracted_factor != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));

		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, 1, abstracted_factor, false);

		#ifdef RECORD_KEEP
		int factor_size = computeSize(factor);
		original_factor_sizes.insert(make_pair(1, factor_size));
		size_of_transition_relation = factor_size;
		int abstracted_factor_size = computeSize(abstracted_factor);
		abstracted_factor_sizes.insert(make_pair(1, abstracted_factor_size));			
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nfactor_1 of size " << factor_size << " abstracted to factor of size " << abstracted_factor_size << endl;
		#endif
	}
	else
	{
		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, 1,factor,false);

		#ifdef RECORD_KEEP
		int factor_size = computeSize(factor);
		original_factor_sizes.insert(make_pair(1, factor_size));
		size_of_transition_relation = factor_size;
		abstracted_factor_sizes.insert(make_pair(1, factor_size));
		#endif
	}
	#ifdef RECORD_KEEP
	string record_file = "skolem_function_generation_details.txt";
	FILE* record_fp = fopen(record_file.c_str(), "a+");
	assert(record_fp != NULL);

	unsigned long long int total_of_factor_sizes = 0;
	unsigned long long int total_of_abstracted_factor_sizes = 0;
	unsigned long long int total_of_factor_support_sizes = 0;
	unsigned long long int total_of_factor_varstoelim_sizes = 0;
	
	fprintf(record_fp, "F = %d\n", number_of_factors); 
	fprintf(record_fp, "E = %d\n", number_of_vars_to_elim); 

	// print details of original factors
	fprintf(record_fp, "V = %d\n\n", original_support_size);

	fprintf(record_fp, "N_f = ");
	for(map<int, int>::iterator original_factor_sizes_it = original_factor_sizes.begin(); original_factor_sizes_it != original_factor_sizes.end(); original_factor_sizes_it++)
	{
		fprintf(record_fp, "%d, ", original_factor_sizes_it->second);
		total_of_factor_sizes = total_of_factor_sizes + original_factor_sizes_it->second;
	} 
	fprintf(record_fp, "\n\n");

	fprintf(record_fp, "A_f = ");
	for(map<int, int>::iterator abstracted_factor_sizes_it = abstracted_factor_sizes.begin(); abstracted_factor_sizes_it != abstracted_factor_sizes.end(); abstracted_factor_sizes_it++)
	{
		fprintf(record_fp, "%d, ", abstracted_factor_sizes_it->second);
		total_of_abstracted_factor_sizes = total_of_abstracted_factor_sizes + abstracted_factor_sizes_it->second;
	} 
	fprintf(record_fp, "\n\n");

	fprintf(record_fp, "V_f = ");
	for(map<int, int>::iterator original_factor_support_sizes_it = original_factor_support_sizes.begin(); original_factor_support_sizes_it != original_factor_support_sizes.end(); original_factor_support_sizes_it++)
	{
		fprintf(record_fp, "%d, ", original_factor_support_sizes_it->second);
		total_of_factor_support_sizes = total_of_factor_support_sizes + original_factor_support_sizes_it->second;
	} 
	fprintf(record_fp, "\n\n");

	fprintf(record_fp, "E_f = ");
	for(map<int, int>::iterator original_factor_varstoelim_sizes_it = original_factor_varstoelim_sizes.begin(); original_factor_varstoelim_sizes_it != original_factor_varstoelim_sizes.end(); original_factor_varstoelim_sizes_it++)
	{
		fprintf(record_fp, "%d, ", original_factor_varstoelim_sizes_it->second);
		total_of_factor_varstoelim_sizes = total_of_factor_varstoelim_sizes + original_factor_varstoelim_sizes_it->second;
	} 
	fprintf(record_fp, "\n\n");

	number_of_compose_operations_for_variable = 0;
	ComposeTime = 0;
				
	#ifdef DETAILED_RECORD_KEEP
	fprintf(record_fp, "v\tF_v\tT_v\tN_v\tC_v\tR_T\tS_T\tF_v\tX_v\n\n");
	#else
	fprintf(record_fp, "v\tF_v\tT_v\tN_v\tC_v\n\n");
	#endif
	fclose(record_fp);


	string 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", benchmark_type.c_str(), benchmark_name.c_str(), machine.c_str());
	if(disable_factorization)
	{
		if(use_uninterpreted_functions)
		{
			fprintf(plot_fp, "\tmonolithic_hierarchial");
		}
		else
		{
			fprintf(plot_fp, "\tmonolithic_inlined");
		}
	}
	else
	{
		if(use_uninterpreted_functions)
		{
			fprintf(plot_fp, "\tfactorized_hierarchial");
		}
		else
		{
			fprintf(plot_fp, "\tfactorized_inlined");
		}
	}
	fprintf(plot_fp, "\t%lu\t1\t%d\t%d\t%d", Factors.size(), number_of_vars_to_elim, number_of_vars_to_elim, original_support_size);

	float avg_of_factor_sizes = (float)total_of_factor_sizes/(float)number_of_factors;
	float avg_of_abstracted_factor_sizes = (float)total_of_abstracted_factor_sizes/(float)number_of_factors;
	float avg_of_factor_support_sizes = (float)total_of_factor_support_sizes/(float)number_of_factors;
	float avg_of_factor_varstoelim_sizes = (float)total_of_factor_varstoelim_sizes/(float)number_of_factors;
	
	fprintf(plot_fp, "\t%d", size_of_transition_relation);
	fprintf(plot_fp, "\t%f\t%f\t%f\t%f\t-", avg_of_factor_sizes, avg_of_abstracted_factor_sizes, avg_of_factor_support_sizes, avg_of_factor_varstoelim_sizes);

	fclose(plot_fp);

	#endif		
}


void Skolem::monolithicSkolemFunctionGenerator(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	initializeMonolithicSkolemFunctionGenerator(Factors, VariablesToEliminate);

	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	cout << "\ninitializeMonolithicSkolemFunctionGenerator finished in " << step_ms << " milliseconds\n";

	total_time_in_generator_initialization = step_ms;
	#endif

	cout << "\n#factors = " << number_of_factors << "\t#variables_to_eliminate = " << number_of_vars_to_elim << endl;

	// compute the skolem functions, i.e. fill the SkolemFunctions matrix
	for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
	{
		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
			timed_out = true; // timed_out flag set
			return;
		}
		

		if(maximum_index_to_eliminate != -1) // to stop computation in between
		{
			if(var_to_elim_index > maximum_index_to_eliminate)
			{
				cout << "\nLet us stop here...\n";
				break;
			}			
		}

		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing skolem_function_" << var_to_elim_index << endl;
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\ncomputing skolem_function_" << var_to_elim_index << "\n";
		#endif

		#ifdef RECORD_KEEP
		unsigned long long int duration_ms;
		struct timeval start_ms, finish_ms;
		gettimeofday (&start_ms, NULL); 
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif

		findFactorsWithVariable(var_to_elim_index);// find the set of factors containing the variable

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
			timed_out = true; // timed_out flag set
			return;
		}

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\nfindFactorsWithVariable finished in " << step_ms << " milliseconds\n";
		
		cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() << endl;
		FactorFindingTime = step_ms;
		#endif

		#ifdef RECORD_KEEP
		NumberOfFactors = FactorsWithVariable.size();
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() <<"\n";
		#endif

		t_Expression* skolem_function;
		t_Expression* factor;

		if(FactorsWithVariable.size() == 0) // factor free of variable
		{
			skolem_function = createFalse(pub_em);		
		}
		else if(local_skolem_function_for_updating_factors == 0) //use alpha as the local skolem function
		{
			// obtain the existing factor
			t_Expression* previous_factor;
			previous_factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, 1);
			assert(previous_factor != NULL);

			skolem_function = computeAlpha(var_to_elim_index, 1); 
			assert(skolem_function != NULL);			
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}
			if(use_uninterpreted_functions) // abstract the skolem_function
			{
				set<string> support_skolem_function;
				computeSupport(skolem_function, support_skolem_function);
				string name_of_function = "skolem";
				t_Expression* abstracted_skolem_function = createAbstraction(name_of_function, var_to_elim_index, 0, support_skolem_function, pub_em);
				assert(abstracted_skolem_function != NULL);
				AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_skolem_function, skolem_function));
				skolem_function = abstracted_skolem_function;
			}


			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, skolem_function);
			assert(factor != NULL);	
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}
			if(use_uninterpreted_functions) // abstract the factor
			{
				set<string> support_factor;
				computeSupport(factor, support_factor);
				string name_of_function = "factor";
				t_Expression* abstracted_factor = createAbstraction(name_of_function, var_to_elim_index+1, 0, support_factor, pub_em);
				assert(abstracted_factor != NULL);
				AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));
				factor = abstracted_factor;
			}

			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, 1, factor, true);
		}
		else if(local_skolem_function_for_updating_factors == 1) //use cofactor-1 as the local skolem function
		{
			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nCalling searchOneDimensionalMatrix(FactorMatrix, " << number_of_factors << ", 1)\n";
			#endif

			// obtain the existing factor
			t_Expression* previous_factor;
			previous_factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, 1);
			assert(previous_factor != NULL);

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nsearchOneDimensionalMatrix(FactorMatrix, " << number_of_factors << ", 1) finished\n";
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nCalling computeCofactorOne(" << var_to_elim_index << ", 1)\n";
			#endif
			skolem_function = computeCofactorOne(var_to_elim_index, 1); 
			assert(skolem_function != NULL);
			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\ncomputeCofactorOne finished\n";			
			#endif
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}
			if(use_uninterpreted_functions) // abstract the skolem_function
			{
				set<string> support_skolem_function;
				computeSupport(skolem_function, support_skolem_function);
				string name_of_function = "skolem";
				t_Expression* abstracted_skolem_function = createAbstraction(name_of_function, var_to_elim_index, 0, support_skolem_function, pub_em);
				assert(abstracted_skolem_function != NULL);
				AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_skolem_function, skolem_function));
				skolem_function = abstracted_skolem_function;
			}
			

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nCalling replaceVariableByFormula(previous_factor, " << var_to_elim_index << ", skolem_function)\n";
			#endif
			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, skolem_function);
			assert(factor != NULL);	
			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nreplaceVariableByFormula finished\n";
			#endif
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGenerator\n";
				timed_out = true; // timed_out flag set
				return;
			}
			if(use_uninterpreted_functions) // abstract the factor
			{
				set<string> support_factor;
				computeSupport(factor, support_factor);
				string name_of_function = "factor";
				t_Expression* abstracted_factor = createAbstraction(name_of_function, var_to_elim_index+1, 0, support_factor, pub_em);
				assert(abstracted_factor != NULL);
				AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));
				factor = abstracted_factor;
			}


			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, 1, factor, true);			
		}	
		

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\ncomputing skolem function and next factor finished in " << step_ms << " milliseconds\n";		
		#endif

		#ifdef DEBUG_SKOLEM
		cout << "\nskolem_function computed\n";		
		#endif

		#ifdef PRINT_SKOLEM_FUNCTIONS
		string skolem_function_file_name = benchmark_name_without_extension;
		skolem_function_file_name += "_skolem_function";
		writeFormulaToFile(pub_em, skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);

		string factor_file_name = benchmark_name_without_extension;
		factor_file_name += "_factor";
		writeFormulaToFile(pub_em, factor, factor_file_name, ".v", var_to_elim_index, 0);
		#endif

		// Enter into matrix
		insertIntoOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index, skolem_function, false);

		
		#ifdef DEBUG_SKOLEM
		cout << "\nclearing variable-specific data-structures\n";
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif
		
		clearVariableSpecificDataStructures();

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\nclearVariableSpecificDataStructures finished in " << step_ms << " milliseconds\n";
		#endif

		#ifdef RECORD_KEEP
		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;
		SkolemFunctionGenTime = duration_ms;

		int skolem_function_size = computeSize(skolem_function);
		SkolemFunctionSize = skolem_function_size;	
   		#endif

		string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
		cout << "\nskolem_function_" << var_to_elim_index << ", i.e., skolem function for " << var_to_elim_name << " computed\n";

		#ifdef RECORD_KEEP
		string record_file = "skolem_function_generation_details.txt";
		FILE* record_fp = fopen(record_file.c_str(), "a+");
		assert(record_fp != NULL);

		sum_of_number_of_factors_containing_variable = sum_of_number_of_factors_containing_variable + NumberOfFactors;
		sum_of_skolem_function_sizes = sum_of_skolem_function_sizes + SkolemFunctionSize;
		total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
		total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
		number_of_variables_eliminated = var_to_elim_index;

		#ifdef DETAILED_RECORD_KEEP
		fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\t%llu\t%llu\t", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable, ComposeTime, FactorFindingTime);

		
		for(set<int>::iterator factor_it = PreviousFactorsWithVariable.begin(); factor_it != PreviousFactorsWithVariable.end(); factor_it++)
		{
			fprintf(record_fp, "%d,", *factor_it);			
		}
				
		fprintf(record_fp, "\t");		
		PreviousFactorsWithVariable.clear();

		for(list<int>::iterator size_it = sizes_of_factors_with_variable.begin(); size_it != sizes_of_factors_with_variable.end(); size_it++)
		{
			fprintf(record_fp, "%d,", *size_it);			
		}		

		sizes_of_factors_with_variable.clear();

		fprintf(record_fp, "\n\n");
		#else
		fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\n\n", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable);
		#endif

		number_of_compose_operations_for_variable = 0;
		ComposeTime = 0;
		
		fclose(record_fp);
		#endif						
	}

	

	if(use_uninterpreted_functions && false) // write the AbstractedTounabstractedFunctionsMap
	{
		string final_qe_result_file = benchmark_name_without_extension;
		final_qe_result_file += "_output.v";
		writeAbstractedTounabstractedFunctionsMap(pub_em, AbstractedTounabstractedFunctionsMap, final_qe_result_file);
	}

	if(perform_reverse_substitution)
	{
		performReverseSubstitutionOfSkolemFunctions();
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			#ifdef RECORD_KEEP
			int final_skolem_function_size = computeSize(final_skolem_function);
			skolem_function_sizes_after_reverse_substitution.push_back(final_skolem_function_size);
			sum_of_skolem_function_sizes_after_reverse_substitution = sum_of_skolem_function_sizes_after_reverse_substitution + final_skolem_function_size;
			#endif

			#ifdef PRINT_SKOLEM_FUNCTIONS
			string skolem_function_file_name = benchmark_name_without_extension;
			skolem_function_file_name += "_skolem_function_after_reverse_substitution";
			writeFormulaToFile(pub_em, final_skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
			#endif
		}
	}

	if(match_outputs_of_monolithic_and_factorized)
	{
		t_Expression* ConjunctionOfFactors = createAnd(Factors, pub_em);
		assert(ConjunctionOfFactors != NULL);
		t_Expression* ConjunctionOfFactors_with_var_substituted = ConjunctionOfFactors;
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
			
			t_HashTable<unsigned long, t_Expression*> cache;
			ConjunctionOfFactors_with_var_substituted = pub_em->ReplaceLeafByExpression(ConjunctionOfFactors_with_var_substituted, var_to_elim_name, final_skolem_function, cache, false, 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);

			assert(ConjunctionOfFactors_with_var_substituted != NULL);			

		}//for ends here
	
		result_of_qe_using_monolithic = ConjunctionOfFactors_with_var_substituted;		
	}

}



void Skolem::performReverseSubstitutionOfSkolemFunctions()
{
	t_HashTable<unsigned long, t_Expression*> reverse_substitution_cache;

	for(int i = number_of_vars_to_elim; i >= 2; i--)
	{
		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::performReverseSubstitutionOfSkolemFunctions()\n";
			timed_out = true; // timed_out flag set
			return;
		}

		t_Expression* skolem_function_to_substitute;
		skolem_function_to_substitute = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, i);
		assert(skolem_function_to_substitute != NULL);	

		cout << "\nReplacing variable_" << i << " by its skolem function in the skolem function for preceding variables" << endl;	

		for(int j = i-1; j >= 1; j--)
		{
			if(checkTimeOut()) // check for time-out
			{
				cout << "\nWarning!!Time-out inside the function Skolem::performReverseSubstitutionOfSkolemFunctions()\n";
				timed_out = true; // timed_out flag set
				return;
			}			
			
			t_Expression* destination_skolem_function;
			destination_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, j);
			assert(destination_skolem_function != NULL);

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nReplacing variable_" << i << " by its skolem function in the skolem function for variable_" << j << endl;
			#endif	

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, destination_skolem_function, "dest_sk_function", ".v", i, j);	
			#endif
			
			if(share_cache_in_reverse_substitution)
			{
				destination_skolem_function = replaceVariableByFormula(destination_skolem_function, i, skolem_function_to_substitute, reverse_substitution_cache);
			}
			else
			{
				destination_skolem_function = replaceVariableByFormula(destination_skolem_function, i, skolem_function_to_substitute);
			}
			assert(destination_skolem_function != NULL);

			#ifdef DEBUG_SKOLEM
			writeFormulaToFile(pub_em, destination_skolem_function, "dest_sk_function_rev_subst", ".v", i, j);	
			#endif


			insertIntoOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, j, destination_skolem_function, true);
		}//for ends here
		
		reverse_substitution_cache.clear();
	}// for ends here

	#ifdef RECORD_KEEP
	total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
	total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
	#endif
}// function ends here




t_Expression* Skolem::computeAlphaCombinedOrGammaCombined(int var_to_elim_index)
{
	// Let us compute alpha_combined_{var_to_elim_index}\vee gamma_combined_{var_to_elim_index}
	// Suppose i = var_to_elim_index

	// i.e. we need to compute alpha_combined_{i}\vee gamma_combined_{i}
	// i.e., conjunction of alpha_combined_or_gamma_combined_components
	// Each alpha_combined_or_gamma_combined_component_i_j = co-factor-1_i_j
	set<t_Expression*> alpha_combined_or_gamma_combined_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing components of alpha_combined_or_gamma_combined\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\ncomputing components of alpha_combined_or_gamma_combined\n";
	#endif

	#ifdef RECORD_KEEP
	int number_of_factors_containing_var_to_elim_index = FactorsWithVariable.size();
	#endif

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index
		// Each alpha_combined_or_gamma_combined_component_i_j = co-factor-1_i_j

		t_Expression* cofactor_1_i_j;
		cofactor_1_i_j = computeCofactorOne(var_to_elim_index, factor_index); 
		assert(cofactor_1_i_j != NULL);	

		t_Expression* alpha_combined_or_gamma_combined_component = cofactor_1_i_j;			
				
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, alpha_combined_or_gamma_combined_component, "alpha_combined_or_gamma_combined_component", ".v", var_to_elim_index, factor_index);		
		cout << "\nalpha_combined_or_gamma_combined_component[" << var_to_elim_index << ", " << factor_index << "] obtained\n";			
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nalpha_combined_or_gamma_combined_component[" << var_to_elim_index << ", " << factor_index << "] obtained\n";	
		cout << "\nsize of alpha_combined_or_gamma_combined_component[" << var_to_elim_index << ", " << factor_index << "] is: " << computeSize(alpha_combined_or_gamma_combined_component) << endl;
		#endif
				
		alpha_combined_or_gamma_combined_components.insert(alpha_combined_or_gamma_combined_component);	

		FactorsAffectingSkolemFunction.push_back(factor_index);
						
	}// for each factor ends here

	// recall that alpha_combined_or_gamma_combined = conjunction of alpha_combined_or_gamma_combined_components
	t_Expression* alpha_combined_or_gamma_combined;				
	if(alpha_combined_or_gamma_combined_components.size() == 0) // we should return true in this case as per the defn. of alpha_combined_or_gamma_combined
	{
		alpha_combined_or_gamma_combined = createTrue(pub_em); 
		assert(alpha_combined_or_gamma_combined != NULL);
	}
	else
	{
		alpha_combined_or_gamma_combined = createAnd(alpha_combined_or_gamma_combined_components, pub_em);
		assert(alpha_combined_or_gamma_combined != NULL);
	}

	if(use_uninterpreted_functions) // abstract the alpha_combined_or_gamma_combined
	{
		set<string> support_alpha_combined_or_gamma_combined;
		computeSupport(alpha_combined_or_gamma_combined, support_alpha_combined_or_gamma_combined);
		string name_of_function = "alpha_combined_or_gamma_combined";
		t_Expression* abstracted_alpha_combined_or_gamma_combined = createAbstraction(name_of_function, var_to_elim_index, 0, support_alpha_combined_or_gamma_combined, pub_em);
		assert(abstracted_alpha_combined_or_gamma_combined != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_alpha_combined_or_gamma_combined, alpha_combined_or_gamma_combined));
		alpha_combined_or_gamma_combined = abstracted_alpha_combined_or_gamma_combined;
	}


	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, alpha_combined_or_gamma_combined, "alpha_combined_or_gamma_combined", ".v", var_to_elim_index, 0);				
	#endif

	#ifdef RECORD_KEEP
	NumberOfFactors = number_of_factors_containing_var_to_elim_index;
	#endif

	return alpha_combined_or_gamma_combined;		
} // function ends here



int Skolem::computeSize(t_Expression* formula)
{
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 

	assert(formula != NULL);

	int size;
	static t_HashTable<unsigned long int, int > cache;
	
	unsigned long int formulaID = formula->getID();
	t_HashTable<unsigned long int, int >::iterator cache_it = cache.find(formulaID);
	if (cache_it != cache.end())
	{
		size = cache_it.getValue();		
	}
	else
	{
		size = pub_em->getSizeOfExpression(formula);
		cache[formulaID] = size;
	}

	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	total_time_in_compute_size = total_time_in_compute_size + step_ms;

	return size;
}// function ends here


void Skolem::findFactorsWithVariable(string &var_to_elim, set<int> &factors_with_var_to_elim)
{
	factors_with_var_to_elim.clear();

	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);

		if(!formulaFreeOfVariable(factor, var_to_elim))
		{
			factors_with_var_to_elim.insert(factor_index);	
		}
	}
}

bool Skolem::formulaFreeOfVariable(t_Expression* formula, string &var_string)
{
	assert(formula != NULL);

	set<string> support;
	computeSupport(formula, support);
	if(support.find(var_string) == support.end()) // formula is free of var_string
	{
		return true;
	}
	else
	{
		return false;
	}
}


void Skolem::getNextVariableToEliminate(string &var_to_elim_selected, unsigned long long int &var_to_elim_selected_cost, int var_to_elim_index_of_last_ordered_variable)
{
	var_to_elim_selected = "";
	bool first_var_encountered = false;
	
	for(set<string>::iterator var_it = unordered_vars_to_elim.begin(); var_it != unordered_vars_to_elim.end(); var_it++)
	{
		string var_to_elim = *var_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nvar_to_elim = " << var_to_elim << endl;
		#endif

		unsigned long long int cost;

		// Let's compute cost1: cost of \alpha \vee \gamma
		unsigned long long int cost1 = 0;

		set<int> factors_with_var_to_elim;

		if(apply_scope_reduction)
		{
			findTopFactorsWithVariable(var_to_elim, factors_with_var_to_elim);
		}
		else
		{
			findFactorsWithVariable(var_to_elim, factors_with_var_to_elim);
		}

		#ifdef DEBUG_SKOLEM
		showSet(factors_with_var_to_elim, "factors_with_var_to_elim");
		#endif

		for(set<int>::iterator factors_with_var_to_elim_it = factors_with_var_to_elim.begin(); factors_with_var_to_elim_it != factors_with_var_to_elim.end(); factors_with_var_to_elim_it++)
		{
			int factor_with_var_to_elim = *factors_with_var_to_elim_it;

			map<int, int>::iterator factor_to_costs_map_it = factor_to_costs_map.find(factor_with_var_to_elim);
			assert(factor_to_costs_map_it != factor_to_costs_map.end());

			unsigned long long int cost_for_factor = (unsigned long long int)(factor_to_costs_map_it->second);
			cost1 = cost1 + cost_for_factor;			
		}

		#ifdef DEBUG_SKOLEM
		cout << "\ncost1 = " << cost1 << endl;
		#endif

		// Let's compute cost2: cost of delta part
		unsigned long long int cost2 = 0;

		set<int> SkylineVariables = computeSkylineInLeastCostFirst(var_to_elim, false);
		
		#ifdef DEBUG_SKOLEM
		showSet(SkylineVariables, "SkylineVariables");
		#endif

		int min_skyline_variable = number_of_vars_to_elim;
		for(set<int>::iterator SkylineVariables_it = SkylineVariables.begin(); SkylineVariables_it != SkylineVariables.end(); SkylineVariables_it++)
		{
			int skyline_variable = *SkylineVariables_it;
			if(skyline_variable < min_skyline_variable)
				min_skyline_variable = skyline_variable;
			
			map<int, int>::iterator deltas_to_costs_map_it = deltas_to_costs_map.find(skyline_variable);
			assert(deltas_to_costs_map_it != deltas_to_costs_map.end());

			unsigned long long int cost_for_delta = (unsigned long long int)(deltas_to_costs_map_it->second);
			cost2 = cost2 + cost_for_delta;
		} 

		#ifdef DEBUG_SKOLEM
		cout << "\ncost2 = " << cost2 << endl;
		cout << "\nmin_skyline_variable = " << min_skyline_variable << endl;
		#endif

		for(int skolem_function_index = min_skyline_variable+1; skolem_function_index <= var_to_elim_index_of_last_ordered_variable; skolem_function_index++)
		{
			map<int, int>::iterator skolemfunctions_to_costs_map_it = skolemfunctions_to_costs_map.find(skolem_function_index);
			assert(skolemfunctions_to_costs_map_it != skolemfunctions_to_costs_map.end());

			unsigned long long int cost_for_skolem = (unsigned long long int)(skolemfunctions_to_costs_map_it->second);
			cost2 = cost2 + cost_for_skolem;
		} 

		if(true)
		{
			// Let's compute cost3: cost of correction part
			// correction part is negation of conjunction of cofactor-0's
			// Hence, cost3 = cost1

			unsigned long long int cost3;

			if(var_to_elim_index_of_last_ordered_variable == 0) // we are selecting the first variable 
			{
				cost3 = 0;
			}
			else
			{
				cost3 = cost1;
			}

			// Let's compute cost: cost1 + cost2 + cost3
			cost = cost1 + cost2 + cost3;

			#ifdef DEBUG_SKOLEM
			cout << "\ncost2 = " << cost2 << endl;
			cout << "\ncost3 = " << cost3 << endl;
			cout << "\ncost = " << cost << endl;
			#endif
		
		}
		else
		{
			// Let's compute cost: cost1 + cost2
			cost = cost1 + cost2;

			#ifdef DEBUG_SKOLEM
			cout << "\ncost2 = " << cost2 << endl;
			cout << "\ncost = " << cost << endl;
			#endif
		}

		if(!first_var_encountered) // first variable encountered now
		{
			var_to_elim_selected = var_to_elim;
			var_to_elim_selected_cost = cost;

			first_var_encountered = true;
		}
		else if(cost < var_to_elim_selected_cost)
		{
			var_to_elim_selected = var_to_elim;
			var_to_elim_selected_cost = cost;
		}

		#ifdef DEBUG_SKOLEM
		cout << "\nvar_to_elim_selected = " << var_to_elim_selected << endl;
		cout << "\nvar_to_elim_selected_cost = " << var_to_elim_selected_cost << endl;
		#endif		
		
	}// for ends here

	assert(first_var_encountered);

}// function ends here



set<int> Skolem::computeSkylineInLeastCostFirst(string &var_to_elim, bool upate_eqclasses)
{
	// Let's first find the factors connected to var_to_elim
	map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.find(var_to_elim);
	assert(factor_graph_vars_to_factors_map_it != factor_graph_vars_to_factors_map.end());
	set<int> FactorsContainingVartoelim = factor_graph_vars_to_factors_map_it->second;

	// let's find the neighbours of var_to_elim
	set<string> Neighbours;
	for(set<int>::iterator FactorsContainingVartoelim_it = FactorsContainingVartoelim.begin(); FactorsContainingVartoelim_it != FactorsContainingVartoelim.end(); FactorsContainingVartoelim_it++)
	{
		int FactorContainingVartoelim = *FactorsContainingVartoelim_it;

		map<int, set<string> >::iterator factor_graph_factors_to_vars_map_it = factor_graph_factors_to_vars_map.find(FactorContainingVartoelim);
		assert(factor_graph_factors_to_vars_map_it != factor_graph_factors_to_vars_map.end());
		set<string> VariablesConnectedToFactor = factor_graph_factors_to_vars_map_it->second;

		for(set<string>::iterator VariablesConnectedToFactor_it = VariablesConnectedToFactor.begin(); VariablesConnectedToFactor_it != VariablesConnectedToFactor.end();  VariablesConnectedToFactor_it++)
		{
			string VariableConnectedToFactor = *VariablesConnectedToFactor_it;
			if(VariableConnectedToFactor == var_to_elim || searchVarNameToVarIndexMap(var_name_to_var_index_map, VariableConnectedToFactor) >= 1)
			{
				Neighbours.insert(VariableConnectedToFactor);
			}
		}		
	}

	set<string> merged_equivalence_class;
	int location_of_merged_equivalence_class;
	mergeEquivalenceClasses(Neighbours, merged_equivalence_class, location_of_merged_equivalence_class);
	// merge equivalence classes of variables \in Neighbours

	if(upate_eqclasses)
	{
		for(set<string>::iterator Neighbours_it = Neighbours.begin(); Neighbours_it != Neighbours.end(); Neighbours_it++)	
		{
			string neighbour = *Neighbours_it;
			assert(vars_to_eqclassnos_map.find(neighbour) != vars_to_eqclassnos_map.end());
			vars_to_eqclassnos_map[neighbour] = location_of_merged_equivalence_class;			
		}

		assert(eqclassnos_to_eqclasses_map.find(location_of_merged_equivalence_class) != eqclassnos_to_eqclasses_map.end());
		eqclassnos_to_eqclasses_map[location_of_merged_equivalence_class] = merged_equivalence_class;
	}

	set<string> reachable_variables = merged_equivalence_class;
	reachable_variables.erase(var_to_elim);
	
	set<int> SkylineVariables;
	for(set<string>::iterator reachable_variables_it = reachable_variables.begin(); reachable_variables_it != reachable_variables.end(); reachable_variables_it++)
	{
		string reachable_variable = *reachable_variables_it;
		set<int> reachable_factors;
		map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.find(reachable_variable);
		assert(factor_graph_vars_to_factors_map_it != factor_graph_vars_to_factors_map.end());
		reachable_factors = factor_graph_vars_to_factors_map_it->second;

		// skyline includes top variables of the reachable_factors
		for(set<int>::iterator reachable_factors_it = reachable_factors.begin(); reachable_factors_it != reachable_factors.end(); reachable_factors_it++)
		{
			int reachable_factor = *reachable_factors_it;

			map<int, string >::iterator factor_graph_factors_to_topvars_map_it = factor_graph_factors_to_topvars_map.find(reachable_factor);
			assert(factor_graph_factors_to_topvars_map_it != factor_graph_factors_to_topvars_map.end());
			string top_variable = factor_graph_factors_to_topvars_map_it->second;

			int top_variable_index = searchVarNameToVarIndexMap(var_name_to_var_index_map, top_variable);
			assert(top_variable_index != -1);
			SkylineVariables.insert(top_variable_index);
		}
	}

	return SkylineVariables;	
}


void Skolem::findStronglyConnectedComponentsInFactorGraph()
{
	for(map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.begin(); factor_graph_vars_to_factors_map_it != factor_graph_vars_to_factors_map.end(); factor_graph_vars_to_factors_map_it++)
	{
		// take each variable to be eliminated
		string var_to_elim = factor_graph_vars_to_factors_map_it->first;
		// Let's first find the factors connected to var_to_elim
		set<int> FactorsContainingVartoelim = factor_graph_vars_to_factors_map_it->second;

		// let's find the neighbours of var_to_elim
		set<string> Neighbours;
		for(set<int>::iterator FactorsContainingVartoelim_it = FactorsContainingVartoelim.begin(); FactorsContainingVartoelim_it != FactorsContainingVartoelim.end(); FactorsContainingVartoelim_it++)
		{
			int FactorContainingVartoelim = *FactorsContainingVartoelim_it;

			map<int, set<string> >::iterator factor_graph_factors_to_vars_map_it = factor_graph_factors_to_vars_map.find(FactorContainingVartoelim);
			assert(factor_graph_factors_to_vars_map_it != factor_graph_factors_to_vars_map.end());
			set<string> VariablesConnectedToFactor = factor_graph_factors_to_vars_map_it->second;

			set_union(Neighbours.begin(), Neighbours.end(), VariablesConnectedToFactor.begin(), VariablesConnectedToFactor.end(), inserter(Neighbours, Neighbours.end()));
		}

		set<string> merged_scc;
		int location_of_merged_scc;
		mergeStronglyConnectedComponents(Neighbours, merged_scc, location_of_merged_scc);
		// merge sccs of variables \in Neighbours

		for(set<string>::iterator Neighbours_it = Neighbours.begin(); Neighbours_it != Neighbours.end(); Neighbours_it++)	
		{
			string neighbour = *Neighbours_it;
			assert(factor_graph_vars_to_sccnos_map.find(neighbour) != factor_graph_vars_to_sccnos_map.end());
			factor_graph_vars_to_sccnos_map[neighbour] = location_of_merged_scc;			
		}

		assert(factor_graph_sccnos_to_sccs_map.find(location_of_merged_scc) != factor_graph_sccnos_to_sccs_map.end());
		factor_graph_sccnos_to_sccs_map[location_of_merged_scc] = merged_scc;
	}// for ends here
	
}


void Skolem::mergeEquivalenceClasses(set<string> &Neighbours, set<string> &merged_equivalence_class, int &location_of_merged_equivalence_class)
{
	set<int> eqclassnos;
	merged_equivalence_class.clear();
	for(set<string>::iterator Neighbours_it = Neighbours.begin(); Neighbours_it != Neighbours.end(); Neighbours_it++)	
	{
		string neighbour = *Neighbours_it;

		map<string, int >::iterator vars_to_eqclassnos_map_it = vars_to_eqclassnos_map.find(neighbour);
		assert(vars_to_eqclassnos_map_it != vars_to_eqclassnos_map.end());
		int eqclassno = vars_to_eqclassnos_map_it->second;
		eqclassnos.insert(eqclassno);

		map<int, set<string> >::iterator eqclassnos_to_eqclasses_map_it = eqclassnos_to_eqclasses_map.find(eqclassno);
		assert(eqclassnos_to_eqclasses_map_it != eqclassnos_to_eqclasses_map.end());
		set<string> eqclass = eqclassnos_to_eqclasses_map_it->second;

		set_union(merged_equivalence_class.begin(), merged_equivalence_class.end(), eqclass.begin(), eqclass.end(), inserter(merged_equivalence_class, merged_equivalence_class.end()));			
	}
	set<int>::iterator eqclassnos_it = eqclassnos.begin();
	location_of_merged_equivalence_class = *eqclassnos_it;
}


void Skolem::mergeStronglyConnectedComponents(set<string> &Neighbours, set<string> &merged_scc, int &location_of_merged_scc)
{
	set<int> sccnos;
	merged_scc.clear();
	for(set<string>::iterator Neighbours_it = Neighbours.begin(); Neighbours_it != Neighbours.end(); Neighbours_it++)	
	{
		string neighbour = *Neighbours_it;

		map<string, int >::iterator factor_graph_vars_to_sccnos_map_it = factor_graph_vars_to_sccnos_map.find(neighbour);
		assert(factor_graph_vars_to_sccnos_map_it != factor_graph_vars_to_sccnos_map.end());
		int sccno = factor_graph_vars_to_sccnos_map_it->second;
		sccnos.insert(sccno);

		map<int, set<string> >::iterator factor_graph_sccnos_to_sccs_map_it = factor_graph_sccnos_to_sccs_map.find(sccno);
		assert(factor_graph_sccnos_to_sccs_map_it != factor_graph_sccnos_to_sccs_map.end());
		set<string> scc = factor_graph_sccnos_to_sccs_map_it->second;

		set_union(merged_scc.begin(), merged_scc.end(), scc.begin(), scc.end(), inserter(merged_scc, merged_scc.end()));
	}
	set<int>::iterator sccnos_it = sccnos.begin();
	location_of_merged_scc = *sccnos_it;
}


bool Skolem::checkIfDeltaIsNeeded(string &var_to_elim)
{
	if(topvars.find(var_to_elim) == topvars.end()) // var_to_elim is not a top-var
	{
		return false;
	}
	else
	{
		map<string, int >::iterator factor_graph_vars_to_sccnos_map_it = factor_graph_vars_to_sccnos_map.find(var_to_elim);
		assert(factor_graph_vars_to_sccnos_map_it != factor_graph_vars_to_sccnos_map.end());
		int scc_of_var_to_elim = factor_graph_vars_to_sccnos_map_it->second;

		for(set<string>::iterator var_it = unordered_vars_to_elim.begin(); var_it != unordered_vars_to_elim.end(); var_it++)
		{
			string unordered_var_to_elim = *var_it;

			map<string, int >::iterator factor_graph_vars_to_sccnos_map_it2 = factor_graph_vars_to_sccnos_map.find(unordered_var_to_elim);
			assert(factor_graph_vars_to_sccnos_map_it2 != factor_graph_vars_to_sccnos_map.end());
			int scc_of_unordered_var_to_elim = factor_graph_vars_to_sccnos_map_it2->second;

			if(scc_of_var_to_elim == scc_of_unordered_var_to_elim) // var_to_elim is reachable from unordered_var_to_elim
			{
				return true;
			}
		}//for ends here

		return false;
	}//else ends here	
}


void Skolem::updateTopVariablesOfFactors(string &var_to_elim)
{
	// find factors connected to var_to_elim
	map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.find(var_to_elim);
	set<int> FactorsContainingVartoelim = factor_graph_vars_to_factors_map_it->second;

	bool var_to_elim_is_in_top = false;
	
	for(set<int>::iterator FactorsContainingVartoelim_it = FactorsContainingVartoelim.begin(); FactorsContainingVartoelim_it != FactorsContainingVartoelim.end(); FactorsContainingVartoelim_it++)
	{
		int FactorContainingVartoelim = *FactorsContainingVartoelim_it;
		if(factor_graph_factors_to_topvars_map.find(FactorContainingVartoelim) == factor_graph_factors_to_topvars_map.end()) // factor does not have a top variable
		{
			factor_graph_factors_to_topvars_map.insert(make_pair(FactorContainingVartoelim, var_to_elim));
			var_to_elim_is_in_top = true;
		}
	}
	if(var_to_elim_is_in_top)
	{
		topvars.insert(var_to_elim);
	}
}


void Skolem::showDataStructuresForLeastCostOrdering()
{
	cout<<"\n\nshowDataStructuresForLeastCostOrdering()\n";
	cout<<"\nfactor_graph_factors_to_vars_map\n";
	for(map<int, set<string> >::iterator factor_graph_factors_to_vars_map_it = factor_graph_factors_to_vars_map.begin(); factor_graph_factors_to_vars_map_it != factor_graph_factors_to_vars_map.end(); factor_graph_factors_to_vars_map_it++)
	{
		cout << endl << factor_graph_factors_to_vars_map_it->first <<"\t" ;
		showSet(factor_graph_factors_to_vars_map_it->second);
	}

	cout<<"\nfactor_graph_vars_to_factors_map\n";
	for(map<string, set<int> >::iterator factor_graph_vars_to_factors_map_it = factor_graph_vars_to_factors_map.begin(); factor_graph_vars_to_factors_map_it != factor_graph_vars_to_factors_map.end(); factor_graph_vars_to_factors_map_it++)
	{
		cout << endl << factor_graph_vars_to_factors_map_it->first <<"\t" ;
		showSet(factor_graph_vars_to_factors_map_it->second);
	}

	cout<<"\nfactor_graph_factors_to_topvars_map\n";
	for(map<int, string >::iterator factor_graph_factors_to_topvars_map_it = factor_graph_factors_to_topvars_map.begin(); factor_graph_factors_to_topvars_map_it != factor_graph_factors_to_topvars_map.end(); factor_graph_factors_to_topvars_map_it++)
	{
		cout << endl << factor_graph_factors_to_topvars_map_it->first <<"\t" ;
		cout << factor_graph_factors_to_topvars_map_it->second;
	}

	cout<<"\ntopvars\n";
	showSet(topvars);

	cout<<"\nfactor_graph_vars_to_sccnos_map\n";
	for(map<string, int >::iterator factor_graph_vars_to_sccnos_map_it = factor_graph_vars_to_sccnos_map.begin(); factor_graph_vars_to_sccnos_map_it != factor_graph_vars_to_sccnos_map.end(); factor_graph_vars_to_sccnos_map_it++)
	{
		cout << endl << factor_graph_vars_to_sccnos_map_it->first <<"\t" ;
		cout << factor_graph_vars_to_sccnos_map_it->second;
	}

	cout<<"\nfactor_graph_sccnos_to_sccs_map\n";
	for(map<int, set<string> >::iterator factor_graph_sccnos_to_sccs_map_it = factor_graph_sccnos_to_sccs_map.begin(); factor_graph_sccnos_to_sccs_map_it != factor_graph_sccnos_to_sccs_map.end(); factor_graph_sccnos_to_sccs_map_it++)
	{
		cout << endl << factor_graph_sccnos_to_sccs_map_it->first <<"\t" ;
		showSet(factor_graph_sccnos_to_sccs_map_it->second);
	}

	cout<<"\nvars_to_eqclassnos_map\n";
	for(map<string, int >::iterator vars_to_eqclassnos_map_it = vars_to_eqclassnos_map.begin(); vars_to_eqclassnos_map_it != vars_to_eqclassnos_map.end(); vars_to_eqclassnos_map_it++)
	{
		cout << endl << vars_to_eqclassnos_map_it->first <<"\t" ;
		cout << vars_to_eqclassnos_map_it->second;
	}

	cout<<"\neqclassnos_to_eqclasses_map\n";
	for(map<int, set<string> >::iterator eqclassnos_to_eqclasses_map_it = eqclassnos_to_eqclasses_map.begin(); eqclassnos_to_eqclasses_map_it != eqclassnos_to_eqclasses_map.end(); eqclassnos_to_eqclasses_map_it++)
	{
		cout << endl << eqclassnos_to_eqclasses_map_it->first <<"\t" ;
		showSet(eqclassnos_to_eqclasses_map_it->second);
	}

	cout<<"\nordered_vars_to_elim\n";
	showList(ordered_vars_to_elim);

	cout<<"\nunordered_vars_to_elim\n";
	showSet(unordered_vars_to_elim);

	cout<<"\nfactor_to_costs_map\n";
	for(map<int, int >::iterator factor_to_costs_map_it = factor_to_costs_map.begin(); factor_to_costs_map_it != factor_to_costs_map.end(); factor_to_costs_map_it++)
	{
		cout << endl << factor_to_costs_map_it->first <<"\t" ;
		cout << factor_to_costs_map_it->second;
	}

	cout<<"\nskolemfunctions_to_costs_map\n";
	for(map<int, int >::iterator skolemfunctions_to_costs_map_it = skolemfunctions_to_costs_map.begin(); skolemfunctions_to_costs_map_it != skolemfunctions_to_costs_map.end(); skolemfunctions_to_costs_map_it++)
	{
		cout << endl << skolemfunctions_to_costs_map_it->first <<"\t" ;
		cout << skolemfunctions_to_costs_map_it->second;
	}

	cout<<"\ndeltas_to_costs_map\n";
	for(map<int, int >::iterator deltas_to_costs_map_it = deltas_to_costs_map.begin(); deltas_to_costs_map_it != deltas_to_costs_map.end(); deltas_to_costs_map_it++)
	{
		cout << endl << deltas_to_costs_map_it->first <<"\t" ;
		cout << deltas_to_costs_map_it->second;
	}
}



void Skolem::clearAllDataStructures()
{
	// clearing global data structures
	var_name_to_var_index_map.clear(); 
	var_index_to_var_name_map.clear(); 
	Skylines.clear();	
	UnionOfSkylines.clear(); 
	FactorMatrix.clear(); 
	DeltaCombinedMatrix.clear(); 
	FactorWiseDeltaCombinedMatrix.clear();
	DeltaCombinedSubstMatrix.clear(); 
	SkolemFunctions.clear();
	AbstractedTounabstractedFunctionsMap.clear();	


	// clearing variable-specific data structures
	FactorsWithVariable.clear();
	CofactorOneMatrix.clear();
	CofactorZeroMatrix.clear();
	NegatedCofactorOneMatrix.clear();
	NegatedCofactorZeroMatrix.clear();
	AlphaMatrix.clear();
	BetaMatrix.clear();
	GammaMatrix.clear();
	DeltaMatrix.clear();
	pub_cofactor_zero_cache.clear();
	pub_cofactor_one_cache.clear();	

}



t_Expression* Skolem::computeCorrectionPart(int var_to_elim_index)
{
	// Suppose i = var_to_elim_index

	set<t_Expression*> correction_part_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing components of correction_part\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\ncomputing components of correction_part\n";
	#endif

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index
		// Each correction_part_component_i_j = co-factor-0_i_j

		t_Expression* cofactor_0_i_j;
		cofactor_0_i_j = computeCofactorZero(var_to_elim_index, factor_index); 
		assert(cofactor_0_i_j != NULL);	

		t_Expression* correction_part_component = cofactor_0_i_j;			
				
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, correction_part_component, "correction_part_component", ".v", var_to_elim_index, factor_index);		
		cout << "\ncorrection_part_component[" << var_to_elim_index << ", " << factor_index << "] obtained\n";			
		#endif
				
		correction_part_components.insert(correction_part_component);					
	}// for each factor ends here

	// recall that correction_part = ~(conjunction of correction_part_components)
	t_Expression* correction_part;				
	if(correction_part_components.size() == 0) 
	{
		correction_part = createFalse(pub_em); 
		assert(correction_part != NULL);
	}
	else
	{
		correction_part = createAnd(correction_part_components, pub_em);
		assert(correction_part != NULL);

		correction_part = createNot(correction_part, pub_em);
		assert(correction_part != NULL);
	}

	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, correction_part, "correction_part", ".v", var_to_elim_index, 0);				
	#endif

	return correction_part;		
} // function ends here





void Skolem::printFactorGraph(set<string> &Final_VariablesToEliminate_Set)
{
	string dot_file_name = benchmark_name_without_extension;
	dot_file_name += "_factor_graph.dot";

	fstream file_op(dot_file_name.c_str(),ios::out);
        file_op << "digraph G {" << endl;

	set<string> PrintedVariables;
	
	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// Suppose j = factor_index
		// first let us obtain factor_1_j
			
		t_Expression* factor_1_j = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor_1_j != NULL);

		set<string> support;
		computeSupport(factor_1_j, support);

		file_op << "f" << factor_index <<"[shape=square, color=red, label=\""<< "f_"<< factor_index <<"\"];"<<endl;

		for(set<string>::iterator support_it = support.begin(); support_it != support.end(); support_it++)
		{
			string variable = *support_it;
			
			if(Final_VariablesToEliminate_Set.find(variable) != Final_VariablesToEliminate_Set.end()) // this is a variable to be eliminated
			{
				if(PrintedVariables.find(variable) == PrintedVariables.end()) //not already printed
				{
					file_op << variable <<"[color=green, label=\""<< variable <<"\"];"<<endl;
					PrintedVariables.insert(variable);
				}

				file_op << "f" << factor_index << "->" << variable << "[dir=none];" << endl;	
			}
			else // this is a variable to remain
			{
			     // do not do anything
			}
		}		
		
	}//for each factor ends here

	file_op << "}" << endl;
	file_op.close();	
}// function ends here


void Skolem::printFactorGraphAsData(set<string> &Final_VariablesToEliminate_Set)
{
	string dat_file_name = benchmark_name_without_extension;
	dat_file_name += "_factor_graph.dat";

	fstream file_op(dat_file_name.c_str(),ios::out);
        
	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// Suppose j = factor_index
		// first let us obtain factor_1_j
			
		t_Expression* factor_1_j = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor_1_j != NULL);

		set<string> support;
		computeSupport(factor_1_j, support);

		for(set<string>::iterator support_it = support.begin(); support_it != support.end(); support_it++)
		{
			string variable = *support_it;
			
			if(Final_VariablesToEliminate_Set.find(variable) != Final_VariablesToEliminate_Set.end()) // this is a variable to be eliminated
			{
				int variable_index = searchVarNameToVarIndexMap(var_name_to_var_index_map, variable);				
				file_op << factor_index <<"\t"<< variable_index << endl;
			}
			else // this is a variable to remain
			{
			     // do not do anything
			}
		}		
		
	}//for each factor ends here

	file_op.close();	
}// function ends here


void Skolem::initializeMonolithicSkolemFunctionGeneratorWithScopeReduction(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	// 1) Remove variables which are not occuring in the factors
	// from the set of variables to be eliminated, and
	// 2) Insert the factors into FactorMatrix
	// 3) Decide the order of variable elimination

	set<string> support;
	set<string> VariablesToEliminate_Set(VariablesToEliminate.begin(), VariablesToEliminate.end());
	set<string> Final_VariablesToEliminate_Set;
	map<string, int> VarsToElim_To_Factors_Map;
	int factor_index = 1;
	number_of_factors = Factors.size();
	// insert factors into FactorMatrix[1...number_of_factors]
	
	#ifdef DETAILED_RECORD_KEEP
	string support_file_name = benchmark_name_without_extension;
	support_file_name += "_support.txt";
	FILE* support_fp = fopen(support_file_name.c_str(), "w");
	assert(support_fp != NULL);
	printSet(VariablesToEliminate_Set, "Original_VariablesToEliminate_Set", support_fp);
	#endif	

	for(set<t_Expression*>::iterator factor_it = Factors.begin(); factor_it != Factors.end(); factor_it++)
	{
		t_Expression* factor = *factor_it;
		assert(factor != NULL);			

		set<string> support_factor;
		computeSupport(factor, support_factor);
		int support_size = support_factor.size();
		original_factor_support_sizes.insert(make_pair(factor_index, support_size));

		copy(support_factor.begin(), support_factor.end(), inserter(support, support.end()));

		set<string> varstoelim_in_support_factor;
		set_intersection(support_factor.begin(), support_factor.end(), VariablesToEliminate_Set.begin(), VariablesToEliminate_Set.end(), inserter(varstoelim_in_support_factor, varstoelim_in_support_factor.begin()));
		int varstoelim_in_support_factor_size = varstoelim_in_support_factor.size();
		original_factor_varstoelim_sizes.insert(make_pair(factor_index, varstoelim_in_support_factor_size)); 
						
		int factor_size = computeSize(factor);
		original_factor_sizes.insert(make_pair(factor_index, factor_size));
		copy(varstoelim_in_support_factor.begin(), varstoelim_in_support_factor.end(), inserter(Final_VariablesToEliminate_Set, Final_VariablesToEliminate_Set.end()));

		for(set<string>::iterator varstoelim_it = varstoelim_in_support_factor.begin(); varstoelim_it != varstoelim_in_support_factor.end(); varstoelim_it++)
		{
			string variable_to_eliminate = *varstoelim_it;
			map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.find(variable_to_eliminate);
			if(VarsToElim_To_Factors_Map_it == VarsToElim_To_Factors_Map.end()) 
			// variable_to_eliminate occuring for the first time
			{
				VarsToElim_To_Factors_Map.insert(make_pair(variable_to_eliminate, 1));
			}
			else
			{
				(VarsToElim_To_Factors_Map_it->second)++;
			}
		} 
		
		#ifdef DETAILED_RECORD_KEEP
		fprintf(support_fp,"\nfactor_%d\n",factor_index);
		cout << endl;
		printSet(support_factor, "support_factor", support_fp);
		cout << endl;
		printSet(varstoelim_in_support_factor, "varstoelim_in_support_factor", support_fp);
		cout << endl;		
		#endif	

		if(use_uninterpreted_functions)
		{
			string name_of_function = "factor";
			t_Expression* abstracted_factor = createAbstraction(name_of_function, 1, factor_index, support_factor, pub_em);
			assert(abstracted_factor != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));

			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, abstracted_factor, false);

			#ifdef RECORD_KEEP
			int abstracted_factor_size = computeSize(abstracted_factor);
			abstracted_factor_sizes.insert(make_pair(factor_index, abstracted_factor_size));			
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nfactor_" << factor_index << " of size " << factor_size << " abstracted to factor of size " << abstracted_factor_size << endl;
			#endif
		}
		else
		{
			insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, factor, false);

			#ifdef RECORD_KEEP
			abstracted_factor_sizes.insert(make_pair(factor_index, factor_size));
			#endif
		}

		factor_index++;		
	}

	#ifdef DETAILED_RECORD_KEEP
	printSet(support, "support", support_fp);
	printSet(Final_VariablesToEliminate_Set, "Final_VariablesToEliminate_Set", support_fp);
	fclose(support_fp);
	#endif
	
	if(order_of_elimination_of_variables == 2)
	{
		// we should read the order from the given file
		list<string> OrderOfVariableEliminationFromFile;
		obtainOrderOfVariableEliminationFromFile(OrderOfVariableEliminationFromFile);

		#ifdef DEBUG_SKOLEM 
		cout << endl << "OrderOfVariableEliminationFromFile" << endl;
		showList(OrderOfVariableEliminationFromFile);
		#endif

		VariablesToEliminate.clear();

		for(list<string>::iterator var_order_it = OrderOfVariableEliminationFromFile.begin(); var_order_it != OrderOfVariableEliminationFromFile.end(); var_order_it++)
		{
			string var_from_order_file = *var_order_it;
			if(Final_VariablesToEliminate_Set.find(var_from_order_file) != Final_VariablesToEliminate_Set.end()) // this is a var to elim
			{
				VariablesToEliminate.push_back(var_from_order_file);
			}
		}

		cout << endl << "VariablesToEliminate" << endl;
		showList(VariablesToEliminate);
		
	}	
	else if(order_of_elimination_of_variables == 1)
	{
		map<int, set<string> > Factors_To_VarsToElim_Map;
		for(map<string, int>::iterator VarsToElim_To_Factors_Map_it = VarsToElim_To_Factors_Map.begin(); VarsToElim_To_Factors_Map_it != VarsToElim_To_Factors_Map.end(); VarsToElim_To_Factors_Map_it++)
		{
			string variable_to_eliminate = VarsToElim_To_Factors_Map_it->first;
			int number_of_factors = VarsToElim_To_Factors_Map_it->second;
			cout << endl << variable_to_eliminate << "\t" << number_of_factors << endl;

			map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.find(number_of_factors);
			if(Factors_To_VarsToElim_Map_it == Factors_To_VarsToElim_Map.end())
			{
				set<string> variables_with_factor_count;
				variables_with_factor_count.insert(variable_to_eliminate);
				Factors_To_VarsToElim_Map.insert(make_pair(number_of_factors, variables_with_factor_count));
			}
			else
			{
				(Factors_To_VarsToElim_Map_it->second).insert(variable_to_eliminate);
			}
		}

		VariablesToEliminate.clear();
		for(map<int, set<string> >::iterator Factors_To_VarsToElim_Map_it = Factors_To_VarsToElim_Map.begin(); Factors_To_VarsToElim_Map_it != Factors_To_VarsToElim_Map.end(); Factors_To_VarsToElim_Map_it++)
		{
			cout << endl << "factor_count = " << Factors_To_VarsToElim_Map_it->first <<"\tvariables = ";
			set<string> variables_with_factor_count = Factors_To_VarsToElim_Map_it->second;
			for(set<string>::iterator variable_it = variables_with_factor_count.begin(); variable_it != variables_with_factor_count.end(); variable_it++)
			{
				cout << *variable_it << ", ";
				VariablesToEliminate.push_back(*variable_it);
			}
		}			
	}
	else
	{
		VariablesToEliminate.clear();
		copy(Final_VariablesToEliminate_Set.begin(), Final_VariablesToEliminate_Set.end(), inserter(VariablesToEliminate, VariablesToEliminate.end()));
	}

	number_of_vars_to_elim = VariablesToEliminate.size();

	#ifdef DETAILED_RECORD_KEEP
	string order_file_name = benchmark_name_without_extension;
	order_file_name += "_monolithic_order.txt";
	FILE* order_fp = fopen(order_file_name.c_str(), "w+");
	assert(order_fp != NULL);
	printList(VariablesToEliminate, order_fp);
	fclose(order_fp);
	#endif
	
	// create the var_name_to_var_index_map and var_index_to_var_name_map
	int var_index = 1;
	for(list<string>::iterator list_it = VariablesToEliminate.begin(); list_it != VariablesToEliminate.end(); list_it++)
	{
		insertIntoVarNameToVarIndexMap(var_name_to_var_index_map, *list_it, var_index);
		insertIntoVarIndexToVarNameMap(var_index_to_var_name_map, var_index, *list_it);

		#ifdef DEBUG_SKOLEM
		cout << "(" << *list_it << ", " << var_index << ") inserted into maps "<< endl;
		#endif	

		var_index++;
	}

	#ifdef DEBUG_SKOLEM
	cout << "number_of_factors = " << number_of_factors << endl;
	cout << "number_of_vars_to_elim = " << number_of_vars_to_elim << endl;
	#endif	

	#ifdef RECORD_KEEP
		string record_file = "skolem_function_generation_details.txt";
		FILE* record_fp = fopen(record_file.c_str(), "a+");
		assert(record_fp != NULL);

		fprintf(record_fp, "F = %d\n", number_of_factors); 
		fprintf(record_fp, "E = %d\n", number_of_vars_to_elim); 

		// print details of original factors
		original_support_size = support.size();	
		fprintf(record_fp, "V = %d\n\n", original_support_size);

		fprintf(record_fp, "N_f = ");

		unsigned long long int total_of_factor_sizes = 0;
		unsigned long long int total_of_abstracted_factor_sizes = 0;
		unsigned long long int total_of_factor_support_sizes = 0;
		unsigned long long int total_of_factor_varstoelim_sizes = 0;
		
		for(map<int, int>::iterator original_factor_sizes_it = original_factor_sizes.begin(); original_factor_sizes_it != original_factor_sizes.end(); original_factor_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_sizes_it->second);
			total_of_factor_sizes = total_of_factor_sizes + original_factor_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "A_f = ");
		for(map<int, int>::iterator abstracted_factor_sizes_it = abstracted_factor_sizes.begin(); abstracted_factor_sizes_it != abstracted_factor_sizes.end(); abstracted_factor_sizes_it++)
		{
			fprintf(record_fp, "%d, ", abstracted_factor_sizes_it->second);
			total_of_abstracted_factor_sizes = total_of_abstracted_factor_sizes + abstracted_factor_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "V_f = ");
		for(map<int, int>::iterator original_factor_support_sizes_it = original_factor_support_sizes.begin(); original_factor_support_sizes_it != original_factor_support_sizes.end(); original_factor_support_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_support_sizes_it->second);
			total_of_factor_support_sizes = total_of_factor_support_sizes + original_factor_support_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		fprintf(record_fp, "E_f = ");
		for(map<int, int>::iterator original_factor_varstoelim_sizes_it = original_factor_varstoelim_sizes.begin(); original_factor_varstoelim_sizes_it != original_factor_varstoelim_sizes.end(); original_factor_varstoelim_sizes_it++)
		{
			fprintf(record_fp, "%d, ", original_factor_varstoelim_sizes_it->second);
			total_of_factor_varstoelim_sizes = total_of_factor_varstoelim_sizes + original_factor_varstoelim_sizes_it->second;
		} 
		fprintf(record_fp, "\n\n");

		number_of_compose_operations_for_variable = 0;
		ComposeTime = 0;

		#ifdef DETAILED_RECORD_KEEP
		fprintf(record_fp, "v\tF_v\tT_v\tN_v\tC_v\tR_T\tS_T\tF_v\tX_v\tO_v\t#O_v\n\n");
		#else
		fprintf(record_fp, "v\tF_v\tT_v\tN_v\tC_v\n\n");
		#endif
		fclose(record_fp);			
		

		string 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", benchmark_type.c_str(), benchmark_name.c_str(), machine.c_str());
		if(disable_factorization)
		{
			if(use_uninterpreted_functions)
			{
				fprintf(plot_fp, "\tmonolithic_hierarchial");
			}
			else
			{
				fprintf(plot_fp, "\tmonolithic_inlined");
			}
		}
		else
		{
			if(use_uninterpreted_functions)
			{
				fprintf(plot_fp, "\tfactorized_hierarchial");
			}
			else
			{
				fprintf(plot_fp, "\tfactorized_inlined");
			}
		}

		fprintf(plot_fp, "\t%d\t%d\t%d\t%d\t%d", number_of_factors, number_of_factors, number_of_vars_to_elim, number_of_vars_to_elim, original_support_size);

		t_Expression* conjunction_of_factors = createAnd(Factors, pub_em);
		assert(conjunction_of_factors != NULL);
		int size_of_conjunction_of_factors = computeSize(conjunction_of_factors);		
		fprintf(plot_fp, "\t%d", size_of_conjunction_of_factors);

		float avg_of_factor_sizes = (float)total_of_factor_sizes/(float)number_of_factors;
		float avg_of_abstracted_factor_sizes = (float)total_of_abstracted_factor_sizes/(float)number_of_factors;
		float avg_of_factor_support_sizes = (float)total_of_factor_support_sizes/(float)number_of_factors;
		float avg_of_factor_varstoelim_sizes = (float)total_of_factor_varstoelim_sizes/(float)number_of_factors;
		fprintf(plot_fp, "\t%f\t%f\t%f\t%f\t-", avg_of_factor_sizes, avg_of_abstracted_factor_sizes, avg_of_factor_support_sizes, avg_of_factor_varstoelim_sizes);

		fclose(plot_fp);

	#endif		
}


void Skolem::monolithicSkolemFunctionGeneratorWithScopeReduction(set<t_Expression*> &Factors, list<string> &VariablesToEliminate)
{
	#ifdef DETAILED_RECORD_KEEP
	unsigned long long int step_ms;
	struct timeval step_start_ms, step_finish_ms;
	gettimeofday (&step_start_ms, NULL); 	
	#endif

	initializeMonolithicSkolemFunctionGeneratorWithScopeReduction(Factors, VariablesToEliminate);

	#ifdef DETAILED_RECORD_KEEP
	gettimeofday (&step_finish_ms, NULL);
   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
	cout << "\ninitializeMonolithicSkolemFunctionGeneratorWithScopeReduction finished in " << step_ms << " milliseconds\n";

	total_time_in_generator_initialization = step_ms;
	#endif

	cout << "\n#factors = " << number_of_factors << "\t#variables_to_eliminate = " << number_of_vars_to_elim << endl;

	// compute the skolem functions, i.e. fill the SkolemFunctions matrix
	for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
	{
		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGeneratorWithScopeReduction\n";
			timed_out = true; // timed_out flag set
			return;
		}
		

		if(maximum_index_to_eliminate != -1) // to stop computation in between
		{
			if(var_to_elim_index > maximum_index_to_eliminate)
			{
				cout << "\nLet us stop here...\n";
				break;
			}			
		}

		#ifdef DEBUG_SKOLEM
		cout << "\ncomputing skolem_function_" << var_to_elim_index << endl;
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\ncomputing skolem_function_" << var_to_elim_index << "\n";
		#endif

		#ifdef RECORD_KEEP
		unsigned long long int duration_ms;
		struct timeval start_ms, finish_ms;
		gettimeofday (&start_ms, NULL); 
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL);
		unsigned long long int total_time_in_compute_size_before_call = total_time_in_compute_size; 	
		#endif

		findFactorsWithVariable(var_to_elim_index);// find the set of factors containing the variable

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGeneratorWithScopeReduction\n";
			timed_out = true; // timed_out flag set
			return;
		}

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\nfindFactorsWithVariable finished in " << step_ms << " milliseconds\n";
		
		cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() << endl;
		FactorFindingTime = step_ms;

		unsigned long long int total_time_in_compute_size_after_call = total_time_in_compute_size;
		unsigned long long int total_time_in_compute_size_in_call = total_time_in_compute_size_after_call - total_time_in_compute_size_before_call;
		cout << "\nTime in findFactorsWithVariable time for computing sizes is " << total_time_in_compute_size_in_call << " milliseconds\n";
		#endif

		#ifdef RECORD_KEEP
		NumberOfFactors = FactorsWithVariable.size();
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nnumber of factors containing the variable = " << FactorsWithVariable.size() <<"\n";
		#endif
		
		t_Expression* skolem_function = computeAlphaCombinedOrGammaCombined(var_to_elim_index);

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGeneratorWithScopeReduction\n";
			timed_out = true; // timed_out flag set
			return;
		}

		assert(skolem_function != NULL);

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\ncomputing skolem function finished in " << step_ms << " milliseconds\n";		
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif

		if(var_to_elim_index != number_of_vars_to_elim) // We need to update the factor matrix
		{
			#ifdef DEBUG_SKOLEM
			cout << "\nupdating factors\n";
			#endif
			updateFactorsUsingGlobalSkolemFunction(var_to_elim_index, skolem_function);
		}

		if(checkTimeOut()) // check for time-out
		{
			cout << "\nWarning!!Time-out inside the function Skolem::monolithicSkolemFunctionGeneratorWithScopeReduction\n";
			timed_out = true; // timed_out flag set
			return;
		}

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\ncomputing next factors finished in " << step_ms << " milliseconds\n";		
		#endif

		#ifdef PRINT_SKOLEM_FUNCTIONS
		string skolem_function_file_name = benchmark_name_without_extension;
		skolem_function_file_name += "_skolem_function";
		writeFormulaToFile(pub_em, skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
		#endif

		// Enter into matrix
		insertIntoOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index, skolem_function, false);

		
		#ifdef DEBUG_SKOLEM
		cout << "\nclearing variable-specific data-structures\n";
		#endif

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_start_ms, NULL); 	
		#endif
		
		clearVariableSpecificDataStructures();

		#ifdef DETAILED_RECORD_KEEP
		gettimeofday (&step_finish_ms, NULL);
	   	step_ms = step_finish_ms.tv_sec * 1000 + step_finish_ms.tv_usec / 1000;
	   	step_ms -= step_start_ms.tv_sec * 1000 + step_start_ms.tv_usec / 1000;
		cout << "\nclearVariableSpecificDataStructures finished in " << step_ms << " milliseconds\n";
		#endif

		#ifdef RECORD_KEEP
		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;
		SkolemFunctionGenTime = duration_ms;

		int skolem_function_size = computeSize(skolem_function);
		SkolemFunctionSize = skolem_function_size;	
   		#endif

		string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
		cout << "\nskolem_function_" << var_to_elim_index << ", i.e., skolem function for " << var_to_elim_name << " computed\n";

		#ifdef RECORD_KEEP
		string record_file = "skolem_function_generation_details.txt";
		FILE* record_fp = fopen(record_file.c_str(), "a+");
		assert(record_fp != NULL);

		sum_of_number_of_factors_containing_variable = sum_of_number_of_factors_containing_variable + NumberOfFactors;
		sum_of_skolem_function_sizes = sum_of_skolem_function_sizes + SkolemFunctionSize;
		total_number_of_compose_operations = total_number_of_compose_operations + number_of_compose_operations_for_variable;
		total_time_in_compose_operations = total_time_in_compose_operations + ComposeTime;
		number_of_variables_eliminated = var_to_elim_index;
		sum_of_numbers_of_affecting_factors = sum_of_numbers_of_affecting_factors + FactorsAffectingSkolemFunction.size();

		#ifdef DETAILED_RECORD_KEEP
		fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\t%llu\t%llu\t", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable, ComposeTime, FactorFindingTime);

		
		for(set<int>::iterator factor_it = PreviousFactorsWithVariable.begin(); factor_it != PreviousFactorsWithVariable.end(); factor_it++)
		{
			fprintf(record_fp, "%d,", *factor_it);			
		}
				
		fprintf(record_fp, "\t");		
		PreviousFactorsWithVariable.clear();

		for(list<int>::iterator size_it = sizes_of_factors_with_variable.begin(); size_it != sizes_of_factors_with_variable.end(); size_it++)
		{
			fprintf(record_fp, "%d,", *size_it);			
		}		

		fprintf(record_fp, "\t");
		sizes_of_factors_with_variable.clear();

		for(list<int>::iterator affect_it = FactorsAffectingSkolemFunction.begin(); affect_it != FactorsAffectingSkolemFunction.end(); affect_it++)
		{
			fprintf(record_fp, "%d,", *affect_it);			
		}
		fprintf(record_fp, "\t");
		fprintf(record_fp, "%d", FactorsAffectingSkolemFunction.size());
			
		FactorsAffectingSkolemFunction.clear();		

		fprintf(record_fp, "\n\n");
		#else
		fprintf(record_fp, "%s\t%d\t%llu\t%d\t%d\n\n", var_to_elim_name.c_str(), NumberOfFactors, SkolemFunctionGenTime, SkolemFunctionSize, number_of_compose_operations_for_variable);
		#endif

		number_of_compose_operations_for_variable = 0;
		ComposeTime = 0;
		
		fclose(record_fp);
		#endif						
	}

	

	if(use_uninterpreted_functions && false) // write the AbstractedTounabstractedFunctionsMap
	{
		string final_qe_result_file = benchmark_name_without_extension;
		final_qe_result_file += "_output.v";
		writeAbstractedTounabstractedFunctionsMap(pub_em, AbstractedTounabstractedFunctionsMap, final_qe_result_file);
	}

	if(perform_reverse_substitution)
	{
		performReverseSubstitutionOfSkolemFunctions();
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			#ifdef RECORD_KEEP
			int final_skolem_function_size = computeSize(final_skolem_function);
			skolem_function_sizes_after_reverse_substitution.push_back(final_skolem_function_size);
			sum_of_skolem_function_sizes_after_reverse_substitution = sum_of_skolem_function_sizes_after_reverse_substitution + final_skolem_function_size;
			#endif

			#ifdef PRINT_SKOLEM_FUNCTIONS
			string skolem_function_file_name = benchmark_name_without_extension;
			skolem_function_file_name += "_skolem_function_after_reverse_substitution";
			writeFormulaToFile(pub_em, final_skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
			#endif
		}
	}

	if(match_outputs_of_monolithic_and_factorized)
	{
		t_Expression* ConjunctionOfFactors = createAnd(Factors, pub_em);
		assert(ConjunctionOfFactors != NULL);
		t_Expression* ConjunctionOfFactors_with_var_substituted = ConjunctionOfFactors;
		
		for(int var_to_elim_index = 1; var_to_elim_index <= number_of_vars_to_elim; var_to_elim_index++)
		{
			t_Expression* final_skolem_function;
			final_skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index);
			assert(final_skolem_function != NULL);	

			string var_to_elim_name = searchVarIndexToVarNameMap(var_index_to_var_name_map, var_to_elim_index);
			
			t_HashTable<unsigned long, t_Expression*> cache;
			ConjunctionOfFactors_with_var_substituted = pub_em->ReplaceLeafByExpression(ConjunctionOfFactors_with_var_substituted, var_to_elim_name, final_skolem_function, cache, false, 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);

			assert(ConjunctionOfFactors_with_var_substituted != NULL);			

		}//for ends here
	
		result_of_qe_using_monolithic = ConjunctionOfFactors_with_var_substituted;		
	}

}




void Skolem::updateFactorsUsingGlobalSkolemFunction(int var_to_elim_index, t_Expression* skolem_function)
{
	assert(var_to_elim_index < number_of_vars_to_elim);
	assert(skolem_function != NULL);

	t_HashTable<unsigned long, t_Expression*> global_skolem_function_substitution_cache;

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// obtain the existing factor
		t_Expression* previous_factor;
		previous_factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(previous_factor != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, previous_factor, "factor", ".v", var_to_elim_index, factor_index);	
		#endif

		t_Expression* factor;
		if(share_cache_in_global_skolem_function_substitution_in_scope_reduced_monolithic_mode)
		{
			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, skolem_function, global_skolem_function_substitution_cache);
		}
		else
		{
			factor = replaceVariableByFormula(previous_factor, var_to_elim_index, skolem_function);
		}
		assert(factor != NULL);
		
		if(use_uninterpreted_functions) // abstract the factor
		{
			set<string> support_factor;
			computeSupport(factor, support_factor);
			string name_of_function = "factor";
			t_Expression* abstracted_factor = createAbstraction(name_of_function, var_to_elim_index+1, factor_index, support_factor, pub_em);
			assert(abstracted_factor != NULL);
			AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_factor, factor));
			factor = abstracted_factor;
		}


		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index+1, factor_index);	
		#endif

		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, factor, true);

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		int size_of_new_factor = computeSize(factor);
		cout << "\nfactor_" << factor_index << " updated to formula of size " << size_of_new_factor << endl;
		#endif		
	}	
}



void Skolem::findTopFactorsWithVariable(int var_to_elim_index)
{
	#ifdef DEBUG_SKOLEM
	cout << "\nfinding top factors with variable_" << var_to_elim_index << endl;
	#endif

	FactorsWithVariable.clear();

	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// We need to consider only the top-factors
		// containing the variable to eliminate
		if(top_factors_considered.find(factor_index) != top_factors_considered.end())
		{
			// this factor cannot be a top-factor for the variable to eliminate,
			// since it is already a top-factor for some other variable.
			continue;
		}
		
		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index, factor_index);	
		#endif

		#ifdef DETAILED_RECORD_KEEP
		//fprintf(support_fp, "%d,", computeSize(factor));	
		#endif
		
		if(!formulaFreeOfVariable(factor, var_to_elim_index))
		{
			FactorsWithVariable.insert(factor_index);

			top_factors_considered.insert(factor_index);				

			#ifdef DETAILED_RECORD_KEEP
			int factor_size = computeSize(factor);
			sizes_of_factors_with_variable.push_back(factor_size);
			sizes_of_factors_affecting_variable.push_back(factor_size);
			#endif

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nfactor_ " << factor_index << " of size " << factor_size << " encountered with variable_" << var_to_elim_index << endl;
			#endif
		}
	}

	#ifdef DETAILED_RECORD_KEEP
	/*
	fprintf(support_fp, "\nsizes of factors with variable : ");	
	for(list<int>::iterator size_it = sizes_of_factors_with_variable.begin(); size_it != sizes_of_factors_with_variable.end(); size_it++)
	{
		fprintf(support_fp, "%d,", *size_it);			
	}
	fclose(support_fp);*/
	#endif

	#ifdef DEBUG_SKOLEM
	showSet(FactorsWithVariable, "FactorsWithVariable");
	#endif
}



void Skolem::findTopFactorsWithVariable(string &var_to_elim, set<int> &factors_with_var_to_elim)
{
	factors_with_var_to_elim.clear();

	for(int factor_index = 1; factor_index <= number_of_factors; factor_index++)
	{
		// We need to consider only the top-factors
		// containing the variable to eliminate
		if(top_factors_considered.find(factor_index) != top_factors_considered.end())
		{
			// this factor cannot be a top-factor for the variable to eliminate,
			// since it is already a top-factor for some other variable.
			continue;
		}

		t_Expression* factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);

		if(!formulaFreeOfVariable(factor, var_to_elim))
		{
			factors_with_var_to_elim.insert(factor_index);	
		}
	}
}


t_Expression* Skolem::computeDeltaCombined(int var_to_elim_index, t_Expression* local_skolem_function)
{
	// Let us compute delta_combined_{var_to_elim_index}
	// Suppose i = var_to_elim_index
	// i.e. we need to compute delta_combined_{i}

	t_Expression* delta_combined;
	t_Expression* conjunction_of_factors;		

	// delta_combined_{i} = \neg(conjunction of factors with var_to_elim_index with 
	// 			var_to_elim_index substituted by local_skolem_function)
	// 			i.e. \neg \exists var_to_elim_index. (conjunction of factors with var_to_elim_index)
	set<t_Expression*> conjunction_of_factors_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing delta_combined_" << var_to_elim_index << endl;
	#endif

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// obtain the factor
		t_Expression* factor;
		factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);

		conjunction_of_factors_components.insert(factor);
	}	

	if(conjunction_of_factors_components.size() == 0) // no factor with var_to_elim_index
	{
		delta_combined = createTrue(pub_em); // by defn., delta_combined is false; we are actually returning \neg of delta_combined here
		assert(delta_combined != NULL);
	}
	else
	{
		conjunction_of_factors = createAnd(conjunction_of_factors_components, pub_em);
		assert(conjunction_of_factors != NULL);

		assert(local_skolem_function != NULL);
		t_Expression* conjunction_of_factors_var_to_elim_index_eliminated = replaceVariableByFormula(conjunction_of_factors, var_to_elim_index, local_skolem_function);
		assert(conjunction_of_factors_var_to_elim_index_eliminated != NULL);

		delta_combined = conjunction_of_factors_var_to_elim_index_eliminated;
		assert(delta_combined != NULL);
	}		

	if(use_uninterpreted_functions) // abstract the delta_combined
	{
		set<string> support_delta_combined;
		computeSupport(delta_combined, support_delta_combined);
		string name_of_function = "delta_combined";
		t_Expression* abstracted_delta_combined = createAbstraction(name_of_function, var_to_elim_index, 0, support_delta_combined, pub_em);
		assert(abstracted_delta_combined != NULL);
		AbstractedTounabstractedFunctionsMap.insert(make_pair(abstracted_delta_combined, delta_combined));
		delta_combined = abstracted_delta_combined;
	}

	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, delta_combined, "delta_combined", ".v", var_to_elim_index, 0);	
	#endif

	return delta_combined;	
} // function ends here



void Skolem::computeDeltaCombined(int var_to_elim_index, t_Expression* local_skolem_function, map<int, t_Expression*> &factor_wise_delta_combined)
{
	// Let us compute delta_combined_{var_to_elim_index}
	// Suppose i = var_to_elim_index
	// i.e. we need to compute delta_combined_{i} as individual factors

	assert(local_skolem_function != NULL);

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing delta_combined_" << var_to_elim_index << endl;
	#endif

	t_HashTable<unsigned long, t_Expression*> skolem_substitution_cache;

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// obtain the factor
		t_Expression* factor;
		factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(factor != NULL);		
		
		t_Expression* factor_with_var_to_elim_index_eliminated;
		if(share_cache_in_global_skolem_function_substitution_in_scope_reduced_factorized_mode)
		{
			factor_with_var_to_elim_index_eliminated = replaceVariableByFormula(factor, var_to_elim_index, local_skolem_function, skolem_substitution_cache);
		}
		else
		{
			factor_with_var_to_elim_index_eliminated = replaceVariableByFormula(factor, var_to_elim_index, local_skolem_function);
		}
		assert(factor_with_var_to_elim_index_eliminated != NULL);

		factor_wise_delta_combined.insert(make_pair(factor_index, factor_with_var_to_elim_index_eliminated));

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\n######size of factor_wise_delta_combined_" << factor_index << " is: " << computeSize(factor_with_var_to_elim_index_eliminated) << endl;
		#endif
		
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor_with_var_to_elim_index_eliminated, "delta_combined", ".v", var_to_elim_index, factor_index);	
		#endif
	}		
	
} // function ends here


t_Expression* Skolem::computeDeltaCombinedWithSkolemFunctionsSubstitutedKeepingFactorsIndividual(int delta_combined_index, int subst_index)
{
	// step-1: let's take the factor-wise delta-combined, replace variables from delta_combined_index to subst_index
	// by their skolem functions
	
	// sanity checks
	assert(delta_combined_index >= 1);
	assert(subst_index >= delta_combined_index);

	// obtain the existing factor-wise delta-combined with substitutions
	map<int, t_Expression*> factor_wise_delta_combined_with_substitutions;
	map<int, map<int, t_Expression*> >::iterator FactorWiseDeltaCombinedMatrix_it = FactorWiseDeltaCombinedMatrix.find(delta_combined_index);
	assert(FactorWiseDeltaCombinedMatrix_it != FactorWiseDeltaCombinedMatrix.end());
	factor_wise_delta_combined_with_substitutions = FactorWiseDeltaCombinedMatrix_it->second;
	
	int index_upto_which_already_substituted = searchOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, delta_combined_index);
	assert(index_upto_which_already_substituted >= delta_combined_index);	

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nindex_upto_which_already_substituted = " << index_upto_which_already_substituted << endl;
	int number_of_variables_substituted = 0;
	#endif

	t_HashTable<unsigned long, t_Expression*> skolem_substitution_cache;

	for(int current_subst_index = index_upto_which_already_substituted + 1; current_subst_index <= subst_index; current_subst_index++)
	{
		assert(current_subst_index > delta_combined_index);

		t_Expression* skolem_function;
		skolem_function = searchOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, current_subst_index);
		assert(skolem_function != NULL);

		#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
		cout << "\nReplacing variable_" << current_subst_index << " by its skolem function\n";
		number_of_variables_substituted++;
		#endif

		for(map<int, t_Expression*>::iterator factor_wise_delta_combined_it = factor_wise_delta_combined_with_substitutions.begin(); factor_wise_delta_combined_it != factor_wise_delta_combined_with_substitutions.end();  factor_wise_delta_combined_it++)
		{
			t_Expression* delta_combined_with_substitutions = factor_wise_delta_combined_it->second;
			assert(delta_combined_with_substitutions != NULL);

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nsize of delta_combined_with_substitutions is: " << computeSize(delta_combined_with_substitutions) << endl;
			cout << "\nsize of skolem_function is: " << computeSize(skolem_function) << endl;
			#endif

			t_Expression* delta_combined_with_substitutions_new;

			if(formulaFreeOfVariable(delta_combined_with_substitutions, current_subst_index))
			{
				delta_combined_with_substitutions_new = delta_combined_with_substitutions;
			}
			else
			{
				if(share_cache_in_global_skolem_function_substitution_in_scope_reduced_factorized_mode)
				{
					delta_combined_with_substitutions_new = replaceVariableByFormula(delta_combined_with_substitutions, current_subst_index, skolem_function, skolem_substitution_cache);
				}
				else
				{
					delta_combined_with_substitutions_new = replaceVariableByFormula(delta_combined_with_substitutions, current_subst_index, skolem_function);
				}
			}
			assert(delta_combined_with_substitutions_new != NULL);

			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\nsize of result of replaceVariableByFormula is: " << computeSize(delta_combined_with_substitutions_new) << endl;
			#endif

			factor_wise_delta_combined_it->second = delta_combined_with_substitutions_new;
		}

		skolem_substitution_cache.clear();
	}

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nnumber of variables substituted = " << number_of_variables_substituted << endl;
	#endif
	
	FactorWiseDeltaCombinedMatrix[delta_combined_index] = factor_wise_delta_combined_with_substitutions;	
	insertIntoOneDimensionalMatrix(DeltaCombinedSubstMatrix, number_of_vars_to_elim, delta_combined_index, subst_index, true);

	// step-2: let's take the present factor-wise delta-combined, and compute the conjunctions of factors with var_to_elim_index	

	t_Expression* delta_combined_conjunction;	
	set<t_Expression*> delta_combined_conjunction_components;
	int var_to_elim_index =  subst_index + 1;	

	for(map<int, t_Expression*>::iterator factor_wise_delta_combined_it = factor_wise_delta_combined_with_substitutions.begin(); factor_wise_delta_combined_it != factor_wise_delta_combined_with_substitutions.end();  factor_wise_delta_combined_it++)
	{
		t_Expression* delta_combined_with_substitutions = factor_wise_delta_combined_it->second;
		int size_of_factor_affecting_skolem_function = computeSize(delta_combined_with_substitutions);
		
		if(!formulaFreeOfVariable(delta_combined_with_substitutions, var_to_elim_index))
		{
			#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
			cout << "\n****:size of delta_combined_with_substitutions_" << factor_wise_delta_combined_it->first << " is: " << size_of_factor_affecting_skolem_function << endl;
			#endif		

			delta_combined_conjunction_components.insert(delta_combined_with_substitutions);

			FactorsAffectingSkolemFunction.push_back(factor_wise_delta_combined_it->first);
			sizes_of_factors_affecting_variable.push_back(size_of_factor_affecting_skolem_function);
		}
	}	

	if(delta_combined_conjunction_components.size() == 0) // no factor with var_to_elim_index
	{
		delta_combined_conjunction = createTrue(pub_em); // by defn., delta_combined is false; but we are working on \neg here
		assert(delta_combined_conjunction != NULL);
	}
	else
	{
		delta_combined_conjunction = createAnd(delta_combined_conjunction_components, pub_em);
		assert(delta_combined_conjunction != NULL);
	}

	sizes_of_conflict_conjuncts_affecting_variable.push_back(computeSize(delta_combined_conjunction));
	
	return delta_combined_conjunction;
}



int Skolem::computeCostOfFactorWiseDeltaCombined(map<int, t_Expression*>& factor_wise_delta_combined)
{
	int delta_cost;
	bool find_exact_size = true;
	if(find_exact_size)
	{
		t_Expression* delta_combined_conjunction;	
		set<t_Expression*> delta_combined_conjunction_components;
		
		for(map<int, t_Expression*>::iterator factor_wise_delta_combined_it = factor_wise_delta_combined.begin(); factor_wise_delta_combined_it != 	factor_wise_delta_combined.end(); factor_wise_delta_combined_it++)
		{
			delta_combined_conjunction_components.insert(factor_wise_delta_combined_it->second);
		}
		
		if(delta_combined_conjunction_components.size() == 0) // no factor with var_to_elim_index
		{
			delta_cost = 1; // delta_combined is true in this case
		}
		else
		{
			delta_combined_conjunction = createAnd(delta_combined_conjunction_components, pub_em);
			assert(delta_combined_conjunction != NULL);
			delta_cost = computeSize(delta_combined_conjunction);
		}
	}
	else
	{
		delta_cost = 0;
		for(map<int, t_Expression*>::iterator factor_wise_delta_combined_it = factor_wise_delta_combined.begin(); factor_wise_delta_combined_it != 	factor_wise_delta_combined.end(); factor_wise_delta_combined_it++)
		{
			delta_cost = delta_cost + computeSize(factor_wise_delta_combined_it->second);
		}
	}

	return delta_cost;
	
}

					

t_Expression* Skolem::computeSkolemFunctionUsingBadSet(int var_to_elim_index, t_Expression* &cofactor_one_of_bad_set)
{
	// skolem function = (conjunction of co-factor-1's of factors with var_to_elim_index) \wedge (cofactor-1 of \neg bad_set)

	#ifdef RECORD_KEEP
	unsigned long long int alpha_duration_ms, delta_duration_ms;
	struct timeval start_ms, finish_ms;
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&start_ms, NULL); 
	#endif

	// computing alpha_combined_or_gamma_combined{var_to_elim_index}
	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing alpha_combined_or_gamma_combined_" << var_to_elim_index << "\n";
	#endif
		
	t_Expression* alpha_combined_or_gamma_combined = computeAlphaCombinedOrGammaCombined(var_to_elim_index);
	assert(alpha_combined_or_gamma_combined != NULL);

	if(checkTimeOut()) // check for time-out
	{
		cout << "\nWarning!!Time-out inside the function Skolem::computeSkolemFunction\n";
		timed_out = true; // timed_out flag set
		return NULL;
	}

	#ifdef DEBUG_SKOLEM
	cout << "\nalpha_combined_or_gamma_combined_" << var_to_elim_index << " computed\n";
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&finish_ms, NULL);
	alpha_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
	alpha_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
	AlphaCombGenTime = alpha_duration_ms;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	cout << "\ncomputeAlphaCombinedOrGammaCombined finished in " << alpha_duration_ms << "milli seconds\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nsize of alpha_combined_or_gamma_combined is " << computeSize(alpha_combined_or_gamma_combined) << endl;
	#endif

	#ifdef RECORD_KEEP
	AlphaPartSize = computeSize(alpha_combined_or_gamma_combined);
	#endif
	
	// computing cofactor-1 of bad part
	#ifdef RECORD_KEEP
	gettimeofday (&start_ms, NULL); 
	#endif

	// computing bad_part_{var_to_elim_index}
	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing bad_part_" << var_to_elim_index << "\n";
	#endif

	t_Expression* bad_part;
	if(!formulaFreeOfVariable(bad_set, var_to_elim_index)) 
	{
		// replace var_to_elim_index in bad_set by one
		t_Expression* cofactor_one;
		if(reuse_same_cache_for_computations)
		{
			cofactor_one = replaceVariableByConstant(bad_set, var_to_elim_index, 1, pub_cofactor_one_cache);
		}
		else
		{
			cofactor_one = replaceVariableByConstant(bad_set, var_to_elim_index, 1);
		}	
		assert(cofactor_one != NULL);

		cofactor_one_of_bad_set = cofactor_one;
		bad_part = createNot(cofactor_one, pub_em);
		assert(bad_part != NULL);
	}
	else
	{
		cofactor_one_of_bad_set = bad_set;
		bad_part = createTrue(pub_em);
		assert(bad_part != NULL);
		
	}	

	#ifdef DEBUG_SKOLEM
	cout << "\nbad_part computed\n";
	writeFormulaToFile(pub_em, bad_part, "bad_part", ".v", var_to_elim_index, 0);
	#endif

	#ifdef RECORD_KEEP
	gettimeofday (&finish_ms, NULL);
	delta_duration_ms = finish_ms.tv_sec * 1000 + finish_ms.tv_usec / 1000;
	delta_duration_ms -= start_ms.tv_sec * 1000 + start_ms.tv_usec / 1000;
	DeltaPartGenTime = delta_duration_ms;
	#endif

	#ifdef DETAILED_RECORD_KEEP
	cout << "\ncomputing delta part finished in " << delta_duration_ms << "milli seconds\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nsize of bad_part is " << computeSize(bad_part) << endl;
	#endif

	#ifdef RECORD_KEEP
	DeltaPartSize = computeSize(bad_part);
	#endif
	
        //computing skolem_function

	t_Expression* skolem_function;	
	// skolem_function = alpha_combined_or_gamma_combined \wedge bad_part
	skolem_function = createAnd(alpha_combined_or_gamma_combined, bad_part, pub_em);	
	assert(skolem_function != NULL);

	#ifdef DEBUG_SKOLEM
	cout << "\nskolem_function computed\n";	
	#endif

	#ifdef PRINT_SKOLEM_FUNCTIONS
	string skolem_function_file_name = benchmark_name_without_extension;
	skolem_function_file_name += "_skolem_function";
	writeFormulaToFile(pub_em, skolem_function, skolem_function_file_name, ".v", var_to_elim_index, 0);
	#endif

	// Enter into matrix
	insertIntoOneDimensionalMatrix(SkolemFunctions, number_of_vars_to_elim, var_to_elim_index, skolem_function, false);
		
	return skolem_function;		
}




void Skolem::updateBadSet(int var_to_elim_index, t_Expression* cofactor_one_of_bad_set)
{
	// bad_set = (disjunction of alpha's of factors with var_to_elim_index \vee co-factor-0 of bad_set)\wedge
	//	     (disjunction of beta's of factors with var_to_elim_index \vee co-factor-1 of bad_set)

	#ifdef DEBUG_SKOLEM
	cout << "\nupdating bad_set\n";
	#endif

	set<t_Expression*> alpha_components; 
	set<t_Expression*> beta_components; 
		
	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index
		// Get alpha_i_j and beta_i_j

		t_Expression* alpha_i_j;
		alpha_i_j = computeAlpha(var_to_elim_index, factor_index); 
		assert(alpha_i_j != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, alpha_i_j, "alpha", ".v", var_to_elim_index, factor_index);		
		cout << "\nalpha_" << var_to_elim_index << "_" << factor_index << " obtained\n";			
		#endif

		t_Expression* beta_i_j;
		beta_i_j = computeBeta(var_to_elim_index, factor_index); 
		assert(beta_i_j != NULL);	
	
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, beta_i_j, "beta", ".v", var_to_elim_index, factor_index);		
		cout << "\nbeta_" << var_to_elim_index << "_" << factor_index << " obtained\n";			
		#endif

				
		alpha_components.insert(alpha_i_j);
		beta_components.insert(beta_i_j);
						
	}// for each factor ends here
	
	if(checkTimeOut()) // check for time-out
	{
		cout << "\nWarning!!Time-out inside the function Skolem::updateBadSet\n";
		timed_out = true; // timed_out flag set
		return;
	}

	if(!formulaFreeOfVariable(bad_set, var_to_elim_index)) 
	{
		// replace var_to_elim_index in bad_set by zero
		// we already have cofactor_one
		t_Expression* cofactor_zero;
		if(reuse_same_cache_for_computations)
		{
			cofactor_zero = replaceVariableByConstant(bad_set, var_to_elim_index, 0, pub_cofactor_zero_cache);
		}
		else
		{
			cofactor_zero = replaceVariableByConstant(bad_set, var_to_elim_index, 0);
		}	
		assert(cofactor_zero != NULL);
		alpha_components.insert(cofactor_zero);
		
		beta_components.insert(cofactor_one_of_bad_set);
	}
	else
	{
		alpha_components.insert(bad_set);		
		beta_components.insert(bad_set);
		
	}

	t_Expression* alpha_part;
	alpha_part = createOr(alpha_components, pub_em);
	assert(alpha_part != NULL);

		
	t_Expression* beta_part;
	beta_part = createOr(beta_components, pub_em);
	assert(beta_part != NULL);

	bad_set = createAnd(alpha_part, beta_part, pub_em);	
	assert(bad_set != NULL);

	#ifdef DEBUG_SKOLEM
	cout << "\nbad_set computed\n";	
	writeFormulaToFile(pub_em, bad_set, "bad_set", ".v", var_to_elim_index, 0);	
	#endif

	#ifdef RECORD_KEEP
	DeltaCombinedSize = computeSize(bad_set);
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\nsize of bad_set is " << DeltaCombinedSize << endl;
	#endif

	if(checkTimeOut()) // check for time-out
	{
		cout << "\nWarning!!Time-out inside the function Skolem::updateBadSet\n";
		timed_out = true; // timed_out flag set
		return;
	}

}



void Skolem::updateFactorsWithoutComposition(int var_to_elim_index)
{
	assert(var_to_elim_index < number_of_vars_to_elim);

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// obtain the existing factor
		t_Expression* previous_factor;
		previous_factor = searchOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index);
		assert(previous_factor != NULL);

		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, previous_factor, "factor", ".v", var_to_elim_index, factor_index);	
		#endif

		t_Expression* delta;
		delta = computeDelta(var_to_elim_index, factor_index); 
		assert(delta != NULL);

		t_Expression* factor = createNot(delta, pub_em);
		assert(factor != NULL);
		
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index+1, factor_index);	
		#endif

		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, factor, true);
	}	
}




void Skolem::updateFactorsUsingQuantifierEliminatedResult(int var_to_elim_index, t_Expression* quantifier_eliminated_result)
{
	assert(var_to_elim_index < number_of_vars_to_elim);

	int factor_count = 1;

	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		t_Expression* factor;		
		if(factor_count == FactorsWithVariable.size())
		{
			factor = quantifier_eliminated_result;
		}
		else
		{
			factor = createTrue(pub_em);
		}
		assert(factor != NULL);
		
		#ifdef DEBUG_SKOLEM
		writeFormulaToFile(pub_em, factor, "factor", ".v", var_to_elim_index+1, factor_index);	
		#endif

		insertIntoOneDimensionalMatrix(FactorMatrix, number_of_factors, factor_index, factor, true);

		factor_count++;
	}	
}



t_Expression* Skolem::computeQuantifierEliminatedResultUsingCofactors(int var_to_elim_index)
{
	// We need to compute (conjunction of co-factor-1_i_j's) \vee (conjunction of co-factor-0_i_j's)
	set<t_Expression*> cofactor_one_components; 
	set<t_Expression*> cofactor_zero_components; 

	#ifdef DEBUG_SKOLEM
	cout << "\ncomputing components of QuantifierEliminatedResult\n";
	#endif

	#ifdef PRINT_VERY_DETAILED_RECORDS_ON_SCREEN
	cout << "\ncomputing components of QuantifierEliminatedResult\n";
	#endif


	for(set<int>::iterator factor_it = FactorsWithVariable.begin(); factor_it != FactorsWithVariable.end(); factor_it++)
	{
		int factor_index = *factor_it;

		#ifdef DEBUG_SKOLEM
		cout << "\nfactor_index = " << factor_index << endl;
		#endif

		// Suppose j = factor_index

		t_Expression* cofactor_1_i_j;
		cofactor_1_i_j = computeCofactorOne(var_to_elim_index, factor_index); 
		assert(cofactor_1_i_j != NULL);	
		cofactor_one_components.insert(cofactor_1_i_j);	

		t_Expression* cofactor_0_i_j;
		cofactor_0_i_j = computeCofactorZero(var_to_elim_index, factor_index); 
		assert(cofactor_0_i_j != NULL);	
		cofactor_zero_components.insert(cofactor_0_i_j);
						
	}// for each factor ends here

	t_Expression* cofactor_one;				
	if(cofactor_one_components.size() == 0) 
	{
		cofactor_one = createTrue(pub_em); 
		assert(cofactor_one != NULL);
	}
	else
	{
		cofactor_one = createAnd(cofactor_one_components, pub_em);
		assert(cofactor_one != NULL);
	}

	t_Expression* cofactor_zero;				
	if(cofactor_zero_components.size() == 0) 
	{
		cofactor_zero = createTrue(pub_em); 
		assert(cofactor_zero != NULL);
	}
	else
	{
		cofactor_zero = createAnd(cofactor_zero_components, pub_em);
		assert(cofactor_zero != NULL);
	}

	t_Expression* QuantifierEliminatedResult = createOr(cofactor_one, cofactor_zero, pub_em);
	assert(QuantifierEliminatedResult != NULL);

	#ifdef DEBUG_SKOLEM
	writeFormulaToFile(pub_em, QuantifierEliminatedResult, "QuantifierEliminatedResult", ".v", var_to_elim_index, 0);				
	#endif

	return QuantifierEliminatedResult;	
}