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/proof_manager.cpp | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 121 |
1 files changed, 117 insertions, 4 deletions
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) |