src/theory/skolem_lemma.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The skolem lemma utility.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__SKOLEM_LEMMA_H
  19 #define CVC5__THEORY__SKOLEM_LEMMA_H
  20
  21 #include "expr/node.h"
  22 #include "proof/trust_node.h"
  23
  24 namespace cvc5 {
  25 namespace theory {
  26
  27 /**
  28  * A skolem lemma is a pair containing a trust node repreresenting a lemma
  29  * and the skolem it is for. A common example would be the trust node proving
  30  * the lemma:
  31  *    (ite C (= k A) (= k B))
  32  * and the skolem k.
  33  *
  34  * Skolem lemmas can be used as a way of tracking the relevance of a lemma.
  35  * They can be used for things like term formula removal and preprocessing.
  36  */
  37 class SkolemLemma
  38 {
  39  public:
  40   /**
  41    * Make skolem from trust node lem of kind LEMMA and skolem k.
  42    */
  43   SkolemLemma(TrustNode lem, Node k);
  44   /**
  45    * Make skolem lemma from witness form of skolem k. If non-null, pg is
  46    * proof generator that can generator a proof for getSkolemLemmaFor(k).
  47    */
  48   SkolemLemma(Node k, ProofGenerator* pg);
  49
  50   /** The lemma, a trust node of kind LEMMA */
  51   TrustNode d_lemma;
  52   /** The skolem associated with that lemma */
  53   Node d_skolem;
  54
  55   /** Get proven from the lemma */
  56   Node getProven() const;
  57   /**
  58    * Get the lemma for skolem k based on its witness form. If k has witness
  59    * form (witness ((x T)) (P x)), this is the formula (P k).
  60    */
  61   static Node getSkolemLemmaFor(Node k);
  62 };
  63
  64 }  // namespace theory
  65 }  // namespace cvc5
  66
  67 #endif /* CVC5__THEORY__SKOLEM_LEMMA_H */