summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g101
-rw-r--r--src/parser/parser.cpp37
-rw-r--r--src/parser/parser.h24
3 files changed, 34 insertions, 128 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 18dfcd473..c82a984d2 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -11,7 +11,7 @@
**
** \brief Parser for CVC presentation input language
**
- ** Parser for CVC input language.
+ ** Parser for CVC presentation input language.
**/
grammar Cvc;
@@ -866,7 +866,7 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
// NOTE: do not clear the vectors here!
}
: identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
- { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t);
+ { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t, false);
terms.insert(terms.end(), vars.begin(), vars.end());
for(unsigned i = 0; i < vars.size(); ++i) {
types.push_back(t);
@@ -957,7 +957,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
}
} else {
Debug("parser") << " " << *i << " not declared" << std::endl;
- Expr func = PARSER_STATE->mkVar(*i, t);
+ Expr func = PARSER_STATE->mkVar(*i, t, true);
if(topLevel) {
Command* decl = new DeclareFunctionCommand(*i, func, t);
seq->addCommand(decl);
@@ -977,7 +977,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
i != i_end;
++i) {
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
- Expr func = EXPR_MANAGER->mkVar(*i, t);
+ Expr func = EXPR_MANAGER->mkVar(*i, t, true);
PARSER_STATE->defineFunction(*i, f);
Command* decl = new DefineFunctionCommand(*i, func, f);
seq->addCommand(decl);
@@ -1176,14 +1176,14 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
}
} else {
// tuple type [ T, U, V... ]
- t = PARSER_STATE->mkTupleType(types);
+ t = EXPR_MANAGER->mkTupleType(types);
}
}
/* record types */
| SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ
- { t = PARSER_STATE->mkRecordType(typeIds); }
+ { t = EXPR_MANAGER->mkRecordType(typeIds); }
/* bitvector types */
| BITVECTOR_TOK LPAREN k=numeral RPAREN
@@ -1340,7 +1340,7 @@ prefixFormula[CVC4::Expr& f]
boundVarDecl[ids,t] RPAREN COLON formula[f]
{ PARSER_STATE->popScope();
UNSUPPORTED("array literals not supported yet");
- f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()));
+ f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType()), true);
}
;
@@ -1489,30 +1489,16 @@ tupleStore[CVC4::Expr& f]
: k=numeral ASSIGN_TOK uminusTerm[f2]
{
Type t = f.getType();
- if(! t.isDatatype()) {
+ if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-update applied to non-tuple");
}
- Datatype tuple = DatatypeType(f.getType()).getDatatype();
- if(tuple.getName() != "__cvc4_tuple") {
- PARSER_STATE->parseError("tuple-update applied to non-tuple");
- }
- if(k < tuple[0].getNumArgs()) {
- std::vector<Expr> args;
- for(unsigned i = 0; i < tuple[0].getNumArgs(); ++i) {
- if(i == k) {
- args.push_back(f2);
- } else {
- Expr selectorOp = tuple[0][i].getSelector();
- Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- args.push_back(select);
- }
- }
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, tuple[0].getConstructor(), args);
- } else {
+ size_t length = TupleType(t).getLength();
+ if(k >= length) {
std::stringstream ss;
- ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot update index " << k;
+ ss << "tuple is of length " << length << "; cannot update index " << k;
PARSER_STATE->parseError(ss.str());
}
+ f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2);
}
;
@@ -1528,31 +1514,15 @@ recordStore[CVC4::Expr& f]
: identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
{
Type t = f.getType();
- if(! t.isDatatype()) {
- PARSER_STATE->parseError("record-update applied to non-record");
- }
- Datatype record = DatatypeType(f.getType()).getDatatype();
- if(record.getName() != "__cvc4_record") {
+ if(! t.isRecord()) {
PARSER_STATE->parseError("record-update applied to non-record");
}
- const DatatypeConstructorArg* updateArg = 0;
- try {
- updateArg = &record[0][id];
- } catch(IllegalArgumentException& e) {
+ const Record& rec = RecordType(t).getRecord();
+ Record::const_iterator fld = rec.find(id);
+ if(fld == rec.end()) {
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
- std::vector<Expr> args;
- for(unsigned i = 0; i < record[0].getNumArgs(); ++i) {
- const DatatypeConstructorArg* thisArg = &record[0][i];
- if(thisArg == updateArg) {
- args.push_back(f2);
- } else {
- Expr selectorOp = record[0][i].getSelector();
- Expr select = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- args.push_back(select);
- }
- }
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, record[0].getConstructor(), args);
+ f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2);
}
;
@@ -1667,37 +1637,28 @@ postfixTerm[CVC4::Expr& f]
| DOT
( identifier[id,CHECK_NONE,SYM_VARIABLE]
{ Type t = f.getType();
- if(! t.isDatatype()) {
+ if(! t.isRecord()) {
PARSER_STATE->parseError("record-select applied to non-record");
}
- Datatype record = DatatypeType(f.getType()).getDatatype();
- if(record.getName() != "__cvc4_record") {
- PARSER_STATE->parseError("record-select applied to non-record");
- }
- try {
- Expr selectorOp = record[0][id].getSelector();
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- } catch(IllegalArgumentException& e) {
+ const Record& rec = RecordType(t).getRecord();
+ Record::const_iterator fld = rec.find(id);
+ if(fld == rec.end()) {
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
+ f = MK_EXPR(MK_CONST(RecordSelect(id)), f);
}
| k=numeral
{ Type t = f.getType();
- if(! t.isDatatype()) {
- PARSER_STATE->parseError("tuple-select applied to non-tuple");
- }
- Datatype tuple = DatatypeType(f.getType()).getDatatype();
- if(tuple.getName() != "__cvc4_tuple") {
+ if(! t.isTuple()) {
PARSER_STATE->parseError("tuple-select applied to non-tuple");
}
- try {
- Expr selectorOp = tuple[0][k].getSelector();
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, selectorOp, f);
- } catch(IllegalArgumentException& e) {
+ size_t length = TupleType(t).getLength();
+ if(k >= length) {
std::stringstream ss;
- ss << "tuple is of length " << tuple[0].getNumArgs() << "; cannot access index " << k;
+ ss << "tuple is of length " << length << "; cannot access index " << k;
PARSER_STATE->parseError(ss.str());
}
+ f = MK_EXPR(MK_CONST(TupleSelect(k)), f);
}
)
)*
@@ -1871,8 +1832,8 @@ simpleTerm[CVC4::Expr& f]
for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
types.push_back((*i).getType());
}
- DatatypeType t = PARSER_STATE->mkTupleType(types);
- f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
+ TupleType t = EXPR_MANAGER->mkTupleType(types);
+ f = MK_EXPR(kind::TUPLE, args);
}
}
@@ -1902,8 +1863,8 @@ simpleTerm[CVC4::Expr& f]
for(unsigned i = 0; i < names.size(); ++i) {
typeIds.push_back(std::make_pair(names[i], args[i].getType()));
}
- DatatypeType t = PARSER_STATE->mkRecordType(typeIds);
- f = EXPR_MANAGER->mkExpr(kind::APPLY_CONSTRUCTOR, t.getDatatype()[0].getConstructor(), args);
+ RecordType t = EXPR_MANAGER->mkRecordType(typeIds);
+ f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), args);
}
/* variable / zero-ary constructor application */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index ef386f57e..10ca16001 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -138,8 +138,8 @@ bool Parser::isPredicate(const std::string& name) {
Expr
Parser::mkVar(const std::string& name, const Type& type,
bool levelZero) {
- Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
- Expr expr = d_exprManager->mkVar(name, type);
+ Debug("parser") << "mkVar(" << name << ", " << type << ", " << levelZero << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
defineVar(name, expr, levelZero);
return expr;
}
@@ -156,7 +156,7 @@ Expr
Parser::mkFunction(const std::string& name, const Type& type,
bool levelZero) {
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
- Expr expr = d_exprManager->mkVar(name, type);
+ Expr expr = d_exprManager->mkVar(name, type, levelZero);
defineFunction(name, expr, levelZero);
return expr;
}
@@ -339,37 +339,6 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
return types;
}
-DatatypeType Parser::mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds) {
- DatatypeType& dtt = d_recordTypes[typeIds];
- if(dtt.isNull()) {
- Datatype dt("__cvc4_record");
-Debug("datatypes") << "make new record_ctor" << std::endl;
- DatatypeConstructor c("__cvc4_record_ctor");
- for(std::vector< std::pair<std::string, Type> >::const_iterator i = typeIds.begin(); i != typeIds.end(); ++i) {
- c.addArg((*i).first, (*i).second);
- }
- dt.addConstructor(c);
- dtt = d_exprManager->mkDatatypeType(dt);
- } else {
-Debug("datatypes") << "use old record_ctor" << std::endl;
-}
- return dtt;
-}
-
-DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
- DatatypeType& dtt = d_tupleTypes[types];
- if(dtt.isNull()) {
- Datatype dt("__cvc4_tuple");
- DatatypeConstructor c("__cvc4_tuple_ctor");
- for(std::vector<Type>::const_iterator i = types.begin(); i != types.end(); ++i) {
- c.addArg("__cvc4_tuple_stor", *i);
- }
- dt.addConstructor(c);
- dtt = d_exprManager->mkDatatypeType(dt);
- }
- return dtt;
-}
-
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index eb76900d2..eed8531a5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -141,20 +141,6 @@ class CVC4_PUBLIC Parser {
/** Are we only parsing? */
bool d_parseOnly;
- /**
- * We might see the same record type multiple times; we have
- * to match always to the same Type. This map contains all the
- * record types we have.
- */
- std::map<std::vector< std::pair<std::string, Type> >, DatatypeType> d_recordTypes;
-
- /**
- * We might see the same tuple type multiple times; we have
- * to match always to the same Type. This map contains all the
- * tuple types we have.
- */
- std::map<std::vector<Type>, DatatypeType> d_tupleTypes;
-
/** The set of operators available in the current logic. */
std::set<Kind> d_logicOperators;
@@ -420,16 +406,6 @@ public:
mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
/**
- * Create a record type, or if there's already a matching one, return that one.
- */
- DatatypeType mkRecordType(const std::vector< std::pair<std::string, Type> >& typeIds);
-
- /**
- * Create a tuple type, or if there's already a matching one, return that one.
- */
- DatatypeType mkTupleType(const std::vector<Type>& types);
-
- /**
* Add an operator to the current legal set.
*
* @param kind the built-in operator to add
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback