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

  Last updated: September 23, 2013
*********************************************************************/

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

This is the .yacc file for the parser for bit-vector constraints 
in SMTLIB format

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

#include <stdio.h>
#include <vector>
#include <map>
#include <set>
#include <stack>
#include <string>
#include <iostream>
#include <sstream>
#include <algorithm>
#include "idinfo.h"

#include "ExpressionMisc.h"
#define YYDEBUG 1

using namespace std;

void SMTerror(char *);
int SMTlex(void);  
int SMTwrap()
 {
   return 1;
 }


class VectorOfExpressions
{
 public:
  vector<t_Expression*> v_expressions;
  VectorOfExpressions(const vector<t_Expression*> &v_expressions_to_push)
    {
      for(int i=0;i<v_expressions_to_push.size();i++)
        {
	  t_Expression* expression_to_push = v_expressions_to_push[i];
	  assert(expression_to_push != NULL);
          v_expressions.push_back(expression_to_push);
        }
    }
  VectorOfExpressions() //A do nothing constructor..
    {
    }

};

void assign_expressions(class VectorOfExpressions *v_exprs_in, vector<t_Expression*> &v_exprs)
{
  assert(v_exprs_in != NULL);
  for(int i=0;i<v_exprs_in->v_expressions.size();i++)
    {
      v_exprs.push_back(v_exprs_in->v_expressions[i]);
    }
}


t_ConfigurationOptions config_options("config.txt");
t_ExpressionManager *em = new t_ExpressionManager(config_options);
vector<t_Expression*> root;
set<string> VarSetToElim;
t_HashTable <string, int> WidthTable;

%}


%union{
  struct IDinfo *ds_Id;
  class t_Expression *expnode;
  class VectorOfExpressions *vector_of_expressions;
  int value;
}

%token <value> LOG_NOT Log_And Log_Or Ite Define Bool Real Int BitVector BV_ADD BV_MUL Benchmark Extrafuns Formula Ifthenelse Extract Concat BV_OR Let BV_AND BV_SHL BV_LSHR ZERO_EXTEND BV_NOT BV_SUB BV_UDIV BV_ULT BV_XOR IFF SIGN_EXTEND Flet Extrapreds BV_NEG BV_SLE BV_ULE BV_UGT Assumption BV_UGE BV_SGE Exists 
%token <value> Assert Check Define_Type UType t_EQSym t_NESym t_LTSym 
%token <value> t_LESym t_GTSym t_GESym t_Plus t_Minus t_Ampersand t_UnaryMinus
%token <value> t_Star t_Slash t_LeftParen t_RightParen t_doubleColon
%token <value> t_Colon t_Semicolon t_Arrow t_Box t_Bar t_Dot t_LeftBrack t_RightBrack


%token  <ds_Id> t_Identifier t_AbstractLit t_BvLit_Dec t_BoolLit t_Var

%type <value> smt_basic_types

%type <expnode> expr 

%type <vector_of_expressions> exprlist 
%%

 /*------------------Grammar----------------------------------------*/


start : t_LeftParen Benchmark t_Identifier bench_attribute t_RightParen
	{
	cout<<"Parsing Finished Successfully \n";
	} 
	;

bench_attribute : fun_declaration | formula_declaration | pred_declaration | assumption_declaration | elimination_declaration | fun_declaration bench_attribute | formula_declaration bench_attribute | pred_declaration bench_attribute | assumption_declaration bench_attribute | elimination_declaration bench_attribute;

fun_declaration : t_Colon Extrafuns t_LeftParen fun_symb_decl t_RightParen;

pred_declaration : t_Colon Extrapreds t_LeftParen pred_symb_decl t_RightParen;

elimination_declaration : t_Colon Exists t_LeftParen  id_list t_RightParen;

id_list : t_Identifier {
			string variable = strdup($1->name);
			VarSetToElim.insert(variable);
			}
           | id_list t_Identifier  {
				    string variable = strdup($2->name);
				    VarSetToElim.insert(variable);
				   };

elimination_id_list : t_LeftParen t_Identifier Int t_RightParen 
                                     {
                                     	cout<<"This is not yet implemented\n";					
                                     	exit(1);
	                             }
           | elimination_id_list  t_LeftParen t_Identifier Int t_RightParen 
                                     {
                                       cout<<"This is not yet implemented\n";					
                                       exit(1);
                                     };


fun_symb_decl : t_LeftParen t_Identifier smt_basic_types t_LeftBrack t_AbstractLit t_RightBrack t_RightParen
		  { 
			 string variable = strdup($2->name);
			 string width_str = strdup($5->name);
			 int width = atoi(width_str.c_str());	
			 addEntryToWidthTable(variable, width, WidthTable);			 
		   }
                   |
                   t_LeftParen t_Identifier smt_basic_types t_RightParen
                    { 
                      	cout<<"This is not yet implemented\n";					
                        exit(1);   
			 
		     };

pred_symb_decl : t_LeftParen t_Identifier t_RightParen
		
			{ 
			 cout<<"This is not yet implemented\n";					
                         exit(1); 			 
		       };


smt_basic_types : 
                  Bool { 
		      $$ = $1;		    
		  } 
                  | 
                  Real { 
		      $$ = $1;		    
		  } 
                  | 
                  Int { 
		     $$ = $1;			    
		  }
                   |
		   BitVector
		   {
		    $$ = $1;		
		   };

formula_declaration :  t_Colon Formula expr 
			{
			assert($3 != NULL);
			root.push_back($3);
			}
                        |
                        t_Colon Formula t_LeftParen  Exists elimination_id_list expr t_RightParen
                        {
			assert($6 != NULL);
                        root.push_back($6);
			}
                        ;


assumption_declaration : t_Colon Assumption expr 
			{
                         cout<<"This is not yet implemented\n";					
                         exit(1); 
			};

exprlist: expr { 
	       vector<t_Expression*> vector_expr;
	       assert($1 != NULL);
	       vector_expr.push_back($1);
	       class VectorOfExpressions *obj_expr = new VectorOfExpressions(vector_expr);
	       assert(obj_expr != NULL);
	       $$ = obj_expr;	
	       }
             |
          exprlist expr
	     {
	       assert($1 != NULL);
	       assert($2 != NULL);
		
	       ($1->v_expressions).push_back($2);
	        $$ = $1;
	     }
;

expr : t_LeftParen LOG_NOT exprlist t_RightParen 
              { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 1);
	       t_Expression* leaf_expr = vector_expr[0];
	       assert(leaf_expr != NULL);

	       t_Expression* this_expr;
	       if(isTrue(leaf_expr, em))
	       	{
			this_expr = getFalse(em);
	       	}
	       else if(isFalse(leaf_expr, em))
	       	{
			this_expr = getTrue(em);
	       	}
	       else
	       	{
			string not_name = "lognot";
			this_expr = CreateNode(not_name, leaf_expr, em);
	       	}
	       assert(this_expr != NULL);
	       $$ = this_expr;
	      }
;


expr : t_LeftParen Log_And exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() >= 2);

	       // let's check if the result is false, and avoid true children
	       bool result_is_false = false;
	       vector <t_Expression*> vector_expr_with_true_avoided;
	       for(int i = 0; i < vector_expr.size(); i++)
		{
			t_Expression* leaf_expr = vector_expr[i];
	       		assert(leaf_expr != NULL);
			
			
	       		if(isFalse(leaf_expr, em))
	       		{
				result_is_false = true;
				break;
	       		}
	       		else if(!isTrue(leaf_expr, em))
	       		{
				vector_expr_with_true_avoided.push_back(leaf_expr);
	       		}
		}

	       t_Expression* this_expr;
	       if(result_is_false)
		{
			this_expr = getFalse(em);
		}
	       else if(vector_expr_with_true_avoided.size() == 0) // all operands are true
	       	{
			this_expr = getTrue(em);
	       	}
	       else if(vector_expr_with_true_avoided.size() == 1) // all operands except one are true
	       	{
			this_expr = vector_expr_with_true_avoided[0];
	       	}
	       else
	       	{
			string and_name = "logand";
			this_expr = CreateNode(and_name, vector_expr_with_true_avoided, em);
	       	}
	       assert(this_expr != NULL);
	       $$ = this_expr;
	     }
;


expr : t_LeftParen Log_Or exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() >= 2);

	       // let's check if the result is true, and avoid false children
	       bool result_is_true = false;
	       vector <t_Expression*> vector_expr_with_false_avoided;
	       for(int i = 0; i < vector_expr.size(); i++)
		{
			t_Expression* leaf_expr = vector_expr[i];
	       		assert(leaf_expr != NULL);
			
			
	       		if(isTrue(leaf_expr, em))
	       		{
				result_is_true = true;
				break;
	       		}
	       		else if(!isFalse(leaf_expr, em))
	       		{
				vector_expr_with_false_avoided.push_back(leaf_expr);
	       		}
		}

	       t_Expression* this_expr;
	       if(result_is_true)
		{
			this_expr = getTrue(em);
		}
	       else if(vector_expr_with_false_avoided.size() == 0) // all operands are false
	       	{
			this_expr = getFalse(em);
	       	}
	       else if(vector_expr_with_false_avoided.size() == 1) // all operands except one are false
	       	{
			this_expr = vector_expr_with_false_avoided[0];
	       	}
	       else
	       	{
			string or_name = "logor";
			this_expr = CreateNode(or_name, vector_expr_with_false_avoided, em);
	       	}
	       assert(this_expr != NULL);
	       $$ = this_expr;	      
	     }
;


expr : t_LeftParen Ifthenelse exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 3);

	       t_Expression* cond_expr = vector_expr[0];
	       assert(cond_expr != NULL);
	       t_Expression* then_expr = vector_expr[1];
	       assert(then_expr != NULL);
	       t_Expression* else_expr = vector_expr[2];
	       assert(else_expr != NULL);

		
	       t_Expression* this_expr;
	       if(isTrue(cond_expr, em))
	       	{
			this_expr = then_expr;
	       	}
	       else if(isFalse(cond_expr, em))
	       	{
			this_expr = else_expr;
	       	}
	       else
	       	{
			string ite_name = "ite";
			this_expr = CreateNode(ite_name, cond_expr, then_expr, else_expr, em);
	       	}
	       assert(this_expr != NULL);
	       $$ = this_expr;
	     }
;


expr : t_LeftParen t_EQSym exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
	       if(left_expr == right_expr)
	       	{
			this_expr = getTrue(em);
	       	}
	       else
	       	{
		       string bvequality_name = "=";
		       this_expr = CreateNode(bvequality_name, left_expr, right_expr, em);		              
	       	}
		assert(this_expr != NULL);
		$$ = this_expr;	
	     }
;


expr : t_LeftParen BV_ULT exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvult_name = "bvult";
	       this_expr = CreateNode(bvult_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;	
	     }
;


expr : t_LeftParen BV_UGT exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvugt_name = "bvugt";
	       this_expr = CreateNode(bvugt_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;	      
	     }
;

expr : t_LeftParen BV_ULE exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvule_name = "bvule";
	       this_expr = CreateNode(bvule_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;	
	     }
;

expr : t_LeftParen BV_UGE exprlist t_RightParen 
             { 
	       assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvuge_name = "bvuge";
	       this_expr = CreateNode(bvuge_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;	
	     }
;

expr : t_LeftParen BV_MUL exprlist t_RightParen 
             { 
               assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvmul_name = "bvmul";
	       this_expr = CreateNode(bvmul_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;
	     }
;

expr : t_LeftParen BV_ADD exprlist t_RightParen 
             { 
               assert($3 != NULL);
	       vector <t_Expression*> vector_expr = $3->v_expressions;
	       assert(vector_expr.size() == 2);

	       t_Expression* left_expr = vector_expr[0];
	       assert(left_expr != NULL);
	       t_Expression* right_expr = vector_expr[1];
	       assert(right_expr != NULL);

	       t_Expression* this_expr;
               string bvadd_name = "bvadd";
	       this_expr = CreateNode(bvadd_name, left_expr, right_expr, em);
	       assert(this_expr != NULL);
	       $$ = this_expr;
	     }
;


expr     : t_Identifier
	{
	 string variable = strdup($1->name);
	 int width = getWidthOfVariable(variable, WidthTable);
	 assert(width > 0);
	 
	 t_Expression* this_expr = CreateSymbol(variable, width, em);
	 assert(this_expr != NULL);
	 $$ = this_expr;
	}

	 |

        t_BvLit_Dec t_LeftBrack t_AbstractLit t_RightBrack
	{
	  string bvconstant = strdup($1->name);
          // bvconstant is like bv"decimal-constant"
	  bvconstant = bvconstant.substr(2); // avoid the bv part

	  string width_str = strdup($3->name);
          int width = atoi(width_str.c_str());

	  if(width > sizeof(unsigned long long int)*BYTE_SIZE)
	  {
		cout << "\nError in SMT.y! Width of bit-vector constant more than " << sizeof(unsigned long long int)*BYTE_SIZE << endl;
		cout << "The parser does not have the function to convert a decimal string of width more than "<< sizeof(unsigned long long int)*BYTE_SIZE << " to binary string, although the quantifier eliminator can support bit-vectors of arbitrary width\n";
		exit(-1);
	  }
	  else
	  {
		// let's convert the string to unsigned long long int
		unsigned long long int number = strtoull(bvconstant.c_str(), NULL, 10);
		string binarystring = integerToBinaryStringWithZeroPadding(number, width);
		
		t_Expression* this_expr = CreateConstant(binarystring, width, em);
		assert(this_expr != NULL);
		$$ = this_expr;
	  }
	}
       
         |

        t_BoolLit 
	{
	  string boolconstant = strdup($1->name);

	  t_Expression* this_expr;
	  if(boolconstant == "true")
	  {
	  	this_expr = getTrue(em);
	  }
	  else
	  {
		this_expr = getFalse(em);
	  }

	  assert(this_expr != NULL);
	  $$ = this_expr;
	}
;

	

%%
extern FILE* SMTout;

void SMTerror(char* str)
{
  fprintf( SMTout, "ERROR from parser: %s\n", str );
}