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 "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__PROOF__LFSC__LFSC_UTIL_H |
19 |
|
#define CVC5__PROOF__LFSC__LFSC_UTIL_H |
20 |
|
|
21 |
|
#include <iostream> |
22 |
|
#include <map> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
#include "proof/proof_letify.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace proof { |
29 |
|
|
30 |
|
/** |
31 |
|
* LFSC rules. The enum below contains all rules that don't correspond to a |
32 |
|
* PfRule, e.g. congruence in LFSC does not have the same form as congruence |
33 |
|
* in the internal calculus. |
34 |
|
*/ |
35 |
|
enum class LfscRule : uint32_t |
36 |
|
{ |
37 |
|
//----------- translated rules |
38 |
|
|
39 |
|
// We defined LFSC versions for rules that either don't exist in the internal |
40 |
|
// calculus, or have a different set of arugments/children. |
41 |
|
|
42 |
|
// scope has a different structure, e.g. uses lambdas |
43 |
|
SCOPE, |
44 |
|
// must distinguish equalities and disequalities |
45 |
|
NEG_SYMM, |
46 |
|
// congruence is done via a higher-order variant of congruence |
47 |
|
CONG, |
48 |
|
// we use unrolled binary versions of and intro |
49 |
|
AND_INTRO1, |
50 |
|
AND_INTRO2, |
51 |
|
// needed as a helper for SCOPE |
52 |
|
NOT_AND_REV, |
53 |
|
PROCESS_SCOPE, |
54 |
|
// arithmetic |
55 |
|
ARITH_SUM_UB, |
56 |
|
|
57 |
|
// form of quantifier rules varies from internal calculus |
58 |
|
INSTANTIATE, |
59 |
|
SKOLEMIZE, |
60 |
|
|
61 |
|
// a lambda with argument |
62 |
|
LAMBDA, |
63 |
|
// a proof-let "plet" |
64 |
|
PLET, |
65 |
|
//----------- unknown |
66 |
|
UNKNOWN, |
67 |
|
}; |
68 |
|
|
69 |
|
/** |
70 |
|
* Converts a lfsc rule to a string. Note: This function is also used in |
71 |
|
* `safe_print()`. Changing this function name or signature will result in |
72 |
|
* `safe_print()` printing "<unsupported>" instead of the proper strings for |
73 |
|
* the enum values. |
74 |
|
* |
75 |
|
* @param id The lfsc rule |
76 |
|
* @return The name of the lfsc rule |
77 |
|
*/ |
78 |
|
const char* toString(LfscRule id); |
79 |
|
|
80 |
|
/** |
81 |
|
* Writes a lfsc rule name to a stream. |
82 |
|
* |
83 |
|
* @param out The stream to write to |
84 |
|
* @param id The lfsc rule to write to the stream |
85 |
|
* @return The stream |
86 |
|
*/ |
87 |
|
std::ostream& operator<<(std::ostream& out, LfscRule id); |
88 |
|
/** Get LFSC rule from a node */ |
89 |
|
LfscRule getLfscRule(Node n); |
90 |
|
/** Get LFSC rule from a node, return true if success and store in lr */ |
91 |
|
bool getLfscRule(Node n, LfscRule& lr); |
92 |
|
/** Make node for LFSC rule */ |
93 |
|
Node mkLfscRuleNode(LfscRule r); |
94 |
|
|
95 |
|
/** Helper class used for letifying LFSC proofs. */ |
96 |
|
class LfscProofLetifyTraverseCallback : public ProofLetifyTraverseCallback |
97 |
|
{ |
98 |
|
public: |
99 |
|
bool shouldTraverse(const ProofNode* pn) override; |
100 |
|
}; |
101 |
|
|
102 |
|
} // namespace proof |
103 |
|
} // namespace cvc5 |
104 |
|
|
105 |
|
#endif |