1 /********************* */
2 /*! \file array_proof.cpp
4 ** Top contributors (to current version):
5 ** Guy Katz, Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 ** [[ Add lengthier description here ]]
14 ** \todo document this file
18 #include "proof/array_proof.h"
22 #include "proof/proof_manager.h"
23 #include "proof/simplify_boolean_node.h"
24 #include "proof/theory_proof.h"
25 #include "theory/arrays/theory_arrays.h"
31 class ArrayProofPrinter
: public theory::eq::EqProof::PrettyPrinter
{
33 ArrayProofPrinter(unsigned row
, unsigned row1
, unsigned ext
)
34 : d_row(row
), d_row1(row1
), d_ext(ext
) {}
36 std::string
printTag(unsigned tag
) override
;
40 const unsigned d_row1
;
42 }; // class ArrayProofPrinter
44 std::string
ArrayProofPrinter::printTag(unsigned tag
) {
45 if (tag
== theory::eq::MERGED_THROUGH_CONGRUENCE
) return "Congruence";
46 if (tag
== theory::eq::MERGED_THROUGH_EQUALITY
) return "Pure Equality";
47 if (tag
== theory::eq::MERGED_THROUGH_REFLEXIVITY
) return "Reflexivity";
48 if (tag
== theory::eq::MERGED_THROUGH_CONSTANTS
) return "Constants";
49 if (tag
== theory::eq::MERGED_THROUGH_TRANS
) return "Transitivity";
51 if (tag
== d_row
) return "Read Over Write";
52 if (tag
== d_row1
) return "Read Over Write (1)";
53 if (tag
== d_ext
) return "Extensionality";
55 std::ostringstream result
;
62 inline static Node
eqNode(TNode n1
, TNode n2
) {
63 return NodeManager::currentNM()->mkNode(kind::EQUAL
, n1
, n2
);
66 // congrence matching term helper
67 inline static bool match(TNode n1
, TNode n2
) {
68 Debug("mgd") << "match " << n1
<< " " << n2
<< std::endl
;
69 if(ProofManager::currentPM()->hasOp(n1
)) {
70 n1
= ProofManager::currentPM()->lookupOp(n1
);
72 if(ProofManager::currentPM()->hasOp(n2
)) {
73 n2
= ProofManager::currentPM()->lookupOp(n2
);
75 Debug("mgd") << "+ match " << n1
<< " " << n2
<< std::endl
;
76 Debug("pf::array") << "+ match: step 1" << std::endl
;
81 if(n1
.getType().isFunction() && n2
.hasOperator()) {
82 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
83 return n1
== ProofManager::currentPM()->lookupOp(n2
.getOperator());
85 return n1
== n2
.getOperator();
89 if(n2
.getType().isFunction() && n1
.hasOperator()) {
90 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
91 return n2
== ProofManager::currentPM()->lookupOp(n1
.getOperator());
93 return n2
== n1
.getOperator();
97 if(n1
.hasOperator() && n2
.hasOperator() && n1
.getOperator() != n2
.getOperator()) {
98 if (!((n1
.getKind() == kind::SELECT
&& n2
.getKind() == kind::PARTIAL_SELECT_0
) ||
99 (n1
.getKind() == kind::SELECT
&& n2
.getKind() == kind::PARTIAL_SELECT_1
) ||
100 (n1
.getKind() == kind::PARTIAL_SELECT_1
&& n2
.getKind() == kind::SELECT
) ||
101 (n1
.getKind() == kind::PARTIAL_SELECT_1
&& n2
.getKind() == kind::PARTIAL_SELECT_0
) ||
102 (n1
.getKind() == kind::PARTIAL_SELECT_0
&& n2
.getKind() == kind::SELECT
) ||
103 (n1
.getKind() == kind::PARTIAL_SELECT_0
&& n2
.getKind() == kind::PARTIAL_SELECT_1
)
109 for(size_t i
= 0; i
< n1
.getNumChildren() && i
< n2
.getNumChildren(); ++i
) {
118 ProofArray::ProofArray(std::shared_ptr
<theory::eq::EqProof
> pf
, unsigned row
,
119 unsigned row1
, unsigned ext
)
120 : d_proof(pf
), d_reasonRow(row
), d_reasonRow1(row1
), d_reasonExt(ext
) {}
122 void ProofArray::toStream(std::ostream
& out
) {
127 void ProofArray::toStream(std::ostream
& out
, const ProofLetMap
& map
) {
128 Trace("pf::array") << "; Print Array proof..." << std::endl
;
129 toStreamLFSC(out
, ProofManager::getArrayProof(), *d_proof
, map
);
130 Debug("pf::array") << "; Print Array proof done!" << std::endl
;
133 void ProofArray::toStreamLFSC(std::ostream
& out
, TheoryProof
* tp
,
134 const theory::eq::EqProof
& pf
,
135 const ProofLetMap
& map
) {
136 Debug("pf::array") << "Printing array proof in LFSC : " << std::endl
;
137 ArrayProofPrinter
proofPrinter(d_reasonRow
, d_reasonRow1
, d_reasonExt
);
138 pf
.debug_print("pf::array", 0, &proofPrinter
);
139 Debug("pf::array") << std::endl
;
140 toStreamRecLFSC(out
, tp
, pf
, 0, map
);
141 Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl
;
144 Node
ProofArray::toStreamRecLFSC(std::ostream
& out
, TheoryProof
* tp
,
145 const theory::eq::EqProof
& pf
, unsigned tb
,
146 const ProofLetMap
& map
) {
147 Debug("pf::array") << std::endl
149 << "toStreamRecLFSC called. tb = " << tb
150 << " . proof:" << std::endl
;
151 ArrayProofPrinter
proofPrinter(d_reasonRow
, d_reasonRow1
, d_reasonExt
);
152 pf
.debug_print("pf::array", 0, &proofPrinter
);
153 Debug("pf::array") << std::endl
;
156 Assert(pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
);
157 Assert(!pf
.d_node
.isNull());
158 Assert(pf
.d_children
.size() >= 2);
161 std::shared_ptr
<theory::eq::EqProof
> subTrans
=
162 std::make_shared
<theory::eq::EqProof
>();
163 subTrans
->d_id
= theory::eq::MERGED_THROUGH_TRANS
;
164 subTrans
->d_node
= pf
.d_node
;
167 while (i
< pf
.d_children
.size()) {
168 if (pf
.d_children
[i
]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
)
169 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
171 // Look for the negative clause, with which we will form a contradiction.
172 if(!pf
.d_children
[i
]->d_node
.isNull() && pf
.d_children
[i
]->d_node
.getKind() == kind::NOT
) {
178 // Handle congruence closures over equalities.
179 else if (pf
.d_children
[i
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&& pf
.d_children
[i
]->d_node
.isNull()) {
180 Debug("pf::array") << "Handling congruence over equalities" << std::endl
;
182 // Gather the sequence of consecutive congruence closures.
183 std::vector
<std::shared_ptr
<const theory::eq::EqProof
>> congruenceClosures
;
185 Debug("pf::array") << "Collecting congruence sequence" << std::endl
;
187 i
+ count
< pf
.d_children
.size() &&
188 pf
.d_children
[i
+ count
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&&
189 pf
.d_children
[i
+ count
]->d_node
.isNull();
191 Debug("pf::array") << "Found a congruence: " << std::endl
;
192 pf
.d_children
[i
+ count
]->debug_print("pf::array", 0, &proofPrinter
);
193 congruenceClosures
.push_back(pf
.d_children
[i
+ count
]);
196 Debug("pf::array") << "Total number of congruences found: " << congruenceClosures
.size() << std::endl
;
198 // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
199 bool targetAppearsBefore
= true;
200 bool targetAppearsAfter
= true;
202 if ((i
== 0) || (i
== 1 && neg
== 0)) {
203 Debug("pf::array") << "Target does not appear before" << std::endl
;
204 targetAppearsBefore
= false;
207 if ((i
+ count
>= pf
.d_children
.size()) ||
208 (!pf
.d_children
[i
+ count
]->d_node
.isNull() &&
209 pf
.d_children
[i
+ count
]->d_node
.getKind() == kind::NOT
)) {
210 Debug("pf::array") << "Target does not appear after" << std::endl
;
211 targetAppearsAfter
= false;
214 // Assert that we have precisely one target clause.
215 Assert(targetAppearsBefore
!= targetAppearsAfter
);
217 // Begin breaking up the congruences and ordering the equalities correctly.
218 std::vector
<std::shared_ptr
<theory::eq::EqProof
>> orderedEqualities
;
220 // Insert target clause first.
221 if (targetAppearsBefore
) {
222 orderedEqualities
.push_back(pf
.d_children
[i
- 1]);
223 // The target has already been added to subTrans; remove it.
224 subTrans
->d_children
.pop_back();
226 orderedEqualities
.push_back(pf
.d_children
[i
+ count
]);
229 // Start with the congruence closure closest to the target clause, and work our way back/forward.
230 if (targetAppearsBefore
) {
231 for (unsigned j
= 0; j
< count
; ++j
) {
232 if (pf
.d_children
[i
+ j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
233 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ j
]->d_children
[0]);
234 if (pf
.d_children
[i
+ j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
235 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ j
]->d_children
[1]);
238 for (unsigned j
= 0; j
< count
; ++j
) {
239 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
240 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]);
241 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
242 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]);
246 // Copy the result into the main transitivity proof.
247 subTrans
->d_children
.insert(subTrans
->d_children
.end(), orderedEqualities
.begin(), orderedEqualities
.end());
249 // Increase i to skip over the children that have been processed.
251 if (targetAppearsAfter
) {
256 // Else, just copy the child proof as is
258 subTrans
->d_children
.push_back(pf
.d_children
[i
]);
263 bool disequalityFound
= (neg
>= 0);
264 if (!disequalityFound
) {
265 Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl
;
266 Debug("pf::array") << "Proof for: " << pf
.d_node
<< std::endl
;
267 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
268 Assert(pf
.d_node
.getNumChildren() == 2);
269 Assert (pf
.d_node
[0].isConst() && pf
.d_node
[1].isConst());
273 std::stringstream ss
, ss2
;
274 //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
275 Debug("mgdx") << "\nsubtrans has " << subTrans
->d_children
.size() << " children\n";
276 if(!disequalityFound
|| pf
.d_children
.size() > 2) {
277 n1
= toStreamRecLFSC(ss
, tp
, *subTrans
, 1, map
);
279 n1
= toStreamRecLFSC(ss
, tp
, *(subTrans
->d_children
[0]), 1, map
);
280 Debug("mgdx") << "\nsubTrans unique child "
281 << subTrans
->d_children
[0]->d_id
282 << " was proven\ngot: " << n1
<< std::endl
;
285 out
<< "(clausify_false (contra _ ";
287 if (disequalityFound
) {
288 Node n2
= pf
.d_children
[neg
]->d_node
;
289 Assert(n2
.getKind() == kind::NOT
);
290 Debug("mgdx") << "\nhave proven: " << n1
<< std::endl
;
291 Debug("mgdx") << "n2 is " << n2
<< std::endl
;
292 Debug("mgdx") << "n2->d_id is " << pf
.d_children
[neg
]->d_id
<< std::endl
;
293 Debug("mgdx") << "n2[0] is " << n2
[0] << std::endl
;
295 if (n2
[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2
[0][0] << std::endl
; }
296 if (n1
.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1
[1] << std::endl
; }
298 if ((pf
.d_children
[neg
]->d_id
== d_reasonExt
) ||
299 (pf
.d_children
[neg
]->d_id
== theory::eq::MERGED_THROUGH_TRANS
)) {
300 // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
303 toStreamRecLFSC(ss2
, tp
, *pf
.d_children
[neg
], 1, map
);
305 } else if (n2
[0].getKind() == kind::APPLY_UF
) {
306 out
<< "(trans _ _ _ _ ";
307 out
<< "(symm _ _ _ ";
309 out
<< ") (pred_eq_f _ " << ProofManager::getLitName(n2
[0]) << ")) t_t_neq_f))" << std::endl
;
311 Assert((n1
[0] == n2
[0][0] && n1
[1] == n2
[0][1]) || (n1
[1] == n2
[0][0] && n1
[0] == n2
[0][1]));
312 if(n1
[1] == n2
[0][0]) {
313 out
<< "(symm _ _ _ " << ss
.str() << ")";
317 Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2
[0] << " ) = " <<
318 ProofManager::getLitName(n2
[0]) << std::endl
;
320 out
<< " " << ProofManager::getLitName(n2
[0]);
324 Assert(n2
.getKind() == kind::EQUAL
);
325 Assert((n1
[0] == n2
[0] && n1
[1] == n2
[1]) || (n1
[1] == n2
[0] && n1
[0] == n2
[1]));
329 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out
,
335 out
<< "))" << std::endl
;
339 if (pf
.d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
) {
340 Debug("mgd") << "\nok, looking at congruence:\n";
341 pf
.debug_print("mgd", 0, &proofPrinter
);
342 std::stack
<const theory::eq::EqProof
*> stk
;
343 for (const theory::eq::EqProof
* pf2
= &pf
;
344 pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
;
345 pf2
= pf2
->d_children
[0].get()) {
346 Debug("mgd") << "Looking at pf2 with d_node: " << pf2
->d_node
348 Assert(!pf2
->d_node
.isNull());
349 Assert(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
||
350 pf2
->d_node
.getKind() == kind::BUILTIN
||
351 pf2
->d_node
.getKind() == kind::APPLY_UF
||
352 pf2
->d_node
.getKind() == kind::SELECT
||
353 pf2
->d_node
.getKind() == kind::PARTIAL_SELECT_0
||
354 pf2
->d_node
.getKind() == kind::PARTIAL_SELECT_1
||
355 pf2
->d_node
.getKind() == kind::STORE
);
357 Assert(pf2
->d_children
.size() == 2);
358 out
<< "(cong _ _ _ _ _ _ ";
361 Assert(stk
.top()->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
);
362 // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
363 NodeBuilder
<> b1
, b2
;
365 const theory::eq::EqProof
* pf2
= stk
.top();
367 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
368 Node n1
= toStreamRecLFSC(out
, tp
, *(pf2
->d_children
[0]), tb
+ 1, map
);
370 std::stringstream ss
;
371 Node n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
374 Debug("mgd") << "\nok, in FIRST cong[" << stk
.size() << "]" << "\n";
375 pf2
->debug_print("mgd", 0, &proofPrinter
);
377 Debug("mgd") << "n1 is a proof for: " << pf2
->d_children
[0]->d_node
<< ". It is: " << n1
<< std::endl
;
378 Debug("mgd") << "n2 is a proof for: " << pf2
->d_children
[1]->d_node
<< ". It is: " << n2
<< std::endl
;
380 Debug("mgd") << "looking at " << pf2
->d_node
<< "\n";
381 Debug("mgd") << " " << n1
<< "\n";
382 Debug("mgd") << " " << n2
<< "\n";
385 if(match(pf2
->d_node
, n1
[0])) {
386 Debug("mgd") << "SIDE IS 0\n";
389 Debug("mgd") << "SIDE IS 1\n";
390 if(!match(pf2
->d_node
, n1
[1])) {
391 Debug("mgd") << "IN BAD CASE, our first subproof is\n";
392 pf2
->d_children
[0]->debug_print("mgd", 0, &proofPrinter
);
394 Assert(match(pf2
->d_node
, n1
[1]));
398 if(n1
[side
].getKind() == kind::APPLY_UF
||
399 n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
||
400 n1
[side
].getKind() == kind::SELECT
||
401 n1
[side
].getKind() == kind::PARTIAL_SELECT_1
||
402 n1
[side
].getKind() == kind::STORE
) {
403 if(n1
[side
].getKind() == kind::APPLY_UF
|| n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
) {
404 b1
<< kind::PARTIAL_APPLY_UF
;
405 b1
<< n1
[side
].getOperator();
406 } else if (n1
[side
].getKind() == kind::SELECT
|| n1
[side
].getKind() == kind::PARTIAL_SELECT_1
) {
407 // b1 << n1[side].getKind();
410 b1
<< kind::PARTIAL_APPLY_UF
;
411 b1
<< ProofManager::currentPM()->mkOp(n1
[side
].getOperator());
413 b1
.append(n1
[side
].begin(), n1
[side
].end());
415 else if (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
) {
416 b1
<< kind::PARTIAL_SELECT_1
;
421 if(n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
||
422 n1
[1-side
].getKind() == kind::APPLY_UF
||
423 n1
[1-side
].getKind() == kind::SELECT
||
424 n1
[1-side
].getKind() == kind::PARTIAL_SELECT_1
||
425 n1
[1-side
].getKind() == kind::STORE
) {
426 if(n1
[1-side
].getKind() == kind::APPLY_UF
||
427 n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
) {
428 b2
<< kind::PARTIAL_APPLY_UF
;
429 b2
<< n1
[1-side
].getOperator();
430 } else if (n1
[1-side
].getKind() == kind::SELECT
|| n1
[1-side
].getKind() == kind::PARTIAL_SELECT_1
) {
431 // b2 << n1[1-side].getKind();
434 b2
<< kind::PARTIAL_APPLY_UF
;
435 b2
<< ProofManager::currentPM()->mkOp(n1
[1-side
].getOperator());
437 b2
.append(n1
[1-side
].begin(), n1
[1-side
].end());
438 } else if (n1
[1-side
].getKind() == kind::PARTIAL_SELECT_0
) {
439 b2
<< kind::PARTIAL_SELECT_1
;
443 Debug("mgd") << "pf2->d_node " << pf2
->d_node
<< std::endl
;
444 Debug("mgd") << "b1.getNumChildren() " << b1
.getNumChildren() << std::endl
;
445 Debug("mgd") << "n1 " << n1
<< std::endl
;
446 Debug("mgd") << "n2 " << n2
<< std::endl
;
447 // These debug prints can cause a problem if we're constructing a SELECT node and it doesn't have enough
449 // Debug("mgd") << "b1 " << b1 << std::endl;
450 // Debug("mgd") << "b2 " << b2 << std::endl;
451 Debug("mgd") << "side " << side
<< std::endl
;
452 Debug("mgd") << "pf2->d_node's number of children: " << pf2
->d_node
.getNumChildren() << std::endl
;
453 Debug("mgd") << "pf2->d_node's meta kind: " << pf2
->d_node
.getMetaKind() << std::endl
;
454 Debug("mgd") << "Is this meta kind considered parameterized? " << (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
) << std::endl
;
456 if(pf2
->d_node
[b1
.getNumChildren() +
457 (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
? 1 : 0) +
458 (n1
[side
].getKind() == kind::PARTIAL_SELECT_1
? 1 : 0) -
459 (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[side
]) {
464 Assert(pf2
->d_node
[b1
.getNumChildren() +
465 (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
? 1 : 0) +
466 (n1
[side
].getKind() == kind::PARTIAL_SELECT_1
? 1 : 0) -
467 (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[1-side
]);
470 out
<< "(symm _ _ _ " << ss
.str() << ")";
473 Debug("mgd") << "After first insertion:" << std::endl
;
474 Debug("mgd") << "b1 " << b1
<< std::endl
;
475 Debug("mgd") << "b2 " << b2
<< std::endl
;
478 while(!stk
.empty()) {
480 Debug("mgd") << "\nMORE TO DO\n";
484 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
487 n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
489 Debug("mgd") << "\nok, in cong[" << stk
.size() << "]" << "\n";
490 Debug("mgd") << "looking at " << pf2
->d_node
<< "\n";
491 Debug("mgd") << " " << n1
<< "\n";
492 Debug("mgd") << " " << n2
<< "\n";
493 Debug("mgd") << " " << b1
<< "\n";
494 Debug("mgd") << " " << b2
<< "\n";
495 if(pf2
->d_node
[b1
.getNumChildren()] == n2
[side
]) {
500 Assert(pf2
->d_node
[b1
.getNumChildren()] == n2
[1-side
]);
503 out
<< "(symm _ _ _ " << ss
.str() << ")";
510 Debug("mgd") << "at end assert!" << std::endl
511 << "pf2->d_node = " << pf2
->d_node
<< std::endl
512 << "n1 (assigned from b1) = " << n1
<< std::endl
513 << "n2 (assigned from b2) = " << n2
<< std::endl
;
515 if(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
) {
516 Assert(n1
== pf2
->d_node
);
519 Debug("mgd") << "n1.getOperator().getType().getNumChildren() = "
520 << n1
.getOperator().getType().getNumChildren() << std::endl
;
521 Debug("mgd") << "n1.getNumChildren() + 1 = "
522 << n1
.getNumChildren() + 1 << std::endl
;
524 Assert(!((n1
.getKind() == kind::PARTIAL_SELECT_0
&& n1
.getNumChildren() == 2)));
525 if (n1
.getKind() == kind::PARTIAL_SELECT_1
&& n1
.getNumChildren() == 2) {
526 Debug("mgd") << "Finished a SELECT. Updating.." << std::endl
;
527 b1
.clear(kind::SELECT
);
528 b1
.append(n1
.begin(), n1
.end());
530 Debug("mgd") << "New n1: " << n1
<< std::endl
;
531 // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
532 // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
533 // b1.clear(kind::PARTIAL_SELECT_1);
534 // b1.append(n1.begin(), n1.end());
536 // Debug("mgd") << "New n1: " << n1 << std::endl;
538 } else if(n1
.getOperator().getType().getNumChildren() == n1
.getNumChildren() + 1) {
539 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
540 b1
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
542 b1
.clear(kind::APPLY_UF
);
543 b1
<< n1
.getOperator();
545 b1
.append(n1
.begin(), n1
.end());
547 Debug("mgd") << "at[2] end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
548 if(pf2
->d_node
.getKind() == kind::APPLY_UF
) {
549 Assert(n1
== pf2
->d_node
);
553 Debug("mgd") << "n2.getOperator().getType().getNumChildren() = "
554 << n2
.getOperator().getType().getNumChildren() << std::endl
;
555 Debug("mgd") << "n2.getNumChildren() + 1 = "
556 << n2
.getNumChildren() + 1 << std::endl
;
558 Assert(!((n2
.getKind() == kind::PARTIAL_SELECT_0
&& n2
.getNumChildren() == 2)));
559 if (n2
.getKind() == kind::PARTIAL_SELECT_1
&& n2
.getNumChildren() == 2) {
560 Debug("mgd") << "Finished a SELECT. Updating.." << std::endl
;
561 b2
.clear(kind::SELECT
);
562 b2
.append(n2
.begin(), n2
.end());
564 Debug("mgd") << "New n2: " << n2
<< std::endl
;
565 // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
566 // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
567 // b2.clear(kind::PARTIAL_SELECT_1);
568 // b2.append(n2.begin(), n2.end());
570 // Debug("mgd") << "New n2: " << n2 << std::endl;
572 } else if(n2
.getOperator().getType().getNumChildren() == n2
.getNumChildren() + 1) {
573 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
574 b2
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
576 b2
.clear(kind::APPLY_UF
);
577 b2
<< n2
.getOperator();
579 b2
.append(n2
.begin(), n2
.end());
582 Node n
= (side
== 0 ? eqNode(n1
, n2
) : eqNode(n2
, n1
));
584 Debug("mgdx") << "\ncong proved: " << n
<< "\n";
588 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_REFLEXIVITY
) {
589 Assert(!pf
.d_node
.isNull());
590 Assert(pf
.d_children
.empty());
592 tp
->printTerm(NodeManager::currentNM()->toExpr(pf
.d_node
), out
, map
);
594 return eqNode(pf
.d_node
, pf
.d_node
);
597 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_EQUALITY
) {
598 Assert(!pf
.d_node
.isNull());
599 Assert(pf
.d_children
.empty());
600 Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf
.d_node
.negate() << " ) = " <<
601 ProofManager::getLitName(pf
.d_node
.negate()) << std::endl
;
602 out
<< ProofManager::getLitName(pf
.d_node
.negate());
606 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_CONSTANTS
) {
607 Debug("pf::array") << "Proof for: " << pf
.d_node
<< std::endl
;
608 Assert(pf
.d_node
.getKind() == kind::NOT
);
609 Node n
= pf
.d_node
[0];
610 Assert(n
.getKind() == kind::EQUAL
);
611 Assert(n
.getNumChildren() == 2);
612 Assert(n
[0].isConst() && n
[1].isConst());
614 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out
,
621 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
) {
622 bool firstNeg
= false;
623 bool secondNeg
= false;
625 Assert(!pf
.d_node
.isNull());
626 Assert(pf
.d_children
.size() >= 2);
627 std::stringstream ss
;
628 Debug("mgd") << "\ndoing trans proof[[\n";
629 pf
.debug_print("mgd", 0, &proofPrinter
);
630 Debug("mgd") << "\n";
632 pf
.d_children
[0]->d_node
= simplifyBooleanNode(pf
.d_children
[0]->d_node
);
634 Node n1
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
635 Debug("mgd") << "\ndoing trans proof, got n1 " << n1
<< "\n";
637 Debug("mgdx") << "\ntrans proof[0], got n1 " << n1
<< "\n";
640 bool identicalEqualities
= false;
641 bool evenLengthSequence
;
642 Node nodeAfterEqualitySequence
;
644 std::map
<size_t, Node
> childToStream
;
646 for(size_t i
= 1; i
< pf
.d_children
.size(); ++i
) {
647 std::stringstream
ss1(ss
.str()), ss2
;
650 // In congruences, we can have something like a[x] - it's important to keep these,
651 // and not turn them into (a[x]=true), because that will mess up the congruence application
654 if (pf
.d_children
[i
]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
)
655 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
657 // It is possible that we've already converted the i'th child to stream. If so,
658 // use previously stored result. Otherwise, convert and store.
660 if (childToStream
.find(i
) != childToStream
.end())
661 n2
= childToStream
[i
];
663 n2
= toStreamRecLFSC(ss2
, tp
, *(pf
.d_children
[i
]), tb
+ 1, map
);
664 childToStream
[i
] = n2
;
667 Debug("mgd") << "\ndoing trans proof, got (first) n2 " << n2
<< "\n";
669 // The following branch is dedicated to handling sequences of identical equalities,
670 // i.e. trans[ a=b, a=b, a=b ].
672 // There are two cases:
673 // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
675 // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
676 // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
677 // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
678 // and use it to determine which option we need.
680 if(n2
.getKind() == kind::EQUAL
) {
681 if (((n1
[0] == n2
[0]) && (n1
[1] == n2
[1])) || ((n1
[0] == n2
[1]) && (n1
[1] == n2
[0]))) {
682 // We are in a sequence of identical equalities
684 Debug("pf::array") << "Detected identical equalities: " << std::endl
<< "\t" << n1
<< std::endl
;
686 if (!identicalEqualities
) {
687 // The sequence of identical equalities has started just now
688 identicalEqualities
= true;
690 Debug("pf::array") << "The sequence is just beginning. Determining length..." << std::endl
;
692 // Determine whether the length of this sequence is odd or even.
693 evenLengthSequence
= true;
694 bool sequenceOver
= false;
697 while (j
< pf
.d_children
.size() && !sequenceOver
) {
698 std::stringstream dontCare
;
699 nodeAfterEqualitySequence
= toStreamRecLFSC(dontCare
, tp
, *(pf
.d_children
[j
]), tb
+ 1, map
);
701 if (((nodeAfterEqualitySequence
[0] == n1
[0]) && (nodeAfterEqualitySequence
[1] == n1
[1])) ||
702 ((nodeAfterEqualitySequence
[0] == n1
[1]) && (nodeAfterEqualitySequence
[1] == n1
[0]))) {
703 evenLengthSequence
= !evenLengthSequence
;
711 if (evenLengthSequence
) {
712 // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
714 Debug("pf::array") << "Equality sequence of even length" << std::endl
;
715 Debug("pf::array") << "n1 is: " << n1
<< std::endl
;
716 Debug("pf::array") << "n2 is: " << n2
<< std::endl
;
717 Debug("pf::array") << "pf-d_node is: " << pf
.d_node
<< std::endl
;
718 Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence
<< std::endl
;
720 ss
<< "(trans _ _ _ _ ";
722 // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
724 if (match(n1
[0], pf
.d_node
[0])) {
725 n1
= eqNode(n1
[0], n1
[0]);
726 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
727 } else if (match(n1
[1], pf
.d_node
[1])) {
728 n1
= eqNode(n1
[1], n1
[1]);
729 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
731 Debug("pf::array") << "Error: identical equalities over, but hands don't match what we're proving."
736 // We have a "next node". Use it to guide us.
737 if (nodeAfterEqualitySequence
.getKind() == kind::NOT
) {
738 nodeAfterEqualitySequence
= nodeAfterEqualitySequence
[0];
741 Assert(nodeAfterEqualitySequence
.getKind() == kind::EQUAL
);
743 if ((n1
[0] == nodeAfterEqualitySequence
[0]) || (n1
[0] == nodeAfterEqualitySequence
[1])) {
746 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
747 n1
= eqNode(n1
[0], n1
[0]);
749 } else if ((n1
[1] == nodeAfterEqualitySequence
[0]) || (n1
[1] == nodeAfterEqualitySequence
[1])) {
752 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
753 n1
= eqNode(n1
[1], n1
[1]);
756 Debug("pf::array") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl
;
764 Debug("pf::array") << "Equality sequence length is odd!" << std::endl
;
768 Debug("pf::array") << "Have proven: " << n1
<< std::endl
;
773 // Ignore the redundancy.
778 if (identicalEqualities
) {
779 // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
780 identicalEqualities
= false;
783 Debug("mgd") << "\ndoing trans proof, got n2 " << n2
<< "\n";
785 Debug("mgdx") << "\ntrans proof[" << i
<< "], got n2 " << n2
<< "\n";
786 Debug("mgdx") << (n2
.getKind() == kind::EQUAL
) << "\n";
788 if ((n1
.getNumChildren() >= 2) && (n2
.getNumChildren() >= 2)) {
789 Debug("mgdx") << n1
[0].getId() << " " << n1
[1].getId() << " / " << n2
[0].getId() << " " << n2
[1].getId() << "\n";
790 Debug("mgdx") << n1
[0].getId() << " " << n1
[0] << "\n";
791 Debug("mgdx") << n1
[1].getId() << " " << n1
[1] << "\n";
792 Debug("mgdx") << n2
[0].getId() << " " << n2
[0] << "\n";
793 Debug("mgdx") << n2
[1].getId() << " " << n2
[1] << "\n";
794 Debug("mgdx") << (n1
[0] == n2
[0]) << "\n";
795 Debug("mgdx") << (n1
[1] == n2
[1]) << "\n";
796 Debug("mgdx") << (n1
[0] == n2
[1]) << "\n";
797 Debug("mgdx") << (n1
[1] == n2
[0]) << "\n";
801 // We can hadnle one of the equalities being negative, but not both
802 Assert((n1
.getKind() != kind::NOT
) || (n2
.getKind() != kind::NOT
));
807 if (n1
.getKind() == kind::NOT
) {
808 Debug("mgdx") << "n1 is negative" << std::endl
;
809 Debug("pf::array") << "n1 = " << n1
<< ", n2 = " << n2
<< std::endl
;
811 ss
<< "(negtrans1 _ _ _ _ ";
813 } else if (n2
.getKind() == kind::NOT
) {
814 Debug("mgdx") << "n2 is negative" << std::endl
;
815 Debug("pf::array") << "n1 = " << n1
<< ", n2 = " << n2
<< std::endl
;
817 ss
<< "(negtrans2 _ _ _ _ ";
820 ss
<< "(trans _ _ _ _ ";
823 if((n2
.getKind() == kind::EQUAL
) && (n1
.getKind() == kind::EQUAL
))
824 // Both elements of the transitivity rule are equalities/iffs
827 if(tb
== 1) { Debug("mgdx") << "case 1\n"; }
828 n1
= eqNode(n1
[1], n2
[1]);
829 ss
<< (firstNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1
.str() << ") " << ss2
.str();
830 } else if(n1
[1] == n2
[1]) {
831 if(tb
== 1) { Debug("mgdx") << "case 2\n"; }
832 n1
= eqNode(n1
[0], n2
[0]);
833 ss
<< ss1
.str() << (secondNeg
? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2
.str() << ")";
834 } else if(n1
[0] == n2
[1]) {
835 if(tb
== 1) { Debug("mgdx") << "case 3\n"; }
836 if(!firstNeg
&& !secondNeg
) {
837 n1
= eqNode(n2
[0], n1
[1]);
838 ss
<< ss2
.str() << " " << ss1
.str();
839 } else if (firstNeg
) {
840 n1
= eqNode(n1
[1], n2
[0]);
841 ss
<< " (negsymm _ _ _ " << ss1
.str() << ") (symm _ _ _ " << ss2
.str() << ")";
844 n1
= eqNode(n1
[1], n2
[0]);
845 ss
<< " (symm _ _ _ " << ss1
.str() << ") (negsymm _ _ _ " << ss2
.str() << ")";
847 if(tb
== 1) { Debug("mgdx") << "++ proved " << n1
<< "\n"; }
848 } else if(n1
[1] == n2
[0]) {
849 if(tb
== 1) { Debug("mgdx") << "case 4\n"; }
850 n1
= eqNode(n1
[0], n2
[1]);
851 ss
<< ss1
.str() << " " << ss2
.str();
853 Warning() << "\n\ntrans proof failure at step " << i
<< "\n\n";
854 Warning() << "0 proves " << n1
<< "\n";
855 Warning() << "1 proves " << n2
<< "\n\n";
856 pf
.debug_print("mgdx", 0, &proofPrinter
);
857 //toStreamRec(Warning.getStream(), pf, 0);
861 Debug("mgd") << "++ trans proof[" << i
<< "], now have " << n1
<< std::endl
;
862 } else if(n1
.getKind() == kind::EQUAL
) {
863 // n1 is an equality/iff, but n2 is a predicate
866 ss
<< (firstNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ")
867 << ss1
.str() << ") (pred_eq_t _ " << ss2
.str() << ")";
868 } else if(n1
[1] == n2
) {
870 ss
<< ss1
.str() << " (pred_eq_t _ " << ss2
.str() << ")";
874 } else if(n2
.getKind() == kind::EQUAL
) {
875 // n2 is an equality/iff, but n1 is a predicate
878 ss
<< (secondNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ")
879 << ss2
.str() << ") (pred_eq_t _ " << ss1
.str() << ")";
880 } else if(n2
[1] == n1
) {
882 ss
<< ss2
.str() << " (pred_eq_t _ " << ss1
.str() << ")";
887 // Both n1 and n2 are prediacates. Don't know what to do...
893 if (firstNeg
|| secondNeg
) {
894 n1
= (n1
.getKind() == kind::NOT
) ? n1
[0] : n1
.notNode();
899 Debug("mgd") << "\n++ trans proof done, have proven " << n1
<< std::endl
;
900 //return (firstNeg || secondNeg) ? n1.notNode() : n1;
904 else if (pf
.d_id
== d_reasonRow
) {
905 Debug("mgd") << "row lemma: " << pf
.d_node
<< std::endl
;
906 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
909 if (pf
.d_node
[1].getKind() == kind::SELECT
) {
910 // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k).
911 TNode t1
, t2
, t3
, t4
;
913 if(pf
.d_node
[1].getKind() == kind::SELECT
&&
914 pf
.d_node
[1][0].getKind() == kind::STORE
&&
915 pf
.d_node
[0].getKind() == kind::SELECT
&&
916 pf
.d_node
[0][0] == pf
.d_node
[1][0][0] &&
917 pf
.d_node
[0][1] == pf
.d_node
[1][1]) {
918 t2
= pf
.d_node
[1][0][1];
919 t3
= pf
.d_node
[1][1];
920 t1
= pf
.d_node
[0][0];
921 t4
= pf
.d_node
[1][0][2];
922 ret
= pf
.d_node
[1].eqNode(pf
.d_node
[0]);
923 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
925 Assert(pf
.d_node
[0].getKind() == kind::SELECT
&&
926 pf
.d_node
[0][0].getKind() == kind::STORE
&&
927 pf
.d_node
[1].getKind() == kind::SELECT
&&
928 pf
.d_node
[1][0] == pf
.d_node
[0][0][0] &&
929 pf
.d_node
[1][1] == pf
.d_node
[0][1]);
930 t2
= pf
.d_node
[0][0][1];
931 t3
= pf
.d_node
[0][1];
932 t1
= pf
.d_node
[1][0];
933 t4
= pf
.d_node
[0][0][2];
935 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
938 // inner index != outer index
939 // t3 is the outer index
941 Assert(pf
.d_children
.size() == 1);
942 std::stringstream ss
;
943 Node subproof
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
946 tp
->printTerm(t2
.toExpr(), out
, map
);
948 tp
->printTerm(t3
.toExpr(), out
, map
);
950 tp
->printTerm(t1
.toExpr(), out
, map
);
952 tp
->printTerm(t4
.toExpr(), out
, map
);
956 Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf
.d_children
[0]->d_node
957 << ". t3 is: " << t3
<< std::endl
958 << "subproof is: " << subproof
<< std::endl
;
960 Debug("pf::array") << "Subproof is: " << ss
.str() << std::endl
;
962 // The subproof needs to show that t2 != t3. This can either be a direct disequality,
963 // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant.
964 if (subproof
.getKind() == kind::NOT
) {
965 // The subproof is for t2 != t3 (or t3 != t2)
966 if (subproof
[0][1] == t3
) {
967 Debug("pf::array") << "Dont need symmetry!" << std::endl
;
970 Debug("pf::array") << "Need symmetry!" << std::endl
;
971 out
<< "(negsymm _ _ _ " << ss
.str() << ")";
974 // Either t2 or t3 is a constant.
975 Assert(subproof
.getKind() == kind::EQUAL
);
976 Assert(subproof
[0].isConst() || subproof
[1].isConst());
977 Assert(t2
.isConst() || t3
.isConst());
978 Assert(!(t2
.isConst() && t3
.isConst()));
980 bool t2IsConst
= t2
.isConst();
981 if (subproof
[0].isConst()) {
983 // (t3 == subproof[1]) == subproof[0] != t2
985 // subproof already shows constant = t3
986 Assert(t3
== subproof
[1]);
987 out
<< "(negtrans _ _ _ _ ";
988 tp
->printConstantDisequalityProof(out
, t2
.toExpr(), subproof
[0].toExpr(), map
);
993 Assert(t2
== subproof
[1]);
994 out
<< "(negsymm _ _ _ ";
995 out
<< "(negtrans _ _ _ _ ";
996 tp
->printConstantDisequalityProof(out
, t3
.toExpr(), subproof
[0].toExpr(), map
);
1003 // (t3 == subproof[0]) == subproof[1] != t2
1005 // subproof already shows constant = t3
1006 Assert(t3
== subproof
[0]);
1007 out
<< "(negtrans _ _ _ _ ";
1008 tp
->printConstantDisequalityProof(out
, t2
.toExpr(), subproof
[1].toExpr(), map
);
1010 out
<< "(symm _ _ _ " << ss
.str() << ")";
1013 Assert(t2
== subproof
[0]);
1014 out
<< "(negsymm _ _ _ ";
1015 out
<< "(negtrans _ _ _ _ ";
1016 tp
->printConstantDisequalityProof(out
, t3
.toExpr(), subproof
[1].toExpr(), map
);
1018 out
<< "(symm _ _ _ " << ss
.str() << ")";
1027 Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl
;
1029 Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf
.d_children
[0]->d_node
<< std::endl
;
1031 // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k])
1033 // If we wanted to remove the need for "negativerow", we would need to prove i==k using a new satlem. We would:
1034 // 1. Create a new satlem.
1035 // 2. Assume that i != k
1036 // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k])
1037 // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), obtaining our contradiction
1039 TNode t1
, t2
, t3
, t4
;
1042 // pf.d_node is an equality, i==k.
1046 // pf.d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
1047 // or its symmetrical version.
1050 if (pf
.d_children
[0]->d_node
[0][0].getKind() == kind::SELECT
&&
1051 pf
.d_children
[0]->d_node
[0][0][0].getKind() == kind::STORE
) {
1053 } else if (pf
.d_children
[0]->d_node
[0][1].getKind() == kind::SELECT
&&
1054 pf
.d_children
[0]->d_node
[0][1][0].getKind() == kind::STORE
) {
1061 Debug("pf::array") << "Side is: " << side
<< std::endl
;
1063 // The array's index and element types will come from the subproof...
1064 t3
= pf
.d_children
[0]->d_node
[0][side
][0][0];
1065 t4
= pf
.d_children
[0]->d_node
[0][side
][0][2];
1068 // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
1069 bool swap
= (t2
== pf
.d_children
[0]->d_node
[0][side
][0][1]);
1071 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
1073 Assert(pf
.d_children
.size() == 1);
1074 std::stringstream ss
;
1075 Node subproof
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
1077 Debug("pf::array") << "Subproof is: " << ss
.str() << std::endl
;
1080 out
<< "(symm _ _ _ ";
1083 out
<< "(negativerow _ _ ";
1084 tp
->printTerm(swap
? t2
.toExpr() : t1
.toExpr(), out
, map
);
1086 tp
->printTerm(swap
? t1
.toExpr() : t2
.toExpr(), out
, map
);
1088 tp
->printTerm(t3
.toExpr(), out
, map
);
1090 tp
->printTerm(t4
.toExpr(), out
, map
);
1094 out
<< "(negsymm _ _ _ " << ss
.str() << ")";
1109 else if (pf
.d_id
== d_reasonRow1
) {
1110 Debug("mgd") << "row1 lemma: " << pf
.d_node
<< std::endl
;
1111 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
1114 if(pf
.d_node
[1].getKind() == kind::SELECT
&&
1115 pf
.d_node
[1][0].getKind() == kind::STORE
&&
1116 pf
.d_node
[1][0][1] == pf
.d_node
[1][1] &&
1117 pf
.d_node
[1][0][2] == pf
.d_node
[0]) {
1118 t1
= pf
.d_node
[1][0][0];
1119 t2
= pf
.d_node
[1][0][1];
1121 ret
= pf
.d_node
[1].eqNode(pf
.d_node
[0]);
1122 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1124 Assert(pf
.d_node
[0].getKind() == kind::SELECT
&&
1125 pf
.d_node
[0][0].getKind() == kind::STORE
&&
1126 pf
.d_node
[0][0][1] == pf
.d_node
[0][1] &&
1127 pf
.d_node
[0][0][2] == pf
.d_node
[1]);
1128 t1
= pf
.d_node
[0][0][0];
1129 t2
= pf
.d_node
[0][0][1];
1132 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1134 out
<< "(row1 _ _ ";
1135 tp
->printTerm(t1
.toExpr(), out
, map
);
1137 tp
->printTerm(t2
.toExpr(), out
, map
);
1139 tp
->printTerm(t3
.toExpr(), out
, map
);
1144 else if (pf
.d_id
== d_reasonExt
) {
1145 Assert(pf
.d_node
.getKind() == kind::NOT
);
1146 Assert(pf
.d_node
[0].getKind() == kind::EQUAL
);
1147 Assert(pf
.d_children
.size() == 1);
1148 std::shared_ptr
<theory::eq::EqProof
> child_proof
= pf
.d_children
[0];
1149 Assert(child_proof
->d_node
.getKind() == kind::NOT
);
1150 Assert(child_proof
->d_node
[0].getKind() == kind::EQUAL
);
1152 Debug("mgd") << "EXT lemma: " << pf
.d_node
<< std::endl
;
1155 t1
= child_proof
->d_node
[0][0];
1156 t2
= child_proof
->d_node
[0][1];
1157 t3
= pf
.d_node
[0][0][1];
1159 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1161 out
<< "(or_elim_1 _ _ ";
1162 out
<< ProofManager::getLitName(child_proof
->d_node
[0]);
1164 out
<< ProofManager::getArrayProof()->skolemToLiteral(t3
.toExpr());
1171 Assert(!pf
.d_node
.isNull());
1172 Assert(pf
.d_children
.empty());
1173 Debug("mgd") << "theory proof: " << pf
.d_node
<< " by rule " << int(pf
.d_id
) << std::endl
;
1174 AlwaysAssert(false);
1179 ArrayProof::ArrayProof(theory::arrays::TheoryArrays
* arrays
, TheoryProofEngine
* pe
)
1180 : TheoryProof(arrays
, pe
)
1183 void ArrayProof::registerTerm(Expr term
) {
1184 // already registered
1185 if (d_declarations
.find(term
) != d_declarations
.end())
1188 Type type
= term
.getType();
1189 if (type
.isSort()) {
1190 // declare uninterpreted sorts
1191 d_sorts
.insert(type
);
1194 if (term
.getKind() == kind::APPLY_UF
) {
1195 Expr function
= term
.getOperator();
1196 d_declarations
.insert(function
);
1199 if (term
.isVariable()) {
1200 d_declarations
.insert(term
);
1203 if (term
.getKind() == kind::SELECT
&& term
.getType().isBoolean()) {
1204 // Ensure cnf literals
1206 ProofManager::currentPM()->ensureLiteral(eqNode(term
, NodeManager::currentNM()->mkConst(true)));
1207 ProofManager::currentPM()->ensureLiteral(eqNode(term
, NodeManager::currentNM()->mkConst(false)));
1210 // recursively declare all other terms
1211 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
1212 // could belong to other theories
1213 d_proofEngine
->registerTerm(term
[i
]);
1217 std::string
ArrayProof::skolemToLiteral(Expr skolem
) {
1218 Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem
<< ")" << std::endl
;
1219 Assert(d_skolemToLiteral
.find(skolem
) != d_skolemToLiteral
.end());
1220 return d_skolemToLiteral
[skolem
];
1223 void LFSCArrayProof::printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
1224 Assert (theory::Theory::theoryOf(term
) == theory::THEORY_ARRAY
);
1226 if (theory::Theory::theoryOf(term
) != theory::THEORY_ARRAY
) {
1227 // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
1228 // hiding as a subterm of an array term. In that case, send it back to the dispatcher.
1229 d_proofEngine
->printBoundTerm(term
, os
, map
);
1233 if (term
.getKind() == kind::VARIABLE
|| term
.getKind() == kind::SKOLEM
) {
1238 Assert ((term
.getKind() == kind::SELECT
) || (term
.getKind() == kind::PARTIAL_SELECT_0
) || (term
.getKind() == kind::PARTIAL_SELECT_1
) || (term
.getKind() == kind::STORE
));
1240 switch (term
.getKind()) {
1241 case kind::SELECT
: {
1242 Assert(term
.getNumChildren() == 2);
1244 bool convertToBool
= (term
[1].getType().isBoolean() && !d_proofEngine
->printsAsBool(term
[1]));
1246 os
<< "(apply _ _ (apply _ _ (read ";
1247 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1249 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1251 printTerm(term
[0], os
, map
);
1253 if (convertToBool
) os
<< "(f_to_b ";
1254 printTerm(term
[1], os
, map
);
1255 if (convertToBool
) os
<< ")";
1260 case kind::PARTIAL_SELECT_0
:
1261 Assert(term
.getNumChildren() == 1);
1263 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1265 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1269 case kind::PARTIAL_SELECT_1
:
1270 Debug("pf::array") << "This branch has not beed tested yet." << std::endl
;
1273 Assert(term
.getNumChildren() == 1);
1274 os
<< "(apply _ _ (read ";
1275 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1277 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1279 printTerm(term
[0], os
, map
);
1284 os
<< "(apply _ _ (apply _ _ (apply _ _ (write ";
1285 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1287 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1289 printTerm(term
[0], os
, map
);
1291 printTerm(term
[1], os
, map
);
1293 printTerm(term
[2], os
, map
);
1303 void LFSCArrayProof::printOwnedSort(Type type
, std::ostream
& os
) {
1304 Debug("pf::array") << std::endl
<< "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type
<< std::endl
;
1305 Assert (type
.isArray() || type
.isSort());
1306 if (type
.isArray()){
1307 ArrayType
array_type(type
);
1309 Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: "
1310 << array_type
.getIndexType()
1311 << ", element type: " << array_type
.getConstituentType() << std::endl
;
1314 printSort(array_type
.getIndexType(), os
);
1316 printSort(array_type
.getConstituentType(), os
);
1323 void LFSCArrayProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
) {
1324 os
<< " ;; Array Theory Lemma \n;;";
1325 for (unsigned i
= 0; i
< lemma
.size(); ++i
) {
1326 os
<< lemma
[i
] <<" ";
1329 //os << " (clausify_false trust)";
1330 ArrayProof::printTheoryLemmaProof(lemma
, os
, paren
, map
);
1333 void LFSCArrayProof::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1334 // declaring the sorts
1335 for (TypeSet::const_iterator it
= d_sorts
.begin(); it
!= d_sorts
.end(); ++it
) {
1336 if (!ProofManager::currentPM()->wasPrinted(*it
)) {
1337 os
<< "(% " << *it
<< " sort\n";
1339 ProofManager::currentPM()->markPrinted(*it
);
1344 void LFSCArrayProof::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1345 Debug("pf::array") << "Arrays declaring terms..." << std::endl
;
1347 for (ExprSet::const_iterator it
= d_declarations
.begin(); it
!= d_declarations
.end(); ++it
) {
1350 Assert(term
.getType().isArray() || term
.isVariable());
1352 Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is: " << term
1353 << ". It's type is: " << term
.getType()
1356 if (term
.getType().isArray()){
1357 ArrayType
array_type(term
.getType());
1359 Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is an array. Index type: "
1360 << array_type
.getIndexType()
1361 << ", element type: " << array_type
.getConstituentType() << std::endl
;
1363 os
<< "(% " << ProofManager::sanitize(term
) << " ";
1367 printSort(array_type
.getIndexType(), os
);
1369 printSort(array_type
.getConstituentType(), os
);
1374 Assert(term
.isVariable());
1375 if (ProofManager::getSkolemizationManager()->isSkolem(*it
)) {
1376 Debug("pf::array") << "This term is a skoelm!" << std::endl
;
1377 d_skolemDeclarations
.insert(*it
);
1379 os
<< "(% " << ProofManager::sanitize(term
) << " ";
1381 os
<< term
.getType() << ")\n";
1387 Debug("pf::array") << "Declaring terms done!" << std::endl
;
1390 void LFSCArrayProof::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1391 Debug("pf::array") << "Array: print deferred declarations called" << std::endl
;
1394 for (ExprSet::const_iterator it
= d_skolemDeclarations
.begin(); it
!= d_skolemDeclarations
.end(); ++it
) {
1396 Node equality
= ProofManager::getSkolemizationManager()->getDisequality(*it
);
1398 Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: term is: " << *it
<< std::endl
1399 << "It is a witness for: " << equality
<< std::endl
;
1401 std::ostringstream newSkolemLiteral
;
1402 newSkolemLiteral
<< ".sl" << count
++;
1403 std::string skolemLiteral
= newSkolemLiteral
.str();
1405 d_skolemToLiteral
[*it
] = skolemLiteral
;
1407 Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: new skolem literal is: " << skolemLiteral
<< std::endl
;
1409 Assert(equality
.getKind() == kind::NOT
);
1410 Assert(equality
[0].getKind() == kind::EQUAL
);
1412 Node array_one
= equality
[0][0];
1413 Node array_two
= equality
[0][1];
1417 printTerm(array_one
.toExpr(), os
, map
);
1419 printTerm(array_two
.toExpr(), os
, map
);
1421 os
<< ProofManager::sanitize(*it
);
1423 os
<< skolemLiteral
.c_str();
1430 void LFSCArrayProof::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
1431 // Nothing to do here at this point.
1434 bool LFSCArrayProof::printsAsBool(const Node
&n
)
1436 if (n
.getKind() == kind::SELECT
)
1442 } /* CVC4 namespace */