1 /********************* */
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Yoni Zohar
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/uf_proof.h"
21 #include "proof/proof_manager.h"
22 #include "proof/simplify_boolean_node.h"
23 #include "theory/uf/theory_uf.h"
27 void ProofUF::toStream(std::ostream
& out
) const
33 void ProofUF::toStream(std::ostream
& out
, const ProofLetMap
& map
) const
35 Trace("theory-proof-debug") << "; Print UF proof..." << std::endl
;
36 //AJR : carry this further?
37 toStreamLFSC(out
, ProofManager::getUfProof(), *d_proof
, map
);
40 void ProofUF::toStreamLFSC(std::ostream
& out
,
42 const theory::eq::EqProof
& pf
,
43 const ProofLetMap
& map
)
45 Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl
;
46 Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl
;
47 pf
.debug_print("lfsc-uf");
48 Debug("lfsc-uf") << std::endl
;
49 toStreamRecLFSC( out
, tp
, pf
, 0, map
);
52 Node
ProofUF::toStreamRecLFSC(std::ostream
& out
,
54 const theory::eq::EqProof
& pf
,
56 const ProofLetMap
& map
)
58 Debug("pf::uf") << std::endl
60 << "toStreamRecLFSC called. tb = " << tb
61 << " . proof:" << std::endl
;
64 // Special case: false was an input, so the proof is just "false".
65 if (pf
.d_id
== theory::eq::MERGED_THROUGH_EQUALITY
&&
66 pf
.d_node
== NodeManager::currentNM()->mkConst(false)) {
67 out
<< "(clausify_false ";
68 out
<< ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
69 out
<< ")" << std::endl
;
73 std::shared_ptr
<theory::eq::EqProof
> subTrans
=
74 std::make_shared
<theory::eq::EqProof
>();
76 int neg
= tp
->assertAndPrint(pf
, map
, subTrans
);
79 std::stringstream ss
, ss2
;
80 Debug("pf::uf") << "\nsubtrans has " << subTrans
->d_children
.size() << " children\n";
81 bool disequalityFound
= (neg
>= 0);
83 if(!disequalityFound
|| subTrans
->d_children
.size() >= 2) {
84 n1
= toStreamRecLFSC(ss
, tp
, *subTrans
, 1, map
);
86 n1
= toStreamRecLFSC(ss
, tp
, *(subTrans
->d_children
[0]), 1, map
);
87 Debug("pf::uf") << "\nsubTrans unique child "
88 << subTrans
->d_children
[0]->d_id
89 << " was proven\ngot: " << n1
<< std::endl
;
92 Debug("pf::uf") << "\nhave proven: " << n1
<< std::endl
;
94 out
<< "(clausify_false (contra _ ";
95 if (disequalityFound
) {
96 Node n2
= pf
.d_children
[neg
]->d_node
;
97 Assert(n2
.getKind() == kind::NOT
);
99 Debug("pf::uf") << "n2 is " << n2
[0] << std::endl
;
101 if (n2
[0].getNumChildren() > 0)
103 Debug("pf::uf") << "\nn2[0]: " << n2
[0][0] << std::endl
;
105 if (n1
.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1
[1] << std::endl
; }
107 if(n2
[0].getKind() == kind::APPLY_UF
) {
108 out
<< "(trans _ _ _ _ ";
110 if (n1
[0] == n2
[0]) {
111 out
<< "(symm _ _ _ ";
115 Assert(n1
[1] == n2
[0]);
118 out
<< "(pred_eq_f _ " << ProofManager::getLitName(n2
[0]) << ")) t_t_neq_f))" << std::endl
;
119 } else if (n2
[0].getKind() == kind::BOOLEAN_TERM_VARIABLE
) {
120 out
<< ss
.str() << " " << ProofManager::getLitName(n2
[0]) << "))";
122 Assert((n1
[0] == n2
[0][0] && n1
[1] == n2
[0][1]) || (n1
[1] == n2
[0][0] && n1
[0] == n2
[0][1]));
123 if(n1
[1] == n2
[0][0]) {
124 out
<< "(symm _ _ _ " << ss
.str() << ")";
128 out
<< " " << ProofManager::getLitName(n2
[0]) << "))" << std::endl
;
132 Assert(n2
.getKind() == kind::EQUAL
);
133 Assert((n1
[0] == n2
[0] && n1
[1] == n2
[1]) || (n1
[1] == n2
[0] && n1
[0] == n2
[1]));
137 ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(
138 out
, n1
[0].toExpr(), n1
[1].toExpr(), map
);
139 out
<< "))" << std::endl
;
146 case theory::eq::MERGED_THROUGH_CONGRUENCE
: {
147 Debug("pf::uf") << "\nok, looking at congruence:\n";
148 pf
.debug_print("pf::uf");
149 std::stack
<const theory::eq::EqProof
*> stk
;
150 for (const theory::eq::EqProof
* pf2
= &pf
;
151 pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
;
152 pf2
= pf2
->d_children
[0].get()) {
153 Assert(!pf2
->d_node
.isNull());
154 Assert(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
155 || pf2
->d_node
.getKind() == kind::BUILTIN
156 || pf2
->d_node
.getKind() == kind::APPLY_UF
157 || pf2
->d_node
.getKind() == kind::SELECT
158 || pf2
->d_node
.getKind() == kind::STORE
);
159 Assert(pf2
->d_children
.size() == 2);
160 out
<< "(cong _ _ _ _ _ _ ";
163 Assert(stk
.top()->d_children
[0]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
);
164 NodeBuilder
<> b1(kind::PARTIAL_APPLY_UF
), b2(kind::PARTIAL_APPLY_UF
);
165 const theory::eq::EqProof
* pf2
= stk
.top();
167 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
168 Node n1
= toStreamRecLFSC(out
, tp
, *(pf2
->d_children
[0]), tb
+ 1, map
);
170 std::stringstream ss
;
171 Node n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
172 Debug("pf::uf") << "\nok, in FIRST cong[" << stk
.size() << "]" << "\n";
173 pf2
->debug_print("pf::uf");
174 Debug("pf::uf") << "looking at " << pf2
->d_node
<< "\n";
175 Debug("pf::uf") << " " << n1
<< "\n";
176 Debug("pf::uf") << " " << n2
<< "\n";
178 if (tp
->match(pf2
->d_node
, n1
[0]))
181 Debug("pf::uf") << "SIDE IS 0\n";
186 Debug("pf::uf") << "SIDE IS 1\n";
188 if (!tp
->match(pf2
->d_node
, n1
[1]))
190 Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
191 pf2
->d_children
[0]->debug_print("pf::uf");
193 Assert(tp
->match(pf2
->d_node
, n1
[1]));
196 if (n1
[side
].getKind() == kind::APPLY_UF
197 || n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
198 || n1
[side
].getKind() == kind::SELECT
199 || n1
[side
].getKind() == kind::STORE
)
201 if (n1
[side
].getKind() == kind::APPLY_UF
202 || n1
[side
].getKind() == kind::PARTIAL_APPLY_UF
)
204 b1
<< n1
[side
].getOperator();
206 b1
<< ProofManager::currentPM()->mkOp(n1
[side
].getOperator());
208 b1
.append(n1
[side
].begin(), n1
[side
].end());
212 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
) {
213 if (n1
[1 - side
].getKind() == kind::PARTIAL_APPLY_UF
214 || n1
[1 - side
].getKind() == kind::APPLY_UF
)
216 b2
<< n1
[1-side
].getOperator();
218 b2
<< ProofManager::currentPM()->mkOp(n1
[1-side
].getOperator());
220 b2
.append(n1
[1-side
].begin(), n1
[1-side
].end());
224 Debug("pf::uf") << "pf2->d_node " << pf2
->d_node
<< std::endl
;
225 Debug("pf::uf") << "b1.getNumChildren() " << b1
.getNumChildren() << std::endl
;
226 Debug("pf::uf") << "n1 " << n1
<< std::endl
;
227 Debug("pf::uf") << "n2 " << n2
<< std::endl
;
228 Debug("pf::uf") << "side " << side
<< std::endl
;
229 if(pf2
->d_node
[b1
.getNumChildren() - (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[side
]) {
234 Assert(pf2
->d_node
[b1
.getNumChildren() - (pf2
->d_node
.getMetaKind() == kind::metakind::PARAMETERIZED
? 0 : 1)] == n2
[1-side
]);
237 out
<< "(symm _ _ _ " << ss
.str() << ")";
240 while(!stk
.empty()) {
242 Debug("pf::uf") << "\nMORE TO DO\n";
246 Assert(pf2
->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
);
249 n2
= toStreamRecLFSC(ss
, tp
, *(pf2
->d_children
[1]), tb
+ 1, map
);
250 Debug("pf::uf") << "\nok, in cong[" << stk
.size() << "]" << "\n";
251 Debug("pf::uf") << "looking at " << pf2
->d_node
<< "\n";
252 Debug("pf::uf") << " " << n1
<< "\n";
253 Debug("pf::uf") << " " << n2
<< "\n";
254 Debug("pf::uf") << " " << b1
<< "\n";
255 Debug("pf::uf") << " " << b2
<< "\n";
256 if(pf2
->d_node
[b1
.getNumChildren()] == n2
[side
]) {
261 Assert(pf2
->d_node
[b1
.getNumChildren()] == n2
[1-side
]);
264 out
<< "(symm _ _ _ " << ss
.str() << ")";
270 Debug("pf::uf") << "at end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
271 if(pf2
->d_node
.getKind() == kind::PARTIAL_APPLY_UF
) {
272 Assert(n1
== pf2
->d_node
);
274 if(n1
.getOperator().getType().getNumChildren() == n1
.getNumChildren() + 1) {
275 if(ProofManager::currentPM()->hasOp(n1
.getOperator())) {
276 b1
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
278 b1
.clear(kind::APPLY_UF
);
279 b1
<< n1
.getOperator();
281 b1
.append(n1
.begin(), n1
.end());
283 Debug("pf::uf") << "at[2] end assert, got " << pf2
->d_node
<< " and " << n1
<< std::endl
;
284 if(pf2
->d_node
.getKind() == kind::APPLY_UF
) {
285 Assert(n1
== pf2
->d_node
);
288 if(n2
.getOperator().getType().getNumChildren() == n2
.getNumChildren() + 1) {
289 if(ProofManager::currentPM()->hasOp(n2
.getOperator())) {
290 b2
.clear(ProofManager::currentPM()->lookupOp(n2
.getOperator()).getConst
<Kind
>());
292 b2
.clear(kind::APPLY_UF
);
293 b2
<< n2
.getOperator();
295 b2
.append(n2
.begin(), n2
.end());
298 Node n
= (side
== 0 ? n1
.eqNode(n2
) : n2
.eqNode(n1
));
300 Debug("pf::uf") << "\ncong proved: " << n
<< "\n";
305 case theory::eq::MERGED_THROUGH_REFLEXIVITY
:
307 Assert(!pf
.d_node
.isNull());
308 Assert(pf
.d_children
.empty());
310 tp
->printTerm(NodeManager::currentNM()->toExpr(pf
.d_node
), out
, map
);
312 return pf
.d_node
.eqNode(pf
.d_node
);
314 case theory::eq::MERGED_THROUGH_EQUALITY
:
315 Assert(!pf
.d_node
.isNull());
316 Assert(pf
.d_children
.empty());
317 out
<< ProofManager::getLitName(pf
.d_node
.negate());
320 case theory::eq::MERGED_THROUGH_TRANS
: {
321 Assert(!pf
.d_node
.isNull());
322 Assert(pf
.d_children
.size() >= 2);
323 std::stringstream ss
;
324 Debug("pf::uf") << "\ndoing trans proof[[\n";
325 pf
.debug_print("pf::uf");
326 Debug("pf::uf") << "\n";
328 pf
.d_children
[0]->d_node
= simplifyBooleanNode(pf
.d_children
[0]->d_node
);
330 Node n1
= toStreamRecLFSC(ss
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
331 Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1
<< "\n";
334 Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1
<< "\n";
337 bool identicalEqualities
= false;
338 bool evenLengthSequence
;
339 std::stringstream dontCare
;
340 Node nodeAfterEqualitySequence
=
341 toStreamRecLFSC(dontCare
, tp
, *(pf
.d_children
[0]), tb
+ 1, map
);
343 std::map
<size_t, Node
> childToStream
;
344 std::stringstream
ss1(ss
.str()), ss2
;
345 std::pair
<Node
, Node
> nodePair
;
346 for(size_t i
= 1; i
< pf
.d_children
.size(); ++i
) {
347 std::stringstream
ss1(ss
.str()), ss2
;
350 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
352 // It is possible that we've already converted the i'th child to stream.
354 // use previously stored result. Otherwise, convert and store.
356 if (childToStream
.find(i
) != childToStream
.end())
357 n2
= childToStream
[i
];
360 n2
= toStreamRecLFSC(ss2
, tp
, *(pf
.d_children
[i
]), tb
+ 1, map
);
361 childToStream
[i
] = n2
;
364 // The following branch is dedicated to handling sequences of identical
366 // i.e. trans[ a=b, a=b, a=b ].
368 // There are two cases:
369 // 1. The number of equalities is odd. Then, the sequence can be
370 // collapsed to just one equality,
372 // 2. The number of equalities is even. Now, we have two options: a=a
373 // or b=b. To determine this,
374 // we look at the node after the equality sequence. If it needs a,
375 // we go for a=a; and if it needs
376 // b, we go for b=b. If there is no following node, we look at the
377 // goal of the transitivity proof,
378 // and use it to determine which option we need.
379 if (n2
.getKind() == kind::EQUAL
)
381 if (((n1
[0] == n2
[0]) && (n1
[1] == n2
[1]))
382 || ((n1
[0] == n2
[1]) && (n1
[1] == n2
[0])))
384 // We are in a sequence of identical equalities
386 Debug("pf::uf") << "Detected identical equalities: " << std::endl
387 << "\t" << n1
<< std::endl
;
389 if (!identicalEqualities
)
391 // The sequence of identical equalities has started just now
392 identicalEqualities
= true;
395 << "The sequence is just beginning. Determining length..."
398 // Determine whether the length of this sequence is odd or even.
399 evenLengthSequence
= true;
400 bool sequenceOver
= false;
403 while (j
< pf
.d_children
.size() && !sequenceOver
)
405 std::stringstream dontCare
;
406 nodeAfterEqualitySequence
= toStreamRecLFSC(
407 dontCare
, tp
, *(pf
.d_children
[j
]), tb
+ 1, map
);
409 if (((nodeAfterEqualitySequence
[0] == n1
[0])
410 && (nodeAfterEqualitySequence
[1] == n1
[1]))
411 || ((nodeAfterEqualitySequence
[0] == n1
[1])
412 && (nodeAfterEqualitySequence
[1] == n1
[0])))
414 evenLengthSequence
= !evenLengthSequence
;
425 tp
->identicalEqualitiesPrinterHelper(evenLengthSequence
,
432 nodeAfterEqualitySequence
);
434 nodeAfterEqualitySequence
= nodePair
.second
;
439 // Ignore the redundancy.
444 if (identicalEqualities
) {
445 // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
446 identicalEqualities
= false;
449 Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2
<< "\n";
451 Debug("pf::uf") << "\ntrans proof[" << i
<< "], got n2 " << n2
<< "\n";
452 Debug("pf::uf") << (n2
.getKind() == kind::EQUAL
) << "\n";
454 if ((n1
.getNumChildren() >= 2) && (n2
.getNumChildren() >= 2)) {
455 Debug("pf::uf") << n1
[0].getId() << " " << n1
[1].getId() << " / " << n2
[0].getId() << " " << n2
[1].getId() << "\n";
456 Debug("pf::uf") << n1
[0].getId() << " " << n1
[0] << "\n";
457 Debug("pf::uf") << n1
[1].getId() << " " << n1
[1] << "\n";
458 Debug("pf::uf") << n2
[0].getId() << " " << n2
[0] << "\n";
459 Debug("pf::uf") << n2
[1].getId() << " " << n2
[1] << "\n";
460 Debug("pf::uf") << (n1
[0] == n2
[0]) << "\n";
461 Debug("pf::uf") << (n1
[1] == n2
[1]) << "\n";
462 Debug("pf::uf") << (n1
[0] == n2
[1]) << "\n";
463 Debug("pf::uf") << (n1
[1] == n2
[0]) << "\n";
467 ss
<< "(trans _ _ _ _ ";
469 if(n2
.getKind() == kind::EQUAL
&& n1
.getKind() == kind::EQUAL
)
470 // Both elements of the transitivity rule are equalities/iffs
473 if(tb
== 1) { Debug("pf::uf") << "case 1\n"; }
474 n1
= n1
[1].eqNode(n2
[1]);
475 ss
<< "(symm _ _ _ " << ss1
.str() << ") " << ss2
.str();
476 } else if(n1
[1] == n2
[1]) {
477 if(tb
== 1) { Debug("pf::uf") << "case 2\n"; }
478 n1
= n1
[0].eqNode(n2
[0]);
479 ss
<< ss1
.str() << " (symm _ _ _ " << ss2
.str() << ")";
480 } else if(n1
[0] == n2
[1]) {
481 if(tb
== 1) { Debug("pf::uf") << "case 3\n"; }
482 n1
= n2
[0].eqNode(n1
[1]);
483 ss
<< ss2
.str() << " " << ss1
.str();
484 if(tb
== 1) { Debug("pf::uf") << "++ proved " << n1
<< "\n"; }
485 } else if(n1
[1] == n2
[0]) {
486 if(tb
== 1) { Debug("pf::uf") << "case 4\n"; }
487 n1
= n1
[0].eqNode(n2
[1]);
488 ss
<< ss1
.str() << " " << ss2
.str();
490 Warning() << "\n\ntrans proof failure at step " << i
<< "\n\n";
491 Warning() << "0 proves " << n1
<< "\n";
492 Warning() << "1 proves " << n2
<< "\n\n";
493 pf
.debug_print("pf::uf",0);
494 //toStreamRec(Warning.getStream(), pf, 0);
498 Debug("pf::uf") << "++ trans proof[" << i
<< "], now have " << n1
<< std::endl
;
499 } else if(n1
.getKind() == kind::EQUAL
) {
500 // n1 is an equality/iff, but n2 is a predicate
502 n1
= n1
[1].eqNode(NodeManager::currentNM()->mkConst(true));
503 ss
<< "(symm _ _ _ " << ss1
.str() << ") (pred_eq_t _ " << ss2
.str() << ")";
504 } else if(n1
[1] == n2
) {
505 n1
= n1
[0].eqNode(NodeManager::currentNM()->mkConst(true));
506 ss
<< ss1
.str() << " (pred_eq_t _ " << ss2
.str() << ")";
510 } else if(n2
.getKind() == kind::EQUAL
) {
511 // n2 is an equality/iff, but n1 is a predicate
513 n1
= n2
[1].eqNode(NodeManager::currentNM()->mkConst(true));
514 ss
<< "(symm _ _ _ " << ss2
.str() << ") (pred_eq_t _ " << ss1
.str() << ")";
515 } else if(n2
[1] == n1
) {
516 n1
= n2
[0].eqNode(NodeManager::currentNM()->mkConst(true));
517 ss
<< ss2
.str() << " (pred_eq_t _ " << ss1
.str() << ")";
522 // Both n1 and n2 are predicates.
523 // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2))
524 if (n1
.getKind() == kind::NOT
) {
525 Assert(n2
.getKind() == kind::NOT
);
526 Assert(pf
.d_node
[0] == n1
[0] || pf
.d_node
[0] == n2
[0]);
527 Assert(pf
.d_node
[1] == n1
[0] || pf
.d_node
[1] == n2
[0]);
528 Assert(n1
[0].getKind() == kind::BOOLEAN_TERM_VARIABLE
);
529 Assert(n2
[0].getKind() == kind::BOOLEAN_TERM_VARIABLE
);
531 if (pf
.d_node
[0] == n1
[0]) {
532 ss
<< "(false_preds_equal _ _ " << ss1
.str() << " " << ss2
.str() << ") ";
533 ss
<< "(pred_refl_neg _ " << ss2
.str() << ")";
535 ss
<< "(false_preds_equal _ _ " << ss2
.str() << " " << ss1
.str() << ") ";
536 ss
<< "(pred_refl_neg _ " << ss1
.str() << ")";
540 } else if (n1
.getKind() == kind::BOOLEAN_TERM_VARIABLE
) {
541 Assert(n2
.getKind() == kind::BOOLEAN_TERM_VARIABLE
);
542 Assert(pf
.d_node
[0] == n1
|| pf
.d_node
[0] == n2
);
543 Assert(pf
.d_node
[1] == n1
|| pf
.d_node
[2] == n2
);
545 if (pf
.d_node
[0] == n1
) {
546 ss
<< "(true_preds_equal _ _ " << ss1
.str() << " " << ss2
.str() << ") ";
547 ss
<< "(pred_refl_pos _ " << ss2
.str() << ")";
549 ss
<< "(true_preds_equal _ _ " << ss2
.str() << " " << ss1
.str() << ") ";
550 ss
<< "(pred_refl_pos _ " << ss1
.str() << ")";
563 Debug("pf::uf") << "\n++ trans proof done, have proven " << n1
<< std::endl
;
568 Assert(!pf
.d_node
.isNull());
569 Assert(pf
.d_children
.empty());
570 Debug("pf::uf") << "theory proof: " << pf
.d_node
<< " by rule " << int(pf
.d_id
) << std::endl
;
576 UFProof::UFProof(theory::uf::TheoryUF
* uf
, TheoryProofEngine
* pe
)
577 : TheoryProof(uf
, pe
)
580 theory::TheoryId
UFProof::getTheoryId() { return theory::THEORY_UF
; }
581 void UFProof::registerTerm(Expr term
) {
582 // already registered
583 if (d_declarations
.find(term
) != d_declarations
.end())
586 Type type
= term
.getType();
588 // declare uninterpreted sorts
589 d_sorts
.insert(type
);
592 if (term
.getKind() == kind::APPLY_UF
) {
593 Expr function
= term
.getOperator();
594 d_declarations
.insert(function
);
597 if (term
.isVariable()) {
598 d_declarations
.insert(term
);
601 if (term
.getKind() == kind::BOOLEAN_TERM_VARIABLE
) {
602 // Ensure cnf literals
604 ProofManager::currentPM()->ensureLiteral(
605 asNode
.eqNode(NodeManager::currentNM()->mkConst(true)));
606 ProofManager::currentPM()->ensureLiteral(
607 asNode
.eqNode(NodeManager::currentNM()->mkConst(false)));
611 // recursively declare all other terms
612 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
613 // could belong to other theories
614 d_proofEngine
->registerTerm(term
[i
]);
618 void LFSCUFProof::printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
619 Debug("pf::uf") << std::endl
<< "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term
<< std::endl
;
621 Assert (theory::Theory::theoryOf(term
) == theory::THEORY_UF
);
623 if (term
.getKind() == kind::VARIABLE
||
624 term
.getKind() == kind::SKOLEM
||
625 term
.getKind() == kind::BOOLEAN_TERM_VARIABLE
) {
630 Assert (term
.getKind() == kind::APPLY_UF
);
632 if(term
.getType().isBoolean()) {
635 Expr func
= term
.getOperator();
636 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
640 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
642 bool convertToBool
= (term
[i
].getType().isBoolean() && !d_proofEngine
->printsAsBool(term
[i
]));
643 if (convertToBool
) os
<< "(f_to_b ";
644 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
645 if (convertToBool
) os
<< ")";
648 if(term
.getType().isBoolean()) {
653 void LFSCUFProof::printOwnedSort(Type type
, std::ostream
& os
) {
654 Debug("pf::uf") << std::endl
<< "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type
<< std::endl
;
656 Assert (type
.isSort());
660 void LFSCUFProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
) {
661 os
<< " ;; UF Theory Lemma \n;;";
662 for (unsigned i
= 0; i
< lemma
.size(); ++i
) {
663 os
<< lemma
[i
] <<" ";
666 //os << " (clausify_false trust)";
667 UFProof::printTheoryLemmaProof(lemma
, os
, paren
, map
);
670 void LFSCUFProof::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
671 for (TypeSet::const_iterator it
= d_sorts
.begin(); it
!= d_sorts
.end(); ++it
) {
672 if (!ProofManager::currentPM()->wasPrinted(*it
)) {
673 os
<< "(% " << *it
<< " sort\n";
675 ProofManager::currentPM()->markPrinted(*it
);
680 void LFSCUFProof::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
681 // declaring the terms
682 Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl
;
684 for (ExprSet::const_iterator it
= d_declarations
.begin(); it
!= d_declarations
.end(); ++it
) {
687 os
<< "(% " << ProofManager::sanitize(term
) << " ";
690 Type type
= term
.getType();
691 if (type
.isFunction()) {
692 std::ostringstream fparen
;
693 FunctionType ftype
= (FunctionType
)type
;
694 std::vector
<Type
> args
= ftype
.getArgTypes();
695 args
.push_back(ftype
.getRangeType());
697 for (unsigned i
= 0; i
< args
.size(); i
++) {
698 Type arg_type
= args
[i
];
700 d_proofEngine
->printSort(arg_type
, os
);
701 if (i
< args
.size() - 2) {
706 os
<< fparen
.str() << "))\n";
708 Assert (term
.isVariable());
714 Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl
;
717 void LFSCUFProof::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
718 // Nothing to do here at this point.
721 void LFSCUFProof::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
722 // Nothing to do here at this point.
725 bool LFSCUFProof::printsAsBool(const Node
&n
) {
726 if (n
.getKind() == kind::BOOLEAN_TERM_VARIABLE
)
732 void LFSCUFProof::printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
) {
733 Node falseNode
= NodeManager::currentNM()->mkConst(false);
734 Node trueNode
= NodeManager::currentNM()->mkConst(true);
736 Assert(c1
== falseNode
.toExpr() || c1
== trueNode
.toExpr());
737 Assert(c2
== falseNode
.toExpr() || c2
== trueNode
.toExpr());
740 if (c1
== trueNode
.toExpr())
743 os
<< "(symm _ _ _ t_t_neq_f)";
746 } /* namespace CVC4 */