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

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

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

Monniaux.cpp and Monniaux.h contains the code for the algorithm 
Monniaux described in the paper "Extending Quantifier Elimination
to Linear Inequalities on Bit-Vectors" in TACAS 2013.  

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

#include <iostream>
#include <exception>
#include "Monniaux.h"


using namespace std;

/**********************************************************************/
/*              Constructor, destructor                               */
/**********************************************************************/



t_Monniaux::t_Monniaux(t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm)
{
	if (t_monniaux_instance != NULL) 
	{
    		cerr << "Error in t_Monniaux::t_Monniaux: Attempt to create multiple copies of t_Monniaux" << endl;
    		cerr << "There should be only one copy of t_Monniaux" << endl;
    		assert(0);
  	}

	pvt_VariableList = VariableList;
	pvt_WidthTable = WidthTable;
	pvt_use_bvlibrary_for_layer2_computations = use_bvlibrary_for_layer2_computations;
	pvt_em = em;
	pvt_bvm = bvm;

	t_Logger* logManager = t_Logger::getInstance();
	pvt_logFile = new ofstream();
    	pvt_logFile->open("monniaux.log");
    	logManager->LOG("monniaux started", pvt_logFile, c_DebugLevelVerbosity);
}

t_Monniaux::~t_Monniaux()
{
      	t_Logger* logManager = t_Logger::getInstance();
	logManager->LOG("monniaux is deleted", pvt_logFile, c_DebugLevelVerbosity);
	pvt_logFile->close();
}       

t_Monniaux* t_Monniaux::t_monniaux_instance = NULL;

t_Monniaux* t_Monniaux::getInstance(t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm)
{
	if(t_monniaux_instance == NULL)
	{
		try
		{
			t_monniaux_instance = new t_Monniaux(VariableList, WidthTable, use_bvlibrary_for_layer2_computations, em, bvm);
		}
		catch(bad_alloc&) 
		{
		      cerr << "Memory allocation failure in t_Monniaux::getInstance" << endl;
      		      assert(0);
    		}
  	}
	return t_monniaux_instance;
}

/**********************************************************************/
/*             Functions for implementing Monniaux                    */
/**********************************************************************/


// Given an expression node F representing a Boolean combination of LMES, LMDs, and LMIs, 
// this function applies the algorithm Monniaux in TACAS'13 paper to compute \exists variables. F
// Returns NULL in case of errors; result of \exists variables. F otherwise.  
t_Expression* 
t_Monniaux::Monniaux(t_Expression* F, const vector<string> &variables, t_solver solver)
{
	if(F == NULL)
	{
		t_Logger* logManager = t_Logger::getInstance();
		logManager->LOG("ERROR!! F is NULL in function t_Monniaux::Monniaux", pvt_logFile, c_RunLevelVerbosity);
		return NULL;
	}
	else // F is not NULL
	{
		string FLabel = pvt_em->getLabelOfExpression(F);
		// only Boolean combination allowed
		assert("logand" == FLabel || "logor" == FLabel || "lognot" == FLabel);

		// check in hash table first
		t_Expression* ResultFromHashTable = checkIn_Monniaux_HashTable(F, variables);

		if(ResultFromHashTable != NULL) //hash table hit
		{
			// for debugging
			cout<<"\nHash hit in Monniaux\n";
			// for debugging ends here

			return ResultFromHashTable;
		}
		else //hash table miss
		{
			// for debugging
			cout<<"\nHash miss in Monniaux\n";
			// for debugging ends here

			string and_name = "logand";
			string or_name = "logor";
			string not_name = "lognot";
			
			t_Expression* O; // O stores the final result
			t_Expression* H;
			map<string, string> model;
			bool H_is_sat;

			H = F;
			O = getFalse(pvt_em); // O := false
			assert(O != NULL);
			
			// check if H is sat; get model if sat
			bool solving_done = obtainModelOfFormula(H, H_is_sat, solver, model, pvt_em); 
			assert(solving_done);

			while(H_is_sat)
			{
				// for debugging
				cout<<"\nIteration of Monniaux loop starting\n";
				// for debugging ends here
				set<t_Expression*> CoreConstraints;
				// model |= H; hence model |= F
				// CoreConstraints = subset of LMCs of F sufficient to lead to model |= F
				// Generalize combines Generalize1 and Generalize2 of TACAS'13 paper
				bool generalization_done = Generalize(F, model, CoreConstraints);
				assert(generalization_done);

				// for debugging
				displaySetOfExpressionsOnScreen("CoreConstraints", CoreConstraints, pvt_em);
				// for debugging ends here

				t_Expression* ConjunctionOfCoreConstraints = obtainKandNodeFromASetOfConstraints(CoreConstraints, pvt_em, pvt_bvm, pvt_VariableList, pvt_WidthTable);
				assert(ConjunctionOfCoreConstraints != NULL);

				// for debugging
				pvt_em->printExpressionToFileAsDAG("ConjunctionOfCoreConstraints", ConjunctionOfCoreConstraints, cout);
				// for debugging ends here

				t_Expression* Pi;				
				// for debugging
				cout<<"\nProject is called\n";
				// for debugging ends here
				t_Project* Project_Instance = t_Project::getInstance(pvt_VariableList, pvt_WidthTable, pvt_use_bvlibrary_for_layer2_computations, pvt_em, pvt_bvm);
				assert(Project_Instance != NULL);
				Pi = Project_Instance->Project(ConjunctionOfCoreConstraints, variables);
				assert(Pi != NULL);
				assert(!isFalse(Pi, pvt_em)); // Pi cannot be false
				// for debugging
				pvt_em->printExpressionToFileAsDAG("Pi", Pi, cout);
				// for debugging ends here
				
				assert(!isTrue(O, pvt_em)); // O cannot be true

				// O := O \vee Pi
				if(isTrue(Pi, pvt_em))  // Pi = true; hence O := true
				{
					O = getTrue(pvt_em);
					break; // no need to continue now!!
				}
				else if(isFalse(O, pvt_em))  // O = false; hence O := Pi
				{
					O = Pi;
				}
				else
				{
					O = CreateNode(or_name, O, Pi, pvt_em); 
				}
				assert(O != NULL);
				// for debugging
				pvt_em->printExpressionToFileAsDAG("O", O, cout);
				// for debugging ends here
				
				// NegPi := \neg Pi
				t_Expression* NegPi;
				NegPi = CreateNode(not_name, Pi, pvt_em); 
				assert(NegPi != NULL);
				// for debugging
				pvt_em->printExpressionToFileAsDAG("NegPi", NegPi, cout);
				// for debugging ends here

				// H := H \wedge \neg Pi
				assert(!isFalse(H, pvt_em)); // H cannot be false
				assert(!isTrue(H, pvt_em)); // H cannot be true

				H = CreateNode(and_name, H, NegPi, pvt_em); 
				assert(H != NULL);
				// for debugging
				pvt_em->printExpressionToFileAsDAG("H", H, cout);
				// for debugging ends here

				// find the next model of H
				solving_done = obtainModelOfFormula(H, H_is_sat, solver, model, pvt_em); 
				assert(solving_done);

			}// while loop ends here

			// O = \exists variables. F here

			// update the hash table
			bool HashTable_Updated = update_Monniaux_HashTable(F, variables, O);
			if(!HashTable_Updated)
			{
				t_Logger* logManager = t_Logger::getInstance();
				logManager->LOG("ERROR!! Hash table insertion failure in function t_Monniaux::Monniaux", pvt_logFile, c_RunLevelVerbosity);
				return NULL;
			}
			else
			{
				return O;
			}// else of if(!HashTable_Updated) ends here

		}// hash table miss ends here

	}// F is not NULL ends here

}// function ends here

				
				
// Checks if (F, variables) is existing in pvt_Monniaux_HashTable. 
// Returns the result if existing; NULL otherwise.  
t_Expression*
t_Monniaux::checkIn_Monniaux_HashTable(t_Expression* F, const vector<string> &variables)
{
	assert(F != NULL);	

	// key = address of input kand node + variables to be eliminated
	string key = toString(F);

	int var_size = variables.size();
	for(int i = 0; i < var_size; i++)
	{		
		key += variables[i];	
	}

	t_HTStatusValue <t_Expression*> result_search = pvt_Monniaux_HashTable.hashtable_search(key);

	if(result_search.success())
	{
		return result_search.getValue();
	}
	else
	{
		return NULL;
	}
}//function ends here



// Updates pvt_Monniaux_HashTable with (F, variables) ---> O. 
// Returns false in case of errors; true otherwise. 
bool
t_Monniaux::update_Monniaux_HashTable(t_Expression* F, const vector<string> &variables, t_Expression* O)
{
	assert(F != NULL);
	assert(O != NULL);

	// key = address of input kand node + variables to be eliminated
	string key = toString(F);		
	
	int var_size = variables.size();
	for(int i = 0; i < var_size; i++)
	{		
		key += variables[i];	
	}
	
	t_HTStatusValue <t_Expression*> insert_result = pvt_Monniaux_HashTable.hashtable_insert(key, O);
	if (insert_result.success())
        {
        	return true;
        }
	else
        {
		t_Logger* logManager = t_Logger::getInstance();
        	logManager->LOG("ERROR!! Failure in hash table insertion in function t_Monniaux::update_Monniaux_HashTable", pvt_logFile, c_RunLevelVerbosity);
                return false;
        }
}//function ends here
				
				

			
// This function combines algorithms Generalize1 and Generalize2 of TACAS'13 paper.
// Given a formula F and model s.t. model |= F, this function finds 
// CoreConstraints - a subset of LMCs of F sufficient to lead to model |= F.
// Returns false in case of errors; true otherwise. 
bool
t_Monniaux::Generalize(t_Expression* F, map<string, string> &model, set<t_Expression*> &CoreConstraints)
{
	t_HashTable<unsigned long long int, pair<bool, set<t_Expression*> > > cache;

	bool evaluated_value = GeneralizeRecurse(F, model, CoreConstraints, cache);
	if(!evaluated_value) // model |= F; but F evaluated with model gives false
	{
		t_Logger* logManager = t_Logger::getInstance();
        	logManager->LOG("Error in evaluation in function t_Monniaux::Generalize", pvt_logFile, c_RunLevelVerbosity);
                return false;	
	}
	else // F evaluated with model gives true
	{
		return true;
	}
}


// Internal recursive function called by Generalize.
// Given a formula F and model, this function evaluates F with model. 
// Suppose F evaluates to b under model where b \in \{ true, false \}.
// The function finds CoreConstraints - a subset of LMCs of F 
// sufficient to make F evaluate to b under model. The function returns b. 
bool
t_Monniaux::GeneralizeRecurse(t_Expression* F, map<string, string> &model, set<t_Expression*> &CoreConstraints, t_HashTable<unsigned long long int, pair<bool, set<t_Expression*> > > &cache)
{
	assert(F != NULL);

	bool evaluated_value;

	t_HTStatusValue <pair<bool, set<t_Expression*> > > result_search = cache.hashtable_search(F->getID()); // check in cache first
	if(result_search.success()) //cache hit
	{
		evaluated_value = (result_search.getValue()).first; 
		CoreConstraints = (result_search.getValue()).second;
		return evaluated_value;
	}
	else //cache miss
	{
		CoreConstraints.clear();

		string Label = pvt_em->getLabelOfExpression(F);
		assert("eqz" == Label || "diseqz" == Label || "leq" == Label || "kand" == Label || "logand" == Label || "logor" == Label || "lognot" == Label);
		
		if("eqz" == Label || "diseqz" == Label || "leq" == Label) // LMC encountered
		{
			// Let us evaluate the LMC
      			bool evaluation_done = evaluateLMC(F, model, evaluated_value, pvt_em, pvt_bvm, pvt_WidthTable);
			assert(evaluation_done);

			if(evaluated_value) //F evaluates to true under model
			{
				// insert F into CoreConstraints
				CoreConstraints.insert(F); 
			}
			else
			{
				// insert ~F into CoreConstraints
				string not_name = "lognot";
				t_Expression* NegatedLMC = CreateNode(not_name, F, pvt_em); // F is obviously an LMC here; no need to check for constants
				assert(NegatedLMC != NULL);
				CoreConstraints.insert(NegatedLMC); 
			}
		}// LMC encountered ends here
		else if("kand" == Label || "logand" == Label) // and node encountered
		{
			// evaluate each child and find core constraints from each child
			// if all children evaluate to true, then 
			//	return true with core constraints as the union of core constraints of all children
			// o/w 
			//	return false with core constraints as the smallest one among core constraints of children evaluated to false

			set<t_Expression*> UnionOfCoresOfTrueChildren; // union of core constraints of all true children
			set<t_Expression*> MinimumAmongCoresOfFalseChildren; // smallest among the core constraints of all false children

			evaluated_value = true;  
			
			vector<t_Expression*> Children = pvt_em->getVectorOfOperands(F); 
			int children_size = Children.size();
			assert(children_size != 0);
			
			for(int index = 0; index < children_size; index++) //take each child
			{
				t_Expression* Child = Children[index];
				assert(Child != NULL);

				// evaluate the child using model and find the core
				set<t_Expression*> CoreOfChild; 
				bool child_value = GeneralizeRecurse(Child, model, CoreOfChild, cache);

				if(evaluated_value) // all children encountered so far are true
				{
					if(child_value) // this child is also true
					{
						// update UnionOfCoresOfTrueChildren
						UnionOfCoresOfTrueChildren.insert(CoreOfChild.begin(), CoreOfChild.end());
					}
					else // this child is the first false child
					{
						MinimumAmongCoresOfFalseChildren = CoreOfChild;
						evaluated_value = false;
					}
				}
				else // some false child is already encountered	
				{
					// nothing to do for true child

					if(!child_value) // this child is false
					{
						if(CoreOfChild.size() < MinimumAmongCoresOfFalseChildren.size())
						{
							MinimumAmongCoresOfFalseChildren = CoreOfChild;
						}
					}
				}
			}

			if(evaluated_value) // all children are true
			{
				CoreConstraints = UnionOfCoresOfTrueChildren;
			}
			else // some child is false
			{
				CoreConstraints = MinimumAmongCoresOfFalseChildren;
			}
		}// and node encountered ends here
		else if("logor" == Label) // or node encountered
		{
			// evaluate each child and find core constraints from each child
			// if all children evaluate to false, then 
			//	return false with core constraints as the union of core constraints of all children
			// o/w 
			//	return true with core constraints as the smallest one among core constraints of children evaluated to true

			set<t_Expression*> UnionOfCoresOfFalseChildren; // union of core constraints of all false children
			set<t_Expression*> MinimumAmongCoresOfTrueChildren; // smallest among the core constraints of all true children

			evaluated_value = false;  
			
			vector<t_Expression*> Children = pvt_em->getVectorOfOperands(F); 
			int children_size = Children.size();
			assert(children_size != 0);
			
			for(int index = 0; index < children_size; index++) //take each child
			{
				t_Expression* Child = Children[index];
				assert(Child != NULL);

				// evaluate the child using model and find the core
				set<t_Expression*> CoreOfChild; 
				bool child_value = GeneralizeRecurse(Child, model, CoreOfChild, cache);

				if(!evaluated_value) // all children encountered so far are false
				{
					if(!child_value) // this child is also false
					{
						// update UnionOfCoresOfTrueChildren
						UnionOfCoresOfFalseChildren.insert(CoreOfChild.begin(), CoreOfChild.end());
					}
					else // this child is the first true child
					{
						MinimumAmongCoresOfTrueChildren = CoreOfChild;
						evaluated_value = true;
					}
				}
				else // some true child is already encountered	
				{
					// nothing to do for false child

					if(child_value) // this child is true
					{
						if(CoreOfChild.size() < MinimumAmongCoresOfTrueChildren.size())
						{
							MinimumAmongCoresOfTrueChildren = CoreOfChild;
						}
					}
				}
			}

			if(!evaluated_value) // all children are false
			{
				CoreConstraints = UnionOfCoresOfFalseChildren;
			}
			else // some child is true
			{
				CoreConstraints = MinimumAmongCoresOfTrueChildren;
			}
		}// or node encountered ends here
		else // not node encountered
		{
			// core constraints = core constraints of the child
			// evaluated_value = negation of evaluated value from child
			
			vector<t_Expression*> Children = pvt_em->getVectorOfOperands(F); 
			int children_size = Children.size();
			assert(children_size == 1);
			
			t_Expression* Child = Children[0];
			assert(Child != NULL);

			// evaluate the child using model and find the core
			set<t_Expression*> CoreOfChild; 
			bool child_value = GeneralizeRecurse(Child, model, CoreOfChild, cache);

			CoreConstraints = CoreOfChild; 
			
			if(child_value) 
			{
				evaluated_value = false; 
			}
			else
			{
				evaluated_value = true; 
			}
		}// not node encountered ends here
	
	// insert F --> (evaluated_value, CoreConstraints) into cache
	t_HTStatusValue <pair<bool, set<t_Expression*> > > insert_result = cache.hashtable_insert(F->getID(), make_pair(evaluated_value, CoreConstraints));
	assert(insert_result.success());			

	return evaluated_value;
	}//cache miss ends here     

}// Function ends