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