1 /********************* */
2 /*! \file cnf_proof.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Andrew Reynolds, Alex Ozdemir
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
11 **
12 ** \brief [[ Add one-line brief description here ]]
13 **
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
16 **/
17
18 #include "proof/cnf_proof.h"
19
20 #include "proof/clause_id.h"
21 #include "proof/proof_manager.h"
22 #include "proof/proof_utils.h"
23 #include "proof/theory_proof.h"
24 #include "prop/cnf_stream.h"
25 #include "prop/minisat/minisat.h"
26 #include "prop/sat_solver_types.h"
27
28 namespace CVC4 {
29
CnfProof(prop::CnfStream * stream,context::Context * ctx,const std::string & name)30 CnfProof::CnfProof(prop::CnfStream* stream,
31 context::Context* ctx,
32 const std::string& name)
33 : d_cnfStream(stream)
34 , d_clauseToAssertion(ctx)
35 , d_assertionToProofRule(ctx)
36 , d_currentAssertionStack()
37 , d_currentDefinitionStack()
38 , d_clauseToDefinition(ctx)
39 , d_definitions()
40 , d_cnfDeps()
41 , d_name(name)
42 {
43 // Setting the proof object for the CnfStream
44 d_cnfStream->setProof(this);
45 }
46
~CnfProof()47 CnfProof::~CnfProof() {}
48
isAssertion(Node node)49 bool CnfProof::isAssertion(Node node) {
50 return d_assertionToProofRule.find(node) !=
51 d_assertionToProofRule.end();
52 }
53
isDefinition(Node node)54 bool CnfProof::isDefinition(Node node) {
55 return d_definitions.find(node) !=
56 d_definitions.end();
57 }
58
getProofRule(Node node)59 ProofRule CnfProof::getProofRule(Node node) {
60 Assert (isAssertion(node));
61 NodeToProofRule::iterator it = d_assertionToProofRule.find(node);
62 return (*it).second;
63 }
64
getProofRule(ClauseId clause)65 ProofRule CnfProof::getProofRule(ClauseId clause) {
66 TNode assertion = getAssertionForClause(clause);
67 return getProofRule(assertion);
68 }
69
getAssertionForClause(ClauseId clause)70 Node CnfProof::getAssertionForClause(ClauseId clause) {
71 ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause);
72 Assert (it != d_clauseToAssertion.end());
73 return (*it).second;
74 }
75
getDefinitionForClause(ClauseId clause)76 Node CnfProof::getDefinitionForClause(ClauseId clause) {
77 ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause);
78 Assert (it != d_clauseToDefinition.end());
79 return (*it).second;
80 }
81
registerConvertedClause(ClauseId clause,bool explanation)82 void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
83 Assert (clause != ClauseIdUndef &&
84 clause != ClauseIdError &&
85 clause != ClauseIdEmpty);
86
87 // Explanations do not need a CNF conversion proof since they are in CNF
88 // (they will only need a theory proof as they are theory valid)
89 if (explanation) {
90 Debug("proof:cnf") << "CnfProof::registerConvertedClause "
91 << clause << " explanation? " << explanation << std::endl;
92 Assert (d_explanations.find(clause) == d_explanations.end());
93 d_explanations.insert(clause);
94 return;
95 }
96
97 Node current_assertion = getCurrentAssertion();
98 Node current_expr = getCurrentDefinition();
99
100 Debug("proof:cnf") << "CnfProof::registerConvertedClause "
101 << clause << " assertion = " << current_assertion
102 << clause << " definition = " << current_expr << std::endl;
103
104 setClauseAssertion(clause, current_assertion);
105 setClauseDefinition(clause, current_expr);
106 }
107
registerTrueUnitClause(ClauseId clauseId)108 void CnfProof::registerTrueUnitClause(ClauseId clauseId)
109 {
110 Node trueNode = NodeManager::currentNM()->mkConst<bool>(true);
111 pushCurrentAssertion(trueNode);
112 pushCurrentDefinition(trueNode);
113 registerConvertedClause(clauseId);
114 popCurrentAssertion();
115 popCurrentDefinition();
116 d_cnfStream->ensureLiteral(trueNode);
117 d_trueUnitClause = clauseId;
118 }
119
registerFalseUnitClause(ClauseId clauseId)120 void CnfProof::registerFalseUnitClause(ClauseId clauseId)
121 {
122 Node falseNode = NodeManager::currentNM()->mkConst<bool>(false).notNode();
123 pushCurrentAssertion(falseNode);
124 pushCurrentDefinition(falseNode);
125 registerConvertedClause(clauseId);
126 popCurrentAssertion();
127 popCurrentDefinition();
128 d_cnfStream->ensureLiteral(falseNode);
129 d_falseUnitClause = clauseId;
130 }
131
setClauseAssertion(ClauseId clause,Node expr)132 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
133 Debug("proof:cnf") << "CnfProof::setClauseAssertion "
134 << clause << " assertion " << expr << std::endl;
135 // We can add the same clause from different assertions. In this
136 // case we keep the first assertion. For example asserting a /\ b
137 // and then b /\ c where b is an atom, would assert b twice (note
138 // that since b is top level, it is not cached by the CnfStream)
139 if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end())
140 return;
141
142 d_clauseToAssertion.insert (clause, expr);
143 }
144
setClauseDefinition(ClauseId clause,Node definition)145 void CnfProof::setClauseDefinition(ClauseId clause, Node definition) {
146 Debug("proof:cnf") << "CnfProof::setClauseDefinition "
147 << clause << " definition " << definition << std::endl;
148 // We keep the first definition
149 if (d_clauseToDefinition.find(clause) != d_clauseToDefinition.end())
150 return;
151
152 d_clauseToDefinition.insert(clause, definition);
153 d_definitions.insert(definition);
154 }
155
registerAssertion(Node assertion,ProofRule reason)156 void CnfProof::registerAssertion(Node assertion, ProofRule reason) {
157 Debug("proof:cnf") << "CnfProof::registerAssertion "
158 << assertion << " reason " << reason << std::endl;
159 // We can obtain the assertion from different reasons (e.g. if the
160 // assertion is a lemma over shared terms both theories can generate
161 // the same lemma) We only need to prove the lemma in one way, so we
162 // keep the first reason.
163 if (isAssertion(assertion)) {
164 return;
165 }
166 d_assertionToProofRule.insert(assertion, reason);
167 }
168
getProofRecipe(const std::set<Node> & lemma)169 LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
170 Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
171 return d_lemmaToProofRecipe[lemma];
172 }
173
haveProofRecipe(const std::set<Node> & lemma)174 bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
175 return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
176 }
177
setCnfDependence(Node from,Node to)178 void CnfProof::setCnfDependence(Node from, Node to) {
179 Debug("proof:cnf") << "CnfProof::setCnfDependence "
180 << "from " << from << std::endl
181 << " to " << to << std::endl;
182
183 Assert (from != to);
184 d_cnfDeps.insert(std::make_pair(from, to));
185 }
186
pushCurrentAssertion(Node assertion)187 void CnfProof::pushCurrentAssertion(Node assertion) {
188 Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
189 << std::endl;
190
191 d_currentAssertionStack.push_back(assertion);
192
193 Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
194 << "new stack size = " << d_currentAssertionStack.size()
195 << std::endl;
196 }
197
popCurrentAssertion()198 void CnfProof::popCurrentAssertion() {
199 Assert (d_currentAssertionStack.size());
200
201 Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
202 << d_currentAssertionStack.back() << std::endl;
203
204 d_currentAssertionStack.pop_back();
205
206 Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
207 << "new stack size = " << d_currentAssertionStack.size()
208 << std::endl;
209 }
210
getCurrentAssertion()211 Node CnfProof::getCurrentAssertion() {
212 Assert (d_currentAssertionStack.size());
213 return d_currentAssertionStack.back();
214 }
215
setProofRecipe(LemmaProofRecipe * proofRecipe)216 void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
217 Assert(proofRecipe);
218 Assert(proofRecipe->getNumSteps() > 0);
219 d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
220 }
221
pushCurrentDefinition(Node definition)222 void CnfProof::pushCurrentDefinition(Node definition) {
223 Debug("proof:cnf") << "CnfProof::pushCurrentDefinition "
224 << definition << std::endl;
225
226 d_currentDefinitionStack.push_back(definition);
227 }
228
popCurrentDefinition()229 void CnfProof::popCurrentDefinition() {
230 Assert (d_currentDefinitionStack.size());
231
232 Debug("proof:cnf") << "CnfProof::popCurrentDefinition "
233 << d_currentDefinitionStack.back() << std::endl;
234
235 d_currentDefinitionStack.pop_back();
236 }
237
getCurrentDefinition()238 Node CnfProof::getCurrentDefinition() {
239 Assert (d_currentDefinitionStack.size());
240 return d_currentDefinitionStack.back();
241 }
242
getAtom(prop::SatVariable var)243 Node CnfProof::getAtom(prop::SatVariable var) {
244 prop::SatLiteral lit (var);
245 Node node = d_cnfStream->getNode(lit);
246 return node;
247 }
248
collectAtoms(const prop::SatClause * clause,std::set<Node> & atoms)249 void CnfProof::collectAtoms(const prop::SatClause* clause,
250 std::set<Node>& atoms) {
251 for (unsigned i = 0; i < clause->size(); ++i) {
252 prop::SatLiteral lit = clause->operator[](i);
253 prop::SatVariable var = lit.getSatVariable();
254 TNode atom = getAtom(var);
255 if (atoms.find(atom) == atoms.end()) {
256 atoms.insert(atom);
257 }
258 }
259 }
260
getLiteral(TNode atom)261 prop::SatLiteral CnfProof::getLiteral(TNode atom) {
262 return d_cnfStream->getLiteral(atom);
263 }
264
hasLiteral(TNode atom)265 bool CnfProof::hasLiteral(TNode atom) {
266 return d_cnfStream->hasLiteral(atom);
267 }
268
ensureLiteral(TNode atom,bool noPreregistration)269 void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) {
270 d_cnfStream->ensureLiteral(atom, noPreregistration);
271 }
272
collectAtomsForClauses(const IdToSatClause & clauses,std::set<Node> & atoms)273 void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses,
274 std::set<Node>& atoms) {
275 IdToSatClause::const_iterator it = clauses.begin();
276 for (; it != clauses.end(); ++it) {
277 const prop::SatClause* clause = it->second;
278 collectAtoms(clause, atoms);
279 }
280 }
281
collectAtomsAndRewritesForLemmas(const IdToSatClause & lemmaClauses,std::set<Node> & atoms,NodePairSet & rewrites)282 void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
283 std::set<Node>& atoms,
284 NodePairSet& rewrites) {
285 IdToSatClause::const_iterator it = lemmaClauses.begin();
286 for (; it != lemmaClauses.end(); ++it) {
287 const prop::SatClause* clause = it->second;
288
289 // TODO: just calculate the map from ID to recipe once,
290 // instead of redoing this over and over again
291 std::vector<Expr> clause_expr;
292 std::set<Node> clause_expr_nodes;
293 for(unsigned i = 0; i < clause->size(); ++i) {
294 prop::SatLiteral lit = (*clause)[i];
295 Node node = getAtom(lit.getSatVariable());
296 Expr atom = node.toExpr();
297 if (atom.isConst()) {
298 Assert (atom == utils::mkTrue());
299 continue;
300 }
301 clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
302 }
303
304 LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes);
305
306 for (unsigned i = 0; i < recipe.getNumSteps(); ++i) {
307 const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i);
308 Node atom = proofStep->getLiteral();
309
310 if (atom == Node()) {
311 // The last proof step always has the empty node as its target...
312 continue;
313 }
314
315 if (atom.getKind() == kind::NOT) {
316 atom = atom[0];
317 }
318
319 atoms.insert(atom);
320 }
321
322 LemmaProofRecipe::RewriteIterator rewriteIt;
323 for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) {
324 rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second));
325
326 // The unrewritten terms also need to have literals, so insert them into atoms
327 Node rewritten = rewriteIt->first;
328 if (rewritten.getKind() == kind::NOT) {
329 rewritten = rewritten[0];
330 }
331 atoms.insert(rewritten);
332 }
333 }
334 }
335
collectAssertionsForClauses(const IdToSatClause & clauses,NodeSet & assertions)336 void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
337 NodeSet& assertions) {
338 IdToSatClause::const_iterator it = clauses.begin();
339 for (; it != clauses.end(); ++it) {
340 TNode used_assertion = getAssertionForClause(it->first);
341 assertions.insert(used_assertion);
342 // it can be the case that a definition for a clause is an assertion
343 // but it is not the assertion for the clause
344 // e.g. the assertions [(and a b), a]
345 TNode used_definition = getDefinitionForClause(it->first);
346 if (isAssertion(used_definition)) {
347 assertions.insert(used_definition);
348 }
349 }
350 }
351
352 // Detects whether a clause has x v ~x for some x
353 // If so, returns the positive occurence's idx first, then the negative's
detectTrivialTautology(const prop::SatClause & clause)354 Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology(
355 const prop::SatClause& clause)
356 {
357 // a map from a SatVariable to its previous occurence's polarity and location
358 std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices;
359 for (size_t i = 0; i < clause.size(); ++i)
360 {
361 prop::SatLiteral lit = clause[i];
362 prop::SatVariable var = lit.getSatVariable();
363 bool polarity = !lit.isNegated();
364
365 // Check if this var has already occured w/ opposite polarity
366 auto iter = varsToPolsAndIndices.find(var);
367 if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
368 {
369 if (iter->second.first)
370 {
371 return Maybe<std::pair<size_t, size_t>>{
372 std::make_pair(iter->second.second, i)};
373 }
374 else
375 {
376 return Maybe<std::pair<size_t, size_t>>{
377 std::make_pair(i, iter->second.second)};
378 }
379 }
380 varsToPolsAndIndices[var] = std::make_pair(polarity, i);
381 }
382 return Maybe<std::pair<size_t, size_t>>{};
383 }
384
printAtomMapping(const std::set<Node> & atoms,std::ostream & os,std::ostream & paren)385 void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
386 std::ostream& os,
387 std::ostream& paren) {
388 std::set<Node>::const_iterator it = atoms.begin();
389 std::set<Node>::const_iterator end = atoms.end();
390
391 for (;it != end; ++it) {
392 os << "(decl_atom ";
393 Node atom = *it;
394 prop::SatVariable var = getLiteral(atom).getSatVariable();
395 //FIXME hideous
396 LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
397 pe->printLetTerm(atom.toExpr(), os);
398
399 os << " (\\ " << ProofManager::getVarName(var, d_name);
400 os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
401 paren << ")))";
402 }
403 }
404
printAtomMapping(const std::set<Node> & atoms,std::ostream & os,std::ostream & paren,ProofLetMap & letMap)405 void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
406 std::ostream& os,
407 std::ostream& paren,
408 ProofLetMap &letMap) {
409 std::set<Node>::const_iterator it = atoms.begin();
410 std::set<Node>::const_iterator end = atoms.end();
411
412 for (;it != end; ++it) {
413 os << "(decl_atom ";
414 Node atom = *it;
415 prop::SatVariable var = getLiteral(atom).getSatVariable();
416 //FIXME hideous
417 LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
418 if (pe->printsAsBool(atom.toExpr())) os << "(p_app ";
419 pe->printBoundTerm(atom.toExpr(), os, letMap);
420 if (pe->printsAsBool(atom.toExpr())) os << ")";
421
422 os << " (\\ " << ProofManager::getVarName(var, d_name);
423 os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
424 paren << ")))";
425 }
426 }
427
428 // maps each expr to the position it had in the clause and the polarity it had
clauseToNode(const prop::SatClause & clause,std::map<Node,unsigned> & childIndex,std::map<Node,bool> & childPol)429 Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause,
430 std::map<Node, unsigned>& childIndex,
431 std::map<Node, bool>& childPol ) {
432 std::vector< Node > children;
433 for (unsigned i = 0; i < clause.size(); ++i) {
434 prop::SatLiteral lit = clause[i];
435 prop::SatVariable var = lit.getSatVariable();
436 Node atom = getAtom(var);
437 children.push_back( lit.isNegated() ? atom.negate() : atom );
438 childIndex[atom] = i;
439 childPol[atom] = !lit.isNegated();
440 }
441 return children.size()==1 ? children[0] :
442 NodeManager::currentNM()->mkNode(kind::OR, children );
443 }
444
printCnfProofForClause(ClauseId id,const prop::SatClause * clause,std::ostream & os,std::ostream & paren)445 void LFSCCnfProof::printCnfProofForClause(ClauseId id,
446 const prop::SatClause* clause,
447 std::ostream& os,
448 std::ostream& paren) {
449 Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting "
450 << std::endl;
451
452 os << "(satlem _ _ ";
453 std::ostringstream clause_paren;
454 printClause(*clause, os, clause_paren);
455 os << "(clausify_false ";
456
457 // FIXMEEEEEEEEEEEE
458 // os <<"trust)";
459 // os << clause_paren.str()
460 // << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
461 // paren << "))";
462
463 // return;
464
465 Assert( clause->size()>0 );
466
467 // If the clause contains x v ~x, it's easy!
468 //
469 // It's important to check for this case, because our other logic for
470 // recording the location of variables in the clause assumes the clause is
471 // not tautological
472 Maybe<std::pair<size_t, size_t>> isTrivialTaut =
473 detectTrivialTautology(*clause);
474 if (isTrivialTaut.just())
475 {
476 size_t posIndexInClause = isTrivialTaut.value().first;
477 size_t negIndexInClause = isTrivialTaut.value().second;
478 Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
479 << negIndexInClause << " (-) make this clause a tautology"
480 << std::endl;
481
482 std::string proofOfPos =
483 ProofManager::getLitName((*clause)[negIndexInClause], d_name);
484 std::string proofOfNeg =
485 ProofManager::getLitName((*clause)[posIndexInClause], d_name);
486 os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
487 }
488 else
489 {
490 Node base_assertion = getDefinitionForClause(id);
491
492 // get the assertion for the clause id
493 std::map<Node, unsigned> childIndex;
494 std::map<Node, bool> childPol;
495 Node assertion = clauseToNode(*clause, childIndex, childPol);
496 // if there is no reason, construct assertion directly. This can happen
497 // for unit clauses.
498 if (base_assertion.isNull())
499 {
500 base_assertion = assertion;
501 }
502 // os_base is proof of base_assertion
503 std::stringstream os_base;
504
505 // checks if tautological definitional clause or top-level clause
506 // and prints the proof of the top-level formula
507 bool is_input = printProofTopLevel(base_assertion, os_base);
508
509 if (is_input)
510 {
511 Debug("cnf-pf") << std::endl
512 << "; base assertion is input. proof: " << os_base.str()
513 << std::endl;
514 }
515
516 // get base assertion with polarity
517 bool base_pol = base_assertion.getKind() != kind::NOT;
518 base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0]
519 : base_assertion;
520
521 std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion);
522 bool is_in_clause = itci != childIndex.end();
523 unsigned base_index = is_in_clause ? itci->second : 0;
524 Trace("cnf-pf") << std::endl;
525 Trace("cnf-pf") << "; input = " << is_input
526 << ", is_in_clause = " << is_in_clause << ", id = " << id
527 << ", assertion = " << assertion
528 << ", base assertion = " << base_assertion << std::endl;
529 if (!is_input)
530 {
531 Assert(is_in_clause);
532 prop::SatLiteral blit = (*clause)[base_index];
533 os_base << ProofManager::getLitName(blit, d_name);
534 base_pol = !childPol[base_assertion]; // WHY? if the case is =>
535 }
536 Trace("cnf-pf") << "; polarity of base assertion = " << base_pol
537 << std::endl;
538 Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
539
540 bool success = false;
541 if (is_input && is_in_clause && childPol[base_assertion] == base_pol)
542 {
543 // if both in input and in clause, the proof is trivial. this is the case
544 // for unit clauses.
545 Trace("cnf-pf") << "; trivial" << std::endl;
546 os << "(contra _ ";
547 success = true;
548 prop::SatLiteral lit = (*clause)[itci->second];
549 if (base_pol)
550 {
551 os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
552 }
553 else
554 {
555 os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
556 }
557 os << ")";
558 } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
559 ((base_assertion.getKind()==kind::OR ||
560 base_assertion.getKind()==kind::IMPLIES) && base_pol)) {
561 Trace("cnf-pf") << "; and/or case 1" << std::endl;
562 success = true;
563 std::stringstream os_main;
564 std::stringstream os_paren;
565 //eliminate each one
566 for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) {
567 Trace("cnf-pf-debug") << "; base_assertion[" << j << "] is: " << base_assertion[j]
568 << ", and its kind is: " << base_assertion[j].getKind() << std::endl ;
569
570 Node child_base = base_assertion[j].getKind()==kind::NOT ?
571 base_assertion[j][0] : base_assertion[j];
572 bool child_pol = base_assertion[j].getKind()!=kind::NOT;
573
574 Trace("cnf-pf-debug") << "; child " << j << " "
575 << ", child base: " << child_base
576 << ", child pol: " << child_pol
577 << ", childPol[child_base] "
578 << childPol[child_base] << ", base pol: " << base_pol << std::endl;
579
580 std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
581
582 if( itcic!=childIndex.end() ){
583 //Assert( child_pol==childPol[child_base] );
584 os_main << "(or_elim_1 _ _ ";
585 prop::SatLiteral lit = (*clause)[itcic->second];
586 // Should be if in the original formula it was negated
587 // if( childPol[child_base] && base_pol ){
588
589 // Adding the below to catch a specific case where the first child of an IMPLIES is negative,
590 // in which case we need not_not introduction.
591 if (base_assertion.getKind() == kind::IMPLIES && !child_pol && base_pol) {
592 os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") ";
593 } else if (childPol[child_base] && base_pol) {
594 os_main << ProofManager::getLitName(lit, d_name) << " ";
595 }else{
596 os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") ";
597 }
598 if( base_assertion.getKind()==kind::AND ){
599 os_main << "(not_and_elim _ _ ";
600 os_paren << ")";
601 }
602 os_paren << ")";
603 }else{
604 success = false;
605 }
606 }
607
608 if( success ){
609 if( base_assertion.getKind()==kind::IMPLIES ){
610 os_main << "(impl_elim _ _ ";
611 }
612 os_main << os_base.str();
613 if( base_assertion.getKind()==kind::IMPLIES ){
614 os_main << ")";
615 }
616 os_main << os_paren.str();
617 int last_index = base_assertion.getNumChildren()-1;
618 Node child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index];
619 //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT;
620 std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
621 if( itcic!=childIndex.end() ){
622 os << "(contra _ ";
623 prop::SatLiteral lit = (*clause)[itcic->second];
624 if( childPol[child_base] && base_pol){
625 os << os_main.str() << " " << ProofManager::getLitName(lit, d_name);
626 }else{
627 os << ProofManager::getLitName(lit, d_name) << " " << os_main.str();
628 }
629 os << ")";
630 }else{
631 success = false;
632 }
633 }
634 }else if ((base_assertion.getKind()==kind::AND && base_pol) ||
635 ((base_assertion.getKind()==kind::OR ||
636 base_assertion.getKind()==kind::IMPLIES) && !base_pol)) {
637
638 std::stringstream os_main;
639
640 Node iatom;
641 if (is_in_clause) {
642 Assert( assertion.getNumChildren()==2 );
643 iatom = assertion[ base_index==0 ? 1 : 0];
644 } else {
645 Assert( assertion.getNumChildren()==1 );
646 iatom = assertion[0];
647 }
648
649 Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl;
650 Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom;
651 bool e_pol = iatom.getKind()!=kind::NOT;
652 std::map< Node, unsigned >::iterator itcic = childIndex.find( e_base );
653 if( itcic!=childIndex.end() ){
654 prop::SatLiteral lit = (*clause)[itcic->second];
655 //eliminate until we find iatom
656 for( unsigned j=0; j<base_assertion.getNumChildren(); j++ ){
657 Node child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j];
658 bool child_pol = base_assertion[j].getKind()!=kind::NOT;
659 if( j==0 && base_assertion.getKind()==kind::IMPLIES ){
660 child_pol = !child_pol;
661 }
662 if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){
663 success = true;
664 bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol );
665 if( elimNn ){
666 os_main << "(not_not_elim _ ";
667 }
668 std::stringstream os_paren;
669 if( j+1<base_assertion.getNumChildren() ){
670 os_main << "(and_elim_1 _ _ ";
671 if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
672 os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
673 os_paren << ")";
674 }
675 os_paren << ")";
676 }
677 for( unsigned k=0; k<j; k++ ){
678 os_main << "(and_elim_2 _ _ ";
679 if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
680 os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
681 os_paren << ")";
682 }
683 os_paren << ")";
684 }
685 os_main << os_base.str() << os_paren.str();
686 if( elimNn ){
687 os_main << ")";
688 }
689 break;
690 }
691 }
692 if( success ){
693 os << "(contra _ ";
694 if( !e_pol ){
695 os << ProofManager::getLitName(lit, d_name) << " " << os_main.str();
696 }else{
697 os << os_main.str() << " " << ProofManager::getLitName(lit, d_name);
698 }
699 os << ")";
700 }
701 }
702 }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){
703 //eliminate negation
704 int num_nots_2 = 0;
705 int num_nots_1 = 0;
706 Kind k;
707 if( !base_pol ){
708 if( base_assertion.getKind()==kind::EQUAL ){
709 num_nots_2 = 1;
710 }
711 k = kind::EQUAL;
712 }else{
713 k = base_assertion.getKind();
714 }
715 std::vector< unsigned > indices;
716 std::vector< bool > pols;
717 success = true;
718 int elimNum = 0;
719 for( unsigned i=0; i<2; i++ ){
720 Node child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i];
721 bool child_pol = base_assertion[i].getKind()!=kind::NOT;
722 std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
723 if( itcic!=childIndex.end() ){
724 indices.push_back( itcic->second );
725 pols.push_back( childPol[child_base] );
726 if( i==0 ){
727 //figure out which way to elim
728 elimNum = child_pol==childPol[child_base] ? 2 : 1;
729 if( (elimNum==2)==(k==kind::EQUAL) ){
730 num_nots_2++;
731 }
732 if( elimNum==1 ){
733 num_nots_1++;
734 }
735 }
736 }else{
737 success = false;
738 break;
739 }
740 }
741 Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl;
742 if( success ){
743 os << "(contra _ ";
744 std::stringstream os_base_n;
745 if( num_nots_2==2 ){
746 os_base_n << "(not_not_elim _ ";
747 }
748 os_base_n << "(or_elim_1 _ _ ";
749 prop::SatLiteral lit1 = (*clause)[indices[0]];
750 if( !pols[0] || num_nots_1==1 ){
751 os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
752 }else{
753 Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
754 os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
755 }
756 Assert( elimNum!=0 );
757 os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
758 if( !base_pol ){
759 os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
760 }else{
761 os_base_n << os_base.str();
762 }
763 os_base_n << "))";
764 if( num_nots_2==2 ){
765 os_base_n << ")";
766 num_nots_2 = 0;
767 }
768 prop::SatLiteral lit2 = (*clause)[indices[1]];
769 if( pols[1]==(num_nots_2==0) ){
770 os << os_base_n.str() << " ";
771 if( num_nots_2==1 ){
772 os << "(not_not_intro _ " << ProofManager::getLitName(lit2, d_name) << ")";
773 }else{
774 os << ProofManager::getLitName(lit2, d_name);
775 }
776 }else{
777 os << ProofManager::getLitName(lit2, d_name) << " " << os_base_n.str();
778 }
779 os << ")";
780 }
781 }else if( base_assertion.getKind()==kind::ITE ){
782 std::map< unsigned, unsigned > appears;
783 std::map< unsigned, Node > appears_expr;
784 unsigned appears_count = 0;
785 for( unsigned r=0; r<3; r++ ){
786 Node child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r];
787 std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
788 if( itcic!=childIndex.end() ){
789 appears[r] = itcic->second;
790 appears_expr[r] = child_base;
791 appears_count++;
792 }
793 }
794 if( appears_count==2 ){
795 success = true;
796 int elimNum = 1;
797 unsigned index1 = 0;
798 unsigned index2 = 1;
799 if( appears.find( 0 )==appears.end() ){
800 elimNum = 3;
801 index1 = 1;
802 index2 = 2;
803 }else if( appears.find( 1 )==appears.end() ){
804 elimNum = 2;
805 index1 = 0;
806 index2 = 2;
807 }
808 std::stringstream os_main;
809 os_main << "(or_elim_1 _ _ ";
810 prop::SatLiteral lit1 = (*clause)[appears[index1]];
811 if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){
812 os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
813 }else{
814 os_main << ProofManager::getLitName(lit1, d_name) << " ";
815 }
816 os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ ";
817 os_main << os_base.str() << "))";
818 os << "(contra _ ";
819 prop::SatLiteral lit2 = (*clause)[appears[index2]];
820 if( !childPol[appears_expr[index2]] || !base_pol ){
821 os << ProofManager::getLitName(lit2, d_name) << " " << os_main.str();
822 }else{
823 os << os_main.str() << " " << ProofManager::getLitName(lit2, d_name);
824 }
825 os << ")";
826 }
827 }else if( base_assertion.isConst() ){
828 bool pol = base_assertion==NodeManager::currentNM()->mkConst( true );
829 if( pol!=base_pol ){
830 success = true;
831 if( pol ){
832 os << "(contra _ truth " << os_base.str() << ")";
833 }else{
834 os << os_base.str();
835 }
836 }
837 }
838
839 if( !success ){
840 Trace("cnf-pf") << std::endl;
841 Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << std::endl;
842 Trace("cnf-pf") << ";!!!!!!!!! Clause is : ";
843 for (unsigned i = 0; i < clause->size(); ++i) {
844 Trace("cnf-pf") << (*clause)[i] << " ";
845 }
846 Trace("cnf-pf") << std::endl;
847 os << "trust-bad";
848 }
849 }
850
851 os << ")" << clause_paren.str()
852 << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
853
854 paren << "))";
855 }
856
printClause(const prop::SatClause & clause,std::ostream & os,std::ostream & paren)857 void LFSCCnfProof::printClause(const prop::SatClause& clause,
858 std::ostream& os,
859 std::ostream& paren) {
860 for (unsigned i = 0; i < clause.size(); ++i) {
861 prop::SatLiteral lit = clause[i];
862 prop::SatVariable var = lit.getSatVariable();
863 if (lit.isNegated()) {
864 os << "(ast _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " ";
865 paren << "))";
866 } else {
867 os << "(asf _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " ";
868 paren << "))";
869 }
870 }
871 }
872
873 // print a proof of the top-level formula e, based on the input assertions
printProofTopLevel(Node e,std::ostream & out)874 bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) {
875 if (!isAssertion(e)) {
876 // check if deduced by CNF
877 // dependence on top level fact i.e. a depends on (a and b)
878 NodeToNode::const_iterator itd = d_cnfDeps.find(e);
879 if (itd != d_cnfDeps.end()) {
880 TNode parent = itd->second;
881 //check if parent is an input assertion
882 std::stringstream out_parent;
883 if (printProofTopLevel(parent, out_parent)) {
884 if(parent.getKind()==kind::AND ||
885 (parent.getKind()==kind::NOT && (parent[0].getKind()==kind::IMPLIES ||
886 parent[0].getKind()==kind::OR))) {
887 Node parent_base = parent.getKind()==kind::NOT ? parent[0] : parent;
888 Node e_base = e.getKind()==kind::NOT ? e[0] : e;
889 bool e_pol = e.getKind()!=kind::NOT;
890 for( unsigned i=0; i<parent_base.getNumChildren(); i++ ){
891 Node child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i];
892 bool child_pol = parent_base[i].getKind()!=kind::NOT;
893 if( parent_base.getKind()==kind::IMPLIES && i==0 ){
894 child_pol = !child_pol;
895 }
896 if (e_base==child_base &&
897 (e_pol==child_pol)==(parent_base.getKind()==kind::AND)) {
898 bool elimNn = ((parent_base.getKind()==kind::OR ||
899 (parent_base.getKind()==kind::IMPLIES && i==1)) && e_pol);
900 if (elimNn) {
901 out << "(not_not_elim _ ";
902 }
903 std::stringstream out_paren;
904 if (i+1 < parent_base.getNumChildren()) {
905 out << "(and_elim_1 _ _ ";
906 if( parent_base.getKind()==kind::OR ||
907 parent_base.getKind()==kind::IMPLIES ){
908 out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" )
909 << "_elim _ _ ";
910 out_paren << ")";
911 }
912 out_paren << ")";
913 }
914 for( unsigned j=0; j<i; j++ ){
915 out << "(and_elim_2 _ _ ";
916 if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
917 out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
918 out_paren << ")";
919 }
920 out_paren << ")";
921 }
922 out << out_parent.str();
923 out << out_paren.str();
924 if( elimNn ){
925 out << ")";
926 }
927 return true;
928 }
929 }
930 } else {
931 Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
932 << " is not correct type (" << parent << ")" << std::endl;
933 }
934 } else {
935 Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
936 << " is not input" << std::endl;
937 }
938 } else {
939 Trace("cnf-pf-debug") << "; isInputAssertion : " << e
940 << " has no parent" << std::endl;
941 }
942 return false;
943 } else {
944 out << ProofManager::getPreprocessedAssertionName(e);
945 return true;
946 }
947 }
948
949 } /* CVC4 namespace */
950