From 7f445f50998e787915052e125c85077c69fd8a0f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Apr 2022 20:16:55 -0500 Subject: [PATCH] Simplify internal representation of instantiated sorts (#8620) Previously, sort constructors were stored as underlying operator of the NodeValue of instantiated sorts. This made it very difficult to access what sort constructor was used to construct the uninterpreted sort. Moreover, this representation made it virtually impossible to have a clean implementation of the LFSC printer for instantiated uninterpreted sorts, which requires renaming sort constructors. This introduces a new kind INSTANTIATED_SORT_TYPE, which acts as an uninterpreted sort. The sort constructor is stored as the first child in its AST, which is analogous to parametric datatypes. It furthermore restricts SORT_TYPE to 0 children. This is work towards having correct LFSC proof output when the input contains instantiated uninterpreted sorts. --- src/expr/dtype_cons.cpp | 18 ++++++---- src/expr/node_manager_template.cpp | 10 ++---- src/expr/type_node.cpp | 33 +++++++++++-------- src/printer/smt2/smt2_printer.cpp | 1 + src/theory/builtin/kinds | 16 ++++++--- src/theory/builtin/type_enumerator.cpp | 2 +- .../datatypes/theory_datatypes_type_rules.cpp | 6 ++-- 7 files changed, 53 insertions(+), 33 deletions(-) diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index c56d17214..cda9f8a63 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -643,15 +643,21 @@ TypeNode DTypeConstructor::doParametricSubstitution( children.push_back( doParametricSubstitution((*i), paramTypes, paramReplacements)); } - for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i) + if (range.getKind() == INSTANTIATED_SORT_TYPE) { - if (paramTypes[i].getUninterpretedSortConstructorArity() - == origChildren.size()) + // paramTypes contains a list of uninterpreted sort constructors. + // paramReplacements contains a list of instantiated parametric datatypes. + // If range is (INSTANTIATED_SORT_TYPE c T1 ... Tn), and + // paramTypes[i] is c + // paramReplacements[i] is (PARAMETRIC_DATATYPE d S1 ... Sn) + // then we return (PARAMETRIC_DATATYPE d T'1 ... T'n) where T'1 ...T'n + // is the result of recursively processing T1 ... Tn. + for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i) { - TypeNode tn = paramTypes[i].instantiate(origChildren); - if (range == tn) + if (paramTypes[i] == origChildren[0]) { - TypeNode tret = paramReplacements[i].instantiate(children); + std::vector params(children.begin() + 1, children.end()); + TypeNode tret = paramReplacements[i].instantiate(params); return tret; } } diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 57b59dce9..7a367dcf0 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -894,17 +894,13 @@ TypeNode NodeManager::mkSort(TypeNode constructor, Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr()) && hasAttribute(constructor.d_nv, expr::VarNameAttr())) << "expected a sort constructor"; - std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size()) << "arity mismatch in application of sort constructor"; - NodeBuilder nb(this, kind::SORT_TYPE); - Node sortTag = Node(constructor.d_nv->d_children[0]); - nb << sortTag; + NodeBuilder nb(this, kind::INSTANTIATED_SORT_TYPE); + nb << constructor; nb.append(children); - TypeNode type = nb.constructTypeNode(); - setAttribute(type, expr::VarNameAttr(), name); - return type; + return nb.constructTypeNode(); } TypeNode NodeManager::mkSortConstructor(const std::string& name, size_t arity) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index d7b832c70..59feac41f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -369,9 +369,7 @@ std::vector TypeNode::getInstantiatedParamTypes() const { Assert(isInstantiated()); vector params; - for (uint32_t i = isInstantiatedDatatype() ? 1 : 0, i_end = getNumChildren(); - i < i_end; - ++i) + for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i) { params.push_back((*this)[i]); } @@ -428,7 +426,7 @@ bool TypeNode::isInstantiatedDatatype() const { bool TypeNode::isInstantiatedUninterpretedSort() const { - return isUninterpretedSort() && getNumChildren() > 0; + return getKind() == kind::INSTANTIATED_SORT_TYPE; } bool TypeNode::isInstantiated() const @@ -439,7 +437,12 @@ bool TypeNode::isInstantiated() const TypeNode TypeNode::instantiate(const std::vector& params) const { NodeManager* nm = NodeManager::currentNM(); - if (getKind() == kind::PARAMETRIC_DATATYPE) + Kind k = getKind(); + TypeNode ret; + // Note that parametric datatypes we instantiate have an AST where they are + // applied to their default parameters. In constrast, sort constructors have + // no children. + if (k == kind::PARAMETRIC_DATATYPE) { Assert(params.size() == getNumChildren() - 1); TypeNode cons = @@ -450,10 +453,14 @@ TypeNode TypeNode::instantiate(const std::vector& params) const { paramsNodes.push_back(t); } - return nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); + ret = nm->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes); } - Assert(isUninterpretedSortConstructor()); - return nm->mkSort(*this, params); + else + { + Assert(isUninterpretedSortConstructor()); + ret = nm->mkSort(*this, params); + } + return ret; } uint64_t TypeNode::getUninterpretedSortConstructorArity() const @@ -476,10 +483,8 @@ std::string TypeNode::getName() const TypeNode TypeNode::getUninterpretedSortConstructor() const { - Assert(isInstantiatedUninterpretedSort()); - NodeBuilder nb(kind::SORT_TYPE); - nb << NodeManager::operatorFromType(*this); - return nb.constructTypeNode(); + Assert(getKind() == kind::INSTANTIATED_SORT_TYPE); + return (*this)[0]; } bool TypeNode::isParameterInstantiatedDatatype(size_t n) const @@ -509,7 +514,9 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){ /** Is this a sort kind */ bool TypeNode::isUninterpretedSort() const { - return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ); + Kind k = getKind(); + return k == kind::INSTANTIATED_SORT_TYPE + || (k == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr())); } /** Is this a sort constructor kind */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 41fa39575..5367c0e19 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -859,6 +859,7 @@ void Smt2Printer::toStream(std::ostream& out, } } break; + case kind::INSTANTIATED_SORT_TYPE: break; case kind::PARAMETRIC_DATATYPE: break; // separation logic diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index fafeb6e2f..4175947ef 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -256,14 +256,23 @@ sort BUILTIN_OPERATOR_TYPE \ "the type for built-in operators" variable SORT_TAG "sort tag" -parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpreted' sorts" -# This is really "unknown" cardinality, but maybe this will be good -# enough (for now) ? +parameterized SORT_TYPE SORT_TAG 0 "specifies types of user-declared 'uninterpreted' sorts" +# The cardinality of uninterpreted sorts is defined infinite here, although they are given special treatment in TypeNode::getCardinalityClass cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" well-founded SORT_TYPE \ "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +enumerator SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h" + +# an instantiated sort has the same properties as an ordinary uninterpreted sort +operator INSTANTIATED_SORT_TYPE 1: "instantiated uninterpreted sort" +cardinality INSTANTIATED_SORT_TYPE "Cardinality(Cardinality::INTEGERS)" +well-founded INSTANTIATED_SORT_TYPE \ + "::cvc5::internal::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ + "::cvc5::internal::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" +enumerator INSTANTIATED_SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h" constant UNINTERPRETED_SORT_VALUE \ class \ @@ -272,7 +281,6 @@ constant UNINTERPRETED_SORT_VALUE \ "util/uninterpreted_sort_value.h" \ "the kind of expressions representing uninterpreted sort values; payload is an instance of the cvc5::internal::AbstractValue class (used in models)" typerule UNINTERPRETED_SORT_VALUE ::cvc5::internal::theory::builtin::UninterpretedSortValueTypeRule -enumerator SORT_TYPE ::cvc5::internal::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 2593a46e5..4464f630a 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -26,7 +26,7 @@ UninterpretedSortEnumerator::UninterpretedSortEnumerator( TypeNode type, TypeEnumeratorProperties* tep) : TypeEnumeratorBase(type), d_count(0) { - Assert(type.getKind() == kind::SORT_TYPE); + Assert(type.isUninterpretedSort()); d_has_fixed_bound = false; Trace("uf-type-enum") << "UF enum " << type << ", tep = " << tep << std::endl; if (tep && tep->d_fixed_usort_card) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index f4450a57d..edf797da1 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -69,7 +69,8 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager, std::vector instTypes; m.getMatches(instTypes); TypeNode range = t.instantiate(instTypes); - Trace("typecheck-idt") << "Return " << range << std::endl; + Trace("typecheck-idt") << "Return (constructor) " << range << " for " << n + << std::endl; return range; } else @@ -149,7 +150,8 @@ TypeNode DatatypeSelectorTypeRule::computeType(NodeManager* nodeManager, TypeNode range = selType[1]; range = range.substitute( types.begin(), types.end(), matches.begin(), matches.end()); - Trace("typecheck-idt") << "Return " << range << std::endl; + Trace("typecheck-idt") << "Return (selector) " << range << " for " << n + << " from " << selType[1] << std::endl; return range; } else -- 2.30.2