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 "smt/smt_statistics_registry.h" |
21 |
|
#include "theory/eager_proof_generator.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 |
9459 |
InferenceManager::InferenceManager(Theory& t, |
34 |
|
TheoryState& state, |
35 |
9459 |
ProofNodeManager* pnm) |
36 |
|
: InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"), |
37 |
|
d_pnm(pnm), |
38 |
|
d_ipc(pnm == nullptr ? nullptr |
39 |
1192 |
: new InferProofCons(state.getSatContext(), pnm)), |
40 |
|
d_lemPg(pnm == nullptr |
41 |
|
? nullptr |
42 |
|
: new EagerProofGenerator( |
43 |
10651 |
pnm, state.getUserContext(), "datatypes::lemPg")) |
44 |
|
{ |
45 |
9459 |
d_false = NodeManager::currentNM()->mkConst(false); |
46 |
9459 |
} |
47 |
|
|
48 |
9459 |
InferenceManager::~InferenceManager() |
49 |
|
{ |
50 |
9459 |
} |
51 |
|
|
52 |
316788 |
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 |
316788 |
if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp)) |
61 |
|
{ |
62 |
21965 |
d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id)); |
63 |
|
} |
64 |
|
else |
65 |
|
{ |
66 |
294823 |
d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id)); |
67 |
|
} |
68 |
316788 |
} |
69 |
|
|
70 |
2410522 |
void InferenceManager::process() |
71 |
|
{ |
72 |
|
// process pending lemmas, used infrequently, only for definitional lemmas |
73 |
2410522 |
doPendingLemmas(); |
74 |
|
// now process the pending facts |
75 |
2410522 |
doPendingFacts(); |
76 |
2410522 |
} |
77 |
|
|
78 |
1162 |
void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p) |
79 |
|
{ |
80 |
1162 |
if (isProofEnabled()) |
81 |
|
{ |
82 |
160 |
TrustNode trn = processDtLemma(lem, Node::null(), id); |
83 |
80 |
trustedLemma(trn, id); |
84 |
80 |
return; |
85 |
|
} |
86 |
|
// otherwise send as a normal lemma directly |
87 |
1082 |
lemma(lem, id, p); |
88 |
|
} |
89 |
|
|
90 |
4512 |
void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id) |
91 |
|
{ |
92 |
4512 |
if (isProofEnabled()) |
93 |
|
{ |
94 |
1542 |
Node exp = NodeManager::currentNM()->mkAnd(conf); |
95 |
771 |
prepareDtInference(d_false, exp, id, d_ipc.get()); |
96 |
|
} |
97 |
4512 |
conflictExp(id, conf, d_ipc.get()); |
98 |
4512 |
} |
99 |
|
|
100 |
363635 |
bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; } |
101 |
|
|
102 |
21951 |
TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id) |
103 |
|
{ |
104 |
|
// set up a proof constructor |
105 |
43902 |
std::shared_ptr<InferProofCons> ipcl; |
106 |
21951 |
if (isProofEnabled()) |
107 |
|
{ |
108 |
900 |
ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm); |
109 |
|
} |
110 |
21951 |
conc = prepareDtInference(conc, exp, id, ipcl.get()); |
111 |
|
// send it as a lemma |
112 |
43902 |
Node lem; |
113 |
21951 |
if (!exp.isNull() && !exp.isConst()) |
114 |
|
{ |
115 |
21348 |
lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc); |
116 |
|
} |
117 |
|
else |
118 |
|
{ |
119 |
603 |
lem = conc; |
120 |
|
} |
121 |
21951 |
if (isProofEnabled()) |
122 |
|
{ |
123 |
|
// store its proof |
124 |
1800 |
std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc); |
125 |
1800 |
std::shared_ptr<ProofNode> pn = pbody; |
126 |
900 |
if (!exp.isNull() && !exp.isConst()) |
127 |
|
{ |
128 |
1466 |
std::vector<Node> expv; |
129 |
733 |
expv.push_back(exp); |
130 |
733 |
pn = d_pnm->mkScope(pbody, expv); |
131 |
|
} |
132 |
900 |
d_lemPg->setProofFor(lem, pn); |
133 |
|
} |
134 |
43902 |
return TrustNode::mkTrustLemma(lem, d_lemPg.get()); |
135 |
|
} |
136 |
|
|
137 |
291337 |
Node InferenceManager::processDtFact(Node conc, |
138 |
|
Node exp, |
139 |
|
InferenceId id, |
140 |
|
ProofGenerator*& pg) |
141 |
|
{ |
142 |
291337 |
pg = d_ipc.get(); |
143 |
291337 |
return prepareDtInference(conc, exp, id, d_ipc.get()); |
144 |
|
} |
145 |
|
|
146 |
314059 |
Node InferenceManager::prepareDtInference(Node conc, |
147 |
|
Node exp, |
148 |
|
InferenceId id, |
149 |
|
InferProofCons* ipc) |
150 |
|
{ |
151 |
628118 |
Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp |
152 |
314059 |
<< " by " << id << std::endl; |
153 |
314059 |
if (conc.getKind() == EQUAL && conc[0].getType().isBoolean()) |
154 |
|
{ |
155 |
|
// must turn (= conc false) into (not conc) |
156 |
511 |
conc = Rewriter::rewrite(conc); |
157 |
|
} |
158 |
314059 |
if (isProofEnabled()) |
159 |
|
{ |
160 |
12219 |
Assert(ipc != nullptr); |
161 |
|
// If proofs are enabled, notify the proof constructor. |
162 |
|
// Notice that we have to reconstruct a datatypes inference here. This is |
163 |
|
// because the inference in the pending vector may be destroyed as we are |
164 |
|
// processing this inference, if we triggered to backtrack based on the |
165 |
|
// call below, since it is a unique pointer. |
166 |
|
std::shared_ptr<DatatypesInference> di = |
167 |
24438 |
std::make_shared<DatatypesInference>(this, conc, exp, id); |
168 |
12219 |
ipc->notifyFact(di); |
169 |
|
} |
170 |
314059 |
return conc; |
171 |
|
} |
172 |
|
|
173 |
|
} // namespace datatypes |
174 |
|
} // namespace theory |
175 |
28191 |
} // namespace cvc5 |