diff options
| -rw-r--r-- | NEWS | 1 | ||||
| -rw-r--r-- | src/parser/cvc/Cvc.g | 39 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 19 | ||||
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 7 |
4 files changed, 53 insertions, 13 deletions
@@ -6,6 +6,7 @@ Changes since 1.4 * Support for unsat cores. * Simplification mode "incremental" no longer supported. * Support for array constants in constraints. +* Syntax for array models have changed in some language front-ends. Changes since 1.3 ================= diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 0a440f299..74c236dd1 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1368,14 +1368,6 @@ prefixFormula[CVC4::Expr& f] PARSER_STATE->preemptCommand(cmd); f = func; } - - /* array literals */ - | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN - 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()), ExprManager::VAR_FLAG_GLOBAL); - } ; instantiationPatterns[ CVC4::Expr& expr ] @@ -1898,7 +1890,7 @@ simpleTerm[CVC4::Expr& f] std::vector<std::string> names; Expr e; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; - Type t; + Type t, t2; } /* if-then-else */ : iteTerm[f] @@ -1928,7 +1920,6 @@ simpleTerm[CVC4::Expr& f] f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>()); } - /* empty set literal */ | LBRACE RBRACE { f = MK_CONST(EmptySet(Type())); } @@ -1942,6 +1933,32 @@ simpleTerm[CVC4::Expr& f] } } + /* array literals */ + | ARRAY_TOK /* { PARSER_STATE->pushScope(); } */ LPAREN + restrictedType[t, CHECK_DECLARED] OF_TOK restrictedType[t2, CHECK_DECLARED] + RPAREN COLON simpleTerm[f] + { /* Eventually if we support a bound var (like a lambda) for array + * literals, we can use the push/pop scope. */ + /* PARSER_STATE->popScope(); */ + t = EXPR_MANAGER->mkArrayType(t, t2); + if(!f.isConst()) { + std::stringstream ss; + ss << "expected constant term inside array constant, but found " + << "nonconstant term" << std::endl + << "the term: " << f; + PARSER_STATE->parseError(ss.str()); + } + if(!t2.isComparableTo(f.getType())) { + std::stringstream ss; + ss << "type mismatch inside array constant term:" << std::endl + << "array type: " << t << std::endl + << "expected const type: " << t2 << std::endl + << "computed const type: " << f.getType(); + PARSER_STATE->parseError(ss.str()); + } + f = MK_CONST( ArrayStoreAll(t, f) ); + } + /* boolean literals */ | TRUE_TOK { f = MK_CONST(bool(true)); } | FALSE_TOK { f = MK_CONST(bool(false)); } @@ -1986,7 +2003,7 @@ simpleTerm[CVC4::Expr& f] ; /** - * Matches (and performs) a type ascription. + * Matches a type ascription. * The f arg is the term to check (it is an input-only argument). */ typeAscription[const CVC4::Expr& f, CVC4::Type& t] diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4491e5643..6a98755f2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1010,10 +1010,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] RPAREN_TOK term[f, f2] RPAREN_TOK { if(!type.isArray()) { - PARSER_STATE->parseError("(as const...) type ascription can only be used for array sorts."); + std::stringstream ss; + ss << "expected array constant term, but cast is not of array type" << std::endl + << "cast type: " << type; + PARSER_STATE->parseError(ss.str()); + } + if(!f.isConst()) { + std::stringstream ss; + ss << "expected constant term inside array constant, but found " + << "nonconstant term:" << std::endl + << "the term: " << f; + PARSER_STATE->parseError(ss.str()); } if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) { - PARSER_STATE->parseError("type of the array cast is not compatible with term."); + std::stringstream ss; + ss << "type mismatch inside array constant term:" << std::endl + << "array type: " << type << std::endl + << "expected const type: " << ArrayType(type).getConstituentType() << std::endl + << "computed const type: " << f.getType(); + PARSER_STATE->parseError(ss.str()); } expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) ); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 9b3e83578..2d89d3aff 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -168,6 +168,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; } + case kind::STORE_ALL: { + const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); + out << "ARRAY(" << asa.getType().getIndexType() << " OF " + << asa.getType().getConstituentType() << ") : " << asa.getExpr(); + break; + } + default: // fall back on whatever operator<< does on underlying type; we // might luck out and print something reasonable |