1 /********************* */
2 /*! \file proof_manager.cpp
4 ** Top contributors (to current version):
5 ** Guy Katz, Liana Hadarean, Andres Noetzli
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
18 #include "proof/proof_manager.h"
20 #include "base/cvc4_assert.h"
21 #include "context/context.h"
22 #include "options/bv_options.h"
23 #include "options/proof_options.h"
24 #include "proof/bitvector_proof.h"
25 #include "proof/clause_id.h"
26 #include "proof/cnf_proof.h"
27 #include "proof/lfsc_proof_printer.h"
28 #include "proof/proof_utils.h"
29 #include "proof/sat_proof_implementation.h"
30 #include "proof/theory_proof.h"
31 #include "smt/smt_engine.h"
32 #include "smt/smt_engine_scope.h"
33 #include "smt_util/node_visitor.h"
34 #include "theory/arrays/theory_arrays.h"
35 #include "theory/output_channel.h"
36 #include "theory/term_registration_visitor.h"
37 #include "theory/uf/equality_engine.h"
38 #include "theory/uf/theory_uf.h"
39 #include "theory/valuation.h"
40 #include "util/hash.h"
41 #include "util/proof.h"
45 std::string
nodeSetToString(const std::set
<Node
>& nodes
) {
46 std::ostringstream os
;
47 std::set
<Node
>::const_iterator it
;
48 for (it
= nodes
.begin(); it
!= nodes
.end(); ++it
) {
54 std::string
append(const std::string
& str
, uint64_t num
) {
55 std::ostringstream os
;
60 ProofManager::ProofManager(context::Context
* context
, ProofFormat format
)
66 d_inputCoreFormulas(context
),
67 d_outputCoreFormulas(context
),
75 ProofManager::~ProofManager() {
76 if (d_satProof
) delete d_satProof
;
77 if (d_cnfProof
) delete d_cnfProof
;
78 if (d_theoryProof
) delete d_theoryProof
;
81 ProofManager
* ProofManager::currentPM() {
82 return smt::currentProofManager();
84 const Proof
& ProofManager::getProof(SmtEngine
* smt
)
86 if (!currentPM()->d_fullProof
)
88 Assert(currentPM()->d_format
== LFSC
);
89 currentPM()->d_fullProof
.reset(new LFSCProof(
91 static_cast<CoreSatProof
*>(getSatProof()),
92 static_cast<LFSCCnfProof
*>(getCnfProof()),
93 static_cast<LFSCTheoryProofEngine
*>(getTheoryProofEngine())));
95 return *(currentPM()->d_fullProof
);
98 CoreSatProof
* ProofManager::getSatProof() {
99 Assert (currentPM()->d_satProof
);
100 return currentPM()->d_satProof
;
103 CnfProof
* ProofManager::getCnfProof() {
104 Assert (currentPM()->d_cnfProof
);
105 return currentPM()->d_cnfProof
;
108 TheoryProofEngine
* ProofManager::getTheoryProofEngine() {
109 Assert (currentPM()->d_theoryProof
!= NULL
);
110 return currentPM()->d_theoryProof
;
113 UFProof
* ProofManager::getUfProof() {
114 Assert (options::proof());
115 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF
);
119 BitVectorProof
* ProofManager::getBitVectorProof() {
120 Assert (options::proof());
121 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV
);
122 return (BitVectorProof
*)pf
;
125 ArrayProof
* ProofManager::getArrayProof() {
126 Assert (options::proof());
127 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS
);
128 return (ArrayProof
*)pf
;
131 ArithProof
* ProofManager::getArithProof() {
132 Assert (options::proof());
133 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH
);
134 return (ArithProof
*)pf
;
137 SkolemizationManager
* ProofManager::getSkolemizationManager() {
138 Assert (options::proof() || options::unsatCores());
139 return &(currentPM()->d_skolemizationManager
);
142 void ProofManager::initSatProof(Minisat::Solver
* solver
) {
143 Assert (currentPM()->d_satProof
== NULL
);
144 Assert(currentPM()->d_format
== LFSC
);
145 currentPM()->d_satProof
= new CoreSatProof(solver
, d_context
, "");
148 void ProofManager::initCnfProof(prop::CnfStream
* cnfStream
,
149 context::Context
* ctx
) {
150 ProofManager
* pm
= currentPM();
151 Assert(pm
->d_satProof
!= NULL
);
152 Assert (pm
->d_cnfProof
== NULL
);
153 Assert (pm
->d_format
== LFSC
);
154 CnfProof
* cnf
= new LFSCCnfProof(cnfStream
, ctx
, "");
155 pm
->d_cnfProof
= cnf
;
157 // true and false have to be setup in a special way
158 Node true_node
= NodeManager::currentNM()->mkConst
<bool>(true);
159 Node false_node
= NodeManager::currentNM()->mkConst
<bool>(false).notNode();
161 pm
->d_cnfProof
->pushCurrentAssertion(true_node
);
162 pm
->d_cnfProof
->pushCurrentDefinition(true_node
);
163 pm
->d_cnfProof
->registerConvertedClause(pm
->d_satProof
->getTrueUnit());
164 pm
->d_cnfProof
->popCurrentAssertion();
165 pm
->d_cnfProof
->popCurrentDefinition();
167 pm
->d_cnfProof
->pushCurrentAssertion(false_node
);
168 pm
->d_cnfProof
->pushCurrentDefinition(false_node
);
169 pm
->d_cnfProof
->registerConvertedClause(pm
->d_satProof
->getFalseUnit());
170 pm
->d_cnfProof
->popCurrentAssertion();
171 pm
->d_cnfProof
->popCurrentDefinition();
175 void ProofManager::initTheoryProofEngine() {
176 Assert (currentPM()->d_theoryProof
== NULL
);
177 Assert (currentPM()->d_format
== LFSC
);
178 currentPM()->d_theoryProof
= new LFSCTheoryProofEngine();
181 std::string
ProofManager::getInputClauseName(ClauseId id
,
182 const std::string
& prefix
) {
183 return append(prefix
+".pb", id
);
186 std::string
ProofManager::getLemmaClauseName(ClauseId id
,
187 const std::string
& prefix
) {
188 return append(prefix
+".lemc", id
);
191 std::string
ProofManager::getLemmaName(ClauseId id
, const std::string
& prefix
) {
192 return append(prefix
+"lem", id
);
195 std::string
ProofManager::getLearntClauseName(ClauseId id
,
196 const std::string
& prefix
) {
197 return append(prefix
+".cl", id
);
199 std::string
ProofManager::getVarName(prop::SatVariable var
,
200 const std::string
& prefix
) {
201 return append(prefix
+".v", var
);
203 std::string
ProofManager::getAtomName(prop::SatVariable var
,
204 const std::string
& prefix
) {
205 return append(prefix
+".a", var
);
207 std::string
ProofManager::getLitName(prop::SatLiteral lit
,
208 const std::string
& prefix
) {
209 return append(prefix
+".l", lit
.toInt());
212 std::string
ProofManager::getPreprocessedAssertionName(Node node
,
213 const std::string
& prefix
) {
214 if (currentPM()->d_assertionFilters
.find(node
) != currentPM()->d_assertionFilters
.end()) {
215 return currentPM()->d_assertionFilters
[node
];
218 node
= node
.getKind() == kind::BITVECTOR_EAGER_ATOM
? node
[0] : node
;
219 return append(prefix
+".PA", node
.getId());
221 std::string
ProofManager::getAssertionName(Node node
,
222 const std::string
& prefix
) {
223 return append(prefix
+".A", node
.getId());
225 std::string
ProofManager::getInputFormulaName(const Expr
& expr
) {
226 return currentPM()->d_inputFormulaToName
[expr
];
229 std::string
ProofManager::getAtomName(TNode atom
,
230 const std::string
& prefix
) {
231 prop::SatLiteral lit
= currentPM()->d_cnfProof
->getLiteral(atom
);
232 Assert(!lit
.isNegated());
233 return getAtomName(lit
.getSatVariable(), prefix
);
236 std::string
ProofManager::getLitName(TNode lit
,
237 const std::string
& prefix
) {
238 std::string litName
= getLitName(currentPM()->d_cnfProof
->getLiteral(lit
), prefix
);
239 if (currentPM()->d_rewriteFilters
.find(litName
) != currentPM()->d_rewriteFilters
.end()) {
240 return currentPM()->d_rewriteFilters
[litName
];
246 bool ProofManager::hasLitName(TNode lit
) {
247 return currentPM()->d_cnfProof
->hasLiteral(lit
);
250 std::string
ProofManager::sanitize(TNode node
) {
251 Assert (node
.isVar() || node
.isConst());
253 std::string name
= node
.toString();
255 std::replace(name
.begin(), name
.end(), ' ', '_');
256 } else if (node
.isConst()) {
257 name
.erase(std::remove(name
.begin(), name
.end(), '('), name
.end());
258 name
.erase(std::remove(name
.begin(), name
.end(), ')'), name
.end());
259 name
.erase(std::remove(name
.begin(), name
.end(), ' '), name
.end());
260 name
= "const" + name
;
266 void ProofManager::traceDeps(TNode n
, ExprSet
* coreAssertions
) {
267 Debug("cores") << "trace deps " << n
<< std::endl
;
268 if ((n
.isConst() && n
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
269 (n
.getKind() == kind::NOT
&& n
[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
272 if(d_inputCoreFormulas
.find(n
.toExpr()) != d_inputCoreFormulas
.end()) {
273 // originating formula was in core set
274 Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl
;
275 coreAssertions
->insert(n
.toExpr());
277 Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl
;
278 if(d_deps
.find(n
) == d_deps
.end()) {
279 if (options::allowEmptyDependencies()) {
280 Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl
;
283 InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n
.toString().c_str());
285 Assert(d_deps
.find(n
) != d_deps
.end());
286 std::vector
<Node
> deps
= (*d_deps
.find(n
)).second
;
287 for(std::vector
<Node
>::const_iterator i
= deps
.begin(); i
!= deps
.end(); ++i
) {
288 Debug("cores") << " + tracing deps: " << n
<< " -deps-on- " << *i
<< std::endl
;
289 if( !(*i
).isNull() ){
290 traceDeps(*i
, coreAssertions
);
296 void ProofManager::traceDeps(TNode n
, CDExprSet
* coreAssertions
) {
297 Debug("cores") << "trace deps " << n
<< std::endl
;
298 if ((n
.isConst() && n
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
299 (n
.getKind() == kind::NOT
&& n
[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
302 if(d_inputCoreFormulas
.find(n
.toExpr()) != d_inputCoreFormulas
.end()) {
303 // originating formula was in core set
304 Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl
;
305 coreAssertions
->insert(n
.toExpr());
307 Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl
;
308 if(d_deps
.find(n
) == d_deps
.end()) {
309 if (options::allowEmptyDependencies()) {
310 Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl
;
313 InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n
.toString().c_str());
315 Assert(d_deps
.find(n
) != d_deps
.end());
316 std::vector
<Node
> deps
= (*d_deps
.find(n
)).second
;
318 for(std::vector
<Node
>::const_iterator i
= deps
.begin(); i
!= deps
.end(); ++i
) {
319 Debug("cores") << " + tracing deps: " << n
<< " -deps-on- " << *i
<< std::endl
;
320 if( !(*i
).isNull() ){
321 traceDeps(*i
, coreAssertions
);
327 void ProofManager::traceUnsatCore() {
328 Assert (options::unsatCores());
329 d_satProof
->refreshProof();
330 IdToSatClause used_lemmas
;
331 IdToSatClause used_inputs
;
332 d_satProof
->collectClausesUsed(used_inputs
,
335 // At this point, there should be no assertions without a clause id
336 Assert(d_cnfProof
->isAssertionStackEmpty());
338 IdToSatClause::const_iterator it
= used_inputs
.begin();
339 for(; it
!= used_inputs
.end(); ++it
) {
340 Node node
= d_cnfProof
->getAssertionForClause(it
->first
);
341 ProofRule rule
= d_cnfProof
->getProofRule(node
);
343 Debug("cores") << "core input assertion " << node
<< std::endl
;
344 Debug("cores") << "with proof rule " << rule
<< std::endl
;
345 if (rule
== RULE_TSEITIN
||
346 rule
== RULE_GIVEN
) {
347 // trace dependences back to actual assertions
348 // (this adds them to the unsat core)
349 traceDeps(node
, &d_outputCoreFormulas
);
354 bool ProofManager::unsatCoreAvailable() const {
355 return d_satProof
->derivedEmptyClause();
358 std::vector
<Expr
> ProofManager::extractUnsatCore() {
359 std::vector
<Expr
> result
;
360 output_core_iterator it
= begin_unsat_core();
361 output_core_iterator end
= end_unsat_core();
362 while ( it
!= end
) {
363 result
.push_back(*it
);
369 void ProofManager::constructSatProof() {
370 if (!d_satProof
->proofConstructed()) {
371 d_satProof
->constructProof();
375 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory
, std::vector
<Node
> &lemmas
) {
376 Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
377 Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
381 IdToSatClause used_lemmas
;
382 IdToSatClause used_inputs
;
383 d_satProof
->collectClausesUsed(used_inputs
, used_lemmas
);
385 IdToSatClause::const_iterator it
;
388 Debug("pf::lemmasUnsatCore") << "Dumping all lemmas in unsat core" << std::endl
;
389 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
390 std::set
<Node
> lemma
= satClauseToNodeSet(it
->second
);
391 Debug("pf::lemmasUnsatCore") << nodeSetToString(lemma
);
393 // TODO: we should be able to drop the "haveProofRecipe" check.
394 // however, there are some rewrite issues with the arith solver, resulting
395 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
396 LemmaProofRecipe recipe
;
397 if (!getCnfProof()->haveProofRecipe(lemma
)) {
398 Debug("pf::lemmasUnsatCore") << "\t[no recipe]" << std::endl
;
402 recipe
= getCnfProof()->getProofRecipe(lemma
);
403 Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe
.getTheory()
404 << ", original = " << recipe
.getOriginalLemma() << "]" << std::endl
;
405 if (recipe
.simpleLemma() && recipe
.getTheory() == theory
&& seen
.find(recipe
.getOriginalLemma()) == seen
.end()) {
406 lemmas
.push_back(recipe
.getOriginalLemma());
407 seen
.insert(recipe
.getOriginalLemma());
412 std::set
<Node
> ProofManager::satClauseToNodeSet(prop::SatClause
* clause
) {
413 std::set
<Node
> result
;
414 for (unsigned i
= 0; i
< clause
->size(); ++i
) {
415 prop::SatLiteral lit
= (*clause
)[i
];
416 Node node
= getCnfProof()->getAtom(lit
.getSatVariable());
417 Expr atom
= node
.toExpr();
418 if (atom
!= utils::mkTrue())
419 result
.insert(lit
.isNegated() ? node
.notNode() : node
);
425 Node
ProofManager::getWeakestImplicantInUnsatCore(Node lemma
) {
426 Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
427 Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
429 // If we're doing aggressive minimization, work on all lemmas, not just conjunctions.
430 if (!options::aggressiveCoreMin() && (lemma
.getKind() != kind::AND
))
435 NodeBuilder
<> builder(kind::AND
);
437 IdToSatClause used_lemmas
;
438 IdToSatClause used_inputs
;
439 d_satProof
->collectClausesUsed(used_inputs
, used_lemmas
);
441 IdToSatClause::const_iterator it
;
442 std::set
<Node
>::iterator lemmaIt
;
444 if (!options::aggressiveCoreMin()) {
445 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
446 std::set
<Node
> currentLemma
= satClauseToNodeSet(it
->second
);
448 // TODO: we should be able to drop the "haveProofRecipe" check.
449 // however, there are some rewrite issues with the arith solver, resulting
450 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
451 LemmaProofRecipe recipe
;
452 if (!getCnfProof()->haveProofRecipe(currentLemma
))
455 recipe
= getCnfProof()->getProofRecipe(currentLemma
);
456 if (recipe
.getOriginalLemma() == lemma
) {
457 for (lemmaIt
= currentLemma
.begin(); lemmaIt
!= currentLemma
.end(); ++lemmaIt
) {
460 // Check that each conjunct appears in the original lemma.
462 for (unsigned i
= 0; i
< lemma
.getNumChildren(); ++i
) {
463 if (lemma
[i
] == *lemmaIt
)
474 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
475 std::set
<Node
> currentLemma
= satClauseToNodeSet(it
->second
);
477 // TODO: we should be able to drop the "haveProofRecipe" check.
478 // however, there are some rewrite issues with the arith solver, resulting
479 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
480 LemmaProofRecipe recipe
;
481 if (!getCnfProof()->haveProofRecipe(currentLemma
))
484 recipe
= getCnfProof()->getProofRecipe(currentLemma
);
485 if (recipe
.getOriginalLemma() == lemma
) {
486 NodeBuilder
<> disjunction(kind::OR
);
487 for (lemmaIt
= currentLemma
.begin(); lemmaIt
!= currentLemma
.end(); ++lemmaIt
) {
488 disjunction
<< *lemmaIt
;
491 Node conjunct
= (disjunction
.getNumChildren() == 1) ? disjunction
[0] : disjunction
;
497 AlwaysAssert(builder
.getNumChildren() != 0);
499 if (builder
.getNumChildren() == 1)
505 void ProofManager::addAssertion(Expr formula
) {
506 Debug("proof:pm") << "assert: " << formula
<< std::endl
;
507 d_inputFormulas
.insert(formula
);
508 std::ostringstream name
;
509 name
<< "A" << d_inputFormulaToName
.size();
510 d_inputFormulaToName
[formula
] = name
.str();
513 void ProofManager::addCoreAssertion(Expr formula
) {
514 Debug("cores") << "assert: " << formula
<< std::endl
;
515 d_deps
[Node::fromExpr(formula
)]; // empty vector of deps
516 d_inputCoreFormulas
.insert(formula
);
519 void ProofManager::addDependence(TNode n
, TNode dep
) {
521 Debug("cores") << "dep: " << n
<< " : " << dep
<< std::endl
;
522 if( !dep
.isNull() && d_deps
.find(dep
) == d_deps
.end()) {
523 Debug("cores") << "WHERE DID " << dep
<< " come from ??" << std::endl
;
525 std::vector
<Node
> deps
= d_deps
[n
].get();
531 void ProofManager::addUnsatCore(Expr formula
) {
532 Assert (d_inputCoreFormulas
.find(formula
) != d_inputCoreFormulas
.end());
533 d_outputCoreFormulas
.insert(formula
);
536 void ProofManager::addAssertionFilter(const Node
& node
, const std::string
& rewritten
) {
537 d_assertionFilters
[node
] = rewritten
;
540 void ProofManager::setLogic(const LogicInfo
& logic
) {
544 LFSCProof::LFSCProof(SmtEngine
* smtEngine
,
547 LFSCTheoryProofEngine
* theory
)
550 d_theoryProof(theory
),
551 d_smtEngine(smtEngine
)
554 void LFSCProof::toStream(std::ostream
& out
, const ProofLetMap
& map
) const
559 void LFSCProof::toStream(std::ostream
& out
) const
561 Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER
);
563 Assert(!d_satProof
->proofConstructed());
564 d_satProof
->constructProof();
566 // collecting leaf clauses in resolution proof
567 IdToSatClause used_lemmas
;
568 IdToSatClause used_inputs
;
569 d_satProof
->collectClausesUsed(used_inputs
,
572 IdToSatClause::iterator it2
;
573 Debug("pf::pm") << std::endl
<< "Used inputs: " << std::endl
;
574 for (it2
= used_inputs
.begin(); it2
!= used_inputs
.end(); ++it2
) {
575 Debug("pf::pm") << "\t input = " << *(it2
->second
) << std::endl
;
577 Debug("pf::pm") << std::endl
;
579 // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
580 // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
581 // Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl;
583 // Debug("pf::pm") << std::endl;
584 Debug("pf::pm") << std::endl
<< "Used lemmas: " << std::endl
;
585 for (it2
= used_lemmas
.begin(); it2
!= used_lemmas
.end(); ++it2
) {
587 std::vector
<Expr
> clause_expr
;
588 for(unsigned i
= 0; i
< it2
->second
->size(); ++i
) {
589 prop::SatLiteral lit
= (*(it2
->second
))[i
];
590 Expr atom
= d_cnfProof
->getAtom(lit
.getSatVariable()).toExpr();
591 if (atom
.isConst()) {
592 Assert (atom
== utils::mkTrue());
595 Expr expr_lit
= lit
.isNegated() ? atom
.notExpr(): atom
;
596 clause_expr
.push_back(expr_lit
);
599 Debug("pf::pm") << "\t lemma " << it2
->first
<< " = " << *(it2
->second
) << std::endl
;
600 Debug("pf::pm") << "\t";
601 for (unsigned i
= 0; i
< clause_expr
.size(); ++i
) {
602 Debug("pf::pm") << clause_expr
[i
] << " ";
604 Debug("pf::pm") << std::endl
;
606 Debug("pf::pm") << std::endl
;
608 // collecting assertions that lead to the clauses being asserted
609 NodeSet used_assertions
;
610 d_cnfProof
->collectAssertionsForClauses(used_inputs
, used_assertions
);
612 NodeSet::iterator it3
;
613 Debug("pf::pm") << std::endl
<< "Used assertions: " << std::endl
;
614 for (it3
= used_assertions
.begin(); it3
!= used_assertions
.end(); ++it3
)
615 Debug("pf::pm") << "\t assertion = " << *it3
<< std::endl
;
617 std::set
<Node
> atoms
;
619 NodePairSet rewrites
;
620 // collects the atoms in the clauses
621 d_cnfProof
->collectAtomsAndRewritesForLemmas(used_lemmas
, atoms
, rewrites
);
623 if (!rewrites
.empty()) {
624 Debug("pf::pm") << std::endl
<< "Rewrites used in lemmas: " << std::endl
;
625 NodePairSet::const_iterator rewriteIt
;
626 for (rewriteIt
= rewrites
.begin(); rewriteIt
!= rewrites
.end(); ++rewriteIt
) {
627 Debug("pf::pm") << "\t" << rewriteIt
->first
<< " --> " << rewriteIt
->second
<< std::endl
;
629 Debug("pf::pm") << std::endl
<< "Rewrite printing done" << std::endl
;
631 Debug("pf::pm") << "No rewrites in lemmas found" << std::endl
;
634 // The derived/unrewritten atoms may not have CNF literals required later on.
635 // If they don't, add them.
636 std::set
<Node
>::const_iterator it
;
637 for (it
= atoms
.begin(); it
!= atoms
.end(); ++it
) {
638 Debug("pf::pm") << "Ensure literal for atom: " << *it
<< std::endl
;
639 if (!d_cnfProof
->hasLiteral(*it
)) {
640 // For arithmetic: these literals are not normalized, causing an error in Arith.
641 if (theory::Theory::theoryOf(*it
) == theory::THEORY_ARITH
) {
642 d_cnfProof
->ensureLiteral(*it
, true); // This disables preregistration with the theory solver.
644 d_cnfProof
->ensureLiteral(*it
); // Normal method, with theory solver preregisteration.
649 d_cnfProof
->collectAtomsForClauses(used_inputs
, atoms
);
650 d_cnfProof
->collectAtomsForClauses(used_lemmas
, atoms
);
652 // collects the atoms in the assertions
653 for (NodeSet::const_iterator it
= used_assertions
.begin();
654 it
!= used_assertions
.end(); ++it
) {
655 utils::collectAtoms(*it
, atoms
);
656 // utils::collectAtoms(*it, newAtoms);
659 std::set
<Node
>::iterator atomIt
;
660 Debug("pf::pm") << std::endl
<< "Dumping atoms from lemmas, inputs and assertions: "
661 << std::endl
<< std::endl
;
662 for (atomIt
= atoms
.begin(); atomIt
!= atoms
.end(); ++atomIt
) {
663 Debug("pf::pm") << "\tAtom: " << *atomIt
<< std::endl
;
665 smt::SmtScope
scope(d_smtEngine
);
666 std::ostringstream paren
;
669 out
<< " ;; Declarations\n";
671 // declare the theory atoms
672 Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl
;
673 for(it
= atoms
.begin(); it
!= atoms
.end(); ++it
) {
674 Debug("pf::pm") << "\tTerm: " << (*it
).toExpr() << std::endl
;
675 d_theoryProof
->registerTerm((*it
).toExpr());
678 Debug("pf::pm") << std::endl
<< "Term registration done!" << std::endl
<< std::endl
;
680 Debug("pf::pm") << std::endl
<< "LFSCProof::toStream: starting to print assertions" << std::endl
;
682 // print out all the original assertions
683 d_theoryProof
->registerTermsFromAssertions();
684 d_theoryProof
->printSortDeclarations(out
, paren
);
685 d_theoryProof
->printTermDeclarations(out
, paren
);
686 d_theoryProof
->printAssertions(out
, paren
);
688 Debug("pf::pm") << std::endl
<< "LFSCProof::toStream: print assertions DONE" << std::endl
;
690 out
<< "(: (holds cln)\n\n";
693 // Have the theory proofs print deferred declarations, e.g. for skolem variables.
694 out
<< " ;; Printing deferred declarations \n\n";
695 d_theoryProof
->printDeferredDeclarations(out
, paren
);
697 out
<< "\n ;; Printing the global let map";
698 d_theoryProof
->finalizeBvConflicts(used_lemmas
, out
);
699 ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
700 ProofLetMap globalLetMap
;
701 if (options::lfscLetification()) {
702 ProofManager::currentPM()->printGlobalLetMap(atoms
, globalLetMap
, out
, paren
);
705 out
<< " ;; Printing aliasing declarations \n\n";
706 d_theoryProof
->printAliasingDeclarations(out
, paren
, globalLetMap
);
708 out
<< " ;; Rewrites for Lemmas \n";
709 d_theoryProof
->printLemmaRewrites(rewrites
, out
, paren
);
711 // print trust that input assertions are their preprocessed form
712 printPreprocessedAssertions(used_assertions
, out
, paren
, globalLetMap
);
714 // print mapping between theory atoms and internal SAT variables
715 out
<< ";; Printing mapping from preprocessed assertions into atoms \n";
716 d_cnfProof
->printAtomMapping(atoms
, out
, paren
, globalLetMap
);
718 Debug("pf::pm") << std::endl
<< "Printing cnf proof for clauses" << std::endl
;
720 IdToSatClause::const_iterator cl_it
= used_inputs
.begin();
721 // print CNF conversion proof for each clause
722 for (; cl_it
!= used_inputs
.end(); ++cl_it
) {
723 d_cnfProof
->printCnfProofForClause(cl_it
->first
, cl_it
->second
, out
, paren
);
726 Debug("pf::pm") << std::endl
<< "Printing cnf proof for clauses DONE" << std::endl
;
728 Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl
;
729 d_theoryProof
->printTheoryLemmas(used_lemmas
, out
, paren
, globalLetMap
);
730 Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl
;
732 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
&& ProofManager::getBitVectorProof()) {
733 proof::LFSCProofPrinter::printResolutionEmptyClause(
734 ProofManager::getBitVectorProof()->getSatProof(), out
, paren
);
736 // print actual resolution proof
737 proof::LFSCProofPrinter::printResolutions(d_satProof
, out
, paren
);
738 proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof
, out
, paren
);
745 void LFSCProof::printPreprocessedAssertions(const NodeSet
& assertions
,
748 ProofLetMap
& globalLetMap
) const
750 os
<< "\n ;; In the preprocessor we trust \n";
751 NodeSet::const_iterator it
= assertions
.begin();
752 NodeSet::const_iterator end
= assertions
.end();
754 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl
;
756 if (options::fewerPreprocessingHoles()) {
757 // Check for assertions that did not get rewritten, and update the printing filter.
758 checkUnrewrittenAssertion(assertions
);
760 // For the remaining assertions, bind them to input assertions.
761 for (; it
!= end
; ++it
) {
762 // Rewrite preprocessing step if it cannot be eliminated
763 if (!ProofManager::currentPM()->have_input_assertion((*it
).toExpr())) {
764 os
<< "(th_let_pf _ (trust_f (iff ";
768 if (((*it
).isConst() && *it
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
769 ((*it
).getKind() == kind::NOT
&& (*it
)[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
770 inputAssertion
= NodeManager::currentNM()->mkConst
<bool>(true).toExpr();
772 // Figure out which input assertion led to this assertion
773 ExprSet inputAssertions
;
774 ProofManager::currentPM()->traceDeps(*it
, &inputAssertions
);
776 Debug("pf::pm") << "Original assertions for " << *it
<< " are: " << std::endl
;
778 ProofManager::assertions_iterator assertionIt
;
779 for (assertionIt
= inputAssertions
.begin(); assertionIt
!= inputAssertions
.end(); ++assertionIt
) {
780 Debug("pf::pm") << "\t" << *assertionIt
<< std::endl
;
783 if (inputAssertions
.size() == 0) {
784 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl
;
785 // For now just use the first assertion...
786 inputAssertion
= *(ProofManager::currentPM()->begin_assertions());
788 if (inputAssertions
.size() != 1) {
789 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl
;
791 inputAssertion
= *inputAssertions
.begin();
795 if (!ProofManager::currentPM()->have_input_assertion(inputAssertion
)) {
796 // The thing returned by traceDeps does not appear in the input assertions...
797 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl
;
798 // For now just use the first assertion...
799 inputAssertion
= *(ProofManager::currentPM()->begin_assertions());
802 Debug("pf::pm") << "Original assertion for " << *it
806 << ProofManager::currentPM()->getInputFormulaName(inputAssertion
)
809 ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion
, os
, globalLetMap
);
811 ProofManager::currentPM()->printTrustedTerm(*it
, os
, globalLetMap
);
813 os
<< "(\\ "<< ProofManager::getPreprocessedAssertionName(*it
, "") << "\n";
816 std::ostringstream rewritten
;
818 rewritten
<< "(or_elim_1 _ _ ";
819 rewritten
<< "(not_not_intro _ ";
820 rewritten
<< ProofManager::currentPM()->getInputFormulaName(inputAssertion
);
821 rewritten
<< ") (iff_elim_1 _ _ ";
822 rewritten
<< ProofManager::getPreprocessedAssertionName(*it
, "");
825 ProofManager::currentPM()->addAssertionFilter(*it
, rewritten
.str());
829 for (; it
!= end
; ++it
) {
830 os
<< "(th_let_pf _ ";
834 ProofManager::currentPM()->printTrustedTerm(*it
, os
, globalLetMap
);
837 os
<< "(\\ "<< ProofManager::getPreprocessedAssertionName(*it
, "") << "\n";
845 void LFSCProof::checkUnrewrittenAssertion(const NodeSet
& rewrites
) const
847 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl
;
849 NodeSet::const_iterator rewrite
;
850 for (rewrite
= rewrites
.begin(); rewrite
!= rewrites
.end(); ++rewrite
) {
851 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite
<< std::endl
;
852 if (ProofManager::currentPM()->have_input_assertion((*rewrite
).toExpr())) {
853 Assert(ProofManager::currentPM()->have_input_assertion((*rewrite
).toExpr()));
854 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
855 << "\tAdding filter: "
856 << ProofManager::getPreprocessedAssertionName(*rewrite
, "")
858 << ProofManager::currentPM()->getInputFormulaName((*rewrite
).toExpr())
860 ProofManager::currentPM()->addAssertionFilter(*rewrite
,
861 ProofManager::currentPM()->getInputFormulaName((*rewrite
).toExpr()));
863 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite
<< std::endl
;
870 bool ProofManager::hasOp(TNode n
) const {
871 return d_bops
.find(n
) != d_bops
.end();
874 Node
ProofManager::lookupOp(TNode n
) const {
875 std::map
<Node
, Node
>::const_iterator i
= d_bops
.find(n
);
876 Assert(i
!= d_bops
.end());
880 Node
ProofManager::mkOp(TNode n
) {
881 Trace("mgd-pm-mkop") << "MkOp : " << n
<< " " << n
.getKind() << std::endl
;
882 if(n
.getKind() != kind::BUILTIN
) {
888 Assert((n
.getConst
<Kind
>() == kind::SELECT
) || (n
.getConst
<Kind
>() == kind::STORE
));
890 Debug("mgd-pm-mkop") << "making an op for " << n
<< "\n";
892 std::stringstream ss
;
894 std::string s
= ss
.str();
895 Debug("mgd-pm-mkop") << " : " << s
<< std::endl
;
896 std::vector
<TypeNode
> v
;
897 v
.push_back(NodeManager::currentNM()->integerType());
898 if(n
.getConst
<Kind
>() == kind::SELECT
) {
899 v
.push_back(NodeManager::currentNM()->integerType());
900 v
.push_back(NodeManager::currentNM()->integerType());
901 } else if(n
.getConst
<Kind
>() == kind::STORE
) {
902 v
.push_back(NodeManager::currentNM()->integerType());
903 v
.push_back(NodeManager::currentNM()->integerType());
904 v
.push_back(NodeManager::currentNM()->integerType());
906 TypeNode type
= NodeManager::currentNM()->mkFunctionType(v
);
907 Debug("mgd-pm-mkop") << "typenode is: " << type
<< "\n";
908 op
= NodeManager::currentNM()->mkSkolem(s
, type
, " ignore", NodeManager::SKOLEM_NO_NOTIFY
);
911 Debug("mgd-pm-mkop") << "returning the op: " << op
<< "\n";
914 //---end from Morgan---
916 bool ProofManager::wasPrinted(const Type
& type
) const {
917 return d_printedTypes
.find(type
) != d_printedTypes
.end();
920 void ProofManager::markPrinted(const Type
& type
) {
921 d_printedTypes
.insert(type
);
924 void ProofManager::addRewriteFilter(const std::string
&original
, const std::string
&substitute
) {
925 d_rewriteFilters
[original
] = substitute
;
928 bool ProofManager::haveRewriteFilter(TNode lit
) {
929 std::string litName
= getLitName(currentPM()->d_cnfProof
->getLiteral(lit
));
930 return d_rewriteFilters
.find(litName
) != d_rewriteFilters
.end();
933 void ProofManager::clearRewriteFilters() {
934 d_rewriteFilters
.clear();
937 std::ostream
& operator<<(std::ostream
& out
, CVC4::ProofRule k
) {
943 out
<< "RULE_DERIVED";
945 case RULE_RECONSTRUCT
:
946 out
<< "RULE_RECONSTRUCT";
952 out
<< "RULE_INVALID";
955 out
<< "RULE_CONFLICT";
958 out
<< "RULE_TSEITIN";
963 case RULE_ARRAYS_EXT
:
964 out
<< "RULE_ARRAYS";
966 case RULE_ARRAYS_ROW
:
967 out
<< "RULE_ARRAYS";
970 out
<< "ProofRule Unknown! [" << unsigned(k
) << "]";
976 void ProofManager::registerRewrite(unsigned ruleId
, Node original
, Node result
){
977 Assert (currentPM()->d_theoryProof
!= NULL
);
978 currentPM()->d_rewriteLog
.push_back(RewriteLogEntry(ruleId
, original
, result
));
981 void ProofManager::clearRewriteLog() {
982 Assert (currentPM()->d_theoryProof
!= NULL
);
983 currentPM()->d_rewriteLog
.clear();
986 std::vector
<RewriteLogEntry
> ProofManager::getRewriteLog() {
987 return currentPM()->d_rewriteLog
;
990 void ProofManager::dumpRewriteLog() const {
991 Debug("pf::rr") << "Dumpign rewrite log:" << std::endl
;
993 for (unsigned i
= 0; i
< d_rewriteLog
.size(); ++i
) {
994 Debug("pf::rr") << "\tRule " << d_rewriteLog
[i
].getRuleId()
996 << d_rewriteLog
[i
].getOriginal()
998 << d_rewriteLog
[i
].getResult() << std::endl
;
1002 void bind(Expr term
, ProofLetMap
& map
, Bindings
& letOrder
) {
1003 ProofLetMap::iterator it
= map
.find(term
);
1004 if (it
!= map
.end())
1007 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
)
1008 bind(term
[i
], map
, letOrder
);
1010 // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)).
1011 // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too.
1012 Kind k
= term
.getKind();
1013 if (((k
== kind::OR
) || (k
== kind::AND
)) && term
.getNumChildren() > 2) {
1014 Node currentExpression
= term
[term
.getNumChildren() - 1];
1015 for (int i
= term
.getNumChildren() - 2; i
>= 0; --i
) {
1016 NodeBuilder
<> builder(k
);
1018 builder
<< currentExpression
.toExpr();
1019 currentExpression
= builder
;
1020 bind(currentExpression
.toExpr(), map
, letOrder
);
1023 unsigned newId
= ProofLetCount::newId();
1024 ProofLetCount
letCount(newId
);
1025 map
[term
] = letCount
;
1026 letOrder
.push_back(LetOrderElement(term
, newId
));
1030 void ProofManager::printGlobalLetMap(std::set
<Node
>& atoms
,
1031 ProofLetMap
& letMap
,
1033 std::ostringstream
& paren
) {
1035 std::set
<Node
>::const_iterator atom
;
1036 for (atom
= atoms
.begin(); atom
!= atoms
.end(); ++atom
) {
1037 bind(atom
->toExpr(), letMap
, letOrder
);
1040 // TODO: give each theory a chance to add atoms. For now, just query BV directly...
1041 const std::set
<Node
>* additionalAtoms
= ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
1042 for (atom
= additionalAtoms
->begin(); atom
!= additionalAtoms
->end(); ++atom
) {
1043 bind(atom
->toExpr(), letMap
, letOrder
);
1046 for (unsigned i
= 0; i
< letOrder
.size(); ++i
) {
1047 Expr currentExpr
= letOrder
[i
].expr
;
1048 unsigned letId
= letOrder
[i
].id
;
1049 ProofLetMap::iterator it
= letMap
.find(currentExpr
);
1050 Assert(it
!= letMap
.end());
1051 out
<< "\n(@ let" << letId
<< " ";
1052 d_theoryProof
->printBoundTerm(currentExpr
, out
, letMap
);
1054 it
->second
.increment();
1057 out
<< std::endl
<< std::endl
;
1060 void ProofManager::ensureLiteral(Node node
) {
1061 d_cnfProof
->ensureLiteral(node
);
1063 void ProofManager::printTrustedTerm(Node term
,
1065 ProofLetMap
& globalLetMap
)
1067 TheoryProofEngine
* tpe
= ProofManager::currentPM()->getTheoryProofEngine();
1068 if (tpe
->printsAsBool(term
)) os
<< "(p_app ";
1069 tpe
->printTheoryTerm(term
.toExpr(), os
, globalLetMap
);
1070 if (tpe
->printsAsBool(term
)) os
<< ")";
1072 } /* CVC4 namespace */