Add support for datatypes updater elimination rules in Eunoia (cvc5#1…

…1625)

Furthermore, simplifies the updater elimination rule in a minor way for
simplicity.

Also, fixes a bug in how tuple update terms were output in cpc, and adds
their (missing) definition to the theory file.

This completes the CPC+Eunoia signature for datatypes.

proofs/eo/cpc/programs/Datatypes.eo

@@ -99,5 +99,4 @@
 ; return: >
 ;   The nth argument of t.
 (define $dt_arg_nth ((T Type :implicit) (t T) (n Int))
-  (eo::list_nth @list ($dt_arg_list t) n)
-)
+  (eo::list_nth @list ($dt_arg_list t) n))

proofs/eo/cpc/rules/Datatypes.eo

@@ -295,3 +295,134 @@
   :requires ((($dt_find_cycle t (@list s)) true)) 
   :conclusion (= (= s t) false)
 )
+
+;;;;; ProofRewriteRule::DT_COLLAPSE_UPDATER
+
+; program: $mk_dt_collapse_updater_rhs
+; args:
+; - c U: The remaining term to process.
+; - a T: The value to replace as an argument of t.
+; - n Int: The argument position (from the end) which a should replace.
+; return: >
+;   The result of updating the n^th argument from the end in t.
+(program $dt_collapse_updater_rhs ((U Type) (T Type) (f (-> T U)) (x T) (a T) (n Int))
+  (U T Int) U
+  (
+    (($dt_collapse_updater_rhs (f x) a 0)  (f a))
+    (($dt_collapse_updater_rhs (f x) a n)  (_ ($dt_collapse_updater_rhs f a (eo::add n -1)) x))
+  )
+)
+
+; program: $tuple_collapse_updater_rhs
+; args:
+; - c U: The remaining tuple term to process.
+; - a T: The value to replace as an argument of t.
+; - n Int: The argument position which a should replace.
+; return: >
+;   The result of updating the n^th argument in t.
+(program $tuple_collapse_updater_rhs ((U Type) (T Type) (W Type) (f (-> T U)) (x T) (a T) (b T) (n Int) (ts W :list))
+  (U T Int) U
+  (
+  (($tuple_collapse_updater_rhs (tuple b ts) a 0)   (tuple a ts))
+  (($tuple_collapse_updater_rhs (tuple b ts) a n)   (eo::cons tuple b ($tuple_collapse_updater_rhs ts a (eo::add n -1))))
+  (($tuple_collapse_updater_rhs tuple.unit a n)     tuple.unit)
+  )
+)
+
+; program: $mk_dt_collapse_updater_rhs
+; args:
+; - c U: The update term to process, expected to be an updater applied to a constructor application.
+; return: >
+;   The result of collasping the update term.
+(program $mk_dt_collapse_updater_rhs ((D Type) (T Type) (W Type) (s (-> D T)) (t D) (a T) (tr D) (n Int))
+  (D) Bool
+  (
+  (($mk_dt_collapse_updater_rhs (update s t a))       (eo::define ((c ($get_fun t)))
+                                                      (eo::define ((ss ($dt_get_selectors (eo::typeof t) c)))
+                                                      (eo::define ((index (eo::list_find eo::List::cons ss s)))
+                                                        (eo::ite (eo::is_neg index)
+                                                          t ; unchanged if not correct constructor
+                                                          ($dt_collapse_updater_rhs t a (eo::add (eo::len ss) index -1)))))))
+  (($mk_dt_collapse_updater_rhs (tuple.update n t a)) ($tuple_collapse_updater_rhs t a n))
+  )
+)
+
+; rule: dt-collapse-updater
+; implements: ProofRewriteRule::DT_COLLAPSE_UPDATER
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   We require that the index^th argument of the term t we are selecting from
+;   is the right hand side of the equality, where index is the index of the
+;   selector in the constructor of t.
+; conclusion: The given equality.
+(declare-rule dt-collapse-updater ((D Type) (t D) (s D))
+  :args ((= t s))
+  :requires ((($mk_dt_collapse_updater_rhs t) s))
+  :conclusion (= t s)
+)
+
+;;;;; ProofRewriteRule::DT_UPDATER_ELIM
+
+; program: $dt_updater_elim_rhs
+; args:
+; - s (-> D T): the selector specifying the argument.
+; - D t: The datatype term we are updating.
+; - a T: The value to replace at the s argument of t.
+; - ss eo::List: The remaining selector arguments to process.
+; - c U: The result of updating t we have accumulated so far.
+; return: >
+;   The result of updating the argument specified by s in t.
+(program $dt_updater_elim_rhs ((D Type) (T Type) (U Type) (s (-> D T)) (s1 (-> D T)) (t D) (a T) (ss eo::List :list) (c U))
+  ((-> D T) D T eo::List U) D
+  (
+    (($dt_updater_elim_rhs s t a (eo::List::cons s ss) c)   ($dt_updater_elim_rhs s t a ss (c a)))
+    (($dt_updater_elim_rhs s t a (eo::List::cons s1 ss) c)  ($dt_updater_elim_rhs s t a ss (c (s1 t))))
+    (($dt_updater_elim_rhs s t a eo::List::nil c)           c)
+  )
+)
+
+; program: $tuple_updater_elim_rhs
+; args:
+; - n Int: the index specifying the argument.
+; - D t: The tuple term we are updating.
+; - a T: The value to replace at the n^th argument of t.
+; - ss eo::List: The remaining selector arguments to process.
+; return: >
+;   The result of updating the argument specified by s in t.
+(program $tuple_updater_elim_rhs ((D Type) (T Type) (U Type) (n Int) (s (-> D T)) (t D) (a T) (ss eo::List :list) (c U))
+  (Int D T eo::List) D
+  (
+    (($tuple_updater_elim_rhs n t a (eo::List::cons (tuple.select n) ss))   (eo::cons tuple a ($tuple_updater_elim_rhs n t a ss)))
+    (($tuple_updater_elim_rhs n t a (eo::List::cons s ss))                  (eo::cons tuple (s t) ($tuple_updater_elim_rhs n t a ss)))
+    (($tuple_updater_elim_rhs n t a eo::List::nil)                          tuple.unit)
+  )
+)
+
+; program: $mk_dt_updater_elim_rhs
+; args:
+; - s D: The update term.
+; - ss eo::List: The list of selectors for the type of s.
+; return: >
+;   The right hand side is obtained by updating the proper argument of t.
+(program $mk_dt_updater_elim_rhs ((D Type) (T Type) (U Type) (s (-> D T)) (t D) (a T) (tr D) (c U) (n Int) (ss eo::List))
+  (D U eo::List) Bool
+  (
+    (($mk_dt_updater_elim_rhs (update s t a) c ss)            ($dt_updater_elim_rhs s t a ss ($dt_inst_cons_of (eo::typeof t) c))) ; ensure the constructor is annotated
+    (($mk_dt_updater_elim_rhs (tuple.update n t a) tuple ss)  ($tuple_updater_elim_rhs n t a ss))
+  )
+)
+
+; rule: dt-updater-elim
+; implements: ProofRewriteRule::DT_UPDATER_ELIM
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   We require that the right hand side is an ITE where the then branch is
+;   obtained by updating the proper argument of t, as implemented by $is_dt_updater_elim.
+; conclusion: The given equality.
+(declare-rule dt-updater-elim ((D Type) (S Type) (T Type) (C Type) (s S) (t D) (a T) (u (-> S D T D)) (tu D) (c C))
+  :args ((= (u s t a) (ite (is c t) tu t)))
+  :requires ((($mk_dt_updater_elim_rhs (u s t a) c ($dt_get_selectors (eo::typeof t) c)) tu))
+  :conclusion (= (u s t a) (ite (is c t) tu t))
+)

proofs/eo/cpc/theories/Datatypes.eo

@@ -32,6 +32,10 @@
 (declare-const tuple.select
     (-> (! Type :var T :implicit)
         (! Int :var i) T (eo::list_nth Tuple T i)))
+; disclaimer: This function is not in the SMT-LIB standard.
+(declare-const tuple.update
+    (-> (! Type :var T :implicit)
+        (! Int :var i) T (eo::list_nth Tuple T i) T))
 
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further function

src/proof/alf/alf_node_converter.cpp

@@ -54,7 +54,9 @@ BaseAlfNodeConverter::BaseAlfNodeConverter(NodeManager* nm) : NodeConverter(nm)
 
 AlfNodeConverter::AlfNodeConverter(NodeManager* nm) : BaseAlfNodeConverter(nm)
 {
-  d_sortType = nm->mkSort("sortType");
+  // use builtin operator type as the type of sorts, which makes a difference
+  // e.g. for converting terms of kind SORT_TO_TERM.
+  d_sortType = nm->builtinOperatorType();
 }
 
 AlfNodeConverter::~AlfNodeConverter() {}
@@ -155,7 +157,7 @@ Node AlfNodeConverter::postConvert(Node n)
     // must ensure we print higher-order function applications with "_"
     if (!n.getOperator().isVar())
     {
-    TypeNode tn = n.getType();
+      TypeNode tn = n.getType();
       std::vector<Node> args;
       args.push_back(n.getOperator());
       args.insert(args.end(), n.begin(), n.end());
@@ -322,6 +324,10 @@ Node AlfNodeConverter::postConvert(Node n)
     // is refactored to silently ignore this kind, this case can be deleted.
     return n[0];
   }
+  else if (k == Kind::SORT_TO_TERM)
+  {
+    return typeAsNode(n.getConst<SortToTerm>().getType());
+  }
   else if (GenericOp::isIndexedOperatorKind(k))
   {
     TypeNode tn = n.getType();
@@ -524,17 +530,14 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n)
         size_t index = DType::indexOf(op);
         const DType& dt = DType::datatypeOf(op);
         size_t cindex = DType::cindexOf(op);
-        opName << "update";
         if (dt.isTuple())
         {
-          std::vector<Node> args;
-          args.push_back(d_nm->mkConstInt(cindex));
-          Node ssym = mkInternalApp(
-              "tuple.select", args, dt[cindex][index].getSelector().getType());
-          indices.push_back(ssym);
+          opName << "tuple.update";
+          indices.push_back(d_nm->mkConstInt(index));
         }
         else
         {
+          opName << "update";
           indices.push_back(dt[cindex][index].getSelector());
         }
       }

src/proof/alf/alf_printer.cpp

@@ -309,6 +309,8 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n)
     case ProofRewriteRule::DT_CONS_EQ:
     case ProofRewriteRule::DT_CONS_EQ_CLASH:
     case ProofRewriteRule::DT_CYCLE:
+    case ProofRewriteRule::DT_COLLAPSE_UPDATER:
+    case ProofRewriteRule::DT_UPDATER_ELIM:
     case ProofRewriteRule::QUANT_MERGE_PRENEX:
     case ProofRewriteRule::QUANT_MINISCOPE_AND:
     case ProofRewriteRule::QUANT_MINISCOPE_OR:

src/theory/datatypes/datatypes_rewriter.cpp

@@ -1158,13 +1158,11 @@ Node DatatypesRewriter::expandUpdater(const Node& n)
     }
   }
   ret = b;
-  if (dt.getNumConstructors() > 1)
-  {
-    // must be the right constructor to update
-    Node tester = nm->mkNode(Kind::APPLY_TESTER, dc.getTester(), n[0]);
-    ret = nm->mkNode(Kind::ITE, tester, ret, n[0]);
-  }
-  return ret;
+  // note it may be that this dt has one constructor, in which case this
+  // tester will rewrite to true.
+  // must be the right constructor to update
+  Node tester = nm->mkNode(Kind::APPLY_TESTER, dc.getTester(), n[0]);
+  return nm->mkNode(Kind::ITE, tester, ret, n[0]);
 }
 Node DatatypesRewriter::expandNullableLift(Node n)
 {