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

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

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

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

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

#ifndef project_h
#define project_h

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

using namespace std;


// t_compute: unsigned int type of maximum possible width. 
// In layer2, computations are done using machine arithmetic
// if pvt_use_bvlibrary_for_layer2_computations is false and 
// the width of variable to be eliminated is less than
// number of bits of t_compute. 
typedef unsigned long long int t_compute;

// The following definitions are for defining the side of the variable, 
// and the type of the coefficient encountered during unification. 
enum t_side_of_variable_in_unification {BOTH, NONE, LEFT, RIGHT};
enum t_type_of_coefficient_in_unification {ORIGINAL, NEGATED};


class t_Project{
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 layer1. 
	// key = address of input kand node + variable to be eliminated
	// value = simplified kand node after layer1
    	t_HashTable <string, t_Expression*> pvt_QE1_Layer1_HashTable;


	// Memoization table for layer2. 
	// key = address of input kand node + variable to be eliminated
	// value = simplified kand node after layer2
    	t_HashTable <string, t_Expression*> pvt_QE1_Layer2_HashTable;


	// Memoization table for layer3. 
	// key = address of input kand node + variables to be eliminated
	// value = simplified Boolean combination after layer3
    	t_HashTable <string, t_Expression*> pvt_Layer3_HashTable;


	// Memoization table for Project. 
	// key = address of input kand node + variables to be eliminated
	// value = resulting Boolean combination after Project
    	t_HashTable <string, t_Expression*> pvt_Project_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_Project(t_HashTable <string, int> &VariableList, t_HashTable <string, int> &WidthTable, bool use_bvlibrary_for_layer2_computations, t_ExpressionManager* em, BVManager* bvm);

	~t_Project();

	static t_Project* t_project_instance;

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

	
	/**********************************************************************/
	/*         	Part 1: Functions related to Kappa finding            */
	/**********************************************************************/




	// Given an "eqz" node, this function finds the kappa value in Kappa, and the odd part in OddPart.
	// Returns false in case of errors; true otherwise
	// Note that "eqz" node is in the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. 
	// Let ci be 2^{k_i}.e_i. Hence Kappa = k_i and OddPart = e_i
	// If the "eqz" node is free of the variable, then Kappa = UINT_MAX and OddPart is not changed by the function

	// Important: Use this function only if both Kappa value and OddPart are required. 
	// If only the Kappa value is required, use findKappaValueOfEqz
	bool findKappaValueAndOddPartOfEqz(t_Expression* eqzNode, const string &variable, unsigned int &Kappa, bvatom &OddPart);



	// Given an "eqz" node, this function finds the kappa value in Kappa.
	// Returns false in case of errors; true otherwise
	// Note that "eqz" node is of the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. 
	// Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i.
	// If the "eqz" node is free of the variable, then Kappa = UINT_MAX.
	
	// Important: Use this function if only the Kappa value is required. 
	// If both the Kappa value and OddPart are required, use findKappaValueAndOddPartOfEqz.
	bool findKappaValueOfEqz(t_Expression* eqzNode, const string &variable, unsigned int &Kappa);


	
	// Given an "diseqz" node, this function finds the kappa value in Kappa.
	// Returns false in case of errors; true otherwise
	// Note that "diseqz" node is of the form c_1.x_1 + ... +c_n.x_n != 0. Let x_i be the variable. 
	// Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i.
	// If the "diseqz" node is free of the variable, then Kappa = UINT_MAX.
	bool findKappaValueOfDiseqz(t_Expression* DiseqzNode, const string &variable, unsigned int &Kappa);



	// Given a "kadd" node, this function finds the kappa value in Kappa.
	// Returns false in case of errors; true otherwise
	// Note that "kadd" node is of the form c_1.x_1 + ... +c_n.x_n. Let x_i be the variable. 
	// Let c_i be 2^{k_i}.e_i. Hence Kappa = k_i.
	// If the "kadd" node is free of the variable, then Kappa = UINT_MAX.
	bool findKappaValueOfKadd(t_Expression* kaddNode, const string &variable, unsigned int &Kappa);



	// Given an "leq" node, this function finds the kappa value in Kappa.
	// Returns false in case of errors; true otherwise
	// Note that "leq" node is of the form c_1.x_1 + ... +c_n.x_n <= d_1.x_1 + ... +d_n.x_n. 
	// Let x_i be the variable. Let c_i be 2^{k_i}.e_i. Let d_i be 2^{k'_i}.e'_i.
	// Kappa = min(k_i, k'_i). 
	// If the "leq" node is free of the variable, then Kappa = UINT_MAX.
	bool findKappaValueOfLeq(t_Expression* LeqNode, const string &variable, unsigned int &Kappa);




	// Given a kand node and variable, 
	// this function finds the kappa of the kand node for the variable,.i.e.
	// the minimum among the kappa values of the constraints in kand. 
	// If all the constraints are free of the variable, "Kappa" is set as UINT_MAX. 
	// Returns false in case of errors; true otherwise. 
	bool findKappaValueOfKandNode(t_Expression* kandNode, const string &variable, unsigned int &minKappa);



	// Given a set of constraints i.e. equations, disequations, and inequations, 
	// this function finds in "minKappa", the minimum among the kappa values of
	// the constraints. If all the constraints are free of the variable, 
	// "minKappa" is set as UINT_MAX. Returns false in case of errors; true otherwise. 
	bool findMinimumKappaValueAmongSetOfConstraints(const set<t_Expression*> &Constraints, const string &variable, unsigned int &minKappa);



	// Given a monom, i.e. "bvmul" node, this function finds the kappa value and odd part 
	// of the coefficient of the variable in the monom. In case the monom is free of the variable,
	// Kappa is set as UINT_MAX. Returns false in case of errors; true otherwise. 
	bool findKappaValueAndOddPartOfMonom(t_Expression* monom, const string &variable, unsigned int &Kappa, bvatom &OddPart); 



	// Given a monom, i.e. "bvmul" node, this function finds the kappa value
	// of the coefficient of the variable in the monom. In case the monom is free of the variable,
	// Kappa is set as UINT_MAX. Returns false in case of errors; true otherwise. 
	bool findKappaValueOfMonom(t_Expression* monom, const string &variable, unsigned int &Kappa); 





	/**********************************************************************/
	/*              Part 2: Functions for Layer1                          */
	/**********************************************************************/





	// Given a "kand" node, this function finds the "eqz" node with the minimum kappa value in pivotEqzNode,
	// the kappa value in minKappa, and the odd part in oddPartOfMinKappa.
	// Returns false in case of errors; true otherwise
	// Note that "eqz" node is in the form c_1.x_1 + ... +c_n.x_n = 0. Let x_i be the variable. 
	// Let ci be 2^{k_i}.e_i. Hence kappa = k_i and odd part = e_i
	// If the equations in "kand" node are free of the variable, then minKappa = UINT_MAX. 
	// In this case, pivotEqzNode and OddPart are not changed by the function. 
	bool findEquationWithMinimumKappaValue(t_Expression* kandNode, const string &variable, t_Expression* &pivotEqzNode, unsigned int &minKappa, bvatom &oddPartOfMinKappa);

	
	
	// Given an "eqz" node c_0 + c_1.x_1 + ... +c_n.x_n = 0, pivot variable x_i, let c_i be 2^{k_i}.e_i. 
	// Hence "eqz" node is c_0 + c_1.x_1 + ... 2^{k_i}.e_i.x_i+ ... +c_n.x_n = 0. Hence "eqz" node 
	// can be expressed as 2^{k_i}.x_i = MI(e_i).(-c_0) + MI(e_i).(-c_1).x_1 + ... + MI(e_i).(-c_n).x_n. 

	// Given an "eqz" node c_0 + c_1.x_1 + ... +c_n.x_n = 0, pivot variable x_i, and odd part e_i, this 
	// function returns MI(e_i).(-c_0) + MI(e_i).(-c_1).x_1 + ... + MI(e_i).(-c_n).x_n as
	// Constant = MI(e_i).(-c_0) and CoefficientMap = vector < (x_1, MI(e_i).(-c_1)),  ... ,(x_n,  MI(e_i).(-c_n)) >

	// Returns false in case of errors; true otherwise. 
	bool getRHSOfEquationInNormalFormAsCoefficientMap(t_Expression* eqzNode, const string &PivotVariable, const bvatom &OddPart, bvatom &Constant, vector< pair< string, bvatom > > &CoefficientMap);


	
	// Given a "kand" node, variable, and PivotEquation 2^{k}.x_i = t, where
	// k is represented as KappaOfPivotEquation and t is represented as 
	// ConstantOfPivotEquationInNormalForm and CoefficientMapOfPivotEquationInNormalForm, 
	// this function, takes each constraint in the "kand" node,
	 
	// (1) if the constraint is not the PivotEquation, 
	// then recreates the constraint by replacing each occurance of 2^{k}.x_i by t, 
	// (2) if the constraint is the PivotEquation and if layer1 eliminates the variable,
	// then replaces the PivotEquation by \exists x.(2^{k}.x_i = t) \equiv (2^{p-k}. t = 0),
	// (3) if the constraint is the PivotEquation and layer1 does not eliminate the variable,
	// then keeps the PivotEquation. 
	
	// Recreates the "kand" node, and returns it. 
	// Returns true node if the result is true. Returns NULL in case of errors. 
	
	// Sets layer1_eliminates_variable to true / false depending on whether layer1 completely
	// eliminates the variable or not. 
	t_Expression* substituteAndSimplifyKandNodeUsingPivotEquation(t_Expression* kandNode, const string &variable, t_Expression* PivotEquation, unsigned int  KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm, bool &layer1_eliminates_variable);



	// Given a "kadd" node, variable, and pivot equation 2^{k}.x_i = t, where
	// k is represented as KappaOfPivotEquation, and t is represented as 
	// ConstantOfPivotEquationInNormalForm and CoefficientMapOfPivotEquationInNormalForm, 
	// this function, 
	// recreates the "kadd" node by replacing each occurance of 2^{k}.x_i by t, 
	// and returns it. Returns NULL in case of errors. 
	t_Expression* substituteAndSimplifyKaddNodeUsingPivotEquation(t_Expression* kaddNode, const string &variable, unsigned int  KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm);	
	



	// We have PivotEquation as 2^{k}.x_{i} = t mod 2^{p}. 
	// This function creates 2^{p-k}. t = 0 in RecreatedPivotEquation. 
	// Returns false in case of errors, true otherwise. 
	bool QEFromSingleEquation(const string &variable, t_Expression* PivotEquation, unsigned int  KappaOfPivotEquation, const bvatom &ConstantOfPivotEquationInNormalForm, const vector< pair< string, bvatom > > &CoefficientMapOfPivotEquationInNormalForm, t_Expression* &RecreatedPivotEquation);
	



	
	// Given a "kand" node, this function applies layer1 to eliminate variable
	// Returns NULL in case of errors, true node if the result is true, and
	// simplified "kand" node otherwise. 
	t_Expression* QE1_Layer1(t_Expression* kandNode, const string &variable);



	
	// Checks if (InputKandNode, variable) is existing in QE1_Layer1_HashTable. 
	// Returns the result if existing; NULL otherwise.  
	t_Expression* checkIn_QE1_Layer1_HashTable(t_Expression* InputKandNode, const string &variable);




	// Updates QE1_Layer1_HashTable with (InputKandNode, variable) ---> OutputKandNode. 
	// Returns false in case of errors; true otherwise. 
	bool update_QE1_Layer1_HashTable(t_Expression* InputKandNode, const string &variable, t_Expression* OutputKandNode);



	
	// Given a "kand" node, this function applies layer1 to eliminate multiple variables. 
	// Returns NULL in case of errors, true node if the result is true, and simplified "kand" node otherwise. 
	t_Expression* Layer1(t_Expression* kandNode, const vector<string> &variables); 






	/**********************************************************************/
	/*              Part 3: Functions for Layer2                          */
	/**********************************************************************/





	// Given a "kand" node, this function calls the function to apply layer2 
	// for eliminating multiple variables in a loop. Dropping constraints involving a 
	// variable may help in dropping constraints involving other variables. Hence we
	// call the function to apply layer2 until no more droppping is possible.
	// Returns NULL in case of errors, true node if the result is true, 
	// and simplified "kand" node otherwise. 
	t_Expression* Layer2(t_Expression* kandNode, const vector<string> &variables);



	// Given a "kand" node, this function applies layer2 for eliminating multiple 
	// variables. 
	// Returns NULL in case of errors, true node if the result is true, 
	// and simplified "kand" node otherwise. 
	t_Expression* Layer2Step(t_Expression* kandNode, const vector<string> &variables);



	// Given a "kand" node, this function applies layer2 to eliminate variable.
	// Returns NULL in case of errors, true node if the result is true, and
	// simplified "kand" node otherwise. 
	t_Expression* QE1_Layer2Step(t_Expression* kandNode, const string &variable);



	// Updates pvt_QE1_Layer2_HashTable with (InputKandNode, variable) ---> OutputKandNode. 
	// Returns false in case of errors; true otherwise. 
	bool update_QE1_Layer2_HashTable(t_Expression* InputKandNode, const string &variable, t_Expression* OutputKandNode);



	// Checks if (InputKandNode, variable) is existing in pvt_QE1_Layer2_HashTable. 
	// Returns the result if existing; NULL otherwise.  
	t_Expression* checkIn_QE1_Layer2_HashTable(t_Expression* InputKandNode, const string &variable);
	


	// find the core constraints among E_x, D_x, and I_x in E_core_x, D_core_x, and I_core_x.
	// i.e. find E_core_x, D_core_x, and I_core_x such that 
	// \exists x. (E_x \union D_x \union I_x) \equiv exists x. (E_core_x \union D_core_x \union I_core_x)
	// returns false in the case of errors; true otherwise.
	bool findCoreConstraints(const set<t_Expression*> &E_x, const set<t_Expression*> &D_x, const set<t_Expression*> &I_x, const string &variable, set<t_Expression*> &E_core_x, set<t_Expression*> &D_core_x, set<t_Expression*> &I_core_x);



	// Suppose ~core = D_neg_core_x \union I_neg_core_x. 
	// This function finds the least constraing constraints of ~core in D_new and I_new. 
	// Least constraining constraints are those with the maximum kappa value. 
	// Returns false in case of errors; true otherwise. 
	bool getLeastConstrainingConstraints(const set<t_Expression*> &D_neg_core_x, const set<t_Expression*> &I_neg_core_x, const string &variable, set<t_Expression*> &D_new, set<t_Expression*> &I_new);



	// Checks if
	// \exists x. (E_core_x \union D_core_x \union I_core_x \union D_neg_core_x \union I_neg_core_x) \equiv
	// \exists x. (E_core_x \union D_core_x \union I_core_x)
	// i.e. \exists x. (core \union ~core) \equiv  \exists x. (core)
	// using the idea described in TACAS'13 paper
	//
	// Sets Extendable to true if yes, false otherwise.
	// Returns false in case of errors; true otherwise. 
	bool isExt(const set<t_Expression*> &E_core_x, const set<t_Expression*> &D_core_x, const set<t_Expression*> &I_core_x, const set<t_Expression*> &D_neg_core_x, const set<t_Expression*> &I_neg_core_x, const string &variable, bool &Extendable);



	// compute 2^{Kappa} using machine arithmetic
	t_compute findTwosPower_UsingMachineArithmetic(unsigned Kappa);



	// compute 2^{Kappa} using bv-library
	// WidthOfResult is the width (no: of bits) of the result bvatom
	bvatom findTwosPower_UsingBVLibrary(unsigned WidthOfResult, unsigned Kappa);



	// Using machine arithmetic, 
	// finds Mu_D i.e. the number of valuations of the bits of variable 
	// disallowed by the disequations, and checks if Mu_D < Mu_I. 
	// Sets Extendable to true if Mu_D < Mu_I, and to false if Mu_D >= Mu_I. 
	// Returns false in the case of errors; true otherwise. 
	bool checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingMachineArithmetic(t_compute Mu_I, const set<t_Expression*> &D_neg_core_x, const string &variable, unsigned p, unsigned Kappa_0, bool &Extendable);



	// Using bv-library, 
	// finds Mu_D i.e. the number of valuations of the bits of variable 
	// disallowed by the disequations, and checks if Mu_D < Mu_I. 
	// Sets Extendable to true if Mu_D < Mu_I, and to false if Mu_D >= Mu_I. 
	// Returns false in the case of errors; true otherwise. 
	// Width (no: of bits) of the result bvatom is p+1
	bool checkIfCombinationsDisallowedByDisequations_LessThan_Mu_I_UsingBVLibrary(bvatom Mu_I, const set<t_Expression*> &D_neg_core_x, const string &variable, unsigned p, unsigned Kappa_0, bool &Extendable); 



	
	// Using machine arithmetic, 
	// finds Mu_I i.e. under-approximation of the number of valuations to the
	// most significant Kappa_0 bits of variable satisfying the inequations. 
	// Returns false in the case of errors; true otherwise. 
	bool computeCombinationsPermittedByInequations_UsingMachineArithmetic(unsigned Kappa_0, const set<t_Expression*> &I_neg_core_x, const string &variable, unsigned p, t_compute &Mu_I);




	// Using bv-library, 
	// finds Mu_I i.e. under-approximation of the number of valuations to the
	// most significant Kappa_0 bits of variable satisfying the inequations. 
	// Returns false in the case of errors; true otherwise. 
	bool computeCombinationsPermittedByInequations_UsingBVLibrary(unsigned Kappa_0, const set<t_Expression*> &I_neg_core_x, const string &variable, unsigned p, bvatom &Mu_I);


	

	// Using machine arithmetic,
	// finds the maximum possible value a term (kaddNode) can take. 
	// If the term is a constant, then the maximum possible value is the constant.
	// Otherwise, if the term can be expressed as 2^{Tau}.t, where Tau \in \{0,...,p-1},
	// then the maximum possible value is 2^{p} - 2^{Tau}.
	// Returns false in case of errors; true otherwise. 
	bool computeMaximumPossibleValueOfKadd_UsingMachineArithmetic(t_Expression* kaddNode, unsigned int p, t_compute &MaxPossibleValue);



	
	// Using bv-library,
	// finds the maximum possible value a term (kaddNode) can take. 
	// If the term is a constant, then the maximum possible value is the constant.
	// Otherwise, if the term can be expressed as 2^{Tau}.t, where Tau \in \{0,...,p-1},
	// then the maximum possible value is 2^{p} - 2^{Tau}.
	// Returns false in case of errors; true otherwise. 
	bool computeMaximumPossibleValueOfKadd_UsingBVLibrary(t_Expression* kaddNode, unsigned int p, bvatom &MaxPossibleValue);




	// Using machine arithmetic,
	// finds the minimum possible value a term (kaddNode) can take. 
	// If the term is a constant, then the minimum possible value is the constant.
	// Otherwise, if the term can be expressed as 2^{Tau}.t + Constant, 
	// where Tau \in \{0,...,p-1}, then the minimum possible value is  Constant mod 2^{Tau}.
	// Returns false in case of errors; true otherwise. 
	bool computeMinimumPossibleValueOfKadd_UsingMachineArithmetic(t_Expression* kaddNode, unsigned int p, t_compute &MinPossibleValue);




	// Using bv-library,
	// finds the minimum possible value a term (kaddNode) can take. 
	// If the term is a constant, then the minimum possible value is the constant.
	// Otherwise, if the term can be expressed as 2^{Tau}.t + Constant, 
	// where Tau \in \{0,...,p-1}, then the minimum possible value is  Constant mod 2^{Tau}.
	// Returns false in case of errors; true otherwise. 
	bool computeMinimumPossibleValueOfKadd_UsingBVLibrary(t_Expression* kaddNode, unsigned int p, bvatom &MinPossibleValue);



	// Find min among two t_compute values
	t_compute  minimum(t_compute a, t_compute b);



	// Find min among two bvatoms
	bvatom	minimum(bvatom a, bvatom b);



	// Find max among two t_compute values
	t_compute  maximum(t_compute a, t_compute b);



	// Find max among two bvatoms
	bvatom	maximum(bvatom a, bvatom b);



	// displays bound map on screen
	bool displayBoundMapOnScreen(map<t_Expression*, pair<t_compute, t_compute> > &BoundMap);


	bool displayBoundMapOnScreen(map<t_Expression*, pair<bvatom, bvatom> > &BoundMap);





	/**********************************************************************/
	/*              Part 4: Functions for Layer3                          */
	/**********************************************************************/





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



	// Updates pvt_Layer3_HashTable with (InputKandNode, variables) ---> OutputKandNode. 
	// Returns false in case of errors; true otherwise. 
	bool update_Layer3_HashTable(t_Expression* InputKandNode, const vector<string> &variables, t_Expression* OutputKandNode);



	// Given a "kand" node, this function applies layer3 for eliminating multiple 
	// variables. Returns NULL in case of errors, true node if the result is true, 
	// and an equivalent Boolean combination otherwise.  
	t_Expression* Layer3(t_Expression* kandNode, const vector<string> &variables);



	// Given a set of inequations I_variable involving variable, this function checks if 
	// all the inequations in I_variable are unified w.r.t. variable. 
	// In other words, this function checks if each inequation is of the form
	// a.variable \bowtie t, where a is a constant, \bowtie \in {<=, >=}, and t is a term free of variable.
	// Note that a must be the same for all the inequations.
	// This function sets constraints_with_variable_are_in_unified_form to 
	// true if all the inequations in I_variable are unified w.r.t. variable, 
	// false otherwise.
 	// Returns false in case of errors, true otherwise.  
	bool constraintsInUnifiedForm(const set<t_Expression*> &I_variable, const string &variable, bool &constraints_with_variable_are_in_unified_form);



	// Here I_variable is a set of inequations involving variable, 
	// where each inequation is of the form a.variable \bowtie t, 
	// such that a is a constant, \bowtie \in {<=, >=}, and t is a term free of variable,
	// and Kappa(a.variable, variable) = 0. Also a is the same for all the inequations.
	// This function performs the standard Fourier-Motzkin algorithm
	// for QE from reals to compute \exists variable.(I_variable).
	// Note that since Kappa(a.variable, variable) = 0, standard 
	// Fourier-Motzkin algorithm on reals works on bit-vectors also.
	// Returns false in case of errors, true otherwise.  
	bool standardFourierMotzkin(const set<t_Expression*> &I_variable, const string &variable, set<t_Expression*> &Inequations_From_FM);



	// Here I_variable is a set of inequations involving variable, 
	// where each inequation is of the form a.variable \bowtie t, 
	// such that a is a constant, \bowtie \in {<=, >=}, t is a term free of variable,
	// and Kappa = Kappa(a.variable, variable) != 0. 
	// Also a is the same for all the inequations.
	// This function performs modified Fourier-Motzkin algorithm for LMIs
	// in the TACAS'13 paper to compute \exists variable.(I_variable).
	// Result of \exists variable.(I_variable) is the conjunction of constraints in Constraints_From_FM
	// If result_is_conjunctive then,
	// each constraint in Constraints_From_FM is an LMI
	// otherwise,
	// each constraint in Constraints_From_FM is a disjunction of kand nodes
	// Returns false in case of errors, true otherwise.  
	bool modifiedFourierMotzkin(const set<t_Expression*> &I_variable, const string &variable, unsigned Kappa, set<t_Expression*> &Constraints_From_FM, bool &result_is_conjunctive);



	// Here I_variables is a set of inequations involving variables.
	// This function finds a subset of variables which can be unified together. 
	// NonUnifiableVariables is a set of variables which cannot be unified.
	// The idea here is to select a subset of variables excluding those in NonUnifiableVariables, 
	// such that no two variables in the subset appear in the same constraint. 
	// Returns false in case of errors, true otherwise.  
	bool findVariablesWhichCanBeUnifiedTogether(const set<t_Expression*> &I_variables, const set<string> &variables, const set<string> &NonUnifiableVariables,  set<string> &VariablesToUnifyTogether);

	


	// Suppose we need to compute \exists X.(I_X).
	// Let variables be a subset of X. This function unifies I_X w.r.t. variables. 
	// Although the TACAS paper presents converting to unified form for a 
	// number of cases, 
	// this function performs unification of only constraints
	// of the form \exists x. A, 
	// where x is a variable to be unified and A is a conjunction of LMIs, 
	// such that, each LMI in A is of the form, 
	//
	// ax+t_1 <= t_2,  -ax+t_1 <= t_2,  t_1 <= ax+t_2,  t_1 <= -ax+t_2,
	// ax+b_1 <= ax+b_2, or -ax+b_1 <= -ax+b_2, 
	// where a, b_1, b_2 are constants, and t_1, t_2 are terms free of x.
	//
	// The function converts each LMI in such a conjunction to a Boolean
	// combination of LMCs. 
	//
	// In order to perform unification of I_X w.r.t. a set of variables, the function
	// takes each constraint and variable contained in it to be unified, checks if
	// the constraint can be unified w.r.t. the variable, and performs unification if possible. 
	//  
	// unification_successful is set to true if unification w.r.t. at least one variable could be
	// done; to false otherwise.
	// Returns NULL in case of errors; the unified expression otherwise. 
	t_Expression*	convertToUnifiedForm(const set<t_Expression*> &I_X, const set<string> &variables, bool &unification_successful);




	// Given an inequation t_1 <= t_2, a variable x in the support of t_1 <= t_2, 
	// and side_of_variable indicating the side of t_1 <= t_2 where x occurs,
	// this function performs the following:
	// 
	// (1) If side_of_variable is LEFT, i.e. t_1 <= t_2 is like ax+t_3 <= t_2,  then
	// it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively. 
	// Also it sets constraint_non_unifiable to false.
	//
	// (2) If side_of_variable is RIGHT, i.e. t_1 <= t_2 is like t_1 <= ax+t_3,  then
	// it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively.  
	// Also it sets constraint_non_unifiable to false.
	//
	// (3) If side_of_variable is BOTH, i.e. t_1 <= t_2 is like a_1x+t_3 <= a_2x+t_4,  then
	// it checks if a_1 == a_2 and t_3 and t_4 are constants. If yes, then,
	// it finds a and -a in CoefOfVarToUnify and AIOfCoefOfVarToUnify respectively.  
	// Also it sets constraint_non_unifiable to false. 
	// Otherwise, it sets constraint_non_unifiable to true. 
	//
	// Returns false in case of errors; true otherwise.
	bool getCoefOfVarToUnifyAndAIOfCoefOfVarToUnify(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, bvatom &CoefOfVarToUnify, bvatom &AIOfCoefOfVarToUnify, bool &constraint_non_unifiable);




	// Checks if the coefficient of the variable to be  eliminated is the same/additive inverse
	// of the coefficients which previously appeared. Sets  type_of_coefficient to ORIGINAL/NEGATED according to it. 
	//
	// Given an inequation t_1 <= t_2, a variable x in the support of t_1 <= t_2, 
	// side_of_variable indicating the side of t_1 <= t_2 where x occurs, 
	// CoefOfVarToUnify as the previously appeared coefficient, and AIOfCoefOfVarToUnify
	// as the additive inverse of the previously appeared coefficient,
	// this function performs the following:
	// 
	// (1) If side_of_variable is LEFT, i.e. t_1 <= t_2 is like ax+t_3 <= t_2,  then
	// it finds a and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. 
	// If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL;
	// if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED.
	// Also it sets constraint_non_unifiable to false.
	// If a != CoefOfVarToUnify and a != AIOfCoefOfVarToUnify then sets constraint_non_unifiable to true.
	//
	// (2) If side_of_variable is RIGHT, i.e. t_1 <= t_2 is like t_1 <= ax+t_3,  then
	// it finds a and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. 
	// If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL;
	// if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED.
	// Also it sets constraint_non_unifiable to false.
	// If a != CoefOfVarToUnify and a != AIOfCoefOfVarToUnify then sets constraint_non_unifiable to true.
	//
	// (3) If side_of_variable is BOTH, i.e. t_1 <= t_2 is like a_1x+t_3 <= a_2x+t_4,  then
	// it checks if a_1 == a_2 and t_3 and t_4 are constants. If yes, then,
	// it finds a = a_1 and checks if a == CoefOfVarToUnify or a == AIOfCoefOfVarToUnify. 
	// If a == CoefOfVarToUnify then, type_of_coefficient is set to ORIGINAL;
	// if a == AIOfCoefOfVarToUnify then, type_of_coefficient is set to NEGATED.
	// Also it sets constraint_non_unifiable to false. 
	// Otherwise, it sets constraint_non_unifiable to true. 
	// 
	// Returns false in case of errors; true otherwise.
	bool findTypeOfCoefficient(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, bvatom CoefOfVarToUnify, bvatom AIOfCoefOfVarToUnify, t_type_of_coefficient_in_unification &type_of_coefficient, bool &constraint_non_unifiable);


	
	// Given an inequation \alpha <= \beta, a variable x in the support of \alpha <= \beta, 
	// side_of_variable indicating the side of \alpha <= \beta where x occurs,
	// this function performs the following:
	// 
	// (1) If side_of_variable is LEFT and type_of_coefficient is ORIGINAL, 
	//  i.e. \alpha <= \beta is like ax+t_1 <= t_2,  then 
	// 
	// If t_1 is zero, then we have ax <= t2; 
	// in this case constraint_already_unified is set to true
	//
	// otherwise, it generates the following Boolean combination unified w.r.t. x:
	//		
	//	((t_1 \neq 0)\wedge (-t_1 \le ax)\wedge (t_1 \le t_2)) \vee
	//	((t_1 = 0)\wedge (ax <= t_2 - t_1)) \vee
	//	((-t_1 \le ax)\wedge (ax <= t_2 - t_1)) \vee	
	//	((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (ax <= t_2 - t_1)) 
	//
	// also constraint_already_unified is set to false. 
	// 
	// (2) If side_of_variable is LEFT and type_of_coefficient is NEGATED, 
	//  i.e. \alpha <= \beta is like -ax+t_1 <= t_2,  then it generates the following
	//  Boolean combination unified w.r.t. x:
	//
	// 	((t_1 \neq 0)\wedge (ax \neq 0)\wedge (ax \le t_1)\wedge (t_1 \le t_2)) \vee
	// 	((t_2 = 0)\wedge (ax = 0)) \vee
	// 	((t_1 = 0)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) \vee
	// 	((ax \neq 0)\wedge (ax <= t_1)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) \vee
	// 	((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (ax = 0)) \vee
	// 	((t_1 \neq 0)\wedge (t_1 \le t_2)\wedge (t_2 - t_1 \neq 0)\wedge (t_1 - t_2 <= ax)) 
	//
	// also constraint_already_unified is set to false. 
	// 
	// (3) If side_of_variable is RIGHT and type_of_coefficient is ORIGINAL, 
	//  i.e. \alpha <= \beta is like t_1 <= ax+t_2,  then 
	//
	// If t_2 is zero, then we have t_1 <= ax; 
	// in this case constraint_already_unified is set to true
	// 
	// otherwise, it generates the following Boolean combination unified w.r.t. x:
	//
	//	((t_2 \neq 0)\wedge (ax \le -t_2-1)\wedge (t_1 \le t_2-1))\vee
	// 	((t_2 = 0)\wedge (t_1-t_2 <= ax))\vee
	// 	((t_2 \neq 0)\wedge (t_1 \le t_2-1)\wedge (t_1-t_2 <= ax))\vee
	// 	((t_2 \neq 0)\wedge (ax <= -t_2-1)\wedge (t_1-t_2 <= ax))
	//
	// also constraint_already_unified is set to false. 
	// 
	// (4) If side_of_variable is RIGHT and type_of_coefficient is NEGATED, 
	//  i.e. \alpha <= \beta is like t_1 <= -ax+t_2,  then it generates the following
	//  Boolean combination unified w.r.t. x:
	//
	// 	((t_2 \neq 0)\wedge (ax = 0)\wedge (t_1 \le t_2-1)) \vee
	// 	((t_2 \neq 0)\wedge (t_2 + 1 \le ax)\wedge (-t_2 - 1 \neq 0)\wedge (t_1 \le t_2-1)) \vee
	// 	((t_2 = 0)\wedge (t_1 - t_2 = 0)) \vee
	// 	((t_2 = 0)\wedge (ax \neq 0)\wedge (ax \le t_2 - t_1)) \vee
	// 	((t_1 \le t_2 - 1)\wedge (t_1 - t_2 = 0)\wedge (t_2 \neq 0)) \vee
	// 	((t_1 \le t_2 - 1)\wedge (ax \neq 0)\wedge (ax \le t_2 - t_1)\wedge (t_2 \neq 0)) \vee
	// 	((t_2 \neq 0)\wedge (ax = 0)\wedge (t_1 - t_2 = 0)) \vee
	// 	((t_2 \neq 0)\wedge (-t_2 - 1 \neq 0)\wedge (t_2 + 1 \le ax)\wedge  (t_1 - t_2 = 0)) \vee
	// 	((t_2 \neq 0)\wedge (-t_2 - 1 \neq 0)\wedge (t_2 + 1 \le ax)\wedge  (ax \neq 0)\wedge (ax \le t_2 - t_1))
	//
	// also constraint_already_unified is set to false. 
	// 			
	bool unifyInequationWithVariableOnOneSide(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, t_type_of_coefficient_in_unification type_of_coefficient, vector<t_Expression*> &UnifiedVector, bool &constraint_non_unifiable);

	
	// Given an inequation of the form a.x+b_1 \le a.x+b_2, where b_1 and b_2 are constants,
	// this function performs the following:
	// 
	// (1) If type_of_coefficient is ORIGINAL, then 
	//
	// it generates the following Boolean combinations unified w.r.t. x:
	//		
	// 	(ax \le -b_2-1) 		if b_1 = 0 and b_2\neq 0
	// 	(ax \ge -b_1)   		if b_2 = 0 and b_1\neq 0
	// 	(ax \le -b_2-1)\vee (ax \ge -b_1) if b_1 < b_2 and b_1\neq 0
	// 	(ax \le -b_2-1)\wedge (ax \ge -b_1) if b_1 > b_2 and b_2\neq 0
	//
	// (2) If type_of_coefficient is NEGATED, then
	//  it generates the following Boolean combination unified w.r.t. x:
	//
	//  	(ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_1+1)) 	if b_1=0 and b_2\neq 0
	//	((ax \neq 0)\wedge (ax \le b_1)) 			if b_2=0 and b_1\neq 0
	//	(ax=0)\vee ((b_2+1 \neq 0)\wedge (ax \ge b_2+1))\vee ((ax \neq 0)\wedge (ax \le b_1)) 	if b_1 < b_2 and b_1\neq 0
	//	((ax \ge b_2+1)\wedge (ax \le b_1)) 			if b_1 > b_2 and b_2\neq 0
	//
	// constraint_already_unified is always set to false.  
	// 	
	bool unifyInequationWithVariableOnBothSides(t_Expression* Inequation, const string &VarToUnify, t_side_of_variable_in_unification side_of_variable, t_type_of_coefficient_in_unification type_of_coefficient, vector<t_Expression*> &UnifiedVector, bool &constraint_already_unified);




	
	// Given an Inequation and variable, this function finds the side of the Inequation 
	// where the variable appears - NONE, BOTH, LEFT, or RIGHT
	t_side_of_variable_in_unification findSideOfVariableInInequation(t_Expression* Inequation, const string &variable);



	/**********************************************************************/
	/*              Part 5: Functions for Project                         */
	/**********************************************************************/



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


	// Updates pvt_Project_HashTable with (InputKandNode, variables) ---> OutputNode. 
	bool update_Project_HashTable(t_Expression* InputKandNode, const vector<string> &variables, t_Expression* OutputNode);


	// Given a kandNode and vector of variables X, this function 
	// applies the algorithm Project in TACAS'13 paper, in order to compute \exists X. kandNode. 
	t_Expression* Project(t_Expression* kandNode, const vector<string> &X);


};

#endif