Minimal fixing version for tuple update parsing (#7228)

This takes the essential changes from #7218 so that the current ANTLR issues are avoided.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8f9e01c6cf545b013349149080cedb690c3d71e4..674aeca1fd1bfa2e45b37ecff96532f1a410d489 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1577,12 +1577,13 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
  * - For declared functions f, we return (2).
  * - For indexed functions like testers (_ is C) and bitvector extract
  * (_ extract n m), we return (3) for the appropriate operator.
- * - For tuple selectors (_ tupSel n), we return (1) and (3). api::Kind is set to
- * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the
- * caller as the n^th generic tuple selector. We do this since there is no
- * AST expression representing generic tuple select, and we do not have enough
- * type information at this point to know the type of the tuple we will be
- * selecting from.
+ * - For tuple selectors (_ tuple_select n) and updaters (_ tuple_update n), we
+ * return (1) and (3). api::Kind is set to APPLY_SELECTOR or APPLY_UPDATER
+ * respectively, and expr is set to n, which is to be interpreted by the
+ * caller as the n^th generic tuple selector or updater. We do this since there
+ * is no AST expression representing generic tuple select, and we do not have
+ * enough type information at this point to know the type of the tuple we will
+ * be selecting from.
  *
  * (Ascripted Identifiers)
  *
@@ -1703,7 +1704,35 @@ identifier[cvc5::ParseOp& p]
       }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
-        p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
+        std::string opName = AntlrInput::tokenText($sym);
+        api::Kind k = PARSER_STATE->getIndexedOpKind(opName);
+        if (k == api::APPLY_UPDATER)
+        {
+          // we adopt a special syntax (_ tuple_update n) for tuple updaters
+          if (numerals.size() != 1)
+          {
+            PARSER_STATE->parseError(
+                "Unexpected syntax for tuple selector or updater.");
+          }
+          // The operator is dependent upon inferring the type of the arguments,
+          // and hence the type is not available yet. Hence, we remember the
+          // index as a numeral in the parse operator.
+          p.d_kind = k;
+          p.d_expr = SOLVER->mkInteger(numerals[0]);
+        }
+        else if (numerals.size() == 1)
+        {
+          p.d_op = SOLVER->mkOp(k, numerals[0]);
+        }
+        else if (numerals.size() == 2)
+        {
+          p.d_op = SOLVER->mkOp(k, numerals[0], numerals[1]);
+        }
+        else
+        {
+          PARSER_STATE->parseError(
+              "Unexpected number of numerals for indexed symbol.");
+        }
       }
     )
     RPAREN_TOK

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2fd4a55967e3fa53cedd90783d0531af8d61f4a4..40716d9087b9e0c30734165807292db9b7c7134d 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,6 +135,7 @@ void Smt2::addDatatypesOperators()
   {
     Parser::addOperator(api::APPLY_UPDATER);
     addOperator(api::DT_SIZE, "dt.size");
+    addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update");
   }
 }
 
@@ -382,25 +383,15 @@ api::Term Smt2::mkIndexedConstant(const std::string& name,
   return api::Term();
 }
 
-api::Op Smt2::mkIndexedOp(const std::string& name,
-                          const std::vector<uint64_t>& numerals)
+api::Kind Smt2::getIndexedOpKind(const std::string& name)
 {
   const auto& kIt = d_indexedOpKindMap.find(name);
   if (kIt != d_indexedOpKindMap.end())
   {
-    api::Kind k = (*kIt).second;
-    if (numerals.size() == 1)
-    {
-      return d_solver->mkOp(k, numerals[0]);
-    }
-    else if (numerals.size() == 2)
-    {
-      return d_solver->mkOp(k, numerals[0], numerals[1]);
-    }
+    return (*kIt).second;
   }
-
   parseError(std::string("Unknown indexed function `") + name + "'");
-  return api::Op();
+  return api::UNDEFINED_KIND;
 }
 
 api::Term Smt2::bindDefineFunRec(
@@ -1037,22 +1028,24 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     Debug("parser") << "applyParseOp: return store all " << ret << std::endl;
     return ret;
   }
-  else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
+  else if ((p.d_kind == api::APPLY_SELECTOR || p.d_kind == api::APPLY_UPDATER)
+           && !p.d_expr.isNull())
   {
     // tuple selector case
     if (!p.d_expr.isUInt64Value())
     {
-      parseError("index of tupSel is larger than size of uint64_t");
+      parseError(
+          "index of tuple select or update is larger than size of uint64_t");
     }
     uint64_t n = p.d_expr.getUInt64Value();
-    if (args.size() != 1)
+    if (args.size() != (p.d_kind == api::APPLY_SELECTOR ? 1 : 2))
     {
-      parseError("tupSel should only be applied to one tuple argument");
+      parseError("wrong number of arguments for tuple select or update");
     }
     api::Sort t = args[0].getSort();
     if (!t.isTuple())
     {
-      parseError("tupSel applied to non-tuple");
+      parseError("tuple select or update applied to non-tuple");
     }
     size_t length = t.getTupleLength();
     if (n >= length)
@@ -1062,8 +1055,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError(ss.str());
     }
     const api::Datatype& dt = t.getDatatype();
-    api::Term ret = d_solver->mkTerm(
-        api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
+    api::Term ret;
+    if (p.d_kind == api::APPLY_SELECTOR)
+    {
+      ret = d_solver->mkTerm(
+          api::APPLY_SELECTOR, dt[0][n].getSelectorTerm(), args[0]);
+    }
+    else
+    {
+      ret = d_solver->mkTerm(
+          api::APPLY_UPDATER, dt[0][n].getUpdaterTerm(), args[0], args[1]);
+    }
     Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
     return ret;
   }

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 97eb95c003b30f33f73695d2585be3b02f51fdd4..fd68732fe688e073afab4109f9baa8aa87a2db2f 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -121,15 +121,13 @@ class Smt2 : public Parser
                               const std::vector<uint64_t>& numerals);
 
   /**
-   * Creates an indexed operator term, e.g. (_ extract 5 0).
+   * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".
    *
    * @param name The name of the operator (e.g. "extract")
-   * @param numerals The parameters for the operator (e.g. [5, 0])
-   * @return The operator term corresponding to the indexed operator or a parse
+   * @return The kind corresponding to the indexed operator or a parse
    *         error if the name is not valid.
    */
-  api::Op mkIndexedOp(const std::string& name,
-                      const std::vector<uint64_t>& numerals);
+  api::Kind getIndexedOpKind(const std::string& name);
 
   /**
    * Returns the expression that name should be interpreted as.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6217276b1698241f4744c945fe4cae305059fe36..3c0fe838bad2380d2253fb6fd0bfd64a26656308 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -791,11 +791,19 @@ void Smt2Printer::toStream(std::ostream& out,
     size_t index = DType::indexOf(op);
     const DType& dt = DType::datatypeOf(op);
     size_t cindex = DType::cindexOf(op);
-    out << "(_ update ";
-    toStream(out,
-             dt[cindex][index].getSelector(),
-             toDepth < 0 ? toDepth : toDepth - 1);
-    out << ") ";
+    if (dt.isTuple())
+    {
+      stillNeedToPrintParams = false;
+      out << "(_ tuple_update " << DType::indexOf(op) << ") ";
+    }
+    else
+    {
+      out << "(_ update ";
+      toStream(out,
+               dt[cindex][index].getSelector(),
+               toDepth < 0 ? toDepth : toDepth - 1);
+      out << ") ";
+    }
   }
   break;
   case kind::APPLY_SELECTOR_TOTAL:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 301e26bf92ed185a74ddc8f34ca746c189eba29e..47d352695e084fb952a29b5cf2a3cbe3053e5ae9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -522,6 +522,7 @@ set(regress_0_tests
   regress0/datatypes/tuple-no-clash.cvc
   regress0/datatypes/tuple-record-bug.cvc
   regress0/datatypes/tuple.cvc
+  regress0/datatypes/tuple_update.smt2
   regress0/datatypes/tuples-empty.smt2
   regress0/datatypes/tuples-multitype.smt2
   regress0/datatypes/typed_v10l30054.cvc

diff --git a/test/regress/regress0/datatypes/tuple_update.smt2 b/test/regress/regress0/datatypes/tuple_update.smt2
new file mode 100644 (file)
index 0000000..9812da7
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple_update.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () (Tuple Int Int))
+(declare-fun y () (Tuple Int Int))
+(assert (= ((_ tuple_update 0) x 1) ((_ tuple_update 1) y 2)))
+(check-sat)