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 |
15275 |
InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state) |
34 |
|
: InferenceManagerBuffered(env, t, state, "theory::datatypes::"), |
35 |
15275 |
d_ipc(isProofEnabled() |
36 |
5372 |
? new InferProofCons(context(), env.getProofNodeManager()) |
37 |
|
: nullptr), |
38 |
15275 |
d_lemPg(isProofEnabled() |
39 |
5372 |
? new EagerProofGenerator(env.getProofNodeManager(), |
40 |
5372 |
userContext(), |
41 |
5372 |
"datatypes::lemPg") |
42 |
61941 |
: nullptr) |
43 |
|
{ |
44 |
15275 |
d_false = NodeManager::currentNM()->mkConst(false); |
45 |
15275 |
} |
46 |
|
|
47 |
15270 |
InferenceManager::~InferenceManager() |
48 |
|
{ |
49 |
15270 |
} |
50 |
|
|
51 |
541121 |
void InferenceManager::addPendingInference(Node conc, |
52 |
|
InferenceId id, |
53 |
|
Node exp, |
54 |
|
bool forceLemma) |
55 |
|
{ |
56 |
|
// if we are forcing the inference to be processed as a lemma, or if the |
57 |
|
// inference must be sent as a lemma based on the policy in |
58 |
|
// mustCommunicateFact. |
59 |
541121 |
if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp)) |
60 |
|
{ |
61 |
20543 |
d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id)); |
62 |
|
} |
63 |
|
else |
64 |
|
{ |
65 |
520578 |
d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id)); |
66 |
|
} |
67 |
541121 |
} |
68 |
|
|
69 |
6068178 |
void InferenceManager::process() |
70 |
|
{ |
71 |
|
// if we are in conflict, immediately reset and clear pending |
72 |
6068178 |
if (d_theoryState.isInConflict()) |
73 |
|
{ |
74 |
19043 |
reset(); |
75 |
19043 |
clearPending(); |
76 |
19043 |
return; |
77 |
|
} |
78 |
|
// process pending lemmas, used infrequently, only for definitional lemmas |
79 |
6049135 |
doPendingLemmas(); |
80 |
|
// now process the pending facts |
81 |
6049135 |
doPendingFacts(); |
82 |
|
} |
83 |
|
|
84 |
1720 |
void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p) |
85 |
|
{ |
86 |
1720 |
if (isProofEnabled()) |
87 |
|
{ |
88 |
168 |
TrustNode trn = processDtLemma(lem, Node::null(), id); |
89 |
84 |
trustedLemma(trn, id); |
90 |
84 |
return; |
91 |
|
} |
92 |
|
// otherwise send as a normal lemma directly |
93 |
1636 |
lemma(lem, id, p); |
94 |
|
} |
95 |
|
|
96 |
4090 |
void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id) |
97 |
|
{ |
98 |
4090 |
if (isProofEnabled()) |
99 |
|
{ |
100 |
394 |
Node exp = NodeManager::currentNM()->mkAnd(conf); |
101 |
197 |
prepareDtInference(d_false, exp, id, d_ipc.get()); |
102 |
|
} |
103 |
4090 |
conflictExp(id, conf, d_ipc.get()); |
104 |
4090 |
} |
105 |
|
|
106 |
20292 |
TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) |
107 |
|
{ |
108 |
|
// set up a proof constructor |
109 |
40584 |
std::shared_ptr<InferProofCons> ipcl; |
110 |
20292 |
if (isProofEnabled()) |
111 |
|
{ |
112 |
1018 |
ipcl = |
113 |
2036 |
std::make_shared<InferProofCons>(nullptr, d_env.getProofNodeManager()); |
114 |
|
} |
115 |
20292 |
conc = prepareDtInference(conc, exp, id, ipcl.get()); |
116 |
|
// send it as a lemma |
117 |
40584 |
Node lem; |
118 |
20292 |
if (!exp.isNull() && !exp.isConst()) |
119 |
|
{ |
120 |
19465 |
lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
827 |
lem = conc; |
125 |
|
} |
126 |
20292 |
if (isProofEnabled()) |
127 |
|
{ |
128 |
|
// store its proof |
129 |
2036 |
std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc); |
130 |
2036 |
std::shared_ptr<ProofNode> pn = pbody; |
131 |
1018 |
if (!exp.isNull() && !exp.isConst()) |
132 |
|
{ |
133 |
1594 |
std::vector<Node> expv; |
134 |
797 |
expv.push_back(exp); |
135 |
797 |
pn = d_env.getProofNodeManager()->mkScope(pbody, expv); |
136 |
|
} |
137 |
1018 |
d_lemPg->setProofFor(lem, pn); |
138 |
|
} |
139 |
40584 |
return TrustNode::mkTrustLemma(lem, d_lemPg.get()); |
140 |
|
} |
141 |
|
|
142 |
516156 |
Node InferenceManager::processDtFact(Node conc, |
143 |
|
Node exp, |
144 |
|
InferenceId id, |
145 |
|
ProofGenerator*& pg) |
146 |
|
{ |
147 |
516156 |
pg = d_ipc.get(); |
148 |
516156 |
return prepareDtInference(conc, exp, id, d_ipc.get()); |
149 |
|
} |
150 |
|
|
151 |
536645 |
Node InferenceManager::prepareDtInference(Node conc, |
152 |
|
Node exp, |
153 |
|
InferenceId id, |
154 |
|
InferProofCons* ipc) |
155 |
|
{ |
156 |
1073290 |
Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp |
157 |
536645 |
<< " by " << id << std::endl; |
158 |
536645 |
if (conc.getKind() == EQUAL && conc[0].getType().isBoolean()) |
159 |
|
{ |
160 |
|
// must turn (= conc false) into (not conc) |
161 |
812 |
conc = rewrite(conc); |
162 |
|
} |
163 |
536645 |
if (isProofEnabled()) |
164 |
|
{ |
165 |
13703 |
Assert(ipc != nullptr); |
166 |
|
// If proofs are enabled, notify the proof constructor. |
167 |
|
// Notice that we have to reconstruct a datatypes inference here. This is |
168 |
|
// because the inference in the pending vector may be destroyed as we are |
169 |
|
// processing this inference, if we triggered to backtrack based on the |
170 |
|
// call below, since it is a unique pointer. |
171 |
|
std::shared_ptr<DatatypesInference> di = |
172 |
27406 |
std::make_shared<DatatypesInference>(this, conc, exp, id); |
173 |
13703 |
ipc->notifyFact(di); |
174 |
|
} |
175 |
536645 |
return conc; |
176 |
|
} |
177 |
|
|
178 |
|
} // namespace datatypes |
179 |
|
} // namespace theory |
180 |
31140 |
} // namespace cvc5 |