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 |
|
* Datatypes inference manager. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/datatypes/inference_manager.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "options/datatypes_options.h" |
20 |
|
#include "proof/eager_proof_generator.h" |
21 |
|
#include "smt/smt_statistics_registry.h" |
22 |
|
#include "theory/rewriter.h" |
23 |
|
#include "theory/theory.h" |
24 |
|
#include "theory/theory_state.h" |
25 |
|
#include "theory/trust_substitutions.h" |
26 |
|
|
27 |
|
using namespace cvc5::kind; |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
namespace theory { |
31 |
|
namespace datatypes { |
32 |
|
|
33 |
9927 |
InferenceManager::InferenceManager(Theory& t, |
34 |
|
TheoryState& state, |
35 |
9927 |
ProofNodeManager* pnm) |
36 |
|
: InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"), |
37 |
|
d_pnm(pnm), |
38 |
|
d_ipc(pnm == nullptr ? nullptr |
39 |
1243 |
: new InferProofCons(state.getSatContext(), pnm)), |
40 |
|
d_lemPg(pnm == nullptr |
41 |
|
? nullptr |
42 |
|
: new EagerProofGenerator( |
43 |
11170 |
pnm, state.getUserContext(), "datatypes::lemPg")) |
44 |
|
{ |
45 |
9927 |
d_false = NodeManager::currentNM()->mkConst(false); |
46 |
9927 |
} |
47 |
|
|
48 |
9924 |
InferenceManager::~InferenceManager() |
49 |
|
{ |
50 |
9924 |
} |
51 |
|
|
52 |
302422 |
void InferenceManager::addPendingInference(Node conc, |
53 |
|
InferenceId id, |
54 |
|
Node exp, |
55 |
|
bool forceLemma) |
56 |
|
{ |
57 |
|
// if we are forcing the inference to be processed as a lemma, or if the |
58 |
|
// inference must be sent as a lemma based on the policy in |
59 |
|
// mustCommunicateFact. |
60 |
302422 |
if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp)) |
61 |
|
{ |
62 |
22423 |
d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id)); |
63 |
|
} |
64 |
|
else |
65 |
|
{ |
66 |
279999 |
d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id)); |
67 |
|
} |
68 |
302422 |
} |
69 |
|
|
70 |
2599235 |
void InferenceManager::process() |
71 |
|
{ |
72 |
|
// if we are in conflict, immediately reset and clear pending |
73 |
2599235 |
if (d_theoryState.isInConflict()) |
74 |
|
{ |
75 |
11377 |
reset(); |
76 |
11377 |
clearPending(); |
77 |
11377 |
return; |
78 |
|
} |
79 |
|
// process pending lemmas, used infrequently, only for definitional lemmas |
80 |
2587858 |
doPendingLemmas(); |
81 |
|
// now process the pending facts |
82 |
2587858 |
doPendingFacts(); |
83 |
|
} |
84 |
|
|
85 |
1277 |
void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p) |
86 |
|
{ |
87 |
1277 |
if (isProofEnabled()) |
88 |
|
{ |
89 |
180 |
TrustNode trn = processDtLemma(lem, Node::null(), id); |
90 |
90 |
trustedLemma(trn, id); |
91 |
90 |
return; |
92 |
|
} |
93 |
|
// otherwise send as a normal lemma directly |
94 |
1187 |
lemma(lem, id, p); |
95 |
|
} |
96 |
|
|
97 |
2466 |
void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id) |
98 |
|
{ |
99 |
2466 |
if (isProofEnabled()) |
100 |
|
{ |
101 |
372 |
Node exp = NodeManager::currentNM()->mkAnd(conf); |
102 |
186 |
prepareDtInference(d_false, exp, id, d_ipc.get()); |
103 |
|
} |
104 |
2466 |
conflictExp(id, conf, d_ipc.get()); |
105 |
2466 |
} |
106 |
|
|
107 |
347807 |
bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; } |
108 |
|
|
109 |
22359 |
TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) |
110 |
|
{ |
111 |
|
// set up a proof constructor |
112 |
44718 |
std::shared_ptr<InferProofCons> ipcl; |
113 |
22359 |
if (isProofEnabled()) |
114 |
|
{ |
115 |
980 |
ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm); |
116 |
|
} |
117 |
22359 |
conc = prepareDtInference(conc, exp, id, ipcl.get()); |
118 |
|
// send it as a lemma |
119 |
44718 |
Node lem; |
120 |
22359 |
if (!exp.isNull() && !exp.isConst()) |
121 |
|
{ |
122 |
21602 |
lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); |
123 |
|
} |
124 |
|
else |
125 |
|
{ |
126 |
757 |
lem = conc; |
127 |
|
} |
128 |
22359 |
if (isProofEnabled()) |
129 |
|
{ |
130 |
|
// store its proof |
131 |
1960 |
std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc); |
132 |
1960 |
std::shared_ptr<ProofNode> pn = pbody; |
133 |
980 |
if (!exp.isNull() && !exp.isConst()) |
134 |
|
{ |
135 |
1546 |
std::vector<Node> expv; |
136 |
773 |
expv.push_back(exp); |
137 |
773 |
pn = d_pnm->mkScope(pbody, expv); |
138 |
|
} |
139 |
980 |
d_lemPg->setProofFor(lem, pn); |
140 |
|
} |
141 |
44718 |
return TrustNode::mkTrustLemma(lem, d_lemPg.get()); |
142 |
|
} |
143 |
|
|
144 |
276801 |
Node InferenceManager::processDtFact(Node conc, |
145 |
|
Node exp, |
146 |
|
InferenceId id, |
147 |
|
ProofGenerator*& pg) |
148 |
|
{ |
149 |
276801 |
pg = d_ipc.get(); |
150 |
276801 |
return prepareDtInference(conc, exp, id, d_ipc.get()); |
151 |
|
} |
152 |
|
|
153 |
299346 |
Node InferenceManager::prepareDtInference(Node conc, |
154 |
|
Node exp, |
155 |
|
InferenceId id, |
156 |
|
InferProofCons* ipc) |
157 |
|
{ |
158 |
598692 |
Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp |
159 |
299346 |
<< " by " << id << std::endl; |
160 |
299346 |
if (conc.getKind() == EQUAL && conc[0].getType().isBoolean()) |
161 |
|
{ |
162 |
|
// must turn (= conc false) into (not conc) |
163 |
508 |
conc = Rewriter::rewrite(conc); |
164 |
|
} |
165 |
299346 |
if (isProofEnabled()) |
166 |
|
{ |
167 |
11376 |
Assert(ipc != nullptr); |
168 |
|
// If proofs are enabled, notify the proof constructor. |
169 |
|
// Notice that we have to reconstruct a datatypes inference here. This is |
170 |
|
// because the inference in the pending vector may be destroyed as we are |
171 |
|
// processing this inference, if we triggered to backtrack based on the |
172 |
|
// call below, since it is a unique pointer. |
173 |
|
std::shared_ptr<DatatypesInference> di = |
174 |
22752 |
std::make_shared<DatatypesInference>(this, conc, exp, id); |
175 |
11376 |
ipc->notifyFact(di); |
176 |
|
} |
177 |
299346 |
return conc; |
178 |
|
} |
179 |
|
|
180 |
|
} // namespace datatypes |
181 |
|
} // namespace theory |
182 |
29505 |
} // namespace cvc5 |