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 "theory/skolem_lemma.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
|
23 |
|
SkolemLemma::SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k) |
24 |
|
{ |
25 |
|
Assert(lem.getKind() == TrustNodeKind::LEMMA); |
26 |
|
} |
27 |
|
|
28 |
980 |
SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k) |
29 |
|
{ |
30 |
1960 |
Node lem = getSkolemLemmaFor(k); |
31 |
980 |
d_lemma = TrustNode::mkTrustLemma(lem, pg); |
32 |
980 |
} |
33 |
|
|
34 |
980 |
Node SkolemLemma::getSkolemLemmaFor(Node k) |
35 |
|
{ |
36 |
1960 |
Node w = SkolemManager::getWitnessForm(k); |
37 |
980 |
Assert(w.getKind() == kind::WITNESS); |
38 |
1960 |
TNode tx = w[0][0]; |
39 |
1960 |
TNode tk = k; |
40 |
1960 |
return w[1].substitute(tx, tk); |
41 |
|
} |
42 |
|
|
43 |
|
} // namespace theory |
44 |
22746 |
} // namespace cvc5 |