(proof-new) Add the arrays proof checker (#5047)

Includes adding the standard method for constructing the extensionality skolem using the skolem manager.

9 files changed, 365 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5695e271e..a72a5f6bb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -366,6 +366,10 @@ libcvc4_add_sources(
   theory/arith/type_enumerator.h
   theory/arrays/array_info.cpp
   theory/arrays/array_info.h
+  theory/arrays/proof_checker.cpp
+  theory/arrays/proof_checker.h
+  theory/arrays/skolem_cache.cpp
+  theory/arrays/skolem_cache.h
   theory/arrays/theory_arrays.cpp
   theory/arrays/theory_arrays.h
   theory/arrays/theory_arrays_rewriter.cpp
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 57dd3e0bd..400567b5d 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -102,6 +102,13 @@ const char* toString(PfRule id)
     case PfRule::FALSE_ELIM: return "FALSE_ELIM";
     case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
     case PfRule::HO_CONG: return "HO_CONG";
+    //================================================= Array rules
+    case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
+    case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA:
+      return "ARRAYS_READ_OVER_WRITE_CONTRA";
+    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";
     //================================================= 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 c02292dab..a51cb92f0 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -595,6 +595,39 @@ enum class PfRule : uint32_t
   // Notice that this rule is only used when the application kinds are APPLY_UF.
   HO_CONG,
 
+  //================================================= Array rules
+  // ======== Read over write
+  // Children: (P:(not (= i1 i2)))
+  // Arguments: ((select (store a i2 e) i1))
+  // ----------------------------------------
+  // Conclusion: (= (select (store a i2 e) i1) (select a i1))
+  ARRAYS_READ_OVER_WRITE,
+  // ======== Read over write, contrapositive
+  // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
+  // Arguments: none
+  // ----------------------------------------
+  // Conclusion: (= i1 i2)
+  ARRAYS_READ_OVER_WRITE_CONTRA,
+  // ======== Read over write 1
+  // Children: none
+  // Arguments: ((select (store a i e) i))
+  // ----------------------------------------
+  // Conclusion: (= (select (store a i e) i) e)
+  ARRAYS_READ_OVER_WRITE_1,
+  // ======== Extensionality
+  // Children: (P:(not (= a b)))
+  // Arguments: none
+  // ----------------------------------------
+  // Conclusion: (not (= (select a k) (select b k)))
+  // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
+  ARRAYS_EXT,
+  // ======== Array Trust
+  // Children: (P1 ... Pn)
+  // Arguments: (F)
+  // ---------------------
+  // Conclusion: F
+  ARRAYS_TRUST,
+
   //================================================= Quantifiers rules
   // ======== Witness intro
   // Children: (P:F[t])
diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp
new file mode 100644
index 000000000..a3cd82678
--- /dev/null
+++ b/src/theory/arrays/proof_checker.cpp
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 arrays proof checker
+ **/
+
+#include "theory/arrays/proof_checker.h"
+#include "expr/skolem_manager.h"
+#include "theory/arrays/skolem_cache.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE, this);
+  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
+  pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
+  pc->registerChecker(PfRule::ARRAYS_EXT, this);
+  // trusted rules
+  pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
+}
+
+Node ArraysProofRuleChecker::checkInternal(PfRule id,
+                                           const std::vector<Node>& children,
+                                           const std::vector<Node>& args)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (id == PfRule::ARRAYS_READ_OVER_WRITE)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    Node ideq = children[0];
+    if (ideq.getKind() != kind::NOT || ideq[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    Node lhs = args[0];
+    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
+        || lhs[0][1] != ideq[0][0])
+    {
+      return Node::null();
+    }
+    Node rhs = nm->mkNode(kind::SELECT, lhs[0][0], ideq[0][1]);
+    return lhs.eqNode(rhs);
+  }
+  else if (id == PfRule::ARRAYS_READ_OVER_WRITE_CONTRA)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    Node adeq = children[0];
+    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL)
+    {
+      return Node::null();
+    }
+    Node lhs = adeq[0][0];
+    Node rhs = adeq[0][1];
+    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
+        || rhs.getKind() != kind::SELECT || lhs[1] != rhs[1])
+    {
+      return Node::null();
+    }
+    return lhs[1].eqNode(lhs[0][1]);
+  }
+  if (id == PfRule::ARRAYS_READ_OVER_WRITE_1)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    Node lhs = args[0];
+    if (lhs.getKind() != kind::SELECT || lhs[0].getKind() != kind::STORE
+        || lhs[0][1] != lhs[1])
+    {
+      return Node::null();
+    }
+    Node rhs = lhs[0][2];
+    return lhs.eqNode(rhs);
+  }
+  if (id == PfRule::ARRAYS_EXT)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    Node adeq = children[0];
+    if (adeq.getKind() != kind::NOT || adeq[0].getKind() != kind::EQUAL
+        || !adeq[0][0].getType().isArray())
+    {
+      return Node::null();
+    }
+    Node k = SkolemCache::getExtIndexSkolem(adeq);
+    Node a = adeq[0][0];
+    Node b = adeq[0][1];
+    Node as = nm->mkNode(kind::SELECT, a, k);
+    Node bs = nm->mkNode(kind::SELECT, b, k);
+    return as.eqNode(bs).notNode();
+  }
+  if (id == PfRule::ARRAYS_TRUST)
+  {
+    // "trusted" rules
+    Assert(!args.empty());
+    Assert(args[0].getType().isBoolean());
+    return args[0];
+  }
+  // no rule
+  return Node::null();
+}
+
+}  // namespace arrays
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
new file mode 100644
index 000000000..3bf7afecb
--- /dev/null
+++ b/src/theory/arrays/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 Array proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
+#define CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+/** A checker for array reasoning in proofs */
+class ArraysProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  ArraysProofRuleChecker() {}
+  ~ArraysProofRuleChecker() {}
+
+  /** 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 arrays
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARRAYS__PROOF_CHECKER_H */
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
new file mode 100644
index 000000000..70217a4d7
--- /dev/null
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -0,0 +1,87 @@
+/*********************                                                        */
+/*! \file skolem_cache.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 Arrays skolem cache
+ **/
+
+#include "theory/arrays/skolem_cache.h"
+
+#include "expr/attribute.h"
+#include "expr/skolem_manager.h"
+#include "expr/type_node.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+/**
+ * A bound variable corresponding to an index for witnessing the satisfiability
+ * of array disequalities.
+ */
+struct ExtIndexVarAttributeId
+{
+};
+typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute;
+
+SkolemCache::SkolemCache() {}
+
+Node SkolemCache::getExtIndexSkolem(Node deq)
+{
+  Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL);
+  Node a = deq[0][0];
+  Node b = deq[0][1];
+  Assert(a.getType().isArray());
+  Assert(b.getType() == a.getType());
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  // get the reference index, which notice is deterministic for a, b in the
+  // lifetime of the node manager
+  Node x = getExtIndexVar(deq);
+
+  // make the axiom for x
+  Node as = nm->mkNode(SELECT, a, x);
+  Node bs = nm->mkNode(SELECT, b, x);
+  Node deqIndex = as.eqNode(bs).notNode();
+  Node axiom = nm->mkNode(IMPLIES, deq, deqIndex);
+
+  // make the skolem that witnesses the above axiom
+  SkolemManager* sm = nm->getSkolemManager();
+  return sm->mkSkolem(
+      x,
+      axiom,
+      "array_ext_index",
+      "an extensional lemma index variable from the theory of arrays");
+}
+
+Node SkolemCache::getExtIndexVar(Node deq)
+{
+  ExtIndexVarAttribute eiva;
+  if (deq.hasAttribute(eiva))
+  {
+    return deq.getAttribute(eiva);
+  }
+  Node a = deq[0][0];
+  Node b = deq[0][1];
+  TypeNode atn = a.getType();
+  Assert(atn.isArray());
+  Assert(atn == b.getType());
+  TypeNode atnIndex = atn.getArrayIndexType();
+  Node v = NodeManager::currentNM()->mkBoundVar(atnIndex);
+  deq.setAttribute(eiva, v);
+  return v;
+}
+
+}  // namespace arrays
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h
new file mode 100644
index 000000000..b07e87dc6
--- /dev/null
+++ b/src/theory/arrays/skolem_cache.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file skolem_cache.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 Arrays skolem cache
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
+#define CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+/**
+ * The arrays skolem cache, which provides static methods for constructing
+ * skolems with witness forms.
+ */
+class SkolemCache
+{
+ public:
+  SkolemCache();
+  ~SkolemCache() {}
+
+  /**
+   * Get the skolem correspoding to the index that witnesses the disequality
+   * deq between arrays a and b. The witness form of this skolem is:
+   * (witness ((x T)) (=> (not (= a b)) (not (= (select a x) (select b x)))))
+   * This skolem is unique for deq, calling this method will always return the
+   * same skolem over the lifetime of deq.
+   */
+  static Node getExtIndexSkolem(Node deq);
+
+ private:
+  /**
+   * Get the bound variable x of the witness term above for disequality deq
+   * between arrays.
+   */
+  static Node getExtIndexVar(Node deq);
+};
+
+}  // namespace arrays
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 28953ab05..cfa956f8b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -126,6 +126,12 @@ TheoryArrays::TheoryArrays(context::Context* c,
   d_ppEqualityEngine.addFunctionKind(kind::SELECT);
   d_ppEqualityEngine.addFunctionKind(kind::STORE);
 
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    d_pchecker.registerTo(pc);
+  }
+
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
 }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index dea3d4136..a35074f15 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -26,6 +26,7 @@
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "theory/arrays/array_info.h"
+#include "theory/arrays/proof_checker.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -341,6 +342,9 @@ class TheoryArrays : public Theory {
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
+  /** The proof checker */
+  ArraysProofRuleChecker d_pchecker;
+
   /** Conflict when merging constants */
   void conflict(TNode a, TNode b);