diff options
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 1049 |
1 files changed, 620 insertions, 429 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 263e1fe8c..884a67856 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -26,518 +26,709 @@ using namespace CVC4::prop; namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream) +CnfProof::CnfProof(CnfStream* stream, + context::Context* ctx, + const std::string& name) : d_cnfStream(stream) -{} + , d_clauseToAssertion(ctx) + , d_assertionToProofRule(ctx) + , d_currentAssertionStack() + , d_currentDefinitionStack() + , d_clauseToDefinition(ctx) + , d_definitions() + , d_cnfDeps() + , d_name(name) +{ + // Setting the proof object for the CnfStream + d_cnfStream->setProof(this); +} + +CnfProof::~CnfProof() {} -CnfProof::~CnfProof() { +bool CnfProof::isAssertion(Node node) { + return d_assertionToProofRule.find(node) != + d_assertionToProofRule.end(); } -Expr CnfProof::getAtom(prop::SatVariable var) { - prop::SatLiteral lit (var); - Node node = d_cnfStream->getNode(lit); - Expr atom = node.toExpr(); - return atom; +bool CnfProof::isDefinition(Node node) { + return d_definitions.find(node) != + d_definitions.end(); +} + +ProofRule CnfProof::getProofRule(Node node) { + Assert (isAssertion(node)); + NodeToProofRule::iterator it = d_assertionToProofRule.find(node); + return (*it).second; +} +ProofRule CnfProof::getProofRule(ClauseId clause) { + TNode assertion = getAssertionForClause(clause); + return getProofRule(assertion); } -prop::SatLiteral CnfProof::getLiteral(TNode atom) { - return d_cnfStream->getLiteral(atom); +Node CnfProof::getAssertionForClause(ClauseId clause) { + ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); + Assert (it != d_clauseToAssertion.end()); + return (*it).second; } -Expr CnfProof::getAssertion(uint64_t id) { - return d_cnfStream->getAssertion(id).toExpr(); +Node CnfProof::getDefinitionForClause(ClauseId clause) { + ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause); + Assert (it != d_clauseToDefinition.end()); + return (*it).second; } -void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { - for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) { - d_atomsDeclared.insert(lit.getSatVariable()); - os << "(decl_atom "; - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 || - ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 || - ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) { - Expr atom = getAtom(lit.getSatVariable()); - LFSCTheoryProof::printTerm(atom, os); - } else { - // print fake atoms for all other logics (for now) - os << "true "; - } +void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { + Assert (clause != ClauseIdUndef && + clause != ClauseIdError && + clause != ClauseIdEmpty); + + // Explanations do not need a CNF conversion proof since they are in CNF + // (they will only need a theory proof as they are theory valid) + if (explanation) { + Debug("proof:cnf") << "CnfProof::registerConvertedClause " + << clause << " explanation? " << explanation << std::endl; + Assert (d_explanations.find(clause) == d_explanations.end()); + d_explanations.insert(clause); + return; + } - os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n"; - paren << ")))"; - } + Node current_assertion = getCurrentAssertion(); + Node current_expr = getCurrentDefinition(); + + Debug("proof:cnf") << "CnfProof::registerConvertedClause " + << clause << " assertion = " << current_assertion + << clause << " definition = " << current_expr << std::endl; + + setClauseAssertion(clause, current_assertion); + setClauseDefinition(clause, current_expr); +} + +void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { + Debug("proof:cnf") << "CnfProof::setClauseAssertion " + << clause << " assertion " << expr << std::endl; + // We can add the same clause from different assertions. In this + // case we keep the first assertion. For example asserting a /\ b + // and then b /\ c where b is an atom, would assert b twice (note + // that since b is top level, it is not cached by the CnfStream) + if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) + return; + + d_clauseToAssertion.insert (clause, expr); +} + +void CnfProof::setClauseDefinition(ClauseId clause, Node definition) { + Debug("proof:cnf") << "CnfProof::setClauseDefinition " + << clause << " definition " << definition << std::endl; + // We keep the first definition + if (d_clauseToDefinition.find(clause) != d_clauseToDefinition.end()) + return; + + d_clauseToDefinition.insert(clause, definition); + d_definitions.insert(definition); +} + +void CnfProof::registerAssertion(Node assertion, ProofRule reason) { + Debug("proof:cnf") << "CnfProof::registerAssertion " + << assertion << " reason " << reason << std::endl; + // We can obtain the assertion from different reasons (e.g. if the + // assertion is a lemma over shared terms both theories can generate + // the same lemma) We only need to prove the lemma in one way, so we + // keep the first reason. + if (isAssertion(assertion)) { + return; } + d_assertionToProofRule.insert(assertion, reason); } -void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { - printPreprocess(os, paren); - printInputClauses(os, paren); - printTheoryLemmas(os, paren); +void CnfProof::setCnfDependence(Node from, Node to) { + Debug("proof:cnf") << "CnfProof::setCnfDependence " + << "from " << from << std::endl + << " to " << to << std::endl; + + Assert (from != to); + d_cnfDeps.insert(std::make_pair(from, to)); } -void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) { - os << " ;; Preprocessing \n"; - __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator it = ProofManager::currentPM()->begin_deps(); - __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end = ProofManager::currentPM()->end_deps(); +void CnfProof::pushCurrentAssertion(Node assertion) { + Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " + << assertion << std::endl; - for (; it != end; ++it) { - if( !it->second.empty() ){ - Expr e = it->first.toExpr(); - os << "(th_let_pf _ "; + d_currentAssertionStack.push_back(assertion); +} - //TODO - Trace("cnf-pf-debug") << "; preprocess assertion : " << e << std::endl; - os << "(trust_f "; - LFSCTheoryProof::printTerm(e, os); - os << ") "; +void CnfProof::popCurrentAssertion() { + Assert (d_currentAssertionStack.size()); + + Debug("proof:cnf") << "CnfProof::popCurrentAssertion " + << d_currentAssertionStack.back() << std::endl; + + d_currentAssertionStack.pop_back(); +} - os << "(\\ A" << ProofManager::currentPM()->getAssertionCounter() << std::endl; - ProofManager::currentPM()->setAssertion( e ); - paren << "))"; +Node CnfProof::getCurrentAssertion() { + Assert (d_currentAssertionStack.size()); + return d_currentAssertionStack.back(); +} + +void CnfProof::pushCurrentDefinition(Node definition) { + Debug("proof:cnf") << "CnfProof::pushCurrentDefinition " + << definition << std::endl; + + d_currentDefinitionStack.push_back(definition); +} + +void CnfProof::popCurrentDefinition() { + Assert (d_currentDefinitionStack.size()); + + Debug("proof:cnf") << "CnfProof::popCurrentDefinition " + << d_currentDefinitionStack.back() << std::endl; + + d_currentDefinitionStack.pop_back(); +} + +Node CnfProof::getCurrentDefinition() { + Assert (d_currentDefinitionStack.size()); + return d_currentDefinitionStack.back(); +} + + +Node CnfProof::getAtom(prop::SatVariable var) { + prop::SatLiteral lit (var); + Node node = d_cnfStream->getNode(lit); + return node; +} + + +void CnfProof::collectAtoms(const prop::SatClause* clause, + NodeSet& atoms) { + for (unsigned i = 0; i < clause->size(); ++i) { + SatLiteral lit = clause->operator[](i); + SatVariable var = lit.getSatVariable(); + TNode atom = getAtom(var); + if (atoms.find(atom) == atoms.end()) { + Assert (atoms.find(atom) == atoms.end()); + atoms.insert(atom); + } + } +} + +prop::SatLiteral CnfProof::getLiteral(TNode atom) { + return d_cnfStream->getLiteral(atom); +} + +void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses, + NodeSet& atom_map) { + IdToSatClause::const_iterator it = clauses.begin(); + for (; it != clauses.end(); ++it) { + const prop::SatClause* clause = it->second; + collectAtoms(clause, atom_map); + } + +} + +void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, + NodeSet& assertions) { + IdToSatClause::const_iterator it = clauses.begin(); + for (; it != clauses.end(); ++it) { + TNode used_assertion = getAssertionForClause(it->first); + assertions.insert(used_assertion); + // it can be the case that a definition for a clause is an assertion + // but it is not the assertion for the clause + // e.g. the assertions [(and a b), a] + TNode used_definition = getDefinitionForClause(it->first); + if (isAssertion(used_definition)) { + assertions.insert(used_definition); } } } -Expr LFSCCnfProof::clauseToExpr( const prop::SatClause& clause, - std::map< Expr, unsigned >& childIndex, - std::map< Expr, bool >& childPol ) { +void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren) { + NodeSet::const_iterator it = atoms.begin(); + NodeSet::const_iterator end = atoms.end(); + + for (;it != end; ++it) { + os << "(decl_atom "; + Node atom = *it; + prop::SatVariable var = getLiteral(atom).getSatVariable(); + //FIXME hideous + LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); + pe->printLetTerm(atom.toExpr(), os); + + os << " (\\ " << ProofManager::getVarName(var, d_name) + << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + paren << ")))"; + } +} + +// maps each expr to the position it had in the clause and the polarity it had +Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause, + std::map<Node, unsigned>& childIndex, + std::map<Node, bool>& childPol ) { std::vector< Node > children; for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); - Node atom = Node::fromExpr( getAtom(var) ); + Node atom = getAtom(var); children.push_back( lit.isNegated() ? atom.negate() : atom ); - childIndex[atom.toExpr()] = i; - childPol[atom.toExpr()] = !lit.isNegated(); + childIndex[atom] = i; + childPol[atom] = !lit.isNegated(); } - return children.size()==1 ? children[0].toExpr() : NodeManager::currentNM()->mkNode( kind::OR, children ).toExpr(); + return children.size()==1 ? children[0] : + NodeManager::currentNM()->mkNode(kind::OR, children ); } -void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { - os << " ;; Clauses\n"; - ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); - ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); - - - for (; it != end; ++it) { - ClauseId id = it->first; - const prop::SatClause* clause = it->second; - printAtomMapping(clause, os, paren); - os << "(satlem _ _ "; - std::ostringstream clause_paren; - printClause(*clause, os, clause_paren); - os << "(clausify_false "; - - Assert( clause->size()>0 ); - - Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id ); - ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id ); - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << "; formula for clause id " << id << " : " << base_assertion << std::endl; - - //get the assertion for the clause id - std::map< Expr, unsigned > childIndex; - std::map< Expr, bool > childPol; - Expr assertion = clauseToExpr( *clause, childIndex, childPol ); - //if there is no reason, construct assertion directly. This can happen for unit clauses. - if( base_assertion.isNull() ){ - base_assertion = assertion; - } - //os_base is proof of base_assertion - std::stringstream os_base; - bool is_input = ProofManager::currentPM()->isInputAssertion( base_assertion, os_base ); - - //get base assertion with polarity - bool base_pol = base_assertion.getKind()!=kind::NOT; - base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; - - std::map< Expr, unsigned >::iterator itci = childIndex.find( base_assertion ); - bool is_in_clause = itci!=childIndex.end(); - unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; - if( !is_input ){ - Assert( is_in_clause ); - prop::SatLiteral blit = (*clause)[ base_index ]; - os_base << ProofManager::getLitName(blit); - base_pol = !childPol[base_assertion]; +void LFSCCnfProof::printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren) { + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(*clause, os, clause_paren); + os << "(clausify_false "; + + // FIXMEEEEEEEEEEEE + // os <<"trust)"; + // os << clause_paren.str() + // << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + // paren << "))"; + + // return; + + Assert( clause->size()>0 ); + + Node base_assertion = getDefinitionForClause(id); + + //get the assertion for the clause id + std::map<Node, unsigned > childIndex; + std::map<Node, bool > childPol; + Node assertion = clauseToNode( *clause, childIndex, childPol ); + //if there is no reason, construct assertion directly. This can happen for unit clauses. + if( base_assertion.isNull() ){ + base_assertion = assertion; + } + //os_base is proof of base_assertion + std::stringstream os_base; + + // checks if tautological definitional clause or top-level clause + // and prints the proof of the top-level formula + bool is_input = printProofTopLevel(base_assertion, os_base); + + //get base assertion with polarity + bool base_pol = base_assertion.getKind()!=kind::NOT; + base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; + + std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion ); + bool is_in_clause = itci!=childIndex.end(); + unsigned base_index = is_in_clause ? itci->second : 0; + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; + if (!is_input){ + Assert(is_in_clause); + prop::SatLiteral blit = (*clause)[ base_index ]; + os_base << ProofManager::getLitName(blit, d_name); + base_pol = !childPol[base_assertion]; // WHY? if the case is => + } + Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; + Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; + + bool success = false; + if( is_input && + is_in_clause && + childPol[base_assertion]==base_pol ){ + //if both in input and in clause, the proof is trivial. this is the case for unit clauses. + Trace("cnf-pf") << "; trivial" << std::endl; + os << "(contra _ "; + success = true; + prop::SatLiteral lit = (*clause)[itci->second]; + if( base_pol ){ + os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); + }else{ + os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); } - Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; - Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; - - bool success = false; - if( is_input && is_in_clause && childPol[base_assertion]==base_pol ){ - //if both in input and in clause, the proof is trivial. this is the case for unit clauses. - Trace("cnf-pf") << "; trivial" << std::endl; - os << "(contra _ "; - success = true; - prop::SatLiteral lit = (*clause)[itci->second]; - if( base_pol ){ - os << os_base.str() << " " << ProofManager::getLitName(lit); - }else{ - os << ProofManager::getLitName(lit) << " " << os_base.str(); + os << ")"; + } else if ((base_assertion.getKind()==kind::AND && !base_pol) || + ((base_assertion.getKind()==kind::OR || + base_assertion.getKind()==kind::IMPLIES) && base_pol)) { + Trace("cnf-pf") << "; and/or case 1" << std::endl; + success = true; + std::stringstream os_main; + std::stringstream os_paren; + //eliminate each one + for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) { + Node child_base = base_assertion[j].getKind()==kind::NOT ? + base_assertion[j][0] : base_assertion[j]; + bool child_pol = base_assertion[j].getKind()!=kind::NOT; + + if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ + child_pol = !child_pol; } - os << ")"; - }else if( ( base_assertion.getKind()==kind::AND && !base_pol ) || ( ( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ) && base_pol ) ){ - Trace("cnf-pf") << "; and/or case 1" << std::endl; - success = true; - std::stringstream os_main; - std::stringstream os_paren; - //eliminate each one - for( int j=base_assertion.getNumChildren()-2; j>=0; j-- ){ - Expr child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; - bool child_pol = base_assertion[j].getKind()!=kind::NOT; - if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ - child_pol = !child_pol; + + Trace("cnf-pf-debug") << "; child " << j << " " + << child_base << " " + << child_pol << " " + << childPol[child_base] << std::endl; + + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + + if( itcic!=childIndex.end() ){ + //Assert( child_pol==childPol[child_base] ); + os_main << "(or_elim_1 _ _ "; + prop::SatLiteral lit = (*clause)[itcic->second]; + // Should be if in the original formula it was negated + if( childPol[child_base] && base_pol ){ + os_main << ProofManager::getLitName(lit, d_name) << " "; + }else{ + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; } - Trace("cnf-pf-debug") << "; child " << j << " " << child_base << " " << child_pol << " " << childPol[child_base] << std::endl; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - //Assert( child_pol==childPol[child_base] ); - os_main << "(or_elim_1 _ _ "; - prop::SatLiteral lit = (*clause)[itcic->second]; - if( childPol[child_base] && base_pol ){ - os_main << ProofManager::getLitName(lit) << " "; - }else{ - os_main << "(not_not_intro _ " << ProofManager::getLitName(lit) << ") "; - } - if( base_assertion.getKind()==kind::AND ){ - os_main << "(not_and_elim _ _ "; - os_paren << ")"; - } + if( base_assertion.getKind()==kind::AND ){ + os_main << "(not_and_elim _ _ "; os_paren << ")"; - }else{ - success = false; } + os_paren << ")"; + }else{ + success = false; } - if( success ){ - if( base_assertion.getKind()==kind::IMPLIES ){ - os_main << "(impl_elim _ _ "; - } - os_main << os_base.str(); - if( base_assertion.getKind()==kind::IMPLIES ){ - os_main << ")"; - } - os_main << os_paren.str(); - int last_index = base_assertion.getNumChildren()-1; - Expr child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index]; - //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - os << "(contra _ "; - prop::SatLiteral lit = (*clause)[itcic->second]; - if( childPol[child_base] && base_pol ){ - os << os_main.str() << " " << ProofManager::getLitName(lit); - }else{ - os << ProofManager::getLitName(lit) << " " << os_main.str(); - } - os << ")"; - }else{ - success = false; - } + } + if( success ){ + if( base_assertion.getKind()==kind::IMPLIES ){ + os_main << "(impl_elim _ _ "; } - }else if( ( base_assertion.getKind()==kind::AND && base_pol ) || ( ( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ) && !base_pol ) ){ - std::stringstream os_main; - Expr iatom; - if( is_in_clause ){ - Assert( assertion.getNumChildren()==2 ); - iatom = assertion[ base_index==0 ? 1 : 0]; - }else{ - Assert( assertion.getNumChildren()==1 ); - iatom = assertion[0]; + os_main << os_base.str(); + if( base_assertion.getKind()==kind::IMPLIES ){ + os_main << ")"; } - Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl; - Expr e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom; - bool e_pol = iatom.getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( e_base ); + os_main << os_paren.str(); + int last_index = base_assertion.getNumChildren()-1; + Node child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index]; + //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); if( itcic!=childIndex.end() ){ + os << "(contra _ "; prop::SatLiteral lit = (*clause)[itcic->second]; - //eliminate until we find iatom - for( unsigned j=0; j<base_assertion.getNumChildren(); j++ ){ - Expr child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; - bool child_pol = base_assertion[j].getKind()!=kind::NOT; - if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ - child_pol = !child_pol; + if( childPol[child_base] && base_pol){ + os << os_main.str() << " " << ProofManager::getLitName(lit, d_name); + }else{ + os << ProofManager::getLitName(lit, d_name) << " " << os_main.str(); + } + os << ")"; + }else{ + success = false; + } + } + }else if ((base_assertion.getKind()==kind::AND && base_pol) || + ((base_assertion.getKind()==kind::OR || + base_assertion.getKind()==kind::IMPLIES) && !base_pol)) { + + std::stringstream os_main; + + Node iatom; + if (is_in_clause) { + Assert( assertion.getNumChildren()==2 ); + iatom = assertion[ base_index==0 ? 1 : 0]; + } else { + Assert( assertion.getNumChildren()==1 ); + iatom = assertion[0]; + } + + Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl; + Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom; + bool e_pol = iatom.getKind()!=kind::NOT; + std::map< Node, unsigned >::iterator itcic = childIndex.find( e_base ); + if( itcic!=childIndex.end() ){ + prop::SatLiteral lit = (*clause)[itcic->second]; + //eliminate until we find iatom + for( unsigned j=0; j<base_assertion.getNumChildren(); j++ ){ + Node child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; + bool child_pol = base_assertion[j].getKind()!=kind::NOT; + if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ + child_pol = !child_pol; + } + if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){ + success = true; + bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol ); + if( elimNn ){ + os_main << "(not_not_elim _ "; } - if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){ - success = true; - bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol ); - if( elimNn ){ - os_main << "(not_not_elim _ "; - } - std::stringstream os_paren; - if( j+1<base_assertion.getNumChildren() ){ - os_main << "(and_elim_1 _ _ "; - if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){ - os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ "; - os_paren << ")"; - } + std::stringstream os_paren; + if( j+1<base_assertion.getNumChildren() ){ + os_main << "(and_elim_1 _ _ "; + if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){ + os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ "; os_paren << ")"; } - for( unsigned k=0; k<j; k++ ){ - os_main << "(and_elim_2 _ _ "; - if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){ - os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ "; - os_paren << ")"; - } + os_paren << ")"; + } + for( unsigned k=0; k<j; k++ ){ + os_main << "(and_elim_2 _ _ "; + if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){ + os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ "; os_paren << ")"; } - os_main << os_base.str() << os_paren.str(); - if( elimNn ){ - os_main << ")"; - } - break; + os_paren << ")"; } - } - if( success ){ - os << "(contra _ "; - if( !e_pol ){ - os << ProofManager::getLitName(lit) << " " << os_main.str(); - }else{ - os << os_main.str() << " " << ProofManager::getLitName(lit); + os_main << os_base.str() << os_paren.str(); + if( elimNn ){ + os_main << ")"; } - os << ")"; - } - } - }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){ - //eliminate negation - int num_nots_2 = 0; - int num_nots_1 = 0; - Kind k; - if( !base_pol ){ - if( base_assertion.getKind()==kind::IFF ){ - num_nots_2 = 1; - } - k = kind::IFF; - }else{ - k = base_assertion.getKind(); - } - std::vector< unsigned > indices; - std::vector< bool > pols; - success = true; - int elimNum = 0; - for( unsigned i=0; i<2; i++ ){ - Expr child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i]; - bool child_pol = base_assertion[i].getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - indices.push_back( itcic->second ); - pols.push_back( childPol[child_base] ); - if( i==0 ){ - //figure out which way to elim - elimNum = child_pol==childPol[child_base] ? 2 : 1; - if( (elimNum==2)==(k==kind::IFF) ){ - num_nots_2++; - } - if( elimNum==1 ){ - num_nots_1++; - } - } - }else{ - success = false; break; } } - Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl; if( success ){ os << "(contra _ "; - std::stringstream os_base_n; - if( num_nots_2==2 ){ - os_base_n << "(not_not_elim _ "; - } - os_base_n << "(or_elim_1 _ _ "; - prop::SatLiteral lit1 = (*clause)[indices[0]]; - if( !pols[0] || num_nots_1==1 ){ - os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1) << ") "; - }else{ - os_base_n << ProofManager::getLitName(lit1) << " "; - } - Assert( elimNum!=0 ); - os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; - if( !base_pol ){ - os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; - }else{ - os_base_n << os_base.str(); - } - os_base_n << "))"; - if( num_nots_2==2 ){ - os_base_n << ")"; - num_nots_2 = 0; - } - prop::SatLiteral lit2 = (*clause)[indices[1]]; - if( pols[1]==(num_nots_2==0) ){ - os << os_base_n.str() << " "; - if( num_nots_2==1 ){ - os << "(not_not_intro _ " << ProofManager::getLitName(lit2) << ")"; - }else{ - os << ProofManager::getLitName(lit2); - } + if( !e_pol ){ + os << ProofManager::getLitName(lit, d_name) << " " << os_main.str(); }else{ - os << ProofManager::getLitName(lit2) << " " << os_base_n.str(); + os << os_main.str() << " " << ProofManager::getLitName(lit, d_name); } os << ")"; } - }else if( base_assertion.getKind()==kind::ITE ){ - std::map< unsigned, unsigned > appears; - std::map< unsigned, Expr > appears_expr; - unsigned appears_count = 0; - for( unsigned r=0; r<3; r++ ){ - Expr child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r]; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - appears[r] = itcic->second; - appears_expr[r] = child_base; - appears_count++; - } + } + }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){ + //eliminate negation + int num_nots_2 = 0; + int num_nots_1 = 0; + Kind k; + if( !base_pol ){ + if( base_assertion.getKind()==kind::IFF ){ + num_nots_2 = 1; } - if( appears_count==2 ){ - success = true; - int elimNum = 1; - unsigned index1 = 0; - unsigned index2 = 1; - if( appears.find( 0 )==appears.end() ){ - elimNum = 3; - index1 = 1; - index2 = 2; - }else if( appears.find( 1 )==appears.end() ){ - elimNum = 2; - index1 = 0; - index2 = 2; - } - std::stringstream os_main; - os_main << "(or_elim_1 _ _ "; - prop::SatLiteral lit1 = (*clause)[appears[index1]]; - if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){ - os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1) << ") "; - }else{ - os_main << ProofManager::getLitName(lit1) << " "; - } - os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ "; - os_main << os_base.str() << "))"; - os << "(contra _ "; - prop::SatLiteral lit2 = (*clause)[appears[index2]]; - if( !childPol[appears_expr[index2]] || !base_pol ){ - os << ProofManager::getLitName(lit2) << " " << os_main.str(); - }else{ - os << os_main.str() << " " << ProofManager::getLitName(lit2); + k = kind::IFF; + }else{ + k = base_assertion.getKind(); + } + std::vector< unsigned > indices; + std::vector< bool > pols; + success = true; + int elimNum = 0; + for( unsigned i=0; i<2; i++ ){ + Node child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i]; + bool child_pol = base_assertion[i].getKind()!=kind::NOT; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + if( itcic!=childIndex.end() ){ + indices.push_back( itcic->second ); + pols.push_back( childPol[child_base] ); + if( i==0 ){ + //figure out which way to elim + elimNum = child_pol==childPol[child_base] ? 2 : 1; + if( (elimNum==2)==(k==kind::IFF) ){ + num_nots_2++; + } + if( elimNum==1 ){ + num_nots_1++; + } } - os << ")"; + }else{ + success = false; + break; + } + } + Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl; + if( success ){ + os << "(contra _ "; + std::stringstream os_base_n; + if( num_nots_2==2 ){ + os_base_n << "(not_not_elim _ "; + } + os_base_n << "(or_elim_1 _ _ "; + prop::SatLiteral lit1 = (*clause)[indices[0]]; + if( !pols[0] || num_nots_1==1 ){ + os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; + }else{ + os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } - }else if( base_assertion.isConst() ){ - bool pol = base_assertion==NodeManager::currentNM()->mkConst( true ).toExpr(); - if( pol!=base_pol ){ - success = true; - if( pol ){ - os << "(contra _ truth " << os_base.str() << ")"; + Assert( elimNum!=0 ); + os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; + if( !base_pol ){ + os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; + }else{ + os_base_n << os_base.str(); + } + os_base_n << "))"; + if( num_nots_2==2 ){ + os_base_n << ")"; + num_nots_2 = 0; + } + prop::SatLiteral lit2 = (*clause)[indices[1]]; + if( pols[1]==(num_nots_2==0) ){ + os << os_base_n.str() << " "; + if( num_nots_2==1 ){ + os << "(not_not_intro _ " << ProofManager::getLitName(lit2, d_name) << ")"; }else{ - os << os_base.str(); + os << ProofManager::getLitName(lit2, d_name); } + }else{ + os << ProofManager::getLitName(lit2, d_name) << " " << os_base_n.str(); } + os << ")"; } - - if( !success ){ - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << ", proof rule = " << pr << std::endl; - Trace("cnf-pf") << ";!!!!!!!!! Clause is : "; - for (unsigned i = 0; i < clause->size(); ++i) { - Trace("cnf-pf") << (*clause)[i] << " "; + }else if( base_assertion.getKind()==kind::ITE ){ + std::map< unsigned, unsigned > appears; + std::map< unsigned, Node > appears_expr; + unsigned appears_count = 0; + for( unsigned r=0; r<3; r++ ){ + Node child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r]; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + if( itcic!=childIndex.end() ){ + appears[r] = itcic->second; + appears_expr[r] = child_base; + appears_count++; } - Trace("cnf-pf") << std::endl; - os << "trust-bad"; - } - - os << ")" << clause_paren.str() - << " (\\ " << ProofManager::getInputClauseName(id) << "\n"; - paren << "))"; - } -} - -void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas\n"; - ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas(); - ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas(); - - for(size_t n = 0; it != end; ++it, ++n) { - if(n % 100 == 0) { - Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl; } - - ClauseId id = it->first; - const prop::SatClause* clause = it->second; - NodeBuilder<> c(kind::AND); - for(unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = (*clause)[i]; - prop::SatVariable var = lit.getSatVariable(); - if(lit.isNegated()) { - c << Node::fromExpr(getAtom(var)); - } else { - c << Node::fromExpr(getAtom(var)).notNode(); + if( appears_count==2 ){ + success = true; + int elimNum = 1; + unsigned index1 = 0; + unsigned index2 = 1; + if( appears.find( 0 )==appears.end() ){ + elimNum = 3; + index1 = 1; + index2 = 2; + }else if( appears.find( 1 )==appears.end() ){ + elimNum = 2; + index1 = 0; + index2 = 2; } - } - Node cl = c; - if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { - uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; - TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); - if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { - Debug("cores") << "; extensional lemma!" << std::endl; - Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT); - TNode myk = cl[0][0][1]; - Debug("cores") << "; so my skolemized k is " << myk << std::endl; - os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n"; - paren << ")))"; + std::stringstream os_main; + os_main << "(or_elim_1 _ _ "; + prop::SatLiteral lit1 = (*clause)[appears[index1]]; + if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){ + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; + }else{ + os_main << ProofManager::getLitName(lit1, d_name) << " "; + } + os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ "; + os_main << os_base.str() << "))"; + os << "(contra _ "; + prop::SatLiteral lit2 = (*clause)[appears[index2]]; + if( !childPol[appears_expr[index2]] || !base_pol ){ + os << ProofManager::getLitName(lit2, d_name) << " " << os_main.str(); + }else{ + os << os_main.str() << " " << ProofManager::getLitName(lit2, d_name); } + os << ")"; } - printAtomMapping(clause, os, paren); - os << "(satlem _ _ "; - std::ostringstream clause_paren; - printClause(*clause, os, clause_paren); - - Debug("cores") << "\n;id is " << id << std::endl; - if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { - uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; - Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl; - Assert(int32_t(proof_id & 0xffffffff) != -1); - TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); - Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl; - Debug("cores") << "; that means the lemma was " << orig << std::endl; - if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { - Debug("cores") << "; extensional" << std::endl; - os << "(clausify_false trust)\n"; - } else if(proof_id == 0) { - // theory propagation caused conflict - //ProofManager::currentPM()->printProof(os, cl); - os << "(clausify_false trust)\n"; - } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) { - os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; - //ProofManager::currentPM()->printProof(os, cl); - os << "(clausify_false trust)\n"; - } else { - os << "\n;; need to generate a (lemma) proof of " << cl; - os << "\n;; DON'T KNOW HOW !!\n"; - os << "(clausify_false trust)\n"; + }else if( base_assertion.isConst() ){ + bool pol = base_assertion==NodeManager::currentNM()->mkConst( true ); + if( pol!=base_pol ){ + success = true; + if( pol ){ + os << "(contra _ truth " << os_base.str() << ")"; + }else{ + os << os_base.str(); } - } else { - os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; - ProofManager::currentPM()->printProof(os, cl); } - os << clause_paren.str() - << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n"; - paren << "))"; } + + if( !success ){ + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << std::endl; + Trace("cnf-pf") << ";!!!!!!!!! Clause is : "; + for (unsigned i = 0; i < clause->size(); ++i) { + Trace("cnf-pf") << (*clause)[i] << " "; + } + Trace("cnf-pf") << std::endl; + os << "trust-bad"; + } + + os << ")" << clause_paren.str() + << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + paren << "))"; } -void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) { +void LFSCCnfProof::printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren) { for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { - os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; + os << "(ast _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " "; paren << "))"; } else { - os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; + os << "(asf _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " "; paren << "))"; } } } +// print a proof of the top-level formula e, based on the input assertions +bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) { + if (!isAssertion(e)) { + // check if deduced by CNF + // dependence on top level fact i.e. a depends on (a and b) + NodeToNode::const_iterator itd = d_cnfDeps.find(e); + if (itd != d_cnfDeps.end()) { + TNode parent = itd->second; + //check if parent is an input assertion + std::stringstream out_parent; + if (printProofTopLevel(parent, out_parent)) { + if(parent.getKind()==kind::AND || + (parent.getKind()==kind::NOT && (parent[0].getKind()==kind::IMPLIES || + parent[0].getKind()==kind::OR))) { + Node parent_base = parent.getKind()==kind::NOT ? parent[0] : parent; + Node e_base = e.getKind()==kind::NOT ? e[0] : e; + bool e_pol = e.getKind()!=kind::NOT; + for( unsigned i=0; i<parent_base.getNumChildren(); i++ ){ + Node child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i]; + bool child_pol = parent_base[i].getKind()!=kind::NOT; + if( parent_base.getKind()==kind::IMPLIES && i==0 ){ + child_pol = !child_pol; + } + if (e_base==child_base && + (e_pol==child_pol)==(parent_base.getKind()==kind::AND)) { + bool elimNn = ((parent_base.getKind()==kind::OR || + (parent_base.getKind()==kind::IMPLIES && i==1)) && e_pol); + if (elimNn) { + out << "(not_not_elim _ "; + } + std::stringstream out_paren; + if (i+1 < parent_base.getNumChildren()) { + out << "(and_elim_1 _ _ "; + if( parent_base.getKind()==kind::OR || + parent_base.getKind()==kind::IMPLIES ){ + out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) + << "_elim _ _ "; + out_paren << ")"; + } + out_paren << ")"; + } + for( unsigned j=0; j<i; j++ ){ + out << "(and_elim_2 _ _ "; + if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){ + out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ "; + out_paren << ")"; + } + out_paren << ")"; + } + out << out_parent.str(); + out << out_paren.str(); + if( elimNn ){ + out << ")"; + } + return true; + } + } + } else { + Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e + << " is not correct type (" << parent << ")" << std::endl; + } + } else { + Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e + << " is not input" << std::endl; + } + } else { + Trace("cnf-pf-debug") << "; isInputAssertion : " << e + << " has no parent" << std::endl; + } + return false; + } else { + out << ProofManager::getPreprocessedAssertionName(e); + return true; + } +} + + + } /* CVC4 namespace */ |