(proof-new) Add quantifiers proof checker (#4593)

Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.

This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.

2 files changed, 158 insertions, 0 deletions

diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
new file mode 100644
index 000000000..a86fc90f8
--- /dev/null
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -0,0 +1,109 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** 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
+ ** 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 quantifiers proof checker
+ **/
+
+#include "theory/quantifiers/proof_checker.h"
+
+#include "expr/skolem_manager.h"
+#include "theory/builtin/proof_checker.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  // add checkers
+  pc->registerChecker(PfRule::WITNESS_INTRO, this);
+  pc->registerChecker(PfRule::EXISTS_INTRO, this);
+  pc->registerChecker(PfRule::SKOLEMIZE, this);
+  pc->registerChecker(PfRule::INSTANTIATE, this);
+}
+
+Node QuantifiersProofRuleChecker::checkInternal(
+    PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  // compute what was proven
+  if (id == PfRule::WITNESS_INTRO || id == PfRule::EXISTS_INTRO)
+  {
+    Assert(children.size() == 1);
+    Assert(args.size() == 1);
+    SkolemManager* sm = nm->getSkolemManager();
+    Node p = children[0];
+    Node t = args[0];
+    Node exists = sm->mkExistential(t, p);
+    if (id == PfRule::EXISTS_INTRO)
+    {
+      return exists;
+    }
+    std::vector<Node> skolems;
+    sm->mkSkolemize(exists, skolems, "k");
+    Assert(skolems.size() == 1);
+    return skolems[0];
+  }
+  else if (id == PfRule::SKOLEMIZE)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    // can use either negated FORALL or EXISTS
+    if (children[0].getKind() != EXISTS
+        && (children[0].getKind() != NOT || children[0][0].getKind() != FORALL))
+    {
+      return Node::null();
+    }
+    SkolemManager* sm = nm->getSkolemManager();
+    Node exists;
+    if (children[0].getKind() == EXISTS)
+    {
+      exists = children[0];
+    }
+    else
+    {
+      std::vector<Node> echildren(children[0][0].begin(), children[0][0].end());
+      exists = nm->mkNode(EXISTS, echildren);
+    }
+    std::vector<Node> skolems;
+    Node res = sm->mkSkolemize(exists, skolems, "k");
+    return res;
+  }
+  else if (id == PfRule::INSTANTIATE)
+  {
+    Assert(children.size() == 1);
+    if (children[0].getKind() != FORALL
+        || args.size() != children[0][0].getNumChildren())
+    {
+      return Node::null();
+    }
+    Node body = children[0][1];
+    std::vector<Node> vars;
+    std::vector<Node> subs;
+    for (unsigned i = 0, nargs = args.size(); i < nargs; i++)
+    {
+      vars.push_back(children[0][0][i]);
+      subs.push_back(args[i]);
+    }
+    Node inst =
+        body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+    return inst;
+  }
+
+  // no rule
+  return Node::null();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h
new file mode 100644
index 000000000..fd55dbf31
--- /dev/null
+++ b/src/theory/quantifiers/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-2019 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 Quantifiers proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+#define CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** A checker for quantifiers proofs */
+class QuantifiersProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  QuantifiersProofRuleChecker() {}
+  ~QuantifiersProofRuleChecker() {}
+
+  /** 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 quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */