From 10df4ba0752eb23c76b9aa847e3ad116673a47b6 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 10 Mar 2015 15:15:26 +0100 Subject: [PATCH] CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions. --- proofs/signatures/smt.plf | 95 +++--- proofs/signatures/th_base.plf | 1 + src/proof/cnf_proof.cpp | 361 ++++++++++++++++++++- src/proof/cnf_proof.h | 7 +- src/proof/proof_manager.cpp | 121 ++++++- src/proof/proof_manager.h | 31 +- src/proof/sat_proof.cpp | 2 + src/proof/theory_proof.cpp | 5 +- src/prop/cnf_stream.cpp | 143 ++++---- src/prop/cnf_stream.h | 24 +- src/smt/smt_engine.cpp | 44 +-- test/regress/regress0/uf/Makefile.am | 5 +- test/regress/regress0/uf/cnf-iff-base.smt2 | 16 + test/regress/regress0/uf/cnf-iff.smt2 | 38 +++ test/regress/regress0/uf/cnf-ite.smt2 | 35 ++ 15 files changed, 771 insertions(+), 157 deletions(-) create mode 100644 test/regress/regress0/uf/cnf-iff-base.smt2 create mode 100644 test/regress/regress0/uf/cnf-iff.smt2 create mode 100644 test/regress/regress0/uf/cnf-ite.smt2 diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 942e17df0..62cdf3f94 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -135,6 +135,12 @@ (! u2 (th_holds (or f1 f2)) (th_holds f1)))))) +(declare not_or_elim + (! f1 formula + (! f2 formula + (! u2 (th_holds (not (or f1 f2))) + (th_holds (and (not f1) (not f2))))))) + ;; and elimination (declare and_elim_1 @@ -149,20 +155,12 @@ (! u (th_holds (and f1 f2)) (th_holds f2))))) -;; not impl elimination - -(declare not_impl_elim_1 - (! f1 formula - (! f2 formula - (! u (th_holds (not (impl f1 f2))) - (th_holds f1))))) - -(declare not_impl_elim_2 +(declare not_and_elim (! f1 formula (! f2 formula - (! u (th_holds (not (impl f1 f2))) - (th_holds (not f2)))))) - + (! u2 (th_holds (not (and f1 f2))) + (th_holds (or (not f1) (not f2))))))) + ;; impl elimination (declare impl_intro (! f1 formula @@ -174,37 +172,54 @@ (declare impl_elim (! f1 formula (! f2 formula - (! u1 (th_holds f1) (! u2 (th_holds (impl f1 f2)) - (th_holds f2)))))) + (th_holds (or (not f1) f2)))))) +(declare not_impl_elim + (! f1 formula + (! f2 formula + (! u (th_holds (not (impl f1 f2))) + (th_holds (and f1 (not f2))))))) + ;; iff elimination (declare iff_elim_1 (! f1 formula (! f2 formula (! u1 (th_holds (iff f1 f2)) - (th_holds (impl f1 f2)))))) + (th_holds (or (not f1) f2)))))) (declare iff_elim_2 (! f1 formula (! f2 formula (! u1 (th_holds (iff f1 f2)) - (th_holds (impl f2 f1)))))) + (th_holds (or f1 (not f2))))))) -(declare not_iff_elim_1 +(declare not_iff_elim (! f1 formula (! f2 formula - (! u1 (th_holds (not f1)) (! u2 (th_holds (not (iff f1 f2))) - (th_holds f2)))))) + (th_holds (iff f1 (not f2))))))) + +; xor elimination -(declare not_iff_elim_2 +(declare xor_elim_1 (! f1 formula (! f2 formula - (! u1 (th_holds f1) - (! u2 (th_holds (not (iff f1 f2))) - (th_holds (not f2))))))) + (! u1 (th_holds (xor f1 f2)) + (th_holds (or (not f1) (not f2))))))) + +(declare xor_elim_2 + (! f1 formula + (! f2 formula + (! u1 (th_holds (xor f1 f2)) + (th_holds (or f1 f2)))))) + +(declare not_xor_elim + (! f1 formula + (! f2 formula + (! u2 (th_holds (not (xor f1 f2))) + (th_holds (iff f1 f2)))))) ;; ite elimination @@ -212,65 +227,43 @@ (! a formula (! b formula (! c formula - (! u1 (th_holds a) (! u2 (th_holds (ifte a b c)) - (th_holds b))))))) + (th_holds (or (not a) b))))))) (declare ite_elim_2 (! a formula (! b formula (! c formula - (! u1 (th_holds (not a)) (! u2 (th_holds (ifte a b c)) - (th_holds c))))))) + (th_holds (or a c))))))) (declare ite_elim_3 (! a formula (! b formula (! c formula - (! u1 (th_holds (not b)) (! u2 (th_holds (ifte a b c)) - (th_holds c))))))) - -(declare ite_elim_2n - (! a formula - (! b formula - (! c formula - (! u1 (th_holds a) - (! u2 (th_holds (ifte (not a) b c)) - (th_holds c))))))) + (th_holds (or b c))))))) (declare not_ite_elim_1 (! a formula (! b formula (! c formula - (! u1 (th_holds a) (! u2 (th_holds (not (ifte a b c))) - (th_holds (not b)))))))) + (th_holds (or (not a) (not b)))))))) (declare not_ite_elim_2 (! a formula (! b formula (! c formula - (! u1 (th_holds (not a)) (! u2 (th_holds (not (ifte a b c))) - (th_holds (not c)))))))) + (th_holds (or a (not c)))))))) (declare not_ite_elim_3 (! a formula (! b formula (! c formula - (! u1 (th_holds b) (! u2 (th_holds (not (ifte a b c))) - (th_holds (not c)))))))) - -(declare not_ite_elim_2n - (! a formula - (! b formula - (! c formula - (! u1 (th_holds a) - (! u2 (th_holds (not (ifte (not a) b c))) - (th_holds (not c)))))))) + (th_holds (or (not b) (not c)))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 977409b6a..9dd950b5b 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -23,6 +23,7 @@ ; inference rules : (declare trust (th_holds false)) ; temporary +(declare trust_f (! f formula (th_holds f))) ; temporary (declare refl (! s sort 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, NodeHashFunction >::const_iterator it = ProofManager::currentPM()->begin_deps(); + __gnu_cxx::hash_map< Node, std::vector, 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 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 deps = (*d_deps.find(n)).second; for(std::vector::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; isecond; + 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, NodeHashFunction >::const_iterator begin_deps() const { return d_deps.begin(); } + __gnu_cxx::hash_map< Node, std::vector, 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 ); } } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index fd30cd997..c8d86c73d 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: Morgan Deters, Dejan Jovanovic - ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway + ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway, 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 @@ -61,8 +61,8 @@ TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, c CnfStream(satSolver, registrar, context, fullLitToNodeMap) { } -void CnfStream::assertClause(TNode node, SatClause& c) { - Debug("cnf") << "Inserting into stream " << c << endl; +void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { + Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl; if(Dump.isOn("clauses")) { if(c.size() == 1) { Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr())); @@ -76,28 +76,31 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Dump("clauses") << AssertCommand(Expr(n.toExpr())); } } + //store map between clause and original formula + PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); ); d_satSolver->addClause(c, d_removable, d_proofId); + PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); ); } -void CnfStream::assertClause(TNode node, SatLiteral a) { +void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) { SatClause clause(1); clause[0] = a; - assertClause(node, clause); + assertClause(node, clause, proof_id); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id) { SatClause clause(2); clause[0] = a; clause[1] = b; - assertClause(node, clause); + assertClause(node, clause, proof_id); } -void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) { +void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id) { SatClause clause(3); clause[0] = a; clause[1] = b; clause[2] = c; - assertClause(node, clause); + assertClause(node, clause, proof_id); } bool CnfStream::hasLiteral(TNode n) const { @@ -260,10 +263,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) { SatLiteral xorLit = newLiteral(xorNode); - assertClause(xorNode, a, b, ~xorLit); - assertClause(xorNode, ~a, ~b, ~xorLit); - assertClause(xorNode, a, ~b, xorLit); - assertClause(xorNode, ~a, b, xorLit); + assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN); + assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN); + assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN); + assertClause(xorNode, ~a, b, xorLit, RULE_TSEITIN); return xorLit; } @@ -292,14 +295,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) { // lit | ~(a_1 | a_2 | a_3 | ... | a_n) // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(orNode, orLit, ~clause[i]); + assertClause(orNode, orLit, ~clause[i], RULE_TSEITIN); } // lit -> (a_1 | a_2 | a_3 | ... | a_n) // ~lit | a_1 | a_2 | a_3 | ... | a_n clause[n_children] = ~orLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(orNode, clause); + assertClause(orNode.negate(), clause, RULE_TSEITIN); // Return the literal return orLit; @@ -329,7 +332,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // ~lit | (a_1 & a_2 & a_3 & ... & a_n) // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) for(unsigned i = 0; i < n_children; ++i) { - assertClause(andNode, ~andLit, ~clause[i]); + assertClause(andNode.negate(), ~andLit, ~clause[i], RULE_TSEITIN); } // lit <- (a_1 & a_2 & a_3 & ... a_n) @@ -337,7 +340,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) { // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n clause[n_children] = andLit; // This needs to go last, as the clause might get modified by the SAT solver - assertClause(andNode, clause); + assertClause(andNode, clause, RULE_TSEITIN); return andLit; } @@ -356,13 +359,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { // lit -> (a->b) // ~lit | ~ a | b - assertClause(impliesNode, ~impliesLit, ~a, b); + assertClause(impliesNode.negate(), ~impliesLit, ~a, b, RULE_TSEITIN); // (a->b) -> lit // ~(~a | b) | lit // (a | l) & (~b | l) - assertClause(impliesNode, a, impliesLit); - assertClause(impliesNode, ~b, impliesLit); + assertClause(impliesNode, a, impliesLit, RULE_TSEITIN); + assertClause(impliesNode, ~b, impliesLit, RULE_TSEITIN); return impliesLit; } @@ -385,16 +388,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { // lit -> ((a-> b) & (b->a)) // ~lit | ((~a | b) & (~b | a)) // (~a | b | ~lit) & (~b | a | ~lit) - assertClause(iffNode, ~a, b, ~iffLit); - assertClause(iffNode, a, ~b, ~iffLit); + assertClause(iffNode.negate(), ~a, b, ~iffLit, RULE_TSEITIN); + assertClause(iffNode.negate(), a, ~b, ~iffLit, RULE_TSEITIN); // (a<->b) -> lit // ~((a & b) | (~a & ~b)) | lit // (~(a & b)) & (~(~a & ~b)) | lit // ((~a | ~b) & (a | b)) | lit // (~a | ~b | lit) & (a | b | lit) - assertClause(iffNode, ~a, ~b, iffLit); - assertClause(iffNode, a, b, iffLit); + assertClause(iffNode, ~a, ~b, iffLit, RULE_TSEITIN); + assertClause(iffNode, a, b, iffLit, RULE_TSEITIN); return iffLit; } @@ -429,9 +432,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // lit -> (t | e) & (b -> t) & (!b -> e) // lit -> (t | e) & (!b | t) & (b | e) // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) - assertClause(iteNode, ~iteLit, thenLit, elseLit); - assertClause(iteNode, ~iteLit, ~condLit, thenLit); - assertClause(iteNode, ~iteLit, condLit, elseLit); + assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit, RULE_TSEITIN); + assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit, RULE_TSEITIN); + assertClause(iteNode.negate(), ~iteLit, condLit, elseLit, RULE_TSEITIN); // If ITE is false then one of the branches is false and the condition // implies which one @@ -439,9 +442,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) { // !lit -> (!t | !e) & (b -> !t) & (!b -> !e) // !lit -> (!t | !e) & (!b | !t) & (b | !e) // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) - assertClause(iteNode, iteLit, ~thenLit, ~elseLit); - assertClause(iteNode, iteLit, ~condLit, ~thenLit); - assertClause(iteNode, iteLit, condLit, ~elseLit); + assertClause(iteNode, iteLit, ~thenLit, ~elseLit, RULE_TSEITIN); + assertClause(iteNode, iteLit, ~condLit, ~thenLit, RULE_TSEITIN); + assertClause(iteNode, iteLit, condLit, ~elseLit, RULE_TSEITIN); return iteLit; } @@ -506,13 +509,14 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { else return ~nodeLit; } -void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id) { Assert(node.getKind() == AND); if (!negated) { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - convertAndAssert(*conjunct, false); + PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).toExpr(), node.toExpr() ) ); + convertAndAssert(*conjunct, false, proof_id); } } else { // If the node is a disjunction, we construct a clause and assert it @@ -524,11 +528,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) { clause[i] = toCNF(*disjunct, true); } Assert(disjunct == node.end()); - assertClause(node, clause); + assertClause(node.negate(), clause, proof_id); } } -void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule proof_id) { Assert(node.getKind() == OR); if (!negated) { // If the node is a disjunction, we construct a clause and assert it @@ -540,17 +544,18 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) { clause[i] = toCNF(*disjunct, false); } Assert(disjunct == node.end()); - assertClause(node, clause); + assertClause(node, clause, proof_id); } else { // If the node is a conjunction, we handle each conjunct separately for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); conjunct != node_end; ++conjunct ) { - convertAndAssert(*conjunct, true); + PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).negate().toExpr(), node.negate().toExpr() ) ); + convertAndAssert(*conjunct, true, proof_id); } } } -void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) { if (!negated) { // p XOR q SatLiteral p = toCNF(node[0], false); @@ -559,11 +564,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { SatClause clause1(2); clause1[0] = ~p; clause1[1] = ~q; - assertClause(node, clause1); + assertClause(node, clause1, proof_id); SatClause clause2(2); clause2[0] = p; clause2[1] = q; - assertClause(node, clause2); + assertClause(node, clause2, proof_id); } else { // !(p XOR q) is the same as p <=> q SatLiteral p = toCNF(node[0], false); @@ -572,15 +577,15 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) { SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(node, clause1); + assertClause(node.negate(), clause1, proof_id); SatClause clause2(2); clause2[0] = p; clause2[1] = ~q; - assertClause(node, clause2); + assertClause(node.negate(), clause2, proof_id); } } -void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule proof_id) { if (!negated) { // p <=> q SatLiteral p = toCNF(node[0], false); @@ -589,11 +594,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(node, clause1); + assertClause(node, clause1, proof_id); SatClause clause2(2); clause2[0] = p; clause2[1] = ~q; - assertClause(node, clause2); + assertClause(node, clause2, proof_id); } else { // !(p <=> q) is the same as p XOR q SatLiteral p = toCNF(node[0], false); @@ -602,15 +607,15 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) { SatClause clause1(2); clause1[0] = ~p; clause1[1] = ~q; - assertClause(node, clause1); + assertClause(node.negate(), clause1, proof_id); SatClause clause2(2); clause2[0] = p; clause2[1] = q; - assertClause(node, clause2); + assertClause(node.negate(), clause2, proof_id); } } -void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id) { if (!negated) { // p => q SatLiteral p = toCNF(node[0], false); @@ -619,29 +624,35 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) { SatClause clause(2); clause[0] = ~p; clause[1] = q; - assertClause(node, clause); + assertClause(node, clause, proof_id); } else {// Construct the + PROOF(ProofManager::currentPM()->setCnfDep( node[0].toExpr(), node.negate().toExpr() ) ); + PROOF(ProofManager::currentPM()->setCnfDep( node[1].negate().toExpr(), node.negate().toExpr() ) ); // !(p => q) is the same as (p && ~q) - convertAndAssert(node[0], false); - convertAndAssert(node[1], true); + convertAndAssert(node[0], false, proof_id); + convertAndAssert(node[1], true, proof_id); } } -void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule proof_id) { // ITE(p, q, r) SatLiteral p = toCNF(node[0], false); SatLiteral q = toCNF(node[1], negated); SatLiteral r = toCNF(node[2], negated); // Construct the clauses: // (p => q) and (!p => r) + Node nnode = node; + if( negated ){ + nnode = node.negate(); + } SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; - assertClause(node, clause1); + assertClause(nnode, clause1, proof_id); SatClause clause2(2); clause2[0] = p; clause2[1] = r; - assertClause(node, clause2); + assertClause(nnode, clause2, proof_id); } // At the top level we must ensure that all clauses that are asserted are @@ -661,10 +672,10 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated // We aren't producing proofs or unsat cores; use an invalid proof id. d_proofId = uint64_t(-1); } - convertAndAssert(node, negated); + convertAndAssert(node, negated, proof_id); } -void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { +void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { @@ -675,29 +686,35 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { switch(node.getKind()) { case AND: - convertAndAssertAnd(node, negated); + convertAndAssertAnd(node, negated, proof_id); break; case OR: - convertAndAssertOr(node, negated); + convertAndAssertOr(node, negated, proof_id); break; case IFF: - convertAndAssertIff(node, negated); + convertAndAssertIff(node, negated, proof_id); break; case XOR: - convertAndAssertXor(node, negated); + convertAndAssertXor(node, negated, proof_id); break; case IMPLIES: - convertAndAssertImplies(node, negated); + convertAndAssertImplies(node, negated, proof_id); break; case ITE: - convertAndAssertIte(node, negated); + convertAndAssertIte(node, negated, proof_id); break; case NOT: - convertAndAssert(node[0], !negated); + convertAndAssert(node[0], !negated, proof_id); break; default: + { + Node nnode = node; + if( negated ){ + nnode = node.negate(); + } // Atoms - assertClause(node, toCNF(node, negated)); + assertClause(nnode, toCNF(node, negated), proof_id); + } break; } } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index b22290ae4..d5d01d126 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: Morgan Deters, Dejan Jovanovic - ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway + ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, 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 @@ -133,14 +133,14 @@ protected: * @param node the node giving rise to this clause * @param clause the clause to assert */ - void assertClause(TNode node, SatClause& clause); + void assertClause(TNode node, SatClause& clause, ProofRule proof_id); /** * Asserts the unit clause to the sat solver. * @param node the node giving rise to this clause * @param a the unit literal of the clause */ - void assertClause(TNode node, SatLiteral a); + void assertClause(TNode node, SatLiteral a, ProofRule proof_id); /** * Asserts the binary clause to the sat solver. @@ -148,7 +148,7 @@ protected: * @param a the first literal in the clause * @param b the second literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b); + void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id); /** * Asserts the ternary clause to the sat solver. @@ -157,7 +157,7 @@ protected: * @param b the second literal in the clause * @param c the thirs literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id); /** * Acquires a new variable from the SAT solver to represent the node @@ -298,7 +298,7 @@ private: /** * Same as above, except that removable is remembered. */ - void convertAndAssert(TNode node, bool negated); + void convertAndAssert(TNode node, bool negated, ProofRule proof_id); // Each of these formulas handles takes care of a Node of each Kind. // @@ -318,12 +318,12 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - void convertAndAssertAnd(TNode node, bool negated); - void convertAndAssertOr(TNode node, bool negated); - void convertAndAssertXor(TNode node, bool negated); - void convertAndAssertIff(TNode node, bool negated); - void convertAndAssertImplies(TNode node, bool negated); - void convertAndAssertIte(TNode node, bool negated); + void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id); /** * Transforms the node into CNF recursively. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index eca8c9d17..eb7792d2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -162,7 +162,6 @@ public: PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); ); d_nodes[i] = n; } - };/* class AssertionPipeline */ struct SmtEngineStatistics { @@ -572,8 +571,9 @@ public: * formula might be pushed out to the propositional layer * immediately, or it might be simplified and kept, or it might not * even be simplified. + * the 2nd and 3rd arguments added for bookkeeping for proofs */ - void addFormula(TNode n) + void addFormula(TNode n, bool inUnsatCore, bool inInput = true) throw(TypeCheckingException, LogicException); /** @@ -1930,7 +1930,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Node falseNode = NodeManager::currentNM()->mkConst(false); Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(falseNode); + addFormula(falseNode, false, false); d_propagatorNeedsFinish = true; return false; } @@ -1969,7 +1969,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << d_nonClausalLearnedLiterals[i] << endl; Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); + addFormula(NodeManager::currentNM()->mkConst(false), false, false); d_propagatorNeedsFinish = true; return false; } @@ -2005,7 +2005,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << learnedLiteral << endl; Assert(!options::unsatCores()); d_assertions.clear(); - d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); + addFormula(NodeManager::currentNM()->mkConst(false), false, false); d_propagatorNeedsFinish = true; return false; default: @@ -2031,7 +2031,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // if (!equations.empty()) { // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); // d_assertions.clear(); - // d_assertions.push_back(NodeManager::currentNM()->mkConst(false)); + // addFormula(NodeManager::currentNM()->mkConst(false), false, false); // return; // } // d_topLevelSubstitutions.simplifyRHS(constantPropagations); @@ -2642,7 +2642,7 @@ void SmtEnginePrivate::doMiplibTrick() { Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); - d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq))); + addFormula(Rewriter::rewrite(geq.andNode(leq)), false, false); SubstitutionMap nullMap(&d_fakeContext); Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions status = d_smt.d_theoryEngine->solve(geq, nullMap); @@ -2693,7 +2693,7 @@ void SmtEnginePrivate::doMiplibTrick() { } newAssertion = Rewriter::rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; - d_assertions.push_back(newAssertion); + addFormula(newAssertion, false, false); Debug("miplib") << " assertions to remove: " << endl; for(vector::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) { Debug("miplib") << " " << *k << endl; @@ -3417,7 +3417,7 @@ void SmtEnginePrivate::processAssertions() { d_iteSkolemMap.clear(); } -void SmtEnginePrivate::addFormula(TNode n) +void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) throw(TypeCheckingException, LogicException) { if (n == d_true) { @@ -3425,7 +3425,17 @@ void SmtEnginePrivate::addFormula(TNode n) return; } - Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; + Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl; + // Give it to proof manager + PROOF( + if( inInput ){ + // n is an input assertion + ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); + }else{ + // n is the result of an unknown preprocessing step, add it to dependency map to null + ProofManager::currentPM()->addDependence(n, Node::null()); + } + ); // Add the normalized formula to the queue d_assertions.push_back(n); @@ -3465,8 +3475,6 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); - // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); ); } // check to see if a postsolve() is pending @@ -3487,7 +3495,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE if(d_assertionList != NULL) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode()); + d_private->addFormula(e.getNode(), inUnsatCore); } Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); @@ -3553,8 +3561,6 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); - // Give it to proof manager - PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3573,7 +3579,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce if(d_assertionList != NULL) { d_assertionList->push_back(e.notExpr()); } - d_private->addFormula(e.getNode().notNode()); + d_private->addFormula(e.getNode().notNode(), inUnsatCore); // Run the check Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); @@ -3625,9 +3631,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); ); - + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex @@ -3637,7 +3641,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec if(d_assertionList != NULL) { d_assertionList->push_back(e); } - d_private->addFormula(e.getNode()); + d_private->addFormula(e.getNode(), inUnsatCore); return quickCheck().asValidityResult(); }/* SmtEngine::assertFormula() */ diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index da992286e..a8e7b6a8e 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -45,7 +45,10 @@ TESTS = \ simple.02.cvc \ simple.03.cvc \ simple.04.cvc \ - proof00.smt2 + proof00.smt2 \ + cnf-iff.smt2 \ + cnf-iff-base.smt2 \ + cnf-ite.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/cnf-iff-base.smt2 b/test/regress/regress0/uf/cnf-iff-base.smt2 new file mode 100644 index 000000000..9c538de6c --- /dev/null +++ b/test/regress/regress0/uf/cnf-iff-base.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) + +(declare-fun f (U) U) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) + +(assert (= (not (= (f a) d)) (not (= d (f b))))) + +(assert (or (not (= (f a) d)) (not (= d (f b))))) +(assert (or (= (f a) d) (= d (f b)))) + +(check-sat) diff --git a/test/regress/regress0/uf/cnf-iff.smt2 b/test/regress/regress0/uf/cnf-iff.smt2 new file mode 100644 index 000000000..03377005c --- /dev/null +++ b/test/regress/regress0/uf/cnf-iff.smt2 @@ -0,0 +1,38 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) + +(declare-fun f (U) U) +(declare-fun g (U) U) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(declare-fun e () U) +(declare-fun h () U) +(declare-fun i () U) + +(assert (or +(= a c) +(= h c) +(not (= h d)) +(not (= h e)) +(= h i) +(= (= (f a) d) (= d (f b))) +(= (not (= (f a) d)) (not (= d (f b)))) +(not (= (not (= d (f b))) (= (f a) d))) +(not (= (= d (f b)) (not (= (f a) d)))) +(xor (= (f a) d) (not (= d (f b)))) +(xor (not (= (f a) d)) (= d (f b))) +(not (xor (= (f a) d) (= d (f b)))) +(not (xor (not (= (f a) d)) (not (= d (f b))))) +)) +(assert (not (= h i))) +(assert (or (not (= (f a) d)) (not (= d (f b))))) +(assert (or (= (f a) d) (= d (f b)))) +(assert (and (not (= b e)) (not (= c a)))) +(assert (and (= h e) (not (= b e)))) + +(assert (not (or (= b h) (= c h)))) +(assert (not (or (= b h) (not (= d h))))) +(check-sat) diff --git a/test/regress/regress0/uf/cnf-ite.smt2 b/test/regress/regress0/uf/cnf-ite.smt2 new file mode 100644 index 000000000..851eb45aa --- /dev/null +++ b/test/regress/regress0/uf/cnf-ite.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --simplification=none +; EXPECT: unsat + +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) + +(declare-fun f (U) U) +(declare-fun g (U) U) +(declare-fun a () U) +(declare-fun b () U) +(declare-fun c () U) +(declare-fun d () U) +(declare-fun e () U) +(declare-fun h () U) +(declare-fun i () U) + +(assert (or +(ite (= (f a) d) (not (= d (f b))) (= a c)) +(ite (not (= (f a) d)) (= d e) (not (= d (f b)))) +(not (ite (not (= (f a) d)) (= d e) (= d (f b)))) +(not (ite (= (f a) d) (= d (f b)) (= a c))) +(ite (not (= (f a) e)) (= e (f b)) (= a c)) +(ite (= (f a) e) (= e e) (= e (f b))) +(not (ite (= (f a) e) (= e e) (not (= e (f b))))) +(not (ite (not (= (f a) e)) (not (= e (f b))) (= a c))) +(= a b) +)) + +(assert (and (= (f a) d) (= d (f b)))) +(assert (and (not (= (f a) e)) (not (= e (f b))))) + +(assert (not (= a b))) + +(check-sat) -- 2.30.2