17 files changed, 244 insertions, 23 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 908e788f8..1f83c94d6 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 37d442968..e1ca46bfb 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 60883e4ef..1dd9ba8b6 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2,9 +2,9 @@
 /*! \file equality_engine.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Guy Katz, Andrew Reynolds
+ **   Dejan Jovanovic, Andrew Reynolds, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 0ae95b34a..cf6eabfb7 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -2,9 +2,9 @@
 /*! \file equality_engine.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Guy Katz
+ **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0e6d283fe..14cd80436 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -2,9 +2,9 @@
 /*! \file equality_engine_types.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Andrew Reynolds, Andres Noetzli
+ **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 23b7b9217..d90a02486 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -2,9 +2,9 @@
 /*! \file ho_extension.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index 47336e085..d00372c98 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp
new file mode 100644
index 000000000..f866e77dd
--- /dev/null
+++ b/src/theory/uf/proof_checker.cpp
@@ -0,0 +1,172 @@
+/*********************                                                        */
+/*! \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 equality proof checker
+ **/
+
+#include "theory/uf/proof_checker.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+void UfProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  // add checkers
+  pc->registerChecker(PfRule::REFL, this);
+  pc->registerChecker(PfRule::SYMM, this);
+  pc->registerChecker(PfRule::TRANS, this);
+  pc->registerChecker(PfRule::CONG, this);
+  pc->registerChecker(PfRule::TRUE_INTRO, this);
+  pc->registerChecker(PfRule::TRUE_ELIM, this);
+  pc->registerChecker(PfRule::FALSE_INTRO, this);
+  pc->registerChecker(PfRule::FALSE_ELIM, this);
+}
+
+Node UfProofRuleChecker::checkInternal(PfRule id,
+                                       const std::vector<Node>& children,
+                                       const std::vector<Node>& args)
+{
+  // compute what was proven
+  if (id == PfRule::REFL)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    return args[0].eqNode(args[0]);
+  }
+  else if (id == PfRule::SYMM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    bool polarity = children[0].getKind() != NOT;
+    Node eqp = polarity ? children[0] : children[0][0];
+    if (eqp.getKind() != EQUAL)
+    {
+      // not a (dis)equality
+      return Node::null();
+    }
+    Node conc = eqp[1].eqNode(eqp[0]);
+    return polarity ? conc : conc.notNode();
+  }
+  else if (id == PfRule::TRANS)
+  {
+    Assert(children.size() > 0);
+    Assert(args.empty());
+    Node first;
+    Node curr;
+    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
+    {
+      Node eqp = children[i];
+      if (eqp.getKind() != EQUAL)
+      {
+        return Node::null();
+      }
+      if (first.isNull())
+      {
+        first = eqp[0];
+      }
+      else if (eqp[0] != curr)
+      {
+        return Node::null();
+      }
+      curr = eqp[1];
+    }
+    return first.eqNode(curr);
+  }
+  else if (id == PfRule::CONG)
+  {
+    Assert(children.size() > 0);
+    Assert(args.size() == 1);
+    // We do congruence over builtin kinds using operatorToKind
+    std::vector<Node> lchildren;
+    std::vector<Node> rchildren;
+    // get the expected kind for args[0]
+    Kind k = NodeManager::getKindForFunction(args[0]);
+    if (k == kind::UNDEFINED_KIND)
+    {
+      k = NodeManager::operatorToKind(args[0]);
+    }
+    if (k == kind::UNDEFINED_KIND)
+    {
+      return Node::null();
+    }
+    Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k
+                        << ", metakind=" << kind::metaKindOf(k) << std::endl;
+    if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+    {
+      // parameterized kinds require the operator
+      lchildren.push_back(args[0]);
+      rchildren.push_back(args[0]);
+    }
+    for (size_t i = 0, nchild = children.size(); i < nchild; i++)
+    {
+      Node eqp = children[i];
+      if (eqp.getKind() != EQUAL)
+      {
+        return Node::null();
+      }
+      lchildren.push_back(eqp[0]);
+      rchildren.push_back(eqp[1]);
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    Node l = nm->mkNode(k, lchildren);
+    Node r = nm->mkNode(k, rchildren);
+    return l.eqNode(r);
+  }
+  else if (id == PfRule::TRUE_INTRO)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    Node trueNode = NodeManager::currentNM()->mkConst(true);
+    return children[0].eqNode(trueNode);
+  }
+  else if (id == PfRule::TRUE_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
+        || !children[0][1].getConst<bool>())
+    {
+      return Node::null();
+    }
+    return children[0][0];
+  }
+  else if (id == PfRule::FALSE_INTRO)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != kind::NOT)
+    {
+      return Node::null();
+    }
+    Node falseNode = NodeManager::currentNM()->mkConst(false);
+    return children[0][0].eqNode(falseNode);
+  }
+  else if (id == PfRule::FALSE_ELIM)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != EQUAL || !children[0][1].isConst()
+        || children[0][1].getConst<bool>())
+    {
+      return Node::null();
+    }
+    return children[0][0].notNode();
+  }
+  // no rule
+  return Node::null();
+}
+
+}  // namespace uf
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h
new file mode 100644
index 000000000..92d853f3a
--- /dev/null
+++ b/src/theory/uf/proof_checker.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \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 Equality proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__UF__PROOF_CHECKER_H
+#define CVC4__THEORY__UF__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+/** A checker for builtin proofs */
+class UfProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  UfProofRuleChecker() {}
+  ~UfProofRuleChecker() {}
+
+  /** 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 uf
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index 27d045120..513c58783 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -2,9 +2,9 @@
 /*! \file symmetry_breaker.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Liana Hadarean, Tim King
+ **   Morgan Deters, Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index d528e948f..c7fc51465 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1098d42ce..8334f29d1 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 8627eb3f0..a3e908b1f 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -2,9 +2,9 @@
 /*! \file theory_uf.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
+ **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index d667aea7e..56d44b769 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -2,9 +2,9 @@
 /*! \file theory_uf_model.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Clark Barrett
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 4454b7e8c..138ad1238 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -2,9 +2,9 @@
 /*! \file theory_uf_model.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 1cc8ab876..e651edb51 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index f782cd618..372ca9ad0 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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