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-2019 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/check.h"
21 #include "context/context.h"
22 #include "options/bv_options.h"
23 #include "options/proof_options.h"
24 #include "proof/clause_id.h"
25 #include "proof/cnf_proof.h"
26 #include "proof/lfsc_proof_printer.h"
27 #include "proof/proof_utils.h"
28 #include "proof/resolution_bitvector_proof.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/smt_statistics_registry.h"
34 #include "smt_util/node_visitor.h"
35 #include "theory/arrays/theory_arrays.h"
36 #include "theory/output_channel.h"
37 #include "theory/term_registration_visitor.h"
38 #include "theory/uf/equality_engine.h"
39 #include "theory/uf/theory_uf.h"
40 #include "theory/valuation.h"
41 #include "util/hash.h"
42 #include "util/proof.h"
46 std::string
nodeSetToString(const std::set
<Node
>& nodes
) {
47 std::ostringstream os
;
48 std::set
<Node
>::const_iterator it
;
49 for (it
= nodes
.begin(); it
!= nodes
.end(); ++it
) {
55 std::string
append(const std::string
& str
, uint64_t num
) {
56 std::ostringstream os
;
61 ProofManager::ProofManager(context::Context
* context
, ProofFormat format
)
67 d_inputCoreFormulas(context
),
68 d_outputCoreFormulas(context
),
76 ProofManager::~ProofManager() {
77 if (d_satProof
) delete d_satProof
;
78 if (d_cnfProof
) delete d_cnfProof
;
79 if (d_theoryProof
) delete d_theoryProof
;
82 ProofManager
* ProofManager::currentPM() {
83 return smt::currentProofManager();
85 const Proof
& ProofManager::getProof(SmtEngine
* smt
)
87 if (!currentPM()->d_fullProof
)
89 Assert(currentPM()->d_format
== LFSC
);
90 currentPM()->d_fullProof
.reset(new LFSCProof(
92 static_cast<CoreSatProof
*>(getSatProof()),
93 static_cast<LFSCCnfProof
*>(getCnfProof()),
94 static_cast<LFSCTheoryProofEngine
*>(getTheoryProofEngine())));
96 return *(currentPM()->d_fullProof
);
99 CoreSatProof
* ProofManager::getSatProof() {
100 Assert(currentPM()->d_satProof
);
101 return currentPM()->d_satProof
;
104 CnfProof
* ProofManager::getCnfProof() {
105 Assert(currentPM()->d_cnfProof
);
106 return currentPM()->d_cnfProof
;
109 TheoryProofEngine
* ProofManager::getTheoryProofEngine() {
110 Assert(currentPM()->d_theoryProof
!= NULL
);
111 return currentPM()->d_theoryProof
;
114 UFProof
* ProofManager::getUfProof() {
115 Assert(options::proof());
116 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF
);
120 proof::ResolutionBitVectorProof
* ProofManager::getBitVectorProof()
122 Assert(options::proof());
123 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV
);
124 return static_cast<proof::ResolutionBitVectorProof
*>(pf
);
127 ArrayProof
* ProofManager::getArrayProof() {
128 Assert(options::proof());
129 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS
);
130 return (ArrayProof
*)pf
;
133 ArithProof
* ProofManager::getArithProof() {
134 Assert(options::proof());
135 TheoryProof
* pf
= getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARITH
);
136 return (ArithProof
*)pf
;
139 SkolemizationManager
* ProofManager::getSkolemizationManager() {
140 Assert(options::proof() || options::unsatCores());
141 return &(currentPM()->d_skolemizationManager
);
144 void ProofManager::initSatProof(Minisat::Solver
* solver
) {
145 Assert(currentPM()->d_satProof
== NULL
);
146 Assert(currentPM()->d_format
== LFSC
);
147 currentPM()->d_satProof
= new CoreSatProof(solver
, d_context
, "");
150 void ProofManager::initCnfProof(prop::CnfStream
* cnfStream
,
151 context::Context
* ctx
) {
152 ProofManager
* pm
= currentPM();
153 Assert(pm
->d_satProof
!= NULL
);
154 Assert(pm
->d_cnfProof
== NULL
);
155 Assert(pm
->d_format
== LFSC
);
156 CnfProof
* cnf
= new LFSCCnfProof(cnfStream
, ctx
, "");
157 pm
->d_cnfProof
= cnf
;
159 // true and false have to be setup in a special way
160 Node true_node
= NodeManager::currentNM()->mkConst
<bool>(true);
161 Node false_node
= NodeManager::currentNM()->mkConst
<bool>(false).notNode();
163 pm
->d_cnfProof
->pushCurrentAssertion(true_node
);
164 pm
->d_cnfProof
->pushCurrentDefinition(true_node
);
165 pm
->d_cnfProof
->registerConvertedClause(pm
->d_satProof
->getTrueUnit());
166 pm
->d_cnfProof
->popCurrentAssertion();
167 pm
->d_cnfProof
->popCurrentDefinition();
169 pm
->d_cnfProof
->pushCurrentAssertion(false_node
);
170 pm
->d_cnfProof
->pushCurrentDefinition(false_node
);
171 pm
->d_cnfProof
->registerConvertedClause(pm
->d_satProof
->getFalseUnit());
172 pm
->d_cnfProof
->popCurrentAssertion();
173 pm
->d_cnfProof
->popCurrentDefinition();
177 void ProofManager::initTheoryProofEngine() {
178 Assert(currentPM()->d_theoryProof
== NULL
);
179 Assert(currentPM()->d_format
== LFSC
);
180 currentPM()->d_theoryProof
= new LFSCTheoryProofEngine();
183 std::string
ProofManager::getInputClauseName(ClauseId id
,
184 const std::string
& prefix
) {
185 return append(prefix
+".pb", id
);
188 std::string
ProofManager::getLemmaClauseName(ClauseId id
,
189 const std::string
& prefix
) {
190 return append(prefix
+".lemc", id
);
193 std::string
ProofManager::getLemmaName(ClauseId id
, const std::string
& prefix
) {
194 return append(prefix
+"lem", id
);
197 std::string
ProofManager::getLearntClauseName(ClauseId id
,
198 const std::string
& prefix
) {
199 return append(prefix
+".cl", id
);
201 std::string
ProofManager::getVarName(prop::SatVariable var
,
202 const std::string
& prefix
) {
203 return append(prefix
+".v", var
);
205 std::string
ProofManager::getAtomName(prop::SatVariable var
,
206 const std::string
& prefix
) {
207 return append(prefix
+".a", var
);
209 std::string
ProofManager::getLitName(prop::SatLiteral lit
,
210 const std::string
& prefix
) {
211 return append(prefix
+".l", lit
.toInt());
214 std::string
ProofManager::getPreprocessedAssertionName(Node node
,
215 const std::string
& prefix
) {
216 if (currentPM()->d_assertionFilters
.find(node
) != currentPM()->d_assertionFilters
.end()) {
217 return currentPM()->d_assertionFilters
[node
];
220 node
= node
.getKind() == kind::BITVECTOR_EAGER_ATOM
? node
[0] : node
;
221 return append(prefix
+".PA", node
.getId());
223 std::string
ProofManager::getAssertionName(Node node
,
224 const std::string
& prefix
) {
225 return append(prefix
+".A", node
.getId());
227 std::string
ProofManager::getInputFormulaName(const Expr
& expr
) {
228 return currentPM()->d_inputFormulaToName
[expr
];
231 std::string
ProofManager::getAtomName(TNode atom
,
232 const std::string
& prefix
) {
233 prop::SatLiteral lit
= currentPM()->d_cnfProof
->getLiteral(atom
);
234 Assert(!lit
.isNegated());
235 return getAtomName(lit
.getSatVariable(), prefix
);
238 std::string
ProofManager::getLitName(TNode lit
,
239 const std::string
& prefix
) {
240 std::string litName
= getLitName(currentPM()->d_cnfProof
->getLiteral(lit
), prefix
);
241 if (currentPM()->d_rewriteFilters
.find(litName
) != currentPM()->d_rewriteFilters
.end()) {
242 return currentPM()->d_rewriteFilters
[litName
];
248 bool ProofManager::hasLitName(TNode lit
) {
249 return currentPM()->d_cnfProof
->hasLiteral(lit
);
252 std::string
ProofManager::sanitize(TNode node
) {
253 Assert(node
.isVar() || node
.isConst());
255 std::string name
= node
.toString();
257 std::replace(name
.begin(), name
.end(), ' ', '_');
258 } else if (node
.isConst()) {
259 name
.erase(std::remove(name
.begin(), name
.end(), '('), name
.end());
260 name
.erase(std::remove(name
.begin(), name
.end(), ')'), name
.end());
261 name
.erase(std::remove(name
.begin(), name
.end(), ' '), name
.end());
262 name
= "const" + name
;
268 void ProofManager::traceDeps(TNode n
, ExprSet
* coreAssertions
) {
269 Debug("cores") << "trace deps " << n
<< std::endl
;
270 if ((n
.isConst() && n
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
271 (n
.getKind() == kind::NOT
&& n
[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
274 if(d_inputCoreFormulas
.find(n
.toExpr()) != d_inputCoreFormulas
.end()) {
275 // originating formula was in core set
276 Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl
;
277 coreAssertions
->insert(n
.toExpr());
279 Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl
;
280 if(d_deps
.find(n
) == d_deps
.end()) {
281 if (options::allowEmptyDependencies()) {
282 Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl
;
286 << "Cannot trace dependence information back to input assertion:\n`"
289 Assert(d_deps
.find(n
) != d_deps
.end());
290 std::vector
<Node
> deps
= (*d_deps
.find(n
)).second
;
291 for(std::vector
<Node
>::const_iterator i
= deps
.begin(); i
!= deps
.end(); ++i
) {
292 Debug("cores") << " + tracing deps: " << n
<< " -deps-on- " << *i
<< std::endl
;
293 if( !(*i
).isNull() ){
294 traceDeps(*i
, coreAssertions
);
300 void ProofManager::traceDeps(TNode n
, CDExprSet
* coreAssertions
) {
301 Debug("cores") << "trace deps " << n
<< std::endl
;
302 if ((n
.isConst() && n
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
303 (n
.getKind() == kind::NOT
&& n
[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
306 if(d_inputCoreFormulas
.find(n
.toExpr()) != d_inputCoreFormulas
.end()) {
307 // originating formula was in core set
308 Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl
;
309 coreAssertions
->insert(n
.toExpr());
311 Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl
;
312 if(d_deps
.find(n
) == d_deps
.end()) {
313 if (options::allowEmptyDependencies()) {
314 Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl
;
318 << "Cannot trace dependence information back to input assertion:\n`"
321 Assert(d_deps
.find(n
) != d_deps
.end());
322 std::vector
<Node
> deps
= (*d_deps
.find(n
)).second
;
324 for(std::vector
<Node
>::const_iterator i
= deps
.begin(); i
!= deps
.end(); ++i
) {
325 Debug("cores") << " + tracing deps: " << n
<< " -deps-on- " << *i
<< std::endl
;
326 if( !(*i
).isNull() ){
327 traceDeps(*i
, coreAssertions
);
333 void ProofManager::traceUnsatCore() {
334 Assert(options::unsatCores());
335 d_satProof
->refreshProof();
336 IdToSatClause used_lemmas
;
337 IdToSatClause used_inputs
;
338 d_satProof
->collectClausesUsed(used_inputs
,
341 // At this point, there should be no assertions without a clause id
342 Assert(d_cnfProof
->isAssertionStackEmpty());
344 IdToSatClause::const_iterator it
= used_inputs
.begin();
345 for(; it
!= used_inputs
.end(); ++it
) {
346 Node node
= d_cnfProof
->getAssertionForClause(it
->first
);
347 ProofRule rule
= d_cnfProof
->getProofRule(node
);
349 Debug("cores") << "core input assertion " << node
<< std::endl
;
350 Debug("cores") << "with proof rule " << rule
<< std::endl
;
351 if (rule
== RULE_TSEITIN
||
352 rule
== RULE_GIVEN
) {
353 // trace dependences back to actual assertions
354 // (this adds them to the unsat core)
355 traceDeps(node
, &d_outputCoreFormulas
);
360 bool ProofManager::unsatCoreAvailable() const {
361 return d_satProof
->derivedEmptyClause();
364 std::vector
<Expr
> ProofManager::extractUnsatCore() {
365 std::vector
<Expr
> result
;
366 output_core_iterator it
= begin_unsat_core();
367 output_core_iterator end
= end_unsat_core();
368 while ( it
!= end
) {
369 result
.push_back(*it
);
375 void ProofManager::constructSatProof() {
376 if (!d_satProof
->proofConstructed()) {
377 d_satProof
->constructProof();
381 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory
, std::vector
<Node
> &lemmas
) {
382 Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off";
383 Assert(unsatCoreAvailable())
384 << "Cannot get unsat core at this time. Mabye the input is SAT?";
388 IdToSatClause used_lemmas
;
389 IdToSatClause used_inputs
;
390 d_satProof
->collectClausesUsed(used_inputs
, used_lemmas
);
392 IdToSatClause::const_iterator it
;
395 Debug("pf::lemmasUnsatCore") << "Dumping all lemmas in unsat core" << std::endl
;
396 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
397 std::set
<Node
> lemma
= satClauseToNodeSet(it
->second
);
398 Debug("pf::lemmasUnsatCore") << nodeSetToString(lemma
);
400 // TODO: we should be able to drop the "haveProofRecipe" check.
401 // however, there are some rewrite issues with the arith solver, resulting
402 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
403 LemmaProofRecipe recipe
;
404 if (!getCnfProof()->haveProofRecipe(lemma
)) {
405 Debug("pf::lemmasUnsatCore") << "\t[no recipe]" << std::endl
;
409 recipe
= getCnfProof()->getProofRecipe(lemma
);
410 Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe
.getTheory()
411 << ", original = " << recipe
.getOriginalLemma() << "]" << std::endl
;
412 if (recipe
.simpleLemma() && recipe
.getTheory() == theory
&& seen
.find(recipe
.getOriginalLemma()) == seen
.end()) {
413 lemmas
.push_back(recipe
.getOriginalLemma());
414 seen
.insert(recipe
.getOriginalLemma());
419 std::set
<Node
> ProofManager::satClauseToNodeSet(prop::SatClause
* clause
) {
420 std::set
<Node
> result
;
421 for (unsigned i
= 0; i
< clause
->size(); ++i
) {
422 prop::SatLiteral lit
= (*clause
)[i
];
423 Node node
= getCnfProof()->getAtom(lit
.getSatVariable());
424 Expr atom
= node
.toExpr();
425 if (atom
!= utils::mkTrue())
426 result
.insert(lit
.isNegated() ? node
.notNode() : node
);
432 Node
ProofManager::getWeakestImplicantInUnsatCore(Node lemma
) {
433 Assert(PROOF_ON()) << "Cannot compute unsat core when proofs are off";
434 Assert(unsatCoreAvailable())
435 << "Cannot get unsat core at this time. Mabye the input is SAT?";
437 // If we're doing aggressive minimization, work on all lemmas, not just conjunctions.
438 if (!options::aggressiveCoreMin() && (lemma
.getKind() != kind::AND
))
443 NodeBuilder
<> builder(kind::AND
);
445 IdToSatClause used_lemmas
;
446 IdToSatClause used_inputs
;
447 d_satProof
->collectClausesUsed(used_inputs
, used_lemmas
);
449 IdToSatClause::const_iterator it
;
450 std::set
<Node
>::iterator lemmaIt
;
452 if (!options::aggressiveCoreMin()) {
453 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
454 std::set
<Node
> currentLemma
= satClauseToNodeSet(it
->second
);
456 // TODO: we should be able to drop the "haveProofRecipe" check.
457 // however, there are some rewrite issues with the arith solver, resulting
458 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
459 LemmaProofRecipe recipe
;
460 if (!getCnfProof()->haveProofRecipe(currentLemma
))
463 recipe
= getCnfProof()->getProofRecipe(currentLemma
);
464 if (recipe
.getOriginalLemma() == lemma
) {
465 for (lemmaIt
= currentLemma
.begin(); lemmaIt
!= currentLemma
.end(); ++lemmaIt
) {
468 // Check that each conjunct appears in the original lemma.
470 for (unsigned i
= 0; i
< lemma
.getNumChildren(); ++i
) {
471 if (lemma
[i
] == *lemmaIt
)
482 for (it
= used_lemmas
.begin(); it
!= used_lemmas
.end(); ++it
) {
483 std::set
<Node
> currentLemma
= satClauseToNodeSet(it
->second
);
485 // TODO: we should be able to drop the "haveProofRecipe" check.
486 // however, there are some rewrite issues with the arith solver, resulting
487 // in non-registered recipes. For now we assume no one is requesting arith lemmas.
488 LemmaProofRecipe recipe
;
489 if (!getCnfProof()->haveProofRecipe(currentLemma
))
492 recipe
= getCnfProof()->getProofRecipe(currentLemma
);
493 if (recipe
.getOriginalLemma() == lemma
) {
494 NodeBuilder
<> disjunction(kind::OR
);
495 for (lemmaIt
= currentLemma
.begin(); lemmaIt
!= currentLemma
.end(); ++lemmaIt
) {
496 disjunction
<< *lemmaIt
;
499 Node conjunct
= (disjunction
.getNumChildren() == 1) ? disjunction
[0] : disjunction
;
505 AlwaysAssert(builder
.getNumChildren() != 0);
507 if (builder
.getNumChildren() == 1)
513 void ProofManager::addAssertion(Expr formula
) {
514 Debug("proof:pm") << "assert: " << formula
<< std::endl
;
515 d_inputFormulas
.insert(formula
);
516 std::ostringstream name
;
517 name
<< "A" << d_inputFormulaToName
.size();
518 d_inputFormulaToName
[formula
] = name
.str();
521 void ProofManager::addCoreAssertion(Expr formula
) {
522 Debug("cores") << "assert: " << formula
<< std::endl
;
523 d_deps
[Node::fromExpr(formula
)]; // empty vector of deps
524 d_inputCoreFormulas
.insert(formula
);
527 void ProofManager::addDependence(TNode n
, TNode dep
) {
529 Debug("cores") << "dep: " << n
<< " : " << dep
<< std::endl
;
530 if( !dep
.isNull() && d_deps
.find(dep
) == d_deps
.end()) {
531 Debug("cores") << "WHERE DID " << dep
<< " come from ??" << std::endl
;
533 std::vector
<Node
> deps
= d_deps
[n
].get();
539 void ProofManager::addUnsatCore(Expr formula
) {
540 Assert(d_inputCoreFormulas
.find(formula
) != d_inputCoreFormulas
.end());
541 d_outputCoreFormulas
.insert(formula
);
544 void ProofManager::addAssertionFilter(const Node
& node
, const std::string
& rewritten
) {
545 d_assertionFilters
[node
] = rewritten
;
548 void ProofManager::setLogic(const LogicInfo
& logic
) {
552 LFSCProof::LFSCProof(SmtEngine
* smtEngine
,
555 LFSCTheoryProofEngine
* theory
)
558 d_theoryProof(theory
),
559 d_smtEngine(smtEngine
)
562 void LFSCProof::toStream(std::ostream
& out
, const ProofLetMap
& map
) const
567 void LFSCProof::toStream(std::ostream
& out
) const
569 TimerStat::CodeTimer
proofProductionTimer(
570 ProofManager::currentPM()->getStats().d_proofProductionTime
);
572 IdToSatClause used_lemmas
;
573 IdToSatClause used_inputs
;
574 std::set
<Node
> atoms
;
575 NodePairSet rewrites
;
576 NodeSet used_assertions
;
579 CodeTimer skeletonProofTimer
{
580 ProofManager::currentPM()->getStats().d_skeletonProofTraceTime
};
581 Assert(!d_satProof
->proofConstructed());
582 d_satProof
->constructProof();
584 // collecting leaf clauses in resolution proof
585 d_satProof
->collectClausesUsed(used_inputs
, used_lemmas
);
587 IdToSatClause::iterator it2
;
588 Debug("pf::pm") << std::endl
<< "Used inputs: " << std::endl
;
589 for (it2
= used_inputs
.begin(); it2
!= used_inputs
.end(); ++it2
)
591 Debug("pf::pm") << "\t input = " << *(it2
->second
) << std::endl
;
593 Debug("pf::pm") << std::endl
;
595 Debug("pf::pm") << std::endl
<< "Used lemmas: " << std::endl
;
596 for (it2
= used_lemmas
.begin(); it2
!= used_lemmas
.end(); ++it2
)
598 std::vector
<Expr
> clause_expr
;
599 for (unsigned i
= 0; i
< it2
->second
->size(); ++i
)
601 prop::SatLiteral lit
= (*(it2
->second
))[i
];
602 Expr atom
= d_cnfProof
->getAtom(lit
.getSatVariable()).toExpr();
605 Assert(atom
== utils::mkTrue());
608 Expr expr_lit
= lit
.isNegated() ? atom
.notExpr() : atom
;
609 clause_expr
.push_back(expr_lit
);
612 Debug("pf::pm") << "\t lemma " << it2
->first
<< " = " << *(it2
->second
)
614 Debug("pf::pm") << "\t";
615 for (unsigned i
= 0; i
< clause_expr
.size(); ++i
)
617 Debug("pf::pm") << clause_expr
[i
] << " ";
619 Debug("pf::pm") << std::endl
;
621 Debug("pf::pm") << std::endl
;
623 // collecting assertions that lead to the clauses being asserted
624 d_cnfProof
->collectAssertionsForClauses(used_inputs
, used_assertions
);
626 NodeSet::iterator it3
;
627 Debug("pf::pm") << std::endl
<< "Used assertions: " << std::endl
;
628 for (it3
= used_assertions
.begin(); it3
!= used_assertions
.end(); ++it3
)
629 Debug("pf::pm") << "\t assertion = " << *it3
<< std::endl
;
631 // collects the atoms in the clauses
632 d_cnfProof
->collectAtomsAndRewritesForLemmas(used_lemmas
, atoms
, rewrites
);
634 if (!rewrites
.empty())
636 Debug("pf::pm") << std::endl
<< "Rewrites used in lemmas: " << std::endl
;
637 NodePairSet::const_iterator rewriteIt
;
638 for (rewriteIt
= rewrites
.begin(); rewriteIt
!= rewrites
.end();
641 Debug("pf::pm") << "\t" << rewriteIt
->first
<< " --> "
642 << rewriteIt
->second
<< std::endl
;
644 Debug("pf::pm") << std::endl
<< "Rewrite printing done" << std::endl
;
648 Debug("pf::pm") << "No rewrites in lemmas found" << std::endl
;
651 // The derived/unrewritten atoms may not have CNF literals required later
652 // on. If they don't, add them.
653 std::set
<Node
>::const_iterator it
;
654 for (it
= atoms
.begin(); it
!= atoms
.end(); ++it
)
656 Debug("pf::pm") << "Ensure literal for atom: " << *it
<< std::endl
;
657 if (!d_cnfProof
->hasLiteral(*it
))
659 // For arithmetic: these literals are not normalized, causing an error
661 if (theory::Theory::theoryOf(*it
) == theory::THEORY_ARITH
)
663 d_cnfProof
->ensureLiteral(
665 true); // This disables preregistration with the theory solver.
669 d_cnfProof
->ensureLiteral(
670 *it
); // Normal method, with theory solver preregisteration.
675 d_cnfProof
->collectAtomsForClauses(used_inputs
, atoms
);
676 d_cnfProof
->collectAtomsForClauses(used_lemmas
, atoms
);
678 // collects the atoms in the assertions
679 for (NodeSet::const_iterator it
= used_assertions
.begin();
680 it
!= used_assertions
.end();
683 utils::collectAtoms(*it
, atoms
);
686 std::set
<Node
>::iterator atomIt
;
687 Debug("pf::pm") << std::endl
688 << "Dumping atoms from lemmas, inputs and assertions: "
691 for (atomIt
= atoms
.begin(); atomIt
!= atoms
.end(); ++atomIt
)
693 Debug("pf::pm") << "\tAtom: " << *atomIt
<< std::endl
;
697 smt::SmtScope
scope(d_smtEngine
);
698 ProofLetMap globalLetMap
;
699 std::ostringstream paren
;
702 ProofManager::currentPM()->getStats().d_proofDeclarationsTime
};
705 out
<< " ;; Declarations\n";
707 // declare the theory atoms
708 Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl
;
709 for (std::set
<Node
>::const_iterator it
= atoms
.begin(); it
!= atoms
.end(); ++it
)
711 Debug("pf::pm") << "\tTerm: " << (*it
).toExpr() << std::endl
;
712 d_theoryProof
->registerTerm((*it
).toExpr());
715 Debug("pf::pm") << std::endl
716 << "Term registration done!" << std::endl
719 Debug("pf::pm") << std::endl
720 << "LFSCProof::toStream: starting to print assertions"
723 // print out all the original assertions
724 d_theoryProof
->registerTermsFromAssertions();
725 d_theoryProof
->printSortDeclarations(out
, paren
);
726 d_theoryProof
->printTermDeclarations(out
, paren
);
727 d_theoryProof
->printAssertions(out
, paren
);
729 Debug("pf::pm") << std::endl
730 << "LFSCProof::toStream: print assertions DONE"
733 out
<< "(: (holds cln)\n\n";
736 // Have the theory proofs print deferred declarations, e.g. for skolem
738 out
<< " ;; Printing deferred declarations \n\n";
739 d_theoryProof
->printDeferredDeclarations(out
, paren
);
741 out
<< "\n ;; Printing the global let map";
742 d_theoryProof
->finalizeBvConflicts(used_lemmas
, out
);
743 ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
744 if (options::lfscLetification())
746 ProofManager::currentPM()->printGlobalLetMap(
747 atoms
, globalLetMap
, out
, paren
);
750 out
<< " ;; Printing aliasing declarations \n\n";
751 d_theoryProof
->printAliasingDeclarations(out
, paren
, globalLetMap
);
753 out
<< " ;; Rewrites for Lemmas \n";
754 d_theoryProof
->printLemmaRewrites(rewrites
, out
, paren
);
756 // print trust that input assertions are their preprocessed form
757 printPreprocessedAssertions(used_assertions
, out
, paren
, globalLetMap
);
761 CodeTimer cnfProofTimer
{
762 ProofManager::currentPM()->getStats().d_cnfProofTime
};
763 // print mapping between theory atoms and internal SAT variables
764 out
<< ";; Printing mapping from preprocessed assertions into atoms \n";
765 d_cnfProof
->printAtomMapping(atoms
, out
, paren
, globalLetMap
);
767 Debug("pf::pm") << std::endl
768 << "Printing cnf proof for clauses" << std::endl
;
770 IdToSatClause::const_iterator cl_it
= used_inputs
.begin();
771 // print CNF conversion proof for each clause
772 for (; cl_it
!= used_inputs
.end(); ++cl_it
)
774 d_cnfProof
->printCnfProofForClause(
775 cl_it
->first
, cl_it
->second
, out
, paren
);
780 CodeTimer theoryLemmaTimer
{
781 ProofManager::currentPM()->getStats().d_theoryLemmaTime
};
782 Debug("pf::pm") << std::endl
783 << "Printing cnf proof for clauses DONE" << std::endl
;
785 Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl
;
786 d_theoryProof
->printTheoryLemmas(used_lemmas
, out
, paren
, globalLetMap
);
787 Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!"
792 CodeTimer finalProofTimer
{
793 ProofManager::currentPM()->getStats().d_finalProofTime
};
794 out
<< ";; Printing final unsat proof \n";
795 if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
796 && ProofManager::getBitVectorProof())
798 ProofManager::getBitVectorProof()->printEmptyClauseProof(out
, paren
);
802 // print actual resolution proof
803 proof::LFSCProofPrinter::printResolutions(d_satProof
, out
, paren
);
804 proof::LFSCProofPrinter::printResolutionEmptyClause(
805 d_satProof
, out
, paren
);
813 void LFSCProof::printPreprocessedAssertions(const NodeSet
& assertions
,
816 ProofLetMap
& globalLetMap
) const
818 os
<< "\n ;; In the preprocessor we trust \n";
819 NodeSet::const_iterator it
= assertions
.begin();
820 NodeSet::const_iterator end
= assertions
.end();
822 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl
;
824 if (options::fewerPreprocessingHoles()) {
825 // Check for assertions that did not get rewritten, and update the printing filter.
826 checkUnrewrittenAssertion(assertions
);
828 // For the remaining assertions, bind them to input assertions.
829 for (; it
!= end
; ++it
) {
830 // Rewrite preprocessing step if it cannot be eliminated
831 if (!ProofManager::currentPM()->have_input_assertion((*it
).toExpr())) {
832 os
<< "(th_let_pf _ (trust_f (iff ";
836 if (((*it
).isConst() && *it
== NodeManager::currentNM()->mkConst
<bool>(true)) ||
837 ((*it
).getKind() == kind::NOT
&& (*it
)[0] == NodeManager::currentNM()->mkConst
<bool>(false))) {
838 inputAssertion
= NodeManager::currentNM()->mkConst
<bool>(true).toExpr();
840 // Figure out which input assertion led to this assertion
841 ExprSet inputAssertions
;
842 ProofManager::currentPM()->traceDeps(*it
, &inputAssertions
);
844 Debug("pf::pm") << "Original assertions for " << *it
<< " are: " << std::endl
;
846 ProofManager::assertions_iterator assertionIt
;
847 for (assertionIt
= inputAssertions
.begin(); assertionIt
!= inputAssertions
.end(); ++assertionIt
) {
848 Debug("pf::pm") << "\t" << *assertionIt
<< std::endl
;
851 if (inputAssertions
.size() == 0) {
852 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl
;
853 // For now just use the first assertion...
854 inputAssertion
= *(ProofManager::currentPM()->begin_assertions());
856 if (inputAssertions
.size() != 1) {
857 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl
;
859 inputAssertion
= *inputAssertions
.begin();
863 if (!ProofManager::currentPM()->have_input_assertion(inputAssertion
)) {
864 // The thing returned by traceDeps does not appear in the input assertions...
865 Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl
;
866 // For now just use the first assertion...
867 inputAssertion
= *(ProofManager::currentPM()->begin_assertions());
870 Debug("pf::pm") << "Original assertion for " << *it
874 << ProofManager::currentPM()->getInputFormulaName(inputAssertion
)
877 ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion
, os
, globalLetMap
);
879 ProofManager::currentPM()->printTrustedTerm(*it
, os
, globalLetMap
);
881 os
<< "(\\ "<< ProofManager::getPreprocessedAssertionName(*it
, "") << "\n";
884 std::ostringstream rewritten
;
886 rewritten
<< "(or_elim_1 _ _ ";
887 rewritten
<< "(not_not_intro _ ";
888 rewritten
<< ProofManager::currentPM()->getInputFormulaName(inputAssertion
);
889 rewritten
<< ") (iff_elim_1 _ _ ";
890 rewritten
<< ProofManager::getPreprocessedAssertionName(*it
, "");
893 ProofManager::currentPM()->addAssertionFilter(*it
, rewritten
.str());
897 for (; it
!= end
; ++it
) {
898 os
<< "(th_let_pf _ ";
902 ProofManager::currentPM()->printTrustedTerm(*it
, os
, globalLetMap
);
905 os
<< "(\\ "<< ProofManager::getPreprocessedAssertionName(*it
, "") << "\n";
913 void LFSCProof::checkUnrewrittenAssertion(const NodeSet
& rewrites
) const
915 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl
;
917 NodeSet::const_iterator rewrite
;
918 for (rewrite
= rewrites
.begin(); rewrite
!= rewrites
.end(); ++rewrite
) {
919 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite
<< std::endl
;
920 if (ProofManager::currentPM()->have_input_assertion((*rewrite
).toExpr())) {
922 ProofManager::currentPM()->have_input_assertion((*rewrite
).toExpr()));
923 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl
924 << "\tAdding filter: "
925 << ProofManager::getPreprocessedAssertionName(*rewrite
, "")
927 << ProofManager::currentPM()->getInputFormulaName((*rewrite
).toExpr())
929 ProofManager::currentPM()->addAssertionFilter(*rewrite
,
930 ProofManager::currentPM()->getInputFormulaName((*rewrite
).toExpr()));
932 Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite
<< std::endl
;
939 bool ProofManager::hasOp(TNode n
) const {
940 return d_bops
.find(n
) != d_bops
.end();
943 Node
ProofManager::lookupOp(TNode n
) const {
944 std::map
<Node
, Node
>::const_iterator i
= d_bops
.find(n
);
945 Assert(i
!= d_bops
.end());
949 Node
ProofManager::mkOp(TNode n
) {
950 Trace("mgd-pm-mkop") << "MkOp : " << n
<< " " << n
.getKind() << std::endl
;
951 if(n
.getKind() != kind::BUILTIN
) {
957 Assert((n
.getConst
<Kind
>() == kind::SELECT
)
958 || (n
.getConst
<Kind
>() == kind::STORE
));
960 Debug("mgd-pm-mkop") << "making an op for " << n
<< "\n";
962 std::stringstream ss
;
964 std::string s
= ss
.str();
965 Debug("mgd-pm-mkop") << " : " << s
<< std::endl
;
966 std::vector
<TypeNode
> v
;
967 v
.push_back(NodeManager::currentNM()->integerType());
968 if(n
.getConst
<Kind
>() == kind::SELECT
) {
969 v
.push_back(NodeManager::currentNM()->integerType());
970 v
.push_back(NodeManager::currentNM()->integerType());
971 } else if(n
.getConst
<Kind
>() == kind::STORE
) {
972 v
.push_back(NodeManager::currentNM()->integerType());
973 v
.push_back(NodeManager::currentNM()->integerType());
974 v
.push_back(NodeManager::currentNM()->integerType());
976 TypeNode type
= NodeManager::currentNM()->mkFunctionType(v
);
977 Debug("mgd-pm-mkop") << "typenode is: " << type
<< "\n";
978 op
= NodeManager::currentNM()->mkSkolem(s
, type
, " ignore", NodeManager::SKOLEM_NO_NOTIFY
);
981 Debug("mgd-pm-mkop") << "returning the op: " << op
<< "\n";
984 //---end from Morgan---
986 bool ProofManager::wasPrinted(const Type
& type
) const {
987 return d_printedTypes
.find(type
) != d_printedTypes
.end();
990 void ProofManager::markPrinted(const Type
& type
) {
991 d_printedTypes
.insert(type
);
994 void ProofManager::addRewriteFilter(const std::string
&original
, const std::string
&substitute
) {
995 d_rewriteFilters
[original
] = substitute
;
998 bool ProofManager::haveRewriteFilter(TNode lit
) {
999 std::string litName
= getLitName(currentPM()->d_cnfProof
->getLiteral(lit
));
1000 return d_rewriteFilters
.find(litName
) != d_rewriteFilters
.end();
1003 void ProofManager::clearRewriteFilters() {
1004 d_rewriteFilters
.clear();
1007 std::ostream
& operator<<(std::ostream
& out
, CVC4::ProofRule k
) {
1010 out
<< "RULE_GIVEN";
1013 out
<< "RULE_DERIVED";
1015 case RULE_RECONSTRUCT
:
1016 out
<< "RULE_RECONSTRUCT";
1019 out
<< "RULE_TRUST";
1022 out
<< "RULE_INVALID";
1025 out
<< "RULE_CONFLICT";
1028 out
<< "RULE_TSEITIN";
1031 out
<< "RULE_SPLIT";
1033 case RULE_ARRAYS_EXT
:
1034 out
<< "RULE_ARRAYS";
1036 case RULE_ARRAYS_ROW
:
1037 out
<< "RULE_ARRAYS";
1040 out
<< "ProofRule Unknown! [" << unsigned(k
) << "]";
1046 void ProofManager::registerRewrite(unsigned ruleId
, Node original
, Node result
){
1047 Assert(currentPM()->d_theoryProof
!= NULL
);
1048 currentPM()->d_rewriteLog
.push_back(RewriteLogEntry(ruleId
, original
, result
));
1051 void ProofManager::clearRewriteLog() {
1052 Assert(currentPM()->d_theoryProof
!= NULL
);
1053 currentPM()->d_rewriteLog
.clear();
1056 std::vector
<RewriteLogEntry
> ProofManager::getRewriteLog() {
1057 return currentPM()->d_rewriteLog
;
1060 void ProofManager::dumpRewriteLog() const {
1061 Debug("pf::rr") << "Dumpign rewrite log:" << std::endl
;
1063 for (unsigned i
= 0; i
< d_rewriteLog
.size(); ++i
) {
1064 Debug("pf::rr") << "\tRule " << d_rewriteLog
[i
].getRuleId()
1066 << d_rewriteLog
[i
].getOriginal()
1068 << d_rewriteLog
[i
].getResult() << std::endl
;
1072 void bind(Expr term
, ProofLetMap
& map
, Bindings
& letOrder
) {
1073 ProofLetMap::iterator it
= map
.find(term
);
1074 if (it
!= map
.end())
1077 for (unsigned i
= 0; i
< term
.getNumChildren(); ++i
)
1078 bind(term
[i
], map
, letOrder
);
1080 // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)).
1081 // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too.
1082 Kind k
= term
.getKind();
1083 if (((k
== kind::OR
) || (k
== kind::AND
)) && term
.getNumChildren() > 2) {
1084 Node currentExpression
= term
[term
.getNumChildren() - 1];
1085 for (int i
= term
.getNumChildren() - 2; i
>= 0; --i
) {
1086 NodeBuilder
<> builder(k
);
1088 builder
<< currentExpression
.toExpr();
1089 currentExpression
= builder
;
1090 bind(currentExpression
.toExpr(), map
, letOrder
);
1093 unsigned newId
= ProofLetCount::newId();
1094 ProofLetCount
letCount(newId
);
1095 map
[term
] = letCount
;
1096 letOrder
.push_back(LetOrderElement(term
, newId
));
1100 void ProofManager::printGlobalLetMap(std::set
<Node
>& atoms
,
1101 ProofLetMap
& letMap
,
1103 std::ostringstream
& paren
) {
1105 std::set
<Node
>::const_iterator atom
;
1106 for (atom
= atoms
.begin(); atom
!= atoms
.end(); ++atom
) {
1107 bind(atom
->toExpr(), letMap
, letOrder
);
1110 // TODO: give each theory a chance to add atoms. For now, just query BV directly...
1111 const std::set
<Node
>* additionalAtoms
= ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
1112 for (atom
= additionalAtoms
->begin(); atom
!= additionalAtoms
->end(); ++atom
) {
1113 bind(atom
->toExpr(), letMap
, letOrder
);
1116 for (unsigned i
= 0; i
< letOrder
.size(); ++i
) {
1117 Expr currentExpr
= letOrder
[i
].expr
;
1118 unsigned letId
= letOrder
[i
].id
;
1119 ProofLetMap::iterator it
= letMap
.find(currentExpr
);
1120 Assert(it
!= letMap
.end());
1121 out
<< "\n(@ let" << letId
<< " ";
1122 d_theoryProof
->printBoundTerm(currentExpr
, out
, letMap
);
1124 it
->second
.increment();
1127 out
<< std::endl
<< std::endl
;
1130 void ProofManager::ensureLiteral(Node node
) {
1131 d_cnfProof
->ensureLiteral(node
);
1133 void ProofManager::printTrustedTerm(Node term
,
1135 ProofLetMap
& globalLetMap
)
1137 TheoryProofEngine
* tpe
= ProofManager::currentPM()->getTheoryProofEngine();
1138 if (tpe
->printsAsBool(term
)) os
<< "(p_app ";
1139 tpe
->printTheoryTerm(term
.toExpr(), os
, globalLetMap
);
1140 if (tpe
->printsAsBool(term
)) os
<< ")";
1143 ProofManager::ProofManagerStatistics::ProofManagerStatistics()
1144 : d_proofProductionTime("proof::ProofManager::proofProductionTime"),
1146 "proof::ProofManager::proofProduction::theoryLemmaTime"),
1147 d_skeletonProofTraceTime(
1148 "proof::ProofManager::proofProduction::skeletonProofTraceTime"),
1149 d_proofDeclarationsTime(
1150 "proof::ProofManager::proofProduction::proofDeclarationsTime"),
1151 d_cnfProofTime("proof::ProofManager::proofProduction::cnfProofTime"),
1152 d_finalProofTime("proof::ProofManager::proofProduction::finalProofTime")
1154 smtStatisticsRegistry()->registerStat(&d_proofProductionTime
);
1155 smtStatisticsRegistry()->registerStat(&d_theoryLemmaTime
);
1156 smtStatisticsRegistry()->registerStat(&d_skeletonProofTraceTime
);
1157 smtStatisticsRegistry()->registerStat(&d_proofDeclarationsTime
);
1158 smtStatisticsRegistry()->registerStat(&d_cnfProofTime
);
1159 smtStatisticsRegistry()->registerStat(&d_finalProofTime
);
1162 ProofManager::ProofManagerStatistics::~ProofManagerStatistics()
1164 smtStatisticsRegistry()->unregisterStat(&d_proofProductionTime
);
1165 smtStatisticsRegistry()->unregisterStat(&d_theoryLemmaTime
);
1166 smtStatisticsRegistry()->unregisterStat(&d_skeletonProofTraceTime
);
1167 smtStatisticsRegistry()->unregisterStat(&d_proofDeclarationsTime
);
1168 smtStatisticsRegistry()->unregisterStat(&d_cnfProofTime
);
1169 smtStatisticsRegistry()->unregisterStat(&d_finalProofTime
);
1172 } /* CVC4 namespace */