summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g5
-rw-r--r--src/parser/smt2/Smt2.g26
-rw-r--r--src/parser/smt2/smt2.cpp24
-rw-r--r--src/parser/smt2/smt2.h4
4 files changed, 53 insertions, 6 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index c497fcd0d..e6d7f9d86 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -931,7 +931,10 @@ toplevelDeclaration[CVC4::Command*& cmd]
* A bound variable declaration.
*/
boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
- : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
+@init {
+ Command* local_cmd = NULL;
+}
+ : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[local_cmd,t,ids,false]
;
/**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 38163c579..29d3e45b6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -749,7 +749,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
$cmd = new EmptyCommand();
}
| /* check-synth */
- CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+ CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet();PARSER_STATE->defineSygusFuns(); }
{ Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar));
std::vector<Expr> bodyv;
@@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
Debug("parser-sygus") << "...constructed exists " << body << std::endl;
}
- body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+ if( !PARSER_STATE->getSygusFunSymbols().empty() ){
+ body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+ }
Debug("parser-sygus") << "...constructed forall " << body << std::endl;
Command* c = new SetUserAttributeCommand("sygus", sygusVar);
c->setMuted(true);
@@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
std::string sname;
std::vector< Expr > let_vars;
bool readingLet = false;
+ std::string s;
}
: LPAREN_TOK
//read operator
@@ -799,6 +802,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
//since we enforce satisfaction completeness, immediately convert to total version
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+ }else if( k==CVC4::kind::BITVECTOR_UREM ){
+ k = CVC4::kind::BITVECTOR_UREM_TOTAL;
}
sgt.d_name = kind::kindToString(k);
sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -834,6 +839,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
k = PARSER_STATE->getOperatorKind(name);
if( k==CVC4::kind::BITVECTOR_UDIV ){
k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+ }else if( k==CVC4::kind::BITVECTOR_UREM ){
+ k = CVC4::kind::BITVECTOR_UREM_TOTAL;
}
sgt.d_name = kind::kindToString(k);
sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -890,6 +897,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
sgt.d_gterm_type = SygusGTerm::gterm_op;
}
+ | str[s,false]
+ { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl;
+ sgt.d_expr = MK_CONST( ::CVC4::String(s) );
+ sgt.d_name = s;
+ sgt.d_gterm_type = SygusGTerm::gterm_op;
+ }
| symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
{ if( readEnum ){
name = name + "__Enum__" + name2;
@@ -1594,6 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
Debug("parser") << "Empty set encountered: " << f << " "
<< f2 << " " << type << std::endl;
expr = MK_CONST( ::CVC4::EmptySet(type) );
+ } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) {
+ //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
+ //However, the expression has 0 children. So we convert to a SEP_NIL variable.
+ expr = EXPR_MANAGER->mkSepNil(type);
} else {
if(f.getType() != type) {
PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1898,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
| EMPTYSET_TOK
{ expr = MK_CONST( ::CVC4::EmptySet(Type())); }
+ | NILREF_TOK
+ { expr = MK_CONST( ::CVC4::NilRef(Type())); }
// NOTE: Theory constants go here
;
@@ -2633,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val';
INST_CLOSURE_TOK : 'inst-closure';
EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
// Other set theory operators are not
// tokenized and handled directly when
// processing a term
@@ -2773,7 +2793,7 @@ STRING_LITERAL_2_0
* will be part of the token text. Use the str[] parser rule instead.
*/
STRING_LITERAL_2_5
- : { PARSER_STATE->v2_5() }?=>
+ : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
'"' (~('"') | '""')* '"'
;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 463adcb54..9f3c43f09 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,16 @@ void Smt2::addFloatingPointOperators() {
Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
}
+void Smt2::addSepOperators() {
+ addOperator(kind::SEP_STAR, "sep");
+ addOperator(kind::SEP_PTO, "pto");
+ addOperator(kind::SEP_WAND, "wand");
+ addOperator(kind::SEP_EMP, "emp");
+ Parser::addOperator(kind::SEP_STAR);
+ Parser::addOperator(kind::SEP_PTO);
+ Parser::addOperator(kind::SEP_WAND);
+ Parser::addOperator(kind::SEP_EMP);
+}
void Smt2::addTheory(Theory theory) {
switch(theory) {
@@ -258,7 +268,11 @@ void Smt2::addTheory(Theory theory) {
defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
addFloatingPointOperators();
break;
-
+
+ case THEORY_SEP:
+ addSepOperators();
+ break;
+
default:
std::stringstream ss;
ss << "internal error: unsupported theory " << theory;
@@ -311,6 +325,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
return d_logic.isTheoryEnabled(theory::THEORY_UF);
case THEORY_FP:
return d_logic.isTheoryEnabled(theory::THEORY_FP);
+ case THEORY_SEP:
+ return d_logic.isTheoryEnabled(theory::THEORY_SEP);
default:
std::stringstream ss;
ss << "internal error: unsupported theory " << theory;
@@ -354,6 +370,8 @@ void Smt2::setLogic(std::string name) {
name = "UFLIRA";
} else if(name == "BV") {
name = "UFBV";
+ } else if(name == "SLIA") {
+ name = "UFSLIA";
} else if(name == "ALL_SUPPORTED") {
//no change
} else {
@@ -417,6 +435,10 @@ void Smt2::setLogic(std::string name) {
addTheory(THEORY_FP);
}
+ if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
+ addTheory(THEORY_SEP);
+ }
+
}/* Smt2::setLogic() */
void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1ae2c9dd7..b99e142ba 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -51,7 +51,8 @@ public:
THEORY_SETS,
THEORY_STRINGS,
THEORY_UF,
- THEORY_FP
+ THEORY_FP,
+ THEORY_SEP
};
private:
@@ -344,6 +345,7 @@ private:
void addFloatingPointOperators();
+ void addSepOperators();
};/* class Smt2 */
}/* CVC4::parser namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback