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

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

6 files changed, 321 insertions, 0 deletions

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);