From 23d43d39d17c739bc47799ba25bc6f2eae05faa1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Apr 2021 17:32:40 -0500 Subject: [PATCH] Add internal support for datatype update (#6450) --- src/expr/dtype_cons.cpp | 45 ++++++++++--------- src/expr/dtype_selector.cpp | 9 +++- src/expr/dtype_selector.h | 9 +++- src/expr/node_manager.cpp | 23 ++++++++++ src/expr/node_manager.h | 23 +++------- src/expr/type_node.cpp | 7 ++- src/expr/type_node.h | 3 ++ src/printer/smt2/smt2_printer.cpp | 1 + src/theory/datatypes/kinds | 11 ++++- .../datatypes/theory_datatypes_type_rules.cpp | 40 +++++++++++++++++ .../datatypes/theory_datatypes_type_rules.h | 5 +++ .../datatypes/theory_datatypes_utils.cpp | 3 +- src/theory/datatypes/theory_datatypes_utils.h | 4 +- test/unit/util/datatype_black.cpp | 29 ++++++++++++ 14 files changed, 166 insertions(+), 46 deletions(-) diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 99e5ad8ac..0baf65dd6 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -48,14 +48,16 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType) Assert(!isResolved()); Assert(!selectorType.isNull()); SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node type = sm->mkDummySkolem( + Node sel = sm->mkDummySkolem( "unresolved_" + selectorName, selectorType, "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); - Trace("datatypes") << "DTypeConstructor::addArg: " << type << std::endl; + // can use null updater for now + Node nullNode; + Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl; std::shared_ptr a = - std::make_shared(selectorName, type); + std::make_shared(selectorName, sel, nullNode); addArg(a); } @@ -67,8 +69,9 @@ void DTypeConstructor::addArg(std::shared_ptr a) void DTypeConstructor::addArgSelf(std::string selectorName) { Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl; + Node nullNode; std::shared_ptr a = - std::make_shared(selectorName + '\0', Node::null()); + std::make_shared(selectorName + '\0', nullNode, nullNode); addArg(a); } @@ -514,11 +517,6 @@ bool DTypeConstructor::resolve( { Trace("datatypes-init") << " ...self selector" << std::endl; range = self; - arg->d_selector = sm->mkDummySkolem( - argName, - nm->mkSelectorType(self, self), - "is a selector", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); } else { @@ -535,11 +533,6 @@ bool DTypeConstructor::resolve( { Trace("datatypes-init") << " ...resolved selector" << std::endl; range = (*j).second; - arg->d_selector = sm->mkDummySkolem( - argName, - nm->mkSelectorType(self, range), - "is a selector", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); } } } @@ -565,14 +558,26 @@ bool DTypeConstructor::resolve( } Trace("datatypes-init") << " ...range after parametric substitution " << range << std::endl; - arg->d_selector = sm->mkDummySkolem( - argName, - nm->mkSelectorType(self, range), - "is a selector", - NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); } + // Internally, selectors (and updaters) are fresh internal skolems which + // we constructor via mkDummySkolem. + arg->d_selector = sm->mkDummySkolem( + argName, + nm->mkSelectorType(self, range), + "is a selector", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + std::string updateName("update_" + argName); + arg->d_updater = sm->mkDummySkolem( + updateName, + nm->mkDatatypeUpdateType(self, range), + "is a selector", + NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY); + // must set indices to ensure datatypes::utils::indexOf works arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex); - arg->d_selector.setAttribute(DTypeIndexAttr(), index++); + arg->d_selector.setAttribute(DTypeIndexAttr(), index); + arg->d_updater.setAttribute(DTypeConsIndexAttr(), cindex); + arg->d_updater.setAttribute(DTypeIndexAttr(), index); + index = index + 1; arg->d_resolved = true; argTypes.push_back(range); // We use \0 as a distinguished marker for unresolved selectors for doing diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index 98a07b2c9..c8497433b 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -21,8 +21,8 @@ using namespace cvc5::kind; namespace cvc5 { -DTypeSelector::DTypeSelector(std::string name, Node selector) - : d_name(name), d_selector(selector), d_resolved(false) +DTypeSelector::DTypeSelector(std::string name, Node selector, Node updater) + : d_name(name), d_selector(selector), d_updater(updater), d_resolved(false) { Assert(name != ""); } @@ -34,6 +34,11 @@ Node DTypeSelector::getSelector() const Assert(d_resolved); return d_selector; } +Node DTypeSelector::getUpdater() const +{ + Assert(d_resolved); + return d_updater; +} Node DTypeSelector::getConstructor() const { diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h index 1c7d63d65..178151062 100644 --- a/src/expr/dtype_selector.h +++ b/src/expr/dtype_selector.h @@ -39,7 +39,7 @@ class DTypeSelector public: /** constructor */ - DTypeSelector(std::string name, Node selector); + DTypeSelector(std::string name, Node selector, Node updater); /** Get the name of this constructor argument. */ const std::string& getName() const; @@ -49,6 +49,11 @@ class DTypeSelector * only permitted after resolution. */ Node getSelector() const; + /** + * Get the upater for this constructor argument; this call is + * only permitted after resolution. + */ + Node getUpdater() const; /** * Get the associated constructor for this constructor argument; @@ -79,6 +84,8 @@ class DTypeSelector std::string d_name; /** the selector expression */ Node d_selector; + /** the updater expression */ + Node d_updater; /** * The constructor associated with this selector. This field is initialized * by the constructor of this selector during a call to diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 591413a8a..0a0781819 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -704,6 +704,29 @@ TypeNode NodeManager::mkConstructorType(const std::vector& args, return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } +TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype selector type"); + return mkTypeNode(kind::SELECTOR_TYPE, domain, range); +} + +TypeNode NodeManager::mkTesterType(TypeNode domain) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype tester"); + return mkTypeNode(kind::TESTER_TYPE, domain); +} + +TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) +{ + CheckArgument( + domain.isDatatype(), domain, "cannot create non-datatype upater type"); + // It is a function type domain x range -> domain, we store only the + // arguments + return mkTypeNode(kind::DT_UPDATE_TYPE, domain, range); +} + TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { if( index==types.size() ){ if( d_data.isNull() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 120806955..8b99f5743 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -987,10 +987,13 @@ class NodeManager TypeNode mkConstructorType(const std::vector& args, TypeNode range); /** Make a type representing a selector with the given parameterization */ - inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); + TypeNode mkSelectorType(TypeNode domain, TypeNode range); /** Make a type representing a tester with given parameterization */ - inline TypeNode mkTesterType(TypeNode domain); + TypeNode mkTesterType(TypeNode domain); + + /** Make a type representing an updater with the given parameterization */ + TypeNode mkDatatypeUpdateType(TypeNode domain, TypeNode range); /** Bits for use in mkSort() flags. */ enum @@ -1131,22 +1134,6 @@ inline TypeNode NodeManager::mkSetType(TypeNode elementType) { return mkTypeNode(kind::SET_TYPE, elementType); } -inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { - CheckArgument(domain.isDatatype(), domain, - "cannot create non-datatype selector type"); - CheckArgument(range.isFirstClass(), - range, - "cannot have selector fields that are not first-class types. " - "Try option --uf-ho."); - return mkTypeNode(kind::SELECTOR_TYPE, domain, range); -} - -inline TypeNode NodeManager::mkTesterType(TypeNode domain) { - CheckArgument(domain.isDatatype(), domain, - "cannot create non-datatype tester"); - return mkTypeNode(kind::TESTER_TYPE, domain ); -} - inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 2d19db16c..483983e6e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -249,7 +249,7 @@ bool TypeNode::isClosedEnumerable() bool TypeNode::isFirstClass() const { return getKind() != kind::CONSTRUCTOR_TYPE && getKind() != kind::SELECTOR_TYPE - && getKind() != kind::TESTER_TYPE + && getKind() != kind::TESTER_TYPE && getKind() != kind::DT_UPDATE_TYPE && (getKind() != kind::TYPE_CONSTANT || (getConst() != REGEXP_TYPE && getConst() != SEXPR_TYPE)); @@ -633,6 +633,11 @@ bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } +bool TypeNode::isDatatypeUpdater() const +{ + return getKind() == kind::DT_UPDATE_TYPE; +} + bool TypeNode::isCodatatype() const { if (isDatatype()) diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 32a1befbd..d73d64b43 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -651,6 +651,9 @@ public: /** Is this a tester type */ bool isTester() const; + /** Is this a datatype updater type */ + bool isDatatypeUpdater() const; + /** Get the internal Datatype specification from a datatype type */ const DType& getDType() const; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 014079b14..9f9492cec 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -919,6 +919,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: case kind::APPLY_SELECTOR_TOTAL: + case kind::APPLY_DT_UPDATE: case kind::PARAMETRIC_DATATYPE: break; // separation logic diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index ab4c3bf6b..4cabddd96 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -31,6 +31,13 @@ cardinality TESTER_TYPE \ "::cvc5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +# tester type has a constructor type +operator DT_UPDATE_TYPE 2 "datatype update" +# can re-use function cardinality +cardinality DT_UPDATE_TYPE \ + "::cvc5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" + 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)" @@ -38,6 +45,8 @@ parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1 "selector application; para parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is a tester, second is a datatype term" +parameterized APPLY_DT_UPDATE DT_UPDATE_TYPE 2 "datatype update application; first parameter is an update, second is a datatype term to update, third is the value to update with" + constant DATATYPE_TYPE \ ::cvc5::DatatypeIndexConstant \ "::cvc5::DatatypeIndexConstantHashFunction" \ @@ -80,6 +89,7 @@ typerule APPLY_CONSTRUCTOR ::cvc5::theory::datatypes::DatatypeConstructorTypeRul typerule APPLY_SELECTOR ::cvc5::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_SELECTOR_TOTAL ::cvc5::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::cvc5::theory::datatypes::DatatypeTesterTypeRule +typerule APPLY_DT_UPDATE ::cvc5::theory::datatypes::DatatypeUpdateTypeRule typerule APPLY_TYPE_ASCRIPTION ::cvc5::theory::datatypes::DatatypeAscriptionTypeRule # constructor applications are constant if they are applied only to constants @@ -103,7 +113,6 @@ parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter i typerule RECORD_UPDATE_OP ::cvc5::theory::datatypes::RecordUpdateOpTypeRule typerule RECORD_UPDATE ::cvc5::theory::datatypes::RecordUpdateTypeRule - operator DT_SIZE 1 "datatypes size" typerule DT_SIZE ::cvc5::theory::datatypes::DtSizeTypeRule diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 36f1aae9d..63f48668c 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -203,6 +203,46 @@ TypeNode DatatypeTesterTypeRule::computeType(NodeManager* nodeManager, return nodeManager->booleanType(); } +TypeNode DatatypeUpdateTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::APPLY_DT_UPDATE); + TypeNode updType = n.getOperator().getType(check); + Assert(updType.getNumChildren() == 2); + if (check) + { + for (size_t i = 0; i < 2; i++) + { + TypeNode childType = n[i].getType(check); + TypeNode t = updType[i]; + if (t.isParametricDatatype()) + { + Debug("typecheck-idt") + << "typecheck parameterized update: " << n << std::endl; + TypeMatcher m(t); + if (!m.doMatching(t, childType)) + { + throw TypeCheckingExceptionPrivate( + n, + "matching failed for update argument of parameterized datatype"); + } + } + else + { + Debug("typecheck-idt") << "typecheck update: " << n << std::endl; + Debug("typecheck-idt") << "test type: " << updType << std::endl; + if (!t.isComparableTo(childType)) + { + throw TypeCheckingExceptionPrivate(n, "bad type for update argument"); + } + } + } + } + // type is the first argument + return updType[0]; +} + TypeNode DatatypeAscriptionTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 8bb66f6fe..3bf4660e6 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -39,6 +39,11 @@ struct DatatypeTesterTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; +struct DatatypeUpdateTypeRule +{ + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + struct DatatypeAscriptionTypeRule { static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index fb00477bf..f651d5f84 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -116,7 +116,8 @@ const DType& datatypeOf(Node n) { case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); case SELECTOR_TYPE: - case TESTER_TYPE: return t[0].getDType(); + case TESTER_TYPE: + case DT_UPDATE_TYPE: return t[0].getDType(); default: Unhandled() << "arg must be a datatype constructor, selector, or tester"; } diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 6824e0fb0..898ee3491 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -54,12 +54,12 @@ int isTester(Node n, Node& a); int isTester(Node n); /** * Get the index of a constructor or tester in its datatype, or the - * index of a selector in its constructor. (Zero is always the + * index of a selector or updater in its constructor. (Zero is always the * first index.) */ size_t indexOf(Node n); /** - * Get the index of constructor corresponding to selector. + * Get the index of constructor corresponding to selector or updater. * (Zero is always the first index.) */ size_t cindexOf(Node n); diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 3fd817e9d..5844868f1 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -227,6 +227,35 @@ TEST_F(TestUtilBlackDatatype, list_boolean) ASSERT_TRUE(listType.mkGroundTerm().getType() == listType); } +TEST_F(TestUtilBlackDatatype, listIntUpdate) +{ + DType list("list"); + TypeNode integerType = d_nodeManager->integerType(); + + std::shared_ptr cons = + std::make_shared("cons"); + cons->addArg("car", integerType); + cons->addArgSelf("cdr"); + list.addConstructor(cons); + + std::shared_ptr nil = + std::make_shared("nil"); + list.addConstructor(nil); + + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const DType& ldt = listType.getDType(); + Node updater = ldt[0][0].getUpdater(); + Node gt = listType.mkGroundTerm(); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node truen = d_nodeManager->mkConst(true); + // construct an update term + Node uterm = d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, zero); + // construct a non well-formed update term + ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, truen) + .getType(true), + TypeCheckingExceptionPrivate); +} + TEST_F(TestUtilBlackDatatype, mutual_list_trees1) { /* Create two mutual datatypes corresponding to this definition -- 2.30.2