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 |
|
* Implementation of method identifier |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/method_id.h" |
17 |
|
|
18 |
|
#include "proof/proof_checker.h" |
19 |
|
#include "util/rational.h" |
20 |
|
|
21 |
|
namespace cvc5 { |
22 |
|
|
23 |
10 |
const char* toString(MethodId id) |
24 |
|
{ |
25 |
10 |
switch (id) |
26 |
|
{ |
27 |
|
case MethodId::RW_REWRITE: return "RW_REWRITE"; |
28 |
|
case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE"; |
29 |
|
case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT"; |
30 |
|
case MethodId::RW_EVALUATE: return "RW_EVALUATE"; |
31 |
|
case MethodId::RW_IDENTITY: return "RW_IDENTITY"; |
32 |
5 |
case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE"; |
33 |
5 |
case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST"; |
34 |
|
case MethodId::SB_DEFAULT: return "SB_DEFAULT"; |
35 |
|
case MethodId::SB_LITERAL: return "SB_LITERAL"; |
36 |
|
case MethodId::SB_FORMULA: return "SB_FORMULA"; |
37 |
|
case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL"; |
38 |
|
case MethodId::SBA_SIMUL: return "SBA_SIMUL"; |
39 |
|
case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT"; |
40 |
|
default: return "MethodId::Unknown"; |
41 |
|
}; |
42 |
|
} |
43 |
|
|
44 |
10 |
std::ostream& operator<<(std::ostream& out, MethodId id) |
45 |
|
{ |
46 |
10 |
out << toString(id); |
47 |
10 |
return out; |
48 |
|
} |
49 |
|
|
50 |
647 |
Node mkMethodId(MethodId id) |
51 |
|
{ |
52 |
647 |
return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id))); |
53 |
|
} |
54 |
|
|
55 |
704 |
bool getMethodId(TNode n, MethodId& i) |
56 |
|
{ |
57 |
|
uint32_t index; |
58 |
704 |
if (!ProofRuleChecker::getUInt32(n, index)) |
59 |
|
{ |
60 |
|
return false; |
61 |
|
} |
62 |
704 |
i = static_cast<MethodId>(index); |
63 |
704 |
return true; |
64 |
|
} |
65 |
|
|
66 |
81809 |
bool getMethodIds(const std::vector<Node>& args, |
67 |
|
MethodId& ids, |
68 |
|
MethodId& ida, |
69 |
|
MethodId& idr, |
70 |
|
size_t index) |
71 |
|
{ |
72 |
81809 |
ids = MethodId::SB_DEFAULT; |
73 |
81809 |
ida = MethodId::SBA_SEQUENTIAL; |
74 |
81809 |
idr = MethodId::RW_REWRITE; |
75 |
82401 |
for (size_t offset = 0; offset <= 2; offset++) |
76 |
|
{ |
77 |
82401 |
if (args.size() > index + offset) |
78 |
|
{ |
79 |
592 |
MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr); |
80 |
592 |
if (!getMethodId(args[index + offset], id)) |
81 |
|
{ |
82 |
|
Trace("builtin-pfcheck") |
83 |
|
<< "Failed to get id from " << args[index + offset] << std::endl; |
84 |
|
return false; |
85 |
|
} |
86 |
|
} |
87 |
|
else |
88 |
|
{ |
89 |
81809 |
break; |
90 |
|
} |
91 |
|
} |
92 |
163618 |
Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / " |
93 |
81809 |
<< ida << " / " << idr << "\n"; |
94 |
81809 |
return true; |
95 |
|
} |
96 |
|
|
97 |
234 |
void addMethodIds(std::vector<Node>& args, |
98 |
|
MethodId ids, |
99 |
|
MethodId ida, |
100 |
|
MethodId idr) |
101 |
|
{ |
102 |
234 |
bool ndefRewriter = (idr != MethodId::RW_REWRITE); |
103 |
234 |
bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL); |
104 |
234 |
if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply) |
105 |
|
{ |
106 |
108 |
args.push_back(mkMethodId(ids)); |
107 |
|
} |
108 |
234 |
if (ndefApply || ndefRewriter) |
109 |
|
{ |
110 |
108 |
args.push_back(mkMethodId(ida)); |
111 |
|
} |
112 |
234 |
if (ndefRewriter) |
113 |
|
{ |
114 |
|
args.push_back(mkMethodId(idr)); |
115 |
|
} |
116 |
234 |
} |
117 |
|
|
118 |
22746 |
} // namespace cvc5 |