From 4f367612a386d21315cee7d377176bc83a1402c5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Nov 2020 10:33:32 -0600
Subject: (proof-new) Proofs for skolemization (#5339)

This adds support for proofs in the quantifiers module that performs skolemization.

Also fixes a bug in the proof checker for skolemization.
---
 src/theory/quantifiers/skolemize.h | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'src/theory/quantifiers/skolemize.h')

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 6db3f6215..4469fe851 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 
@@ -63,15 +64,16 @@ class Skolemize
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersEngine* qe, context::UserContext* u);
+  Skolemize(QuantifiersEngine* qe,
+            context::UserContext* u,
+            ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
-   * If the return value ret of this function
-   * is non-null, then ret is a new skolemization lemma
-   * we generated for q. These lemmas are constructed
-   * once per user-context.
+   * If the return value ret of this function is non-null, then ret is a trust
+   * node corresponding to a new skolemization lemma we generated for q. These
+   * lemmas are constructed once per user-context.
    */
-  Node process(Node q);
+  TrustNode process(Node q);
   /** get skolem constants for quantified formula q */
   bool getSkolemConstants(Node q, std::vector<Node>& skolems);
   /** get the i^th skolem constant for quantified formula q */
@@ -119,6 +121,8 @@ class Skolemize
   bool printSkolemization(std::ostream& out);
 
  private:
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
   /** get self selectors
    * For datatype constructor dtc with type dt,
    * this collects the set of datatype selector applications,
@@ -139,6 +143,10 @@ class Skolemize
       d_skolem_constants;
   /** map from quantified formulas to their skolemized body */
   std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
+  /** Eager proof generator for skolemization lemmas */
+  std::unique_ptr<EagerProofGenerator> d_epg;
 };
 
 } /* CVC4::theory::quantifiers namespace */
-- 
cgit v1.2.3