Add internal support for datatype update (#6450)

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<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 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<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 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<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 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<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 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<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