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
,
122 : d_proof(pf
), d_reasonRow(row
), d_reasonRow1(row1
), d_reasonExt(ext
)
126 void ProofArray::toStream(std::ostream
& out
) const
132 void ProofArray::toStream(std::ostream
& out
, const ProofLetMap
& map
) const
134 Trace("pf::array") << "; Print Array proof..." << std::endl
;
135 toStreamLFSC(out
, ProofManager::getArrayProof(), *d_proof
, map
);
136 Debug("pf::array") << "; Print Array proof done!" << std::endl
;
139 void ProofArray::toStreamLFSC(std::ostream
& out
,
141 const theory::eq::EqProof
& pf
,
142 const ProofLetMap
& map
) const
144 Debug("pf::array") << "Printing array proof in LFSC : " << std::endl
;
145 ArrayProofPrinter
proofPrinter(d_reasonRow
, d_reasonRow1
, d_reasonExt
);
146 pf
.debug_print("pf::array", 0, &proofPrinter
);
147 Debug("pf::array") << std::endl
;
148 toStreamRecLFSC(out
, tp
, pf
, 0, map
);
149 Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl
;
152 Node
ProofArray::toStreamRecLFSC(std::ostream
& out
,
154 const theory::eq::EqProof
& pf
,
156 const ProofLetMap
& map
) const
158 Debug("pf::array") << std::endl
160 << "toStreamRecLFSC called. tb = " << tb
161 << " . proof:" << std::endl
;
162 ArrayProofPrinter
proofPrinter(d_reasonRow
, d_reasonRow1
, d_reasonExt
);
163 pf
.debug_print("pf::array", 0, &proofPrinter
);
164 Debug("pf::array") << std::endl
;
167 Assert(pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
);
168 Assert(!pf
.d_node
.isNull());
169 Assert(pf
.d_children
.size() >= 2);
172 std::shared_ptr
<theory::eq::EqProof
> subTrans
=
173 std::make_shared
<theory::eq::EqProof
>();
174 subTrans
->d_id
= theory::eq::MERGED_THROUGH_TRANS
;
175 subTrans
->d_node
= pf
.d_node
;
178 while (i
< pf
.d_children
.size()) {
179 if (pf
.d_children
[i
]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
)
180 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
182 // Look for the negative clause, with which we will form a contradiction.
183 if(!pf
.d_children
[i
]->d_node
.isNull() && pf
.d_children
[i
]->d_node
.getKind() == kind::NOT
) {
189 // Handle congruence closures over equalities.
190 else if (pf
.d_children
[i
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&& pf
.d_children
[i
]->d_node
.isNull()) {
191 Debug("pf::array") << "Handling congruence over equalities" << std::endl
;
193 // Gather the sequence of consecutive congruence closures.
194 std::vector
<std::shared_ptr
<const theory::eq::EqProof
>> congruenceClosures
;
196 Debug("pf::array") << "Collecting congruence sequence" << std::endl
;
198 i
+ count
< pf
.d_children
.size() &&
199 pf
.d_children
[i
+ count
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&&
200 pf
.d_children
[i
+ count
]->d_node
.isNull();
202 Debug("pf::array") << "Found a congruence: " << std::endl
;
203 pf
.d_children
[i
+ count
]->debug_print("pf::array", 0, &proofPrinter
);
204 congruenceClosures
.push_back(pf
.d_children
[i
+ count
]);
207 Debug("pf::array") << "Total number of congruences found: " << congruenceClosures
.size() << std::endl
;
209 // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
210 bool targetAppearsBefore
= true;
211 bool targetAppearsAfter
= true;
213 if ((i
== 0) || (i
== 1 && neg
== 0)) {
214 Debug("pf::array") << "Target does not appear before" << std::endl
;
215 targetAppearsBefore
= false;
218 if ((i
+ count
>= pf
.d_children
.size()) ||
219 (!pf
.d_children
[i
+ count
]->d_node
.isNull() &&
220 pf
.d_children
[i
+ count
]->d_node
.getKind() == kind::NOT
)) {
221 Debug("pf::array") << "Target does not appear after" << std::endl
;
222 targetAppearsAfter
= false;
225 // Assert that we have precisely one target clause.
226 Assert(targetAppearsBefore
!= targetAppearsAfter
);
228 // Begin breaking up the congruences and ordering the equalities correctly.
229 std::vector
<std::shared_ptr
<theory::eq::EqProof
>> orderedEqualities
;
231 // Insert target clause first.
232 if (targetAppearsBefore
) {
233 orderedEqualities
.push_back(pf
.d_children
[i
- 1]);
234 // The target has already been added to subTrans; remove it.
235 subTrans
->d_children
.pop_back();
237 orderedEqualities
.push_back(pf
.d_children
[i
+ count
]);
240 // Start with the congruence closure closest to the target clause, and work our way back/forward.
241 if (targetAppearsBefore
) {
242 for (unsigned j
= 0; j
< count
; ++j
) {
243 if (pf
.d_children
[i
+ j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
244 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ j
]->d_children
[0]);
245 if (pf
.d_children
[i
+ j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
246 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ j
]->d_children
[1]);
249 for (unsigned j
= 0; j
< count
; ++j
) {
250 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
251 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]);
252 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
253 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]);
257 // Copy the result into the main transitivity proof.
258 subTrans
->d_children
.insert(subTrans
->d_children
.end(), orderedEqualities
.begin(), orderedEqualities
.end());
260 // Increase i to skip over the children that have been processed.
262 if (targetAppearsAfter
) {
267 // Else, just copy the child proof as is
269 subTrans
->d_children
.push_back(pf
.d_children
[i
]);
274 bool disequalityFound
= (neg
>= 0);
275 if (!disequalityFound
) {
276 Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl
;
277 Debug("pf::array") << "Proof for: " << pf
.d_node
<< std::endl
;
278 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
279 Assert(pf
.d_node
.getNumChildren() == 2);
280 Assert (pf
.d_node
[0].isConst() && pf
.d_node
[1].isConst());
284 std::stringstream ss
, ss2
;
285 //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
286 Debug("mgdx") << "\nsubtrans has " << subTrans
->d_children
.size() << " children\n";
287 if(!disequalityFound
|| pf
.d_children
.size() > 2) {
288 n1
= toStreamRecLFSC(ss
, tp
, *subTrans
, 1, map
);
290 n1
= toStreamRecLFSC(ss
, tp
, *(subTrans
->d_children
[0]), 1, map
);
291 Debug("mgdx") << "\nsubTrans unique child "
292 << subTrans
->d_children
[0]->d_id
293 << " was proven\ngot: " << n1
<< std::endl
;
296 out
<< "(clausify_false (contra _ ";
298 if (disequalityFound
) {
299 Node n2
= pf
.d_children
[neg
]->d_node
;
300 Assert(n2
.getKind() == kind::NOT
);
301 Debug("mgdx") << "\nhave proven: " << n1
<< std::endl
;
302 Debug("mgdx") << "n2 is " << n2
<< std::endl
;
303 Debug("mgdx") << "n2->d_id is " << pf
.d_children
[neg
]->d_id
<< std::endl
;
304 Debug("mgdx") << "n2[0] is " << n2
[0] << std::endl
;
306 if (n2
[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2
[0][0] << std::endl
; }
307 if (n1
.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1
[1] << std::endl
; }
309 if ((pf
.d_children
[neg
]->d_id
== d_reasonExt
) ||
310 (pf
.d_children
[neg
]->d_id
== theory::eq::MERGED_THROUGH_TRANS
)) {
311 // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
314 toStreamRecLFSC(ss2
, tp
, *pf
.d_children
[neg
], 1, map
);
316 } else if (n2
[0].getKind() == kind::APPLY_UF
) {
317 out
<< "(trans _ _ _ _ ";
318 out
<< "(symm _ _ _ ";
320 out
<< ") (pred_eq_f _ " << ProofManager::getLitName(n2
[0]) << ")) t_t_neq_f))" << std::endl
;
322 Assert((n1
[0] == n2
[0][0] && n1
[1] == n2
[0][1]) || (n1
[1] == n2
[0][0] && n1
[0] == n2
[0][1]));
323 if(n1
[1] == n2
[0][0]) {
324 out
<< "(symm _ _ _ " << ss
.str() << ")";
328 Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2
[0] << " ) = " <<
329 ProofManager::getLitName(n2
[0]) << std::endl
;
331 out
<< " " << ProofManager::getLitName(n2
[0]);
335 Assert(n2
.getKind() == kind::EQUAL
);
336 Assert((n1
[0] == n2
[0] && n1
[1] == n2
[1]) || (n1
[1] == n2
[0] && n1
[0] == n2
[1]));
340 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out
,
346 out
<< "))" << std::endl
;
350 if (pf
.d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
) {
351 Debug("mgd") << "\nok, looking at congruence:\n";
352 pf
.debug_print("mgd", 0, &proofPrinter
);
353 std::stack
<const theory::eq::EqProof
*> stk
;
354 for (const theory::eq::EqProof
* pf2
= &pf
;
355 pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
;
356 pf2
= pf2
->d_children
[0].get()) {
357 Debug("mgd") << "Looking at pf2 with d_node: " << pf2
->d_node
359 Assert(!pf2
->d_node
.isNull());
360 Assert(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
||
361 pf2
->d_node
.getKind() == kind::BUILTIN
||
362 pf2
->d_node
.getKind() == kind::APPLY_UF
||
363 pf2
->d_node
.getKind() == kind::SELECT
||
364 pf2
->d_node
.getKind() == kind::PARTIAL_SELECT_0
||
365 pf2
->d_node
.getKind() == kind::PARTIAL_SELECT_1
||
366 pf2
->d_node
.getKind() == kind::STORE
);
368 Assert(pf2
->d_children
.size() == 2);
369 out
<< "(cong _ _ _ _ _ _ ";
372 Assert(stk
.top()->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
);
373 // NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
374 NodeBuilder
<> b1
, b2
;
376 const theory::eq::EqProof
* pf2
= stk
.top();
378 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
379 Node n1
= toStreamRecLFSC(out
, tp
, *(pf2
->d_children
[0]), tb
+ 1, map
);
381 std::stringstream ss
;
382 Node n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
385 Debug("mgd") << "\nok, in FIRST cong[" << stk
.size() << "]" << "\n";
386 pf2
->debug_print("mgd", 0, &proofPrinter
);
388 Debug("mgd") << "n1 is a proof for: " << pf2
->d_children
[0]->d_node
<< ". It is: " << n1
<< std::endl
;
389 Debug("mgd") << "n2 is a proof for: " << pf2
->d_children
[1]->d_node
<< ". It is: " << n2
<< std::endl
;
391 Debug("mgd") << "looking at " << pf2
->d_node
<< "\n";
392 Debug("mgd") << " " << n1
<< "\n";
393 Debug("mgd") << " " << n2
<< "\n";
396 if(match(pf2
->d_node
, n1
[0])) {
397 Debug("mgd") << "SIDE IS 0\n";
400 Debug("mgd") << "SIDE IS 1\n";
401 if(!match(pf2
->d_node
, n1
[1])) {
402 Debug("mgd") << "IN BAD CASE, our first subproof is\n";
403 pf2
->d_children
[0]->debug_print("mgd", 0, &proofPrinter
);
405 Assert(match(pf2
->d_node
, n1
[1]));
409 if(n1
[side
].getKind() == kind::APPLY_UF
||
410 n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
||
411 n1
[side
].getKind() == kind::SELECT
||
412 n1
[side
].getKind() == kind::PARTIAL_SELECT_1
||
413 n1
[side
].getKind() == kind::STORE
) {
414 if(n1
[side
].getKind() == kind::APPLY_UF
|| n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
) {
415 b1
<< kind::PARTIAL_APPLY_UF
;
416 b1
<< n1
[side
].getOperator();
417 } else if (n1
[side
].getKind() == kind::SELECT
|| n1
[side
].getKind() == kind::PARTIAL_SELECT_1
) {
418 // b1 << n1[side].getKind();
421 b1
<< kind::PARTIAL_APPLY_UF
;
422 b1
<< ProofManager::currentPM()->mkOp(n1
[side
].getOperator());
424 b1
.append(n1
[side
].begin(), n1
[side
].end());
426 else if (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
) {
427 b1
<< kind::PARTIAL_SELECT_1
;
432 if(n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
||
433 n1
[1-side
].getKind() == kind::APPLY_UF
||
434 n1
[1-side
].getKind() == kind::SELECT
||
435 n1
[1-side
].getKind() == kind::PARTIAL_SELECT_1
||
436 n1
[1-side
].getKind() == kind::STORE
) {
437 if(n1
[1-side
].getKind() == kind::APPLY_UF
||
438 n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
) {
439 b2
<< kind::PARTIAL_APPLY_UF
;
440 b2
<< n1
[1-side
].getOperator();
441 } else if (n1
[1-side
].getKind() == kind::SELECT
|| n1
[1-side
].getKind() == kind::PARTIAL_SELECT_1
) {
442 // b2 << n1[1-side].getKind();
445 b2
<< kind::PARTIAL_APPLY_UF
;
446 b2
<< ProofManager::currentPM()->mkOp(n1
[1-side
].getOperator());
448 b2
.append(n1
[1-side
].begin(), n1
[1-side
].end());
449 } else if (n1
[1-side
].getKind() == kind::PARTIAL_SELECT_0
) {
450 b2
<< kind::PARTIAL_SELECT_1
;
454 Debug("mgd") << "pf2->d_node " << pf2
->d_node
<< std::endl
;
455 Debug("mgd") << "b1.getNumChildren() " << b1
.getNumChildren() << std::endl
;
456 Debug("mgd") << "n1 " << n1
<< std::endl
;
457 Debug("mgd") << "n2 " << n2
<< std::endl
;
458 // These debug prints can cause a problem if we're constructing a SELECT node and it doesn't have enough
460 // Debug("mgd") << "b1 " << b1 << std::endl;
461 // Debug("mgd") << "b2 " << b2 << std::endl;
462 Debug("mgd") << "side " << side
<< std::endl
;
463 Debug("mgd") << "pf2->d_node's number of children: " << pf2
->d_node
.getNumChildren() << std::endl
;
464 Debug("mgd") << "pf2->d_node's meta kind: " << pf2
->d_node
.getMetaKind() << std::endl
;
465 Debug("mgd") << "Is this meta kind considered parameterized? " << (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
) << std::endl
;
467 if(pf2
->d_node
[b1
.getNumChildren() +
468 (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
? 1 : 0) +
469 (n1
[side
].getKind() == kind::PARTIAL_SELECT_1
? 1 : 0) -
470 (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[side
]) {
475 Assert(pf2
->d_node
[b1
.getNumChildren() +
476 (n1
[side
].getKind() == kind::PARTIAL_SELECT_0
? 1 : 0) +
477 (n1
[side
].getKind() == kind::PARTIAL_SELECT_1
? 1 : 0) -
478 (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[1-side
]);
481 out
<< "(symm _ _ _ " << ss
.str() << ")";
484 Debug("mgd") << "After first insertion:" << std::endl
;
485 Debug("mgd") << "b1 " << b1
<< std::endl
;
486 Debug("mgd") << "b2 " << b2
<< std::endl
;
489 while(!stk
.empty()) {
491 Debug("mgd") << "\nMORE TO DO\n";
495 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
498 n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
500 Debug("mgd") << "\nok, in cong[" << stk
.size() << "]" << "\n";
501 Debug("mgd") << "looking at " << pf2
->d_node
<< "\n";
502 Debug("mgd") << " " << n1
<< "\n";
503 Debug("mgd") << " " << n2
<< "\n";
504 Debug("mgd") << " " << b1
<< "\n";
505 Debug("mgd") << " " << b2
<< "\n";
506 if(pf2
->d_node
[b1
.getNumChildren()] == n2
[side
]) {
511 Assert(pf2
->d_node
[b1
.getNumChildren()] == n2
[1-side
]);
514 out
<< "(symm _ _ _ " << ss
.str() << ")";
521 Debug("mgd") << "at end assert!" << std::endl
522 << "pf2->d_node = " << pf2
->d_node
<< std::endl
523 << "n1 (assigned from b1) = " << n1
<< std::endl
524 << "n2 (assigned from b2) = " << n2
<< std::endl
;
526 if(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
) {
527 Assert(n1
== pf2
->d_node
);
530 Debug("mgd") << "n1.getOperator().getType().getNumChildren() = "
531 << n1
.getOperator().getType().getNumChildren() << std::endl
;
532 Debug("mgd") << "n1.getNumChildren() + 1 = "
533 << n1
.getNumChildren() + 1 << std::endl
;
535 Assert(!((n1
.getKind() == kind::PARTIAL_SELECT_0
&& n1
.getNumChildren() == 2)));
536 if (n1
.getKind() == kind::PARTIAL_SELECT_1
&& n1
.getNumChildren() == 2) {
537 Debug("mgd") << "Finished a SELECT. Updating.." << std::endl
;
538 b1
.clear(kind::SELECT
);
539 b1
.append(n1
.begin(), n1
.end());
541 Debug("mgd") << "New n1: " << n1
<< std::endl
;
542 // } else if (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 1) {
543 // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
544 // b1.clear(kind::PARTIAL_SELECT_1);
545 // b1.append(n1.begin(), n1.end());
547 // Debug("mgd") << "New n1: " << n1 << std::endl;
549 } else if(n1
.getOperator().getType().getNumChildren() == n1
.getNumChildren() + 1) {
550 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
551 b1
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
553 b1
.clear(kind::APPLY_UF
);
554 b1
<< n1
.getOperator();
556 b1
.append(n1
.begin(), n1
.end());
558 Debug("mgd") << "at[2] end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
559 if(pf2
->d_node
.getKind() == kind::APPLY_UF
) {
560 Assert(n1
== pf2
->d_node
);
564 Debug("mgd") << "n2.getOperator().getType().getNumChildren() = "
565 << n2
.getOperator().getType().getNumChildren() << std::endl
;
566 Debug("mgd") << "n2.getNumChildren() + 1 = "
567 << n2
.getNumChildren() + 1 << std::endl
;
569 Assert(!((n2
.getKind() == kind::PARTIAL_SELECT_0
&& n2
.getNumChildren() == 2)));
570 if (n2
.getKind() == kind::PARTIAL_SELECT_1
&& n2
.getNumChildren() == 2) {
571 Debug("mgd") << "Finished a SELECT. Updating.." << std::endl
;
572 b2
.clear(kind::SELECT
);
573 b2
.append(n2
.begin(), n2
.end());
575 Debug("mgd") << "New n2: " << n2
<< std::endl
;
576 // } else if (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 1) {
577 // Debug("mgd") << "Finished a PARTIAL_SELECT_1. Updating.." << std::endl;
578 // b2.clear(kind::PARTIAL_SELECT_1);
579 // b2.append(n2.begin(), n2.end());
581 // Debug("mgd") << "New n2: " << n2 << std::endl;
583 } else if(n2
.getOperator().getType().getNumChildren() == n2
.getNumChildren() + 1) {
584 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
585 b2
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
587 b2
.clear(kind::APPLY_UF
);
588 b2
<< n2
.getOperator();
590 b2
.append(n2
.begin(), n2
.end());
593 Node n
= (side
== 0 ? eqNode(n1
, n2
) : eqNode(n2
, n1
));
595 Debug("mgdx") << "\ncong proved: " << n
<< "\n";
599 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_REFLEXIVITY
) {
600 Assert(!pf
.d_node
.isNull());
601 Assert(pf
.d_children
.empty());
603 tp
->printTerm(NodeManager::currentNM()->toExpr(pf
.d_node
), out
, map
);
605 return eqNode(pf
.d_node
, pf
.d_node
);
608 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_EQUALITY
) {
609 Assert(!pf
.d_node
.isNull());
610 Assert(pf
.d_children
.empty());
611 Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf
.d_node
.negate() << " ) = " <<
612 ProofManager::getLitName(pf
.d_node
.negate()) << std::endl
;
613 out
<< ProofManager::getLitName(pf
.d_node
.negate());
617 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_CONSTANTS
) {
618 Debug("pf::array") << "Proof for: " << pf
.d_node
<< std::endl
;
619 Assert(pf
.d_node
.getKind() == kind::NOT
);
620 Node n
= pf
.d_node
[0];
621 Assert(n
.getKind() == kind::EQUAL
);
622 Assert(n
.getNumChildren() == 2);
623 Assert(n
[0].isConst() && n
[1].isConst());
625 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out
,
632 else if (pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
) {
633 bool firstNeg
= false;
634 bool secondNeg
= false;
636 Assert(!pf
.d_node
.isNull());
637 Assert(pf
.d_children
.size() >= 2);
638 std::stringstream ss
;
639 Debug("mgd") << "\ndoing trans proof[[\n";
640 pf
.debug_print("mgd", 0, &proofPrinter
);
641 Debug("mgd") << "\n";
643 pf
.d_children
[0]->d_node
= simplifyBooleanNode(pf
.d_children
[0]->d_node
);
645 Node n1
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
646 Debug("mgd") << "\ndoing trans proof, got n1 " << n1
<< "\n";
648 Debug("mgdx") << "\ntrans proof[0], got n1 " << n1
<< "\n";
651 bool identicalEqualities
= false;
652 bool evenLengthSequence
;
653 Node nodeAfterEqualitySequence
;
655 std::map
<size_t, Node
> childToStream
;
657 for(size_t i
= 1; i
< pf
.d_children
.size(); ++i
) {
658 std::stringstream
ss1(ss
.str()), ss2
;
661 // In congruences, we can have something like a[x] - it's important to keep these,
662 // and not turn them into (a[x]=true), because that will mess up the congruence application
665 if (pf
.d_children
[i
]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
)
666 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
668 // It is possible that we've already converted the i'th child to stream. If so,
669 // use previously stored result. Otherwise, convert and store.
671 if (childToStream
.find(i
) != childToStream
.end())
672 n2
= childToStream
[i
];
674 n2
= toStreamRecLFSC(ss2
, tp
, *(pf
.d_children
[i
]), tb
+ 1, map
);
675 childToStream
[i
] = n2
;
678 Debug("mgd") << "\ndoing trans proof, got (first) n2 " << n2
<< "\n";
680 // The following branch is dedicated to handling sequences of identical equalities,
681 // i.e. trans[ a=b, a=b, a=b ].
683 // There are two cases:
684 // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
686 // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
687 // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
688 // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
689 // and use it to determine which option we need.
691 if(n2
.getKind() == kind::EQUAL
) {
692 if (((n1
[0] == n2
[0]) && (n1
[1] == n2
[1])) || ((n1
[0] == n2
[1]) && (n1
[1] == n2
[0]))) {
693 // We are in a sequence of identical equalities
695 Debug("pf::array") << "Detected identical equalities: " << std::endl
<< "\t" << n1
<< std::endl
;
697 if (!identicalEqualities
) {
698 // The sequence of identical equalities has started just now
699 identicalEqualities
= true;
701 Debug("pf::array") << "The sequence is just beginning. Determining length..." << std::endl
;
703 // Determine whether the length of this sequence is odd or even.
704 evenLengthSequence
= true;
705 bool sequenceOver
= false;
708 while (j
< pf
.d_children
.size() && !sequenceOver
) {
709 std::stringstream dontCare
;
710 nodeAfterEqualitySequence
= toStreamRecLFSC(dontCare
, tp
, *(pf
.d_children
[j
]), tb
+ 1, map
);
712 if (((nodeAfterEqualitySequence
[0] == n1
[0]) && (nodeAfterEqualitySequence
[1] == n1
[1])) ||
713 ((nodeAfterEqualitySequence
[0] == n1
[1]) && (nodeAfterEqualitySequence
[1] == n1
[0]))) {
714 evenLengthSequence
= !evenLengthSequence
;
722 if (evenLengthSequence
) {
723 // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
725 Debug("pf::array") << "Equality sequence of even length" << std::endl
;
726 Debug("pf::array") << "n1 is: " << n1
<< std::endl
;
727 Debug("pf::array") << "n2 is: " << n2
<< std::endl
;
728 Debug("pf::array") << "pf-d_node is: " << pf
.d_node
<< std::endl
;
729 Debug("pf::array") << "Next node is: " << nodeAfterEqualitySequence
<< std::endl
;
731 ss
<< "(trans _ _ _ _ ";
733 // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
735 if (match(n1
[0], pf
.d_node
[0])) {
736 n1
= eqNode(n1
[0], n1
[0]);
737 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
738 } else if (match(n1
[1], pf
.d_node
[1])) {
739 n1
= eqNode(n1
[1], n1
[1]);
740 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
742 Debug("pf::array") << "Error: identical equalities over, but hands don't match what we're proving."
747 // We have a "next node". Use it to guide us.
748 if (nodeAfterEqualitySequence
.getKind() == kind::NOT
) {
749 nodeAfterEqualitySequence
= nodeAfterEqualitySequence
[0];
752 Assert(nodeAfterEqualitySequence
.getKind() == kind::EQUAL
);
754 if ((n1
[0] == nodeAfterEqualitySequence
[0]) || (n1
[0] == nodeAfterEqualitySequence
[1])) {
757 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
758 n1
= eqNode(n1
[0], n1
[0]);
760 } else if ((n1
[1] == nodeAfterEqualitySequence
[0]) || (n1
[1] == nodeAfterEqualitySequence
[1])) {
763 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
764 n1
= eqNode(n1
[1], n1
[1]);
767 Debug("pf::array") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl
;
775 Debug("pf::array") << "Equality sequence length is odd!" << std::endl
;
779 Debug("pf::array") << "Have proven: " << n1
<< std::endl
;
784 // Ignore the redundancy.
789 if (identicalEqualities
) {
790 // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
791 identicalEqualities
= false;
794 Debug("mgd") << "\ndoing trans proof, got n2 " << n2
<< "\n";
796 Debug("mgdx") << "\ntrans proof[" << i
<< "], got n2 " << n2
<< "\n";
797 Debug("mgdx") << (n2
.getKind() == kind::EQUAL
) << "\n";
799 if ((n1
.getNumChildren() >= 2) && (n2
.getNumChildren() >= 2)) {
800 Debug("mgdx") << n1
[0].getId() << " " << n1
[1].getId() << " / " << n2
[0].getId() << " " << n2
[1].getId() << "\n";
801 Debug("mgdx") << n1
[0].getId() << " " << n1
[0] << "\n";
802 Debug("mgdx") << n1
[1].getId() << " " << n1
[1] << "\n";
803 Debug("mgdx") << n2
[0].getId() << " " << n2
[0] << "\n";
804 Debug("mgdx") << n2
[1].getId() << " " << n2
[1] << "\n";
805 Debug("mgdx") << (n1
[0] == n2
[0]) << "\n";
806 Debug("mgdx") << (n1
[1] == n2
[1]) << "\n";
807 Debug("mgdx") << (n1
[0] == n2
[1]) << "\n";
808 Debug("mgdx") << (n1
[1] == n2
[0]) << "\n";
812 // We can hadnle one of the equalities being negative, but not both
813 Assert((n1
.getKind() != kind::NOT
) || (n2
.getKind() != kind::NOT
));
818 if (n1
.getKind() == kind::NOT
) {
819 Debug("mgdx") << "n1 is negative" << std::endl
;
820 Debug("pf::array") << "n1 = " << n1
<< ", n2 = " << n2
<< std::endl
;
822 ss
<< "(negtrans1 _ _ _ _ ";
824 } else if (n2
.getKind() == kind::NOT
) {
825 Debug("mgdx") << "n2 is negative" << std::endl
;
826 Debug("pf::array") << "n1 = " << n1
<< ", n2 = " << n2
<< std::endl
;
828 ss
<< "(negtrans2 _ _ _ _ ";
831 ss
<< "(trans _ _ _ _ ";
834 if((n2
.getKind() == kind::EQUAL
) && (n1
.getKind() == kind::EQUAL
))
835 // Both elements of the transitivity rule are equalities/iffs
838 if(tb
== 1) { Debug("mgdx") << "case 1\n"; }
839 n1
= eqNode(n1
[1], n2
[1]);
840 ss
<< (firstNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ") << ss1
.str() << ") " << ss2
.str();
841 } else if(n1
[1] == n2
[1]) {
842 if(tb
== 1) { Debug("mgdx") << "case 2\n"; }
843 n1
= eqNode(n1
[0], n2
[0]);
844 ss
<< ss1
.str() << (secondNeg
? " (negsymm _ _ _ " : " (symm _ _ _ " ) << ss2
.str() << ")";
845 } else if(n1
[0] == n2
[1]) {
846 if(tb
== 1) { Debug("mgdx") << "case 3\n"; }
847 if(!firstNeg
&& !secondNeg
) {
848 n1
= eqNode(n2
[0], n1
[1]);
849 ss
<< ss2
.str() << " " << ss1
.str();
850 } else if (firstNeg
) {
851 n1
= eqNode(n1
[1], n2
[0]);
852 ss
<< " (negsymm _ _ _ " << ss1
.str() << ") (symm _ _ _ " << ss2
.str() << ")";
855 n1
= eqNode(n1
[1], n2
[0]);
856 ss
<< " (symm _ _ _ " << ss1
.str() << ") (negsymm _ _ _ " << ss2
.str() << ")";
858 if(tb
== 1) { Debug("mgdx") << "++ proved " << n1
<< "\n"; }
859 } else if(n1
[1] == n2
[0]) {
860 if(tb
== 1) { Debug("mgdx") << "case 4\n"; }
861 n1
= eqNode(n1
[0], n2
[1]);
862 ss
<< ss1
.str() << " " << ss2
.str();
864 Warning() << "\n\ntrans proof failure at step " << i
<< "\n\n";
865 Warning() << "0 proves " << n1
<< "\n";
866 Warning() << "1 proves " << n2
<< "\n\n";
867 pf
.debug_print("mgdx", 0, &proofPrinter
);
868 //toStreamRec(Warning.getStream(), pf, 0);
872 Debug("mgd") << "++ trans proof[" << i
<< "], now have " << n1
<< std::endl
;
873 } else if(n1
.getKind() == kind::EQUAL
) {
874 // n1 is an equality/iff, but n2 is a predicate
877 ss
<< (firstNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ")
878 << ss1
.str() << ") (pred_eq_t _ " << ss2
.str() << ")";
879 } else if(n1
[1] == n2
) {
881 ss
<< ss1
.str() << " (pred_eq_t _ " << ss2
.str() << ")";
885 } else if(n2
.getKind() == kind::EQUAL
) {
886 // n2 is an equality/iff, but n1 is a predicate
889 ss
<< (secondNeg
? "(negsymm _ _ _ " : "(symm _ _ _ ")
890 << ss2
.str() << ") (pred_eq_t _ " << ss1
.str() << ")";
891 } else if(n2
[1] == n1
) {
893 ss
<< ss2
.str() << " (pred_eq_t _ " << ss1
.str() << ")";
898 // Both n1 and n2 are prediacates. Don't know what to do...
904 if (firstNeg
|| secondNeg
) {
905 n1
= (n1
.getKind() == kind::NOT
) ? n1
[0] : n1
.notNode();
910 Debug("mgd") << "\n++ trans proof done, have proven " << n1
<< std::endl
;
911 //return (firstNeg || secondNeg) ? n1.notNode() : n1;
915 else if (pf
.d_id
== d_reasonRow
) {
916 Debug("mgd") << "row lemma: " << pf
.d_node
<< std::endl
;
917 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
920 if (pf
.d_node
[1].getKind() == kind::SELECT
) {
921 // This is the case where ((a[i]:=t)[k] == a[k]), and the sub-proof explains why (i != k).
922 TNode t1
, t2
, t3
, t4
;
924 if(pf
.d_node
[1].getKind() == kind::SELECT
&&
925 pf
.d_node
[1][0].getKind() == kind::STORE
&&
926 pf
.d_node
[0].getKind() == kind::SELECT
&&
927 pf
.d_node
[0][0] == pf
.d_node
[1][0][0] &&
928 pf
.d_node
[0][1] == pf
.d_node
[1][1]) {
929 t2
= pf
.d_node
[1][0][1];
930 t3
= pf
.d_node
[1][1];
931 t1
= pf
.d_node
[0][0];
932 t4
= pf
.d_node
[1][0][2];
933 ret
= pf
.d_node
[1].eqNode(pf
.d_node
[0]);
934 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
936 Assert(pf
.d_node
[0].getKind() == kind::SELECT
&&
937 pf
.d_node
[0][0].getKind() == kind::STORE
&&
938 pf
.d_node
[1].getKind() == kind::SELECT
&&
939 pf
.d_node
[1][0] == pf
.d_node
[0][0][0] &&
940 pf
.d_node
[1][1] == pf
.d_node
[0][1]);
941 t2
= pf
.d_node
[0][0][1];
942 t3
= pf
.d_node
[0][1];
943 t1
= pf
.d_node
[1][0];
944 t4
= pf
.d_node
[0][0][2];
946 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
949 // inner index != outer index
950 // t3 is the outer index
952 Assert(pf
.d_children
.size() == 1);
953 std::stringstream ss
;
954 Node subproof
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
957 tp
->printTerm(t2
.toExpr(), out
, map
);
959 tp
->printTerm(t3
.toExpr(), out
, map
);
961 tp
->printTerm(t1
.toExpr(), out
, map
);
963 tp
->printTerm(t4
.toExpr(), out
, map
);
967 Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf
.d_children
[0]->d_node
968 << ". t3 is: " << t3
<< std::endl
969 << "subproof is: " << subproof
<< std::endl
;
971 Debug("pf::array") << "Subproof is: " << ss
.str() << std::endl
;
973 // The subproof needs to show that t2 != t3. This can either be a direct disequality,
974 // or, if (wlog) t2 is constant, it can show that t3 is equal to another constant.
975 if (subproof
.getKind() == kind::NOT
) {
976 // The subproof is for t2 != t3 (or t3 != t2)
977 if (subproof
[0][1] == t3
) {
978 Debug("pf::array") << "Dont need symmetry!" << std::endl
;
981 Debug("pf::array") << "Need symmetry!" << std::endl
;
982 out
<< "(negsymm _ _ _ " << ss
.str() << ")";
985 // Either t2 or t3 is a constant.
986 Assert(subproof
.getKind() == kind::EQUAL
);
987 Assert(subproof
[0].isConst() || subproof
[1].isConst());
988 Assert(t2
.isConst() || t3
.isConst());
989 Assert(!(t2
.isConst() && t3
.isConst()));
991 bool t2IsConst
= t2
.isConst();
992 if (subproof
[0].isConst()) {
994 // (t3 == subproof[1]) == subproof[0] != t2
996 // subproof already shows constant = t3
997 Assert(t3
== subproof
[1]);
998 out
<< "(negtrans _ _ _ _ ";
999 tp
->printConstantDisequalityProof(out
, t2
.toExpr(), subproof
[0].toExpr(), map
);
1004 Assert(t2
== subproof
[1]);
1005 out
<< "(negsymm _ _ _ ";
1006 out
<< "(negtrans _ _ _ _ ";
1007 tp
->printConstantDisequalityProof(out
, t3
.toExpr(), subproof
[0].toExpr(), map
);
1014 // (t3 == subproof[0]) == subproof[1] != t2
1016 // subproof already shows constant = t3
1017 Assert(t3
== subproof
[0]);
1018 out
<< "(negtrans _ _ _ _ ";
1019 tp
->printConstantDisequalityProof(out
, t2
.toExpr(), subproof
[1].toExpr(), map
);
1021 out
<< "(symm _ _ _ " << ss
.str() << ")";
1024 Assert(t2
== subproof
[0]);
1025 out
<< "(negsymm _ _ _ ";
1026 out
<< "(negtrans _ _ _ _ ";
1027 tp
->printConstantDisequalityProof(out
, t3
.toExpr(), subproof
[1].toExpr(), map
);
1029 out
<< "(symm _ _ _ " << ss
.str() << ")";
1038 Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl
;
1040 Debug("pf::array") << "pf.d_children[0]->d_node is: " << pf
.d_children
[0]->d_node
<< std::endl
;
1042 // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k])
1044 // If we wanted to remove the need for "negativerow", we would need to prove i==k using a new satlem. We would:
1045 // 1. Create a new satlem.
1046 // 2. Assume that i != k
1047 // 3. Apply ROW to show that ((a[i]:=t)[k] == a[k])
1048 // 4. Contradict this with the fact that ((a[i]:=t)[k] != a[k]), obtaining our contradiction
1050 TNode t1
, t2
, t3
, t4
;
1053 // pf.d_node is an equality, i==k.
1057 // pf.d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
1058 // or its symmetrical version.
1061 if (pf
.d_children
[0]->d_node
[0][0].getKind() == kind::SELECT
&&
1062 pf
.d_children
[0]->d_node
[0][0][0].getKind() == kind::STORE
) {
1064 } else if (pf
.d_children
[0]->d_node
[0][1].getKind() == kind::SELECT
&&
1065 pf
.d_children
[0]->d_node
[0][1][0].getKind() == kind::STORE
) {
1072 Debug("pf::array") << "Side is: " << side
<< std::endl
;
1074 // The array's index and element types will come from the subproof...
1075 t3
= pf
.d_children
[0]->d_node
[0][side
][0][0];
1076 t4
= pf
.d_children
[0]->d_node
[0][side
][0][2];
1079 // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
1080 bool swap
= (t2
== pf
.d_children
[0]->d_node
[0][side
][0][1]);
1082 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\nt4 " << t4
<< "\n";
1084 Assert(pf
.d_children
.size() == 1);
1085 std::stringstream ss
;
1086 Node subproof
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
1088 Debug("pf::array") << "Subproof is: " << ss
.str() << std::endl
;
1091 out
<< "(symm _ _ _ ";
1094 out
<< "(negativerow _ _ ";
1095 tp
->printTerm(swap
? t2
.toExpr() : t1
.toExpr(), out
, map
);
1097 tp
->printTerm(swap
? t1
.toExpr() : t2
.toExpr(), out
, map
);
1099 tp
->printTerm(t3
.toExpr(), out
, map
);
1101 tp
->printTerm(t4
.toExpr(), out
, map
);
1105 out
<< "(negsymm _ _ _ " << ss
.str() << ")";
1120 else if (pf
.d_id
== d_reasonRow1
) {
1121 Debug("mgd") << "row1 lemma: " << pf
.d_node
<< std::endl
;
1122 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
1125 if(pf
.d_node
[1].getKind() == kind::SELECT
&&
1126 pf
.d_node
[1][0].getKind() == kind::STORE
&&
1127 pf
.d_node
[1][0][1] == pf
.d_node
[1][1] &&
1128 pf
.d_node
[1][0][2] == pf
.d_node
[0]) {
1129 t1
= pf
.d_node
[1][0][0];
1130 t2
= pf
.d_node
[1][0][1];
1132 ret
= pf
.d_node
[1].eqNode(pf
.d_node
[0]);
1133 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1135 Assert(pf
.d_node
[0].getKind() == kind::SELECT
&&
1136 pf
.d_node
[0][0].getKind() == kind::STORE
&&
1137 pf
.d_node
[0][0][1] == pf
.d_node
[0][1] &&
1138 pf
.d_node
[0][0][2] == pf
.d_node
[1]);
1139 t1
= pf
.d_node
[0][0][0];
1140 t2
= pf
.d_node
[0][0][1];
1143 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1145 out
<< "(row1 _ _ ";
1146 tp
->printTerm(t1
.toExpr(), out
, map
);
1148 tp
->printTerm(t2
.toExpr(), out
, map
);
1150 tp
->printTerm(t3
.toExpr(), out
, map
);
1155 else if (pf
.d_id
== d_reasonExt
) {
1156 Assert(pf
.d_node
.getKind() == kind::NOT
);
1157 Assert(pf
.d_node
[0].getKind() == kind::EQUAL
);
1158 Assert(pf
.d_children
.size() == 1);
1159 std::shared_ptr
<theory::eq::EqProof
> child_proof
= pf
.d_children
[0];
1160 Assert(child_proof
->d_node
.getKind() == kind::NOT
);
1161 Assert(child_proof
->d_node
[0].getKind() == kind::EQUAL
);
1163 Debug("mgd") << "EXT lemma: " << pf
.d_node
<< std::endl
;
1166 t1
= child_proof
->d_node
[0][0];
1167 t2
= child_proof
->d_node
[0][1];
1168 t3
= pf
.d_node
[0][0][1];
1170 Debug("mgd") << "t1 " << t1
<< "\nt2 " << t2
<< "\nt3 " << t3
<< "\n";
1172 out
<< "(or_elim_1 _ _ ";
1173 out
<< ProofManager::getLitName(child_proof
->d_node
[0]);
1175 out
<< ProofManager::getArrayProof()->skolemToLiteral(t3
.toExpr());
1182 Assert(!pf
.d_node
.isNull());
1183 Assert(pf
.d_children
.empty());
1184 Debug("mgd") << "theory proof: " << pf
.d_node
<< " by rule " << int(pf
.d_id
) << std::endl
;
1185 AlwaysAssert(false);
1190 ArrayProof::ArrayProof(theory::arrays::TheoryArrays
* arrays
, TheoryProofEngine
* pe
)
1191 : TheoryProof(arrays
, pe
)
1194 void ArrayProof::registerTerm(Expr term
) {
1195 // already registered
1196 if (d_declarations
.find(term
) != d_declarations
.end())
1199 Type type
= term
.getType();
1200 if (type
.isSort()) {
1201 // declare uninterpreted sorts
1202 d_sorts
.insert(type
);
1205 if (term
.getKind() == kind::APPLY_UF
) {
1206 Expr function
= term
.getOperator();
1207 d_declarations
.insert(function
);
1210 if (term
.isVariable()) {
1211 d_declarations
.insert(term
);
1214 if (term
.getKind() == kind::SELECT
&& term
.getType().isBoolean()) {
1215 // Ensure cnf literals
1217 ProofManager::currentPM()->ensureLiteral(eqNode(term
, NodeManager::currentNM()->mkConst(true)));
1218 ProofManager::currentPM()->ensureLiteral(eqNode(term
, NodeManager::currentNM()->mkConst(false)));
1221 // recursively declare all other terms
1222 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
1223 // could belong to other theories
1224 d_proofEngine
->registerTerm(term
[i
]);
1228 std::string
ArrayProof::skolemToLiteral(Expr skolem
) {
1229 Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem
<< ")" << std::endl
;
1230 Assert(d_skolemToLiteral
.find(skolem
) != d_skolemToLiteral
.end());
1231 return d_skolemToLiteral
[skolem
];
1234 void LFSCArrayProof::printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
1235 Assert (theory::Theory::theoryOf(term
) == theory::THEORY_ARRAYS
);
1237 if (theory::Theory::theoryOf(term
) != theory::THEORY_ARRAYS
) {
1238 // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
1239 // hiding as a subterm of an array term. In that case, send it back to the dispatcher.
1240 d_proofEngine
->printBoundTerm(term
, os
, map
);
1244 if (term
.getKind() == kind::VARIABLE
|| term
.getKind() == kind::SKOLEM
) {
1249 Assert ((term
.getKind() == kind::SELECT
) || (term
.getKind() == kind::PARTIAL_SELECT_0
) || (term
.getKind() == kind::PARTIAL_SELECT_1
) || (term
.getKind() == kind::STORE
));
1251 switch (term
.getKind()) {
1252 case kind::SELECT
: {
1253 Assert(term
.getNumChildren() == 2);
1255 bool convertToBool
= (term
[1].getType().isBoolean() && !d_proofEngine
->printsAsBool(term
[1]));
1257 os
<< "(apply _ _ (apply _ _ (read ";
1258 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1260 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1262 printTerm(term
[0], os
, map
);
1264 if (convertToBool
) os
<< "(f_to_b ";
1265 printTerm(term
[1], os
, map
);
1266 if (convertToBool
) os
<< ")";
1271 case kind::PARTIAL_SELECT_0
:
1272 Assert(term
.getNumChildren() == 1);
1274 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1276 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1280 case kind::PARTIAL_SELECT_1
:
1281 Debug("pf::array") << "This branch has not beed tested yet." << std::endl
;
1284 Assert(term
.getNumChildren() == 1);
1285 os
<< "(apply _ _ (read ";
1286 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1288 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1290 printTerm(term
[0], os
, map
);
1295 os
<< "(apply _ _ (apply _ _ (apply _ _ (write ";
1296 printSort(ArrayType(term
[0].getType()).getIndexType(), os
);
1298 printSort(ArrayType(term
[0].getType()).getConstituentType(), os
);
1300 printTerm(term
[0], os
, map
);
1302 printTerm(term
[1], os
, map
);
1304 printTerm(term
[2], os
, map
);
1314 void LFSCArrayProof::printOwnedSort(Type type
, std::ostream
& os
) {
1315 Debug("pf::array") << std::endl
<< "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type
<< std::endl
;
1316 Assert (type
.isArray() || type
.isSort());
1317 if (type
.isArray()){
1318 ArrayType
array_type(type
);
1320 Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: "
1321 << array_type
.getIndexType()
1322 << ", element type: " << array_type
.getConstituentType() << std::endl
;
1325 printSort(array_type
.getIndexType(), os
);
1327 printSort(array_type
.getConstituentType(), os
);
1334 void LFSCArrayProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
) {
1335 os
<< " ;; Array Theory Lemma \n;;";
1336 for (unsigned i
= 0; i
< lemma
.size(); ++i
) {
1337 os
<< lemma
[i
] <<" ";
1340 //os << " (clausify_false trust)";
1341 ArrayProof::printTheoryLemmaProof(lemma
, os
, paren
, map
);
1344 void LFSCArrayProof::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1345 // declaring the sorts
1346 for (TypeSet::const_iterator it
= d_sorts
.begin(); it
!= d_sorts
.end(); ++it
) {
1347 if (!ProofManager::currentPM()->wasPrinted(*it
)) {
1348 os
<< "(% " << *it
<< " sort\n";
1350 ProofManager::currentPM()->markPrinted(*it
);
1355 void LFSCArrayProof::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1356 Debug("pf::array") << "Arrays declaring terms..." << std::endl
;
1358 for (ExprSet::const_iterator it
= d_declarations
.begin(); it
!= d_declarations
.end(); ++it
) {
1361 Assert(term
.getType().isArray() || term
.isVariable());
1363 Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is: " << term
1364 << ". It's type is: " << term
.getType()
1367 if (term
.getType().isArray()){
1368 ArrayType
array_type(term
.getType());
1370 Debug("pf::array") << "LFSCArrayProof::printDeclarations: term is an array. Index type: "
1371 << array_type
.getIndexType()
1372 << ", element type: " << array_type
.getConstituentType() << std::endl
;
1374 os
<< "(% " << ProofManager::sanitize(term
) << " ";
1378 printSort(array_type
.getIndexType(), os
);
1380 printSort(array_type
.getConstituentType(), os
);
1385 Assert(term
.isVariable());
1386 if (ProofManager::getSkolemizationManager()->isSkolem(*it
)) {
1387 Debug("pf::array") << "This term is a skoelm!" << std::endl
;
1388 d_skolemDeclarations
.insert(*it
);
1390 os
<< "(% " << ProofManager::sanitize(term
) << " ";
1392 os
<< term
.getType() << ")\n";
1398 Debug("pf::array") << "Declaring terms done!" << std::endl
;
1401 void LFSCArrayProof::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1402 Debug("pf::array") << "Array: print deferred declarations called" << std::endl
;
1405 for (ExprSet::const_iterator it
= d_skolemDeclarations
.begin(); it
!= d_skolemDeclarations
.end(); ++it
) {
1407 Node equality
= ProofManager::getSkolemizationManager()->getDisequality(*it
);
1409 Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: term is: " << *it
<< std::endl
1410 << "It is a witness for: " << equality
<< std::endl
;
1412 std::ostringstream newSkolemLiteral
;
1413 newSkolemLiteral
<< ".sl" << count
++;
1414 std::string skolemLiteral
= newSkolemLiteral
.str();
1416 d_skolemToLiteral
[*it
] = skolemLiteral
;
1418 Debug("pf::array") << "LFSCArrayProof::printDeferredDeclarations: new skolem literal is: " << skolemLiteral
<< std::endl
;
1420 Assert(equality
.getKind() == kind::NOT
);
1421 Assert(equality
[0].getKind() == kind::EQUAL
);
1423 Node array_one
= equality
[0][0];
1424 Node array_two
= equality
[0][1];
1428 printTerm(array_one
.toExpr(), os
, map
);
1430 printTerm(array_two
.toExpr(), os
, map
);
1432 os
<< ProofManager::sanitize(*it
);
1434 os
<< skolemLiteral
.c_str();
1441 void LFSCArrayProof::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
1442 // Nothing to do here at this point.
1445 bool LFSCArrayProof::printsAsBool(const Node
&n
)
1447 if (n
.getKind() == kind::SELECT
)
1453 } /* CVC4 namespace */