diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 02:13:38 +0000 |
commit | b122cec27ca27d0b48e786191448e0053be78ed0 (patch) | |
tree | 615981d8623e830894f02fc528b173ac7461f934 /src/parser | |
parent | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff) |
Tuples and records merge. Resolves bug 270.
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 101 | ||||
-rw-r--r-- | src/parser/parser.cpp | 37 | ||||
-rw-r--r-- | src/parser/parser.h | 24 |
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 |