From 42b665f2a00643c81b42932fab1441987628c5a5 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 26 Jan 2016 16:04:26 -0800 Subject: Merged bit-vector and uf proof branch. --- src/proof/array_proof.h | 78 +++ src/proof/bitvector_proof.cpp | 602 +++++++++++++++++++ src/proof/bitvector_proof.h | 142 +++++ src/proof/cnf_proof.cpp | 1049 +++++++++++++++++++------------- src/proof/cnf_proof.h | 136 ++++- src/proof/proof.h | 21 +- src/proof/proof_manager.cpp | 546 ++++++++++------- src/proof/proof_manager.h | 196 +++--- src/proof/proof_utils.cpp | 127 ++++ src/proof/proof_utils.h | 178 ++++++ src/proof/sat_proof.h | 291 +++++---- src/proof/sat_proof_implementation.h | 1100 ++++++++++++++++++++++++++++++++++ src/proof/theory_proof.cpp | 684 ++++++++++++++++----- src/proof/theory_proof.h | 282 +++++++-- src/proof/uf_proof.cpp | 804 +++++++++++++++++++++++++ src/proof/uf_proof.h | 75 +++ 16 files changed, 5269 insertions(+), 1042 deletions(-) create mode 100644 src/proof/array_proof.h create mode 100644 src/proof/bitvector_proof.cpp create mode 100644 src/proof/bitvector_proof.h create mode 100644 src/proof/proof_utils.cpp create mode 100644 src/proof/proof_utils.h create mode 100644 src/proof/sat_proof_implementation.h create mode 100644 src/proof/uf_proof.cpp create mode 100644 src/proof/uf_proof.h (limited to 'src/proof') diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h new file mode 100644 index 000000000..beaf5194c --- /dev/null +++ b/src/proof/array_proof.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file array_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** 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 + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Arrray proof + ** + ** Arrau proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ARRAY__PROOF_H +#define __CVC4__ARRAY__PROOF_H + +#include "expr/expr.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "theory/arrays/theory_arrays.h" + +namespace CVC4 { + +namespace theory { +namespace arrays{ +class TheoryArrays; +} /* namespace CVC4::theory::arrays */ +} /* namespace CVC4::theory */ + +class ArrayProof : public TheoryProof { + // TODO: whatever goes in this theory +public: + ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) + : TheoryProof(arrays, proofEngine) + {} + virtual void registerTerm(Expr term) {} + + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + virtual void printSort(Type type, std::ostream& os) = 0; + /** + * Print a proof for the theory lemma. Must prove + * clause representing lemma to be used in resolution proof. + * + * @param lemma clausal form of lemma + * @param os output stream + */ + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) = 0; + /** + * Print the variable/sorts declarations for this theory. + * + * @param os + * @param paren + */ + virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; +}; + +class LFSCArrayProof : public ArrayProof { +public: + LFSCArrayProof(theory::arrays::TheoryArrays* uf, TheoryProofEngine* proofEngine) + : ArrayProof(uf, proofEngine) + {} + // TODO implement + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) {} + virtual void printSort(Type type, std::ostream& os) {} + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) {} + virtual void printDeclarations(std::ostream& os, std::ostream& paren) {} + +}; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__ARRAY__PROOF_H */ diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp new file mode 100644 index 000000000..e067f0bce --- /dev/null +++ b/src/proof/bitvector_proof.cpp @@ -0,0 +1,602 @@ +/********************* */ +/*! \file bitvector_proof.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** 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 +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + + +#include "proof/bitvector_proof.h" +#include "options/bv_options.h" +#include "proof/proof_utils.h" +#include "proof/sat_proof_implementation.h" +#include "prop/bvminisat/bvminisat.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/theory_bv.h" + +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +namespace CVC4 { + +BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : TheoryProof(bv, proofEngine) + , d_declarations() + , d_seenBBTerms() + , d_bbTerms() + , d_bbAtoms() + , d_resolutionProof(NULL) + , d_cnfProof(NULL) + , d_bitblaster(NULL) +{} + +void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { + Assert (d_resolutionProof == NULL); + d_resolutionProof = new LFSCBVSatProof(solver, "bb", true); +} + +void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf) { + Assert (d_cnfProof == NULL); + d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb"); + Assert (d_resolutionProof != NULL); + d_resolutionProof->setCnfProof(d_cnfProof); + + // true and false have to be setup in a special way + Node true_node = NodeManager::currentNM()->mkConst(true); + Node false_node = NodeManager::currentNM()->mkConst(false).notNode(); + + d_cnfProof->pushCurrentAssertion(true_node); + d_cnfProof->pushCurrentDefinition(true_node); + d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit()); + d_cnfProof->popCurrentAssertion(); + d_cnfProof->popCurrentDefinition(); + + d_cnfProof->pushCurrentAssertion(false_node); + d_cnfProof->pushCurrentDefinition(false_node); + d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit()); + d_cnfProof->popCurrentAssertion(); + d_cnfProof->popCurrentDefinition(); +} + +void BitVectorProof::setBitblaster(bv::TBitblaster* bb) { + Assert (d_bitblaster == NULL); + d_bitblaster = bb; +} + +BVSatProof* BitVectorProof::getSatProof() { + Assert (d_resolutionProof != NULL); + return d_resolutionProof; +} + +void BitVectorProof::registerTermBB(Expr term) { + if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) + return; + + d_seenBBTerms.insert(term); + d_bbTerms.push_back(term); +} + +void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { + Expr def = atom.iffExpr(atom_bb); + d_bbAtoms.insert(std::make_pair(atom, def)); + registerTerm(atom); +} + +void BitVectorProof::registerTerm(Expr term) { + d_usedBB.insert(term); + + if (Theory::isLeafOf(term, theory::THEORY_BV) && + !term.isConst()) { + d_declarations.insert(term); + } + + // don't care about parametric operators for bv? + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + d_proofEngine->registerTerm(term[i]); + } +} + +std::string BitVectorProof::getBBTermName(Expr expr) { + std::ostringstream os; + os << "bt"<< expr.getId(); + return os.str(); +} + +void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TCRef cr) { + d_resolutionProof->startResChain(cr); +} + +void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) { + d_resolutionProof->startResChain(lit); +} + +void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) { + std::vector expr_confl; + for (int i = 0; i < confl.size(); ++i) { + prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); + Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; + expr_confl.push_back(expr_lit); + } + Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); + Debug("bv-proof") << "Make conflict for " << conflict << std::endl; + + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { + Debug("bv-proof") << "Abort...already conflict for " << conflict << std::endl; + // This can only happen when we have eager explanations in the bv solver + // if we don't get to propagate p before ~p is already asserted + d_resolutionProof->cancelResChain(); + return; + } + + // we don't need to check for uniqueness in the sat solver then + ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); + d_bbConflictMap[conflict] = clause_id; + d_resolutionProof->endResChain(clause_id); + Debug("bv-proof") << "BitVectorProof::endBVConflict id"< " << conflict << "\n"; + d_isAssumptionConflict = false; +} + +void BitVectorProof::finalizeConflicts(std::vector& conflicts) { + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + Debug("bv-proof") << "Construct full proof." << std::endl; + d_resolutionProof->constructProof(); + return; + } + for(unsigned i = 0; i < conflicts.size(); ++i) { + Expr confl = conflicts[i]; + Debug("bv-proof") << "Finalize conflict " << confl << std::endl; + //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end()); + if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){ + ClauseId id = d_bbConflictMap[confl]; + d_resolutionProof->collectClauses(id); + }else{ + Debug("bv-proof") << "Do not collect clauses for " << confl << std::endl; + } + } +} + +void LFSCBitVectorProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { + Assert (Theory::theoryOf(term) == THEORY_BV); + + // peel off eager bit-blasting trick + if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) { + d_proofEngine->printBoundTerm(term[0], os, map); + return; + } + + switch (term.getKind()) { + case kind::CONST_BITVECTOR : { + printConstant(term, os); + return; + } + case kind::BITVECTOR_AND : + case kind::BITVECTOR_OR : + case kind::BITVECTOR_XOR : + case kind::BITVECTOR_NAND : + case kind::BITVECTOR_NOR : + case kind::BITVECTOR_XNOR : + case kind::BITVECTOR_COMP : + case kind::BITVECTOR_MULT : + case kind::BITVECTOR_PLUS : + case kind::BITVECTOR_SUB : + case kind::BITVECTOR_UDIV : + case kind::BITVECTOR_UREM : + case kind::BITVECTOR_UDIV_TOTAL : + case kind::BITVECTOR_UREM_TOTAL : + case kind::BITVECTOR_SDIV : + case kind::BITVECTOR_SREM : + case kind::BITVECTOR_SMOD : + case kind::BITVECTOR_SHL : + case kind::BITVECTOR_LSHR : + case kind::BITVECTOR_ASHR : + case kind::BITVECTOR_CONCAT : { + printOperatorNary(term, os, map); + return; + } + case kind::BITVECTOR_NEG : + case kind::BITVECTOR_NOT : + case kind::BITVECTOR_ROTATE_LEFT : + case kind::BITVECTOR_ROTATE_RIGHT : { + printOperatorUnary(term, os, map); + return; + } + case kind::EQUAL : + case kind::BITVECTOR_ULT : + case kind::BITVECTOR_ULE : + case kind::BITVECTOR_UGT : + case kind::BITVECTOR_UGE : + case kind::BITVECTOR_SLT : + case kind::BITVECTOR_SLE : + case kind::BITVECTOR_SGT : + case kind::BITVECTOR_SGE : { + printPredicate(term, os, map); + return; + } + case kind::BITVECTOR_EXTRACT : + case kind::BITVECTOR_REPEAT : + case kind::BITVECTOR_ZERO_EXTEND : + case kind::BITVECTOR_SIGN_EXTEND : { + printOperatorParametric(term, os, map); + return; + } + case kind::BITVECTOR_BITOF : { + printBitOf(term, os); + return; + } + case kind::VARIABLE: + case kind::SKOLEM: { + os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")"; + return; + } + default: + Unreachable(); + } +} + +void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os) { + Assert (term.getKind() == kind::BITVECTOR_BITOF); + unsigned bit = term.getOperator().getConst().bitIndex; + Expr var = term[0]; + Assert (var.getKind() == kind::VARIABLE || + var.getKind() == kind::SKOLEM); + os << "(bitof " << ProofManager::sanitize(var) <<" " << bit <<")"; +} + +void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { + Assert (term.isConst()); + os <<"(a_bv " << utils::getSize(term)<<" "; + std::ostringstream paren; + int size = utils::getSize(term); + for (int i = size - 1; i >= 0; --i) { + os << "(bvc "; + os << (utils::getBit(term, i) ? "b1" : "b0") <<" "; + paren << ")"; + } + os << " bvn)"; + os << paren.str(); +} + +void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const LetMap& map) { + std::string op = utils::toLFSCKind(term.getKind()); + std::ostringstream paren; + std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; + unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) : + utils::getSize(term[0]); // cause of COMP + + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { + os <<"("<< op <<" " << size <<" " << holes; + } + d_proofEngine->printBoundTerm(term[0], os, map); + os <<" "; + for (unsigned i = 1; i < term.getNumChildren(); ++i) { + d_proofEngine->printBoundTerm(term[i], os, map); + os << ")"; + } +} + +void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const LetMap& map) { + os <<"("; + os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os << " "; + d_proofEngine->printBoundTerm(term[0], os, map); + os <<")"; +} + +void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMap& map) { + os <<"("; + os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" "; + os << " "; + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os <<")"; +} + +void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const LetMap& map) { + os <<"("; + os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os <<" "; + if (term.getKind() == kind::BITVECTOR_REPEAT) { + unsigned amount = term.getOperator().getConst().repeatAmount; + os << amount <<" _ "; + } + if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) { + unsigned amount = term.getOperator().getConst().signExtendAmount; + os << amount <<" _ "; + } + + if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) { + unsigned amount = term.getOperator().getConst().zeroExtendAmount; + os << amount<<" _ "; + } + if (term.getKind() == kind::BITVECTOR_EXTRACT) { + unsigned low = utils::getExtractLow(term); + unsigned high = utils::getExtractHigh(term); + os << high <<" " << low << " " << utils::getSize(term[0]); + } + os <<" "; + Assert (term.getNumChildren() == 1); + d_proofEngine->printBoundTerm(term[0], os, map); + os <<")"; +} + +void LFSCBitVectorProof::printSort(Type type, std::ostream& os) { + Assert (type.isBitVector()); + unsigned width = utils::getSize(type); + os << "(BitVec "<& lemma, std::ostream& os, std::ostream& paren) { + Expr conflict = utils::mkSortedExpr(kind::OR, lemma); + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { + std::ostringstream lemma_paren; + for (unsigned i = 0; i < lemma.size(); ++i) { + Expr lit = lemma[i]; + + if (lit.getKind() == kind::NOT) { + os << "(intro_assump_t _ _ _ "; + } else { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren <<")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os <<" "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os <<"(\\unit"<printAssumptionsResolution(lemma_id, os, lemma_paren); + os <= 0; --i) { + os << "(bvc "; + os << (utils::getBit(term, i) ? "b1" : "b0") <<" "; + paren << ")"; + } + os << " bvn)"; + os << paren.str(); + return; + } + case kind::BITVECTOR_AND : + case kind::BITVECTOR_OR : + case kind::BITVECTOR_XOR : + case kind::BITVECTOR_NAND : + case kind::BITVECTOR_NOR : + case kind::BITVECTOR_XNOR : + case kind::BITVECTOR_COMP : + case kind::BITVECTOR_MULT : + case kind::BITVECTOR_PLUS : + case kind::BITVECTOR_SUB : + case kind::BITVECTOR_CONCAT : { + for (unsigned i =0; i < term.getNumChildren() - 1; ++i) { + os <<"(bv_bbl_"<< utils::toLFSCKind(kind); + if (kind == kind::BITVECTOR_CONCAT) { + os << " " << utils::getSize(term) <<" _ "; + } + os <<" _ _ _ _ _ _ "; + } + os << getBBTermName(term[0]) <<" "; + + for (unsigned i = 1; i < term.getNumChildren(); ++i) { + os << getBBTermName(term[i]); + os << ") "; + } + return; + } + case kind::BITVECTOR_NEG : + case kind::BITVECTOR_NOT : + case kind::BITVECTOR_ROTATE_LEFT : + case kind::BITVECTOR_ROTATE_RIGHT : { + os <<"(bv_bbl_"<().repeatAmount; + os << amount; + } + if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) { + unsigned amount = term.getOperator().getConst().signExtendAmount; + os << amount; + } + + if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) { + unsigned amount = term.getOperator().getConst().zeroExtendAmount; + os << amount; + } + os <<" _ _ _ _ "; + os << getBBTermName(term[0]); + os <<")"; + return; + } + case kind::BITVECTOR_UDIV : + case kind::BITVECTOR_UREM : + case kind::BITVECTOR_UDIV_TOTAL : + case kind::BITVECTOR_UREM_TOTAL : + case kind::BITVECTOR_SDIV : + case kind::BITVECTOR_SREM : + case kind::BITVECTOR_SMOD : + case kind::BITVECTOR_SHL : + case kind::BITVECTOR_LSHR : + case kind::BITVECTOR_ASHR : { + // these are terms for which bit-blasting is not supported yet + std::ostringstream paren; + os <<"(trust_bblast_term _ "; + paren <<")"; + d_proofEngine->printLetTerm(term, os); + os <<" "; + std::vector bits; + d_bitblaster->bbTerm(term, bits); + + for (int i = utils::getSize(term) - 1; i >= 0; --i) { + os << "(bbltc "; + d_proofEngine->printLetTerm((bits[i]).toExpr(), os); + paren << ")"; + } + os << "bbltn" << paren.str(); + return; + } + + default: + Unreachable("LFSCBitVectorProof Unknown operator"); + } +} + +void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) { + Kind kind = atom.getKind(); + switch(kind) { + case kind::BITVECTOR_ULT : + case kind::BITVECTOR_ULE : + case kind::BITVECTOR_UGT : + case kind::BITVECTOR_UGE : + case kind::BITVECTOR_SLT : + case kind::BITVECTOR_SLE : + case kind::BITVECTOR_SGT : + case kind::BITVECTOR_SGE : + case kind::EQUAL: + { + os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + os << " _ _ _ _ _ _ "; + os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")"; + return; + } + default: + Unreachable("LFSCBitVectorProof Unknown atom kind"); + } +} + + +void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { + // bit-blast terms + std::vector::const_iterator it = d_bbTerms.begin(); + std::vector::const_iterator end = d_bbTerms.end(); + for (; it != end; ++it) { + if (d_usedBB.find(*it) == d_usedBB.end() && + options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) + continue; + os <<"(decl_bblast _ _ _ "; + printTermBitblasting(*it, os); + os << "(\\ "<< getBBTermName(*it); + paren <<"\n))"; + } + // bit-blast atoms + ExprToExpr::const_iterator ait = d_bbAtoms.begin(); + ExprToExpr::const_iterator aend = d_bbAtoms.end(); + for (; ait != aend; ++ait) { + if (d_usedBB.find(ait->first) == d_usedBB.end() && + options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) + continue; + + os << "(th_let_pf _ "; + if (ait->first.getKind() == kind::CONST_BOOLEAN) { + bool val = ait->first.getConst(); + os << "(iff_symm " << (val ? "true" : "false" ) << ")"; + } else { + printAtomBitblasting(ait->first, os); + } + + os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n"; + paren <<"))"; + } +} + +void LFSCBitVectorProof::printResolutionProof(std::ostream& os, + std::ostream& paren) { + // collect the input clauses used + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, + used_lemmas); + Assert (used_lemmas.empty()); + + // print mapping between theory atoms and internal SAT variables + os << ";; BB atom mapping\n"; + + NodeSet atoms; + d_cnfProof->collectAtomsForClauses(used_inputs,atoms); + + // first print bit-blasting + printBitblasting(os, paren); + + // print CNF conversion proof for bit-blasted facts + d_cnfProof->printAtomMapping(atoms, os, paren); + os << ";; Bit-blasting definitional clauses \n"; + for (IdToSatClause::iterator it = used_inputs.begin(); + it != used_inputs.end(); ++it) { + d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); + } + + os << ";; Bit-blasting learned clauses \n"; + d_resolutionProof->printResolutions(os, paren); +} + +} /* namespace CVC4 */ diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h new file mode 100644 index 000000000..80d567f7c --- /dev/null +++ b/src/proof/bitvector_proof.h @@ -0,0 +1,142 @@ +/********************* */ +/*! \file bitvector_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** 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 + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitvector proof + ** + ** Bitvector proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BITVECTOR__PROOF_H +#define __CVC4__BITVECTOR__PROOF_H + +//#include +#include +#include +#include +#include +#include +#include + +#include "expr/expr.h" +#include "proof/theory_proof.h" +#include "prop/bvminisat/core/Solver.h" + + +namespace CVC4 { + +namespace prop { +class CnfStream; +} /* namespace CVC4::prop */ + +namespace theory { +namespace bv { +class TheoryBV; +template class TBitblaster; +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ + +class CnfProof; +} /* namespace CVC4 */ + +namespace CVC4 { + +template class TSatProof; +typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; + +template class LFSCSatProof; +typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof; + +typedef __gnu_cxx::hash_set ExprSet; +typedef __gnu_cxx::hash_map ExprToClauseId; +typedef __gnu_cxx::hash_map ExprToId; +typedef __gnu_cxx::hash_map ExprToExpr; + +class BitVectorProof : public TheoryProof { +protected: + ExprSet d_declarations; + + ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof + + ExprSet d_seenBBTerms; // terms that need to be bit-blasted + std::vector d_bbTerms; // order of bit-blasting + ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted + + // map from Expr representing normalized lemma to ClauseId in SAT solver + ExprToClauseId d_bbConflictMap; + BVSatProof* d_resolutionProof; + + CnfProof* d_cnfProof; + + bool d_isAssumptionConflict; + theory::bv::TBitblaster* d_bitblaster; + std::string getBBTermName(Expr expr); +public: + BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); + + void initSatProof(CVC4::BVMinisat::Solver* solver); + void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); + void setBitblaster(theory::bv::TBitblaster* bb); + + BVSatProof* getSatProof(); + CnfProof* getCnfProof() {return d_cnfProof; } + void finalizeConflicts(std::vector& conflicts); + + void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); + void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); + /** + * All the + * + * @param confl an inconsistent set of bv literals + */ + void endBVConflict(const BVMinisat::Solver::TLitVec& confl); + void markAssumptionConflict() { d_isAssumptionConflict = true; } + bool isAssumptionConflict() { return d_isAssumptionConflict; } + + void registerTermBB(Expr term); + void registerAtomBB(Expr atom, Expr atom_bb); + + virtual void registerTerm(Expr term); + + virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; + virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0; + + virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; + virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0; + +}; + +class LFSCBitVectorProof: public BitVectorProof { + + void printConstant(Expr term, std::ostream& os); + void printOperatorNary(Expr term, std::ostream& os, const LetMap& map); + void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map); + void printPredicate(Expr term, std::ostream& os, const LetMap& map); + void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map); + void printBitOf(Expr term, std::ostream& os); +public: + LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + :BitVectorProof(bv, proofEngine) + {} + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printSort(Type type, std::ostream& os); + virtual void printTermBitblasting(Expr term, std::ostream& os); + virtual void printAtomBitblasting(Expr term, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printBitblasting(std::ostream& os, std::ostream& paren); + virtual void printResolutionProof(std::ostream& os, std::ostream& paren); +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__BITVECTOR__PROOF_H */ diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 263e1fe8c..884a67856 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -26,518 +26,709 @@ using namespace CVC4::prop; namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream) +CnfProof::CnfProof(CnfStream* stream, + context::Context* ctx, + const std::string& name) : d_cnfStream(stream) -{} + , d_clauseToAssertion(ctx) + , d_assertionToProofRule(ctx) + , d_currentAssertionStack() + , d_currentDefinitionStack() + , d_clauseToDefinition(ctx) + , d_definitions() + , d_cnfDeps() + , d_name(name) +{ + // Setting the proof object for the CnfStream + d_cnfStream->setProof(this); +} + +CnfProof::~CnfProof() {} -CnfProof::~CnfProof() { +bool CnfProof::isAssertion(Node node) { + return d_assertionToProofRule.find(node) != + d_assertionToProofRule.end(); } -Expr CnfProof::getAtom(prop::SatVariable var) { - prop::SatLiteral lit (var); - Node node = d_cnfStream->getNode(lit); - Expr atom = node.toExpr(); - return atom; +bool CnfProof::isDefinition(Node node) { + return d_definitions.find(node) != + d_definitions.end(); +} + +ProofRule CnfProof::getProofRule(Node node) { + Assert (isAssertion(node)); + NodeToProofRule::iterator it = d_assertionToProofRule.find(node); + return (*it).second; +} +ProofRule CnfProof::getProofRule(ClauseId clause) { + TNode assertion = getAssertionForClause(clause); + return getProofRule(assertion); } -prop::SatLiteral CnfProof::getLiteral(TNode atom) { - return d_cnfStream->getLiteral(atom); +Node CnfProof::getAssertionForClause(ClauseId clause) { + ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); + Assert (it != d_clauseToAssertion.end()); + return (*it).second; } -Expr CnfProof::getAssertion(uint64_t id) { - return d_cnfStream->getAssertion(id).toExpr(); +Node CnfProof::getDefinitionForClause(ClauseId clause) { + ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause); + Assert (it != d_clauseToDefinition.end()); + return (*it).second; } -void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { - for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) { - d_atomsDeclared.insert(lit.getSatVariable()); - os << "(decl_atom "; - if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 || - ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 || - ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) { - Expr atom = getAtom(lit.getSatVariable()); - LFSCTheoryProof::printTerm(atom, os); - } else { - // print fake atoms for all other logics (for now) - os << "true "; - } +void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { + Assert (clause != ClauseIdUndef && + clause != ClauseIdError && + clause != ClauseIdEmpty); + + // Explanations do not need a CNF conversion proof since they are in CNF + // (they will only need a theory proof as they are theory valid) + if (explanation) { + Debug("proof:cnf") << "CnfProof::registerConvertedClause " + << clause << " explanation? " << explanation << std::endl; + Assert (d_explanations.find(clause) == d_explanations.end()); + d_explanations.insert(clause); + return; + } - os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n"; - paren << ")))"; - } + Node current_assertion = getCurrentAssertion(); + Node current_expr = getCurrentDefinition(); + + Debug("proof:cnf") << "CnfProof::registerConvertedClause " + << clause << " assertion = " << current_assertion + << clause << " definition = " << current_expr << std::endl; + + setClauseAssertion(clause, current_assertion); + setClauseDefinition(clause, current_expr); +} + +void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { + Debug("proof:cnf") << "CnfProof::setClauseAssertion " + << clause << " assertion " << expr << std::endl; + // We can add the same clause from different assertions. In this + // case we keep the first assertion. For example asserting a /\ b + // and then b /\ c where b is an atom, would assert b twice (note + // that since b is top level, it is not cached by the CnfStream) + if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) + return; + + d_clauseToAssertion.insert (clause, expr); +} + +void CnfProof::setClauseDefinition(ClauseId clause, Node definition) { + Debug("proof:cnf") << "CnfProof::setClauseDefinition " + << clause << " definition " << definition << std::endl; + // We keep the first definition + if (d_clauseToDefinition.find(clause) != d_clauseToDefinition.end()) + return; + + d_clauseToDefinition.insert(clause, definition); + d_definitions.insert(definition); +} + +void CnfProof::registerAssertion(Node assertion, ProofRule reason) { + Debug("proof:cnf") << "CnfProof::registerAssertion " + << assertion << " reason " << reason << std::endl; + // We can obtain the assertion from different reasons (e.g. if the + // assertion is a lemma over shared terms both theories can generate + // the same lemma) We only need to prove the lemma in one way, so we + // keep the first reason. + if (isAssertion(assertion)) { + return; } + d_assertionToProofRule.insert(assertion, reason); } -void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { - printPreprocess(os, paren); - printInputClauses(os, paren); - printTheoryLemmas(os, paren); +void CnfProof::setCnfDependence(Node from, Node to) { + Debug("proof:cnf") << "CnfProof::setCnfDependence " + << "from " << from << std::endl + << " to " << to << std::endl; + + Assert (from != to); + d_cnfDeps.insert(std::make_pair(from, to)); } -void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) { - os << " ;; Preprocessing \n"; - __gnu_cxx::hash_map< Node, std::vector, NodeHashFunction >::const_iterator it = ProofManager::currentPM()->begin_deps(); - __gnu_cxx::hash_map< Node, std::vector, NodeHashFunction >::const_iterator end = ProofManager::currentPM()->end_deps(); +void CnfProof::pushCurrentAssertion(Node assertion) { + Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " + << assertion << std::endl; - for (; it != end; ++it) { - if( !it->second.empty() ){ - Expr e = it->first.toExpr(); - os << "(th_let_pf _ "; + d_currentAssertionStack.push_back(assertion); +} - //TODO - Trace("cnf-pf-debug") << "; preprocess assertion : " << e << std::endl; - os << "(trust_f "; - LFSCTheoryProof::printTerm(e, os); - os << ") "; +void CnfProof::popCurrentAssertion() { + Assert (d_currentAssertionStack.size()); + + Debug("proof:cnf") << "CnfProof::popCurrentAssertion " + << d_currentAssertionStack.back() << std::endl; + + d_currentAssertionStack.pop_back(); +} - os << "(\\ A" << ProofManager::currentPM()->getAssertionCounter() << std::endl; - ProofManager::currentPM()->setAssertion( e ); - paren << "))"; +Node CnfProof::getCurrentAssertion() { + Assert (d_currentAssertionStack.size()); + return d_currentAssertionStack.back(); +} + +void CnfProof::pushCurrentDefinition(Node definition) { + Debug("proof:cnf") << "CnfProof::pushCurrentDefinition " + << definition << std::endl; + + d_currentDefinitionStack.push_back(definition); +} + +void CnfProof::popCurrentDefinition() { + Assert (d_currentDefinitionStack.size()); + + Debug("proof:cnf") << "CnfProof::popCurrentDefinition " + << d_currentDefinitionStack.back() << std::endl; + + d_currentDefinitionStack.pop_back(); +} + +Node CnfProof::getCurrentDefinition() { + Assert (d_currentDefinitionStack.size()); + return d_currentDefinitionStack.back(); +} + + +Node CnfProof::getAtom(prop::SatVariable var) { + prop::SatLiteral lit (var); + Node node = d_cnfStream->getNode(lit); + return node; +} + + +void CnfProof::collectAtoms(const prop::SatClause* clause, + NodeSet& atoms) { + for (unsigned i = 0; i < clause->size(); ++i) { + SatLiteral lit = clause->operator[](i); + SatVariable var = lit.getSatVariable(); + TNode atom = getAtom(var); + if (atoms.find(atom) == atoms.end()) { + Assert (atoms.find(atom) == atoms.end()); + atoms.insert(atom); + } + } +} + +prop::SatLiteral CnfProof::getLiteral(TNode atom) { + return d_cnfStream->getLiteral(atom); +} + +void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses, + NodeSet& atom_map) { + IdToSatClause::const_iterator it = clauses.begin(); + for (; it != clauses.end(); ++it) { + const prop::SatClause* clause = it->second; + collectAtoms(clause, atom_map); + } + +} + +void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, + NodeSet& assertions) { + IdToSatClause::const_iterator it = clauses.begin(); + for (; it != clauses.end(); ++it) { + TNode used_assertion = getAssertionForClause(it->first); + assertions.insert(used_assertion); + // it can be the case that a definition for a clause is an assertion + // but it is not the assertion for the clause + // e.g. the assertions [(and a b), a] + TNode used_definition = getDefinitionForClause(it->first); + if (isAssertion(used_definition)) { + assertions.insert(used_definition); } } } -Expr LFSCCnfProof::clauseToExpr( const prop::SatClause& clause, - std::map< Expr, unsigned >& childIndex, - std::map< Expr, bool >& childPol ) { +void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren) { + NodeSet::const_iterator it = atoms.begin(); + NodeSet::const_iterator end = atoms.end(); + + for (;it != end; ++it) { + os << "(decl_atom "; + Node atom = *it; + prop::SatVariable var = getLiteral(atom).getSatVariable(); + //FIXME hideous + LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); + pe->printLetTerm(atom.toExpr(), os); + + os << " (\\ " << ProofManager::getVarName(var, d_name) + << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + paren << ")))"; + } +} + +// maps each expr to the position it had in the clause and the polarity it had +Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause, + std::map& childIndex, + std::map& childPol ) { std::vector< Node > children; for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); - Node atom = Node::fromExpr( getAtom(var) ); + Node atom = getAtom(var); children.push_back( lit.isNegated() ? atom.negate() : atom ); - childIndex[atom.toExpr()] = i; - childPol[atom.toExpr()] = !lit.isNegated(); + childIndex[atom] = i; + childPol[atom] = !lit.isNegated(); } - return children.size()==1 ? children[0].toExpr() : NodeManager::currentNM()->mkNode( kind::OR, children ).toExpr(); + return children.size()==1 ? children[0] : + NodeManager::currentNM()->mkNode(kind::OR, children ); } -void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { - os << " ;; Clauses\n"; - ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); - ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); - - - for (; it != end; ++it) { - ClauseId id = it->first; - const prop::SatClause* clause = it->second; - printAtomMapping(clause, os, paren); - os << "(satlem _ _ "; - std::ostringstream clause_paren; - printClause(*clause, os, clause_paren); - os << "(clausify_false "; - - Assert( clause->size()>0 ); - - Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id ); - ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id ); - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << "; formula for clause id " << id << " : " << base_assertion << std::endl; - - //get the assertion for the clause id - std::map< Expr, unsigned > childIndex; - std::map< Expr, bool > childPol; - Expr assertion = clauseToExpr( *clause, childIndex, childPol ); - //if there is no reason, construct assertion directly. This can happen for unit clauses. - if( base_assertion.isNull() ){ - base_assertion = assertion; - } - //os_base is proof of base_assertion - std::stringstream os_base; - bool is_input = ProofManager::currentPM()->isInputAssertion( base_assertion, os_base ); - - //get base assertion with polarity - bool base_pol = base_assertion.getKind()!=kind::NOT; - base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; - - std::map< Expr, unsigned >::iterator itci = childIndex.find( base_assertion ); - bool is_in_clause = itci!=childIndex.end(); - unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; - if( !is_input ){ - Assert( is_in_clause ); - prop::SatLiteral blit = (*clause)[ base_index ]; - os_base << ProofManager::getLitName(blit); - base_pol = !childPol[base_assertion]; +void LFSCCnfProof::printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren) { + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(*clause, os, clause_paren); + os << "(clausify_false "; + + // FIXMEEEEEEEEEEEE + // os <<"trust)"; + // os << clause_paren.str() + // << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + // paren << "))"; + + // return; + + Assert( clause->size()>0 ); + + Node base_assertion = getDefinitionForClause(id); + + //get the assertion for the clause id + std::map childIndex; + std::map childPol; + Node assertion = clauseToNode( *clause, childIndex, childPol ); + //if there is no reason, construct assertion directly. This can happen for unit clauses. + if( base_assertion.isNull() ){ + base_assertion = assertion; + } + //os_base is proof of base_assertion + std::stringstream os_base; + + // checks if tautological definitional clause or top-level clause + // and prints the proof of the top-level formula + bool is_input = printProofTopLevel(base_assertion, os_base); + + //get base assertion with polarity + bool base_pol = base_assertion.getKind()!=kind::NOT; + base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; + + std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion ); + bool is_in_clause = itci!=childIndex.end(); + unsigned base_index = is_in_clause ? itci->second : 0; + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; + if (!is_input){ + Assert(is_in_clause); + prop::SatLiteral blit = (*clause)[ base_index ]; + os_base << ProofManager::getLitName(blit, d_name); + base_pol = !childPol[base_assertion]; // WHY? if the case is => + } + Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; + Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; + + bool success = false; + if( is_input && + is_in_clause && + childPol[base_assertion]==base_pol ){ + //if both in input and in clause, the proof is trivial. this is the case for unit clauses. + Trace("cnf-pf") << "; trivial" << std::endl; + os << "(contra _ "; + success = true; + prop::SatLiteral lit = (*clause)[itci->second]; + if( base_pol ){ + os << os_base.str() << " " << ProofManager::getLitName(lit, d_name); + }else{ + os << ProofManager::getLitName(lit, d_name) << " " << os_base.str(); } - Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl; - Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl; - - bool success = false; - if( is_input && is_in_clause && childPol[base_assertion]==base_pol ){ - //if both in input and in clause, the proof is trivial. this is the case for unit clauses. - Trace("cnf-pf") << "; trivial" << std::endl; - os << "(contra _ "; - success = true; - prop::SatLiteral lit = (*clause)[itci->second]; - if( base_pol ){ - os << os_base.str() << " " << ProofManager::getLitName(lit); - }else{ - os << ProofManager::getLitName(lit) << " " << os_base.str(); + os << ")"; + } else if ((base_assertion.getKind()==kind::AND && !base_pol) || + ((base_assertion.getKind()==kind::OR || + base_assertion.getKind()==kind::IMPLIES) && base_pol)) { + Trace("cnf-pf") << "; and/or case 1" << std::endl; + success = true; + std::stringstream os_main; + std::stringstream os_paren; + //eliminate each one + for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) { + Node child_base = base_assertion[j].getKind()==kind::NOT ? + base_assertion[j][0] : base_assertion[j]; + bool child_pol = base_assertion[j].getKind()!=kind::NOT; + + if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ + child_pol = !child_pol; } - os << ")"; - }else if( ( base_assertion.getKind()==kind::AND && !base_pol ) || ( ( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ) && base_pol ) ){ - Trace("cnf-pf") << "; and/or case 1" << std::endl; - success = true; - std::stringstream os_main; - std::stringstream os_paren; - //eliminate each one - for( int j=base_assertion.getNumChildren()-2; j>=0; j-- ){ - Expr child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; - bool child_pol = base_assertion[j].getKind()!=kind::NOT; - if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ - child_pol = !child_pol; + + Trace("cnf-pf-debug") << "; child " << j << " " + << child_base << " " + << child_pol << " " + << childPol[child_base] << std::endl; + + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + + if( itcic!=childIndex.end() ){ + //Assert( child_pol==childPol[child_base] ); + os_main << "(or_elim_1 _ _ "; + prop::SatLiteral lit = (*clause)[itcic->second]; + // Should be if in the original formula it was negated + if( childPol[child_base] && base_pol ){ + os_main << ProofManager::getLitName(lit, d_name) << " "; + }else{ + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; } - Trace("cnf-pf-debug") << "; child " << j << " " << child_base << " " << child_pol << " " << childPol[child_base] << std::endl; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - //Assert( child_pol==childPol[child_base] ); - os_main << "(or_elim_1 _ _ "; - prop::SatLiteral lit = (*clause)[itcic->second]; - if( childPol[child_base] && base_pol ){ - os_main << ProofManager::getLitName(lit) << " "; - }else{ - os_main << "(not_not_intro _ " << ProofManager::getLitName(lit) << ") "; - } - if( base_assertion.getKind()==kind::AND ){ - os_main << "(not_and_elim _ _ "; - os_paren << ")"; - } + if( base_assertion.getKind()==kind::AND ){ + os_main << "(not_and_elim _ _ "; os_paren << ")"; - }else{ - success = false; } + os_paren << ")"; + }else{ + success = false; } - if( success ){ - if( base_assertion.getKind()==kind::IMPLIES ){ - os_main << "(impl_elim _ _ "; - } - os_main << os_base.str(); - if( base_assertion.getKind()==kind::IMPLIES ){ - os_main << ")"; - } - os_main << os_paren.str(); - int last_index = base_assertion.getNumChildren()-1; - Expr child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index]; - //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - os << "(contra _ "; - prop::SatLiteral lit = (*clause)[itcic->second]; - if( childPol[child_base] && base_pol ){ - os << os_main.str() << " " << ProofManager::getLitName(lit); - }else{ - os << ProofManager::getLitName(lit) << " " << os_main.str(); - } - os << ")"; - }else{ - success = false; - } + } + if( success ){ + if( base_assertion.getKind()==kind::IMPLIES ){ + os_main << "(impl_elim _ _ "; } - }else if( ( base_assertion.getKind()==kind::AND && base_pol ) || ( ( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ) && !base_pol ) ){ - std::stringstream os_main; - Expr iatom; - if( is_in_clause ){ - Assert( assertion.getNumChildren()==2 ); - iatom = assertion[ base_index==0 ? 1 : 0]; - }else{ - Assert( assertion.getNumChildren()==1 ); - iatom = assertion[0]; + os_main << os_base.str(); + if( base_assertion.getKind()==kind::IMPLIES ){ + os_main << ")"; } - Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl; - Expr e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom; - bool e_pol = iatom.getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( e_base ); + os_main << os_paren.str(); + int last_index = base_assertion.getNumChildren()-1; + Node child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index]; + //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); if( itcic!=childIndex.end() ){ + os << "(contra _ "; prop::SatLiteral lit = (*clause)[itcic->second]; - //eliminate until we find iatom - for( unsigned j=0; j indices; - std::vector< bool > pols; - success = true; - int elimNum = 0; - for( unsigned i=0; i<2; i++ ){ - Expr child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i]; - bool child_pol = base_assertion[i].getKind()!=kind::NOT; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - indices.push_back( itcic->second ); - pols.push_back( childPol[child_base] ); - if( i==0 ){ - //figure out which way to elim - elimNum = child_pol==childPol[child_base] ? 2 : 1; - if( (elimNum==2)==(k==kind::IFF) ){ - num_nots_2++; - } - if( elimNum==1 ){ - num_nots_1++; - } - } - }else{ - success = false; break; } } - Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl; if( success ){ os << "(contra _ "; - std::stringstream os_base_n; - if( num_nots_2==2 ){ - os_base_n << "(not_not_elim _ "; - } - os_base_n << "(or_elim_1 _ _ "; - prop::SatLiteral lit1 = (*clause)[indices[0]]; - if( !pols[0] || num_nots_1==1 ){ - os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1) << ") "; - }else{ - os_base_n << ProofManager::getLitName(lit1) << " "; - } - Assert( elimNum!=0 ); - os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; - if( !base_pol ){ - os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; - }else{ - os_base_n << os_base.str(); - } - os_base_n << "))"; - if( num_nots_2==2 ){ - os_base_n << ")"; - num_nots_2 = 0; - } - prop::SatLiteral lit2 = (*clause)[indices[1]]; - if( pols[1]==(num_nots_2==0) ){ - os << os_base_n.str() << " "; - if( num_nots_2==1 ){ - os << "(not_not_intro _ " << ProofManager::getLitName(lit2) << ")"; - }else{ - os << ProofManager::getLitName(lit2); - } + if( !e_pol ){ + os << ProofManager::getLitName(lit, d_name) << " " << os_main.str(); }else{ - os << ProofManager::getLitName(lit2) << " " << os_base_n.str(); + os << os_main.str() << " " << ProofManager::getLitName(lit, d_name); } os << ")"; } - }else if( base_assertion.getKind()==kind::ITE ){ - std::map< unsigned, unsigned > appears; - std::map< unsigned, Expr > appears_expr; - unsigned appears_count = 0; - for( unsigned r=0; r<3; r++ ){ - Expr child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r]; - std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base ); - if( itcic!=childIndex.end() ){ - appears[r] = itcic->second; - appears_expr[r] = child_base; - appears_count++; - } + } + }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){ + //eliminate negation + int num_nots_2 = 0; + int num_nots_1 = 0; + Kind k; + if( !base_pol ){ + if( base_assertion.getKind()==kind::IFF ){ + num_nots_2 = 1; } - if( appears_count==2 ){ - success = true; - int elimNum = 1; - unsigned index1 = 0; - unsigned index2 = 1; - if( appears.find( 0 )==appears.end() ){ - elimNum = 3; - index1 = 1; - index2 = 2; - }else if( appears.find( 1 )==appears.end() ){ - elimNum = 2; - index1 = 0; - index2 = 2; - } - std::stringstream os_main; - os_main << "(or_elim_1 _ _ "; - prop::SatLiteral lit1 = (*clause)[appears[index1]]; - if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){ - os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1) << ") "; - }else{ - os_main << ProofManager::getLitName(lit1) << " "; - } - os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ "; - os_main << os_base.str() << "))"; - os << "(contra _ "; - prop::SatLiteral lit2 = (*clause)[appears[index2]]; - if( !childPol[appears_expr[index2]] || !base_pol ){ - os << ProofManager::getLitName(lit2) << " " << os_main.str(); - }else{ - os << os_main.str() << " " << ProofManager::getLitName(lit2); + k = kind::IFF; + }else{ + k = base_assertion.getKind(); + } + std::vector< unsigned > indices; + std::vector< bool > pols; + success = true; + int elimNum = 0; + for( unsigned i=0; i<2; i++ ){ + Node child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i]; + bool child_pol = base_assertion[i].getKind()!=kind::NOT; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + if( itcic!=childIndex.end() ){ + indices.push_back( itcic->second ); + pols.push_back( childPol[child_base] ); + if( i==0 ){ + //figure out which way to elim + elimNum = child_pol==childPol[child_base] ? 2 : 1; + if( (elimNum==2)==(k==kind::IFF) ){ + num_nots_2++; + } + if( elimNum==1 ){ + num_nots_1++; + } } - os << ")"; + }else{ + success = false; + break; + } + } + Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl; + if( success ){ + os << "(contra _ "; + std::stringstream os_base_n; + if( num_nots_2==2 ){ + os_base_n << "(not_not_elim _ "; + } + os_base_n << "(or_elim_1 _ _ "; + prop::SatLiteral lit1 = (*clause)[indices[0]]; + if( !pols[0] || num_nots_1==1 ){ + os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; + }else{ + os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } - }else if( base_assertion.isConst() ){ - bool pol = base_assertion==NodeManager::currentNM()->mkConst( true ).toExpr(); - if( pol!=base_pol ){ - success = true; - if( pol ){ - os << "(contra _ truth " << os_base.str() << ")"; + Assert( elimNum!=0 ); + os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; + if( !base_pol ){ + os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; + }else{ + os_base_n << os_base.str(); + } + os_base_n << "))"; + if( num_nots_2==2 ){ + os_base_n << ")"; + num_nots_2 = 0; + } + prop::SatLiteral lit2 = (*clause)[indices[1]]; + if( pols[1]==(num_nots_2==0) ){ + os << os_base_n.str() << " "; + if( num_nots_2==1 ){ + os << "(not_not_intro _ " << ProofManager::getLitName(lit2, d_name) << ")"; }else{ - os << os_base.str(); + os << ProofManager::getLitName(lit2, d_name); } + }else{ + os << ProofManager::getLitName(lit2, d_name) << " " << os_base_n.str(); } + os << ")"; } - - if( !success ){ - Trace("cnf-pf") << std::endl; - Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << ", proof rule = " << pr << std::endl; - Trace("cnf-pf") << ";!!!!!!!!! Clause is : "; - for (unsigned i = 0; i < clause->size(); ++i) { - Trace("cnf-pf") << (*clause)[i] << " "; + }else if( base_assertion.getKind()==kind::ITE ){ + std::map< unsigned, unsigned > appears; + std::map< unsigned, Node > appears_expr; + unsigned appears_count = 0; + for( unsigned r=0; r<3; r++ ){ + Node child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r]; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); + if( itcic!=childIndex.end() ){ + appears[r] = itcic->second; + appears_expr[r] = child_base; + appears_count++; } - Trace("cnf-pf") << std::endl; - os << "trust-bad"; - } - - os << ")" << clause_paren.str() - << " (\\ " << ProofManager::getInputClauseName(id) << "\n"; - paren << "))"; - } -} - -void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - os << " ;; Theory Lemmas\n"; - ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas(); - ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas(); - - for(size_t n = 0; it != end; ++it, ++n) { - if(n % 100 == 0) { - Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl; } - - ClauseId id = it->first; - const prop::SatClause* clause = it->second; - NodeBuilder<> c(kind::AND); - for(unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = (*clause)[i]; - prop::SatVariable var = lit.getSatVariable(); - if(lit.isNegated()) { - c << Node::fromExpr(getAtom(var)); - } else { - c << Node::fromExpr(getAtom(var)).notNode(); + if( appears_count==2 ){ + success = true; + int elimNum = 1; + unsigned index1 = 0; + unsigned index2 = 1; + if( appears.find( 0 )==appears.end() ){ + elimNum = 3; + index1 = 1; + index2 = 2; + }else if( appears.find( 1 )==appears.end() ){ + elimNum = 2; + index1 = 0; + index2 = 2; } - } - Node cl = c; - if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { - uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; - TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); - if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { - Debug("cores") << "; extensional lemma!" << std::endl; - Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT); - TNode myk = cl[0][0][1]; - Debug("cores") << "; so my skolemized k is " << myk << std::endl; - os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n"; - paren << ")))"; + std::stringstream os_main; + os_main << "(or_elim_1 _ _ "; + prop::SatLiteral lit1 = (*clause)[appears[index1]]; + if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){ + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; + }else{ + os_main << ProofManager::getLitName(lit1, d_name) << " "; + } + os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ "; + os_main << os_base.str() << "))"; + os << "(contra _ "; + prop::SatLiteral lit2 = (*clause)[appears[index2]]; + if( !childPol[appears_expr[index2]] || !base_pol ){ + os << ProofManager::getLitName(lit2, d_name) << " " << os_main.str(); + }else{ + os << os_main.str() << " " << ProofManager::getLitName(lit2, d_name); } + os << ")"; } - printAtomMapping(clause, os, paren); - os << "(satlem _ _ "; - std::ostringstream clause_paren; - printClause(*clause, os, clause_paren); - - Debug("cores") << "\n;id is " << id << std::endl; - if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) { - uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id]; - Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl; - Assert(int32_t(proof_id & 0xffffffff) != -1); - TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff); - Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl; - Debug("cores") << "; that means the lemma was " << orig << std::endl; - if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) { - Debug("cores") << "; extensional" << std::endl; - os << "(clausify_false trust)\n"; - } else if(proof_id == 0) { - // theory propagation caused conflict - //ProofManager::currentPM()->printProof(os, cl); - os << "(clausify_false trust)\n"; - } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) { - os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; - //ProofManager::currentPM()->printProof(os, cl); - os << "(clausify_false trust)\n"; - } else { - os << "\n;; need to generate a (lemma) proof of " << cl; - os << "\n;; DON'T KNOW HOW !!\n"; - os << "(clausify_false trust)\n"; + }else if( base_assertion.isConst() ){ + bool pol = base_assertion==NodeManager::currentNM()->mkConst( true ); + if( pol!=base_pol ){ + success = true; + if( pol ){ + os << "(contra _ truth " << os_base.str() << ")"; + }else{ + os << os_base.str(); } - } else { - os << "\n;; need to generate a (conflict) proof of " << cl << "\n"; - ProofManager::currentPM()->printProof(os, cl); } - os << clause_paren.str() - << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n"; - paren << "))"; } + + if( !success ){ + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << std::endl; + Trace("cnf-pf") << ";!!!!!!!!! Clause is : "; + for (unsigned i = 0; i < clause->size(); ++i) { + Trace("cnf-pf") << (*clause)[i] << " "; + } + Trace("cnf-pf") << std::endl; + os << "trust-bad"; + } + + os << ")" << clause_paren.str() + << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + paren << "))"; } -void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) { +void LFSCCnfProof::printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren) { for (unsigned i = 0; i < clause.size(); ++i) { prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { - os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; + os << "(ast _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " "; paren << "))"; } else { - os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " "; + os << "(asf _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " "; paren << "))"; } } } +// print a proof of the top-level formula e, based on the input assertions +bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) { + if (!isAssertion(e)) { + // check if deduced by CNF + // dependence on top level fact i.e. a depends on (a and b) + NodeToNode::const_iterator itd = d_cnfDeps.find(e); + if (itd != d_cnfDeps.end()) { + TNode parent = itd->second; + //check if parent is an input assertion + std::stringstream out_parent; + if (printProofTopLevel(parent, out_parent)) { + if(parent.getKind()==kind::AND || + (parent.getKind()==kind::NOT && (parent[0].getKind()==kind::IMPLIES || + parent[0].getKind()==kind::OR))) { + Node parent_base = parent.getKind()==kind::NOT ? parent[0] : parent; + Node e_base = e.getKind()==kind::NOT ? e[0] : e; + bool e_pol = e.getKind()!=kind::NOT; + for( unsigned i=0; i +#include #include #include +#include "context/cdhashmap.h" #include "proof/sat_proof.h" +#include "proof/sat_proof.h" +#include "util/proof.h" #include "util/proof.h" namespace CVC4 { @@ -35,38 +38,131 @@ namespace prop { class CnfProof; +typedef __gnu_cxx::hash_map SatVarToExpr; +typedef __gnu_cxx::hash_map NodeToNode; +typedef __gnu_cxx::hash_set ClauseIdSet; + +typedef context::CDHashMap ClauseIdToNode; +typedef context::CDHashMap NodeToProofRule; + class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - VarSet d_atomsDeclared; + + /** Map from ClauseId to the assertion that lead to adding this clause **/ + ClauseIdToNode d_clauseToAssertion; + + /** Map from assertion to reason for adding assertion **/ + NodeToProofRule d_assertionToProofRule; + + /** Top of stack is assertion currently being converted to CNF **/ + std::vector d_currentAssertionStack; + + /** Top of stack is top-level fact currently being converted to CNF **/ + std::vector d_currentDefinitionStack; + + + /** Map from ClauseId to the top-level fact that lead to adding this clause **/ + ClauseIdToNode d_clauseToDefinition; + + /** Top-level facts that follow from assertions during convertAndAssert **/ + NodeSet d_definitions; + + /** Map from top-level fact to facts/assertion that it follows from **/ + NodeToNode d_cnfDeps; + + ClauseIdSet d_explanations; + + bool isDefinition(Node node); + + Node getDefinitionForClause(ClauseId clause); + + std::string d_name; public: - CnfProof(CVC4::prop::CnfStream* cnfStream); + CnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx, + const std::string& name); + + + Node getAtom(prop::SatVariable var); + prop::SatLiteral getLiteral(TNode node); + void collectAtoms(const prop::SatClause* clause, + NodeSet& atoms); + void collectAtomsForClauses(const IdToSatClause& clauses, + NodeSet& atoms); + void collectAssertionsForClauses(const IdToSatClause& clauses, + NodeSet& assertions); + + /** Methods for logging what the CnfStream does **/ + // map the clause back to the current assertion where it came from + // if it is an explanation, it does not have a CNF proof since it is + // already in CNF + void registerConvertedClause(ClauseId clause, bool explanation=false); + + /** Clause is one of the clauses defining the node expression*/ + void setClauseDefinition(ClauseId clause, Node node); + + /** Clause is one of the clauses defining top-level assertion node*/ + void setClauseAssertion(ClauseId clause, Node node); + + void registerAssertion(Node assertion, ProofRule reason); + void setCnfDependence(Node from, Node to); + + void pushCurrentAssertion(Node assertion); // the current assertion being converted + void popCurrentAssertion(); + Node getCurrentAssertion(); + + void pushCurrentDefinition(Node assertion); // the current Tseitin definition being converted + void popCurrentDefinition(); + Node getCurrentDefinition(); + + + // accessors for the leaf assertions that are being converted to CNF + bool isAssertion(Node node); + ProofRule getProofRule(Node assertion); + ProofRule getProofRule(ClauseId clause); + Node getAssertionForClause(ClauseId clause); - Expr getAtom(prop::SatVariable var); - Expr getAssertion(uint64_t id); - prop::SatLiteral getLiteral(TNode atom); + + /** Virtual methods for printing things **/ + virtual void printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren) = 0; - virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; + virtual void printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren) = 0; + virtual void printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren) = 0; virtual ~CnfProof(); };/* 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 ); - + Node clauseToNode( const prop::SatClause& clause, + std::map& childIndex, + std::map& childPol ); + bool printProofTopLevel(Node e, std::ostream& out); public: - LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) - : CnfProof(cnfStream) + LFSCCnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx, + const std::string& name) + : CnfProof(cnfStream, ctx, name) {} + ~LFSCCnfProof() {} - virtual void printClauses(std::ostream& os, std::ostream& paren); + void printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren); + + void printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren); + void printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren); };/* class LFSCCnfProof */ } /* CVC4 namespace */ diff --git a/src/proof/proof.h b/src/proof/proof.h index ae4c940a0..d69cd6198 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Proof manager + ** \brief Proof macros ** - ** Proof manager + ** Proof macros **/ #include "cvc4_private.h" @@ -46,14 +46,25 @@ */ #ifdef CVC4_PROOF -# define PROOF(x) if(options::proof() || options::unsatCores()) { x; } -# define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL -# define PROOF_ON() (options::proof() || options::unsatCores()) +# define PROOF(x) if(CVC4::options::proof() || CVC4::options::unsatCores()) { x; } +# define NULLPROOF(x) (CVC4::options::proof() || CVC4::options::unsatCores()) ? x : NULL +# define PROOF_ON() (CVC4::options::proof() || CVC4::options::unsatCores()) +# define THEORY_PROOF(x) if(CVC4::options::proof()) { x; } +# define THEORY_NULLPROOF(x) CVC4::options::proof() ? x : NULL +# define THEORY_PROOF_ON() CVC4::options::proof() #else /* CVC4_PROOF */ # define PROOF(x) # define NULLPROOF(x) NULL # define PROOF_ON() false +# define THEORY_PROOF(x) +# define THEORY_NULLPROOF(x) NULL +# define THEORY_PROOF_ON() false #endif /* CVC4_PROOF */ +#ifdef CVC4_PROOF_STATS /* CVC4_PROOF_STATS */ +# define PSTATS(x) { x; } +#else +# define PSTATS(x) +#endif /* CVC4_PROOF_STATS */ #endif /* __CVC4__PROOF__PROOF_H */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 88d380c4f..0ae020090 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -15,13 +15,20 @@ ** \todo document this file **/ -#include "proof/proof_manager.h" - -#include "base/cvc4_assert.h" #include "context/context.h" + +#include "proof/proof_manager.h" #include "proof/cnf_proof.h" -#include "proof/sat_proof.h" #include "proof/theory_proof.h" +#include "proof/bitvector_proof.h" +#include "proof/proof_utils.h" +#include "proof/sat_proof_implementation.h" +#include "options/bv_options.h" + +#include "util/proof.h" +#include "util/hash.h" + +#include "base/cvc4_assert.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt_util/node_visitor.h" @@ -31,8 +38,7 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/valuation.h" -#include "util/hash.h" -#include "util/proof.h" + namespace CVC4 { @@ -46,17 +52,13 @@ ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), d_theoryProof(NULL), - d_inputClauses(), - d_theoryLemmas(), - d_theoryPropagations(), d_inputFormulas(), d_inputCoreFormulas(), d_outputCoreFormulas(), d_nextId(0), d_fullProof(NULL), d_format(format), - d_deps(), - d_assertion_counter(1) + d_deps() { } @@ -65,21 +67,6 @@ ProofManager::~ProofManager() { delete d_cnfProof; delete d_theoryProof; delete d_fullProof; - - for(IdToClause::iterator it = d_inputClauses.begin(); - it != d_inputClauses.end(); - ++it) { - delete it->second; - } - - for(OrderedIdToClause::iterator it = d_theoryLemmas.begin(); - it != d_theoryLemmas.end(); - ++it) { - delete it->second; - } - - // FIXME: memory leak because there are deleted theory lemmas that - // were not used in the SatProof } ProofManager* ProofManager::currentPM() { @@ -93,13 +80,13 @@ Proof* ProofManager::getProof(SmtEngine* smt) { Assert (currentPM()->d_format == LFSC); currentPM()->d_fullProof = new LFSCProof(smt, - (LFSCSatProof*)getSatProof(), + (LFSCCoreSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), - (LFSCTheoryProof*)getTheoryProof()); + (LFSCTheoryProofEngine*)getTheoryProofEngine()); return currentPM()->d_fullProof; } -SatProof* ProofManager::getSatProof() { +CoreSatProof* ProofManager::getSatProof() { Assert (currentPM()->d_satProof); return currentPM()->d_satProof; } @@ -109,48 +96,135 @@ CnfProof* ProofManager::getCnfProof() { return currentPM()->d_cnfProof; } -TheoryProof* ProofManager::getTheoryProof() { - //Assert (currentPM()->d_theoryProof); +TheoryProofEngine* ProofManager::getTheoryProofEngine() { + Assert (options::proof()); + Assert (currentPM()->d_theoryProof != NULL); return currentPM()->d_theoryProof; } +UFProof* ProofManager::getUfProof() { + Assert (options::proof()); + TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_UF); + return (UFProof*)pf; +} +BitVectorProof* ProofManager::getBitVectorProof() { + Assert (options::proof()); + TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); + return (BitVectorProof*)pf; +} + +ArrayProof* ProofManager::getArrayProof() { + Assert (options::proof()); + TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAY); + return (ArrayProof*)pf; +} + void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); - currentPM()->d_satProof = new LFSCSatProof(solver); + currentPM()->d_satProof = new LFSCCoreSatProof(solver, ""); } -void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { - Assert (currentPM()->d_cnfProof == NULL); - Assert (currentPM()->d_format == LFSC); - currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); +void ProofManager::initCnfProof(prop::CnfStream* cnfStream, + context::Context* ctx) { + ProofManager* pm = currentPM(); + Assert (pm->d_cnfProof == NULL); + Assert (pm->d_format == LFSC); + CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, ""); + pm->d_cnfProof = cnf; + Assert(pm-> d_satProof != NULL); + pm->d_satProof->setCnfProof(cnf); + + // true and false have to be setup in a special way + Node true_node = NodeManager::currentNM()->mkConst(true); + Node false_node = NodeManager::currentNM()->mkConst(false).notNode(); + + pm->d_cnfProof->pushCurrentAssertion(true_node); + pm->d_cnfProof->pushCurrentDefinition(true_node); + pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getTrueUnit()); + pm->d_cnfProof->popCurrentAssertion(); + pm->d_cnfProof->popCurrentDefinition(); + + pm->d_cnfProof->pushCurrentAssertion(false_node); + pm->d_cnfProof->pushCurrentDefinition(false_node); + pm->d_cnfProof->registerConvertedClause(pm->d_satProof->getFalseUnit()); + pm->d_cnfProof->popCurrentAssertion(); + pm->d_cnfProof->popCurrentDefinition(); + } -void ProofManager::initTheoryProof() { +void ProofManager::initTheoryProofEngine(SmtGlobals* globals) { Assert (currentPM()->d_theoryProof == NULL); Assert (currentPM()->d_format == LFSC); - currentPM()->d_theoryProof = new LFSCTheoryProof(); + currentPM()->d_theoryProof = new LFSCTheoryProofEngine(globals); +} + +std::string ProofManager::getInputClauseName(ClauseId id, + const std::string& prefix) { + return append(prefix+".pb", id); +} +std::string ProofManager::getLemmaClauseName(ClauseId id, + const std::string& prefix) { + return append(prefix+".lemc", id); } + std::string ProofManager::getLemmaName(ClauseId id, + const std::string& prefix) { + return append(prefix+"lem", id); +} + +std::string ProofManager::getLearntClauseName(ClauseId id, + const std::string& prefix) { + return append(prefix+".cl", id); +} +std::string ProofManager::getVarName(prop::SatVariable var, + const std::string& prefix) { + return append(prefix+".v", var); +} +std::string ProofManager::getAtomName(prop::SatVariable var, + const std::string& prefix) { + return append(prefix+".a", var); +} +std::string ProofManager::getLitName(prop::SatLiteral lit, + const std::string& prefix) { + return append(prefix+".l", lit.toInt()); +} + -std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); } -std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); } -std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); } -std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); } -std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); } -std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); } -std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); } +std::string ProofManager::getPreprocessedAssertionName(Node node, + const std::string& prefix) { + node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; + return append(prefix+".PA", node.getId()); +} +std::string ProofManager::getAssertionName(Node node, + const std::string& prefix) { + return append(prefix+".A", node.getId()); +} -std::string ProofManager::getAtomName(TNode atom) { +std::string ProofManager::getAtomName(TNode atom, + const std::string& prefix) { prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom); Assert(!lit.isNegated()); - return getAtomName(lit.getSatVariable()); + return getAtomName(lit.getSatVariable(), prefix); } -std::string ProofManager::getLitName(TNode lit) { - return getLitName(currentPM()->d_cnfProof->getLiteral(lit)); +std::string ProofManager::getLitName(TNode lit, + const std::string& prefix) { + return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); +} + +std::string ProofManager::sanitize(TNode var) { + Assert (var.isVar()); + std::string name = var.toString(); + std::replace(name.begin(), name.end(), ' ', '_'); + return name; } + void ProofManager::traceDeps(TNode n) { Debug("cores") << "trace deps " << n << std::endl; + if ((n.isConst() && n == NodeManager::currentNM()->mkConst(true)) || + (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst(false))) { + return; + } if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { // originating formula was in core set Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; @@ -171,45 +245,38 @@ void ProofManager::traceDeps(TNode n) { } } -void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { - /*for (unsigned i = 0; i < clause->size(); ++i) { - prop::SatLiteral lit = clause->operator[](i); - d_propVars.insert(lit.getSatVariable()); - }*/ - if (kind == INPUT) { - Debug("cores") << "; Add to inputClauses " << id << std::endl; - d_inputClauses.insert(std::make_pair(id, clause)); - Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end()); - Debug("cores") << "; core id is " << d_satProof->d_inputClauses[id] << std::endl; - if(d_satProof->d_inputClauses[id] == uint64_t(-1)) { - Debug("cores") << "; + constant unit (true or false)" << std::endl; - } else if(options::unsatCores()) { - Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff); - Debug("cores") << "; core input assertion from CnfStream is " << e << std::endl; - Debug("cores") << "; with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl; - // Invalid proof rules are currently used for parts of CVC4 that don't - // support proofs (these are e.g. unproven theory lemmas) or don't need - // proofs (e.g. split lemmas). We can ignore these safely when - // constructing unsat cores. - if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) != RULE_INVALID) { - // trace dependences back to actual assertions - traceDeps(Node::fromExpr(e)); - } +void ProofManager::traceUnsatCore() { + Assert (options::unsatCores()); + d_satProof->constructProof(); + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_satProof->collectClausesUsed(used_inputs, + used_lemmas); + IdToSatClause::const_iterator it = used_inputs.begin(); + for(; it != used_inputs.end(); ++it) { + Node node = d_cnfProof->getAssertionForClause(it->first); + ProofRule rule = d_cnfProof->getProofRule(node); + + Debug("cores") << "core input assertion " << node << std::endl; + Debug("cores") << "with proof rule " << rule << std::endl; + if (rule == RULE_TSEITIN || + rule == RULE_GIVEN) { + // trace dependences back to actual assertions + // (this adds them to the unsat core) + traceDeps(node); } - } else { - Assert(kind == THEORY_LEMMA); - d_theoryLemmas.insert(std::make_pair(id, clause)); } } -void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { - Debug("cores") << "assert: " << formula << std::endl; +void ProofManager::addAssertion(Expr formula) { + Debug("proof:pm") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); +} + +void ProofManager::addCoreAssertion(Expr formula) { + Debug("cores") << "assert: " << formula << std::endl; d_deps[Node::fromExpr(formula)]; // empty vector of deps - if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) { - Debug("cores") << "adding to input core forms: " << formula << std::endl; - d_inputCoreFormulas.insert(formula); - } + d_inputCoreFormulas.insert(formula); } void ProofManager::addDependence(TNode n, TNode dep) { @@ -232,151 +299,210 @@ void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } -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(); - } -} +LFSCProof::LFSCProof(SmtEngine* smtEngine, + LFSCCoreSatProof* sat, + LFSCCnfProof* cnf, + LFSCTheoryProofEngine* theory) + : d_satProof(sat) + , d_cnfProof(cnf) + , d_theoryProof(theory) + , d_smtEngine(smtEngine) +{} -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 LFSCProof::toStream(std::ostream& out) { + d_satProof->constructProof(); -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; + // collecting leaf clauses in resolution proof + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_satProof->collectClausesUsed(used_inputs, + used_lemmas); + + // collecting assertions that lead to the clauses being asserted + NodeSet used_assertions; + d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions); + + NodeSet atoms; + // collects the atoms in the clauses + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); + d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); + + // collects the atoms in the assertions + for (NodeSet::const_iterator it = used_assertions.begin(); + it != used_assertions.end(); ++it) { + utils::collectAtoms(*it, atoms); } -} -void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) { - Trace("cnf-pf-debug") << "; set registering formula " << n << " proof rule = " << proof_id << std::endl; - d_registering_assertion = n; - d_registering_rule = proof_id; -} + if (Debug.isOn("proof:pm")) { + // std::cout << NodeManager::currentNM(); + Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; + for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { + Debug("proof:pm") << " " << *it << std::endl; + } -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 ); + Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; + for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { + Debug("proof:pm") << " " << *it << std::endl; + } } -} -LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) - : d_satProof(sat) - , d_cnfProof(cnf) - , d_theoryProof(theory) - , d_smtEngine(smtEngine) -{ - d_satProof->constructProof(); -} -void LFSCProof::toStream(std::ostream& out) { + smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; out << " ;; Declarations\n"; - if (d_theoryProof == NULL) { - d_theoryProof = new LFSCTheoryProof(); + + // declare the theory atoms + NodeSet::const_iterator it = atoms.begin(); + NodeSet::const_iterator end = atoms.end(); + for(; it != end; ++it) { + d_theoryProof->registerTerm((*it).toExpr()); } - /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping(); - i != d_cnfProof->end_atom_mapping(); - ++i) { - d_theoryProof->addDeclaration(*i); - }*/ + // print out all the original assertions d_theoryProof->printAssertions(out, paren); - out << " ;; Proof of empty clause follows\n"; + + out << "(: (holds cln)\n"; - d_cnfProof->printClauses(out, paren); - d_satProof->printResolutions(out, paren); - paren <<")))\n;;"; - out << paren.str(); - out << "\n"; + + // print trust that input assertions are their preprocessed form + printPreprocessedAssertions(used_assertions, out, paren); + + // print mapping between theory atoms and internal SAT variables + d_cnfProof->printAtomMapping(atoms, out, paren); + + IdToSatClause::const_iterator cl_it = used_inputs.begin(); + // print CNF conversion proof for each clause + for (; cl_it != used_inputs.end(); ++cl_it) { + d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren); + } + + // FIXME: for now assume all theory lemmas are in CNF form so + // distinguish between them and inputs + // print theory lemmas for resolution proof + d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); + + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { + // print actual resolution proof + // d_satProof->printResolutions(out, paren); + ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren); + paren <<")))\n;;"; + out << paren.str(); + out << "\n"; + } else { + // print actual resolution proof + d_satProof->printResolutions(out, paren); + d_satProof->printResolutionEmptyClause(out, paren); + paren <<")))\n;;"; + out << paren.str(); + out << "\n"; + } +} + +void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, + std::ostream& os, + std::ostream& paren) { + os << " ;; Preprocessing \n"; + NodeSet::const_iterator it = assertions.begin(); + NodeSet::const_iterator end = assertions.end(); + + for (; it != end; ++it) { + os << "(th_let_pf _ "; + + //TODO + os << "(trust_f "; + ProofManager::currentPM()->getTheoryProofEngine()->printLetTerm((*it).toExpr(), os); + os << ") "; + + os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; + paren << "))"; + + } } + + +//---from Morgan--- +bool ProofManager::hasOp(TNode n) const { + return d_bops.find(n) != d_bops.end(); +} + +Node ProofManager::lookupOp(TNode n) const { + std::map::const_iterator i = d_bops.find(n); + Assert(i != d_bops.end()); + return (*i).second; +} + +Node ProofManager::mkOp(TNode n) { + if(n.getKind() != kind::BUILTIN) { + return n; + } + Node& op = d_ops[n]; + if(op.isNull()) { + Debug("mgd") << "making an op for " << n << "\n"; + std::stringstream ss; + ss << n; + std::string s = ss.str(); + Debug("mgd") << " : " << s << std::endl; + std::vector v; + v.push_back(NodeManager::currentNM()->integerType()); + if(n.getConst() == kind::SELECT) { + v.push_back(NodeManager::currentNM()->integerType()); + v.push_back(NodeManager::currentNM()->integerType()); + } else if(n.getConst() == kind::STORE) { + v.push_back(NodeManager::currentNM()->integerType()); + v.push_back(NodeManager::currentNM()->integerType()); + v.push_back(NodeManager::currentNM()->integerType()); + } + TypeNode type = NodeManager::currentNM()->mkFunctionType(v); + op = NodeManager::currentNM()->mkSkolem(s, type, " ignore", NodeManager::SKOLEM_NO_NOTIFY); + d_bops[op] = n; + } + return op; +} +//---end from Morgan--- + +std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { + switch(k) { + case RULE_GIVEN: + out << "RULE_GIVEN"; + break; + case RULE_DERIVED: + out << "RULE_DERIVED"; + break; + case RULE_RECONSTRUCT: + out << "RULE_RECONSTRUCT"; + break; + case RULE_TRUST: + out << "RULE_TRUST"; + break; + case RULE_INVALID: + out << "RULE_INVALID"; + break; + case RULE_CONFLICT: + out << "RULE_CONFLICT"; + break; + case RULE_TSEITIN: + out << "RULE_TSEITIN"; + break; + case RULE_SPLIT: + out << "RULE_SPLIT"; + break; + case RULE_ARRAYS_EXT: + out << "RULE_ARRAYS"; + break; + case RULE_ARRAYS_ROW: + out << "RULE_ARRAYS"; + break; + default: + out << "ProofRule Unknown! [" << unsigned(k) << "]"; + } + + return out; +} + + } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 6864eca3d..5d8bf3d58 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -31,27 +31,52 @@ namespace CVC4 { +class SmtGlobals; + // forward declarations namespace Minisat { class Solver; }/* Minisat namespace */ +namespace BVMinisat { + class Solver; +}/* BVMinisat namespace */ + namespace prop { class CnfStream; }/* CVC4::prop namespace */ class SmtEngine; -typedef int ClauseId; +typedef unsigned ClauseId; +const ClauseId ClauseIdEmpty(-1); +const ClauseId ClauseIdUndef(-2); +const ClauseId ClauseIdError(-3); class Proof; -class SatProof; +template class TSatProof; +typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof; + class CnfProof; +class RewriterProof; +class TheoryProofEngine; class TheoryProof; +class UFProof; +class ArrayProof; +class BitVectorProof; + +template class LFSCSatProof; +typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof; -class LFSCSatProof; class LFSCCnfProof; -class LFSCTheoryProof; +class LFSCTheoryProofEngine; +class LFSCUFProof; +class LFSCBitVectorProof; +class LFSCRewriterProof; + +template class ProofProxy; +typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy; +typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy; namespace prop { typedef uint64_t SatVariable; @@ -67,18 +92,13 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); -typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; -typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause; -typedef __gnu_cxx::hash_set VarSet; +typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; typedef __gnu_cxx::hash_set ExprSet; +typedef __gnu_cxx::hash_set NodeSet; +typedef __gnu_cxx::hash_map, NodeHashFunction > NodeToNodes; +typedef std::hash_set IdHashSet; -typedef int ClauseId; - -enum ClauseKind { - INPUT, - THEORY_LEMMA, - LEARNT -};/* enum ClauseKind */ +typedef unsigned ClauseId; enum ProofRule { RULE_GIVEN, /* input assertion */ @@ -88,44 +108,31 @@ enum ProofRule { 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_SPLIT, /* A splitting lemma of the form a v ~ a*/ + 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; + CoreSatProof* d_satProof; + CnfProof* d_cnfProof; + TheoryProofEngine* d_theoryProof; // information that will need to be shared across proofs - IdToClause d_inputClauses; - OrderedIdToClause d_theoryLemmas; - IdToClause d_theoryPropagations; ExprSet d_inputFormulas; ExprSet d_inputCoreFormulas; ExprSet d_outputCoreFormulas; - //VarSet d_propVars; int d_nextId; Proof* d_fullProof; ProofFormat d_format; // used for now only in debug builds - __gnu_cxx::hash_map< Node, std::vector, NodeHashFunction > d_deps; - + NodeToNodes d_deps; // 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; @@ -137,93 +144,100 @@ public: // initialization static void initSatProof(Minisat::Solver* solver); - static void initCnfProof(CVC4::prop::CnfStream* cnfStream); - static void initTheoryProof(); - - static Proof* getProof(SmtEngine* smt); - static SatProof* getSatProof(); - static CnfProof* getCnfProof(); - static TheoryProof* getTheoryProof(); - + static void initCnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx); + static void initTheoryProofEngine(SmtGlobals* globals); + + // getting various proofs + static Proof* getProof(SmtEngine* smt); + static CoreSatProof* getSatProof(); + static CnfProof* getCnfProof(); + static TheoryProofEngine* getTheoryProofEngine(); + static TheoryProof* getTheoryProof( theory::TheoryId id ); + static UFProof* getUfProof(); + static BitVectorProof* getBitVectorProof(); + static ArrayProof* getArrayProof(); + // iterators over data shared by proofs - typedef IdToClause::const_iterator clause_iterator; - typedef OrderedIdToClause::const_iterator ordered_clause_iterator; 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(); } - - ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } - ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } - size_t num_lemmas() const { return d_theoryLemmas.size(); } + // iterate over the assertions (these are arbitrary boolean formulas) assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); } assertions_iterator end_assertions() const { return d_inputFormulas.end(); } size_t num_assertions() const { return d_inputFormulas.size(); } + +//---from Morgan--- + Node mkOp(TNode n); + Node lookupOp(TNode n) const; + bool hasOp(TNode n) const; + + std::map d_ops; + std::map d_bops; +//---end from Morgan--- + + + // variable prefixes + static std::string getInputClauseName(ClauseId id, const std::string& prefix = ""); + static std::string getLemmaClauseName(ClauseId id, const std::string& prefix = ""); + static std::string getLemmaName(ClauseId id, const std::string& prefix = ""); + static std::string getLearntClauseName(ClauseId id, const std::string& prefix = ""); + static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = ""); + static std::string getAssertionName(Node node, const std::string& prefix = ""); + + static std::string getVarName(prop::SatVariable var, const std::string& prefix = ""); + static std::string getAtomName(prop::SatVariable var, const std::string& prefix = ""); + static std::string getAtomName(TNode atom, const std::string& prefix = ""); + static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = ""); + static std::string getLitName(TNode lit, const std::string& prefix = ""); + + // for SMT variable names that have spaces and other things + static std::string sanitize(TNode var); + - void printProof(std::ostream& os, TNode n); - - void addAssertion(Expr formula, bool inUnsatCore); - void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); - // note that n depends on dep (for cores) + /** Add proof assertion - unlinke addCoreAssertion this is post definition expansion **/ + void addAssertion(Expr formula); + + /** Public unsat core methods **/ + void addCoreAssertion(Expr formula); + void addDependence(TNode n, TNode dep); void addUnsatCore(Expr formula); + void traceUnsatCore(); assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } size_t size_unsat_core() const { return d_outputCoreFormulas.size(); } int nextId() { return d_nextId++; } - // variable prefixes - static std::string getInputClauseName(ClauseId id); - static std::string getLemmaName(ClauseId id); - static std::string getLemmaClauseName(ClauseId id); - static std::string getLearntClauseName(ClauseId id); - - static std::string getVarName(prop::SatVariable var); - static std::string getAtomName(prop::SatVariable var); - static std::string getAtomName(TNode atom); - static std::string getLitName(prop::SatLiteral lit); - static std::string getLitName(TNode lit); - void setLogic(const LogicInfo& logic); const std::string getLogic() const { return d_logic.getLogicString(); } + LogicInfo & getLogicInfo() { return d_logic; } - - 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 { - LFSCSatProof* d_satProof; + LFSCCoreSatProof* d_satProof; LFSCCnfProof* d_cnfProof; - LFSCTheoryProof* d_theoryProof; + LFSCTheoryProofEngine* d_theoryProof; SmtEngine* d_smtEngine; + + // FIXME: hack until we get preprocessing + void printPreprocessedAssertions(const NodeSet& assertions, + std::ostream& os, + std::ostream& paren); public: - LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + LFSCProof(SmtEngine* smtEngine, + LFSCCoreSatProof* sat, + LFSCCnfProof* cnf, + LFSCTheoryProofEngine* theory); virtual void toStream(std::ostream& out); virtual ~LFSCProof() {} };/* class LFSCProof */ +std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k); }/* CVC4 namespace */ + + #endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp new file mode 100644 index 000000000..47b8a235e --- /dev/null +++ b/src/proof/proof_utils.cpp @@ -0,0 +1,127 @@ +/********************* */ +/*! \file proof_utils.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** 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 +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "proof/proof_utils.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace utils { + +void collectAtoms(TNode node, CVC4::NodeSet& seen) { + if (seen.find(node) != seen.end()) + return; + if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) { + seen.insert(node); + return; + } + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + collectAtoms(node[i], seen); + } +} + +std::string toLFSCKind(Kind kind) { + switch(kind) { + // core kinds + case kind::OR : return "or"; + case kind::AND: return "and"; + case kind::XOR: return "xor"; + case kind::EQUAL: return "="; + case kind::IFF: return "iff"; + case kind::IMPLIES: return "impl"; + case kind::NOT: return "not"; + + // bit-vector kinds + case kind::BITVECTOR_AND : + return "bvand"; + case kind::BITVECTOR_OR : + return "bvor"; + case kind::BITVECTOR_XOR : + return "bvxor"; + case kind::BITVECTOR_NAND : + return "bvnand"; + case kind::BITVECTOR_NOR : + return "bvnor"; + case kind::BITVECTOR_XNOR : + return "bvxnor"; + case kind::BITVECTOR_COMP : + return "bvcomp"; + case kind::BITVECTOR_MULT : + return "bvmul"; + case kind::BITVECTOR_PLUS : + return "bvadd"; + case kind::BITVECTOR_SUB : + return "bvsub"; + case kind::BITVECTOR_UDIV : + case kind::BITVECTOR_UDIV_TOTAL : + return "bvudiv"; + case kind::BITVECTOR_UREM : + case kind::BITVECTOR_UREM_TOTAL : + return "bvurem"; + case kind::BITVECTOR_SDIV : + return "bvsdiv"; + case kind::BITVECTOR_SREM : + return "bvsrem"; + case kind::BITVECTOR_SMOD : + return "bvsmod"; + case kind::BITVECTOR_SHL : + return "bvshl"; + case kind::BITVECTOR_LSHR : + return "bvlshr"; + case kind::BITVECTOR_ASHR : + return "bvashr"; + case kind::BITVECTOR_CONCAT : + return "concat"; + case kind::BITVECTOR_NEG : + return "bvneg"; + case kind::BITVECTOR_NOT : + return "bvnot"; + case kind::BITVECTOR_ROTATE_LEFT : + return "rotate_left"; + case kind::BITVECTOR_ROTATE_RIGHT : + return "rotate_right"; + case kind::BITVECTOR_ULT : + return "bvult"; + case kind::BITVECTOR_ULE : + return "bvule"; + case kind::BITVECTOR_UGT : + return "bvugt"; + case kind::BITVECTOR_UGE : + return "bvuge"; + case kind::BITVECTOR_SLT : + return "bvslt"; + case kind::BITVECTOR_SLE : + return "bvsle"; + case kind::BITVECTOR_SGT : + return "bvsgt"; + case kind::BITVECTOR_SGE : + return "bvsge"; + case kind::BITVECTOR_EXTRACT : + return "extract"; + case kind::BITVECTOR_REPEAT : + return "repeat"; + case kind::BITVECTOR_ZERO_EXTEND : + return "zero_extend"; + case kind::BITVECTOR_SIGN_EXTEND : + return "sign_extend"; + default: + Unreachable(); + } +} + +} /* namespace CVC4::utils */ +} /* namespace CVC4 */ diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h new file mode 100644 index 000000000..c27fbe5c2 --- /dev/null +++ b/src/proof/proof_utils.h @@ -0,0 +1,178 @@ +/********************* */ +/*! \file proof_utils.h +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** 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 +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "cvc4_private.h" + +#pragma once + +#include +#include +#include +#include "expr/node_manager.h" + +namespace CVC4 { + +typedef __gnu_cxx::hash_set ExprSet; +typedef __gnu_cxx::hash_set NodeSet; + +namespace utils { + +std::string toLFSCKind(Kind kind); + +inline unsigned getExtractHigh(Expr node) { + return node.getOperator().getConst().high; +} + +inline unsigned getExtractLow(Expr node) { + return node.getOperator().getConst().low; +} + +inline unsigned getSize(Type type) { + BitVectorType bv(type); + return bv.getSize(); +} + + +inline unsigned getSize(Expr node) { + Assert (node.getType().isBitVector()); + return getSize(node.getType()); +} + +inline Expr mkTrue() { + return NodeManager::currentNM()->toExprManager()->mkConst(true); +} + +inline Expr mkFalse() { + return NodeManager::currentNM()->toExprManager()->mkConst(false); +} +inline BitVector mkBitVectorOnes(unsigned size) { + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); +} + +inline Expr mkExpr(Kind k , Expr expr) { + return NodeManager::currentNM()->toExprManager()->mkExpr(k, expr); +} +inline Expr mkExpr(Kind k , Expr e1, Expr e2) { + return NodeManager::currentNM()->toExprManager()->mkExpr(k, e1, e2); +} +inline Expr mkExpr(Kind k , std::vector& children) { + return NodeManager::currentNM()->toExprManager()->mkExpr(k, children); +} + + +inline Expr mkOnes(unsigned size) { + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->toExprManager()->mkConst(val); +} + +inline Expr mkConst(unsigned size, unsigned int value) { + BitVector val(size, value); + return NodeManager::currentNM()->toExprManager()->mkConst(val); +} + +inline Expr mkConst(const BitVector& value) { + return NodeManager::currentNM()->toExprManager()->mkConst(value); +} + +inline Expr mkOr(const std::vector& nodes) { + std::set all; + all.insert(nodes.begin(), nodes.end()); + Assert(all.size() != 0 ); + + if (all.size() == 1) { + // All the same, or just one + return nodes[0]; + } + + + NodeBuilder<> disjunction(kind::OR); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << Node::fromExpr(*it); + ++ it; + } + + Node res = disjunction; + return res.toExpr(); +}/* mkOr() */ + + +inline Expr mkAnd(const std::vector& conjunctions) { + std::set all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << Node::fromExpr(*it); + ++ it; + } + + Node res = conjunction; + return res.toExpr(); +}/* mkAnd() */ + +inline Expr mkSortedExpr(Kind kind, const std::vector& children) { + std::set all; + all.insert(children.begin(), children.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return children[0]; + } + + + NodeBuilder<> res(kind); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + res << Node::fromExpr(*it); + ++ it; + } + + return ((Node)res).toExpr(); +}/* mkSortedNode() */ + +inline const bool getBit(Expr expr, unsigned i) { + Assert (i < utils::getSize(expr) && + expr.isConst()); + Integer bit = expr.getConst().extract(i, i).getValue(); + return (bit == 1u); +} + +void collectAtoms(TNode node, NodeSet& seen); + + +} +} diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 52319431c..95a4c8907 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -20,63 +20,63 @@ #define __CVC4__SAT__PROOF_H #include - #include #include #include #include #include #include - #include "expr/expr.h" #include "proof/proof_manager.h" +#include "util/proof.h" +#include "util/statistics_registry.h" + namespace CVC4 { -namespace Minisat { - class Solver; - typedef uint32_t CRef; -}/* Minisat namespace */ -} -#include "prop/minisat/core/SolverTypes.h" -#include "util/proof.h" -#include "prop/sat_solver_types.h" -namespace std { - using namespace __gnu_cxx; -}/* std namespace */ -namespace CVC4 { +class CnfProof; /** * Helper debugging functions */ -void printDebug(Minisat::Lit l); -void printDebug(Minisat::Clause& c); +template void printDebug(typename Solver::TLit l); +template void printDebug(typename Solver::TClause& c); + +enum ClauseKind { + INPUT, + THEORY_LEMMA, // we need to distinguish because we must reprove deleted theory lemmas + LEARNT +};/* enum ClauseKind */ + +template struct ResStep { - Minisat::Lit lit; + typename Solver::TLit lit; ClauseId id; bool sign; - ResStep(Minisat::Lit l, ClauseId i, bool s) : + ResStep(typename Solver::TLit l, ClauseId i, bool s) : lit(l), id(i), sign(s) {} };/* struct ResStep */ -typedef std::vector< ResStep > ResSteps; -typedef std::set < Minisat::Lit> LitSet; - +template class ResChain { +public: + typedef std::vector< ResStep > ResSteps; + typedef std::set < typename Solver::TLit> LitSet; + private: ClauseId d_start; ResSteps d_steps; LitSet* d_redundantLits; public: ResChain(ClauseId start); - void addStep(Minisat::Lit, ClauseId, bool); + void addStep(typename Solver::TLit, ClauseId, bool); bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } - void addRedundantLit(Minisat::Lit lit); + void addRedundantLit(typename Solver::TLit lit); ~ResChain(); // accessor methods ClauseId getStart() { return d_start; } @@ -84,35 +84,31 @@ public: LitSet* getRedundant() { return d_redundantLits; } };/* class ResChain */ -typedef std::hash_map < ClauseId, Minisat::CRef > IdCRefMap; -typedef std::hash_map < Minisat::CRef, ClauseId > ClauseIdMap; -typedef std::hash_map < ClauseId, Minisat::Lit> IdUnitMap; -typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME -typedef std::hash_map < ClauseId, ResChain*> IdResMap; -typedef std::hash_set < ClauseId > IdHashSet; -typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; -typedef std::vector < ResChain* > ResStack; -typedef std::hash_map IdToSatClause; -typedef std::set < ClauseId > IdSet; -typedef std::vector < Minisat::Lit > LitVector; -typedef __gnu_cxx::hash_map IdToMinisatClause; - -class SatProof; - -class ProofProxy : public ProofProxyAbstract { -private: - SatProof* d_proof; -public: - ProofProxy(SatProof* pf); - void updateCRef(Minisat::CRef oldref, Minisat::CRef newref); -};/* class ProofProxy */ - +template class ProofProxy; class CnfProof; -class SatProof { +template +class TSatProof { protected: - Minisat::Solver* d_solver; + typedef std::set < typename Solver::TLit> LitSet; + typedef std::set < typename Solver::TVar> VarSet; + typedef std::hash_map < ClauseId, typename Solver::TCRef > IdCRefMap; + typedef std::hash_map < typename Solver::TCRef, ClauseId > ClauseIdMap; + typedef std::hash_map < ClauseId, typename Solver::TLit> IdUnitMap; + typedef std::hash_map < int, ClauseId> UnitIdMap; + typedef std::hash_map < ClauseId, ResChain* > IdResMap; + typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; + typedef std::vector < ResChain* > ResStack; + //typedef std::hash_map IdToSatClause; + typedef std::set < ClauseId > IdSet; + typedef std::vector < typename Solver::TLit > LitVector; + typedef __gnu_cxx::hash_map IdToMinisatClause; + typedef __gnu_cxx::hash_map IdToConflicts; + + typename Solver::Solver* d_solver; + CnfProof* d_cnfProof; + // clauses IdCRefMap d_idClause; ClauseIdMap d_clauseId; @@ -120,10 +116,14 @@ protected: UnitIdMap d_unitId; IdHashSet d_deleted; IdToSatClause d_deletedTheoryLemmas; -public: - IdProofRuleMap d_inputClauses; - IdProofRuleMap d_lemmaClauses; + protected: + IdHashSet d_inputClauses; + IdHashSet d_lemmaClauses; + VarSet d_assumptions; // assumption literals for bv solver + IdHashSet d_assumptionConflicts; // assumption conflicts not actually added to SAT solver + IdToConflicts d_assumptionConflictsDebug; + // resolutions IdResMap d_resChains; ResStack d_resStack; @@ -132,38 +132,45 @@ protected: const ClauseId d_emptyClauseId; const ClauseId d_nullId; // proxy class to break circular dependencies - ProofProxy* d_proxy; + ProofProxy* d_proxy; // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdCRefMap d_temp_idClause; + IdCRefMap d_temp_idClause; // unit conflict ClauseId d_unitConflictId; bool d_storedUnitConflict; + + ClauseId d_trueLit; + ClauseId d_falseLit; + + std::string d_name; public: - SatProof(Minisat::Solver* solver, bool checkRes = false); - virtual ~SatProof(); + TSatProof(Solver* solver, const std::string& name, bool checkRes = false); + virtual ~TSatProof(); + void setCnfProof(CnfProof* cnf_proof); protected: void print(ClauseId id); void printRes(ClauseId id); - void printRes(ResChain* res); + void printRes(ResChain* res); bool isInputClause(ClauseId id); - bool isTheoryConflict(ClauseId id); bool isLemmaClause(ClauseId id); + bool isAssumptionConflict(ClauseId id); bool isUnit(ClauseId id); - bool isUnit(Minisat::Lit lit); + bool isUnit(typename Solver::TLit lit); bool hasResolution(ClauseId id); void createLitSet(ClauseId id, LitSet& set); - void registerResolution(ClauseId id, ResChain* res); - - ClauseId getClauseId(Minisat::CRef clause); - ClauseId getClauseId(Minisat::Lit lit); - Minisat::CRef getClauseRef(ClauseId id); - Minisat::Lit getUnit(ClauseId id); - ClauseId getUnitId(Minisat::Lit lit); - Minisat::Clause& getClause(Minisat::CRef ref); + void registerResolution(ClauseId id, ResChain* res); + + ClauseId getClauseId(typename Solver::TCRef clause); + ClauseId getClauseId(typename Solver::TLit lit); + typename Solver::TCRef getClauseRef(ClauseId id); + typename Solver::TLit getUnit(ClauseId id); + ClauseId getUnitId(typename Solver::TLit lit); + typename Solver::TClause& getClause(typename Solver::TCRef ref); + void getLitVec(ClauseId id, LitVector& vec); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); @@ -174,7 +181,7 @@ protected: * * @return */ - ClauseId resolveUnit(Minisat::Lit lit); + ClauseId resolveUnit(typename Solver::TLit lit); /** * Does a depth first search on removed literals and adds the literals * to be removed in the proper order to the stack. @@ -183,27 +190,35 @@ protected: * @param removedSet the previously computed set of redundant literals * @param removeStack the stack of literals in reverse order of resolution */ - void removedDfs(Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); - void removeRedundantFromRes(ResChain* res, ClauseId id); + void removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); + void removeRedundantFromRes(ResChain* res, ClauseId id); public: - void startResChain(Minisat::CRef start); - void addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign); + void startResChain(typename Solver::TLit start); + void startResChain(typename Solver::TCRef start); + void addResolutionStep(typename Solver::TLit lit, typename Solver::TCRef clause, bool sign); /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter * @param clause the clause the resolution is proving */ - void endResChain(Minisat::CRef clause); - void endResChain(Minisat::Lit lit); + //void endResChain(typename Solver::TCRef clause); + void endResChain(typename Solver::TLit lit); + void endResChain(ClauseId id); + /** + * Pops the current resolution of the stack *without* storing it. + * + */ + void cancelResChain(); + /** * Stores in the current derivation the redundant literals that were * eliminated from the conflict clause during conflict clause minimization. * @param lit the eliminated literal */ - void storeLitRedundant(Minisat::Lit lit); + void storeLitRedundant(typename Solver::TLit lit); /// update the CRef Id maps when Minisat does memory reallocation x - void updateCRef(Minisat::CRef old_ref, Minisat::CRef new_ref); + void updateCRef(typename Solver::TCRef old_ref, typename Solver::TCRef new_ref); void finishUpdateCRef(); /** @@ -211,66 +226,142 @@ public: * * @param conflict */ - void finalizeProof(Minisat::CRef conflict); + void finalizeProof(typename Solver::TCRef conflict); /// clause registration methods - ClauseId registerClause(const Minisat::CRef clause, ClauseKind kind, uint64_t proof_id); - ClauseId registerUnitClause(const Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); - - void storeUnitConflict(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); + ClauseId registerClause(const typename Solver::TCRef clause, + ClauseKind kind); + ClauseId registerUnitClause(const typename Solver::TLit lit, + ClauseKind kind); + void registerTrueLit(const typename Solver::TLit lit); + void registerFalseLit(const typename Solver::TLit lit); + + ClauseId getTrueUnit() const; + ClauseId getFalseUnit() const; + + + void registerAssumption(const typename Solver::TVar var); + ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); + + ClauseId storeUnitConflict(typename Solver::TLit lit, + ClauseKind kind); + /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. * @param clause */ - void markDeleted(Minisat::CRef clause); + void markDeleted(typename Solver::TCRef clause); bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause * @param q the literal to be resolved out */ - void resolveOutUnit(Minisat::Lit q); + void resolveOutUnit(typename Solver::TLit q); /** * Constructs the resolution of the literal lit. Called when a clause * containing lit becomes satisfied and is removed. * @param lit */ - void storeUnitResolution(Minisat::Lit lit); - - ProofProxy* getProxy() {return d_proxy; } + void storeUnitResolution(typename Solver::TLit lit); + ProofProxy* getProxy() {return d_proxy; } /** - Constructs the SAT proof identifying the needed lemmas + * Constructs the SAT proof for the given clause, + * by collecting the needed clauses in the d_seen + * data-structures, also notifying the proofmanager. */ - void constructProof(); - + void constructProof(ClauseId id); + void constructProof() { + constructProof(d_emptyClauseId); + } + void collectClauses(ClauseId id); + prop::SatClause* buildClause(ClauseId id); protected: - IdSet d_seenLearnt; - IdHashSet d_seenInput; - IdHashSet d_seenTheoryConflicts; - IdHashSet d_seenLemmas; + IdSet d_seenLearnt; + IdToSatClause d_seenInputs; + IdToSatClause d_seenLemmas; + + std::string varName(typename Solver::TLit lit); + std::string clauseName(ClauseId id); - inline std::string varName(Minisat::Lit lit); - inline std::string clauseName(ClauseId id); - void collectClauses(ClauseId id); void addToProofManager(ClauseId id, ClauseKind kind); + void addToCnfProof(ClauseId id); public: + virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; -};/* class SatProof */ + virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren) = 0; + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) = 0; + -class LFSCSatProof : public SatProof { + void collectClausesUsed(IdToSatClause& inputs, + IdToSatClause& lemmas); + + void storeClauseGlue(ClauseId clause, int glue); + +private: + __gnu_cxx::hash_map d_glueMap; + struct Statistics { + IntStat d_numLearnedClauses; + IntStat d_numLearnedInProof; + IntStat d_numLemmasInProof; + AverageStat d_avgChainLength; + HistogramStat d_resChainLengths; + HistogramStat d_usedResChainLengths; + HistogramStat d_clauseGlue; + HistogramStat d_usedClauseGlue; + Statistics(const std::string& name); + ~Statistics(); + }; + + Statistics d_statistics; +};/* class TSatProof */ + + +template +class ProofProxy { private: - void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); + TSatProof* d_proof; public: - LFSCSatProof(Minisat::Solver* solver, bool checkRes = false) - : SatProof(solver, checkRes) + ProofProxy(TSatProof* pf); + void updateCRef(typename S::TCRef oldref, typename S::TCRef newref); +};/* class ProofProxy */ + + +template +class LFSCSatProof : public TSatProof { +private: + +public: + LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false) + : TSatProof(solver, name, checkRes) {} + virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); virtual void printResolutions(std::ostream& out, std::ostream& paren); + virtual void printResolutionEmptyClause(std::ostream& out, std::ostream& paren); + virtual void printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren); };/* class LFSCSatProof */ + + +template +prop::SatLiteral toSatLiteral(typename Solver::TLit lit); + + +/** +* Convert from minisat clause to SatClause +* +* @param minisat_cl +* @param sat_cl +*/ +template +void toSatClause(const typename Solver::TClause& minisat_cl, + prop::SatClause& sat_cl); + + }/* CVC4 namespace */ #endif /* __CVC4__SAT__PROOF_H */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h new file mode 100644 index 000000000..92645e105 --- /dev/null +++ b/src/proof/sat_proof_implementation.h @@ -0,0 +1,1100 @@ +/********************* */ +/*! \file sat_proof_implementation.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: Morgan Deters + ** 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 + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Resolution proof + ** + ** Resolution proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H +#define __CVC4__SAT__PROOF_IMPLEMENTATION_H + +#include "proof/sat_proof.h" +#include "proof/cnf_proof.h" +#include "prop/minisat/minisat.h" +#include "prop/bvminisat/bvminisat.h" +#include "prop/minisat/core/Solver.h" +#include "prop/bvminisat/core/Solver.h" +#include "prop/sat_solver_types.h" +#include "smt/smt_statistics_registry.h" + +namespace CVC4 { + +template +void printLit (typename Solver::TLit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; +} + +template +void printClause (typename Solver::TClause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } +} + +template +void printClause (std::vector& c) { + for (unsigned i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } +} + + +template +void printLitSet(const std::set& s) { + typename std::set < typename Solver::TLit>::const_iterator it = s.begin(); + for(; it != s.end(); ++it) { + printLit(*it); + Debug("proof:sat") << " "; + } + Debug("proof:sat") << std::endl; +} + +// purely debugging functions +template +void printDebug (typename Solver::TLit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; +} +template +void printDebug (typename Solver::TClause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } + Debug("proof:sat") << std::endl; +} + + +/** + * Converts the clause associated to id to a set of literals + * + * @param id the clause id + * @param set the clause converted to a set of literals + */ +template +void TSatProof::createLitSet(ClauseId id, LitSet& set) { + Assert(set.empty()); + if(isUnit(id)) { + set.insert(getUnit(id)); + return; + } + if ( id == d_emptyClauseId) { + return; + } + // if it's an assumption + if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) { + LitVector* clause = d_assumptionConflictsDebug[id]; + for (unsigned i = 0; i < clause->size(); ++i) { + set.insert(clause->operator[](i)); + } + return; + } + + typename Solver::TCRef ref = getClauseRef(id); + typename Solver::TClause& c = getClause(ref); + for (int i = 0; i < c.size(); i++) { + set.insert(c[i]); + } +} + + +/** + * Resolves clause1 and clause2 on variable var and stores the + * result in clause1 + * @param v + * @param clause1 + * @param clause2 + */ +template +bool resolve(const typename Solver::TLit v, + std::set& clause1, + std::set& clause2, bool s) { + Assert(!clause1.empty()); + Assert(!clause2.empty()); + typename Solver::TLit var = sign(v) ? ~v : v; + if (s) { + // literal appears positive in the first clause + if( !clause2.count(~var)) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << std::endl; + } + return false; + } + clause1.erase(var); + clause2.erase(~var); + typename std::set::iterator it = clause2.begin(); + for (; it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } else { + // literal appears negative in the first clause + if( !clause1.count(~var) || !clause2.count(var)) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit(var); + Debug("proof:sat") << std::endl; + } + return false; + } + clause1.erase(~var); + clause2.erase(var); + typename std::set::iterator it = clause2.begin(); + for (; it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } + return true; +} + +/// ResChain +template +ResChain::ResChain(ClauseId start) : + d_start(start), + d_steps(), + d_redundantLits(NULL) + {} +template +void ResChain::addStep(typename Solver::TLit lit, ClauseId id, bool sign) { + ResStep step(lit, id, sign); + d_steps.push_back(step); +} + +template +void ResChain::addRedundantLit(typename Solver::TLit lit) { + if (d_redundantLits) { + d_redundantLits->insert(lit); + } else { + d_redundantLits = new LitSet(); + d_redundantLits->insert(lit); + } +} + + +/// ProxyProof +template +ProofProxy::ProofProxy(TSatProof* proof): + d_proof(proof) +{} + +template +void ProofProxy::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { + d_proof->updateCRef(oldref, newref); +} + + +/// SatProof +template +TSatProof::TSatProof(Solver* solver, const std::string& name, bool checkRes) + : d_solver(solver) + , d_cnfProof(NULL) + , d_idClause() + , d_clauseId() + , d_idUnit() + , d_deleted() + , d_inputClauses() + , d_lemmaClauses() + , d_assumptions() + , d_assumptionConflicts() + , d_assumptionConflictsDebug() + , d_resChains() + , d_resStack() + , d_checkRes(checkRes) + , d_emptyClauseId(ClauseIdEmpty) + , d_nullId(-2) + , d_temp_clauseId() + , d_temp_idClause() + , d_unitConflictId() + , d_storedUnitConflict(false) + , d_trueLit(ClauseIdUndef) + , d_falseLit(ClauseIdUndef) + , d_name(name) + , d_seenLearnt() + , d_seenInputs() + , d_seenLemmas() + , d_statistics(name) +{ + d_proxy = new ProofProxy(this); +} + +template +TSatProof::~TSatProof() { + delete d_proxy; + + // FIXME: double free if deleted clause also appears in d_seenLemmas? + IdToSatClause::iterator it = d_deletedTheoryLemmas.begin(); + IdToSatClause::iterator end = d_deletedTheoryLemmas.end(); + + for (; it != end; ++it) { + ClauseId id = it->first; + // otherwise deleted in next loop + if (d_seenLemmas.find(id) == d_seenLemmas.end()) + delete it->second; + } + + IdToSatClause::iterator seen_it = d_seenLemmas.begin(); + IdToSatClause::iterator seen_end = d_seenLemmas.end(); + + for (; seen_it != seen_end; ++seen_it) { + delete seen_it->second; + } + + seen_it = d_seenInputs.begin(); + seen_end = d_seenInputs.end(); + + for (; seen_it != seen_end; ++seen_it) { + delete seen_it->second; + } +} + +template +void TSatProof::setCnfProof(CnfProof* cnf_proof) { + Assert (d_cnfProof == NULL); + d_cnfProof = cnf_proof; +} + +/** + * Returns true if the resolution chain corresponding to id + * does resolve to the clause associated to id + * @param id + * + * @return + */ +template +bool TSatProof::checkResolution(ClauseId id) { + if(d_checkRes) { + bool validRes = true; + Assert(d_resChains.find(id) != d_resChains.end()); + ResChain* res = d_resChains[id]; + LitSet clause1; + createLitSet(res->getStart(), clause1); + typename ResChain::ResSteps& steps = res->getSteps(); + for (unsigned i = 0; i < steps.size(); i++) { + typename Solver::TLit var = steps[i].lit; + LitSet clause2; + createLitSet (steps[i].id, clause2); + bool res = resolve (var, clause1, clause2, steps[i].sign); + if(res == false) { + validRes = false; + break; + } + } + // compare clause we claimed to prove with the resolution result + if (isUnit(id)) { + // special case if it was a unit clause + typename Solver::TLit unit = getUnit(id); + validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); + return validRes; + } + if (id == d_emptyClauseId) { + return clause1.empty(); + } + + LitVector c; + getLitVec(id, c); + + for (unsigned i = 0; i < c.size(); ++i) { + int count = clause1.erase(c[i]); + if (count == 0) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + printLit(c[i]); + Debug("proof:sat") << "\n"; + } + validRes = false; + } + } + validRes = clause1.empty(); + if (! validRes) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + printLitSet(clause1); + Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; + printClause(c); + } + } + return validRes; + + } else { + return true; + } +} + + + + +/// helper methods +template +ClauseId TSatProof::getClauseId(typename Solver::TCRef ref) { + if(d_clauseId.find(ref) == d_clauseId.end()) { + Debug("proof:sat") << "Missing clause \n"; + } + Assert(d_clauseId.find(ref) != d_clauseId.end()); + return d_clauseId[ref]; +} + +template +ClauseId TSatProof::getClauseId(typename Solver::TLit lit) { + Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); + return d_unitId[toInt(lit)]; +} +template +typename Solver::TCRef TSatProof::getClauseRef(ClauseId id) { + if (d_idClause.find(id) == d_idClause.end()) { + Debug("proof:sat") << "proof:getClauseRef cannot find clause "< +typename Solver::TClause& TSatProof::getClause(typename Solver::TCRef ref) { + Assert(ref != Solver::TCRef_Undef); + Assert(ref >= 0 && ref < d_solver->ca.size()); + return d_solver->ca[ref]; +} + +template +void TSatProof::getLitVec(ClauseId id, LitVector& vec) { + if (isUnit(id)) { + typename Solver::TLit lit = getUnit(id); + vec.push_back(lit); + return; + } + if (isAssumptionConflict(id)) { + vec = *(d_assumptionConflictsDebug[id]); + return; + } + typename Solver::TCRef cref = getClauseRef(id); + typename Solver::TClause& cl = getClause(cref); + for (int i = 0; i < cl.size(); ++i) { + vec.push_back(cl[i]); + } +} + + +template +typename Solver::TLit TSatProof::getUnit(ClauseId id) { + Assert(d_idUnit.find(id) != d_idUnit.end()); + return d_idUnit[id]; +} +template +bool TSatProof::isUnit(ClauseId id) { + return d_idUnit.find(id) != d_idUnit.end(); +} +template +bool TSatProof::isUnit(typename Solver::TLit lit) { + return d_unitId.find(toInt(lit)) != d_unitId.end(); +} +template +ClauseId TSatProof::getUnitId(typename Solver::TLit lit) { + Assert(isUnit(lit)); + return d_unitId[toInt(lit)]; +} +template +bool TSatProof::hasResolution(ClauseId id) { + return d_resChains.find(id) != d_resChains.end(); +} +template +bool TSatProof::isInputClause(ClauseId id) { + return (d_inputClauses.find(id) != d_inputClauses.end()); +} +template +bool TSatProof::isLemmaClause(ClauseId id) { + return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); +} + +template +bool TSatProof::isAssumptionConflict(ClauseId id) { + return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +} + + +template +void TSatProof::print(ClauseId id) { + if (d_deleted.find(id) != d_deleted.end()) { + Debug("proof:sat") << "del"<(getUnit(id)); + } else if (id == d_emptyClauseId) { + Debug("proof:sat") << "empty "<< std::endl; + } + else { + typename Solver::TCRef ref = getClauseRef(id); + printClause(getClause(ref)); + } +} +template +void TSatProof::printRes(ClauseId id) { + Assert(hasResolution(id)); + Debug("proof:sat") << "id "<< id <<": "; + printRes(d_resChains[id]); +} +template +void TSatProof::printRes(ResChain* res) { + ClauseId start_id = res->getStart(); + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "("; + print(start_id); + } + + typename ResChain::ResSteps& steps = res->getSteps(); + for(unsigned i = 0; i < steps.size(); i++ ) { + typename Solver::TLit v = steps[i].lit; + ClauseId id = steps[i].id; + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "["; + printLit(v); + Debug("proof:sat") << "] "; + print(id); + } + } + Debug("proof:sat") << ") \n"; +} + +/// registration methods +template + ClauseId TSatProof::registerClause(typename Solver::TCRef clause, + ClauseKind kind) { + Assert(clause != Solver::TCRef_Undef); + typename ClauseIdMap::iterator it = d_clauseId.find(clause); + if (it == d_clauseId.end()) { + ClauseId newId = ProofManager::currentPM()->nextId(); + d_clauseId.insert(std::make_pair(clause, newId)); + d_idClause.insert(std::make_pair(newId, clause)); + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + + ClauseId id = d_clauseId[clause]; + Assert(kind != INPUT || d_inputClauses.count(id)); + Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); + + Debug("proof:sat:detailed") << "registerClause CRef: " << clause << " id: " << d_clauseId[clause] + <<" kind: " << kind << "\n"; + //ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); + return id; +} + +template +ClauseId TSatProof::registerUnitClause(typename Solver::TLit lit, + ClauseKind kind) { + Debug("cores") << "registerUnitClause " << kind << std::endl; + typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); + if (it == d_unitId.end()) { + ClauseId newId = ProofManager::currentPM()->nextId(); + d_unitId.insert(std::make_pair(toInt(lit), newId)); + d_idUnit.insert(std::make_pair(newId, lit)); + + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + ClauseId id = d_unitId[toInt(lit)]; + Assert(kind != INPUT || d_inputClauses.count(id)); + Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); + Debug("proof:sat:detailed") << "registerUnitClause id: " << id + <<" kind: " << kind << "\n"; + // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); + return id; +} +template +void TSatProof::registerTrueLit(const typename Solver::TLit lit) { + Assert (d_trueLit == ClauseIdUndef); + d_trueLit = registerUnitClause(lit, INPUT); +} + +template +void TSatProof::registerFalseLit(const typename Solver::TLit lit) { + Assert (d_falseLit == ClauseIdUndef); + d_falseLit = registerUnitClause(lit, INPUT); +} + +template +ClauseId TSatProof::getTrueUnit() const { + Assert (d_trueLit != ClauseIdUndef); + return d_trueLit; +} + +template +ClauseId TSatProof::getFalseUnit() const { + Assert (d_falseLit != ClauseIdUndef); + return d_falseLit; +} + + +template +void TSatProof::registerAssumption(const typename Solver::TVar var) { + Assert (d_assumptions.find(var) == d_assumptions.end()); + d_assumptions.insert(var); +} + +template +ClauseId TSatProof::registerAssumptionConflict(const typename Solver::TLitVec& confl) { + Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; + // Uniqueness is checked in the bit-vector proof + // should be vars + for (int i = 0; i < confl.size(); ++i) { + Assert (d_assumptions.find(var(confl[i])) != d_assumptions.end()); + } + ClauseId new_id = ProofManager::currentPM()->nextId(); + d_assumptionConflicts.insert(new_id); + LitVector* vec_confl = new LitVector(confl.size()); + for (int i = 0; i < confl.size(); ++i) { + vec_confl->operator[](i) = confl[i]; + } + if (Debug.isOn("proof:sat:detailed")) { + printClause(*vec_confl); + Debug("proof:sat:detailed") << "\n"; + } + + d_assumptionConflictsDebug[new_id] = vec_confl; + return new_id; +} + + +template +void TSatProof::removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { + // if we already added the literal return + if (seen.count(lit)) { + return; + } + + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + if (reason_ref == Solver::TCRef_Undef) { + seen.insert(lit); + removeStack.push_back(lit); + return; + } + + int size = getClause(reason_ref).size(); + for (int i = 1; i < size; i++ ) { + typename Solver::TLit v = getClause(reason_ref)[i]; + if(inClause.count(v) == 0 && seen.count(v) == 0) { + removedDfs(v, removedSet, removeStack, inClause, seen); + } + } + if(seen.count(lit) == 0) { + seen.insert(lit); + removeStack.push_back(lit); + } +} + +template +void TSatProof::removeRedundantFromRes(ResChain* res, ClauseId id) { + LitSet* removed = res->getRedundant(); + if (removed == NULL) { + return; + } + + LitSet inClause; + createLitSet(id, inClause); + + LitVector removeStack; + LitSet seen; + for (typename LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { + removedDfs(*it, removed, removeStack, inClause, seen); + } + + for (int i = removeStack.size()-1; i >= 0; --i) { + typename Solver::TLit lit = removeStack[i]; + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + ClauseId reason_id; + + if (reason_ref == Solver::TCRef_Undef) { + Assert(isUnit(~lit)); + reason_id = getUnitId(~lit); + } else { + reason_id = registerClause(reason_ref, LEARNT); + } + res->addStep(lit, reason_id, !sign(lit)); + } + removed->clear(); +} + +template +void TSatProof::registerResolution(ClauseId id, ResChain* res) { + Assert(res != NULL); + + removeRedundantFromRes(res, id); + Assert(res->redundantRemoved()); + + d_resChains[id] = res; + if(Debug.isOn("proof:sat")) { + printRes(id); + } + if(d_checkRes) { + Assert(checkResolution(id)); + } + + PSTATS( + d_statistics.d_resChainLengths << ((uint64_t)res->getSteps().size()); + d_statistics.d_avgChainLength.addEntry((uint64_t)res->getSteps().size()); + ++(d_statistics.d_numLearnedClauses); + ) +} + + +/// recording resolutions +template +void TSatProof::startResChain(typename Solver::TCRef start) { + ClauseId id = getClauseId(start); + ResChain* res = new ResChain(id); + d_resStack.push_back(res); +} + +template +void TSatProof::startResChain(typename Solver::TLit start) { + ClauseId id = getUnitId(start); + ResChain* res = new ResChain(id); + d_resStack.push_back(res); +} + + +template +void TSatProof::addResolutionStep(typename Solver::TLit lit, + typename Solver::TCRef clause, bool sign) { + ClauseId id = registerClause(clause, LEARNT); + ResChain* res = d_resStack.back(); + res->addStep(lit, id, sign); +} + +template +void TSatProof::endResChain(ClauseId id) { + Debug("proof:sat:detailed") <<"endResChain " << id << "\n"; + Assert(d_resStack.size() > 0); + ResChain* res = d_resStack.back(); + registerResolution(id, res); + d_resStack.pop_back(); +} + + +// template +// void TSatProof::endResChain(typename Solver::TCRef clause) { +// Assert(d_resStack.size() > 0); +// ClauseId id = registerClause(clause, LEARNT); +// ResChain* res = d_resStack.back(); +// registerResolution(id, res); +// d_resStack.pop_back(); +// } + +template +void TSatProof::endResChain(typename Solver::TLit lit) { + Assert(d_resStack.size() > 0); + ClauseId id = registerUnitClause(lit, LEARNT); + Debug("proof:sat:detailed") <<"endResChain unit " << id << "\n"; + ResChain* res = d_resStack.back(); + d_glueMap[id] = 1; + registerResolution(id, res); + d_resStack.pop_back(); +} + + +template +void TSatProof::cancelResChain() { + Assert(d_resStack.size() > 0); + d_resStack.pop_back(); +} + + +template +void TSatProof::storeLitRedundant(typename Solver::TLit lit) { + Assert(d_resStack.size() > 0); + ResChain* res = d_resStack.back(); + res->addRedundantLit(lit); +} + +/// constructing resolutions +template +void TSatProof::resolveOutUnit(typename Solver::TLit lit) { + ClauseId id = resolveUnit(~lit); + ResChain* res = d_resStack.back(); + res->addStep(lit, id, !sign(lit)); +} +template +void TSatProof::storeUnitResolution(typename Solver::TLit lit) { + Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; + resolveUnit(lit); +} +template +ClauseId TSatProof::resolveUnit(typename Solver::TLit lit) { + // first check if we already have a resolution for lit + if(isUnit(lit)) { + ClauseId id = getClauseId(lit); + Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + return id; + } + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + Assert(reason_ref != Solver::TCRef_Undef); + + ClauseId reason_id = registerClause(reason_ref, LEARNT); + + ResChain* res = new ResChain(reason_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload reason ptr each time. + typename Solver::TClause* reason = &getClause(reason_ref); + for (int i = 0; + i < reason->size(); + i++, reason = &getClause(reason_ref)) { + typename Solver::TLit l = (*reason)[i]; + if(lit != l) { + ClauseId res_id = resolveUnit(~l); + res->addStep(l, res_id, !sign(l)); + } + } + ClauseId unit_id = registerUnitClause(lit, LEARNT); + registerResolution(unit_id, res); + return unit_id; +} +template +void TSatProof::toStream(std::ostream& out) { + Debug("proof:sat") << "TSatProof::printProof\n"; + Unimplemented("native proof printing not supported yet"); +} +template +ClauseId TSatProof::storeUnitConflict(typename Solver::TLit conflict_lit, + ClauseKind kind) { + Debug("cores") << "STORE UNIT CONFLICT" << std::endl; + Assert(!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit, kind); + d_storedUnitConflict = true; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + return d_unitConflictId; +} +template +void TSatProof::finalizeProof(typename Solver::TCRef conflict_ref) { + Assert(d_resStack.size() == 0); + Assert(conflict_ref != Solver::TCRef_Undef); + ClauseId conflict_id; + if (conflict_ref == Solver::TCRef_Lazy) { + Assert(d_storedUnitConflict); + conflict_id = d_unitConflictId; + + ResChain* res = new ResChain(conflict_id); + typename Solver::TLit lit = d_idUnit[conflict_id]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + + registerResolution(d_emptyClauseId, res); + + return; + } else { + Assert(!d_storedUnitConflict); + conflict_id = registerClause(conflict_ref, LEARNT); //FIXME + } + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; + print(conflict_id); + } + + ResChain* res = new ResChain(conflict_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload conflict ptr each time. + typename Solver::TClause* conflict = &getClause(conflict_ref); + for (int i = 0; + i < conflict->size(); + ++i, conflict = &getClause(conflict_ref)) { + typename Solver::TLit lit = (*conflict)[i]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + } + registerResolution(d_emptyClauseId, res); +} + +/// CRef manager +template +void TSatProof::updateCRef(typename Solver::TCRef oldref, + typename Solver::TCRef newref) { + if (d_clauseId.find(oldref) == d_clauseId.end()) { + return; + } + ClauseId id = getClauseId(oldref); + Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); + Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); + d_temp_clauseId[newref] = id; + d_temp_idClause[id] = newref; +} +template +void TSatProof::finishUpdateCRef() { + d_clauseId.swap(d_temp_clauseId); + d_temp_clauseId.clear(); + + d_idClause.swap(d_temp_idClause); + d_temp_idClause.clear(); +} +template +void TSatProof::markDeleted(typename Solver::TCRef clause) { + if (d_clauseId.find(clause) != d_clauseId.end()) { + ClauseId id = getClauseId(clause); + Assert(d_deleted.find(id) == d_deleted.end()); + d_deleted.insert(id); + if (isLemmaClause(id)) { + const typename Solver::TClause& minisat_cl = getClause(clause); + prop::SatClause* sat_cl = new prop::SatClause(); + toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + } + } +} + +// template<> +// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, +// prop::SatClause& sat_cl) { + +// prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); +// } + + + +template +void TSatProof::constructProof(ClauseId conflict) { + collectClauses(conflict); +} + +template +std::string TSatProof::clauseName(ClauseId id) { + std::ostringstream os; + if (isInputClause(id)) { + os << ProofManager::getInputClauseName(id, d_name); + return os.str(); + } else + if (isLemmaClause(id)) { + os << ProofManager::getLemmaClauseName(id, d_name); + return os.str(); + }else { + os << ProofManager::getLearntClauseName(id, d_name); + return os.str(); + } +} + +template +prop::SatClause* TSatProof::buildClause(ClauseId id) { + if (isUnit(id)) { + typename Solver::TLit lit = getUnit(id); + prop::SatLiteral sat_lit = toSatLiteral(lit); + prop::SatClause* clause = new prop::SatClause(); + clause->push_back(sat_lit); + return clause; + } + + if (isDeleted(id)) { + prop::SatClause* clause = d_deletedTheoryLemmas.find(id)->second; + return clause; + } + + typename Solver::TCRef ref = getClauseRef(id); + const typename Solver::TClause& minisat_cl = getClause(ref); + prop::SatClause* clause = new prop::SatClause(); + toSatClause(minisat_cl, *clause); + return clause; +} + +template +void TSatProof::collectClauses(ClauseId id) { + if (d_seenInputs.find(id) != d_seenInputs.end() || + d_seenLemmas.find(id) != d_seenLemmas.end() || + d_seenLearnt.find(id) != d_seenLearnt.end()) { + return; + } + + if (isInputClause(id)) { + d_seenInputs.insert(std::make_pair(id, buildClause(id))); + return; + } else if (isLemmaClause(id)) { + d_seenLemmas.insert(std::make_pair(id, buildClause(id))); + return; + } else if (!isAssumptionConflict(id)) { + d_seenLearnt.insert(id); + } + + Assert(d_resChains.find(id) != d_resChains.end()); + ResChain* res = d_resChains[id]; + PSTATS( + d_statistics.d_usedResChainLengths << ((uint64_t)res->getSteps().size()); + d_statistics.d_usedClauseGlue << ((uint64_t) d_glueMap[id]); + ); + ClauseId start = res->getStart(); + collectClauses(start); + + typename ResChain::ResSteps steps = res->getSteps(); + for(size_t i = 0; i < steps.size(); i++) { + collectClauses(steps[i].id); + } +} + +template +void TSatProof::collectClausesUsed(IdToSatClause& inputs, + IdToSatClause& lemmas) { + inputs = d_seenInputs; + lemmas = d_seenLemmas; + PSTATS ( + d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); + d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size()); + ); +} + +template +void TSatProof::storeClauseGlue(ClauseId clause, int glue) { + Assert (d_glueMap.find(clause) == d_glueMap.end()); + d_glueMap.insert(std::make_pair(clause, glue)); +} + +template +TSatProof::Statistics::Statistics(const std::string& prefix) + : d_numLearnedClauses("satproof::"+prefix+"::NumLearnedClauses", 0) + , d_numLearnedInProof("satproof::"+prefix+"::NumLearnedInProof", 0) + , d_numLemmasInProof("satproof::"+prefix+"::NumLemmasInProof", 0) + , d_avgChainLength("satproof::"+prefix+"::AvgResChainLength") + , d_resChainLengths("satproof::"+prefix+"::ResChainLengthsHist") + , d_usedResChainLengths("satproof::"+prefix+"::UsedResChainLengthsHist") + , d_clauseGlue("satproof::"+prefix+"::ClauseGlueHist") + , d_usedClauseGlue("satproof::"+prefix+"::UsedClauseGlueHist") { + smtStatisticsRegistry()->registerStat(&d_numLearnedClauses); + smtStatisticsRegistry()->registerStat(&d_numLearnedInProof); + smtStatisticsRegistry()->registerStat(&d_numLemmasInProof); + smtStatisticsRegistry()->registerStat(&d_avgChainLength); + smtStatisticsRegistry()->registerStat(&d_resChainLengths); + smtStatisticsRegistry()->registerStat(&d_usedResChainLengths); + smtStatisticsRegistry()->registerStat(&d_clauseGlue); + smtStatisticsRegistry()->registerStat(&d_usedClauseGlue); +} + +template +TSatProof::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses); + smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof); + smtStatisticsRegistry()->unregisterStat(&d_numLemmasInProof); + smtStatisticsRegistry()->unregisterStat(&d_avgChainLength); + smtStatisticsRegistry()->unregisterStat(&d_resChainLengths); + smtStatisticsRegistry()->unregisterStat(&d_usedResChainLengths); + smtStatisticsRegistry()->unregisterStat(&d_clauseGlue); + smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); +} + + +/// LFSCSatProof class +template +void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + out << "(satlem_simplify _ _ _ "; + + ResChain* res = this->d_resChains[id]; + typename ResChain::ResSteps& steps = res->getSteps(); + + for (int i = steps.size()-1; i >= 0; i--) { + out << "("; + out << (steps[i].sign? "R" : "Q") << " _ _ "; + } + + ClauseId start_id = res->getStart(); + out << this->clauseName(start_id) << " "; + + for(unsigned i = 0; i < steps.size(); i++) { + prop::SatVariable v = prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); + out << this->clauseName(steps[i].id) << " "<d_name) <<")"; + } + + if (id == this->d_emptyClauseId) { + out <<"(\\empty empty)"; + return; + } + + out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem +} + +/// LFSCSatProof class +template +void LFSCSatProof::printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + Assert (this->isAssumptionConflict(id)); + // print the resolution proving the assumption conflict + printResolution(id, out, paren); + // resolve out assumptions to prove empty clause + out << "(satlem_simplify _ _ _ "; + std::vector& confl = *(this->d_assumptionConflictsDebug[id]); + + Assert (confl.size()); + + for (unsigned i = 0; i < confl.size(); ++i) { + prop::SatLiteral lit = toSatLiteral(confl[i]); + out <<"("; + out << (lit.isNegated() ? "Q" : "R") <<" _ _ "; + } + + out << this->clauseName(id)<< " "; + for (int i = confl.size() - 1; i >= 0; --i) { + prop::SatLiteral lit = toSatLiteral(confl[i]); + prop::SatVariable v = lit.getSatVariable(); + out << "unit"<< v <<" "; + out << ProofManager::getVarName(v, this->d_name) <<")"; + } + out <<"(\\ e e)\n"; + paren <<")"; +} + + +template +void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { + Debug("bv-proof") << "; print resolutions" << std::endl; + std::set::iterator it = this->d_seenLearnt.begin(); + for(; it!= this->d_seenLearnt.end(); ++it) { + if(*it != this->d_emptyClauseId) { + Debug("bv-proof") << "; print resolution for " << *it << std::endl; + printResolution(*it, out, paren); + } + } + Debug("bv-proof") << "; done print resolutions" << std::endl; +} + +template +void LFSCSatProof::printResolutionEmptyClause(std::ostream& out, std::ostream& paren) { + printResolution(this->d_emptyClauseId, out, paren); +} + + +inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { + switch(k) { + case CVC4::INPUT: + out << "INPUT"; + break; + case CVC4::THEORY_LEMMA: + out << "THEORY_LEMMA"; + break; + case CVC4::LEARNT: + out << "LEARNT"; + break; + default: + out << "ClauseKind Unknown! [" << unsigned(k) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 6982509b1..b0d6988a5 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -15,145 +15,455 @@ ** \todo document this file **/ -#include "proof/theory_proof.h" +#include "base/cvc4_assert.h" +#include "context/context.h" +#include "options/bv_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" +#include "proof/cnf_proof.h" +#include "proof/cnf_proof.h" #include "proof/proof_manager.h" -using namespace CVC4; +#include "proof/proof_utils.h" +#include "proof/sat_proof.h" +#include "proof/theory_proof.h" +#include "proof/uf_proof.h" +#include "prop/sat_solver_types.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "smt_util/node_visitor.h" +#include "theory/arrays/theory_arrays.h" +#include "theory/bv/theory_bv.h" +#include "theory/output_channel.h" +#include "theory/term_registration_visitor.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/valuation.h" +#include "util/hash.h" +#include "util/proof.h" -TheoryProof::TheoryProof() - : d_termDeclarations() - , d_sortDeclarations() - , d_declarationCache() -{} -void TheoryProof::addDeclaration(Expr term) { - if (d_declarationCache.count(term)) { - return; - } +namespace CVC4 { + +unsigned CVC4::LetCount::counter = 0; +static unsigned LET_COUNT = 1; + +//for proof replay +class ProofOutputChannel : public theory::OutputChannel { +public: + Node d_conflict; + Proof* d_proof; + Node d_lemma; - Type type = term.getType(); - if (type.isSort()) - d_sortDeclarations.insert(type); - if (term.getKind() == kind::APPLY_UF) { - Expr function = term.getOperator(); - d_termDeclarations.insert(function); - } else if (term.isVariable()) { - //Assert (type.isSort() || type.isBoolean()); - d_termDeclarations.insert(term); + ProofOutputChannel() : d_conflict(), d_proof(NULL) {} + + void conflict(TNode n, Proof* pf) throw() { + Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl; + Assert(d_conflict.isNull()); + Assert(!n.isNull()); + d_conflict = n; + Assert(pf != NULL); + d_proof = pf; } - // recursively declare all other terms - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - addDeclaration(term[i]); + bool propagate(TNode x) throw() { + Trace("theory-proof-debug") << "got a propagation: " << x << std::endl; + return true; + } + theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { + Trace("theory-proof-debug") << "new lemma: " << n << std::endl; + d_lemma = n; + return theory::LemmaStatus(TNode::null(), 0); + } + theory::LemmaStatus splitLemma(TNode, bool) throw() { + AlwaysAssert(false); + return theory::LemmaStatus(TNode::null(), 0); + } + void requirePhase(TNode n, bool b) throw() { + Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl; + } + bool flipDecision() throw() { + AlwaysAssert(false); + return false; + } + void setIncomplete() throw() { + AlwaysAssert(false); } - d_declarationCache.insert(term); +};/* class ProofOutputChannel */ + +//for proof replay +class MyPreRegisterVisitor { + theory::Theory* d_theory; + __gnu_cxx::hash_set d_visited; +public: + typedef void return_type; + MyPreRegisterVisitor(theory::Theory* theory) + : d_theory(theory) + , d_visited() + {} + bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); } + void visit(TNode current, TNode parent) { + if(theory::Theory::theoryOf(current) == d_theory->getId()) { + //Trace("theory-proof-debug") << "preregister " << current << std::endl; + d_theory->preRegisterTerm(current); + d_visited.insert(current); + } + } + void start(TNode node) { } + void done(TNode node) { } +}; /* class MyPreRegisterVisitor */ + +TheoryProofEngine::TheoryProofEngine(SmtGlobals* globals) + : d_registrationCache() + , d_theoryProofTable() + , d_globals(globals) +{ + d_theoryProofTable[theory::THEORY_BOOL] = new LFSCBooleanProof(this); } -std::string toLFSCKind(Kind kind) { - switch(kind) { - case kind::OR : return "or"; - case kind::AND: return "and"; - case kind::XOR: return "xor"; - case kind::EQUAL: return "="; - case kind::IFF: return "iff"; - case kind::IMPLIES: return "impl"; - case kind::NOT: return "not"; - default: - Unreachable(); +TheoryProofEngine::~TheoryProofEngine() { + TheoryProofTable::iterator it = d_theoryProofTable.begin(); + TheoryProofTable::iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + delete it->second; } } -void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { - if (term.isVariable()) { - if(term.getType().isBoolean()) { - os << "(p_app " << term << ")"; - } else { - os << term; + +void TheoryProofEngine::registerTheory(theory::Theory* th) { + if( th ){ + theory::TheoryId id = th->getId(); + if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) { + + Trace("theory-proof-debug") << "; register theory " << id << std::endl; + + if (id == theory::THEORY_UF) { + d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); + return; + } + + if (id == theory::THEORY_BV) { + BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); + d_theoryProofTable[id] = bvp; + ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + return; + } + if (id == theory::THEORY_ARRAY) { + d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this); + return; + } + // TODO other theories } + } +} + +TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { + Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end()); + return d_theoryProofTable[id]; +} + +void TheoryProofEngine::registerTerm(Expr term) { + if (d_registrationCache.count(term)) { return; } - switch(Kind k = term.getKind()) { - case kind::APPLY_UF: { - if(term.getType().isBoolean()) { - os << "(p_app "; - } - Expr func = term.getOperator(); + theory::TheoryId theory_id = theory::Theory::theoryOf(term); + + // don't need to register boolean terms + if (theory_id == theory::THEORY_BUILTIN || + term.getKind() == kind::ITE) { for (unsigned i = 0; i < term.getNumChildren(); ++i) { - os << "(apply _ _ "; + registerTerm(term[i]); } - os << func << " "; - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - printTerm(term[i], os); - os << ")"; + d_registrationCache.insert(term); + return; + } + + if (!supportedTheory(theory_id)) return; + + getTheoryProof(theory_id)->registerTerm(term); + d_registrationCache.insert(term); +} + +theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { + // TODO: now CNF proof has a map from formula to proof rule + // that should be checked to figure out what theory is responsible for this + ProofManager* pm = ProofManager::currentPM(); + + if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; + if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; + if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; + Unreachable(); +} + +void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { + LetMap::iterator it = map.find(term); + if (it != map.end()) { + LetCount& count = it->second; + count.increment(); + return; + } + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + bind(term[i], map, let_order); + } + unsigned new_id = LetCount::newId(); + map[term] = LetCount(new_id); + let_order.push_back(LetOrderElement(term, new_id)); +} + +void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { + LetMap map; + Bindings let_order; + bind(term, map, let_order); + std::ostringstream paren; + for (unsigned i = 0; i < let_order.size(); ++i) { + Expr current_expr = let_order[i].expr; + unsigned let_id = let_order[i].id; + LetMap::const_iterator it = map.find(current_expr); + Assert (it != map.end()); + unsigned let_count = it->second.count; + Assert(let_count); + // skip terms that only appear once + if (let_count <= LET_COUNT) { + continue; } - if(term.getType().isBoolean()) { - os << ")"; + + os << "(@ let"<second.count; + if (last_count <= LET_COUNT) { + printTheoryTerm(last, os, map); + } + else { + os << " let"<< last_let_id; + } + os << paren.str(); +} + + +void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) { + theory::TheoryId theory_id = theory::Theory::theoryOf(term); + // boolean terms and ITEs are special because they + // are common to all theories + if (theory_id == theory::THEORY_BUILTIN || + term.getKind() == kind::ITE || + term.getKind() == kind::EQUAL) { + printCoreTerm(term, os, map); + return; + } + // dispatch to proper theory + getTheoryProof(theory_id)->printTerm(term, os, map); +} + +void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) { + if (type.isSort()) { + getTheoryProof(theory::THEORY_UF)->printSort(type, os); + return; + } + if (type.isBitVector()) { + getTheoryProof(theory::THEORY_BV)->printSort(type, os); + return; + } + + if (type.isArray()) { + getTheoryProof(theory::THEORY_ARRAY)->printSort(type, os); + return; + } + Unreachable(); +} + +void LFSCTheoryProofEngine::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(); + + // collect declarations first + for(; it != end; ++it) { + registerTerm(*it); + } + printDeclarations(os, paren); + + it = ProofManager::currentPM()->begin_assertions(); + for (; it != end; ++it) { + // FIXME: merge this with counter + os << "(% A" << counter++ << " (th_holds "; + printLetTerm(*it, os); + os << ")\n"; + paren << ")"; + } + //store map between assertion and counter + // ProofManager::currentPM()->setAssertion( *it ); +} + +void LFSCTheoryProofEngine::printDeclarations(std::ostream& os, std::ostream& paren) { + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->printDeclarations(os, paren); + } +} + +void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren) { + os << " ;; Theory Lemmas \n"; + ProofManager* pm = ProofManager::currentPM(); + IdToSatClause::const_iterator it = lemmas.begin(); + IdToSatClause::const_iterator end = lemmas.end(); + + // BitVector theory is special case: must know all + // conflicts needed ahead of time for resolution + // proof lemmas + std::vector bv_lemmas; + for (; it != end; ++it) { + ClauseId id = it->first; + const prop::SatClause* clause = it->second; + + theory::TheoryId theory_id = getTheoryForLemma(id); + if (theory_id != theory::THEORY_BV) continue; + + std::vector conflict; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue() || + (atom == utils::mkFalse() && lit.isNegated())); + continue; + } + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; + conflict.push_back(expr_lit); + } + bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict)); + } + // FIXME: ugly, move into bit-vector proof by adding lemma + // queue inside each theory_proof + BitVectorProof* bv = ProofManager::getBitVectorProof(); + bv->finalizeConflicts(bv_lemmas); + + bv->printResolutionProof(os, paren); + + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + Assert (lemmas.size() == 1); + // nothing more to do (no combination with eager so far) + return; + } + + it = lemmas.begin(); + + for (; it != end; ++it) { + ClauseId id = it->first; + const prop::SatClause* clause = it->second; + // printing clause as it appears in resolution proof + os << "(satlem _ _ "; + std::ostringstream clause_paren; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + + std::vector clause_expr; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; + clause_expr.push_back(expr_lit); } + + // query appropriate theory for proof of clause + theory::TheoryId theory_id = getTheoryForLemma(id); + Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl; + getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); + // os << " (clausify_false trust)"; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; + paren << "))"; + } +} + +void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { + LetMap::const_iterator it = map.find(term); + Assert (it != map.end()); + unsigned id = it->second.id; + unsigned count = it->second.count; + if (count > LET_COUNT) { + os <<"let"<= 2); - case kind::OR: - case kind::AND: - case kind::XOR: - case kind::IFF: - case kind::IMPLIES: - case kind::NOT: - // print the Boolean operators - os << "(" << toLFSCKind(k); - if(term.getNumChildren() > 2) { - // LFSC doesn't allow declarations with variable numbers of - // arguments, so we have to flatten these N-ary versions. - std::ostringstream paren; + if (term.getNumChildren() == 2) { + os << "(not (= "; + printSort(term[0].getType(), os); + printBoundTerm(term[0], os, map); os << " "; - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - printTerm(term[i], os); - os << " "; - if(i < term.getNumChildren() - 2) { - os << "(" << toLFSCKind(k) << " "; - paren << ")"; - } - } - os << paren.str() << ")"; + printBoundTerm(term[1], os, map); + os << "))"; } else { - // this is for binary and unary operators + unsigned numOfPairs = term.getNumChildren() * (term.getNumChildren() - 1) / 2; + for (unsigned i = 1; i < numOfPairs; ++i) { + os << "(and "; + } + for (unsigned i = 0; i < term.getNumChildren(); ++i) { - os << " "; - printTerm(term[i], os); + for (unsigned j = i + 1; j < term.getNumChildren(); ++j) { + if ((i != 0) || (j != 1)) { + os << "(not (= "; + printSort(term[0].getType(), os); + printBoundTerm(term[i], os, map); + os << " "; + printBoundTerm(term[j], os, map); + os << ")))"; + } else { + os << "(not (= "; + printSort(term[0].getType(), os); + printBoundTerm(term[0], os, map); + os << " "; + printBoundTerm(term[1], os, map); + os << "))"; + } + } } - os << ")"; } - return; - case kind::CONST_BOOLEAN: - os << (term.getConst() ? "true" : "false"); return; case kind::CHAIN: { @@ -164,13 +474,13 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { std::ostringstream paren; for(size_t i = 1; i < n; ++i) { if(i + 1 < n) { - os << "(" << toLFSCKind(kind::AND) << " "; + os << "(" << utils::toLFSCKind(kind::AND) << " "; paren << ")"; } - os << "(" << toLFSCKind(op) << " "; - printTerm(term[i - 1], os); + os << "(" << utils::toLFSCKind(op) << " "; + printBoundTerm(term[i - 1], os, map); os << " "; - printTerm(term[i], os); + printBoundTerm(term[i], os, map); os << ")"; if(i + 1 < n) { os << " "; @@ -184,66 +494,144 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { Unhandled(k); } - Unreachable(); } -void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { - ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); - ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); - - // collect declarations first - for(; it != end; ++it) { - addDeclaration(*it); +void TheoryProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { + //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory + Assert( d_theory!=NULL ); + context::UserContext fakeContext; + ProofOutputChannel oc; + theory::Valuation v(NULL); + //make new copy of theory + theory::Theory* th; + Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; + if(d_theory->getId()==theory::THEORY_UF) { + th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, + ProofManager::currentPM()->getLogicInfo(), + ProofManager::currentPM()->getTheoryProofEngine()->d_globals, + "replay::"); + } else if(d_theory->getId()==theory::THEORY_ARRAY) { + th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, + ProofManager::currentPM()->getLogicInfo(), + ProofManager::currentPM()->getTheoryProofEngine()->d_globals, + "replay::"); + } else { + InternalError(std::string("can't generate theory-proof for ") + ProofManager::currentPM()->getLogic()); } - printDeclarations(os, paren); - - it = ProofManager::currentPM()->begin_assertions(); - for (; it != end; ++it) { - os << "(% A" << ProofManager::currentPM()->getAssertionCounter() << " (th_holds "; - printTerm(*it, os); - os << ")\n"; - paren << ")"; - //store map between assertion and counter - ProofManager::currentPM()->setAssertion( *it ); + th->produceProofs(); + MyPreRegisterVisitor preRegVisitor(th); + for( unsigned i=0; i::run(preRegVisitor, lit); + th->assertFact(lit, false); + } + th->check(theory::Theory::EFFORT_FULL); + if(oc.d_conflict.isNull()) { + Trace("theory-proof-debug") << "; conflict is null" << std::endl; + Assert(!oc.d_lemma.isNull()); + Trace("theory-proof-debug") << "; ++ but got lemma: " << oc.d_lemma << std::endl; + Trace("theory-proof-debug") << "; asserting " << oc.d_lemma[1].negate() << std::endl; + th->assertFact(oc.d_lemma[1].negate(), false); + th->check(theory::Theory::EFFORT_FULL); } + oc.d_proof->toStream(os); + delete th; } -void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { - // declaring the sorts - for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) { - os << "(% " << *it << " sort\n"; - paren << ")"; +bool TheoryProofEngine::supportedTheory(theory::TheoryId id) { + return (id == theory::THEORY_ARRAY || + id == theory::THEORY_BV || + id == theory::THEORY_UF || + id == theory::THEORY_BOOL); +} + +BooleanProof::BooleanProof(TheoryProofEngine* proofEngine) + : TheoryProof(NULL, proofEngine) +{} + +void BooleanProof::registerTerm(Expr term) { + Assert (term.getType().isBoolean()); + + if (term.isVariable() && d_declarations.find(term) == d_declarations.end()) { + d_declarations.insert(term); + return; + } + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + d_proofEngine->registerTerm(term[i]); } +} - // declaring the terms - for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { - Expr term = *it; +void LFSCBooleanProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { + Assert (term.getType().isBoolean()); + if (term.isVariable()) { + os << "(p_app " << ProofManager::sanitize(term) <<")"; + return; + } - os << "(% " << term << " "; - os << "(term "; - - Type type = term.getType(); - if (type.isFunction()) { - std::ostringstream fparen; - FunctionType ftype = (FunctionType)type; - std::vector args = ftype.getArgTypes(); - args.push_back(ftype.getRangeType()); - os << "(arrow"; - for (unsigned i = 0; i < args.size(); i++) { - Type arg_type = args[i]; - //Assert (arg_type.isSort() || arg_type.isBoolean()); - os << " " << arg_type; - if (i < args.size() - 2) { - os << " (arrow"; - fparen << ")"; + Kind k = term.getKind(); + switch(k) { + case kind::OR: + case kind::AND: + case kind::XOR: + case kind::IFF: + case kind::IMPLIES: + case kind::NOT: + // print the Boolean operators + os << "(" << utils::toLFSCKind(k); + if(term.getNumChildren() > 2) { + // LFSC doesn't allow declarations with variable numbers of + // arguments, so we have to flatten these N-ary versions. + std::ostringstream paren; + os << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + if(i < term.getNumChildren() - 2) { + os << "(" << utils::toLFSCKind(k) << " "; + paren << ")"; } } - os << fparen.str() << "))\n"; + os << paren.str() << ")"; } else { - Assert (term.isVariable()); - //Assert (type.isSort() || type.isBoolean()); - os << type << ")\n"; + // this is for binary and unary operators + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << " "; + d_proofEngine->printBoundTerm(term[i], os, map); + } + os << ")"; } - paren << ")"; + return; + + case kind::CONST_BOOLEAN: + os << (term.getConst() ? "true" : "false"); + return; + + default: + Unhandled(k); } + } + +void LFSCBooleanProof::printSort(Type type, std::ostream& os) { + Assert (type.isBoolean()); + os << "Bool"; +} +void LFSCBooleanProof::printDeclarations(std::ostream& os, std::ostream& paren) { + for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { + Expr term = *it; + + os << "(% " << ProofManager::sanitize(term) << " (term "; + printSort(term.getType(), os); + os <<")\n"; + paren <<")"; + } +} + +void LFSCBooleanProof::printTheoryLemmaProof(std::vector& lemma, + std::ostream& os, + std::ostream& paren) { + Unreachable("No boolean lemmas yet!"); +} + +} /* namespace CVC4 */ diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 375ec8205..3d700c388 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -1,56 +1,260 @@ /********************* */ /*! \file theory_proof.h - ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters - ** 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 - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief A manager for UfProofs. - ** - ** A manager for UfProofs. - ** - ** - **/ +** \verbatim +** Original author: Liana Hadarean +** Major contributors: Morgan Deters +** 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 +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief A manager for UfProofs. +** +** A manager for UfProofs. +** +** +**/ #include "cvc4_private.h" #ifndef __CVC4__THEORY_PROOF_H #define __CVC4__THEORY_PROOF_H +#include "util/proof.h" +#include "expr/expr.h" +#include "prop/sat_solver_types.h" #include #include -#include "expr/expr.h" -#include "util/proof.h" namespace CVC4 { - typedef __gnu_cxx::hash_set SortSet; - typedef __gnu_cxx::hash_set ExprSet; - - class TheoryProof { - protected: - ExprSet d_termDeclarations; - SortSet d_sortDeclarations; - ExprSet d_declarationCache; - - public: - TheoryProof(); - virtual ~TheoryProof() {} - virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; - void addDeclaration(Expr atom); - }; - - class LFSCTheoryProof : public TheoryProof { - void printDeclarations(std::ostream& os, std::ostream& paren); - public: - static void printTerm(Expr term, std::ostream& os); - virtual void printAssertions(std::ostream& os, std::ostream& paren); - }; +class SmtGlobals; + +namespace theory { +class Theory; +} + +typedef unsigned ClauseId; + +struct LetCount { + static unsigned counter; + static void resetCounter() { counter = 0; } + static unsigned newId() { return ++counter; } + + unsigned count; + unsigned id; + LetCount() + : count(0) + , id(-1) + {} + + void increment() { ++count; } + LetCount(unsigned i) + : count(1) + , id(i) + {} + LetCount(const LetCount& other) + : count(other.count) + , id (other.id) + {} + bool operator==(const LetCount &other) const { + return other.id == id && other.count == count; + } + LetCount& operator=(const LetCount &rhs) { + if (&rhs == this) return *this; + id = rhs.id; + count = rhs.count; + return *this; + } +}; + +struct LetOrderElement { + Expr expr; + unsigned id; + LetOrderElement(Expr e, unsigned i) + : expr(e) + , id(i) + {} + + LetOrderElement() + : expr() + , id(-1) + {} +}; + +typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; + +typedef __gnu_cxx::hash_map LetMap; +typedef std::vector Bindings; + +class TheoryProof; +typedef unsigned ClauseId; + +typedef __gnu_cxx::hash_set ExprSet; +typedef std::map TheoryProofTable; + +class TheoryProofEngine { +protected: + ExprSet d_registrationCache; + TheoryProofTable d_theoryProofTable; + + /** + * Returns whether the theory is currently supported in proof + * production mode. + */ + bool supportedTheory(theory::TheoryId id); +public: + SmtGlobals* d_globals; + + TheoryProofEngine(SmtGlobals* globals); + virtual ~TheoryProofEngine(); + /** + * Print the theory term (could be atom) by delegating to the + * proper theory + * + * @param term + * @param os + * + * @return + */ + virtual void printLetTerm(Expr term, std::ostream& os) = 0; + virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + /** + * Print the proof representation of the given sort. + * + * @param os + */ + virtual void printSort(Type type, std::ostream& os) = 0; + /** + * Print the theory assertions (arbitrary formulas over + * theory atoms) + * + * @param os + * @param paren closing parenthesis + */ + virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + /** + * Print proofs of all the theory lemmas (must prove + * actual clause used in resolution proof). + * + * @param os + * @param paren + */ + virtual void printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren) = 0; + /** + * Register theory atom (ensures all terms and atoms are declared). + * + * @param atom + */ + void registerTerm(Expr atom); + /** + * Ensures that a theory proof class for the given theory + * is created. + * + * @param theory + */ + void registerTheory(theory::Theory* theory); + theory::TheoryId getTheoryForLemma(ClauseId id); + TheoryProof* getTheoryProof(theory::TheoryId id); +}; + +class LFSCTheoryProofEngine : public TheoryProofEngine { + LetMap d_letMap; + void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map); + void bind(Expr term, LetMap& map, Bindings& let_order); +public: + LFSCTheoryProofEngine(SmtGlobals* globals) + : TheoryProofEngine(globals) {} + + void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printLetTerm(Expr term, std::ostream& os); + virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printAssertions(std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren); + virtual void printSort(Type type, std::ostream& os); +}; + +class TheoryProof { +protected: + // Pointer to the theory for this proof + theory::Theory* d_theory; + TheoryProofEngine* d_proofEngine; +public: + TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine) + : d_theory(th) + , d_proofEngine(proofEngine) + {} + virtual ~TheoryProof() {}; + /** + * Print a term belonging to this theory. + * + * @param term expresion representing term + * @param os output stream + */ + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + /** + * Print the proof representation of the given type. + * + * @param type + * @param os + */ + virtual void printSort(Type type, std::ostream& os) = 0; + /** + * Print a proof for the theory lemmas. Must prove + * clause representing lemmas to be used in resolution proof. + * + * @param os output stream + */ + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + /** + * Print the variable/sorts declarations for this theory. + * + * @param os + * @param paren + */ + virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Register a term of this theory that appears in the proof. + * + * @param term + */ + virtual void registerTerm(Expr term) = 0; +}; + +class BooleanProof : public TheoryProof { +protected: + ExprSet d_declarations; // all the boolean variables +public: + BooleanProof(TheoryProofEngine* proofEngine); + + virtual void registerTerm(Expr term); + + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + + virtual void printSort(Type type, std::ostream& os) = 0; + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) = 0; + virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; +}; + +class LFSCBooleanProof : public BooleanProof { +public: + LFSCBooleanProof(TheoryProofEngine* proofEngine) + : BooleanProof(proofEngine) + {} + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printSort(Type type, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); +}; + + } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp new file mode 100644 index 000000000..ec0d90ae7 --- /dev/null +++ b/src/proof/uf_proof.cpp @@ -0,0 +1,804 @@ +/********************* */ +/*! \file uf_proof.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** 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 +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" +#include "proof/uf_proof.h" +#include "theory/uf/theory_uf.h" +#include + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + + +inline static Node eqNode(TNode n1, TNode n2) { + return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); +} + +// congrence matching term helper +inline static bool match(TNode n1, TNode n2) { + Debug("mgd") << "match " << n1 << " " << n2 << std::endl; + if(ProofManager::currentPM()->hasOp(n1)) { + n1 = ProofManager::currentPM()->lookupOp(n1); + } + if(ProofManager::currentPM()->hasOp(n2)) { + n2 = ProofManager::currentPM()->lookupOp(n2); + } + Debug("mgd") << "+ match " << n1 << " " << n2 << std::endl; + if(n1 == n2) { + return true; + } + if(n1.getType().isFunction() && n2.hasOperator()) { + if(ProofManager::currentPM()->hasOp(n2.getOperator())) { + return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator()); + } else { + return n1 == n2.getOperator(); + } + } + if(n2.getType().isFunction() && n1.hasOperator()) { + if(ProofManager::currentPM()->hasOp(n1.getOperator())) { + return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator()); + } else { + return n2 == n1.getOperator(); + } + } + if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) { + return false; + } + for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) { + if(n1[i] != n2[i]) { + return false; + } + } + return true; +} + + +void ProofUF::toStream(std::ostream& out) { + Trace("theory-proof-debug") << "; Print UF proof..." << std::endl; + //AJR : carry this further? + LetMap map; + toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map); +} + +void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) { + Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl; + pf->debug_print("lfsc-uf"); + Debug("lfsc-uf") << std::endl; + toStreamRecLFSC( out, tp, pf, 0, map ); +} + +Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) { + Debug("gk::proof") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl; + pf->debug_print("gk::proof"); + Debug("gk::proof") << std::endl; + + if(tb == 0) { + Assert(pf->d_id == eq::MERGED_THROUGH_TRANS); + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.size() >= 2); + + int neg = -1; + theory::eq::EqProof subTrans; + subTrans.d_id = eq::MERGED_THROUGH_TRANS; + subTrans.d_node = pf->d_node; + + size_t i = 0; + while (i < pf->d_children.size()) { + // Look for the negative clause, with which we will form a contradiction. + if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { + Assert(neg < 0); + neg = i; + ++i; + } + + // Handle congruence closures over equalities. + else if (pf->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) { + Debug("gk::proof") << "Handling congruence over equalities" << std::endl; + + // Gather the sequence of consecutive congruence closures. + std::vector congruenceClosures; + unsigned count; + Debug("gk::proof") << "Collecting congruence sequence" << std::endl; + for (count = 0; + i + count < pf->d_children.size() && + pf->d_children[i + count]->d_id==eq::MERGED_THROUGH_CONGRUENCE && + pf->d_children[i + count]->d_node.isNull(); + ++count) { + Debug("gk::proof") << "Found a congruence: " << std::endl; + pf->d_children[i+count]->debug_print("gk::proof"); + congruenceClosures.push_back(pf->d_children[i+count]); + } + + Debug("gk::proof") << "Total number of congruences found: " << congruenceClosures.size() << std::endl; + + // Determine if the "target" of the congruence sequence appears right before or right after the sequence. + bool targetAppearsBefore = true; + bool targetAppearsAfter = true; + + if ((i == 0) || (i == 1 && neg == 0)) { + Debug("gk::proof") << "Target does not appear before" << std::endl; + targetAppearsBefore = false; + } + + if ((i + count >= pf->d_children.size()) || + (!pf->d_children[i + count]->d_node.isNull() && + pf->d_children[i + count]->d_node.getKind() == kind::NOT)) { + Debug("gk::proof") << "Target does not appear after" << std::endl; + targetAppearsAfter = false; + } + + // Assert that we have precisely one target clause. + Assert(targetAppearsBefore != targetAppearsAfter); + + // Begin breaking up the congruences and ordering the equalities correctly. + std::vector orderedEqualities; + + + // Insert target clause first. + if (targetAppearsBefore) { + orderedEqualities.push_back(pf->d_children[i - 1]); + // The target has already been added to subTrans; remove it. + subTrans.d_children.pop_back(); + } else { + orderedEqualities.push_back(pf->d_children[i + count]); + } + + // Start with the congruence closure closest to the target clause, and work our way back/forward. + if (targetAppearsBefore) { + for (unsigned j = 0; j < count; ++j) { + if (pf->d_children[i + j]->d_children[0]->d_id != eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); + if (pf->d_children[i + j]->d_children[1]->d_id != eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + } + } else { + for (unsigned j = 0; j < count; ++j) { + if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]); + if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != eq::MERGED_THROUGH_REFLEXIVITY) + orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]); + } + } + + // Copy the result into the main transitivity proof. + subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end()); + + // Increase i to skip over the children that have been processed. + i += count; + if (targetAppearsAfter) { + ++i; + } + } + + // Else, just copy the child proof as is + else { + subTrans.d_children.push_back(pf->d_children[i]); + ++i; + } + } + Assert(neg >= 0); + + Node n1; + std::stringstream ss; + //Assert(subTrans.d_children.size() == pf->d_children.size() - 1); + Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n"; + if(pf->d_children.size() > 2) { + n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map); + } else { + n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map); + Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl; + } + + Node n2 = pf->d_children[neg]->d_node; + Assert(n2.getKind() == kind::NOT); + out << "(clausify_false (contra _ "; + Debug("mgdx") << "\nhave proven: " << n1 << std::endl; + Debug("mgdx") << "n2 is " << n2[0] << std::endl; + + if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; } + if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; } + + if(n2[0].getKind() == kind::APPLY_UF) { + out << "(trans _ _ _ _ "; + out << "(symm _ _ _ "; + out << ss.str(); + out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; + } else { + Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); + if(n1[1] == n2[0][0]) { + out << "(symm _ _ _ " << ss.str() << ")"; + } else { + out << ss.str(); + } + out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl; + } + return Node(); + } + + switch(pf->d_id) { + case eq::MERGED_THROUGH_CONGRUENCE: { + Debug("mgd") << "\nok, looking at congruence:\n"; + pf->debug_print("mgd"); + std::stack stk; + for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + Assert(!pf2->d_node.isNull()); + Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE); + Assert(pf2->d_children.size() == 2); + out << "(cong _ _ _ _ _ _ "; + stk.push(pf2); + } + Assert(stk.top()->d_children[0]->d_id != eq::MERGED_THROUGH_CONGRUENCE); + NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF); + const theory::eq::EqProof* pf2 = stk.top(); + stk.pop(); + Assert(pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE); + Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map); + out << " "; + std::stringstream ss; + Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n"; + pf2->debug_print("mgd"); + Debug("mgd") << "looking at " << pf2->d_node << "\n"; + Debug("mgd") << " " << n1 << "\n"; + Debug("mgd") << " " << n2 << "\n"; + int side = 0; + if(match(pf2->d_node, n1[0])) { + //if(tb == 1) { + Debug("mgd") << "SIDE IS 0\n"; + //} + side = 0; + } else { + //if(tb == 1) { + Debug("mgd") << "SIDE IS 1\n"; + //} + if(!match(pf2->d_node, n1[1])) { + Debug("mgd") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("mgd"); + } + Assert(match(pf2->d_node, n1[1])); + side = 1; + } + if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) { + if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) { + b1 << n1[side].getOperator(); + } else { + b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator()); + } + b1.append(n1[side].begin(), n1[side].end()); + } else { + b1 << n1[side]; + } + if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) { + if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) { + b2 << n1[1-side].getOperator(); + } else { + b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator()); + } + b2.append(n1[1-side].begin(), n1[1-side].end()); + } else { + b2 << n1[1-side]; + } + Debug("mgd") << "pf2->d_node " << pf2->d_node << std::endl; + Debug("mgd") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl; + Debug("mgd") << "n1 " << n1 << std::endl; + Debug("mgd") << "n2 " << n2 << std::endl; + Debug("mgd") << "side " << side << std::endl; + if(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) { + b1 << n2[side]; + b2 << n2[1-side]; + out << ss.str(); + } else { + Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]); + b1 << n2[1-side]; + b2 << n2[side]; + out << "(symm _ _ _ " << ss.str() << ")"; + } + out << ")"; + while(!stk.empty()) { + if(tb == 1) { + Debug("mgd") << "\nMORE TO DO\n"; + } + pf2 = stk.top(); + stk.pop(); + Assert(pf2->d_id == eq::MERGED_THROUGH_CONGRUENCE); + out << " "; + ss.str(""); + n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map); + Debug("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n"; + Debug("mgd") << "looking at " << pf2->d_node << "\n"; + Debug("mgd") << " " << n1 << "\n"; + Debug("mgd") << " " << n2 << "\n"; + Debug("mgd") << " " << b1 << "\n"; + Debug("mgd") << " " << b2 << "\n"; + if(pf2->d_node[b1.getNumChildren()] == n2[side]) { + b1 << n2[side]; + b2 << n2[1-side]; + out << ss.str(); + } else { + Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]); + b1 << n2[1-side]; + b2 << n2[side]; + out << "(symm _ _ _ " << ss.str() << ")"; + } + out << ")"; + } + n1 = b1; + n2 = b2; + Debug("mgd") << "at end assert, got " << pf2->d_node << " and " << n1 << std::endl; + if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) { + Assert(n1 == pf2->d_node); + } + if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) { + if(ProofManager::currentPM()->hasOp(n1.getOperator())) { + b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); + } else { + b1.clear(kind::APPLY_UF); + b1 << n1.getOperator(); + } + b1.append(n1.begin(), n1.end()); + n1 = b1; + Debug("mgd") << "at[2] end assert, got " << pf2->d_node << " and " << n1 << std::endl; + if(pf2->d_node.getKind() == kind::APPLY_UF) { + Assert(n1 == pf2->d_node); + } + } + if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) { + if(ProofManager::currentPM()->hasOp(n2.getOperator())) { + b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst()); + } else { + b2.clear(kind::APPLY_UF); + b2 << n2.getOperator(); + } + b2.append(n2.begin(), n2.end()); + n2 = b2; + } + Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); + if(tb == 1) { + Debug("mgdx") << "\ncong proved: " << n << "\n"; + } + return n; + } + + case eq::MERGED_THROUGH_REFLEXIVITY: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + out << "(refl _ "; + tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map); + out << ")"; + return eqNode(pf->d_node, pf->d_node); + + case eq::MERGED_THROUGH_EQUALITY: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + out << ProofManager::getLitName(pf->d_node.negate()); + return pf->d_node; + + case eq::MERGED_THROUGH_TRANS: { + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.size() >= 2); + std::stringstream ss; + Debug("mgd") << "\ndoing trans proof[[\n"; + pf->debug_print("mgd"); + Debug("mgd") << "\n"; + Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); + Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; + if(tb == 1) { + Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; + } + + bool identicalEqualities = false; + bool evenLengthSequence; + Node nodeAfterEqualitySequence; + + for(size_t i = 1; i < pf->d_children.size(); ++i) { + std::stringstream ss1(ss.str()), ss2; + ss.str(""); + Node n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map); + + // The following branch is dedicated to handling sequences of identical equalities, + // i.e. trans[ a=b, a=b, a=b ]. + // + // There are two cases: + // 1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality, + // i.e. a=b. + // 2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this, + // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs + // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, + // and use it to determine which option we need. + if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { + // We are in a sequence of identical equalities + + Debug("gk::proof") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl; + + if (!identicalEqualities) { + // The sequence of identical equalities has started just now + identicalEqualities = true; + + Debug("gk::proof") << "The sequence is just beginning. Determining length..." << std::endl; + + // Determine whether the length of this sequence is odd or even. + evenLengthSequence = true; + bool sequenceOver = false; + size_t j = i + 1; + + while (j < pf->d_children.size() && !sequenceOver) { + std::stringstream dontCare; + nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map ); + + if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || + ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) { + evenLengthSequence = !evenLengthSequence; + } else { + sequenceOver = true; + } + + ++j; + } + + if (evenLengthSequence) { + // If the length is even, we need to apply transitivity for the "correct" hand of the equality. + + Debug("gk::proof") << "Equality sequence of even length" << std::endl; + Debug("gk::proof") << "n1 is: " << n1 << std::endl; + Debug("gk::proof") << "n2 is: " << n2 << std::endl; + Debug("gk::proof") << "pf-d_node is: " << pf->d_node << std::endl; + Debug("gk::proof") << "Next node is: " << nodeAfterEqualitySequence << std::endl; + + ss << "(trans _ _ _ _ "; + + // If the sequence is at the very end of the transitivity proof, use pf->d_node to guide us. + if (!sequenceOver) { + if (match(n1[0], pf->d_node[0])) { + n1 = eqNode(n1[0], n1[0]); + ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; + } else if (match(n1[1], pf->d_node[1])) { + n1 = eqNode(n1[1], n1[1]); + ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); + } else { + Debug("gk::proof") << "Error: identical equalities over, but hands don't match what we're proving." + << std::endl; + Assert(false); + } + } else { + // We have a "next node". Use it to guide us. + + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || + nodeAfterEqualitySequence.getKind() == kind::IFF); + + if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { + + // Eliminate n1[1] + ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")"; + n1 = eqNode(n1[0], n1[0]); + + } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) { + + // Eliminate n1[0] + ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); + n1 = eqNode(n1[1], n1[1]); + + } else { + Debug("gk::proof") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl; + Assert(false); + } + } + + ss << ")"; + + } else { + Debug("gk::proof") << "Equality sequence length is odd!" << std::endl; + ss.str(ss1.str()); + } + + Debug("gk::proof") << "Have proven: " << n1 << std::endl; + } else { + ss.str(ss1.str()); + } + + // Ignore the redundancy. + continue; + } + } + + if (identicalEqualities) { + // We were in a sequence of identical equalities, but it has now ended. Resume normal operation. + identicalEqualities = false; + } + + Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; + if(tb == 1) { + Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; + Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + + if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { + Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; + Debug("mgdx") << n1[0].getId() << " " << n1[0] << "\n"; + Debug("mgdx") << n1[1].getId() << " " << n1[1] << "\n"; + Debug("mgdx") << n2[0].getId() << " " << n2[0] << "\n"; + Debug("mgdx") << n2[1].getId() << " " << n2[1] << "\n"; + Debug("mgdx") << (n1[0] == n2[0]) << "\n"; + Debug("mgdx") << (n1[1] == n2[1]) << "\n"; + Debug("mgdx") << (n1[0] == n2[1]) << "\n"; + Debug("mgdx") << (n1[1] == n2[0]) << "\n"; + } + } + ss << "(trans _ _ _ _ "; + + if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && + (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + // Both elements of the transitivity rule are equalities/iffs + { + if(n1[0] == n2[0]) { + if(tb == 1) { Debug("mgdx") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); + } else if(n1[1] == n2[1]) { + if(tb == 1) { Debug("mgdx") << "case 2\n"; } + n1 = eqNode(n1[0], n2[0]); + ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")"; + } else if(n1[0] == n2[1]) { + if(tb == 1) { Debug("mgdx") << "case 3\n"; } + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + if(tb == 1) { Debug("mgdx") << "++ proved " << n1 << "\n"; } + } else if(n1[1] == n2[0]) { + if(tb == 1) { Debug("mgdx") << "case 4\n"; } + n1 = eqNode(n1[0], n2[1]); + ss << ss1.str() << " " << ss2.str(); + } else { + Warning() << "\n\ntrans proof failure at step " << i << "\n\n"; + Warning() << "0 proves " << n1 << "\n"; + Warning() << "1 proves " << n2 << "\n\n"; + pf->debug_print("mgdx",0); + //toStreamRec(Warning.getStream(), pf, 0); + Warning() << "\n\n"; + Unreachable(); + } + Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl; + } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + // n1 is an equality/iff, but n2 is a predicate + if(n1[0] == n2) { + n1 = n1[1]; + ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; + } else if(n1[1] == n2) { + n1 = n1[0]; + ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; + } else { + Unreachable(); + } + } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + // n2 is an equality/iff, but n1 is a predicate + if(n2[0] == n1) { + n1 = n2[1]; + ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; + } else if(n2[1] == n1) { + n1 = n2[0]; + ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; + } else { + Unreachable(); + } + } else { + // Both n1 and n2 are prediacates. Don't know what to do... + Unreachable(); + } + + ss << ")"; + } + out << ss.str(); + Debug("mgd") << "\n++ trans proof done, have proven " << n1 << std::endl; + return n1; + } + + case eq::MERGED_ARRAYS_ROW: { + Debug("mgd") << "row lemma: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + TNode t1, t2, t3, t4; + Node ret; + if(pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0].getKind() == kind::STORE && + pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0] == pf->d_node[1][0][0] && + pf->d_node[0][1] == pf->d_node[1][1]) { + t2 = pf->d_node[1][0][1]; + t3 = pf->d_node[1][1]; + t1 = pf->d_node[0][0]; + t4 = pf->d_node[1][0][2]; + ret = pf->d_node[1].eqNode(pf->d_node[0]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + } else { + Assert(pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0].getKind() == kind::STORE && + pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0] == pf->d_node[0][0][0] && + pf->d_node[1][1] == pf->d_node[0][1]); + t2 = pf->d_node[0][0][1]; + t3 = pf->d_node[0][1]; + t1 = pf->d_node[1][0]; + t4 = pf->d_node[0][0][2]; + ret = pf->d_node; + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n"; + } + out << "(row _ _ "; + tp->printTerm(t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << " "; + tp->printTerm(t1.toExpr(), out, map); + out << " "; + tp->printTerm(t4.toExpr(), out, map); + out << " " << ProofManager::getLitName(t2.eqNode(t3)) << ")"; + return ret; + } + + case eq::MERGED_ARRAYS_ROW1: { + Debug("mgd") << "row1 lemma: " << pf->d_node << std::endl; + Assert(pf->d_node.getKind() == kind::EQUAL); + TNode t1, t2, t3; + Node ret; + if(pf->d_node[1].getKind() == kind::SELECT && + pf->d_node[1][0].getKind() == kind::STORE && + pf->d_node[1][0][1] == pf->d_node[1][1] && + pf->d_node[1][0][2] == pf->d_node[0]) { + t1 = pf->d_node[1][0][0]; + t2 = pf->d_node[1][0][1]; + t3 = pf->d_node[0]; + ret = pf->d_node[1].eqNode(pf->d_node[0]); + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + } else { + Assert(pf->d_node[0].getKind() == kind::SELECT && + pf->d_node[0][0].getKind() == kind::STORE && + pf->d_node[0][0][1] == pf->d_node[0][1] && + pf->d_node[0][0][2] == pf->d_node[1]); + t1 = pf->d_node[0][0][0]; + t2 = pf->d_node[0][0][1]; + t3 = pf->d_node[1]; + ret = pf->d_node; + Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\n"; + } + out << "(row1 _ _ "; + tp->printTerm(t1.toExpr(), out, map); + out << " "; + tp->printTerm(t2.toExpr(), out, map); + out << " "; + tp->printTerm(t3.toExpr(), out, map); + out << ")"; + return ret; + } + + default: + Assert(!pf->d_node.isNull()); + Assert(pf->d_children.empty()); + Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl; + AlwaysAssert(false); + return pf->d_node; + } +} + +UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe) + : TheoryProof(uf, pe) +{} + +void UFProof::registerTerm(Expr term) { + // already registered + if (d_declarations.find(term) != d_declarations.end()) + return; + + Type type = term.getType(); + if (type.isSort()) { + // declare uninterpreted sorts + d_sorts.insert(type); + } + + if (term.getKind() == kind::APPLY_UF) { + Expr function = term.getOperator(); + d_declarations.insert(function); + } + + if (term.isVariable()) { + d_declarations.insert(term); + } + + // recursively declare all other terms + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + // could belong to other theories + d_proofEngine->registerTerm(term[i]); + } +} + +void LFSCUFProof::printTerm(Expr term, std::ostream& os, const LetMap& map) { + Assert (Theory::theoryOf(term) == THEORY_UF); + + if (term.getKind() == kind::VARIABLE || + term.getKind() == kind::SKOLEM) { + os << term; + return; + } + + Assert (term.getKind() == kind::APPLY_UF); + + if(term.getType().isBoolean()) { + os << "(p_app "; + } + Expr func = term.getOperator(); + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os << "(apply _ _ "; + } + os << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os, map); + os << ")"; + } + if(term.getType().isBoolean()) { + os << ")"; + } +} + +void LFSCUFProof::printSort(Type type, std::ostream& os) { + Assert (type.isSort()); + os << type <<" "; +} + +void LFSCUFProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren) { + os << " ;; UF Theory Lemma \n;;"; + for (unsigned i = 0; i < lemma.size(); ++i) { + os << lemma[i] <<" "; + } + os <<"\n"; + //os << " (clausify_false trust)"; + UFProof::printTheoryLemmaProof( lemma, os, paren ); +} + +void LFSCUFProof::printDeclarations(std::ostream& os, std::ostream& paren) { + // declaring the sorts + for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) { + os << "(% " << *it << " sort\n"; + paren << ")"; + } + + // declaring the terms + for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { + Expr term = *it; + + os << "(% " << ProofManager::sanitize(term) << " "; + os << "(term "; + + Type type = term.getType(); + if (type.isFunction()) { + std::ostringstream fparen; + FunctionType ftype = (FunctionType)type; + std::vector args = ftype.getArgTypes(); + args.push_back(ftype.getRangeType()); + os << "(arrow"; + for (unsigned i = 0; i < args.size(); i++) { + Type arg_type = args[i]; + os << " " << arg_type; + if (i < args.size() - 2) { + os << " (arrow"; + fparen << ")"; + } + } + os << fparen.str() << "))\n"; + } else { + Assert (term.isVariable()); + os << type << ")\n"; + } + paren << ")"; + } +} diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h new file mode 100644 index 000000000..121db1fcd --- /dev/null +++ b/src/proof/uf_proof.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file uf_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** 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 + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief UF proof + ** + ** UF proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__UF__PROOF_H +#define __CVC4__UF__PROOF_H + +#include "expr/expr.h" +#include "proof/proof_manager.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { + +//proof object outputted by TheoryUF +class ProofUF : public Proof { +private: + static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map); +public: + ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {} + //it is simply an equality engine proof + theory::eq::EqProof * d_proof; + void toStream(std::ostream& out); + static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map); +}; + + +namespace theory { +namespace uf { +class TheoryUF; +} +} + +typedef __gnu_cxx::hash_set TypeSet; + + +class UFProof : public TheoryProof { +protected: + TypeSet d_sorts; // all the uninterpreted sorts in this theory + ExprSet d_declarations; // all the variable/function declarations + +public: + UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine); + + virtual void registerTerm(Expr term); +}; + +class LFSCUFProof : public UFProof { +public: + LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) + : UFProof(uf, proofEngine) + {} + virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printSort(Type type, std::ostream& os); + virtual void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); +}; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__UF__PROOF_H */ -- cgit v1.2.3