1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * The skolem lemma utility.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__SKOLEM_LEMMA_H
19 #define CVC5__THEORY__SKOLEM_LEMMA_H
21 #include "expr/node.h"
22 #include "proof/trust_node.h"
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
31 * (ite C (= k A) (= k B))
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.
41 * Make skolem from trust node lem of kind LEMMA and skolem k.
43 SkolemLemma(TrustNode lem
, Node k
);
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).
48 SkolemLemma(Node k
, ProofGenerator
* pg
);
50 /** The lemma, a trust node of kind LEMMA */
52 /** The skolem associated with that lemma */
55 /** Get proven from the lemma */
56 Node
getProven() const;
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).
61 static Node
getSkolemLemmaFor(Node k
);
67 #endif /* CVC5__THEORY__SKOLEM_LEMMA_H */