summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g211
-rw-r--r--src/parser/parser.cpp15
-rw-r--r--src/parser/parser.h14
3 files changed, 138 insertions, 102 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 794f0a670..543538f32 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -88,6 +88,7 @@ tokens {
BAR = '|';
DOT = '.';
DOTDOT = '..';
+ UNDERSCORE = '_';
SQHASH = '[#';
HASHSQ = '#]';
@@ -349,6 +350,14 @@ Expr createPrecedenceTree(ExprManager* em,
return e;
}
+/** Add n NOTs to the front of e and return the result. */
+Expr addNots(ExprManager* em, size_t n, Expr e) {
+ while(n-- > 0) {
+ e = em->mkExpr(kind::NOT, e);
+ }
+ return e;
+}
+
}/* @parser::members */
@header {
@@ -480,6 +489,7 @@ command returns [CVC4::Command* cmd = 0]
{ PARSER_STATE->popScope();
cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
| toplevelDeclaration[cmd]
+ | SEMICOLON c=command { $cmd = c; }
| EOF
;
@@ -710,7 +720,6 @@ type[CVC4::Type& t,
} else {
args.push_back(t);
}
- Debug("parser") << "type: " << t << std::endl;
}
( ARROW_TOK type[t2,check] { args.push_back(t2); } )?
{ if(t2.isNull()) {
@@ -783,9 +792,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
t = Type(); }
/* subrange types */
- | LBRACKET bound DOTDOT bound RBRACKET
+/* parsing not working -- some kind of conflict betw [0..1] and 0.0
+ | bounds
{ PARSER_STATE->unimplementedFeature("subranges not supported yet");
t = Type(); }
+*/
/* tuple types / old-style function types */
| LBRACKET type[t,check] { types.push_back(t); }
@@ -828,12 +839,6 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
}
;
-bound
- : '_'
- | numeral
- | MINUS_TOK numeral
- ;
-
/**
* Matches a type identifier. Returns the identifier. If the type is
* declared, returns the Type in the 't' parameter; otherwise a null
@@ -873,6 +878,52 @@ typeLetDecl[CVC4::parser::DeclarationCheck check]
formula[CVC4::Expr& f]
@init {
Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ Expr f2;
+ std::vector<CVC4::Expr> expressions;
+ std::vector<unsigned> operators;
+ unsigned op;
+}
+ : n=nots
+ ( prefixFormula[f]
+ { f = addNots(EXPR_MANAGER, n, f); }
+ | comparison[f]
+ { f = addNots(EXPR_MANAGER, n, f);
+ expressions.push_back(f);
+ }
+ i=morecomparisons[expressions,operators]?
+ { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
+ )
+ ;
+
+morecomparisons[std::vector<CVC4::Expr>& expressions,
+ std::vector<unsigned>& operators] returns [size_t i]
+@init {
+ unsigned op;
+ Expr f;
+ $i = expressions.size();
+}
+ : booleanBinop[op] { operators.push_back(op); }
+ n=nots
+ ( prefixFormula[f]
+ { expressions.push_back(addNots(EXPR_MANAGER, n, f)); }
+ | comparison[f]
+ { f = addNots(EXPR_MANAGER, n, f);
+ expressions.push_back(f);
+ }
+ inner=morecomparisons[expressions,operators]?
+ )
+ ;
+
+/** Matches 0 or more NOTs. */
+nots returns [size_t n]
+@init {
+ $n = 0;
+}
+ : ( NOT_TOK { ++$n; } )*
+ ;
+
+prefixFormula[CVC4::Expr& f]
+@init {
std::vector<std::string> ids;
std::vector<Expr> terms;
std::vector<Type> types;
@@ -894,20 +945,20 @@ formula[CVC4::Expr& f]
f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
}
- /* lets: letDecl defines the variables and functionss, we just
+ /* lets: letDecl defines the variables and functionss, we just
* manage the scopes here. NOTE that LET in the CVC language is
* always sequential! */
| LET_TOK { PARSER_STATE->pushScope(); }
letDecl ( COMMA letDecl )*
IN_TOK formula[f] { PARSER_STATE->popScope(); }
- /* lambda */
+ /* lambda */
| LAMBDA { PARSER_STATE->pushScope(); } LPAREN
boundVarDeclsReturn[terms,types]
RPAREN COLON formula[f]
{ PARSER_STATE->popScope();
Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
- Expr func = PARSER_STATE->mkFunction("anonymous", t);
+ Expr func = PARSER_STATE->mkAnonymousFunction("lambda", t);
Command* cmd = new DefineFunctionCommand(func, terms, f);
PARSER_STATE->preemptCommand(cmd);
f = func;
@@ -920,9 +971,6 @@ formula[CVC4::Expr& f]
PARSER_STATE->unimplementedFeature("array literals not supported yet");
f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()));
}
-
- /* everything else */
- | booleanFormula[f]
;
instantiationPatterns
@@ -949,36 +997,6 @@ letDecl
}
;
-booleanFormula[CVC4::Expr& f]
-@init {
- std::vector<CVC4::Expr> expressions;
- std::vector<unsigned> operators;
- unsigned op;
- unsigned notCount = 0;
-}
- : ( NOT_TOK { ++notCount; } )* comparison[f]
- { while(notCount > 0) {
- --notCount;
- f = EXPR_MANAGER->mkExpr(kind::NOT, f);
- }
- expressions.push_back(f);
- Assert(notCount == 0);
- }
- ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f]
- { while(notCount > 0) {
- --notCount;
- f = EXPR_MANAGER->mkExpr(kind::NOT, f);
- }
- operators.push_back(op);
-# warning cannot do NOT FORALL or TRUE AND FORALL, or..
- expressions.push_back(f);
- Assert(notCount == 0);
- }
- )*
- { Assert(notCount == 0);
- f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
- ;
-
booleanBinop[unsigned& op]
@init {
op = LT(1)->getType(LT(1));
@@ -1089,17 +1107,19 @@ bvNegTerm[CVC4::Expr& f]
;
/**
- * Parses an array select / bitvector extract / bitvector shift.
- * These are all parsed the same way because they are all effectively
- * post-fix operators and can continue piling onto an expression.
- * Array selects and bitvector extracts even share similar syntax with
- * their use of [ square brackets ], so we left-factor as much out as
- * possible to make ANTLR happy.
+ * Parses an array select / bitvector extract / bitvector shift /
+ * function or constructor application. These are all parsed the same
+ * way because they are all effectively post-fix operators and can
+ * continue piling onto an expression. Array selects and bitvector
+ * extracts even share similar syntax with their use of [ square
+ * brackets ], so we left-factor as much out as possible to make ANTLR
+ * happy.
*/
selectExtractShift[CVC4::Expr& f]
@init {
Expr f2;
bool extract, left;
+ std::vector<Expr> args;
}
: bvTerm[f]
( /* array select / bitvector extract */
@@ -1115,6 +1135,8 @@ selectExtractShift[CVC4::Expr& f]
f = MK_EXPR(CVC4::kind::SELECT, f, f2);
}
}
+
+ /* left- or right-shift */
| ( LEFTSHIFT_TOK { left = true; }
| RIGHTSHIFT_TOK { left = false; } ) k=numeral
{ // Defined in:
@@ -1127,6 +1149,29 @@ selectExtractShift[CVC4::Expr& f]
MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
}
}
+
+ /* function/constructor application */
+ | LPAREN { args.push_back(f); }
+ formula[f] { args.push_back(f); }
+ ( COMMA formula[f] { args.push_back(f); } )* RPAREN
+ // TODO: check arity
+ { Type t = args.front().getType();
+ Debug("parser") << "type is " << t << std::endl;
+ Debug("parser") << "expr is " << args.front() << std::endl;
+ if(PARSER_STATE->isDefinedFunction(args.front())) {
+ f = MK_EXPR(CVC4::kind::APPLY, args);
+ } else if(t.isFunction()) {
+ f = MK_EXPR(CVC4::kind::APPLY_UF, args);
+ } else if(t.isConstructor()) {
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ } else if(t.isSelector()) {
+ f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
+ } else if(t.isTester()) {
+ f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
+ } else {
+ Unhandled(t);
+ }
+ }
)*
;
@@ -1135,15 +1180,15 @@ bvTerm[CVC4::Expr& f]
Expr f2;
}
/* BV xor */
- : BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); }
- | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); }
- | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); }
- | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
- | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
+ | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
/* BV unary minus */
@@ -1159,7 +1204,7 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV subtraction */
@@ -1172,12 +1217,12 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV multiplication */
| BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN
- { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
+ { f = MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2);
if(k == 0) {
PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0");
}
@@ -1185,7 +1230,7 @@ bvTerm[CVC4::Expr& f]
if(k > size) {
f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f);
} else if(k < size) {
- f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f);
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k - 1, 0)), f);
}
}
/* BV unsigned division */
@@ -1271,44 +1316,8 @@ simpleTerm[CVC4::Expr& f]
std::vector<Expr> args;
Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- /* function/constructor application */
- : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { Debug("parser") << " at level " << PARSER_STATE->getDeclarationLevel() << std::endl;
- Debug("parser") << " isFunction " << PARSER_STATE->isFunctionLike(name) << std::endl;
- Debug("parser") << " isDefinedFunction " << PARSER_STATE->isDefinedFunction(name) << std::endl;
- Debug("parser") << " name " << name << std::endl;
- Debug("parser") << " isDeclared " << PARSER_STATE->isDeclared(name) << std::endl;
- Debug("parser") << " getType " << PARSER_STATE->getType(name) << std::endl;
- PARSER_STATE->checkFunctionLike(name);
- f = PARSER_STATE->getVariable(name);
- args.push_back(f);
- }
- LPAREN formula[f] { args.push_back(f); }
- ( COMMA formula[f] { args.push_back(f); } )* RPAREN
- // TODO: check arity
- { Type t = args.front().getType();
- Debug("parser") << "type is " << t << std::endl;
- Debug("parser") << "expr is " << args.front() << std::endl;
- if(PARSER_STATE->isDefinedFunction(name)) {
- f = MK_EXPR(CVC4::kind::APPLY, args);
- } else if(t.isFunction()) {
- f = MK_EXPR(CVC4::kind::APPLY_UF, args);
- } else if(t.isConstructor()) {
- Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl;
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
- } else if(t.isSelector()) {
- Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl;
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
- } else if(t.isTester()) {
- Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl;
- f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
- } else {
- Unhandled(t);
- }
- }
-
/* if-then-else */
- | iteTerm[f]
+ : iteTerm[f]
/* parenthesized sub-formula / tuple literals */
| LPAREN formula[f] { args.push_back(f); }
@@ -1345,9 +1354,11 @@ simpleTerm[CVC4::Expr& f]
| identifier[name,CHECK_DECLARED,SYM_VARIABLE]
{ f = PARSER_STATE->getVariable(name);
// datatypes: zero-ary constructors
- if(PARSER_STATE->getType(name).isConstructor()) {
- args.push_back(f);
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
+ Type t = PARSER_STATE->getType(name);
+ if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
+ // don't require parentheses, immediately turn it into an
+ // apply
+ f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
}
}
;
@@ -1475,7 +1486,7 @@ numeral returns [unsigned k]
/**
* Matches a decimal literal.
*/
-DECIMAL_LITERAL: DIGIT+ '.' DIGIT+;
+DECIMAL_LITERAL: DIGIT+ DOT DIGIT+;
/**
* Matches a hexadecimal constant.
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 19d1bbcb8..29ade43c1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -45,6 +45,7 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool par
d_input(input),
d_declScopeAllocated(),
d_declScope(&d_declScopeAllocated),
+ d_anonymousFunctionCount(0),
d_done(false),
d_checksEnabled(true),
d_strictMode(strictMode),
@@ -117,6 +118,13 @@ bool Parser::isDefinedFunction(const std::string& name) {
return d_declScope->isBoundDefinedFunction(name);
}
+/* Returns true if the Expr is a defined function. */
+bool Parser::isDefinedFunction(Expr func) {
+ // more permissive in type than isFunction(), because defined
+ // functions can be zero-ary and declared functions cannot.
+ return d_declScope->isBoundDefinedFunction(func);
+}
+
/* Returns true if name is bound to a function returning boolean. */
bool Parser::isPredicate(const std::string& name) {
return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
@@ -138,6 +146,13 @@ Parser::mkFunction(const std::string& name, const Type& type) {
return expr;
}
+Expr
+Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
+ stringstream name;
+ name << prefix << ':' << ++d_anonymousFunctionCount;
+ return mkFunction(name.str(), type);
+}
+
std::vector<Expr>
Parser::mkVars(const std::vector<std::string> names,
const Type& type) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 25fb30be6..033abb42a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -125,8 +125,8 @@ class CVC4_PUBLIC Parser {
*/
DeclarationScope* d_declScope;
- /** The name of the input file. */
-// std::string d_filename;
+ /** How many anonymous functions we've created. */
+ size_t d_anonymousFunctionCount;
/** Are we done */
bool d_done;
@@ -322,6 +322,13 @@ public:
/** Create a new CVC4 function expression of the given type. */
Expr mkFunction(const std::string& name, const Type& type);
+ /**
+ * Create a new CVC4 function expression of the given type,
+ * appending a unique index to its name. (That's the ONLY
+ * difference between mkAnonymousFunction() and mkFunction()).
+ */
+ Expr mkAnonymousFunction(const std::string& prefix, const Type& type);
+
/** Create a new variable definition (e.g., from a let binding). */
void defineVar(const std::string& name, const Expr& val);
@@ -394,6 +401,9 @@ public:
/** Is the symbol bound to a defined function? */
bool isDefinedFunction(const std::string& name);
+ /** Is the Expr a defined function? */
+ bool isDefinedFunction(Expr func);
+
/** Is the symbol bound to a predicate? */
bool isPredicate(const std::string& name);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback