1 /********************* */
2 /*! \file theory_proof.cpp
4 ** Top contributors (to current version):
5 ** Guy Katz, Liana Hadarean, 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 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
17 #include "proof/theory_proof.h"
19 #include "base/cvc4_assert.h"
20 #include "context/context.h"
21 #include "options/bv_options.h"
22 #include "options/proof_options.h"
23 #include "proof/arith_proof.h"
24 #include "proof/array_proof.h"
25 #include "proof/clause_id.h"
26 #include "proof/cnf_proof.h"
27 #include "proof/proof_manager.h"
28 #include "proof/proof_output_channel.h"
29 #include "proof/proof_utils.h"
30 #include "proof/resolution_bitvector_proof.h"
31 #include "proof/sat_proof.h"
32 #include "proof/simplify_boolean_node.h"
33 #include "proof/uf_proof.h"
34 #include "prop/sat_solver_types.h"
35 #include "smt/smt_engine.h"
36 #include "smt/smt_engine_scope.h"
37 #include "smt_util/node_visitor.h"
38 #include "theory/arrays/theory_arrays.h"
39 #include "theory/bv/theory_bv.h"
40 #include "theory/output_channel.h"
41 #include "theory/term_registration_visitor.h"
42 #include "theory/uf/theory_uf.h"
43 #include "theory/valuation.h"
44 #include "util/hash.h"
45 #include "util/proof.h"
49 using proof::LFSCBitVectorProof
;
50 using proof::ResolutionBitVectorProof
;
52 unsigned CVC4::ProofLetCount::counter
= 0;
53 static unsigned LET_COUNT
= 1;
55 TheoryProofEngine::TheoryProofEngine()
56 : d_registrationCache()
57 , d_theoryProofTable()
59 d_theoryProofTable
[theory::THEORY_BOOL
] = new LFSCBooleanProof(this);
62 TheoryProofEngine::~TheoryProofEngine() {
63 TheoryProofTable::iterator it
= d_theoryProofTable
.begin();
64 TheoryProofTable::iterator end
= d_theoryProofTable
.end();
65 for (; it
!= end
; ++it
) {
70 void TheoryProofEngine::registerTheory(theory::Theory
* th
) {
72 theory::TheoryId id
= th
->getId();
73 if(d_theoryProofTable
.find(id
) == d_theoryProofTable
.end()) {
75 Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id
<< std::endl
;
77 if (id
== theory::THEORY_UF
) {
78 d_theoryProofTable
[id
] = new LFSCUFProof((theory::uf::TheoryUF
*)th
, this);
82 if (id
== theory::THEORY_BV
) {
83 auto bv_theory
= static_cast<theory::bv::TheoryBV
*>(th
);
84 ResolutionBitVectorProof
* bvp
= new LFSCBitVectorProof(bv_theory
, this);
85 d_theoryProofTable
[id
] = bvp
;
89 if (id
== theory::THEORY_ARRAYS
) {
90 d_theoryProofTable
[id
] = new LFSCArrayProof((theory::arrays::TheoryArrays
*)th
, this);
94 if (id
== theory::THEORY_ARITH
) {
95 d_theoryProofTable
[id
] = new LFSCArithProof((theory::arith::TheoryArith
*)th
, this);
99 // TODO other theories
104 void TheoryProofEngine::finishRegisterTheory(theory::Theory
* th
) {
106 theory::TheoryId id
= th
->getId();
107 if (id
== theory::THEORY_BV
) {
108 Assert(d_theoryProofTable
.find(id
) != d_theoryProofTable
.end());
109 ResolutionBitVectorProof
* bvp
=
110 (ResolutionBitVectorProof
*)d_theoryProofTable
[id
];
111 ((theory::bv::TheoryBV
*)th
)->setResolutionProofLog(bvp
);
117 TheoryProof
* TheoryProofEngine::getTheoryProof(theory::TheoryId id
) {
118 // The UF theory handles queries for the Builtin theory.
119 if (id
== theory::THEORY_BUILTIN
) {
120 Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl
;
121 id
= theory::THEORY_UF
;
124 if (d_theoryProofTable
.find(id
) == d_theoryProofTable
.end()) {
125 std::stringstream ss
;
126 ss
<< "Error! Proofs not yet supported for the following theory: " << id
<< std::endl
;
127 InternalError(ss
.str().c_str());
130 return d_theoryProofTable
[id
];
133 void TheoryProofEngine::markTermForFutureRegistration(Expr term
, theory::TheoryId id
) {
134 d_exprToTheoryIds
[term
].insert(id
);
137 void TheoryProofEngine::printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
) {
138 Assert(c1
.isConst());
139 Assert(c2
.isConst());
141 Assert(theory::Theory::theoryOf(c1
) == theory::Theory::theoryOf(c2
));
142 getTheoryProof(theory::Theory::theoryOf(c1
))->printConstantDisequalityProof(os
, c1
, c2
, globalLetMap
);
145 void TheoryProofEngine::registerTerm(Expr term
) {
146 Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering term: " << term
<< std::endl
;
148 if (d_registrationCache
.count(term
)) {
152 Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering NEW term: " << term
<< std::endl
;
154 theory::TheoryId theory_id
= theory::Theory::theoryOf(term
);
156 Debug("pf::tp::register") << "Term's theory( " << term
<< " ) = " << theory_id
<< std::endl
;
158 // don't need to register boolean terms
159 if (theory_id
== theory::THEORY_BUILTIN
||
160 term
.getKind() == kind::ITE
) {
161 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
162 registerTerm(term
[i
]);
164 d_registrationCache
.insert(term
);
168 if (!supportedTheory(theory_id
)) return;
170 // Register the term with its owner theory
171 getTheoryProof(theory_id
)->registerTerm(term
);
173 // A special case: the array theory needs to know of every skolem, even if
174 // it belongs to another theory (e.g., a BV skolem)
175 if (ProofManager::getSkolemizationManager()->isSkolem(term
) && theory_id
!= theory::THEORY_ARRAYS
) {
176 Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering a non-array skolem: " << term
<< std::endl
;
177 getTheoryProof(theory::THEORY_ARRAYS
)->registerTerm(term
);
180 d_registrationCache
.insert(term
);
183 theory::TheoryId
TheoryProofEngine::getTheoryForLemma(const prop::SatClause
* clause
) {
184 ProofManager
* pm
= ProofManager::currentPM();
186 std::set
<Node
> nodes
;
187 for(unsigned i
= 0; i
< clause
->size(); ++i
) {
188 prop::SatLiteral lit
= (*clause
)[i
];
189 Node node
= pm
->getCnfProof()->getAtom(lit
.getSatVariable());
190 Expr atom
= node
.toExpr();
191 if (atom
.isConst()) {
192 Assert (atom
== utils::mkTrue());
196 nodes
.insert(lit
.isNegated() ? node
.notNode() : node
);
199 // Ensure that the lemma is in the database.
200 Assert (pm
->getCnfProof()->haveProofRecipe(nodes
));
201 return pm
->getCnfProof()->getProofRecipe(nodes
).getTheory();
204 void LFSCTheoryProofEngine::bind(Expr term
, ProofLetMap
& map
, Bindings
& let_order
) {
205 ProofLetMap::iterator it
= map
.find(term
);
206 if (it
!= map
.end()) {
207 ProofLetCount
& count
= it
->second
;
211 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
212 bind(term
[i
], map
, let_order
);
214 unsigned new_id
= ProofLetCount::newId();
215 map
[term
] = ProofLetCount(new_id
);
216 let_order
.push_back(LetOrderElement(term
, new_id
));
219 void LFSCTheoryProofEngine::printLetTerm(Expr term
, std::ostream
& os
) {
222 bind(term
, map
, let_order
);
223 std::ostringstream paren
;
224 for (unsigned i
= 0; i
< let_order
.size(); ++i
) {
225 Expr current_expr
= let_order
[i
].expr
;
226 unsigned let_id
= let_order
[i
].id
;
227 ProofLetMap::const_iterator it
= map
.find(current_expr
);
228 Assert (it
!= map
.end());
229 unsigned let_count
= it
->second
.count
;
231 // skip terms that only appear once
232 if (let_count
<= LET_COUNT
) {
236 os
<< "(@ let" <<let_id
<< " ";
237 printTheoryTerm(current_expr
, os
, map
);
240 unsigned last_let_id
= let_order
.back().id
;
241 Expr last
= let_order
.back().expr
;
242 unsigned last_count
= map
.find(last
)->second
.count
;
243 if (last_count
<= LET_COUNT
) {
244 printTheoryTerm(last
, os
, map
);
247 os
<< " let" << last_let_id
;
252 void LFSCTheoryProofEngine::printTheoryTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
253 theory::TheoryId theory_id
= theory::Theory::theoryOf(term
);
255 // boolean terms and ITEs are special because they
256 // are common to all theories
257 if (theory_id
== theory::THEORY_BUILTIN
||
258 term
.getKind() == kind::ITE
||
259 term
.getKind() == kind::EQUAL
) {
260 printCoreTerm(term
, os
, map
);
263 // dispatch to proper theory
264 getTheoryProof(theory_id
)->printOwnedTerm(term
, os
, map
);
267 void LFSCTheoryProofEngine::printSort(Type type
, std::ostream
& os
) {
269 getTheoryProof(theory::THEORY_UF
)->printOwnedSort(type
, os
);
272 if (type
.isBitVector()) {
273 getTheoryProof(theory::THEORY_BV
)->printOwnedSort(type
, os
);
277 if (type
.isArray()) {
278 getTheoryProof(theory::THEORY_ARRAYS
)->printOwnedSort(type
, os
);
282 if (type
.isInteger() || type
.isReal()) {
283 getTheoryProof(theory::THEORY_ARITH
)->printOwnedSort(type
, os
);
287 if (type
.isBoolean()) {
288 getTheoryProof(theory::THEORY_BOOL
)->printOwnedSort(type
, os
);
295 void LFSCTheoryProofEngine::performExtraRegistrations() {
296 ExprToTheoryIds::const_iterator it
;
297 for (it
= d_exprToTheoryIds
.begin(); it
!= d_exprToTheoryIds
.end(); ++it
) {
298 if (d_registrationCache
.count(it
->first
)) { // Only register if the term appeared
299 TheoryIdSet::const_iterator theoryIt
;
300 for (theoryIt
= it
->second
.begin(); theoryIt
!= it
->second
.end(); ++theoryIt
) {
301 Debug("pf::tp") << "\tExtra registration of term " << it
->first
302 << " with theory: " << *theoryIt
<< std::endl
;
303 Assert(supportedTheory(*theoryIt
));
304 getTheoryProof(*theoryIt
)->registerTerm(it
->first
);
310 void LFSCTheoryProofEngine::registerTermsFromAssertions() {
311 ProofManager::assertions_iterator it
= ProofManager::currentPM()->begin_assertions();
312 ProofManager::assertions_iterator end
= ProofManager::currentPM()->end_assertions();
314 for(; it
!= end
; ++it
) {
318 performExtraRegistrations();
321 void LFSCTheoryProofEngine::printAssertions(std::ostream
& os
, std::ostream
& paren
) {
322 Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl
<< std::endl
;
324 ProofManager::assertions_iterator it
= ProofManager::currentPM()->begin_assertions();
325 ProofManager::assertions_iterator end
= ProofManager::currentPM()->end_assertions();
327 for (; it
!= end
; ++it
) {
328 Debug("pf::tp") << "printAssertions: assertion is: " << *it
<< std::endl
;
329 os
<< "(% " << ProofManager::currentPM()->getInputFormulaName(*it
) << " (th_holds ";
331 // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
332 ProofLetMap dummyMap
;
334 bool convertFromBool
= (it
->getType().isBoolean() && printsAsBool(*it
));
335 if (convertFromBool
) os
<< "(p_app ";
336 printBoundTerm(*it
, os
, dummyMap
);
337 if (convertFromBool
) os
<< ")";
343 Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl
<< std::endl
;
346 void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet
& rewrites
,
348 std::ostream
& paren
) {
349 Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl
<< std::endl
;
351 NodePairSet::const_iterator it
;
353 for (it
= rewrites
.begin(); it
!= rewrites
.end(); ++it
) {
354 Debug("pf::tp") << "printLemmaRewrites: " << it
->first
<< " --> " << it
->second
<< std::endl
;
357 Node n2
= it
->second
;
358 Assert(n1
.toExpr() == utils::mkFalse() ||
359 theory::Theory::theoryOf(n1
) == theory::Theory::theoryOf(n2
));
361 std::ostringstream rewriteRule
;
362 rewriteRule
<< ".lrr" << d_assertionToRewrite
.size();
364 os
<< "(th_let_pf _ ";
365 getTheoryProof(theory::Theory::theoryOf(n1
))->printRewriteProof(os
, n1
, n2
);
366 os
<< "(\\ " << rewriteRule
.str() << "\n";
368 d_assertionToRewrite
[it
->first
] = rewriteRule
.str();
369 Debug("pf::tp") << "d_assertionToRewrite[" << it
->first
<< "] = " << rewriteRule
.str() << std::endl
;
373 Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl
<< std::endl
;
376 void LFSCTheoryProofEngine::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
377 Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl
<< std::endl
;
379 TheoryProofTable::const_iterator it
= d_theoryProofTable
.begin();
380 TheoryProofTable::const_iterator end
= d_theoryProofTable
.end();
381 for (; it
!= end
; ++it
) {
382 it
->second
->printSortDeclarations(os
, paren
);
385 Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations done" << std::endl
<< std::endl
;
388 void LFSCTheoryProofEngine::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
389 Debug("pf::tp") << "LFSCTheoryProofEngine::printTermDeclarations called" << std::endl
<< std::endl
;
391 TheoryProofTable::const_iterator it
= d_theoryProofTable
.begin();
392 TheoryProofTable::const_iterator end
= d_theoryProofTable
.end();
393 for (; it
!= end
; ++it
) {
394 it
->second
->printTermDeclarations(os
, paren
);
397 Debug("pf::tp") << "LFSCTheoryProofEngine::printTermDeclarations done" << std::endl
<< std::endl
;
400 void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
401 Debug("pf::tp") << "LFSCTheoryProofEngine::printDeferredDeclarations called" << std::endl
;
403 TheoryProofTable::const_iterator it
= d_theoryProofTable
.begin();
404 TheoryProofTable::const_iterator end
= d_theoryProofTable
.end();
405 for (; it
!= end
; ++it
) {
406 it
->second
->printDeferredDeclarations(os
, paren
);
410 void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
411 Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl
;
413 TheoryProofTable::const_iterator it
= d_theoryProofTable
.begin();
414 TheoryProofTable::const_iterator end
= d_theoryProofTable
.end();
415 for (; it
!= end
; ++it
) {
416 it
->second
->printAliasingDeclarations(os
, paren
, globalLetMap
);
420 void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause
& lemmas
) {
421 Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl
<< std::endl
;
423 ProofManager
* pm
= ProofManager::currentPM();
424 for (IdToSatClause::const_iterator it
= lemmas
.begin(); it
!= lemmas
.end(); ++it
) {
425 ClauseId id
= it
->first
;
426 Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id
<< std::endl
;
427 const prop::SatClause
* clause
= it
->second
;
428 std::set
<Node
> nodes
;
429 for(unsigned i
= 0; i
< clause
->size(); ++i
) {
430 prop::SatLiteral lit
= (*clause
)[i
];
431 Node node
= pm
->getCnfProof()->getAtom(lit
.getSatVariable());
432 if (node
.isConst()) {
433 Assert (node
.toExpr() == utils::mkTrue());
436 nodes
.insert(lit
.isNegated() ? node
.notNode() : node
);
439 LemmaProofRecipe recipe
= pm
->getCnfProof()->getProofRecipe(nodes
);
440 recipe
.dump("pf::dumpLemmas");
443 Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl
<< std::endl
;
446 // TODO: this function should be moved into the BV prover.
447 void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause
& lemmas
, std::ostream
& os
) {
448 // BitVector theory is special case: must know all conflicts needed
449 // ahead of time for resolution proof lemmas
450 std::vector
<Expr
> bv_lemmas
;
452 for (IdToSatClause::const_iterator it
= lemmas
.begin(); it
!= lemmas
.end(); ++it
) {
453 const prop::SatClause
* clause
= it
->second
;
455 std::vector
<Expr
> conflict
;
456 std::set
<Node
> conflictNodes
;
457 for(unsigned i
= 0; i
< clause
->size(); ++i
) {
458 prop::SatLiteral lit
= (*clause
)[i
];
459 Node node
= ProofManager::currentPM()->getCnfProof()->getAtom(lit
.getSatVariable());
460 Expr atom
= node
.toExpr();
462 // The literals (true) and (not false) are omitted from conflicts
463 if (atom
.isConst()) {
464 Assert (atom
== utils::mkTrue() ||
465 (atom
== utils::mkFalse() && lit
.isNegated()));
469 Expr expr_lit
= lit
.isNegated() ? atom
.notExpr() : atom
;
470 conflict
.push_back(expr_lit
);
471 conflictNodes
.insert(lit
.isNegated() ? node
.notNode() : node
);
474 LemmaProofRecipe recipe
= ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes
);
476 unsigned numberOfSteps
= recipe
.getNumSteps();
478 prop::SatClause currentClause
= *clause
;
479 std::vector
<Expr
> currentClauseExpr
= conflict
;
481 for (unsigned i
= 0; i
< numberOfSteps
; ++i
) {
482 const LemmaProofRecipe::ProofStep
* currentStep
= recipe
.getStep(i
);
484 if (currentStep
->getTheory() != theory::THEORY_BV
) {
488 // If any rewrites took place, we need to update the conflict clause accordingly
489 std::set
<Node
> missingAssertions
= recipe
.getMissingAssertionsForStep(i
);
490 std::map
<Node
, Node
> explanationToMissingAssertion
;
491 std::set
<Node
>::iterator assertionIt
;
492 for (assertionIt
= missingAssertions
.begin();
493 assertionIt
!= missingAssertions
.end();
495 Node negated
= (*assertionIt
).negate();
496 explanationToMissingAssertion
[recipe
.getExplanation(negated
)] = negated
;
499 currentClause
= *clause
;
500 currentClauseExpr
= conflict
;
502 for (unsigned j
= 0; j
< i
; ++j
) {
503 // Literals already used in previous steps need to be negated
504 Node previousLiteralNode
= recipe
.getStep(j
)->getLiteral();
506 // If this literal is the result of a rewrite, we need to translate it
507 if (explanationToMissingAssertion
.find(previousLiteralNode
) !=
508 explanationToMissingAssertion
.end()) {
509 previousLiteralNode
= explanationToMissingAssertion
[previousLiteralNode
];
512 Node previousLiteralNodeNegated
= previousLiteralNode
.negate();
513 prop::SatLiteral previousLiteralNegated
=
514 ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated
);
516 currentClause
.push_back(previousLiteralNegated
);
517 currentClauseExpr
.push_back(previousLiteralNodeNegated
.toExpr());
520 // If we're in the final step, the last literal is Null and should not be added.
521 // Otherwise, the current literal does NOT need to be negated
522 Node currentLiteralNode
= currentStep
->getLiteral();
524 if (currentLiteralNode
!= Node()) {
525 prop::SatLiteral currentLiteral
=
526 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode
);
528 currentClause
.push_back(currentLiteral
);
529 currentClauseExpr
.push_back(currentLiteralNode
.toExpr());
532 bv_lemmas
.push_back(utils::mkSortedExpr(kind::OR
, currentClauseExpr
));
536 ResolutionBitVectorProof
* bv
= ProofManager::getBitVectorProof();
537 bv
->finalizeConflicts(bv_lemmas
);
538 // bv->printResolutionProof(os, paren, letMap);
541 void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause
& lemmas
,
545 os
<< " ;; Theory Lemmas \n";
546 Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl
;
548 if (Debug
.isOn("pf::dumpLemmas")) {
549 dumpTheoryLemmas(lemmas
);
552 // finalizeBvConflicts(lemmas, os, paren, map);
553 ProofManager::getBitVectorProof()->printResolutionProof(os
, paren
, map
);
555 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
) {
556 Assert (lemmas
.size() == 1);
557 // nothing more to do (no combination with eager so far)
561 ProofManager
* pm
= ProofManager::currentPM();
562 Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl
;
564 for (IdToSatClause::const_iterator it
= lemmas
.begin(); it
!= lemmas
.end(); ++it
) {
565 ClauseId id
= it
->first
;
566 const prop::SatClause
* clause
= it
->second
;
568 Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
571 std::vector
<Expr
> clause_expr
;
572 std::set
<Node
> clause_expr_nodes
;
573 for(unsigned i
= 0; i
< clause
->size(); ++i
) {
574 prop::SatLiteral lit
= (*clause
)[i
];
575 Node node
= pm
->getCnfProof()->getAtom(lit
.getSatVariable());
576 Expr atom
= node
.toExpr();
577 if (atom
.isConst()) {
578 Assert (atom
== utils::mkTrue());
581 Expr expr_lit
= lit
.isNegated() ? atom
.notExpr(): atom
;
582 clause_expr
.push_back(expr_lit
);
583 clause_expr_nodes
.insert(lit
.isNegated() ? node
.notNode() : node
);
586 LemmaProofRecipe recipe
= pm
->getCnfProof()->getProofRecipe(clause_expr_nodes
);
588 if (recipe
.simpleLemma()) {
589 // In a simple lemma, there will be no propositional resolution in the end
591 Debug("pf::tp") << "Simple lemma" << std::endl
;
592 // Printing the clause as it appears in resolution proof
593 os
<< "(satlem _ _ ";
594 std::ostringstream clause_paren
;
595 pm
->getCnfProof()->printClause(*clause
, os
, clause_paren
);
597 // Find and handle missing assertions, due to rewrites
598 std::set
<Node
> missingAssertions
= recipe
.getMissingAssertionsForStep(0);
599 if (!missingAssertions
.empty()) {
600 Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl
;
603 std::set
<Node
>::const_iterator missingAssertion
;
604 for (missingAssertion
= missingAssertions
.begin();
605 missingAssertion
!= missingAssertions
.end();
606 ++missingAssertion
) {
608 Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion
<< std::endl
;
609 Assert(recipe
.wasRewritten(missingAssertion
->negate()));
610 Node explanation
= recipe
.getExplanation(missingAssertion
->negate()).negate();
611 Debug("pf::tp") << "Found explanation: " << explanation
<< std::endl
;
613 // We have a missing assertion.
614 // rewriteIt->first is the assertion after the rewrite (the explanation),
615 // rewriteIt->second is the original assertion that needs to be fed into the theory.
619 for (k
= 0; k
< clause_expr
.size(); ++k
) {
620 if (clause_expr
[k
] == explanation
.toExpr()) {
627 Debug("pf::tp") << "Replacing theory assertion "
633 clause_expr
[k
] = missingAssertion
->toExpr();
635 std::ostringstream rewritten
;
637 if (missingAssertion
->getKind() == kind::NOT
&& (*missingAssertion
)[0].toExpr() == utils::mkFalse()) {
638 rewritten
<< "(or_elim_2 _ _ ";
639 rewritten
<< "(not_not_intro _ ";
640 rewritten
<< pm
->getLitName(explanation
);
641 rewritten
<< ") (iff_elim_2 _ _ ";
642 rewritten
<< d_assertionToRewrite
[missingAssertion
->negate()];
646 rewritten
<< "(or_elim_1 _ _ ";
647 rewritten
<< "(not_not_intro _ ";
648 rewritten
<< pm
->getLitName(explanation
);
649 rewritten
<< ") (iff_elim_1 _ _ ";
650 rewritten
<< d_assertionToRewrite
[missingAssertion
->negate()];
654 Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
655 << pm
->getLitName(*missingAssertion
) << " --> " << rewritten
.str()
656 << ", explanation = " << explanation
657 << std::endl
<< std::endl
;
659 pm
->addRewriteFilter(pm
->getLitName(*missingAssertion
), rewritten
.str());
662 // Query the appropriate theory for a proof of this clause
663 theory::TheoryId theory_id
= getTheoryForLemma(clause
);
664 Debug("pf::tp") << "Get theory lemma from " << theory_id
<< "..." << std::endl
;
665 getTheoryProof(theory_id
)->printTheoryLemmaProof(clause_expr
, os
, paren
, map
);
667 // Turn rewrite filter OFF
668 pm
->clearRewriteFilters();
670 Debug("pf::tp") << "Get theory lemma from " << theory_id
<< "... DONE!" << std::endl
;
671 os
<< clause_paren
.str();
672 os
<< "( \\ " << pm
->getLemmaClauseName(id
) <<"\n";
674 } else { // This is a composite lemma
676 unsigned numberOfSteps
= recipe
.getNumSteps();
677 prop::SatClause currentClause
= *clause
;
678 std::vector
<Expr
> currentClauseExpr
= clause_expr
;
680 for (unsigned i
= 0; i
< numberOfSteps
; ++i
) {
681 const LemmaProofRecipe::ProofStep
* currentStep
= recipe
.getStep(i
);
683 currentClause
= *clause
;
684 currentClauseExpr
= clause_expr
;
686 for (unsigned j
= 0; j
< i
; ++j
) {
687 // Literals already used in previous steps need to be negated
688 Node previousLiteralNode
= recipe
.getStep(j
)->getLiteral();
689 Node previousLiteralNodeNegated
= previousLiteralNode
.negate();
690 prop::SatLiteral previousLiteralNegated
=
691 ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated
);
692 currentClause
.push_back(previousLiteralNegated
);
693 currentClauseExpr
.push_back(previousLiteralNodeNegated
.toExpr());
696 // If the current literal is NULL, can ignore (final step)
697 // Otherwise, the current literal does NOT need to be negated
698 Node currentLiteralNode
= currentStep
->getLiteral();
699 if (currentLiteralNode
!= Node()) {
700 prop::SatLiteral currentLiteral
=
701 ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode
);
703 currentClause
.push_back(currentLiteral
);
704 currentClauseExpr
.push_back(currentLiteralNode
.toExpr());
707 os
<< "(satlem _ _ ";
708 std::ostringstream clause_paren
;
710 pm
->getCnfProof()->printClause(currentClause
, os
, clause_paren
);
712 // query appropriate theory for proof of clause
713 theory::TheoryId theory_id
= currentStep
->getTheory();
714 Debug("pf::tp") << "Get theory lemma from " << theory_id
<< "..." << std::endl
;
716 std::set
<Node
> missingAssertions
= recipe
.getMissingAssertionsForStep(i
);
717 if (!missingAssertions
.empty()) {
718 Debug("pf::tp") << "Have missing assertions for this step!" << std::endl
;
721 // Turn rewrite filter ON
722 std::set
<Node
>::const_iterator missingAssertion
;
723 for (missingAssertion
= missingAssertions
.begin();
724 missingAssertion
!= missingAssertions
.end();
725 ++missingAssertion
) {
727 Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion
<< std::endl
;
729 Assert(recipe
.wasRewritten(missingAssertion
->negate()));
730 Node explanation
= recipe
.getExplanation(missingAssertion
->negate()).negate();
732 Debug("pf::tp") << "Found explanation: " << explanation
<< std::endl
;
734 // We have a missing assertion.
735 // rewriteIt->first is the assertion after the rewrite (the explanation),
736 // rewriteIt->second is the original assertion that needs to be fed into the theory.
740 for (k
= 0; k
< currentClauseExpr
.size(); ++k
) {
741 if (currentClauseExpr
[k
] == explanation
.toExpr()) {
749 Debug("pf::tp") << "Replacing theory assertion "
750 << currentClauseExpr
[k
]
755 currentClauseExpr
[k
] = missingAssertion
->toExpr();
757 std::ostringstream rewritten
;
759 if (missingAssertion
->getKind() == kind::NOT
&& (*missingAssertion
)[0].toExpr() == utils::mkFalse()) {
760 rewritten
<< "(or_elim_2 _ _ ";
761 rewritten
<< "(not_not_intro _ ";
762 rewritten
<< pm
->getLitName(explanation
);
763 rewritten
<< ") (iff_elim_2 _ _ ";
764 rewritten
<< d_assertionToRewrite
[missingAssertion
->negate()];
768 rewritten
<< "(or_elim_1 _ _ ";
769 rewritten
<< "(not_not_intro _ ";
770 rewritten
<< pm
->getLitName(explanation
);
771 rewritten
<< ") (iff_elim_1 _ _ ";
772 rewritten
<< d_assertionToRewrite
[missingAssertion
->negate()];
776 Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
777 << pm
->getLitName(*missingAssertion
) << " --> " << rewritten
.str()
778 << "explanation = " << explanation
779 << std::endl
<< std::endl
;
781 pm
->addRewriteFilter(pm
->getLitName(*missingAssertion
), rewritten
.str());
784 getTheoryProof(theory_id
)->printTheoryLemmaProof(currentClauseExpr
, os
, paren
, map
);
786 // Turn rewrite filter OFF
787 pm
->clearRewriteFilters();
789 Debug("pf::tp") << "Get theory lemma from " << theory_id
<< "... DONE!" << std::endl
;
790 os
<< clause_paren
.str();
791 os
<< "( \\ " << pm
->getLemmaClauseName(id
) << "s" << i
<<"\n";
795 Assert(numberOfSteps
>= 2);
797 os
<< "(satlem_simplify _ _ _ ";
798 for (unsigned i
= 0; i
< numberOfSteps
- 1; ++i
) {
799 // Resolve step i with step i + 1
800 if (recipe
.getStep(i
)->getLiteral().getKind() == kind::NOT
) {
806 os
<< pm
->getLemmaClauseName(id
) << "s" << i
;
810 os
<< pm
->getLemmaClauseName(id
) << "s" << numberOfSteps
- 1 << " ";
813 for (int i
= numberOfSteps
- 2; i
>= 0; --i
) {
814 v
= ProofManager::currentPM()->getCnfProof()->getLiteral(recipe
.getStep(i
)->getLiteral());
815 os
<< ProofManager::getVarName(v
.getSatVariable(), "") << ") ";
818 os
<< "( \\ " << pm
->getLemmaClauseName(id
) << "\n";
824 void LFSCTheoryProofEngine::printBoundTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
825 Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term
<< " ) " << std::endl
;
827 ProofLetMap::const_iterator it
= map
.find(term
);
828 if (it
!= map
.end()) {
829 unsigned id
= it
->second
.id
;
830 unsigned count
= it
->second
.count
;
832 if (count
> LET_COUNT
) {
838 printTheoryTerm(term
, os
, map
);
841 void LFSCTheoryProofEngine::printCoreTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
842 if (term
.isVariable()) {
843 os
<< ProofManager::sanitize(term
);
847 Kind k
= term
.getKind();
851 os
<< (term
.getType().isBoolean() ? "(ifte ": "(ite _ ");
853 bool booleanCase
= term
[0].getType().isBoolean();
854 if (booleanCase
&& printsAsBool(term
[0])) os
<< "(p_app ";
855 printBoundTerm(term
[0], os
, map
);
856 if (booleanCase
&& printsAsBool(term
[0])) os
<< ")";
859 printBoundTerm(term
[1], os
, map
);
861 printBoundTerm(term
[2], os
, map
);
867 bool booleanCase
= term
[0].getType().isBoolean();
874 printSort(term
[0].getType(), os
);
878 if (booleanCase
&& printsAsBool(term
[0])) os
<< "(p_app ";
879 printBoundTerm(term
[0], os
, map
);
880 if (booleanCase
&& printsAsBool(term
[0])) os
<< ")";
884 if (booleanCase
&& printsAsBool(term
[1])) os
<< "(p_app ";
885 printBoundTerm(term
[1], os
, map
);
886 if (booleanCase
&& printsAsBool(term
[1])) os
<< ") ";
893 // Distinct nodes can have any number of chidlren.
894 Assert (term
.getNumChildren() >= 2);
896 if (term
.getNumChildren() == 2) {
898 printSort(term
[0].getType(), os
);
900 printBoundTerm(term
[0], os
, map
);
902 printBoundTerm(term
[1], os
, map
);
905 unsigned numOfPairs
= term
.getNumChildren() * (term
.getNumChildren() - 1) / 2;
906 for (unsigned i
= 1; i
< numOfPairs
; ++i
) {
910 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
911 for (unsigned j
= i
+ 1; j
< term
.getNumChildren(); ++j
) {
912 if ((i
!= 0) || (j
!= 1)) {
914 printSort(term
[0].getType(), os
);
916 printBoundTerm(term
[i
], os
, map
);
918 printBoundTerm(term
[j
], os
, map
);
922 printSort(term
[0].getType(), os
);
924 printBoundTerm(term
[0], os
, map
);
926 printBoundTerm(term
[1], os
, map
);
936 // LFSC doesn't allow declarations with variable numbers of
937 // arguments, so we have to flatten chained operators, like =.
938 Kind op
= term
.getOperator().getConst
<Chain
>().getOperator();
940 bool booleanCase
= false;
941 if (op
==kind::EQUAL
&& term
[0].getType().isBoolean()) {
942 booleanCase
= term
[0].getType().isBoolean();
945 op_str
= utils::toLFSCKind(op
);
947 size_t n
= term
.getNumChildren();
948 std::ostringstream paren
;
949 for(size_t i
= 1; i
< n
; ++i
) {
951 os
<< "(" << utils::toLFSCKind(kind::AND
) << " ";
954 os
<< "(" << op_str
<< " ";
955 if (booleanCase
&& printsAsBool(term
[i
- 1])) os
<< "(p_app ";
956 printBoundTerm(term
[i
- 1], os
, map
);
957 if (booleanCase
&& printsAsBool(term
[i
- 1])) os
<< ")";
959 if (booleanCase
&& printsAsBool(term
[i
])) os
<< "(p_app ";
960 printBoundTerm(term
[i
], os
, map
);
961 if (booleanCase
&& printsAsBool(term
[i
])) os
<< ")";
977 void TheoryProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
980 const ProofLetMap
& map
) {
981 // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
982 Assert(d_theory
!=NULL
);
984 context::UserContext fakeContext
;
985 ProofOutputChannel oc
;
986 theory::Valuation
v(NULL
);
987 //make new copy of theory
989 Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory
->getId() << std::endl
;
991 if (d_theory
->getId()==theory::THEORY_UF
) {
992 th
= new theory::uf::TheoryUF(&fakeContext
, &fakeContext
, oc
, v
,
993 ProofManager::currentPM()->getLogicInfo(),
995 } else if (d_theory
->getId()==theory::THEORY_ARRAYS
) {
996 th
= new theory::arrays::TheoryArrays(&fakeContext
, &fakeContext
, oc
, v
,
997 ProofManager::currentPM()->getLogicInfo(),
999 } else if (d_theory
->getId() == theory::THEORY_ARITH
) {
1000 Trace("theory-proof-debug") << "Arith proofs currently not supported. Use 'trust'" << std::endl
;
1001 os
<< " (clausify_false trust)";
1004 InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic());
1007 Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->ProduceProofs()" << std::endl
;
1008 th
->produceProofs();
1009 Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl
;
1011 MyPreRegisterVisitor
preRegVisitor(th
);
1012 for (unsigned i
=0; i
<lemma
.size(); i
++) {
1013 Node strippedLit
= (lemma
[i
].getKind() == kind::NOT
) ? lemma
[i
][0] : lemma
[i
];
1014 if (strippedLit
.getKind() == kind::EQUAL
||
1015 d_theory
->getId() == theory::Theory::theoryOf(strippedLit
)) {
1016 Node lit
= Node::fromExpr( lemma
[i
] ).negate();
1017 Trace("pf::tp") << "; preregistering and asserting " << lit
<< std::endl
;
1018 NodeVisitor
<MyPreRegisterVisitor
>::run(preRegVisitor
, lit
);
1019 th
->assertFact(lit
, false);
1023 Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl
;
1024 th
->check(theory::Theory::EFFORT_FULL
);
1025 Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->check() DONE" << std::endl
;
1027 if(!oc
.hasConflict()) {
1028 Trace("pf::tp") << "; conflict is null" << std::endl
;
1029 Node lastLemma
= oc
.getLastLemma();
1030 Assert(!lastLemma
.isNull());
1031 Trace("pf::tp") << "; ++ but got lemma: " << lastLemma
<< std::endl
;
1033 if (lastLemma
.getKind() == kind::OR
) {
1034 Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl
;
1035 for (unsigned i
= 0; i
< lastLemma
.getNumChildren(); ++i
) {
1036 if (lastLemma
[i
].getKind() == kind::NOT
) {
1037 Trace("pf::tp") << "; asserting fact: " << lastLemma
[i
][0] << std::endl
;
1038 th
->assertFact(lastLemma
[i
][0], false);
1041 Trace("pf::tp") << "; asserting fact: " << lastLemma
[i
].notNode() << std::endl
;
1042 th
->assertFact(lastLemma
[i
].notNode(), false);
1048 Assert(oc
.getLastLemma().getKind() == kind::NOT
);
1049 Debug("pf::tp") << "NOT lemma" << std::endl
;
1050 Trace("pf::tp") << "; asserting fact: " << oc
.getLastLemma()[0]
1052 th
->assertFact(oc
.getLastLemma()[0], false);
1055 // Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl;
1056 // Trace("pf::tp") << "; asserting " << oc.d_lemma[1].negate() << std::endl;
1057 // th->assertFact(oc.d_lemma[1].negate(), false);
1060 th
->check(theory::Theory::EFFORT_FULL
);
1062 Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl
;
1063 oc
.getConflictProof().toStream(os
, map
);
1064 Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl
;
1067 Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl
;
1069 Debug("pf::tp") << "About to delete the theory solver used for proving the lemma: DONE! " << std::endl
;
1072 bool TheoryProofEngine::supportedTheory(theory::TheoryId id
) {
1073 return (id
== theory::THEORY_ARRAYS
||
1074 id
== theory::THEORY_ARITH
||
1075 id
== theory::THEORY_BV
||
1076 id
== theory::THEORY_UF
||
1077 id
== theory::THEORY_BOOL
);
1080 bool TheoryProofEngine::printsAsBool(const Node
&n
) {
1081 if (!n
.getType().isBoolean()) {
1085 theory::TheoryId theory_id
= theory::Theory::theoryOf(n
);
1086 return getTheoryProof(theory_id
)->printsAsBool(n
);
1089 BooleanProof::BooleanProof(TheoryProofEngine
* proofEngine
)
1090 : TheoryProof(NULL
, proofEngine
)
1093 void BooleanProof::registerTerm(Expr term
) {
1094 Assert (term
.getType().isBoolean());
1096 if (term
.isVariable() && d_declarations
.find(term
) == d_declarations
.end()) {
1097 d_declarations
.insert(term
);
1100 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
1101 d_proofEngine
->registerTerm(term
[i
]);
1105 theory::TheoryId
BooleanProof::getTheoryId() { return theory::THEORY_BOOL
; }
1106 void LFSCBooleanProof::printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
) {
1107 Node falseNode
= NodeManager::currentNM()->mkConst(false);
1108 Node trueNode
= NodeManager::currentNM()->mkConst(true);
1110 Assert(c1
== falseNode
.toExpr() || c1
== trueNode
.toExpr());
1111 Assert(c2
== falseNode
.toExpr() || c2
== trueNode
.toExpr());
1114 if (c1
== trueNode
.toExpr())
1117 os
<< "(negsymm _ _ _ t_t_neq_f)";
1120 void LFSCBooleanProof::printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
1121 Assert (term
.getType().isBoolean());
1122 if (term
.isVariable()) {
1123 os
<< ProofManager::sanitize(term
);
1127 Kind k
= term
.getKind();
1131 if (options::lfscLetification() && term
.getNumChildren() > 2) {
1132 // If letification is on, the entire term is probably a let expression.
1133 // However, we need to transform it from (and a b c) into (and a (and b c)) form first.
1134 Node currentExpression
= term
[term
.getNumChildren() - 1];
1135 for (int i
= term
.getNumChildren() - 2; i
>= 0; --i
) {
1136 NodeBuilder
<> builder(k
);
1138 builder
<< currentExpression
.toExpr();
1139 currentExpression
= builder
;
1142 // The let map should already have the current expression.
1143 ProofLetMap::const_iterator it
= map
.find(currentExpression
.toExpr());
1144 if (it
!= map
.end()) {
1145 unsigned id
= it
->second
.id
;
1146 unsigned count
= it
->second
.count
;
1148 if (count
> LET_COUNT
) {
1155 // If letification is off or there were 2 children, same treatment as the other cases.
1156 // (No break is intentional).
1160 // print the Boolean operators
1161 os
<< "(" << utils::toLFSCKind(k
);
1162 if(term
.getNumChildren() > 2) {
1163 // LFSC doesn't allow declarations with variable numbers of
1164 // arguments, so we have to flatten these N-ary versions.
1165 std::ostringstream paren
;
1167 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
1169 if (printsAsBool(term
[i
])) os
<< "(p_app ";
1170 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
1171 if (printsAsBool(term
[i
])) os
<< ")";
1174 if(i
< term
.getNumChildren() - 2) {
1175 os
<< "(" << utils::toLFSCKind(k
) << " ";
1179 os
<< paren
.str() << ")";
1181 // this is for binary and unary operators
1182 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
) {
1184 if (printsAsBool(term
[i
])) os
<< "(p_app ";
1185 d_proofEngine
->printBoundTerm(term
[i
], os
, map
);
1186 if (printsAsBool(term
[i
])) os
<< ")";
1192 case kind::CONST_BOOLEAN
:
1193 os
<< (term
.getConst
<bool>() ? "true" : "false");
1202 void LFSCBooleanProof::printOwnedSort(Type type
, std::ostream
& os
) {
1203 Assert (type
.isBoolean());
1207 void LFSCBooleanProof::printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1208 // Nothing to do here at this point.
1211 void LFSCBooleanProof::printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1212 for (ExprSet::const_iterator it
= d_declarations
.begin(); it
!= d_declarations
.end(); ++it
) {
1215 os
<< "(% " << ProofManager::sanitize(term
) << " (term ";
1216 printSort(term
.getType(), os
);
1222 void LFSCBooleanProof::printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) {
1223 // Nothing to do here at this point.
1226 void LFSCBooleanProof::printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) {
1227 // Nothing to do here at this point.
1230 void LFSCBooleanProof::printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
1232 std::ostream
& paren
,
1233 const ProofLetMap
& map
) {
1234 Unreachable("No boolean lemmas yet!");
1237 bool LFSCBooleanProof::printsAsBool(const Node
&n
)
1239 Kind k
= n
.getKind();
1241 case kind::BOOLEAN_TERM_VARIABLE
:
1242 case kind::VARIABLE
:
1250 void TheoryProof::printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
) {
1251 // By default, we just print a trust statement. Specific theories can implement
1254 os
<< "(trust_f (not (= _ ";
1255 d_proofEngine
->printBoundTerm(c1
, os
, globalLetMap
);
1257 d_proofEngine
->printBoundTerm(c2
, os
, globalLetMap
);
1261 void TheoryProof::printRewriteProof(std::ostream
& os
, const Node
&n1
, const Node
&n2
) {
1262 // This is the default for a rewrite proof: just a trust statement.
1263 ProofLetMap emptyMap
;
1264 os
<< "(trust_f (iff ";
1265 d_proofEngine
->printBoundTerm(n1
.toExpr(), os
, emptyMap
);
1267 d_proofEngine
->printBoundTerm(n2
.toExpr(), os
, emptyMap
);
1271 bool TheoryProof::match(TNode n1
, TNode n2
)
1273 theory::TheoryId theoryId
= this->getTheoryId();
1274 ProofManager
* pm
= ProofManager::currentPM();
1275 bool ufProof
= (theoryId
== theory::THEORY_UF
);
1276 Debug(ufProof
? "pf::uf" : "mgd") << "match " << n1
<< " " << n2
<< std::endl
;
1279 n1
= pm
->lookupOp(n1
);
1283 n2
= pm
->lookupOp(n2
);
1285 Debug(ufProof
? "pf::uf" : "mgd") << "+ match " << n1
<< " " << n2
1289 Debug("pf::array") << "+ match: step 1" << std::endl
;
1296 if (n1
.getType().isFunction() && n2
.hasOperator())
1298 if (pm
->hasOp(n2
.getOperator()))
1300 return n1
== pm
->lookupOp(n2
.getOperator());
1304 return n1
== n2
.getOperator();
1308 if (n2
.getType().isFunction() && n1
.hasOperator())
1310 if (pm
->hasOp(n1
.getOperator()))
1312 return n2
== pm
->lookupOp(n1
.getOperator());
1316 return n2
== n1
.getOperator();
1320 if (n1
.hasOperator() && n2
.hasOperator()
1321 && n1
.getOperator() != n2
.getOperator())
1324 || !((n1
.getKind() == kind::SELECT
1325 && n2
.getKind() == kind::PARTIAL_SELECT_0
)
1326 || (n1
.getKind() == kind::SELECT
1327 && n2
.getKind() == kind::PARTIAL_SELECT_1
)
1328 || (n1
.getKind() == kind::PARTIAL_SELECT_1
1329 && n2
.getKind() == kind::SELECT
)
1330 || (n1
.getKind() == kind::PARTIAL_SELECT_1
1331 && n2
.getKind() == kind::PARTIAL_SELECT_0
)
1332 || (n1
.getKind() == kind::PARTIAL_SELECT_0
1333 && n2
.getKind() == kind::SELECT
)
1334 || (n1
.getKind() == kind::PARTIAL_SELECT_0
1335 && n2
.getKind() == kind::PARTIAL_SELECT_1
)))
1341 for (size_t i
= 0; i
< n1
.getNumChildren() && i
< n2
.getNumChildren(); ++i
)
1352 int TheoryProof::assertAndPrint(
1353 const theory::eq::EqProof
& pf
,
1354 const ProofLetMap
& map
,
1355 std::shared_ptr
<theory::eq::EqProof
> subTrans
,
1356 theory::eq::EqProof::PrettyPrinter
* pPrettyPrinter
)
1358 theory::TheoryId theoryId
= getTheoryId();
1360 Assert(theoryId
== theory::THEORY_UF
|| theoryId
== theory::THEORY_ARRAYS
);
1361 bool ufProof
= (theoryId
== theory::THEORY_UF
);
1362 std::string theoryName
= theory::getStatsPrefix(theoryId
);
1363 pf
.debug_print(("pf::" + theoryName
).c_str(), 0, pPrettyPrinter
);
1364 Debug("pf::" + theoryName
) << std::endl
;
1366 Assert(pf
.d_id
== theory::eq::MERGED_THROUGH_TRANS
);
1367 Assert(!pf
.d_node
.isNull());
1368 Assert(pf
.d_children
.size() >= 2);
1370 subTrans
->d_id
= theory::eq::MERGED_THROUGH_TRANS
;
1371 subTrans
->d_node
= pf
.d_node
;
1374 while (i
< pf
.d_children
.size())
1376 // special treatment for uf and not for array
1378 || pf
.d_children
[i
]->d_id
!= theory::eq::MERGED_THROUGH_CONGRUENCE
)
1380 pf
.d_children
[i
]->d_node
= simplifyBooleanNode(pf
.d_children
[i
]->d_node
);
1383 // Look for the negative clause, with which we will form a contradiction.
1384 if (!pf
.d_children
[i
]->d_node
.isNull()
1385 && pf
.d_children
[i
]->d_node
.getKind() == kind::NOT
)
1392 // Handle congruence closures over equalities.
1393 else if (pf
.d_children
[i
]->d_id
== theory::eq::MERGED_THROUGH_CONGRUENCE
1394 && pf
.d_children
[i
]->d_node
.isNull())
1396 Debug("pf::" + theoryName
) << "Handling congruence over equalities"
1399 // Gather the sequence of consecutive congruence closures.
1400 std::vector
<std::shared_ptr
<const theory::eq::EqProof
>>
1403 Debug("pf::" + theoryName
) << "Collecting congruence sequence"
1405 for (count
= 0; i
+ count
< pf
.d_children
.size()
1406 && pf
.d_children
[i
+ count
]->d_id
1407 == theory::eq::MERGED_THROUGH_CONGRUENCE
1408 && pf
.d_children
[i
+ count
]->d_node
.isNull();
1411 Debug("pf::" + theoryName
) << "Found a congruence: " << std::endl
;
1412 pf
.d_children
[i
+ count
]->debug_print(
1413 ("pf::" + theoryName
).c_str(), 0, pPrettyPrinter
);
1414 congruenceClosures
.push_back(pf
.d_children
[i
+ count
]);
1417 Debug("pf::" + theoryName
)
1418 << "Total number of congruences found: " << congruenceClosures
.size()
1421 // Determine if the "target" of the congruence sequence appears right
1422 // before or right after the sequence.
1423 bool targetAppearsBefore
= true;
1424 bool targetAppearsAfter
= true;
1426 if ((i
== 0) || (i
== 1 && neg
== 0))
1428 Debug("pf::" + theoryName
) << "Target does not appear before"
1430 targetAppearsBefore
= false;
1433 if ((i
+ count
>= pf
.d_children
.size())
1434 || (!pf
.d_children
[i
+ count
]->d_node
.isNull()
1435 && pf
.d_children
[i
+ count
]->d_node
.getKind() == kind::NOT
))
1437 Debug("pf::" + theoryName
) << "Target does not appear after"
1439 targetAppearsAfter
= false;
1442 // Flow changes between uf and array
1445 // Assert that we have precisely at least one possible clause.
1446 Assert(targetAppearsBefore
|| targetAppearsAfter
);
1448 // If both are valid, assume the one after the sequence is correct
1449 if (targetAppearsAfter
&& targetAppearsBefore
)
1451 targetAppearsBefore
= false;
1456 // Assert that we have precisely one target clause.
1457 Assert(targetAppearsBefore
!= targetAppearsAfter
);
1460 // Begin breaking up the congruences and ordering the equalities
1462 std::vector
<std::shared_ptr
<theory::eq::EqProof
>> orderedEqualities
;
1464 // Insert target clause first.
1465 if (targetAppearsBefore
)
1467 orderedEqualities
.push_back(pf
.d_children
[i
- 1]);
1468 // The target has already been added to subTrans; remove it.
1469 subTrans
->d_children
.pop_back();
1473 orderedEqualities
.push_back(pf
.d_children
[i
+ count
]);
1476 // Start with the congruence closure closest to the target clause, and
1477 // work our way back/forward.
1478 if (targetAppearsBefore
)
1480 for (unsigned j
= 0; j
< count
; ++j
)
1482 if (pf
.d_children
[i
+ j
]->d_children
[0]->d_id
1483 != theory::eq::MERGED_THROUGH_REFLEXIVITY
)
1484 orderedEqualities
.insert(orderedEqualities
.begin(),
1485 pf
.d_children
[i
+ j
]->d_children
[0]);
1486 if (pf
.d_children
[i
+ j
]->d_children
[1]->d_id
1487 != theory::eq::MERGED_THROUGH_REFLEXIVITY
)
1488 orderedEqualities
.insert(orderedEqualities
.end(),
1489 pf
.d_children
[i
+ j
]->d_children
[1]);
1494 for (unsigned j
= 0; j
< count
; ++j
)
1496 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]->d_id
1497 != theory::eq::MERGED_THROUGH_REFLEXIVITY
)
1498 orderedEqualities
.insert(
1499 orderedEqualities
.begin(),
1500 pf
.d_children
[i
+ count
- 1 - j
]->d_children
[0]);
1501 if (pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]->d_id
1502 != theory::eq::MERGED_THROUGH_REFLEXIVITY
)
1503 orderedEqualities
.insert(
1504 orderedEqualities
.end(),
1505 pf
.d_children
[i
+ count
- 1 - j
]->d_children
[1]);
1509 // Copy the result into the main transitivity proof.
1510 subTrans
->d_children
.insert(subTrans
->d_children
.end(),
1511 orderedEqualities
.begin(),
1512 orderedEqualities
.end());
1514 // Increase i to skip over the children that have been processed.
1516 if (targetAppearsAfter
)
1522 // Else, just copy the child proof as is
1525 subTrans
->d_children
.push_back(pf
.d_children
[i
]);
1530 bool disequalityFound
= (neg
>= 0);
1531 if (!disequalityFound
)
1533 Debug("pf::" + theoryName
)
1534 << "A disequality was NOT found. UNSAT due to merged constants"
1536 Debug("pf::" + theoryName
) << "Proof for: " << pf
.d_node
<< std::endl
;
1537 Assert(pf
.d_node
.getKind() == kind::EQUAL
);
1538 Assert(pf
.d_node
.getNumChildren() == 2);
1539 Assert(pf
.d_node
[0].isConst() && pf
.d_node
[1].isConst());
1544 std::pair
<Node
, Node
> TheoryProof::identicalEqualitiesPrinterHelper(
1545 bool evenLengthSequence
,
1547 const theory::eq::EqProof
& pf
,
1548 const ProofLetMap
& map
,
1549 const std::string subproofStr
,
1550 std::stringstream
* outStream
,
1552 Node nodeAfterEqualitySequence
)
1554 theory::TheoryId theoryId
= getTheoryId();
1555 Assert(theoryId
== theory::THEORY_UF
|| theoryId
== theory::THEORY_ARRAYS
);
1556 bool ufProof
= (theoryId
== theory::THEORY_UF
);
1557 std::string theoryName
= theory::getStatsPrefix(theoryId
);
1558 if (evenLengthSequence
)
1560 // If the length is even, we need to apply transitivity for the "correct"
1561 // hand of the equality.
1563 Debug("pf::" + theoryName
) << "Equality sequence of even length"
1565 Debug("pf::" + theoryName
) << "n1 is: " << n
<< std::endl
;
1566 Debug("pf::" + theoryName
) << "pf-d_node is: " << pf
.d_node
<< std::endl
;
1567 Debug("pf::" + theoryName
) << "Next node is: " << nodeAfterEqualitySequence
1570 (*outStream
) << "(trans _ _ _ _ ";
1572 // If the sequence is at the very end of the transitivity proof, use
1573 // pf.d_node to guide us.
1576 if (match(n
[0], pf
.d_node
[0]))
1578 n
= n
[0].eqNode(n
[0]);
1579 (*outStream
) << subproofStr
<< " (symm _ _ _ " << subproofStr
<< ")";
1581 else if (match(n
[1], pf
.d_node
[1]))
1583 n
= n
[1].eqNode(n
[1]);
1584 (*outStream
) << " (symm _ _ _ " << subproofStr
<< ")" << subproofStr
;
1588 Debug("pf::" + theoryName
) << "Error: identical equalities over, but "
1589 "hands don't match what we're proving."
1596 // We have a "next node". Use it to guide us.
1597 if (!ufProof
&& nodeAfterEqualitySequence
.getKind() == kind::NOT
)
1599 nodeAfterEqualitySequence
= nodeAfterEqualitySequence
[0];
1602 Assert(nodeAfterEqualitySequence
.getKind() == kind::EQUAL
);
1604 if ((n
[0] == nodeAfterEqualitySequence
[0])
1605 || (n
[0] == nodeAfterEqualitySequence
[1]))
1608 (*outStream
) << subproofStr
<< " (symm _ _ _ " << subproofStr
<< ")";
1609 n
= n
[0].eqNode(n
[0]);
1611 else if ((n
[1] == nodeAfterEqualitySequence
[0])
1612 || (n
[1] == nodeAfterEqualitySequence
[1]))
1615 (*outStream
) << " (symm _ _ _ " << subproofStr
<< ")" << subproofStr
;
1616 n
= n
[1].eqNode(n
[1]);
1620 Debug("pf::" + theoryName
) << "Error: even length sequence, but I "
1621 "don't know which hand to keep!"
1627 (*outStream
) << ")";
1631 Debug("pf::" + theoryName
) << "Equality sequence length is odd!"
1633 (*outStream
).str(subproofStr
);
1636 Debug("pf::" + theoryName
) << "Have proven: " << n
<< std::endl
;
1637 return std::make_pair
<Node
&, Node
&>(n
, nodeAfterEqualitySequence
);
1640 } /* namespace CVC4 */