1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Yoni Zohar |
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 |
|
* Utilities for LFSC proofs. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/lfsc/lfsc_util.h" |
17 |
|
|
18 |
|
#include "proof/proof_checker.h" |
19 |
|
#include "util/rational.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
namespace proof { |
23 |
|
|
24 |
|
const char* toString(LfscRule id) |
25 |
|
{ |
26 |
|
switch (id) |
27 |
|
{ |
28 |
|
case LfscRule::SCOPE: return "scope"; |
29 |
|
case LfscRule::NEG_SYMM: return "neg_symm"; |
30 |
|
case LfscRule::CONG: return "cong"; |
31 |
|
case LfscRule::AND_INTRO1: return "and_intro1"; |
32 |
|
case LfscRule::AND_INTRO2: return "and_intro2"; |
33 |
|
case LfscRule::NOT_AND_REV: return "not_and_rev"; |
34 |
|
case LfscRule::PROCESS_SCOPE: return "process_scope"; |
35 |
|
case LfscRule::ARITH_SUM_UB: return "arith_sum_ub"; |
36 |
|
case LfscRule::INSTANTIATE: return "instantiate"; |
37 |
|
case LfscRule::SKOLEMIZE: return "skolemize"; |
38 |
|
case LfscRule::LAMBDA: return "\\"; |
39 |
|
case LfscRule::PLET: return "plet"; |
40 |
|
default: return "?"; |
41 |
|
} |
42 |
|
} |
43 |
|
std::ostream& operator<<(std::ostream& out, LfscRule id) |
44 |
|
{ |
45 |
|
out << toString(id); |
46 |
|
return out; |
47 |
|
} |
48 |
|
|
49 |
|
bool getLfscRule(Node n, LfscRule& lr) |
50 |
|
{ |
51 |
|
uint32_t id; |
52 |
|
if (ProofRuleChecker::getUInt32(n, id)) |
53 |
|
{ |
54 |
|
lr = static_cast<LfscRule>(id); |
55 |
|
return true; |
56 |
|
} |
57 |
|
return false; |
58 |
|
} |
59 |
|
|
60 |
|
LfscRule getLfscRule(Node n) |
61 |
|
{ |
62 |
|
LfscRule lr = LfscRule::UNKNOWN; |
63 |
|
getLfscRule(n, lr); |
64 |
|
return lr; |
65 |
|
} |
66 |
|
|
67 |
|
Node mkLfscRuleNode(LfscRule r) |
68 |
|
{ |
69 |
|
return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(r))); |
70 |
|
} |
71 |
|
|
72 |
|
bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) |
73 |
|
{ |
74 |
|
if (pn->getRule() == PfRule::SCOPE) |
75 |
|
{ |
76 |
|
return false; |
77 |
|
} |
78 |
|
if (pn->getRule() != PfRule::LFSC_RULE) |
79 |
|
{ |
80 |
|
return true; |
81 |
|
} |
82 |
|
// do not traverse under LFSC (lambda) scope |
83 |
|
LfscRule lr = getLfscRule(pn->getArguments()[0]); |
84 |
|
return lr != LfscRule::LAMBDA; |
85 |
|
} |
86 |
|
|
87 |
|
} // namespace proof |
88 |
29577 |
} // namespace cvc5 |