1 /********************* */
2 /*! \file arith_proof.cpp
4 ** Top contributors (to current version):
5 ** Guy Katz, Tim King, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
17 #include "proof/arith_proof.h"
22 #include "proof/proof_manager.h"
23 #include "proof/theory_proof.h"
24 #include "theory/arith/theory_arith.h"
28 inline static Node
eqNode(TNode n1
, TNode n2
) {
29 return NodeManager::currentNM()->mkNode(kind::EQUAL
, n1
, n2
);
32 // congrence matching term helper
33 inline static bool match(TNode n1
, TNode n2
) {
34 Debug("pf::arith") << "match " << n1
<< " " << n2
<< std::endl
;
35 if(ProofManager::currentPM()->hasOp(n1
)) {
36 n1
= ProofManager::currentPM()->lookupOp(n1
);
38 if(ProofManager::currentPM()->hasOp(n2
)) {
39 n2
= ProofManager::currentPM()->lookupOp(n2
);
41 Debug("pf::arith") << "+ match " << n1
<< " " << n2
<< std::endl
;
45 if(n1
.getType().isFunction() && n2
.hasOperator()) {
46 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
47 return n1
== ProofManager::currentPM()->lookupOp(n2
.getOperator());
49 return n1
== n2
.getOperator();
52 if(n2
.getType().isFunction() && n1
.hasOperator()) {
53 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
54 return n2
== ProofManager::currentPM()->lookupOp(n1
.getOperator());
56 return n2
== n1
.getOperator();
59 if(n1
.hasOperator() && n2
.hasOperator() && n1
.getOperator() != n2
.getOperator()) {
62 for(size_t i
= 0; i
< n1
.getNumChildren() && i
< n2
.getNumChildren(); ++i
) {
70 void ProofArith::toStream(std::ostream
& out
) const
72 Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl
;
73 //AJR : carry this further?
75 toStreamLFSC(out
, ProofManager::getArithProof(), *d_proof
, map
);
78 void ProofArith::toStreamLFSC(std::ostream
& out
,
80 const theory::eq::EqProof
& pf
,
81 const ProofLetMap
& map
)
83 Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl
;
84 pf
.debug_print("lfsc-arith");
85 Debug("lfsc-arith") << std::endl
;
86 toStreamRecLFSC(out
, tp
, pf
, 0, map
);
89 Node
ProofArith::toStreamRecLFSC(std::ostream
& out
,
91 const theory::eq::EqProof
& pf
,
93 const ProofLetMap
& map
)
95 Debug("pf::arith") << std::endl
97 << "toStreamRecLFSC called. tb = " << tb
98 << " . proof:" << std::endl
;
99 pf
.debug_print("pf::arith");
100 Debug("pf::arith") << std::endl
;
103 Assert(pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
);
104 Assert(!pf
.d_node
.isNull());
105 Assert(pf
.d_children
.size() >= 2);
108 std::shared_ptr
<theory::eq::EqProof
> subTrans
=
109 std::make_shared
<theory::eq::EqProof
>();
110 subTrans
->d_id
= theory::eq::MERGED_THROUGH_TRANS
;
111 subTrans
->d_node
= pf
.d_node
;
114 while (i
< pf
.d_children
.size()) {
115 // Look for the negative clause, with which we will form a contradiction.
116 if(!pf
.d_children
[i
]->d_node
.isNull() && pf
.d_children
[i
]->d_node
.getKind() == kind::NOT
) {
122 // Handle congruence closures over equalities.
123 else if (pf
.d_children
[i
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&& pf
.d_children
[i
]->d_node
.isNull()) {
124 Debug("pf::arith") << "Handling congruence over equalities" << std::endl
;
126 // Gather the sequence of consecutive congruence closures.
127 std::vector
<std::shared_ptr
<const theory::eq::EqProof
>> congruenceClosures
;
129 Debug("pf::arith") << "Collecting congruence sequence" << std::endl
;
131 i
+ count
< pf
.d_children
.size() &&
132 pf
.d_children
[i
+ count
]->d_id
==theory::eq::MERGED_THROUGH_CONGRUENCE
&&
133 pf
.d_children
[i
+ count
]->d_node
.isNull();
135 Debug("pf::arith") << "Found a congruence: " << std::endl
;
136 pf
.d_children
[i
+count
]->debug_print("pf::arith");
137 congruenceClosures
.push_back(pf
.d_children
[i
+count
]);
140 Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures
.size() << std::endl
;
142 // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
143 bool targetAppearsBefore
= true;
144 bool targetAppearsAfter
= true;
146 if ((i
== 0) || (i
== 1 && neg
== 0)) {
147 Debug("pf::arith") << "Target does not appear before" << std::endl
;
148 targetAppearsBefore
= false;
151 if ((i
+ count
>= pf
.d_children
.size()) ||
152 (!pf
.d_children
[i
+ count
]->d_node
.isNull() &&
153 pf
.d_children
[i
+ count
]->d_node
.getKind() == kind::NOT
)) {
154 Debug("pf::arith") << "Target does not appear after" << std::endl
;
155 targetAppearsAfter
= false;
158 // Assert that we have precisely one target clause.
159 Assert(targetAppearsBefore
!= targetAppearsAfter
);
161 // Begin breaking up the congruences and ordering the equalities correctly.
162 std::vector
<std::shared_ptr
<theory::eq::EqProof
>> orderedEqualities
;
165 // Insert target clause first.
166 if (targetAppearsBefore
) {
167 orderedEqualities
.push_back(pf
.d_children
[i
- 1]);
168 // The target has already been added to subTrans; remove it.
169 subTrans
->d_children
.pop_back();
171 orderedEqualities
.push_back(pf
.d_children
[i
+ count
]);
174 // Start with the congruence closure closest to the target clause, and work our way back/forward.
175 if (targetAppearsBefore
) {
176 for (unsigned j
= 0; j
< count
; ++j
) {
177 if (pf
.d_children
[i
+ j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
178 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ j
]->d_children
[0]);
179 if (pf
.d_children
[i
+ j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
180 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ j
]->d_children
[1]);
183 for (unsigned j
= 0; j
< count
; ++j
) {
184 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
185 orderedEqualities
.insert(orderedEqualities
.begin(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]);
186 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]->d_id
!= theory::eq::MERGED_THROUGH_REFLEXIVITY
)
187 orderedEqualities
.insert(orderedEqualities
.end(), pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]);
191 // Copy the result into the main transitivity proof.
192 subTrans
->d_children
.insert(subTrans
->d_children
.end(), orderedEqualities
.begin(), orderedEqualities
.end());
194 // Increase i to skip over the children that have been processed.
196 if (targetAppearsAfter
) {
201 // Else, just copy the child proof as is
203 subTrans
->d_children
.push_back(pf
.d_children
[i
]);
210 std::stringstream ss
;
211 //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
212 Debug("pf::arith") << "\nsubtrans has " << subTrans
->d_children
.size() << " children\n";
213 if(pf
.d_children
.size() > 2) {
214 n1
= toStreamRecLFSC(ss
, tp
, *subTrans
, 1, map
);
216 n1
= toStreamRecLFSC(ss
, tp
, *(subTrans
->d_children
[0]), 1, map
);
217 Debug("pf::arith") << "\nsubTrans unique child " << subTrans
->d_children
[0]->d_id
<< " was proven\ngot: " << n1
<< std::endl
;
220 Node n2
= pf
.d_children
[neg
]->d_node
;
221 Assert(n2
.getKind() == kind::NOT
);
222 out
<< "(clausify_false (contra _ ";
223 Debug("pf::arith") << "\nhave proven: " << n1
<< std::endl
;
224 Debug("pf::arith") << "n2 is " << n2
[0] << std::endl
;
226 if (n2
[0].getNumChildren() > 0) { Debug("pf::arith") << "\nn2[0]: " << n2
[0][0] << std::endl
; }
227 if (n1
.getNumChildren() > 1) { Debug("pf::arith") << "n1[1]: " << n1
[1] << std::endl
; }
229 if(n2
[0].getKind() == kind::APPLY_UF
) {
230 out
<< "(trans _ _ _ _ ";
231 out
<< "(symm _ _ _ ";
233 out
<< ") (pred_eq_f _ " << ProofManager::getLitName(n2
[0]) << ")) t_t_neq_f))" << std::endl
;
235 Assert((n1
[0] == n2
[0][0] && n1
[1] == n2
[0][1]) || (n1
[1] == n2
[0][0] && n1
[0] == n2
[0][1]));
236 if(n1
[1] == n2
[0][0]) {
237 out
<< "(symm _ _ _ " << ss
.str() << ")";
241 out
<< " " << ProofManager::getLitName(n2
[0]) << "))" << std::endl
;
247 case theory::eq::MERGED_THROUGH_CONGRUENCE
: {
248 Debug("pf::arith") << "\nok, looking at congruence:\n";
249 pf
.debug_print("pf::arith");
250 std::stack
<const theory::eq::EqProof
*> stk
;
251 for (const theory::eq::EqProof
* pf2
= &pf
;
252 pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
;
253 pf2
= pf2
->d_children
[0].get()) {
254 Assert(!pf2
->d_node
.isNull());
255 Assert(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
|| pf2
->d_node
.getKind() == kind::BUILTIN
|| pf2
->d_node
.getKind() == kind::APPLY_UF
|| pf2
->d_node
.getKind() == kind::SELECT
|| pf2
->d_node
.getKind() == kind::STORE
);
256 Assert(pf2
->d_children
.size() == 2);
257 out
<< "(cong _ _ _ _ _ _ ";
260 Assert(stk
.top()->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
);
261 NodeBuilder
<> b1(kind::PARTIAL_APPLY_UF
), b2(kind::PARTIAL_APPLY_UF
);
262 const theory::eq::EqProof
* pf2
= stk
.top();
264 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
265 Node n1
= toStreamRecLFSC(out
, tp
, *(pf2
->d_children
[0]), tb
+ 1, map
);
267 std::stringstream ss
;
268 Node n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
269 Debug("pf::arith") << "\nok, in FIRST cong[" << stk
.size() << "]" << "\n";
270 pf2
->debug_print("pf::arith");
271 Debug("pf::arith") << "looking at " << pf2
->d_node
<< "\n";
272 Debug("pf::arith") << " " << n1
<< "\n";
273 Debug("pf::arith") << " " << n2
<< "\n";
275 if(match(pf2
->d_node
, n1
[0])) {
277 Debug("pf::arith") << "SIDE IS 0\n";
282 Debug("pf::arith") << "SIDE IS 1\n";
284 if(!match(pf2
->d_node
, n1
[1])) {
285 Debug("pf::arith") << "IN BAD CASE, our first subproof is\n";
286 pf2
->d_children
[0]->debug_print("pf::arith");
288 Assert(match(pf2
->d_node
, n1
[1]));
291 if(n1
[side
].getKind() == kind::APPLY_UF
|| n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
|| n1
[side
].getKind() == kind::SELECT
|| n1
[side
].getKind() == kind::STORE
) {
292 if(n1
[side
].getKind() == kind::APPLY_UF
|| n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
) {
293 b1
<< n1
[side
].getOperator();
295 b1
<< ProofManager::currentPM()->mkOp(n1
[side
].getOperator());
297 b1
.append(n1
[side
].begin(), n1
[side
].end());
301 if(n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
|| n1
[1-side
].getKind() == kind::APPLY_UF
|| n1
[side
].getKind() == kind::SELECT
|| n1
[side
].getKind() == kind::STORE
) {
302 if(n1
[1-side
].getKind() == kind::PARTIAL_APPLY_UF
|| n1
[1-side
].getKind() == kind::APPLY_UF
) {
303 b2
<< n1
[1-side
].getOperator();
305 b2
<< ProofManager::currentPM()->mkOp(n1
[1-side
].getOperator());
307 b2
.append(n1
[1-side
].begin(), n1
[1-side
].end());
311 Debug("pf::arith") << "pf2->d_node " << pf2
->d_node
<< std::endl
;
312 Debug("pf::arith") << "b1.getNumChildren() " << b1
.getNumChildren() << std::endl
;
313 Debug("pf::arith") << "n1 " << n1
<< std::endl
;
314 Debug("pf::arith") << "n2 " << n2
<< std::endl
;
315 Debug("pf::arith") << "side " << side
<< std::endl
;
316 if(pf2
->d_node
[b1
.getNumChildren() - (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[side
]) {
321 Assert(pf2
->d_node
[b1
.getNumChildren() - (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[1-side
]);
324 out
<< "(symm _ _ _ " << ss
.str() << ")";
327 while(!stk
.empty()) {
329 Debug("pf::arith") << "\nMORE TO DO\n";
333 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
336 n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
337 Debug("pf::arith") << "\nok, in cong[" << stk
.size() << "]" << "\n";
338 Debug("pf::arith") << "looking at " << pf2
->d_node
<< "\n";
339 Debug("pf::arith") << " " << n1
<< "\n";
340 Debug("pf::arith") << " " << n2
<< "\n";
341 Debug("pf::arith") << " " << b1
<< "\n";
342 Debug("pf::arith") << " " << b2
<< "\n";
343 if(pf2
->d_node
[b1
.getNumChildren()] == n2
[side
]) {
348 Assert(pf2
->d_node
[b1
.getNumChildren()] == n2
[1-side
]);
351 out
<< "(symm _ _ _ " << ss
.str() << ")";
357 Debug("pf::arith") << "at end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
358 if(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
) {
359 Assert(n1
== pf2
->d_node
);
361 if(n1
.getOperator().getType().getNumChildren() == n1
.getNumChildren() + 1) {
362 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
363 b1
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
365 b1
.clear(kind::APPLY_UF
);
366 b1
<< n1
.getOperator();
368 b1
.append(n1
.begin(), n1
.end());
370 Debug("pf::arith") << "at[2] end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
371 if(pf2
->d_node
.getKind() == kind::APPLY_UF
) {
372 Assert(n1
== pf2
->d_node
);
375 if(n2
.getOperator().getType().getNumChildren() == n2
.getNumChildren() + 1) {
376 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
377 b2
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
379 b2
.clear(kind::APPLY_UF
);
380 b2
<< n2
.getOperator();
382 b2
.append(n2
.begin(), n2
.end());
385 Node n
= (side
== 0 ? eqNode(n1
, n2
) : eqNode(n2
, n1
));
387 Debug("pf::arith") << "\ncong proved: " << n
<< "\n";
392 case theory::eq::MERGED_THROUGH_REFLEXIVITY
:
393 Assert(!pf
.d_node
.isNull());
394 Assert(pf
.d_children
.empty());
396 tp
->printTerm(NodeManager::currentNM()->toExpr(pf
.d_node
), out
, map
);
398 return eqNode(pf
.d_node
, pf
.d_node
);
400 case theory::eq::MERGED_THROUGH_EQUALITY
:
401 Assert(!pf
.d_node
.isNull());
402 Assert(pf
.d_children
.empty());
403 out
<< ProofManager::getLitName(pf
.d_node
.negate());
406 case theory::eq::MERGED_THROUGH_TRANS
: {
407 Assert(!pf
.d_node
.isNull());
408 Assert(pf
.d_children
.size() >= 2);
409 std::stringstream ss
;
410 Debug("pf::arith") << "\ndoing trans proof[[\n";
411 pf
.debug_print("pf::arith");
412 Debug("pf::arith") << "\n";
413 Node n1
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
414 Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1
<< "\n";
416 Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1
<< "\n";
419 bool identicalEqualities
= false;
420 bool evenLengthSequence
;
421 Node nodeAfterEqualitySequence
;
423 std::map
<size_t, Node
> childToStream
;
425 for(size_t i
= 1; i
< pf
.d_children
.size(); ++i
) {
426 std::stringstream
ss1(ss
.str()), ss2
;
429 // It is possible that we've already converted the i'th child to stream. If so,
430 // use previously stored result. Otherwise, convert and store.
432 if (childToStream
.find(i
) != childToStream
.end())
433 n2
= childToStream
[i
];
435 n2
= toStreamRecLFSC(ss2
, tp
, *(pf
.d_children
[i
]), tb
+ 1, map
);
436 childToStream
[i
] = n2
;
439 // The following branch is dedicated to handling sequences of identical equalities,
440 // i.e. trans[ a=b, a=b, a=b ].
442 // There are two cases:
443 // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
445 // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
446 // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
447 // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
448 // and use it to determine which option we need.
449 if(n2
.getKind() == kind::EQUAL
) {
450 if (((n1
[0] == n2
[0]) && (n1
[1] == n2
[1])) || ((n1
[0] == n2
[1]) && (n1
[1] == n2
[0]))) {
451 // We are in a sequence of identical equalities
453 Debug("pf::arith") << "Detected identical equalities: " << std::endl
<< "\t" << n1
<< std::endl
;
455 if (!identicalEqualities
) {
456 // The sequence of identical equalities has started just now
457 identicalEqualities
= true;
459 Debug("pf::arith") << "The sequence is just beginning. Determining length..." << std::endl
;
461 // Determine whether the length of this sequence is odd or even.
462 evenLengthSequence
= true;
463 bool sequenceOver
= false;
466 while (j
< pf
.d_children
.size() && !sequenceOver
) {
467 std::stringstream dontCare
;
468 nodeAfterEqualitySequence
= toStreamRecLFSC(
469 dontCare
, tp
, *(pf
.d_children
[j
]), tb
+ 1, map
);
471 if (((nodeAfterEqualitySequence
[0] == n1
[0]) && (nodeAfterEqualitySequence
[1] == n1
[1])) ||
472 ((nodeAfterEqualitySequence
[0] == n1
[1]) && (nodeAfterEqualitySequence
[1] == n1
[0]))) {
473 evenLengthSequence
= !evenLengthSequence
;
481 if (evenLengthSequence
) {
482 // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
484 Debug("pf::arith") << "Equality sequence of even length" << std::endl
;
485 Debug("pf::arith") << "n1 is: " << n1
<< std::endl
;
486 Debug("pf::arith") << "n2 is: " << n2
<< std::endl
;
487 Debug("pf::arith") << "pf-d_node is: " << pf
.d_node
<< std::endl
;
488 Debug("pf::arith") << "Next node is: " << nodeAfterEqualitySequence
<< std::endl
;
490 ss
<< "(trans _ _ _ _ ";
492 // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
494 if (match(n1
[0], pf
.d_node
[0])) {
495 n1
= eqNode(n1
[0], n1
[0]);
496 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
497 } else if (match(n1
[1], pf
.d_node
[1])) {
498 n1
= eqNode(n1
[1], n1
[1]);
499 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
501 Debug("pf::arith") << "Error: identical equalities over, but hands don't match what we're proving."
506 // We have a "next node". Use it to guide us.
508 Assert(nodeAfterEqualitySequence
.getKind() == kind::EQUAL
);
510 if ((n1
[0] == nodeAfterEqualitySequence
[0]) || (n1
[0] == nodeAfterEqualitySequence
[1])) {
513 ss
<< ss1
.str() << " (symm _ _ _ " << ss1
.str() << ")";
514 n1
= eqNode(n1
[0], n1
[0]);
516 } else if ((n1
[1] == nodeAfterEqualitySequence
[0]) || (n1
[1] == nodeAfterEqualitySequence
[1])) {
519 ss
<< " (symm _ _ _ " << ss1
.str() << ")" << ss1
.str();
520 n1
= eqNode(n1
[1], n1
[1]);
523 Debug("pf::arith") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl
;
531 Debug("pf::arith") << "Equality sequence length is odd!" << std::endl
;
535 Debug("pf::arith") << "Have proven: " << n1
<< std::endl
;
540 // Ignore the redundancy.
545 if (identicalEqualities
) {
546 // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
547 identicalEqualities
= false;
550 Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2
<< "\n";
552 Debug("pf::arith") << "\ntrans proof[" << i
<< "], got n2 " << n2
<< "\n";
553 Debug("pf::arith") << (n2
.getKind() == kind::EQUAL
) << "\n";
555 if ((n1
.getNumChildren() >= 2) && (n2
.getNumChildren() >= 2)) {
556 Debug("pf::arith") << n1
[0].getId() << " " << n1
[1].getId() << " / " << n2
[0].getId() << " " << n2
[1].getId() << "\n";
557 Debug("pf::arith") << n1
[0].getId() << " " << n1
[0] << "\n";
558 Debug("pf::arith") << n1
[1].getId() << " " << n1
[1] << "\n";
559 Debug("pf::arith") << n2
[0].getId() << " " << n2
[0] << "\n";
560 Debug("pf::arith") << n2
[1].getId() << " " << n2
[1] << "\n";
561 Debug("pf::arith") << (n1
[0] == n2
[0]) << "\n";
562 Debug("pf::arith") << (n1
[1] == n2
[1]) << "\n";
563 Debug("pf::arith") << (n1
[0] == n2
[1]) << "\n";
564 Debug("pf::arith") << (n1
[1] == n2
[0]) << "\n";
567 ss
<< "(trans _ _ _ _ ";
569 if((n2
.getKind() == kind::EQUAL
) && (n1
.getKind() == kind::EQUAL
))
570 // Both elements of the transitivity rule are equalities/iffs
573 if(tb
== 1) { Debug("pf::arith") << "case 1\n"; }
574 n1
= eqNode(n1
[1], n2
[1]);
575 ss
<< "(symm _ _ _ " << ss1
.str() << ") " << ss2
.str();
576 } else if(n1
[1] == n2
[1]) {
577 if(tb
== 1) { Debug("pf::arith") << "case 2\n"; }
578 n1
= eqNode(n1
[0], n2
[0]);
579 ss
<< ss1
.str() << " (symm _ _ _ " << ss2
.str() << ")";
580 } else if(n1
[0] == n2
[1]) {
581 if(tb
== 1) { Debug("pf::arith") << "case 3\n"; }
582 n1
= eqNode(n2
[0], n1
[1]);
583 ss
<< ss2
.str() << " " << ss1
.str();
584 if(tb
== 1) { Debug("pf::arith") << "++ proved " << n1
<< "\n"; }
585 } else if(n1
[1] == n2
[0]) {
586 if(tb
== 1) { Debug("pf::arith") << "case 4\n"; }
587 n1
= eqNode(n1
[0], n2
[1]);
588 ss
<< ss1
.str() << " " << ss2
.str();
590 Warning() << "\n\ntrans proof failure at step " << i
<< "\n\n";
591 Warning() << "0 proves " << n1
<< "\n";
592 Warning() << "1 proves " << n2
<< "\n\n";
593 pf
.debug_print("pf::arith",0);
594 //toStreamRec(Warning.getStream(), pf, 0);
598 Debug("pf::arith") << "++ trans proof[" << i
<< "], now have " << n1
<< std::endl
;
599 } else if(n1
.getKind() == kind::EQUAL
) {
600 // n1 is an equality/iff, but n2 is a predicate
603 ss
<< "(symm _ _ _ " << ss1
.str() << ") (pred_eq_t _ " << ss2
.str() << ")";
604 } else if(n1
[1] == n2
) {
606 ss
<< ss1
.str() << " (pred_eq_t _ " << ss2
.str() << ")";
610 } else if(n2
.getKind() == kind::EQUAL
) {
611 // n2 is an equality/iff, but n1 is a predicate
614 ss
<< "(symm _ _ _ " << ss2
.str() << ") (pred_eq_t _ " << ss1
.str() << ")";
615 } else if(n2
[1] == n1
) {
617 ss
<< ss2
.str() << " (pred_eq_t _ " << ss1
.str() << ")";
622 // Both n1 and n2 are prediacates. Don't know what to do...
629 Debug("pf::arith") << "\n++ trans proof done, have proven " << n1
<< std::endl
;
634 Assert(!pf
.d_node
.isNull());
635 Assert(pf
.d_children
.empty());
636 Debug("pf::arith") << "theory proof: " << pf
.d_node
<< " by rule " << int(pf
.d_id
) << std::endl
;
642 ArithProof::ArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* pe
)
643 : TheoryProof(arith
, pe
), d_realMode(false)
646 theory::TheoryId
ArithProof::getTheoryId() { return theory::THEORY_ARITH
; }
647 void ArithProof::registerTerm(Expr term
) {
648 Debug("pf::arith") << "Arith register term: " << term
<< ". Kind: " << term
.getKind()
649 << ". Type: " << term
.getType() << std::endl
;
651 if (term
.getType().isReal() && !term
.getType().isInteger()) {
652 Debug("pf::arith") << "Entering real mode" << std::endl
;
656 if (term
.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term
)) {
657 d_declarations
.insert(term
);
660 // recursively declare all other terms
661 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
662 // could belong to other theories
663 d_proofEngine
->registerTerm(term
[i
]);
667 void LFSCArithProof::printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
668 Debug("pf::arith") << "Arith print term: " << term
<< ". Kind: " << term
.getKind()
669 << ". Type: " << term
.getType()
670 << ". Number of children: " << term
.getNumChildren() << std::endl
;
672 // !d_realMode <--> term.getType().isInteger()
674 Assert (theory::Theory::theoryOf(term
) == theory::THEORY_ARITH
);
675 switch (term
.getKind()) {
677 case kind::CONST_RATIONAL
: {
678 Assert (term
.getNumChildren() == 0);
679 Assert (term
.getType().isInteger() || term
.getType().isReal());
681 const Rational
& r
= term
.getConst
<Rational
>();
684 os
<< (!d_realMode
? "(a_int " : "(a_real ");
693 os
<< r
.abs().getNumerator();
695 os
<< r
.getDenominator();
707 Assert (term
.getNumChildren() == 1);
708 Assert (term
.getType().isInteger() || term
.getType().isReal());
709 os
<< (!d_realMode
? "(u-_Int " : "(u-_Real ");
710 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
716 Assert (term
.getNumChildren() >= 2);
718 std::stringstream paren
;
719 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
720 os
<< (!d_realMode
? "(+_Int " : "(+_Real ");
721 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
726 d_proofEngine
->printBoundTerm(term
[term
.getNumChildren() - 1], os
, map
);
732 Assert (term
.getNumChildren() >= 2);
734 std::stringstream paren
;
735 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
736 os
<< (!d_realMode
? "(-_Int " : "(-_Real ");
737 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
742 d_proofEngine
->printBoundTerm(term
[term
.getNumChildren() - 1], os
, map
);
748 Assert (term
.getNumChildren() >= 2);
750 std::stringstream paren
;
751 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
752 os
<< (!d_realMode
? "(*_Int " : "(*_Real ");
753 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
758 d_proofEngine
->printBoundTerm(term
[term
.getNumChildren() - 1], os
, map
);
764 case kind::DIVISION_TOTAL
: {
765 Assert (term
.getNumChildren() >= 2);
767 std::stringstream paren
;
768 for (unsigned i
= 0; i
< term
.getNumChildren() - 1; ++i
) {
769 os
<< (!d_realMode
? "(/_Int " : "(/_Real ");
770 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
775 d_proofEngine
->printBoundTerm(term
[term
.getNumChildren() - 1], os
, map
);
781 Assert (term
.getNumChildren() == 2);
782 os
<< (!d_realMode
? "(>_Int " : "(>_Real ");
783 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
785 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
790 Assert (term
.getNumChildren() == 2);
791 os
<< (!d_realMode
? "(>=_Int " : "(>=_Real ");
792 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
794 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
799 Assert (term
.getNumChildren() == 2);
800 os
<< (!d_realMode
? "(<_Int " : "(<_Real ");
801 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
803 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
808 Assert (term
.getNumChildren() == 2);
809 os
<< (!d_realMode
? "(<=_Int " : "(<=_Real ");
810 d_proofEngine
->printBoundTerm(term
[0], os
, map
);
812 d_proofEngine
->printBoundTerm(term
[1], os
, map
);
817 Debug("pf::arith") << "Default printing of term: " << term
<< std::endl
;
823 void LFSCArithProof::printOwnedSort(Type type
, std::ostream
& os
) {
824 Debug("pf::arith") << "Arith print sort: " << type
<< std::endl
;
826 if (type
.isInteger() && d_realMode
) {
827 // If in "real mode", don't use type Int for, e.g., equality.
834 void LFSCArithProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
) {
835 os
<< " ;; Arith Theory Lemma \n;;";
836 for (unsigned i
= 0; i
< lemma
.size(); ++i
) {
837 os
<< lemma
[i
] <<" ";
840 //os << " (clausify_false trust)";
841 ArithProof::printTheoryLemmaProof(lemma
, os
, paren
, map
);
844 void LFSCArithProof::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
847 void LFSCArithProof::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
848 for (ExprSet::const_iterator it
= d_declarations
.begin(); it
!= d_declarations
.end(); ++it
) {
850 Assert(term
.isVariable());
851 os
<< "(% " << ProofManager::sanitize(term
) << " ";
853 os
<< term
.getType() << ")\n";
858 void LFSCArithProof::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
859 // Nothing to do here at this point.
862 void LFSCArithProof::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
863 // Nothing to do here at this point.
866 } /* CVC4 namespace */