1 /********************* */
2 /*! \file infer_proof_cons.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Implementation of inference to proof conversion for datatypes
15 #include "theory/datatypes/infer_proof_cons.h"
17 #include "theory/datatypes/theory_datatypes_utils.h"
18 #include "theory/rewriter.h"
20 using namespace CVC4::kind
;
26 InferProofCons::InferProofCons(context::Context
* c
, ProofNodeManager
* pnm
)
27 : d_pnm(pnm
), d_lazyFactMap(c
== nullptr ? &d_context
: c
)
29 Assert(d_pnm
!= nullptr);
32 void InferProofCons::notifyFact(const std::shared_ptr
<DatatypesInference
>& di
)
34 TNode fact
= di
->d_conc
;
35 if (d_lazyFactMap
.find(fact
) != d_lazyFactMap
.end())
39 Node symFact
= CDProof::getSymmFact(fact
);
40 if (!symFact
.isNull() && d_lazyFactMap
.find(symFact
) != d_lazyFactMap
.end())
44 d_lazyFactMap
.insert(fact
, di
);
47 void InferProofCons::convert(InferenceId infer
, TNode conc
, TNode exp
, CDProof
* cdp
)
49 Trace("dt-ipc") << "convert: " << infer
<< ": " << conc
<< " by " << exp
52 std::vector
<Node
> expv
;
53 if (!exp
.isNull() && !exp
.isConst())
55 if (exp
.getKind() == AND
)
57 for (const Node
& ec
: exp
)
67 NodeManager
* nm
= NodeManager::currentNM();
71 case InferenceId::DATATYPES_UNIF
:
73 Assert(expv
.size() == 1);
74 Assert(exp
.getKind() == EQUAL
&& exp
[0].getKind() == APPLY_CONSTRUCTOR
75 && exp
[1].getKind() == APPLY_CONSTRUCTOR
76 && exp
[0].getOperator() == exp
[1].getOperator());
78 // we may be asked for a proof of (not P) coming from (= P false) or
79 // (= false P), or similarly P from (= P true) or (= true P).
80 bool concPol
= conc
.getKind() != NOT
;
81 Node concAtom
= concPol
? conc
: conc
[0];
83 for (size_t i
= 0, nchild
= exp
[0].getNumChildren(); i
< nchild
; i
++)
85 bool argSuccess
= false;
86 if (conc
.getKind() == EQUAL
)
88 argSuccess
= (exp
[0][i
] == conc
[0] && exp
[1][i
] == conc
[1]);
92 for (size_t j
= 0; j
< 2; j
++)
94 if (exp
[j
][i
] == concAtom
&& exp
[1 - j
][i
].isConst()
95 && exp
[1 - j
][i
].getConst
<bool>() == concPol
)
98 unifConc
= exp
[0][i
].eqNode(exp
[1][i
]);
105 narg
= nm
->mkConst(Rational(i
));
111 if (conc
.getKind() == EQUAL
)
113 // normal case where we conclude an equality
114 cdp
->addStep(conc
, PfRule::DT_UNIF
, {exp
}, {narg
});
118 // must use true or false elim to prove the final
119 cdp
->addStep(unifConc
, PfRule::DT_UNIF
, {exp
}, {narg
});
121 Node eq
= concAtom
.eqNode(nm
->mkConst(concPol
));
123 conc
, concPol
? PfRule::TRUE_ELIM
: PfRule::FALSE_ELIM
, {eq
}, {});
129 case InferenceId::DATATYPES_INST
:
131 if (expv
.size() == 1)
133 Assert(conc
.getKind() == EQUAL
);
134 int n
= utils::isTester(exp
);
138 Node nn
= nm
->mkConst(Rational(n
));
139 Node eq
= exp
.eqNode(conc
);
140 cdp
->addStep(eq
, PfRule::DT_INST
, {}, {t
, nn
});
141 cdp
->addStep(conc
, PfRule::EQ_RESOLVE
, {exp
, eq
}, {});
147 case InferenceId::DATATYPES_SPLIT
:
149 Assert(expv
.empty());
150 Node t
= conc
.getKind() == OR
? conc
[0][0] : conc
[0];
151 cdp
->addStep(conc
, PfRule::DT_SPLIT
, {}, {t
});
155 case InferenceId::DATATYPES_COLLAPSE_SEL
:
157 Assert(exp
.getKind() == EQUAL
);
159 // might be a Boolean conclusion
160 if (conc
.getKind() != EQUAL
)
162 bool concPol
= conc
.getKind() != NOT
;
163 Node concAtom
= concPol
? conc
: conc
[0];
164 concEq
= concAtom
.eqNode(nm
->mkConst(concPol
));
166 Assert(concEq
.getKind() == EQUAL
167 && concEq
[0].getKind() == APPLY_SELECTOR_TOTAL
);
168 Assert(exp
[0].getType().isDatatype());
169 Node sop
= concEq
[0].getOperator();
170 Node sl
= nm
->mkNode(APPLY_SELECTOR_TOTAL
, sop
, exp
[0]);
171 Node sr
= nm
->mkNode(APPLY_SELECTOR_TOTAL
, sop
, exp
[1]);
173 // --------------------- CONG ----------------- DT_COLLAPSE
174 // s(exp[0]) = s(exp[1]) s(exp[1]) = r
175 // --------------------------------------------------- TRANS
177 Node asn
= ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL
);
178 Node seq
= sl
.eqNode(sr
);
179 cdp
->addStep(seq
, PfRule::CONG
, {exp
}, {asn
, sop
});
180 Node sceq
= sr
.eqNode(concEq
[1]);
181 cdp
->addStep(sceq
, PfRule::DT_COLLAPSE
, {}, {sr
});
182 cdp
->addStep(sl
.eqNode(concEq
[1]), PfRule::TRANS
, {seq
, sceq
}, {});
183 if (conc
.getKind() != EQUAL
)
186 conc
.getKind() == NOT
? PfRule::FALSE_ELIM
: PfRule::TRUE_ELIM
;
187 cdp
->addStep(conc
, eid
, {concEq
}, {});
192 case InferenceId::DATATYPES_CLASH_CONFLICT
:
194 cdp
->addStep(conc
, PfRule::MACRO_SR_PRED_ELIM
, {exp
}, {});
198 case InferenceId::DATATYPES_TESTER_CONFLICT
:
200 // rewrites to false under substitution
201 Node fn
= nm
->mkConst(false);
202 cdp
->addStep(fn
, PfRule::MACRO_SR_PRED_ELIM
, expv
, {});
206 case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT
:
208 Assert(expv
.size() == 3);
209 Node tester1
= expv
[0];
211 nm
->mkNode(APPLY_TESTER
, expv
[1].getOperator(), expv
[0][0]);
212 cdp
->addStep(tester1c
,
213 PfRule::MACRO_SR_PRED_TRANSFORM
,
216 Node fn
= nm
->mkConst(false);
217 cdp
->addStep(fn
, PfRule::DT_CLASH
, {tester1
, tester1c
}, {});
221 // inferences currently not supported
222 case InferenceId::DATATYPES_LABEL_EXH
:
223 case InferenceId::DATATYPES_BISIMILAR
:
224 case InferenceId::DATATYPES_CYCLE
:
226 Trace("dt-ipc") << "...no conversion for inference " << infer
233 // failed to reconstruct, add trust
234 Trace("dt-ipc") << "...failed " << infer
<< std::endl
;
235 cdp
->addStep(conc
, PfRule::DT_TRUST
, expv
, {conc
});
239 Trace("dt-ipc") << "...success" << std::endl
;
243 std::shared_ptr
<ProofNode
> InferProofCons::getProofFor(Node fact
)
245 Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact
<< std::endl
;
249 NodeDatatypesInferenceMap::iterator it
= d_lazyFactMap
.find(fact
);
250 if (it
== d_lazyFactMap
.end())
252 Node factSym
= CDProof::getSymmFact(fact
);
253 if (!factSym
.isNull())
255 // Use the symmetric fact. There is no need to explictly make a
256 // SYMM proof, as this is handled by CDProof::getProofFor below.
257 it
= d_lazyFactMap
.find(factSym
);
260 AlwaysAssert(it
!= d_lazyFactMap
.end());
261 // now go back and convert it to proof steps and add to proof
262 std::shared_ptr
<DatatypesInference
> di
= (*it
).second
;
263 // run the conversion
264 convert(di
->getId(), di
->d_conc
, di
->d_exp
, &pf
);
265 return pf
.getProofFor(fact
);
268 std::string
InferProofCons::identify() const
270 return "datatypes::InferProofCons";
273 } // namespace datatypes
274 } // namespace theory