(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.

5 files changed, 341 insertions, 143 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a5160d2fe..c50578c46 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -534,6 +534,8 @@ libcvc4_add_sources(
   theory/quantifiers/instantiate.h
   theory/quantifiers/lazy_trie.cpp
   theory/quantifiers/lazy_trie.h
+  theory/quantifiers/proof_checker.cpp
+  theory/quantifiers/proof_checker.h
   theory/quantifiers/quant_conflict_find.cpp
   theory/quantifiers/quant_conflict_find.h
   theory/quantifiers/quant_epr.cpp
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 595e1d5f7..339b4f582 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -31,15 +31,6 @@ const char* toString(PfRule id)
     case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
     case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
     case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
-    //================================================= Equality rules
-    case PfRule::REFL: return "REFL";
-    case PfRule::SYMM: return "SYMM";
-    case PfRule::TRANS: return "TRANS";
-    case PfRule::CONG: return "CONG";
-    case PfRule::TRUE_INTRO: return "TRUE_INTRO";
-    case PfRule::TRUE_ELIM: return "TRUE_ELIM";
-    case PfRule::FALSE_INTRO: return "FALSE_INTRO";
-    case PfRule::FALSE_ELIM: return "FALSE_ELIM";
     //================================================= Boolean rules
     case PfRule::SPLIT: return "SPLIT";
     case PfRule::AND_ELIM: return "AND_ELIM";
@@ -85,6 +76,20 @@ const char* toString(PfRule id)
     case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1";
     case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2";
     case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3";
+    //================================================= Equality rules
+    case PfRule::REFL: return "REFL";
+    case PfRule::SYMM: return "SYMM";
+    case PfRule::TRANS: return "TRANS";
+    case PfRule::CONG: return "CONG";
+    case PfRule::TRUE_INTRO: return "TRUE_INTRO";
+    case PfRule::TRUE_ELIM: return "TRUE_ELIM";
+    case PfRule::FALSE_INTRO: return "FALSE_INTRO";
+    case PfRule::FALSE_ELIM: return "FALSE_ELIM";
+    //================================================= Quantifiers rules
+    case PfRule::WITNESS_INTRO: return "WITNESS_INTRO";
+    case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
+    case PfRule::SKOLEMIZE: return "SKOLEMIZE";
+    case PfRule::INSTANTIATE: return "INSTANTIATE";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 6acccfffd..daded84d4 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -71,55 +71,102 @@ enum class PfRule : uint32_t
   // has the conclusion (=> F F) and has no free assumptions. More generally, a
   // proof with no free assumptions always concludes a valid formula.
   SCOPE,
-  //================================================= Equality rules
-  // ======== Reflexive
+
+  //======================== Builtin theory (common node operations)
+  // ======== Substitution
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (t, (ids)?)
+  // ---------------------------------------------------------------
+  // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  // where sigma{ids}(Fi) are substitutions, which notice are applied in
+  // reverse order.
+  // Notice that ids is a MethodId identifier, which determines how to convert
+  // the formulas F1, ..., Fn into substitutions.
+  SUBS,
+  // ======== Rewrite
   // Children: none
-  // Arguments: (t)
-  // ---------------------
-  // Conclusion: (= t t)
-  REFL,
-  // ======== Symmetric
-  // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
-  // Arguments: none
-  // -----------------------
-  // Conclusion: (= t2 t1) or (not (= t2 t1))
-  SYMM,
-  // ======== Transitivity
-  // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
-  // Arguments: none
-  // -----------------------
-  // Conclusion: (= t1 tn)
-  TRANS,
-  // ======== Congruence  (subsumed by Substitute?)
-  // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
-  // Arguments: (f)
-  // ---------------------------------------------
-  // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
-  CONG,
-  // ======== True intro
-  // Children: (P:F)
-  // Arguments: none
-  // ----------------------------------------
-  // Conclusion: (= F true)
-  TRUE_INTRO,
-  // ======== True elim
-  // Children: (P:(= F true)
-  // Arguments: none
+  // Arguments: (t, (idr)?)
   // ----------------------------------------
+  // Conclusion: (= t Rewriter{idr}(t))
+  // where idr is a MethodId identifier, which determines the kind of rewriter
+  // to apply, e.g. Rewriter::rewrite.
+  REWRITE,
+  // ======== Substitution + Rewriting equality introduction
+  //
+  // In this rule, we provide a term t and conclude that it is equal to its
+  // rewritten form under a (proven) substitution.
+  //
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (t, (ids (idr)?)?)
+  // ---------------------------------------------------------------
+  // Conclusion: (= t t')
+  // where
+  //   t' is
+  //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
+  //   toSkolem(...) converts terms from witness form to Skolem form,
+  //   toWitness(...) converts terms from Skolem form to witness form.
+  //
+  // Notice that:
+  //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  // In other words, from the point of view of Skolem forms, this rule
+  // transforms t to t' by standard substitution + rewriting.
+  //
+  // The argument ids and idr is optional and specify the identifier of the
+  // substitution and rewriter respectively to be used. For details, see
+  // theory/builtin/proof_checker.h.
+  MACRO_SR_EQ_INTRO,
+  // ======== Substitution + Rewriting predicate introduction
+  //
+  // In this rule, we provide a formula F and conclude it, under the condition
+  // that it rewrites to true under a proven substitution.
+  //
+  // Children: (P1:F1, ..., Pn:Fn)
+  // Arguments: (F, (ids (idr)?)?)
+  // ---------------------------------------------------------------
   // Conclusion: F
-  TRUE_ELIM,
-  // ======== False intro
-  // Children: (P:(not F))
-  // Arguments: none
+  // where
+  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
+  // where ids and idr are method identifiers.
+  //
+  // Notice that we apply rewriting on the witness form of F, meaning that this
+  // rule may conclude an F whose Skolem form is justified by the definition of
+  // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
+  // substitution is applied only within the side condition, meaning the
+  // rewritten form of the witness form of F does not escape this rule.
+  MACRO_SR_PRED_INTRO,
+  // ======== Substitution + Rewriting predicate elimination
+  //
+  // In this rule, if we have proven a formula F, then we may conclude its
+  // rewritten form under a proven substitution.
+  //
+  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
+  // Arguments: ((ids (idr)?)?)
   // ----------------------------------------
-  // Conclusion: (= F false)
-  FALSE_INTRO,
-  // ======== False elim
-  // Children: (P:(= F false)
-  // Arguments: none
+  // Conclusion: F'
+  // where
+  //   F' is
+  //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
+  // where ids and idr are method identifiers.
+  //
+  // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
+  MACRO_SR_PRED_ELIM,
+  // ======== Substitution + Rewriting predicate transform
+  //
+  // In this rule, if we have proven a formula F, then we may provide a formula
+  // G and conclude it if F and G are equivalent after rewriting under a proven
+  // substitution.
+  //
+  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
+  // Arguments: (G, (ids (idr)?)?)
   // ----------------------------------------
-  // Conclusion: (not F)
-  FALSE_ELIM,
+  // Conclusion: G
+  // where
+  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
+  //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  //
+  // Notice that we apply rewriting on the witness form of F and G, similar to
+  // MACRO_SR_PRED_INTRO.
+  MACRO_SR_PRED_TRANSFORM,
 
   //================================================= Boolean rules
   // ======== Split
@@ -378,101 +425,87 @@ enum class PfRule : uint32_t
   // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
   CNF_ITE_NEG3,
 
-  //======================== Builtin theory (common node operations)
-  // ======== Substitution
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (t, (ids)?)
-  // ---------------------------------------------------------------
-  // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
-  // where sigma{ids}(Fi) are substitutions, which notice are applied in
-  // reverse order.
-  // Notice that ids is a MethodId identifier, which determines how to convert
-  // the formulas F1, ..., Fn into substitutions.
-  SUBS,
-  // ======== Rewrite
+  //================================================= Equality rules
+  // ======== Reflexive
   // Children: none
-  // Arguments: (t, (idr)?)
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= t t)
+  REFL,
+  // ======== Symmetric
+  // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
+  // Arguments: none
+  // -----------------------
+  // Conclusion: (= t2 t1) or (not (= t2 t1))
+  SYMM,
+  // ======== Transitivity
+  // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
+  // Arguments: none
+  // -----------------------
+  // Conclusion: (= t1 tn)
+  TRANS,
+  // ======== Congruence  (subsumed by Substitute?)
+  // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
+  // Arguments: (f)
+  // ---------------------------------------------
+  // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
+  CONG,
+  // ======== True intro
+  // Children: (P:F)
+  // Arguments: none
+  // ----------------------------------------
+  // Conclusion: (= F true)
+  TRUE_INTRO,
+  // ======== True elim
+  // Children: (P:(= F true)
+  // Arguments: none
   // ----------------------------------------
-  // Conclusion: (= t Rewriter{idr}(t))
-  // where idr is a MethodId identifier, which determines the kind of rewriter
-  // to apply, e.g. Rewriter::rewrite.
-  REWRITE,
-  // ======== Substitution + Rewriting equality introduction
-  //
-  // In this rule, we provide a term t and conclude that it is equal to its
-  // rewritten form under a (proven) substitution.
-  //
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (t, (ids (idr)?)?)
-  // ---------------------------------------------------------------
-  // Conclusion: (= t t')
-  // where
-  //   t' is
-  //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
-  //   toSkolem(...) converts terms from witness form to Skolem form,
-  //   toWitness(...) converts terms from Skolem form to witness form.
-  //
-  // Notice that:
-  //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
-  // In other words, from the point of view of Skolem forms, this rule
-  // transforms t to t' by standard substitution + rewriting.
-  //
-  // The argument ids and idr is optional and specify the identifier of the
-  // substitution and rewriter respectively to be used. For details, see
-  // theory/builtin/proof_checker.h.
-  MACRO_SR_EQ_INTRO,
-  // ======== Substitution + Rewriting predicate introduction
-  //
-  // In this rule, we provide a formula F and conclude it, under the condition
-  // that it rewrites to true under a proven substitution.
-  //
-  // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (F, (ids (idr)?)?)
-  // ---------------------------------------------------------------
   // Conclusion: F
-  // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
-  // where ids and idr are method identifiers.
-  //
-  // Notice that we apply rewriting on the witness form of F, meaning that this
-  // rule may conclude an F whose Skolem form is justified by the definition of
-  // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
-  // substitution is applied only within the side condition, meaning the
-  // rewritten form of the witness form of F does not escape this rule.
-  MACRO_SR_PRED_INTRO,
-  // ======== Substitution + Rewriting predicate elimination
-  //
-  // In this rule, if we have proven a formula F, then we may conclude its
-  // rewritten form under a proven substitution.
-  //
-  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: ((ids (idr)?)?)
+  TRUE_ELIM,
+  // ======== False intro
+  // Children: (P:(not F))
+  // Arguments: none
   // ----------------------------------------
-  // Conclusion: F'
-  // where
-  //   F' is
-  //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
-  // where ids and idr are method identifiers.
-  //
-  // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
-  MACRO_SR_PRED_ELIM,
-  // ======== Substitution + Rewriting predicate transform
-  //
-  // In this rule, if we have proven a formula F, then we may provide a formula
-  // G and conclude it if F and G are equivalent after rewriting under a proven
-  // substitution.
-  //
-  // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: (G, (ids (idr)?)?)
+  // Conclusion: (= F false)
+  FALSE_INTRO,
+  // ======== False elim
+  // Children: (P:(= F false)
+  // Arguments: none
   // ----------------------------------------
-  // Conclusion: G
-  // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
-  //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
-  //
-  // Notice that we apply rewriting on the witness form of F and G, similar to
-  // MACRO_SR_PRED_INTRO.
-  MACRO_SR_PRED_TRANSFORM,
+  // Conclusion: (not F)
+  FALSE_ELIM,
+
+  //================================================= Quantifiers rules
+  // ======== Witness intro
+  // Children: (P:F[t])
+  // Arguments: (t)
+  // ----------------------------------------
+  // Conclusion: (= t (witness ((x T)) F[x]))
+  // where x is a BOUND_VARIABLE unique to the pair F,t.
+  WITNESS_INTRO,
+  // ======== Exists intro
+  // Children: (P:F[t])
+  // Arguments: (t)
+  // ----------------------------------------
+  // Conclusion: (exists ((x T)) F[x])
+  // where x is a BOUND_VARIABLE unique to the pair F,t.
+  EXISTS_INTRO,
+  // ======== Skolemize
+  // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
+  // Arguments: none
+  // ----------------------------------------
+  // Conclusion: F*sigma
+  // sigma maps x1 ... xn to their representative skolems obtained by
+  // SkolemManager::mkSkolemize, returned in the skolems argument of that
+  // method.
+  SKOLEMIZE,
+  // ======== Instantiate
+  // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
+  // Arguments: (t1 ... tn)
+  // ----------------------------------------
+  // Conclusion: F*sigma
+  // sigma maps x1 ... xn to t1 ... tn.
+  INSTANTIATE,
 
   //================================================= Unknown rule
   UNKNOWN,
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 */