1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Aina Niemetz |
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 inference to proof conversion for datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/infer_proof_cons.h" |
17 |
|
|
18 |
|
#include "proof/proof.h" |
19 |
|
#include "proof/proof_checker.h" |
20 |
|
#include "theory/builtin/proof_checker.h" |
21 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
22 |
|
#include "theory/model_manager.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
#include "util/rational.h" |
25 |
|
|
26 |
|
using namespace cvc5::kind; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace datatypes { |
31 |
|
|
32 |
2227 |
InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm) |
33 |
2227 |
: d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c) |
34 |
|
{ |
35 |
2227 |
Assert(d_pnm != nullptr); |
36 |
2227 |
} |
37 |
|
|
38 |
11881 |
void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di) |
39 |
|
{ |
40 |
23705 |
TNode fact = di->d_conc; |
41 |
11881 |
if (d_lazyFactMap.find(fact) != d_lazyFactMap.end()) |
42 |
|
{ |
43 |
54 |
return; |
44 |
|
} |
45 |
23651 |
Node symFact = CDProof::getSymmFact(fact); |
46 |
11827 |
if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end()) |
47 |
|
{ |
48 |
3 |
return; |
49 |
|
} |
50 |
11824 |
d_lazyFactMap.insert(fact, di); |
51 |
|
} |
52 |
|
|
53 |
6272 |
void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp) |
54 |
|
{ |
55 |
12544 |
Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp |
56 |
6272 |
<< std::endl; |
57 |
|
// split into vector |
58 |
12544 |
std::vector<Node> expv; |
59 |
6272 |
if (!exp.isNull() && !exp.isConst()) |
60 |
|
{ |
61 |
4938 |
if (exp.getKind() == AND) |
62 |
|
{ |
63 |
328 |
for (const Node& ec : exp) |
64 |
|
{ |
65 |
240 |
expv.push_back(ec); |
66 |
|
} |
67 |
|
} |
68 |
|
else |
69 |
|
{ |
70 |
4850 |
expv.push_back(exp); |
71 |
|
} |
72 |
|
} |
73 |
6272 |
NodeManager* nm = NodeManager::currentNM(); |
74 |
6272 |
bool success = false; |
75 |
6272 |
switch (infer) |
76 |
|
{ |
77 |
741 |
case InferenceId::DATATYPES_UNIF: |
78 |
|
{ |
79 |
741 |
Assert(expv.size() == 1); |
80 |
741 |
Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR |
81 |
|
&& exp[1].getKind() == APPLY_CONSTRUCTOR |
82 |
|
&& exp[0].getOperator() == exp[1].getOperator()); |
83 |
1482 |
Node narg; |
84 |
|
// we may be asked for a proof of (not P) coming from (= P false) or |
85 |
|
// (= false P), or similarly P from (= P true) or (= true P). |
86 |
741 |
bool concPol = conc.getKind() != NOT; |
87 |
1482 |
Node concAtom = concPol ? conc : conc[0]; |
88 |
1482 |
Node unifConc = conc; |
89 |
1246 |
for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++) |
90 |
|
{ |
91 |
1245 |
bool argSuccess = false; |
92 |
1245 |
if (conc.getKind() == EQUAL) |
93 |
|
{ |
94 |
1245 |
argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]); |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
|
for (size_t j = 0; j < 2; j++) |
99 |
|
{ |
100 |
|
if (exp[j][i] == concAtom && exp[1 - j][i].isConst() |
101 |
|
&& exp[1 - j][i].getConst<bool>() == concPol) |
102 |
|
{ |
103 |
|
argSuccess = true; |
104 |
|
unifConc = exp[0][i].eqNode(exp[1][i]); |
105 |
|
break; |
106 |
|
} |
107 |
|
} |
108 |
|
} |
109 |
1245 |
if (argSuccess) |
110 |
|
{ |
111 |
740 |
narg = nm->mkConst(Rational(i)); |
112 |
740 |
break; |
113 |
|
} |
114 |
|
} |
115 |
741 |
if (!narg.isNull()) |
116 |
|
{ |
117 |
740 |
if (conc.getKind() == EQUAL) |
118 |
|
{ |
119 |
|
// normal case where we conclude an equality |
120 |
740 |
cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg}); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
|
// must use true or false elim to prove the final |
125 |
|
cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg}); |
126 |
|
// may use symmetry |
127 |
|
Node eq = concAtom.eqNode(nm->mkConst(concPol)); |
128 |
|
cdp->addStep( |
129 |
|
conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {}); |
130 |
|
} |
131 |
740 |
success = true; |
132 |
741 |
} |
133 |
|
} |
134 |
741 |
break; |
135 |
2976 |
case InferenceId::DATATYPES_INST: |
136 |
|
{ |
137 |
2976 |
if (expv.size() == 1) |
138 |
|
{ |
139 |
2703 |
Assert(conc.getKind() == EQUAL); |
140 |
2703 |
int n = utils::isTester(exp); |
141 |
2703 |
if (n >= 0) |
142 |
|
{ |
143 |
5406 |
Node t = exp[0]; |
144 |
5406 |
Node nn = nm->mkConst(Rational(n)); |
145 |
5406 |
Node eq = exp.eqNode(conc); |
146 |
2703 |
cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn}); |
147 |
2703 |
cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {}); |
148 |
2703 |
success = true; |
149 |
|
} |
150 |
|
} |
151 |
|
} |
152 |
2976 |
break; |
153 |
1061 |
case InferenceId::DATATYPES_SPLIT: |
154 |
|
{ |
155 |
1061 |
Assert(expv.empty()); |
156 |
2122 |
Node t = conc.getKind() == OR ? conc[0][0] : conc[0]; |
157 |
1061 |
cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t}); |
158 |
2122 |
success = true; |
159 |
|
} |
160 |
1061 |
break; |
161 |
1182 |
case InferenceId::DATATYPES_COLLAPSE_SEL: |
162 |
|
{ |
163 |
1182 |
Assert(exp.getKind() == EQUAL); |
164 |
2364 |
Node concEq = conc; |
165 |
|
// might be a Boolean conclusion |
166 |
1182 |
if (conc.getKind() != EQUAL) |
167 |
|
{ |
168 |
|
bool concPol = conc.getKind() != NOT; |
169 |
|
Node concAtom = concPol ? conc : conc[0]; |
170 |
|
concEq = concAtom.eqNode(nm->mkConst(concPol)); |
171 |
|
} |
172 |
1182 |
Assert(concEq.getKind() == EQUAL |
173 |
|
&& concEq[0].getKind() == APPLY_SELECTOR_TOTAL); |
174 |
1182 |
Assert(exp[0].getType().isDatatype()); |
175 |
2364 |
Node sop = concEq[0].getOperator(); |
176 |
2364 |
Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]); |
177 |
2364 |
Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]); |
178 |
|
// exp[0] = exp[1] |
179 |
|
// --------------------- CONG ----------------- DT_COLLAPSE |
180 |
|
// s(exp[0]) = s(exp[1]) s(exp[1]) = r |
181 |
|
// --------------------------------------------------- TRANS |
182 |
|
// s(exp[0]) = r |
183 |
2364 |
Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL); |
184 |
2364 |
Node seq = sl.eqNode(sr); |
185 |
1182 |
cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop}); |
186 |
2364 |
Node sceq = sr.eqNode(concEq[1]); |
187 |
1182 |
cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr}); |
188 |
1182 |
cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {}); |
189 |
1182 |
if (conc.getKind() != EQUAL) |
190 |
|
{ |
191 |
|
PfRule eid = |
192 |
|
conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM; |
193 |
|
cdp->addStep(conc, eid, {concEq}, {}); |
194 |
|
} |
195 |
2364 |
success = true; |
196 |
|
} |
197 |
1182 |
break; |
198 |
104 |
case InferenceId::DATATYPES_CLASH_CONFLICT: |
199 |
|
{ |
200 |
104 |
cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {}); |
201 |
104 |
success = true; |
202 |
|
} |
203 |
104 |
break; |
204 |
65 |
case InferenceId::DATATYPES_TESTER_CONFLICT: |
205 |
|
{ |
206 |
|
// rewrites to false under substitution |
207 |
130 |
Node fn = nm->mkConst(false); |
208 |
65 |
cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {}); |
209 |
130 |
success = true; |
210 |
|
} |
211 |
65 |
break; |
212 |
|
case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT: |
213 |
|
{ |
214 |
|
Assert(expv.size() == 3); |
215 |
|
Node tester1 = expv[0]; |
216 |
|
Node tester1c = |
217 |
|
nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]); |
218 |
|
cdp->addStep(tester1c, |
219 |
|
PfRule::MACRO_SR_PRED_TRANSFORM, |
220 |
|
{expv[1], expv[2]}, |
221 |
|
{tester1c}); |
222 |
|
Node fn = nm->mkConst(false); |
223 |
|
cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {}); |
224 |
|
success = true; |
225 |
|
} |
226 |
|
break; |
227 |
|
case InferenceId::DATATYPES_PURIFY: |
228 |
|
{ |
229 |
|
cdp->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {}, {}); |
230 |
|
success = true; |
231 |
|
} |
232 |
|
break; |
233 |
|
// inferences currently not supported |
234 |
143 |
case InferenceId::DATATYPES_LABEL_EXH: |
235 |
|
case InferenceId::DATATYPES_BISIMILAR: |
236 |
|
case InferenceId::DATATYPES_CYCLE: |
237 |
|
default: |
238 |
286 |
Trace("dt-ipc") << "...no conversion for inference " << infer |
239 |
143 |
<< std::endl; |
240 |
143 |
break; |
241 |
|
} |
242 |
|
|
243 |
6272 |
if (!success) |
244 |
|
{ |
245 |
|
// failed to reconstruct, add trust |
246 |
417 |
Trace("dt-ipc") << "...failed " << infer << std::endl; |
247 |
834 |
Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES); |
248 |
417 |
cdp->addStep(conc, PfRule::THEORY_INFERENCE, expv, {conc, t}); |
249 |
|
} |
250 |
|
else |
251 |
|
{ |
252 |
5855 |
Trace("dt-ipc") << "...success" << std::endl; |
253 |
|
} |
254 |
6272 |
} |
255 |
|
|
256 |
6272 |
std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact) |
257 |
|
{ |
258 |
6272 |
Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl; |
259 |
|
// temporary proof |
260 |
12544 |
CDProof pf(d_pnm); |
261 |
|
// get the inference |
262 |
6272 |
NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact); |
263 |
6272 |
if (it == d_lazyFactMap.end()) |
264 |
|
{ |
265 |
|
Node factSym = CDProof::getSymmFact(fact); |
266 |
|
if (!factSym.isNull()) |
267 |
|
{ |
268 |
|
// Use the symmetric fact. There is no need to explictly make a |
269 |
|
// SYMM proof, as this is handled by CDProof::getProofFor below. |
270 |
|
it = d_lazyFactMap.find(factSym); |
271 |
|
} |
272 |
|
} |
273 |
6272 |
AlwaysAssert(it != d_lazyFactMap.end()); |
274 |
|
// now go back and convert it to proof steps and add to proof |
275 |
12544 |
std::shared_ptr<DatatypesInference> di = (*it).second; |
276 |
|
// run the conversion |
277 |
6272 |
convert(di->getId(), di->d_conc, di->d_exp, &pf); |
278 |
12544 |
return pf.getProofFor(fact); |
279 |
|
} |
280 |
|
|
281 |
15369 |
std::string InferProofCons::identify() const |
282 |
|
{ |
283 |
15369 |
return "datatypes::InferProofCons"; |
284 |
|
} |
285 |
|
|
286 |
|
} // namespace datatypes |
287 |
|
} // namespace theory |
288 |
29574 |
} // namespace cvc5 |