%{
/*****************************************************************************/
/*!
* \file smtlib.y
*
* Author: Clark Barrett
*
* Created: Apr 30 2005
*
*
*
* 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.
*
*
*
*/
/*****************************************************************************/
/*
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
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 *strvec;
CVC3::Expr *node;
std::vector *vec;
std::pair, std::vector > *pat_ann;
};
*/
%union {
std::string *str;
klee::expr::ExprHandle node;
};
%start cmd
/* strings are for better error messages.
"_TOK" is so macros don't conflict with kind names */
/*
%type bench_attributes sort_symbs fun_symb_decls pred_symb_decls
%type an_formulas quant_vars an_terms fun_symb patterns
%type pattern
%type benchmark bench_name bench_attribute
%type status fun_symb_decl fun_sig pred_symb_decl pred_sig
%type an_formula quant_var an_atom prop_atom
%type an_term basic_term sort_symb pred_symb
%type var fvar
%type logic_name quant_symb connective user_value attribute annotation
%type annotations
%type patterns_annotations
*/
%type an_formula an_logical_formula an_atom prop_atom
%type an_term basic_term constant
%type an_fun an_arithmetic_fun an_bitwise_fun
%type an_pred
%type logic_name status attribute user_value annotation annotations
%type var fvar symb
%token NUMERAL_TOK
%token SYM_TOK
%token STRING_TOK
%token AR_SYMB
%token USER_VAL_TOK
%token BV_TOK
%token BVBIN_TOK
%token 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;
$$->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;
$$->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;
$$->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 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;
$$->push_back(*$1);
delete $1;
}
|
an_formulas an_formula
{
$1->push_back(*$2);
$$ = $1;
delete $2;
}
;
*/
an_logical_formula:
LPAREN_TOK NOT_TOK an_formula annotations
{
//$$ = Expr::createNot($3);
$$ = NULL;
}
| 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_formula an_formula annotations
{
$$ = AndExpr::create($3, $4);
}
| LPAREN_TOK OR_TOK an_formula an_formula annotations
{
$$ = OrExpr::create($3, $4);
}
| LPAREN_TOK XOR_TOK an_formula an_formula annotations
{
$$ = XorExpr::create($3, $4);
}
| 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 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 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 an_term annotations
{
$$ = NULL; // XXX: not supported yet
}
| 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
{
$$ = NULL; // TODO
}
| LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
{
$$ = NULL; // TODO
}
| 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(*$4);
$$ = ExtractExpr::create($8, off, PARSER->StringToInt(*$6) - 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;
}
%%