Add two datatypes rules to CPC Eunoia signature (cvc5#11358)

Also refactors tuples and nullables to use a more uniform syntax.

Further rules to follow.

proofs/eo/cpc/Cpc.eo

@@ -70,7 +70,7 @@
 (include "./theories/Bags.eo")
 (include "./theories/FiniteFields.eo")
 (include "./rules/Quantifiers.eo")
-(include "./theories/Datatypes.eo")
+(include "./rules/Datatypes.eo")
 (include "./theories/SepLogic.eo")
 (include "./rules/Rewrites.eo")
 

proofs/eo/cpc/rules/Datatypes.eo

@@ -0,0 +1,146 @@
+(include "../theories/Datatypes.eo")
+
+
+; program: $dt_get_constructors
+; args:
+; - T Type: The datatype to get the constructors for.
+; return: The list of constructors of T, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes with a single
+;   constructor. Parametric datatypes must reference the type constructor to
+;   extract their constructors.
+(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type)))
+  (Type) eo::List
+  (
+    (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil))
+    (($dt_get_constructors UnitTuple)     (eo::cons eo::List::cons tuple.unit eo::List::nil))
+    (($dt_get_constructors (DC T))        ($dt_get_constructors DC))   ; user-defined parameteric datatypes, traverse
+    (($dt_get_constructors D)             (eo::dt_constructors D))     ; ordinary user-defined datatypes
+  )
+)
+
+; program: $tuple_get_selectors_rec
+; args:
+; - T Type: The tuple type to get the selectors for.
+; - n Int: The number of component types we have processed so far.
+; return: The list of selectors of T, as a eo::List.
+; note: >
+;   Tuples use a special selector tuple.select indexed by an integer, which is
+;   why they require a special method here.
+(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int))
+  (Type Int) Bool
+  (
+    (($tuple_get_selectors_rec UnitTuple n)     eo::List::nil)
+    (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1))))
+  )
+)
+
+; program: $dt_get_selectors
+; args:
+; - D Type: The type to get the selectors for.
+; - c T: The constructor of D.
+; return: The list of selectors of c, as a eo::List.
+; note: >
+;   (Unit) tuples are treated as a special case of datatypes whose selectors are
+;   tuple.select indexed by an integer, which requires the above method.
+(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list))
+  (Type T) eo::List
+  (
+    (($dt_get_selectors (Tuple T1 T2) tuple)  ($tuple_get_selectors_rec (Tuple T1 T2) 0))
+    (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil)
+    (($dt_get_selectors D c)                  (eo::dt_selectors c)) ; user-defined datatypes
+  )
+)
+
+;;;;; ProofRule::DT_SPLIT
+
+; program: $mk_dt_split
+; args:
+; - L eo::List: The list of a constructors yet to process.
+; - x D: The datatype term we are splitting on.
+; return: A disjunction of testers for the constructors in L, applied to x.
+(program $mk_dt_split ((D Type) (x D) (T Type) (c T) (xs eo::List :list))
+  (eo::List D) Bool
+  (
+    (($mk_dt_split eo::List::nil x)          false)
+    (($mk_dt_split (eo::List::cons c xs) x)  (eo::cons or (is c x) ($mk_dt_split xs x)))
+  )
+)
+
+; rule: dt_split
+; implements: ProofRule::DT_SPLIT.
+; args:
+; - x D: The datatype term to split on.
+; conclusion: >
+;   A disjunction of testers, indicating the possible top symbols of x. This is
+;   computed by getting the constructors for the type of x and calling the above
+;   $mk_dt_split method.
+(declare-rule dt_split ((D Type) (x D))
+  :args (x)
+  :conclusion ($singleton_elim ($mk_dt_split ($dt_get_constructors (eo::typeof x)) x))
+)
+
+;;;;; ProofRewriteRule::DT_INST
+
+; program: $mk_dt_inst_rec
+; args:
+; - L eo::List: The list of a selectors yet to process.
+; - x D: The datatype term we applying dt-inst to.
+; - t T: The accumulated return value, which is a constructor applied to a list of testers applied to x.
+; return: The result of dt-inst for x, given t and the remaining selectors in x.
+(program $mk_dt_inst_rec ((D Type) (x D) (T Type) (t T) (S Type) (s S) (xs eo::List :list))
+  (eo::List D T) Bool
+  (
+    (($mk_dt_inst_rec eo::List::nil x t)          t)
+    (($mk_dt_inst_rec (eo::List::cons s xs) x t)  ($mk_dt_inst_rec xs x (t (s x))))
+  )
+)
+
+; program: $mk_dt_inst_tuple_rec
+; args:
+; - T Type: The type of x we have yet to process.
+; - x D: The tuple term we applying dt-inst to.
+; - n Int: The number of component types of the type of x we have processed.
+; return: The result of dt-inst for x, given t and the remaining selectors in x.
+; note: >
+;   This method is different from $mk_dt_inst_rec since the constructor tuple
+;   is n-ary. For example, for (Tuple Int Int), this method will return
+;   (tuple (tuple.select 0 x) (tuple (tuple.select 1 x) tuple.unit)), whereas
+;   for an ordinary constructor C : (-> Int Int D) with selectors s1, s2,
+;   $mk_dt_inst_rec above returns (C (s1 x) (s2 x)).
+(program $mk_dt_inst_tuple_rec ((D Type) (x D) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int))
+  (Type D Int) Bool
+  (
+    (($mk_dt_inst_tuple_rec UnitTuple x n)     tuple.unit)
+    (($mk_dt_inst_tuple_rec (Tuple T1 T2) x n) (eo::cons tuple (tuple.select n x) ($mk_dt_inst_tuple_rec T2 x (eo::add n 1))))
+  )
+)
+
+; program: $mk_dt_inst
+; args:
+; - D Type: The datatype we are considering.
+; - c C: The constructor of datatype D.
+; - x D: The datatype term of type D we are applying dt-inst to.
+; return: An equality that is equivalent to (is c x).
+(program $mk_dt_inst ((C Type) (D Type) (x D) (c C) (T1 Type) (T2 Type :list) (DC (-> Type Type)))
+  (Type C D) Bool
+  (
+    (($mk_dt_inst (Tuple T1 T2) tuple x)  ($mk_dt_inst_tuple_rec (Tuple T1 T2) x 0))
+    (($mk_dt_inst UnitTuple tuple.unit x) tuple.unit)
+    (($mk_dt_inst D c x)                  ($mk_dt_inst_rec ($dt_get_selectors D c) x c)) ; user-defined datatypes
+  )
+)
+
+; rule: dt-inst
+; implements: ProofRewriteRule::DT_INST.
+; args:
+; - eq Bool: The equality to prove.
+; requires: >
+;   We require that $mk_dt_inst applied to the left hand side returns
+;   the right hand side.
+; conclusion: The given equality.
+(declare-rule dt-inst ((D Type) (T Type) (c T) (x D) (t T))
+  :args ((= (is c x) (= x t)))
+  :requires ((($mk_dt_inst (eo::typeof x) c x) t))
+  :conclusion (= (is c x) (= x t))
+)

proofs/eo/cpc/theories/Datatypes.eo

@@ -1,5 +1,22 @@
 (include "../programs/Nary.eo")
 
+; note: >
+;  This is the generic tester predicate whose first argument is expected to be
+;  a constructor symbol for datatype D. We do not currently check this is the
+;  case.
+(declare-const is (-> (! Type :var C :implicit)
+                      (! Type :var D :implicit)
+                      C D Bool))
+
+; note: >
+;  This is the generic updater whose first argument is expected to be
+;  a selector symbol for datatype D. We do not currently check this is the
+;  case.
+(declare-const update (-> (! Type :var D :implicit)
+                          (! Type :var T :implicit)
+                          (! Type :var S :implicit)
+                          S D T D))
+
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further function
 ;   symbols over this sort are also not part of the SMT-LIB standard.
@@ -15,19 +32,13 @@
 (declare-const tuple.select
     (-> (! Type :var T :implicit)
         (! Int :var i) T (eo::list_nth Tuple T i)))
-(declare-const tuple.update
-    (-> (! Type :var T :implicit) (! Type :var S :implicit)
-        Int T S T))
-(declare-const is-tuple (-> (! Type :var T :implicit) T Bool))
 
 ; disclaimer: >
 ;   This sort is not in the SMT-LIB standard. All further function
 ;   symbols over this sort are also not part of the SMT-LIB standard.
 (declare-const Nullable (-> Type Type))
 (declare-const nullable.null (-> (! Type :var T) (Nullable T)))
 (declare-const nullable.some (-> (! Type :var T :implicit) T (Nullable T)))
-(declare-const nullable.is_some (-> (! Type :var T :implicit) (Nullable T) Bool))
-(declare-const nullable.is_null (-> (! Type :var T :implicit) (Nullable T) Bool))
 (declare-const nullable.val (-> (! Type :var T :implicit) (Nullable T) T))
 
 ; program: $get_type_nullable_lift

src/proof/alf/alf_node_converter.cpp

@@ -457,43 +457,39 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n, bool reqCast)
     {
       if (k == Kind::APPLY_TESTER)
       {
+        indices.clear();
         size_t cindex = DType::indexOf(op);
         const DType& dt = DType::datatypeOf(op);
+        opName << "is";
         if (dt.isTuple())
         {
-          opName << "is-tuple";
-        }
-        else if (dt.isNullable())
-        {
-          if (cindex == 0)
-          {
-            opName << "nullable.is_null";
-          }
-          else
-          {
-            opName << "nullable.is_some";
-          }
+          std::string tname = dt[0].getNumArgs() == 0 ? "tuple.unit" : "tuple";
+          Node tsym = mkInternalSymbol(tname, dt[0].getConstructor().getType());
+          indices.push_back(tsym);
         }
         else
         {
-          opName << "is-" << dt[cindex].getConstructor();
+          indices.push_back(dt[cindex].getConstructor());
         }
-        indices.clear();
       }
       else if (k == Kind::APPLY_UPDATER)
       {
         indices.clear();
         size_t index = DType::indexOf(op);
         const DType& dt = DType::datatypeOf(op);
         size_t cindex = DType::cindexOf(op);
+        opName << "update";
         if (dt.isTuple())
         {
-          opName << "tuple.update";
-          indices.push_back(d_nm->mkConstInt(cindex));
+          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);
         }
         else
         {
-          opName << "update-" << dt[cindex][index].getSelector();
+          indices.push_back(dt[cindex][index].getSelector());
         }
       }
       else if (k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV)

src/proof/alf/alf_printer.cpp

@@ -172,6 +172,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
     case ProofRule::STRING_SEQ_UNIT_INJ:
     case ProofRule::STRING_DECOMPOSE:
     case ProofRule::STRING_EXT:
+    case ProofRule::DT_SPLIT:
     case ProofRule::ITE_EQ:
     case ProofRule::INSTANTIATE:
     case ProofRule::SKOLEMIZE:
@@ -274,6 +275,7 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n)
     case ProofRewriteRule::EXISTS_ELIM:
     case ProofRewriteRule::QUANT_UNUSED_VARS:
     case ProofRewriteRule::ARRAYS_SELECT_CONST:
+    case ProofRewriteRule::DT_INST:
     case ProofRewriteRule::QUANT_MERGE_PRENEX:
     case ProofRewriteRule::QUANT_MINISCOPE:
     case ProofRewriteRule::QUANT_MINISCOPE_FV: