/********************************************************************
  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.  

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

#ifndef monniaux_h
#define monniaux_h

#include "ExpressionMisc.h"
#include "ExpressionManager.h"
#include "HashTable_WithStandardKeys.h"
#include "LogManager.h"
#include "Project.h"
#include <vector>
#include <iostream>
#include <assert.h>
#include <limits.h>

using namespace std;


class t_Monniaux{
private:
	
	// This is the variable list.
	// This gives the index of a variable.
	// Recall that in a kadd node, the children should be 
	// sorted based on the indices of variables in the monoms. 
	t_HashTable <string, int> pvt_VariableList;


	// This is the width table.
	// This gives the width of a variable.
	t_HashTable <string, int> pvt_WidthTable;


	// pointer to expression manager
	t_ExpressionManager* pvt_em;


	// pointer to bit-vector manager
	BVManager* pvt_bvm;


	// for logging
	ofstream* pvt_logFile;


	// Memoization table for Monniaux. 
	// key = address of input expression node + variables to be eliminated
	// value = result of Monniaux
    	t_HashTable <string, t_Expression*> pvt_Monniaux_HashTable;



	// if true, then bvlibrary is used for heuristic computations in layer2.
	// if false, then
	// if width of variable to be eliminated is less than 
	// number of bits for t_compute then,
	// machine arithmetic is used for heuristic computations in layer2,
	// otherwise, bvlibrary is used for heuristic computations in layer2.
	bool pvt_use_bvlibrary_for_layer2_computations;

	
public:
	


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


	t_Monniaux(t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm);

	~t_Monniaux();

	static t_Monniaux* t_monniaux_instance;

  	static t_Monniaux* getInstance(t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm);


	/**********************************************************************/
	/*             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* Monniaux(t_Expression* InputNode, const vector<string> &variables, t_solver solver);


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


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


	// 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 Generalize(t_Expression* F, map<string, string> &model, set<t_Expression*> &CoreConstraints);


	// 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 GeneralizeRecurse(t_Expression* F, map<string, string> &model, set<t_Expression*> &CoreConstraints, t_HashTable<unsigned long long int, pair<bool, set<t_Expression*> > > &cache);
	
	

	
};

#endif