Add support for datatype update (#6449)

This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.

Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.

8 files changed, 37 insertions, 19 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9bda5cff1..538868c6c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -480,6 +480,8 @@ set(regress_0_tests
   regress0/datatypes/issue5280-no-nrec.smt2
   regress0/datatypes/jsat-2.6.smt2
   regress0/datatypes/list-bool.smt2
+  regress0/datatypes/list-update.smt2
+  regress0/datatypes/list-update-sat.smt2
   regress0/datatypes/model-subterms-min.smt2
   regress0/datatypes/mutually-recursive.cvc
   regress0/datatypes/pair-bool-bool.cvc
diff --git a/test/regress/regress0/datatypes/list-update-sat.smt2 b/test/regress/regress0/datatypes/list-update-sat.smt2
new file mode 100644
index 000000000..9f424e595
--- /dev/null
+++ b/test/regress/regress0/datatypes/list-update-sat.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((list 0)) (
+((cons (head Int) (tail list)) (nil))
+))
+(declare-fun a () list)
+(assert (= ((_ update head) a 3) (cons 3 nil)))
+(check-sat)
diff --git a/test/regress/regress0/datatypes/list-update.smt2 b/test/regress/regress0/datatypes/list-update.smt2
new file mode 100644
index 000000000..178f1a000
--- /dev/null
+++ b/test/regress/regress0/datatypes/list-update.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((list 0)) (
+((cons (head Int) (tail list)) (nil))
+))
+(declare-fun a () list)
+(declare-fun b () list)
+(assert ((_ is cons) a))
+(assert (= ((_ update head) a 3) ((_ update head) b 4)))
+(check-sat)
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 3fbdcc0b5..f82e722d3 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -214,6 +214,10 @@ TEST_F(TestApiBlackDatatype, datatypeNames)
   ASSERT_EQ(dselTail.getName(), std::string("tail"));
   ASSERT_EQ(dselTail.getRangeSort(), dtypeSort);
 
+  // get selector from datatype
+  ASSERT_NO_THROW(dt.getSelector("head"));
+  ASSERT_THROW(dt.getSelector("cons"), CVC5ApiException);
+
   // possible to construct null datatype declarations if not using solver
   ASSERT_THROW(DatatypeDecl().getName(), CVC5ApiException);
 }
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 7183fa7a7..8c4e31c22 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -50,7 +50,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
 {
   Op plus = d_solver.mkOp(PLUS);
   Op divisible = d_solver.mkOp(DIVISIBLE, 4);
-  Op record_update = d_solver.mkOp(RECORD_UPDATE, "test");
   Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
   Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
@@ -60,7 +59,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
   Op iand = d_solver.mkOp(IAND, 3);
   Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
   Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
-  Op tuple_update = d_solver.mkOp(TUPLE_UPDATE, 5);
   Op floatingpoint_to_fp_ieee_bitvector =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
   Op floatingpoint_to_fp_floatingpoint =
@@ -76,7 +74,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
 
   ASSERT_EQ(0, plus.getNumIndices());
   ASSERT_EQ(1, divisible.getNumIndices());
-  ASSERT_EQ(1, record_update.getNumIndices());
   ASSERT_EQ(1, bitvector_repeat.getNumIndices());
   ASSERT_EQ(1, bitvector_zero_extend.getNumIndices());
   ASSERT_EQ(1, bitvector_sign_extend.getNumIndices());
@@ -86,7 +83,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
   ASSERT_EQ(1, iand.getNumIndices());
   ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices());
   ASSERT_EQ(1, floatingopint_to_sbv.getNumIndices());
-  ASSERT_EQ(1, tuple_update.getNumIndices());
   ASSERT_EQ(2, floatingpoint_to_fp_ieee_bitvector.getNumIndices());
   ASSERT_EQ(2, floatingpoint_to_fp_floatingpoint.getNumIndices());
   ASSERT_EQ(2, floatingpoint_to_fp_real.getNumIndices());
@@ -105,11 +101,6 @@ TEST_F(TestApiBlackOp, getIndicesString)
   ASSERT_TRUE(divisible_ot.isIndexed());
   std::string divisible_idx = divisible_ot.getIndices<std::string>();
   ASSERT_EQ(divisible_idx, "4");
-
-  Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
-  std::string record_update_idx = record_update_ot.getIndices<std::string>();
-  ASSERT_EQ(record_update_idx, "test");
-  ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, getIndicesUint)
@@ -155,11 +146,6 @@ TEST_F(TestApiBlackOp, getIndicesUint)
   uint32_t floatingpoint_to_sbv_idx =
       floatingpoint_to_sbv_ot.getIndices<uint32_t>();
   ASSERT_EQ(floatingpoint_to_sbv_idx, 13);
-
-  Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
-  uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
-  ASSERT_EQ(tuple_update_idx, 5);
-  ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, getIndicesPairUint)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index c0258be9a..f7e6a3783 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -544,7 +544,6 @@ TEST_F(TestApiBlackSolver, mkOp)
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException);
 
   // mkOp(Kind kind, const std::string& arg)
-  ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf"));
   ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException);
 
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index c2b924bfa..d1b096bda 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -153,11 +153,20 @@ TEST_F(TestApiBlackSort, isTester)
 {
   Sort dt_sort = create_datatype_sort();
   Datatype dt = dt_sort.getDatatype();
-  Sort cons_sort = dt[0].getTesterTerm().getSort();
-  ASSERT_TRUE(cons_sort.isTester());
+  Sort testerSort = dt[0].getTesterTerm().getSort();
+  ASSERT_TRUE(testerSort.isTester());
   ASSERT_NO_THROW(Sort().isTester());
 }
 
+TEST_F(TestApiBlackSort, isUpdater)
+{
+  Sort dt_sort = create_datatype_sort();
+  Datatype dt = dt_sort.getDatatype();
+  Sort updaterSort = dt[0][0].getUpdaterTerm().getSort();
+  ASSERT_TRUE(updaterSort.isUpdater());
+  ASSERT_NO_THROW(Sort().isUpdater());
+}
+
 TEST_F(TestApiBlackSort, isFunction)
 {
   Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(),
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index 5844868f1..a19ab31a1 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -249,9 +249,9 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate)
   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);
+  Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero);
   // construct a non well-formed update term
-  ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, truen)
+  ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, truen)
                    .getType(true),
                TypeCheckingExceptionPrivate);
 }