path: root/lib/SMT/smtlib.y

%{
/*****************************************************************************/
/*!
 * \file smtlib.y
 * 
 * Author: Clark Barrett
 * 
 * Created: Apr 30 2005
 *
 * <hr>
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/
/* 
   This file contains the bison code for the parser that reads in CVC
   commands in SMT-LIB language.
*/

#include "SMTParser.h"
#include "klee/Expr.h"

#include <sstream>

using namespace klee;
using namespace klee::expr;

// Define shortcuts for various things
#define PARSER SMTParser::parserTemp
#define DONE SMTParser::parserTemp->done
#define EXPR SMTParser::parserTemp->query
#define ASSUMPTIONS SMTParser::parserTemp->assumptions
#define QUERY SMTParser::parserTemp->query

#define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled)
#define BVSIZE (SMTParser::parserTemp->bvSize)
#define QUERYPARSED SMTParser::parserTemp->queryParsed

// Suppress the bogus warning suppression in bison (it generates
// compile error)
#undef __GNUC_MINOR__

/* stuff that lives in smtlib.lex */
extern int smtliblex(void);

int smtliberror(const char *s)
{
  std::ostringstream ss;
  ss << SMTParser::parserTemp->fileName << ":" << SMTParser::parserTemp->lineNum
     << ": " << s;
  return SMTParser::parserTemp->Error(ss.str());
}


#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 10485760

%}

/*
%union {
  std::string *str;
  std::vector<std::string> *strvec;
  CVC3::Expr *node;
  std::vector<CVC3::Expr> *vec;
  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
};
*/

%union {
  std::string *str;
  klee::expr::ExprHandle node;
  std::vector<klee::expr::ExprHandle> *vec;
};


%start cmd

/* strings are for better error messages.  
   "_TOK" is so macros don't conflict with kind names */
/*
%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls
%type <vec> an_formulas quant_vars an_terms fun_symb patterns
%type <node> pattern 
%type <node> benchmark bench_name bench_attribute
%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig
%type <node> an_formula quant_var an_atom prop_atom
%type <node> an_term basic_term sort_symb pred_symb
%type <node> var fvar
%type <str> logic_name quant_symb connective user_value attribute annotation
%type <strvec> annotations
%type <pat_ann> patterns_annotations
*/

%type <node> an_formula an_logical_formula an_atom prop_atom
%type <vec> an_formulas
%type <node> an_term basic_term constant
%type <node> an_fun an_arithmetic_fun an_bitwise_fun
%type <node> an_pred
%type <str> logic_name status attribute user_value annotation annotations 
%type <str> var fvar symb

%token <str> NUMERAL_TOK
%token <str> SYM_TOK
%token <str> STRING_TOK
%token <str> AR_SYMB
%token <str> USER_VAL_TOK

%token <str> BV_TOK
%token <str> BVBIN_TOK
%token <str> BVHEX_TOK

%token BITVEC_TOK

%token TRUE_TOK
%token FALSE_TOK
%token ITE_TOK
%token NOT_TOK
%token IMPLIES_TOK
%token IF_THEN_ELSE_TOK
%token AND_TOK
%token OR_TOK
%token XOR_TOK
%token IFF_TOK
%token EXISTS_TOK
%token FORALL_TOK
%token LET_TOK
%token FLET_TOK
%token NOTES_TOK
%token CVC_COMMAND_TOK
%token SORTS_TOK
%token FUNS_TOK
%token PREDS_TOK
%token EXTENSIONS_TOK
%token DEFINITION_TOK
%token AXIOMS_TOK
%token LOGIC_TOK
%token COLON_TOK
%token LBRACKET_TOK
%token RBRACKET_TOK
%token LCURBRACK_TOK
%token RCURBRACK_TOK
%token LPAREN_TOK
%token RPAREN_TOK
%token SAT_TOK
%token UNSAT_TOK
%token UNKNOWN_TOK
%token ASSUMPTION_TOK
%token FORMULA_TOK
%token STATUS_TOK
%token BENCHMARK_TOK
%token EXTRASORTS_TOK
%token EXTRAFUNS_TOK
%token EXTRAPREDS_TOK
%token LANGUAGE_TOK
%token DOLLAR_TOK
%token QUESTION_TOK
%token DISTINCT_TOK
%token SEMICOLON_TOK
%token EOF_TOK
%token PAT_TOK


%token BIT0_TOK
%token BIT1_TOK

%token BVCONCAT_TOK
%token BVEXTRACT_TOK

%token BVNOT_TOK
%token BVAND_TOK
%token BVOR_TOK
%token BVNEG_TOK
%token BVNAND_TOK
%token BVNOR_TOK
%token BVXOR_TOK
%token BVXNOR_TOK

%token EQ_TOK
%token BVCOMP_TOK
%token BVULT_TOK
%token BVULE_TOK
%token BVUGT_TOK
%token BVUGE_TOK
%token BVSLT_TOK
%token BVSLE_TOK
%token BVSGT_TOK
%token BVSGE_TOK

%token BVADD_TOK
%token BVSUB_TOK
%token BVMUL_TOK
%token BVUDIV_TOK
%token BVUREM_TOK
%token BVSDIV_TOK
%token BVSREM_TOK
%token BVSMOD_TOK
%token BVSHL_TOK
%token BVLSHR_TOK
%token BVASHR_TOK

%token REPEAT_TOK
%token ZEXT_TOK
%token SEXT_TOK
%token ROL_TOK
%token ROR_TOK

%%

cmd:
    benchmark
    {
      YYACCEPT;
    }
;

benchmark:
    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { }

  | EOF_TOK
    { 
      DONE = true;
    }
;

bench_name:
    SYM_TOK { }
;

bench_attributes:
    bench_attribute { }

  | bench_attributes bench_attribute { }
;

bench_attribute:
    COLON_TOK ASSUMPTION_TOK an_formula
    {
      ASSUMPTIONS.push_back($3);
    }

  | COLON_TOK FORMULA_TOK an_formula 
    {
      QUERYPARSED = true;
      QUERY = $3;
    }

  | COLON_TOK STATUS_TOK status { }

  | COLON_TOK LOGIC_TOK logic_name 
    {
      if (*$3 != "QF_BV" && *$3 != "QF_AUFBV" && *$3 != "QF_UFBV") {
	std::cerr << "ERROR: Logic " << *$3 << " not supported.";
	exit(1);
      }

      if (*$3 == "QF_AUFBV")
        ARRAYSENABLED = true;
    }
/*
  | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK
    { 
      // XXX?
    }
*/

  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK
    {
      PARSER->DeclareExpr(*$5, atoi($8->c_str()));
    }
/*
  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
    {
      //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
      //delete $4;
    }
*/
  | COLON_TOK NOTES_TOK STRING_TOK
    {  }

  | COLON_TOK CVC_COMMAND_TOK STRING_TOK
    {  }

  | annotation
    {  }
;


logic_name  :
    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
    {
      BVSIZE = atoi($3->c_str());
      delete $3;
      $$ = $1;
    }
  | SYM_TOK
    {
      $$ = $1;
    }
;

status:
    SAT_TOK { }
  | UNSAT_TOK { }
  | UNKNOWN_TOK { }
;

/*
sort_symbs:
    sort_symb 
    {
      $$ = new std::vector<CVC3::Expr>;
      $$->push_back(*$1);
      delete $1;
    }
  | sort_symbs sort_symb
    { 
      $1->push_back(*$2);
      $$ = $1;
      delete $2;
    }
;

fun_symb_decls:
    fun_symb_decl
    {
      $$ = new std::vector<CVC3::Expr>;
      $$->push_back(*$1);
      delete $1;
    }
  |
    fun_symb_decls fun_symb_decl
    {
      $1->push_back(*$2);
      $$ = $1;
      delete $2;
    }
;

fun_symb_decl:
    LPAREN_TOK fun_sig annotations
    {
      $$ = $2;
      delete $3;
    }
  | LPAREN_TOK fun_sig RPAREN_TOK
    {
      $$ = $2;
    }
;

fun_sig:
    fun_symb sort_symbs
    {
      if ($2->size() == 1) {
        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0]));
      }
      else {
        CVC3::Expr tmp(VC->listExpr("_ARROW", *$2));
        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp));
      }
      delete $1;
      delete $2;
    }
;

pred_symb_decls:
    pred_symb_decl
    {
      $$ = new std::vector<CVC3::Expr>;
      $$->push_back(*$1);
      delete $1;
    }
  |
    pred_symb_decls pred_symb_decl
    {
      $1->push_back(*$2);
      $$ = $1;
      delete $2;
    }
;

pred_symb_decl:
    LPAREN_TOK pred_sig annotations
    {
      $$ = $2;
      delete $3;
    }
  | LPAREN_TOK pred_sig RPAREN_TOK
    {
      $$ = $2;
    }
;

pred_sig:
    pred_symb sort_symbs
    {
      std::vector<CVC3::Expr> tmp(*$2);
      tmp.push_back(VC->idExpr("_BOOLEAN"));
      CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp));
      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2));
      delete $1;
      delete $2;
    }
  | pred_symb
    {
      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1),
                                       VC->idExpr("_BOOLEAN")));
      delete $1;
    }
;
*/


an_formulas:
    an_formula
    {
      $$ = new std::vector<klee::expr::ExprHandle>;
      $$->push_back($1);
    }
  |
    an_formulas an_formula
    {
      $1->push_back($2);
      $$ = $1;
    }
;


an_logical_formula:

    LPAREN_TOK NOT_TOK an_formula annotations
    {
      $$ = NotExpr::create($3);
    }

  | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
    {
      $$ = Expr::createImplies($3, $4);
    }

  | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations
    {
      $$ = SelectExpr::create($3, $4, $5);
    }

  | LPAREN_TOK AND_TOK an_formulas annotations
    {
      $$ = PARSER->CreateAnd(*$3);
    }

  | LPAREN_TOK OR_TOK an_formulas annotations
    {
      $$ = PARSER->CreateOr(*$3);
    }

  | LPAREN_TOK XOR_TOK an_formulas annotations
    {
      $$ = PARSER->CreateXor(*$3);
    }

  | LPAREN_TOK IFF_TOK an_formula an_formula annotations
    {
      $$ = EqExpr::create($3, $4);
    }
;


an_formula:
    an_atom
    {
      $$ = $1;
    }

  | an_logical_formula
    {
      $$ = $1;
    }

  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK
        { 
	  PARSER->PushVarEnv();
	  PARSER->AddVar(*$4, $5); 
	} 
    an_formula annotations
    {
      $$ = $8;
      PARSER->PopVarEnv();
    }

  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK 
        { 
	  PARSER->PushFVarEnv();
	  PARSER->AddFVar(*$4, $5); 
	} 
    an_formula annotations
    {
      $$ = $8;
      PARSER->PopFVarEnv();
    }
;



an_atom:
    prop_atom 
    {
      $$ = $1;
    }
  | LPAREN_TOK prop_atom annotations 
    {
      $$ = $2;
    }
  
  | an_pred
    {
      $$ = $1;
    }

/*
  | LPAREN_TOK DISTINCT_TOK an_terms annotations
    {
      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));

//       std::vector<CVC3::Expr> tmp;
//       tmp.push_back(*$2);
//       tmp.insert(tmp.end(), $3->begin(), $3->end());
//       $$ = new CVC3::Expr(VC->listExpr(tmp));
//       for (unsigned i = 0; i < (*$3).size(); ++i) {
//         tmp.push_back(($3)[i])
// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
// 	}
//       }
//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
      delete $3;
      delete $4;
    }
  | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
    {
      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
//       std::vector<CVC3::Expr> tmp;
//       for (unsigned i = 0; i < (*$3).size(); ++i) {
// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
// 	}
//       }
//       $$ = new CVC3::Expr(VC->listExpr("_AND", tmp));
      delete $3;
    }
*/
;

prop_atom:
    TRUE_TOK
    {
      $$ = ConstantExpr::create(1, 1);
    }

  | FALSE_TOK
    { 
      $$ = ConstantExpr::create(0, 1);;
    }

  | fvar
    {
      $$ = PARSER->GetFVar(*$1);
    }
;  


an_pred:
    LPAREN_TOK EQ_TOK an_term an_term annotations
    {
      $$ = EqExpr::create($3, $4);
    }

  | LPAREN_TOK BVULT_TOK an_term an_term annotations
    {
      $$ = UltExpr::create($3, $4);
    }

  | LPAREN_TOK BVULE_TOK an_term an_term annotations
    {
      $$ = UleExpr::create($3, $4);
    }

  | LPAREN_TOK BVUGT_TOK an_term an_term annotations
    {
      $$ = UgtExpr::create($3, $4);
    }

  | LPAREN_TOK BVUGE_TOK an_term an_term annotations
    {
      $$ = UgeExpr::create($3, $4);
    }

  | LPAREN_TOK BVSLT_TOK an_term an_term annotations
    {
      $$ = SltExpr::create($3, $4);
    }

  | LPAREN_TOK BVSLE_TOK an_term an_term annotations
    {
      $$ = SleExpr::create($3, $4);
    }

  | LPAREN_TOK BVSGT_TOK an_term an_term annotations
    {
      $$ = SgtExpr::create($3, $4);
    }

  | LPAREN_TOK BVSGE_TOK an_term an_term annotations
    {
      $$ = SgeExpr::create($3, $4);
    }
;


an_arithmetic_fun:

    LPAREN_TOK BVNEG_TOK an_term an_term annotations
    {
      $$ = NULL;  // XXX: not supported yet
    }

  | LPAREN_TOK BVADD_TOK an_term an_term annotations
    {
      $$ = AddExpr::create($3, $4);
    }

  | LPAREN_TOK BVSUB_TOK an_term an_term annotations
    {
      $$ = SubExpr::create($3, $4);
    }

  | LPAREN_TOK BVMUL_TOK an_term an_term annotations
    {
      $$ = MulExpr::create($3, $4);
    }

  | LPAREN_TOK BVUDIV_TOK an_term an_term annotations
    {
      $$ = UDivExpr::create($3, $4);
    }

  | LPAREN_TOK BVUREM_TOK an_term an_term annotations
    {
      $$ = URemExpr::create($3, $4);
    }

  | LPAREN_TOK BVSDIV_TOK an_term an_term annotations
    {
      $$ = SDivExpr::create($3, $4);
    }

  | LPAREN_TOK BVSREM_TOK an_term an_term annotations
    {
      $$ = SRemExpr::create($3, $4);
    }

  | LPAREN_TOK BVSMOD_TOK an_term an_term annotations
    {
      $$ = NULL; // XXX: not supported yet
    }
;


an_bitwise_fun:
    LPAREN_TOK BVNOT_TOK an_term annotations
    {
      $$ = NotExpr::create($3);
    }

  | LPAREN_TOK BVAND_TOK an_term an_term annotations
    {
      $$ = AndExpr::create($3, $4);
    }

  | LPAREN_TOK BVOR_TOK an_term an_term annotations
    {
      $$ = OrExpr::create($3, $4);
    }

  | LPAREN_TOK BVXOR_TOK an_term an_term annotations
    {
      $$ = XorExpr::create($3, $4);
    }

  | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
    {      
      $$ = NULL; // TODO
    }

  | LPAREN_TOK BVSHL_TOK an_term an_term annotations
    {
      $$ = ShlExpr::create($3, $4);
    }

  | LPAREN_TOK BVLSHR_TOK an_term an_term annotations
    {
      $$ = LShrExpr::create($3, $4);
    }

  | LPAREN_TOK BVASHR_TOK an_term an_term annotations
    {
      $$ = AShrExpr::create($3, $4);
    }

  | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      $$ = NULL; // TODO
    }

  | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      $$ = NULL; // TODO
    }
 
  | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      $$ = ZExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
    }

  | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      $$ = SExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
    }

  | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations
    {
      $$ = ConcatExpr::create($3, $4);
    }

  | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      $$ = NULL; // TODO
    }

  | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
    {
      int off = PARSER->StringToInt(*$6);
      $$ = ExtractExpr::create($8, off, PARSER->StringToInt(*$4) - off + 1);
    }
;


an_fun:
    an_logical_formula
    {
      $$ = $1;
    }

  | an_pred
    {
      $$ = $1;
    }

  | LPAREN_TOK BVCOMP_TOK an_term an_term annotations
    {
      $$ = EqExpr::create($3, $4);
    }
 
  | an_arithmetic_fun
    {
      $$ = $1;
    }

  | an_bitwise_fun
    {
      $$ = $1;
    }

/*
      else if (ARRAYSENABLED && *$1 == "select") {
        $$->push_back(VC->idExpr("_READ"));
      }
      else if (ARRAYSENABLED && *$1 == "store") {
        $$->push_back(VC->idExpr("_WRITE"));
      }
*/
;

constant:
    BIT0_TOK
    {
      $$ = PARSER->GetConstExpr("0", 2, 1);
    }

  | BIT1_TOK
    {
      $$ = PARSER->GetConstExpr("1", 2, 1);
    }

  | BVBIN_TOK
    {
      $$ = PARSER->GetConstExpr($1->substr(5), 2, $1->length()-5);
    }
  | BVHEX_TOK
    {
      $$ = PARSER->GetConstExpr($1->substr(5), 16, ($1->length()-5)*4);
    }
  | BV_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
    {
      $$ = PARSER->GetConstExpr($1->substr(2), 10, PARSER->StringToInt(*$3));
    }
;


an_term:
    basic_term 
    {
      $$ = $1;
    }
  | LPAREN_TOK basic_term annotations 
    {
      $$ = $2;
      delete $3;
    }

  | an_fun
    {
      $$ = $1;
    }

  | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations
    {
      $$ = SelectExpr::create($3, $4, $5);
    }
;


basic_term:
    constant 
    {
      $$ = $1;
    }

  | var
    {
      $$ = PARSER->GetVar(*$1);
    }
  | symb
    {
      std::cout << "SYMBOL " << *$1 << "\n";
      $$ = PARSER->GetVar(*$1);
    }
;



annotations:
    RPAREN_TOK { }
  | annotation annotations { }
;

annotation:
    attribute { }

  | attribute user_value {  }
;

user_value:
    USER_VAL_TOK  
    {
      delete $1;
    }
;

/*
sort_symb:
    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
    {
      if (BVENABLED && *$1 == "BitVec") {
        $$ = new CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)));
      }
      else {
        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3)));
      }
      delete $1;
      delete $3;
    }
  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
    {
      if (BVENABLED && ARRAYSENABLED && *$1 == "Array") {
        $$ = new CVC3::Expr(VC->listExpr("_ARRAY",
                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)),
                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$5))));
      }
      else {
        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5)));
      }
      delete $1;
      delete $3;
      delete $5;
    }
  | SYM_TOK 
    { 
      if (*$1 == "Real") {
	$$ = new CVC3::Expr(VC->idExpr("_REAL"));
      } else if (*$1 == "Int") {
	$$ = new CVC3::Expr(VC->idExpr("_INT"));
      } else {
	$$ = new CVC3::Expr(VC->idExpr(*$1));
      }
      delete $1;
    }
;

*/

/*
fun_symb:
    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
    {
      else if (BVENABLED &&
               $1->size() > 2 &&
               (*$1)[0] == 'b' &&
               (*$1)[1] == 'v') {
        int i = 2;
        while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
        if ((*$1)[i] == '\0') {
          $$->push_back(VC->idExpr("_BVCONST"));
          $$->push_back(VC->ratExpr($1->substr(2), 10));
        }
        else $$->push_back(VC->idExpr(*$1));
      }
      else $$->push_back(VC->idExpr(*$1));
      $$->push_back(VC->ratExpr(*$3));
      delete $1;
      delete $3;
    }
;
*/

attribute:
    COLON_TOK SYM_TOK
    {
      $$ = $2;
    }
;


var:
    QUESTION_TOK SYM_TOK
    {
      $$ = $2;
    }
;


fvar:
    DOLLAR_TOK SYM_TOK
    {
      $$ = $2;
    }
;

symb:
    SYM_TOK
    {
      $$ = $1;
    }

%%