5 files changed, 33 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 039eaf0ad..6e3332651 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1636,7 +1636,11 @@ tupleStore[cvc5::api::Term& f]
       | DOT ( tupleStore[f2]
             | recordStore[f2] ) )
     | ASSIGN_TOK term[f2] )
-    { f = SOLVER->mkTerm(SOLVER->mkOp(api::TUPLE_UPDATE,k), f, f2); }
+    {
+      const api::Datatype& dt = f.getSort().getDatatype();
+      f = SOLVER->mkTerm(
+         api::APPLY_UPDATER, dt[0][k].getUpdaterTerm(), f, f2);
+    }
   ;
 
 /**
@@ -1665,7 +1669,11 @@ recordStore[cvc5::api::Term& f]
       | DOT ( tupleStore[f2]
             | recordStore[f2] ) )
     | ASSIGN_TOK term[f2] )
-    { f = SOLVER->mkTerm(SOLVER->mkOp(api::RECORD_UPDATE,id), f, f2); }
+    {
+      const api::Datatype& dt = f.getSort().getDatatype();
+      f = SOLVER->mkTerm(
+         api::APPLY_UPDATER, dt[0][id].getUpdaterTerm(), f, f2);
+    }
   ;
 
 /** Parses a unary minus term. */
diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp
index 3f7df3794..772b73b1e 100644
--- a/src/parser/parse_op.cpp
+++ b/src/parser/parse_op.cpp
@@ -20,7 +20,7 @@ namespace cvc5 {
 std::ostream& operator<<(std::ostream& os, const ParseOp& p)
 {
   std::stringstream out;
-  out << "(ParseOp ";
+  out << "(ParseOp";
   if (!p.d_expr.isNull())
   {
     out << " :expr " << p.d_expr;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 84c1e66f3..31f8517cd 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -154,6 +154,10 @@ api::Kind Parser::getKindForFunction(api::Term fun)
   {
     return api::APPLY_TESTER;
   }
+  else if (t.isUpdater())
+  {
+    return api::APPLY_UPDATER;
+  }
   return api::UNDEFINED_KIND;
 }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4a612ce6f..dc9a324bb 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1643,6 +1643,22 @@ identifier[cvc5::ParseOp& p]
         api::DatatypeConstructor dc = d.getConstructor(f.toString());
         p.d_expr = dc.getTesterTerm();
       }
+    | UPDATE_TOK term[f, f2]
+      {
+        if (!f.getSort().isSelector())
+        {
+          PARSER_STATE->parseError(
+              "Bad syntax for test (_ update X), X must be a selector.");
+        }
+        std::string sname = f.toString();
+        // get the datatype that f belongs to
+        api::Sort sf = f.getSort().getSelectorDomainSort();
+        api::Datatype d = sf.getDatatype();
+        // find the selector
+        api::DatatypeSelector ds = d.getSelector(f.toString());
+        // get the updater term
+        p.d_expr = ds.getUpdaterTerm();
+      }
     | TUPLE_SEL_TOK m=INTEGER_LITERAL
       {
         // we adopt a special syntax (_ tupSel n)
@@ -2226,6 +2242,7 @@ DECLARE_CODATATYPES_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'dec
 PAR_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }?'par';
 COMPREHENSION_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SETS) }?'comprehension';
 TESTER_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'is';
+UPDATE_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'update';
 MATCH_TOK : { ( PARSER_STATE->v2_6() || PARSER_STATE->sygus() ) && PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }?'match';
 GET_MODEL_TOK : 'get-model';
 BLOCK_MODEL_TOK : 'block-model';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 9d4267dd2..2f19d16f0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators()
 
   if (!strictModeEnabled())
   {
+    Parser::addOperator(api::APPLY_UPDATER);
     addOperator(api::DT_SIZE, "dt.size");
   }
 }