(! 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
(! 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
(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
(! 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))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; inference rules :
(declare trust (th_holds false)) ; temporary
+(declare trust_f (! f formula (th_holds f))) ; temporary
(declare refl
(! s sort
/*! \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
}
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;
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 << "))";
}
/*! \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
};/* 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)
** \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
d_theoryProof(NULL),
d_fullProof(NULL),
d_format(format),
- d_deps()
+ d_deps(),
+ d_assertion_counter(1)
{
}
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);
+ }
}
}
}
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());
// 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)
** \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
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;
// 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;
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(); }
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 {
}
}
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];
}
}
}
Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
+ ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] );
return d_unitId[toInt(lit)];
}
}
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();
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 );
}
}
** \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
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()));
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 {
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;
}
// 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;
// ~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)
// 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;
}
// 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;
}
// 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;
}
// 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
// !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;
}
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
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
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);
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);
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);
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);
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);
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
// 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) {
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;
}
}
** \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
* @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.
* @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.
* @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
/**
* 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.
//
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.
PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
d_nodes[i] = n;
}
-
};/* class AssertionPipeline */
struct SmtEngineStatistics {
* 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);
/**
Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
Assert(!options::unsatCores());
d_assertions.clear();
- d_assertions.push_back(falseNode);
+ addFormula(falseNode, false, false);
d_propagatorNeedsFinish = true;
return false;
}
<< d_nonClausalLearnedLiterals[i] << endl;
Assert(!options::unsatCores());
d_assertions.clear();
- d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
d_propagatorNeedsFinish = true;
return false;
}
<< learnedLiteral << endl;
Assert(!options::unsatCores());
d_assertions.clear();
- d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+ addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
d_propagatorNeedsFinish = true;
return false;
default:
// 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<bool>(false));
+ // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
// return;
// }
// d_topLevelSubstitutions.simplifyRHS(constantPropagations);
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);
}
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<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
Debug("miplib") << " " << *k << endl;
d_iteSkolemMap.clear();
}
-void SmtEnginePrivate::addFormula(TNode n)
+void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
throw(TypeCheckingException, LogicException) {
if (n == d_true) {
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);
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
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);
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) {
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);
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
-
- PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); );
-
+
Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
// Substitute out any abstract values in ex
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() */
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
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff