From: Andrew Reynolds Date: Tue, 6 Aug 2019 22:18:50 +0000 (-0500) Subject: Properly parse qualified identifiers (#3111) X-Git-Tag: cvc5-1.0.0~4040 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f06ea7c4de13e5729885fdfdf5289ee522bb5fa2;p=cvc5.git Properly parse qualified identifiers (#3111) --- diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index dec4ebc97..c8e09b8e0 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -110,7 +110,7 @@ Expr Parser::getExpressionForName(const std::string& name) { } Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { - assert( isDeclared(name) ); + assert(isDeclared(name)); // first check if the variable is declared and not overloaded Expr expr = getVariable(name); if(expr.isNull()) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 663594ce8..2a736402e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1860,17 +1860,50 @@ symbolicExpr[CVC4::SExpr& sexpr] /** * Matches a term. - * @return the expression representing the formula + * @return the expression representing the term. */ term[CVC4::Expr& expr, CVC4::Expr& expr2] @init { + Kind kind = kind::NULL_EXPR; + Expr f; std::string name; + Type type; } : termNonVariable[expr, expr2] - /* a variable */ - | symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { expr = PARSER_STATE->getExpressionForName(name); - assert( !expr.isNull() ); + + // a qualified identifier (section 3.6 of SMT-LIB version 2.6) + + | qualIdentifier[kind,name,f,type] + { + if (kind != kind::NULL_EXPR || !type.isNull()) + { + PARSER_STATE->parseError( + "Bad syntax for qualified identifier operator in term position."); + } + else if (!f.isNull()) + { + expr = f; + } + else if (!PARSER_STATE->isDeclared(name,SYM_VARIABLE)) + { + if (PARSER_STATE->sygus_v1() && name[0] == '-' + && name.find_first_not_of("0123456789", 1) == std::string::npos) + { + // allow unary minus in sygus version 1 + expr = MK_CONST(Rational(name)); + } + else + { + std::stringstream ss; + ss << "Symbol " << name << " is not declared."; + PARSER_STATE->parseError(ss.str()); + } + } + else + { + expr = PARSER_STATE->getExpressionForName(name); + } + assert(!expr.isNull()); } ; @@ -1883,11 +1916,13 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind = kind::NULL_EXPR; - Expr op; + Kind qkind = kind::NULL_EXPR; std::string name; std::vector args; std::vector< std::pair > sortedVarNames; Expr f, f2, f3; + Expr qexpr; + Type qtype; std::string attr; Expr attexpr; std::vector patexprs; @@ -1896,56 +1931,13 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] std::vector< std::pair > binders; bool isBuiltinOperator = false; bool isOverloadedFunction = false; - bool readVariable = false; int match_vindex = -1; std::vector match_ptypes; Type type; Type type2; api::Term atomTerm; } - : LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) - sortSymbol[type, CHECK_DECLARED] RPAREN_TOK - { - if(readVariable) { - Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl; - // get the variable expression for the type - f = PARSER_STATE->getExpressionForNameAndType(name, type); - assert( !f.isNull() ); - } - if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) { - // could be a parametric type constructor or just an overloaded constructor - if(((DatatypeType)type).isParametric()) { - std::vector v; - Expr e = f.getOperator(); - const DatatypeConstructor& dtc = - Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() )); - v.insert(v.end(), f.begin(), f.end()); - expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); - }else{ - expr = f; - } - } else if(f.getKind() == CVC4::kind::EMPTYSET) { - Debug("parser") << "Empty set encountered: " << f << " " - << f2 << " " << type << std::endl; - expr = MK_CONST( ::CVC4::EmptySet(type) ); - } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { - expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET); - } else if(f.getKind() == CVC4::kind::SEP_NIL) { - //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->mkNullaryOperator(type, kind::SEP_NIL); - } else { - if(f.getType() != type) { - PARSER_STATE->parseError("Type ascription not satisfied."); - }else{ - expr = f; - } - } - } - | LPAREN_TOK quantOp[kind] + : LPAREN_TOK quantOp[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK { PARSER_STATE->pushScope(true); @@ -1982,31 +1974,62 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - | LPAREN_TOK functionName[name, CHECK_NONE] - { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); - if(isBuiltinOperator) { - /* A built-in operator */ - kind = PARSER_STATE->getOperatorKind(name); - } else { - /* A non-built-in function application */ - PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE); - expr = PARSER_STATE->getVariable(name); - if(!expr.isNull()) { - PARSER_STATE->checkFunctionLike(expr); - kind = PARSER_STATE->getKindForFunction(expr); - args.push_back(expr); - }else{ - isOverloadedFunction = true; + | LPAREN_TOK qualIdentifier[qkind,name,qexpr,qtype] + { + // process the operator + Debug("parser") << "Parsed qual id: " << qkind << "/" << name << "/" + << qexpr << "/" << qtype << std::endl; + if (qkind != kind::NULL_EXPR) + { + // It is a special case, e.g. tupSel or array constant specification. + // We have to wait until the arguments are parsed to resolve it. + } + else if (!qexpr.isNull()) + { + // An explicit operator, e.g. an indexed symbol. + args.push_back(qexpr); + if (qexpr.getType().isTester()) + { + kind = kind::APPLY_TESTER; + } + } + else + { + isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); + if (isBuiltinOperator) + { + // a builtin operator, convert to kind + kind = PARSER_STATE->getOperatorKind(name); + } + else + { + // A non-built-in function application, get the expression + PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE); + expr = PARSER_STATE->getVariable(name); + if (!expr.isNull()) + { + PARSER_STATE->checkFunctionLike(expr); + kind = PARSER_STATE->getKindForFunction(expr); + args.push_back(expr); + } + else + { + // Could not find the expression. It may be an overloaded symbol, + // in which case we may find it after knowing the types of its + // arguments. + isOverloadedFunction = true; + } } } } - //(termList[args,expr])? RPAREN_TOK termList[args,expr] RPAREN_TOK { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl; for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { Debug("parser") << "++ " << *i << std::endl; } + // We now can figure out what the operator is, if we guessed it was + // overloaded. if(isOverloadedFunction) { std::vector< Type > argTypes; for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { @@ -2021,10 +2044,79 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types."); } } - - bool done = false; - if (isBuiltinOperator) + // handle special cases + if (qkind == kind::STORE_ALL) { + if (args.size() != 1) + { + PARSER_STATE->parseError("Too many arguments to array constant."); + } + if (!args[0].isConst()) + { + std::stringstream ss; + ss << "expected constant term inside array constant, but found " + << "nonconstant term:" << std::endl + << "the term: " << args[0]; + PARSER_STATE->parseError(ss.str()); + } + ArrayType aqtype = static_cast(qtype); + if (!aqtype.getConstituentType().isComparableTo(args[0].getType())) + { + std::stringstream ss; + ss << "type mismatch inside array constant term:" << std::endl + << "array type: " << qtype << std::endl + << "expected const type: " << aqtype.getConstituentType() + << std::endl + << "computed const type: " << args[0].getType(); + PARSER_STATE->parseError(ss.str()); + } + expr = MK_CONST(CVC4::ArrayStoreAll(qtype, args[0])); + } + else if (qkind == kind::APPLY_SELECTOR) + { + if (qexpr.isNull()) + { + PARSER_STATE->parseError("Could not process parsed tuple selector."); + } + // tuple selector case + Integer x = qexpr.getConst().getNumerator(); + if (!x.fitsUnsignedInt()) + { + PARSER_STATE->parseError( + "index of tupSel is larger than size of unsigned int"); + } + unsigned int n = x.toUnsignedInt(); + if (args.size() > 1) + { + PARSER_STATE->parseError( + "tupSel applied to more than one tuple argument"); + } + Type t = args[0].getType(); + if (!t.isTuple()) + { + PARSER_STATE->parseError("tupSel applied to non-tuple"); + } + size_t length = ((DatatypeType)t).getTupleLength(); + if (n >= length) + { + std::stringstream ss; + ss << "tuple is of length " << length << "; cannot access index " + << n; + PARSER_STATE->parseError(ss.str()); + } + const Datatype& dt = ((DatatypeType)t).getDatatype(); + expr = dt[0][n].getSelector(); + expr = MK_EXPR(kind::APPLY_SELECTOR, expr, args); + } + else if (qkind != kind::NULL_EXPR) + { + std::stringstream ss; + ss << "Could not process parsed qualified identifier kind " << qkind; + PARSER_STATE->parseError(ss.str()); + } + else if (isBuiltinOperator) + { + bool done = false; if (args.size() > 2) { if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR @@ -2083,6 +2175,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } else { + bool done = false; if (args.size() >= 2) { // may be partially applied function, in this case we use HO_APPLY @@ -2105,73 +2198,18 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] if (!done) { - expr = MK_EXPR(kind, args); - } - } - } - | LPAREN_TOK - ( /* An indexed function application */ - indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK { - if(kind==CVC4::kind::APPLY_SELECTOR) { - //tuple selector case - Integer x = op.getConst().getNumerator(); - if (!x.fitsUnsignedInt()) { - PARSER_STATE->parseError("index of tupSel is larger than size of unsigned int"); - } - unsigned int n = x.toUnsignedInt(); - if (args.size()>1) { - PARSER_STATE->parseError("tupSel applied to more than one tuple argument"); - } - Type t = args[0].getType(); - if (!t.isTuple()) { - PARSER_STATE->parseError("tupSel applied to non-tuple"); + if (kind == kind::NULL_EXPR) + { + std::vector eargs(args.begin() + 1, args.end()); + expr = MK_EXPR(args[0], eargs); } - size_t length = ((DatatypeType)t).getTupleLength(); - if (n >= length) { - std::stringstream ss; - ss << "tuple is of length " << length << "; cannot access index " << n; - PARSER_STATE->parseError(ss.str()); + else + { + expr = MK_EXPR(kind, args); } - const Datatype & dt = ((DatatypeType)t).getDatatype(); - op = dt[0][n].getSelector(); } - if (kind!=kind::NULL_EXPR) { - expr = MK_EXPR( kind, op, args ); - } else { - expr = MK_EXPR(op, args); - } - PARSER_STATE->checkOperator(expr.getKind(), args.size()); } - | /* Array constant (in Z3 syntax) */ - LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED] - RPAREN_TOK term[f, f2] RPAREN_TOK - { - if(!type.isArray()) { - 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())) { - 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) ); - } - ) + } | /* a let or sygus let binding */ LPAREN_TOK ( LET_TOK LPAREN_TOK @@ -2401,7 +2439,6 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] PARSER_STATE->popScope(); expr = MK_EXPR( CVC4::kind::LAMBDA, args ); } - | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK { std::vector sorts; @@ -2418,6 +2455,211 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] ; +/** + * Matches a qualified identifier, which can be a combination of one or more of + * the following: + * (1) A kind. + * (2) A string name. + * (3) An expression expr. + * (4) A type t. + * + * A qualified identifier is the generic case of function heads. + * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6) + * of qualified identifiers, we additionally parse: + * - "Array constant specifications" of the form (as const (Array T1 T2)), + * which notice are used as function heads e.g. ((as const (Array Int Int)) 0) + * specifies the constant array over integers consisting of constant 0. This + * is handled as if it were a special case of an operator here. + * + * Examples: + * + * (Identifiers) + * + * - For declared functions f, we return (2). + * - For indexed functions like testers (_ is C) and bitvector extract + * (_ extract n m), we return (3) for the appropriate operator. + * - For tuple selectors (_ tupSel n), we return (1) and (3). Kind is set to + * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the + * caller as the n^th generic tuple selector. We do this since there is no + * AST expression representing generic tuple select, and we do not have enough + * type information at this point to know the type of the tuple we will be + * selecting from. + * + * (Ascripted Identifiers) + * + * - For ascripted nullary parametric datatype constructors like + * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate + * specialized constructor C as (3). + * - For ascripted non-nullary parametric datatype constructors like + * (as cons (List Int)), we return the appropriate specialized constructor C + * as (3). + * - Overloaded non-parametric constructors (as C T) return the appropriate + * expression, analogous to the parametric cases above. + * - For other ascripted nullary constants like (as emptyset (Set T)), + * (as sep.nil T), we return the appropriate expression (3). + * - For array constant specifications (as const (Array T1 T2)), we return (1) + * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2), + * where this is to be interpreted by the caller as converting the next parsed + * constant of type T2 to an Array of type (Array T1 T2) over that constant. + * - For ascriptions on normal symbols (as f T), we return the appropriate + * expression (3), which may involve disambiguating f based on type T if it is + * overloaded. + */ +qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type& t] +@init { + Kind k; + std::string baseName; + Expr f; + Type type; +} +: identifier[kind,name,expr] + | LPAREN_TOK AS_TOK + ( CONST_TOK sortSymbol[t, CHECK_DECLARED] + { + if (!t.isArray()) + { + std::stringstream ss; + ss << "expected array constant term, but cast is not of array type" + << std::endl + << "cast type: " << t; + PARSER_STATE->parseError(ss.str()); + } + kind = kind::STORE_ALL; + } + | identifier[k,baseName,f] + sortSymbol[type, CHECK_DECLARED] + { + if (f.isNull()) + { + Trace("parser-overloading") + << "Getting variable expression with name " << baseName + << " and type " << type << std::endl; + // get the variable expression for the type + if (PARSER_STATE->isDeclared(baseName, SYM_VARIABLE)) + { + f = PARSER_STATE->getExpressionForNameAndType(baseName, type); + } + if(f.isNull()) + { + std::stringstream ss; + ss << "Could not resolve expression with name " << baseName + << " and type " << type << std::endl; + PARSER_STATE->parseError(ss.str()); + } + } + Trace("parser-qid") << "Resolve ascription " << type << " on " << f; + Trace("parser-qid") << " " << f.getKind() << " " << f.getType(); + Trace("parser-qid") << std::endl; + // by default, we take f itself + expr = f; + if (f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) + { + // nullary constructors with a type ascription + // could be a parametric constructor or just an overloaded constructor + DatatypeType dtype = static_cast(type); + if (dtype.isParametric()) + { + std::vector v; + Expr e = f.getOperator(); + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + v.push_back(MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, + MK_CONST(AscriptionType( + dtc.getSpecializedConstructorType(type))), + f.getOperator())); + v.insert(v.end(), f.begin(), f.end()); + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); + } + } + else if (f.getType().isConstructor()) + { + // a non-nullary constructor with a type ascription + DatatypeType dtype = static_cast(type); + if (dtype.isParametric()) + { + const DatatypeConstructor& dtc = + Datatype::datatypeOf(f)[Datatype::indexOf(f)]; + expr = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, + MK_CONST(AscriptionType( + dtc.getSpecializedConstructorType(type))), + f); + } + } + else if (f.getKind() == CVC4::kind::EMPTYSET) + { + Debug("parser") << "Empty set encountered: " << f << " " << type + << std::endl; + expr = MK_CONST(::CVC4::EmptySet(type)); + } + else if (f.getKind() == CVC4::kind::UNIVERSE_SET) + { + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET); + } + else if (f.getKind() == CVC4::kind::SEP_NIL) + { + // 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->mkNullaryOperator(type, kind::SEP_NIL); + } + else if (f.getType() != type) + { + PARSER_STATE->parseError("Type ascription not satisfied."); + } + } + ) + RPAREN_TOK + ; + +/** + * Matches an identifier, which can be a combination of one or more of the + * following: + * (1) A kind. + * (2) A string name. + * (3) An expression expr. + * For examples, see documentation of qualIdentifier. + */ +identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr] +@init { + Expr f; + Expr f2; + std::vector numerals; +} +: functionName[name, CHECK_NONE] + + // indexed functions + + | LPAREN_TOK INDEX_TOK + ( TESTER_TOK term[f, f2] + { + if (f.getKind() == kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 0) + { + // for nullary constructors, must get the operator + f = f.getOperator(); + } + if (!f.getType().isConstructor()) + { + PARSER_STATE->parseError( + "Bad syntax for test (_ is X), X must be a constructor."); + } + expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester(); + } + | TUPLE_SEL_TOK m=INTEGER_LITERAL + { + // we adopt a special syntax (_ tupSel n) + kind = CVC4::kind::APPLY_SELECTOR; + // put m in expr so that the caller can deal with this case + expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); + } + | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] + { + expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) + .getExpr(); + } + ) + RPAREN_TOK + ; + /** * Matches an atomic term (a term with no subterms). * @return the expression expr representing the term or formula. @@ -2632,41 +2874,6 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] } ; -/** - * Matches a bit-vector operator (the ones parametrized by numbers) - */ -indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] -@init { - Expr expr; - Expr expr2; - std::vector numerals; -} - : LPAREN_TOK INDEX_TOK - ( TESTER_TOK term[expr, expr2] { - if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){ - //for nullary constructors, must get the operator - expr = expr.getOperator(); - } - if( !expr.getType().isConstructor() ){ - PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor."); - } - op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester(); - kind = CVC4::kind::APPLY_TESTER; - } - | TUPLE_SEL_TOK m=INTEGER_LITERAL { - kind = CVC4::kind::APPLY_SELECTOR; - //put m in op so that the caller (termNonVariable) can deal with this case - op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); - } - | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] - { - op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) - .getExpr(); - } - ) - RPAREN_TOK - ; - /** * Matches a sequence of terms and puts them into the formulas * vector. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 752bf58b4..039f573f9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -502,13 +502,7 @@ bool Smt2::logicIsSet() { } Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) { - if (sygus_v1() && name[0] == '-' - && name.find_first_not_of("0123456789", 1) == std::string::npos) - { - // allow unary minus in sygus version 1 - return getExprManager()->mkConst(Rational(name)); - } - else if (isAbstractValue(name)) + if (isAbstractValue(name)) { return mkAbstractValue(name); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index df553b8bd..37e6e3414 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -505,6 +505,7 @@ set(regress_0_tests regress0/issue1063-overloading-dt-cons.smt2 regress0/issue1063-overloading-dt-fun.smt2 regress0/issue1063-overloading-dt-sel.smt2 + regress0/issue2832-qualId.smt2 regress0/ite.cvc regress0/ite2.smt2 regress0/ite3.smt2 diff --git a/test/regress/regress0/issue2832-qualId.smt2 b/test/regress/regress0/issue2832-qualId.smt2 new file mode 100644 index 000000000..ff6e6e881 --- /dev/null +++ b/test/regress/regress0/issue2832-qualId.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((D 2)) ((par (T1 T2) + ((CL (get_CL T1)) + (CR (get_CR T2)))))) +(declare-sort U 0) +(declare-fun s0 () U) +(define-fun s1 () (D U U) ((as CL (D U U)) s0)) +(check-sat)