diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /src/proof | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/cnf_proof.cpp | 361 | ||||
-rw-r--r-- | src/proof/cnf_proof.h | 7 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 121 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 31 | ||||
-rw-r--r-- | src/proof/sat_proof.cpp | 2 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 5 |
6 files changed, 517 insertions, 10 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 22a40ff69..9634cb47b 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -2,7 +2,7 @@ /*! \file cnf_proof.cpp ** \verbatim ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters + ** Major contributors: Morgan Deters, Andrew Reynolds ** Minor contributors (to current version): none ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa @@ -71,15 +71,54 @@ void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& } void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { + printPreprocess(os, paren); printInputClauses(os, paren); printTheoryLemmas(os, paren); } +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(); + + for (; it != end; ++it) { + if( !it->second.empty() ){ + Expr e = it->first.toExpr(); + os << "(th_let_pf _ "; + + //TODO + os << "(trust_f "; + LFSCTheoryProof::printTerm(e, os); + os << ") "; + + os << "(\\ A" << ProofManager::currentPM()->getAssertionCounter() << std::endl; + ProofManager::currentPM()->setAssertion( e ); + paren << "))"; + } + } +} + +Expr LFSCCnfProof::clauseToExpr( const prop::SatClause& clause, + std::map< Expr, unsigned >& childIndex, + std::map< Expr, 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) ); + children.push_back( lit.isNegated() ? atom.negate() : atom ); + childIndex[atom.toExpr()] = i; + childPol[atom.toExpr()] = !lit.isNegated(); + } + return children.size()==1 ? children[0].toExpr() : NodeManager::currentNM()->mkNode( kind::OR, children ).toExpr(); +} + 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; @@ -87,7 +126,325 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); - os << "(clausify_false trust)" << clause_paren.str() + os << "(clausify_false "; + + Assert( clause->size()>0 ); + + Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id ); + ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id ); + + //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") << 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); + base_pol = !childPol[base_assertion]; + } + 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-- ){ + 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< 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] ){ + 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 << ")"; + } + 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] ){ + os << os_main.str() << " " << ProofManager::getLitName(lit); + }else{ + os << ProofManager::getLitName(lit) << " " << 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; + 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]; + } + 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 ); + if( itcic!=childIndex.end() ){ + 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( 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 << ")"; + } + 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 << ")"; + } + os_main << os_base.str() << os_paren.str(); + if( elimNn ){ + os_main << ")"; + } + break; + } + } + if( success ){ + os << "(contra _ "; + if( !e_pol ){ + os << ProofManager::getLitName(lit) << " " << os_main.str(); + }else{ + os << os_main.str() << " " << ProofManager::getLitName(lit); + } + 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); + } + }else{ + os << ProofManager::getLitName(lit2) << " " << os_base_n.str(); + } + 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++; + } + } + 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); + } + os << ")"; + } + }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() << ")"; + }else{ + os << os_base.str(); + } + } + } + + 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] << " "; + } + Trace("cnf-pf") << std::endl; + os << "trust-bad"; + } + + os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id) << "\n"; paren << "))"; } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 459815e60..c1d245716 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -2,7 +2,7 @@ /*! \file cnf_proof.h ** \verbatim ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters + ** Major contributors: Morgan Deters, Andrew Reynolds ** Minor contributors (to current version): none ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa @@ -50,11 +50,16 @@ public: };/* class CnfProof */ class LFSCCnfProof : public CnfProof { + void printPreprocess(std::ostream& os, std::ostream& paren); void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren); + Expr clauseToExpr( const prop::SatClause& clause, + std::map< Expr, unsigned >& childIndex, + std::map< Expr, bool >& childPol ); + public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 87eded8e6..4bff66b92 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -47,7 +47,8 @@ ProofManager::ProofManager(ProofFormat format): d_theoryProof(NULL), d_fullProof(NULL), d_format(format), - d_deps() + d_deps(), + d_assertion_counter(1) { } @@ -155,7 +156,9 @@ void ProofManager::traceDeps(TNode n) { std::vector<Node> deps = (*d_deps.find(n)).second; for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) { Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; - traceDeps(*i); + if( !(*i).isNull() ){ + traceDeps(*i); + } } } } @@ -203,7 +206,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { void ProofManager::addDependence(TNode n, TNode dep) { if(dep != n) { Debug("cores") << "dep: " << n << " : " << dep << std::endl; - if(d_deps.find(dep) == d_deps.end()) { + if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) { Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl; } //Assert(d_deps.find(dep) != d_deps.end()); @@ -219,6 +222,116 @@ void ProofManager::printProof(std::ostream& os, TNode n) { // no proofs here yet } +void ProofManager::setCnfDep( Expr child, Expr parent ) { + Debug("cores") << "CNF dep : " << child << " : " << parent << std::endl; + d_cnf_dep[child] = parent; +} + +Expr ProofManager::getFormulaForClauseId( ClauseId id ) { + std::map< ClauseId, Expr >::const_iterator it = d_clause_id_to_assertion.find( id ); + if( it!=d_clause_id_to_assertion.end() ){ + return it->second; + }else{ + Node ret; + return ret.toExpr(); + } +} + +ProofRule ProofManager::getProofRuleForClauseId( ClauseId id ) { + std::map< ClauseId, ProofRule >::const_iterator it = d_clause_id_to_rule.find( id ); + if( it!=d_clause_id_to_rule.end() ){ + return it->second; + }else{ + return RULE_INVALID; + } +} + +void ProofManager::setAssertion( Expr e ) { + d_assertion_to_id[e] = d_assertion_counter; + d_assertion_counter++; +} + +// if this function returns true, writes to out a proof of e based on input assertions +bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) { + std::map< Expr, unsigned >::iterator itp = d_assertion_to_id.find( e ); + if( itp==d_assertion_to_id.end() ){ + //check if deduced by CNF + std::map< Expr, Expr >::iterator itd = d_cnf_dep.find( e ); + if( itd!=d_cnf_dep.end() ){ + Expr parent = itd->second; + //check if parent is an input assertion + std::stringstream out_parent; + if( isInputAssertion( parent, out_parent ) ){ + if( parent.getKind()==kind::AND || ( parent.getKind()==kind::NOT && ( parent[0].getKind()==kind::IMPLIES || parent[0].getKind()==kind::OR ) ) ){ + Expr parent_base = parent.getKind()==kind::NOT ? parent[0] : parent; + Expr 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++ ){ + Expr 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 << "A" << itp->second; + return true; + } +} + +void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) { + d_registering_assertion = n; + d_registering_rule = proof_id; +} + +void ProofManager::setRegisteredClauseId( ClauseId id ) { + Trace("cnf-pf-debug") << "set register clause id " << id << " " << d_registering_assertion << std::endl; + if( !d_registering_assertion.isNull() ){ + d_clause_id_to_assertion[id] = d_registering_assertion.toExpr(); + d_clause_id_to_rule[id] = d_registering_rule; + setRegisteringFormula( Node::null(), RULE_INVALID ); + } +} + LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) , d_cnfProof(cnf) diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index d60a3f6e3..43d6723fa 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -85,12 +85,14 @@ enum ProofRule { RULE_TRUST, /* trust without evidence (escape hatch until proofs are fully supported) */ RULE_INVALID, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */ RULE_CONFLICT, /* re-construct as a conflict */ + RULE_TSEITIN, /* Tseitin CNF transformation */ RULE_ARRAYS_EXT, /* arrays, extensional */ RULE_ARRAYS_ROW, /* arrays, read-over-write */ };/* enum ProofRules */ class ProofManager { + SatProof* d_satProof; CnfProof* d_cnfProof; TheoryProof* d_theoryProof; @@ -114,6 +116,14 @@ class ProofManager { // trace dependences back to unsat core void traceDeps(TNode n); + Node d_registering_assertion; + ProofRule d_registering_rule; + std::map< ClauseId, Expr > d_clause_id_to_assertion; + std::map< ClauseId, ProofRule > d_clause_id_to_rule; + std::map< Expr, Expr > d_cnf_dep; + //LFSC number for assertions + unsigned d_assertion_counter; + std::map< Expr, unsigned > d_assertion_to_id; protected: LogicInfo d_logic; @@ -139,6 +149,10 @@ public: typedef ExprSet::const_iterator assertions_iterator; typedef VarSet::const_iterator var_iterator; + + __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator begin_deps() const { return d_deps.begin(); } + __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end_deps() const { return d_deps.end(); } + clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } clause_iterator end_input_clauses() const { return d_inputClauses.end(); } size_t num_input_clauses() const { return d_inputClauses.size(); } @@ -179,6 +193,21 @@ public: void setLogic(const LogicInfo& logic); const std::string getLogic() const { return d_logic.getLogicString(); } + + void setCnfDep( Expr child, Expr parent ); + Expr getFormulaForClauseId( ClauseId id ); + ProofRule getProofRuleForClauseId( ClauseId id ); + unsigned getAssertionCounter() { return d_assertion_counter; } + void setAssertion( Expr e ); + bool isInputAssertion( Expr e, std::ostream& out ); + +public: // AJR : FIXME this is hacky + //currently, to map between ClauseId and Expr, requires: + // (1) CnfStream::assertClause(...) to call setRegisteringFormula, + // (2) SatProof::registerClause(...)/registerUnitClause(...) to call setRegisteredClauseId. + //this is under the assumption that the first call at (2) is invoked for the clause corresponding to the Expr at (1). + void setRegisteringFormula( Node n, ProofRule proof_id ); + void setRegisteredClauseId( ClauseId id ); };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index f7b9c4889..2c86d45a4 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -377,6 +377,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6 } } Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n"; + ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); return d_clauseId[clause]; } @@ -397,6 +398,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6 } } Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n"; + ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); return d_unitId[toInt(lit)]; } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 52989d722..6982509b1 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -188,7 +188,6 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { } void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { - unsigned counter = 0; ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); @@ -200,10 +199,12 @@ void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { it = ProofManager::currentPM()->begin_assertions(); for (; it != end; ++it) { - os << "(% A" << counter++ << " (th_holds "; + os << "(% A" << ProofManager::currentPM()->getAssertionCounter() << " (th_holds "; printTerm(*it, os); os << ")\n"; paren << ")"; + //store map between assertion and counter + ProofManager::currentPM()->setAssertion( *it ); } } |