(proof-new) Add datatypes proof checker (#5340)

This adds the proof rules and proof checker for datatypes.

4 files changed, 237 insertions, 0 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 9448e1939..4ba483101 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -114,6 +114,13 @@ const char* toString(PfRule id)
     case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
     case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
     case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
+    //================================================= Datatype rules
+    case PfRule::DT_UNIF: return "DT_UNIF";
+    case PfRule::DT_INST: return "DT_INST";
+    case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
+    case PfRule::DT_SPLIT: return "DT_SPLIT";
+    case PfRule::DT_CLASH: return "DT_CLASH";
+    case PfRule::DT_TRUST: return "DT_TRUST";
     //================================================= Quantifiers rules
     case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 2b5565318..19efe6285 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -674,6 +674,52 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: F
   ARRAYS_TRUST,
+  
+  //================================================= Datatype rules
+  // ======== Unification
+  // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
+  // Arguments: (i)
+  // ----------------------------------------
+  // Conclusion: (= ti si)
+  // where C is a constructor.
+  DT_UNIF,
+  // ======== Instantiate
+  // Children: none
+  // Arguments: (t, n)
+  // ----------------------------------------
+  // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
+  // where C is the n^th constructor of the type of T, and (_ is C) is the
+  // discriminator (tester) for C.
+  DT_INST,
+  // ======== Collapse
+  // Children: none
+  // Arguments: ((sel_i (C_j t_1 ... t_n)))
+  // ----------------------------------------
+  // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
+  // where C_j is a constructor, r is t_i if sel_i is a correctly applied
+  // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
+  // that the use of mkGroundTerm differs from the rewriter which uses
+  // mkGroundValue in this case.
+  DT_COLLAPSE,
+  // ======== Split
+  // Children: none
+  // Arguments: (t)
+  // ----------------------------------------
+  // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
+  DT_SPLIT,
+  // ======== Clash
+  // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
+  // Arguments: none
+  // ----------------------------------------
+  // Conclusion: false
+  // for i != j.
+  DT_CLASH,
+  // ======== Datatype Trust
+  // Children: (P1 ... Pn)
+  // Arguments: (F)
+  // ---------------------
+  // Conclusion: F
+  DT_TRUST,
 
   //================================================= Quantifiers rules
   // ======== Witness intro
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
new file mode 100644
index 000000000..98060480b
--- /dev/null
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of datatypes proof checker
+ **/
+
+#include "theory/datatypes/proof_checker.h"
+
+#include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  pc->registerChecker(PfRule::DT_UNIF, this);
+  pc->registerChecker(PfRule::DT_INST, this);
+  pc->registerChecker(PfRule::DT_COLLAPSE, this);
+  pc->registerChecker(PfRule::DT_SPLIT, this);
+  pc->registerChecker(PfRule::DT_CLASH, this);
+  // trusted rules
+  pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
+}
+
+Node DatatypesProofRuleChecker::checkInternal(PfRule id,
+                                              const std::vector<Node>& children,
+                                              const std::vector<Node>& args)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (id == PfRule::DT_UNIF)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    uint32_t i;
+    if (children[0].getKind() != kind::EQUAL
+        || children[0][0].getKind() != kind::APPLY_CONSTRUCTOR
+        || children[0][1].getKind() != kind::APPLY_CONSTRUCTOR
+        || children[0][0].getOperator() != children[0][1].getOperator()
+        || !getUInt32(args[0], i))
+    {
+      return Node::null();
+    }
+    if (i >= children[0][0].getNumChildren())
+    {
+      return Node::null();
+    }
+    Assert(children[0][0].getNumChildren() == children[0][1].getNumChildren());
+    return children[0][0][i].eqNode(children[0][1][i]);
+  }
+  else if (id == PfRule::DT_INST)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    Node t = args[0];
+    TypeNode tn = t.getType();
+    uint32_t i;
+    if (!tn.isDatatype() || !getUInt32(args[1], i))
+    {
+      return Node::null();
+    }
+    const DType& dt = tn.getDType();
+    if (i >= dt.getNumConstructors())
+    {
+      return Node::null();
+    }
+    Node tester = utils::mkTester(t, i, dt);
+    Node ticons = Rewriter::rewrite(utils::getInstCons(t, dt, i));
+    return tester.eqNode(t.eqNode(ticons));
+  }
+  else if (id == PfRule::DT_COLLAPSE)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Node t = args[0];
+    if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
+        || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
+    {
+      return Node::null();
+    }
+    Node selector = t.getOperator();
+    size_t constructorIndex = utils::indexOf(t[0].getOperator());
+    const DType& dt = utils::datatypeOf(selector);
+    const DTypeConstructor& dtc = dt[constructorIndex];
+    int selectorIndex = dtc.getSelectorIndexInternal(selector);
+    Node r =
+        selectorIndex < 0 ? t.getType().mkGroundTerm() : t[0][selectorIndex];
+    return t.eqNode(r);
+  }
+  else if (id == PfRule::DT_SPLIT)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    TypeNode tn = args[0].getType();
+    if (!tn.isDatatype())
+    {
+      return Node::null();
+    }
+    const DType& dt = tn.getDType();
+    return utils::mkSplit(args[0], dt);
+  }
+  else if (id == PfRule::DT_CLASH)
+  {
+    Assert(children.size() == 2);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::APPLY_TESTER
+        || children[1].getKind() != kind::APPLY_TESTER
+        || children[0][0] != children[1][0] || children[0] == children[1])
+    {
+      return Node::null();
+    }
+    return nm->mkConst(false);
+  }
+  else if (id == PfRule::DT_TRUST)
+  {
+    Assert(!args.empty());
+    Assert(args[0].getType().isBoolean());
+    return args[0];
+  }
+  // no rule
+  return Node::null();
+}
+
+}  // namespace datatypes
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h
new file mode 100644
index 000000000..e5bd7cad5
--- /dev/null
+++ b/src/theory/datatypes/proof_checker.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Datatypes proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
+#define CVC4__THEORY__DATATYPES__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+/** A checker for array reasoning in proofs */
+class DatatypesProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  DatatypesProofRuleChecker() {}
+  ~DatatypesProofRuleChecker() {}
+
+  /** Register all rules owned by this rule checker into pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace datatypes
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__DATATYPES__PROOF_CHECKER_H */