From: Andrew Reynolds Date: Wed, 9 Mar 2022 00:21:34 +0000 (-0600) Subject: Eliminate the APPLY_SELECTOR_TOTAL kind (#8266) X-Git-Tag: cvc5-1.0.0~297 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9e74418dcc6245c0d2836bfd4d97a0221514ed51;p=cvc5.git Eliminate the APPLY_SELECTOR_TOTAL kind (#8266) --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2cfc262c2..0dd86f814 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -571,7 +571,6 @@ const static std::unordered_map /* Datatypes ------------------------------------------------------- */ {cvc5::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, {cvc5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, - {cvc5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, {cvc5::Kind::APPLY_TESTER, APPLY_TESTER}, {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER}, {cvc5::Kind::DT_SIZE, DT_SIZE}, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 535b96d5f..1ca7893c0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -843,7 +843,6 @@ void Smt2Printer::toStream(std::ostream& out, } } break; - case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; // separation logic diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index ca120c241..cbb945584 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -181,7 +181,7 @@ Node LfscNodeConverter::postConvert(Node n) return convert(theory::uf::TheoryUfRewriter::getHoApplyForApplyUf(n)); } else if (k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_TESTER - || k == APPLY_SELECTOR_TOTAL || k == APPLY_UPDATER) + || k == APPLY_UPDATER) { // must convert other kinds of apply to functions, since we convert to // HO_APPLY @@ -1089,12 +1089,9 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) // get its variable name opName << getNameForUserNameOf(dt[index].getConstructor()); } - else if (k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL) + else if (k == APPLY_SELECTOR) { - if (k == APPLY_SELECTOR_TOTAL) - { - ret = maybeMkSkolemFun(op, macroApply); - } + ret = maybeMkSkolemFun(op, macroApply); if (ret.isNull()) { unsigned index = DType::indexOf(op); diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index a88421c7a..57e2b7fcc 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -50,7 +50,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) { return rewriteConstructor(in); } - else if (kind == kind::APPLY_SELECTOR_TOTAL || kind == kind::APPLY_SELECTOR) + else if (kind == kind::APPLY_SELECTOR) { return rewriteSelector(in); } @@ -375,7 +375,7 @@ RewriteResponse DatatypesRewriter::rewriteConstructor(TNode in) RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) { - Kind k = in.getKind(); + Assert (in.getKind()==kind::APPLY_SELECTOR); if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions @@ -423,25 +423,6 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in) return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } } - else if (k == kind::APPLY_SELECTOR_TOTAL) - { - // evaluates to the first ground value of type tn. - NodeManager* nm = NodeManager::currentNM(); - Node gt = nm->mkGroundValue(tn); - Assert(!gt.isNull()); - if (tn.isDatatype() && !tn.isInstantiatedDatatype()) - { - gt = NodeManager::currentNM()->mkNode( - kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tn)), - gt); - } - Trace("datatypes-rewrite") - << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " << gt << std::endl; - return RewriteResponse(REWRITE_DONE, gt); - } } return RewriteResponse(REWRITE_DONE, in); } diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index ee42add6b..45553a00f 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -41,7 +41,6 @@ cardinality UPDATER_TYPE \ parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor" parameterized APPLY_SELECTOR SELECTOR_TYPE 1 "selector application; parameter is a datatype term (undefined if mis-applied)" -parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; parameter is a datatype term (defined rigidly if mis-applied)" parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term" @@ -89,7 +88,6 @@ constant ASCRIPTION_TYPE \ typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule -typerule APPLY_SELECTOR_TOTAL ::cvc5::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::cvc5::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_UPDATER ::cvc5::theory::datatypes::DatatypeUpdateTypeRule typerule APPLY_TYPE_ASCRIPTION ::cvc5::theory::datatypes::DatatypeAscriptionTypeRule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 74228167a..1461889b1 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -445,8 +445,6 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { Trace("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl; - // should not use APPLY_SELECTOR_TOTAL - Assert(n.getKind() != APPLY_SELECTOR_TOTAL); // must ensure the type is well founded and has no nested recursion if // the option dtNestedRec is not set to true. TypeNode tn = n.getType(); diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 7ce5c0df6..4d907b259 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -118,8 +118,7 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::APPLY_SELECTOR - || n.getKind() == kind::APPLY_SELECTOR_TOTAL); + Assert(n.getKind() == kind::APPLY_SELECTOR); TypeNode selType = n.getOperator().getType(check); TypeNode t = selType[0]; Assert(t.isDatatype());