Add internal support for datatype update (#6450)

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 99e5ad8ac170870c6f49db61d000abe5025a26e7..0baf65dd6bc96794826c102856df6de49806d6b5 100644 (file)
--- 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<DTypeSelector> a =
-      std::make_shared<DTypeSelector>(selectorName, type);
+      std::make_shared<DTypeSelector>(selectorName, sel, nullNode);
   addArg(a);
 }
 
@@ -67,8 +69,9 @@ void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
 void DTypeConstructor::addArgSelf(std::string selectorName)
 {
   Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
+  Node nullNode;
   std::shared_ptr<DTypeSelector> a =
-      std::make_shared<DTypeSelector>(selectorName + '\0', Node::null());
+      std::make_shared<DTypeSelector>(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 98a07b2c9007f7a9424af5a87a7a3ab210178fd0..c8497433beca12ca55662a814d4239882035a91d 100644 (file)
--- 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 1c7d63d658c116d91d22b4bfcfa2051b5694d2c6..178151062fb295d77cd53110dee82d8db32d4493 100644 (file)
--- 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 591413a8aa8064d438afb102827b90db933dd425..0a0781819a7272f045dff1b64f9b708414ad3769 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -704,6 +704,29 @@ TypeNode NodeManager::mkConstructorType(const std::vector<TypeNode>& 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 1208069555586f3f22b714cc38ac2793d17c7818..8b99f5743171e8290453cf70e971558334931e54 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -987,10 +987,13 @@ class NodeManager
   TypeNode mkConstructorType(const std::vector<TypeNode>& 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 2d19db16c2da43e5373d1a20d4d3f4a2bb75394a..483983e6eceded6c1041999beb33a961edc84bcf 100644 (file)
--- 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<TypeConstant>() != REGEXP_TYPE
                  && getConst<TypeConstant>() != 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 32a1befbd20285486dd5b5002ffe3f9b274d0940..d73d64b431139c59d01d82cef7c6475e606ac7a0 100644 (file)
--- 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 014079b14f67cb39c0b07f989e9b4acda9fa54c7..9f9492cece0e951a25800319f942a5b4d2d4d445 100644 (file)
--- 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 ab4c3bf6befa9b7db706f715ec41383f5ea92f32..4cabddd96dc831be5714be134f1e97c56d0e7b24 100644 (file)
--- 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 36f1aae9d1f5327fb98662b4c0533d8cab2ee9d7..63f48668cf49b1810624278cbc0ec9a39f60c306 100644 (file)
--- 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 8bb66f6fe5108c0cbba769a08a5a2c16d9e8d439..3bf4660e6f29aef78d7df7fd77f18328fbdec2d0 100644 (file)
--- 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 fb00477bfb1db6713669efe613049f6d9d880742..f651d5f8466d2cca28c95ff0c6c951fe5e5aeb53 100644 (file)
--- 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 6824e0fb08288f910747f4913217da575e97040f..898ee3491d46e63bb208856eea47690bd59db69a 100644 (file)
--- 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 3fd817e9da1ae4873a6684a1c4ee74af03f77ab0..5844868f1efb7583f94406170a49a5bf815cf401 100644 (file)
--- 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<DTypeConstructor> cons =
+      std::make_shared<DTypeConstructor>("cons");
+  cons->addArg("car", integerType);
+  cons->addArgSelf("cdr");
+  list.addConstructor(cons);
+
+  std::shared_ptr<DTypeConstructor> nil =
+      std::make_shared<DTypeConstructor>("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