summaryrefslogtreecommitdiff
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/array_proof.h78
-rw-r--r--src/proof/bitvector_proof.cpp602
-rw-r--r--src/proof/bitvector_proof.h142
-rw-r--r--src/proof/cnf_proof.cpp1049
-rw-r--r--src/proof/cnf_proof.h136
-rw-r--r--src/proof/proof.h21
-rw-r--r--src/proof/proof_manager.cpp546
-rw-r--r--src/proof/proof_manager.h196
-rw-r--r--src/proof/proof_utils.cpp127
-rw-r--r--src/proof/proof_utils.h178
-rw-r--r--src/proof/sat_proof.h291
-rw-r--r--src/proof/sat_proof_implementation.h1100
-rw-r--r--src/proof/theory_proof.cpp684
-rw-r--r--src/proof/theory_proof.h282
-rw-r--r--src/proof/uf_proof.cpp804
-rw-r--r--src/proof/uf_proof.h75
16 files changed, 5269 insertions, 1042 deletions
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<Expr>& 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<Expr>& 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<bool>(true);
+ Node false_node = NodeManager::currentNM()->mkConst<bool>(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<Node>* 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> 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"<<clause_id<< " => " << conflict << "\n";
+ d_isAssumptionConflict = false;
+}
+
+void BitVectorProof::finalizeConflicts(std::vector<Expr>& 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<BitVectorBitOf>().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<BitVectorRepeat>().repeatAmount;
+ os << amount <<" _ ";
+ }
+ if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
+ unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+ os << amount <<" _ ";
+ }
+
+ if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
+ unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().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 "<<width<<")";
+}
+
+void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& 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"<<bb_var<<"\n";
+ lemma_paren <<")";
+ }
+ Expr lem = utils::mkOr(lemma);
+ Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end());
+ ClauseId lemma_id = d_bbConflictMap[lem];
+ d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
+ os <<lemma_paren.str();
+ }else{
+ Debug("bv-proof") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl;
+ BitVectorProof::printTheoryLemmaProof( lemma, os, paren );
+ }
+}
+void LFSCBitVectorProof::printDeclarations(std::ostream& os, std::ostream& paren) {
+ ExprSet::const_iterator it = d_declarations.begin();
+ ExprSet::const_iterator end = d_declarations.end();
+ for (; it != end; ++it) {
+ os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n";
+ paren <<")";
+ }
+}
+
+
+void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
+ // TODO: once we have the operator elimination rules remove those that we
+ // eliminated
+ Assert (term.getType().isBitVector());
+ Kind kind = term.getKind();
+
+ if (Theory::isLeafOf(term, theory::THEORY_BV) &&
+ !term.isConst()) {
+ os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )";
+ return;
+ }
+
+ switch(kind) {
+ case kind::CONST_BITVECTOR : {
+ os << "(bv_bbl_const "<< 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();
+ 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_"<<utils::toLFSCKind(kind);
+ os <<" _ _ _ _ ";
+ os << getBBTermName(term[0]);
+ os <<")";
+ return;
+ }
+ case kind::BITVECTOR_EXTRACT : {
+ os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
+ os << utils::getSize(term) << " ";
+ os << utils::getExtractHigh(term) << " ";
+ os << utils::getExtractLow(term) << " ";
+ os << " _ _ _ _ ";
+ os << getBBTermName(term[0]);
+ os <<")";
+ return;
+ }
+ case kind::BITVECTOR_REPEAT :
+ case kind::BITVECTOR_ZERO_EXTEND :
+ case kind::BITVECTOR_SIGN_EXTEND : {
+ os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
+ os << utils::getSize(term) <<" ";
+ if (term.getKind() == kind::BITVECTOR_REPEAT) {
+ unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+ os << amount;
+ }
+ if (term.getKind() == kind::BITVECTOR_SIGN_EXTEND) {
+ unsigned amount = term.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+ os << amount;
+ }
+
+ if (term.getKind() == kind::BITVECTOR_ZERO_EXTEND) {
+ unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().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<Node> 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<Expr>::const_iterator it = d_bbTerms.begin();
+ std::vector<Expr>::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<bool>();
+ 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 <cstdint>
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include <iostream>
+#include <set>
+#include <sstream>
+#include <vector>
+
+#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 T> class TBitblaster;
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+
+class CnfProof;
+} /* namespace CVC4 */
+
+namespace CVC4 {
+
+template <class Solver> class TSatProof;
+typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
+
+template <class Solver> class LFSCSatProof;
+typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
+
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
+typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
+typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> 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<Expr> 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<Node>* 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<Node>* bb);
+
+ BVSatProof* getSatProof();
+ CnfProof* getCnfProof() {return d_cnfProof; }
+ void finalizeConflicts(std::vector<Expr>& 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<Expr>& 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<Node>, NodeHashFunction >::const_iterator it = ProofManager::currentPM()->begin_deps();
- __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end = ProofManager::currentPM()->end_deps();
+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<Node, unsigned>& childIndex,
+ std::map<Node, bool>& childPol ) {
std::vector< Node > children;
for (unsigned i = 0; i < clause.size(); ++i) {
prop::SatLiteral lit = clause[i];
prop::SatVariable var = lit.getSatVariable();
- Node atom = Node::fromExpr( getAtom(var) );
+ 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<Node, unsigned > childIndex;
+ std::map<Node, bool > 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<base_assertion.getNumChildren(); j++ ){
- Expr child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j];
- bool child_pol = base_assertion[j].getKind()!=kind::NOT;
- if( j==0 && base_assertion.getKind()==kind::IMPLIES ){
- child_pol = !child_pol;
+ if( childPol[child_base] && base_pol){
+ os << os_main.str() << " " << ProofManager::getLitName(lit, d_name);
+ }else{
+ os << ProofManager::getLitName(lit, d_name) << " " << os_main.str();
+ }
+ os << ")";
+ }else{
+ success = false;
+ }
+ }
+ }else if ((base_assertion.getKind()==kind::AND && base_pol) ||
+ ((base_assertion.getKind()==kind::OR ||
+ base_assertion.getKind()==kind::IMPLIES) && !base_pol)) {
+
+ std::stringstream os_main;
+
+ Node iatom;
+ if (is_in_clause) {
+ Assert( assertion.getNumChildren()==2 );
+ iatom = assertion[ base_index==0 ? 1 : 0];
+ } else {
+ Assert( assertion.getNumChildren()==1 );
+ iatom = assertion[0];
+ }
+
+ Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl;
+ Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom;
+ bool e_pol = iatom.getKind()!=kind::NOT;
+ std::map< Node, unsigned >::iterator itcic = childIndex.find( e_base );
+ if( itcic!=childIndex.end() ){
+ prop::SatLiteral lit = (*clause)[itcic->second];
+ //eliminate until we find iatom
+ for( unsigned j=0; j<base_assertion.getNumChildren(); j++ ){
+ 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;
+ }
+ if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){
+ success = true;
+ bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol );
+ if( elimNn ){
+ os_main << "(not_not_elim _ ";
}
- if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){
- success = true;
- bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol );
- if( elimNn ){
- os_main << "(not_not_elim _ ";
- }
- std::stringstream os_paren;
- if( j+1<base_assertion.getNumChildren() ){
- os_main << "(and_elim_1 _ _ ";
- if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
- os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
- os_paren << ")";
- }
+ std::stringstream os_paren;
+ if( j+1<base_assertion.getNumChildren() ){
+ os_main << "(and_elim_1 _ _ ";
+ if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
+ os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
os_paren << ")";
}
- for( unsigned k=0; k<j; k++ ){
- os_main << "(and_elim_2 _ _ ";
- if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
- os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
- os_paren << ")";
- }
+ os_paren << ")";
+ }
+ for( unsigned k=0; k<j; k++ ){
+ os_main << "(and_elim_2 _ _ ";
+ if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
+ os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
os_paren << ")";
}
- os_main << os_base.str() << os_paren.str();
- if( elimNn ){
- os_main << ")";
- }
- break;
+ os_paren << ")";
}
- }
- if( success ){
- os << "(contra _ ";
- if( !e_pol ){
- os << ProofManager::getLitName(lit) << " " << os_main.str();
- }else{
- os << os_main.str() << " " << ProofManager::getLitName(lit);
+ os_main << os_base.str() << os_paren.str();
+ if( elimNn ){
+ os_main << ")";
}
- os << ")";
- }
- }
- }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){
- //eliminate negation
- int num_nots_2 = 0;
- int num_nots_1 = 0;
- Kind k;
- if( !base_pol ){
- if( base_assertion.getKind()==kind::IFF ){
- num_nots_2 = 1;
- }
- k = kind::IFF;
- }else{
- k = base_assertion.getKind();
- }
- std::vector< unsigned > indices;
- std::vector< bool > pols;
- success = true;
- int elimNum = 0;
- for( unsigned i=0; i<2; i++ ){
- Expr child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i];
- bool child_pol = base_assertion[i].getKind()!=kind::NOT;
- std::map< Expr, unsigned >::iterator itcic = childIndex.find( child_base );
- if( itcic!=childIndex.end() ){
- indices.push_back( itcic->second );
- pols.push_back( childPol[child_base] );
- if( i==0 ){
- //figure out which way to elim
- elimNum = child_pol==childPol[child_base] ? 2 : 1;
- if( (elimNum==2)==(k==kind::IFF) ){
- num_nots_2++;
- }
- if( elimNum==1 ){
- num_nots_1++;
- }
- }
- }else{
- success = false;
break;
}
}
- Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl;
if( success ){
os << "(contra _ ";
- std::stringstream os_base_n;
- if( num_nots_2==2 ){
- os_base_n << "(not_not_elim _ ";
- }
- os_base_n << "(or_elim_1 _ _ ";
- prop::SatLiteral lit1 = (*clause)[indices[0]];
- if( !pols[0] || num_nots_1==1 ){
- os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1) << ") ";
- }else{
- os_base_n << ProofManager::getLitName(lit1) << " ";
- }
- Assert( elimNum!=0 );
- os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
- if( !base_pol ){
- os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
- }else{
- os_base_n << os_base.str();
- }
- os_base_n << "))";
- if( num_nots_2==2 ){
- os_base_n << ")";
- num_nots_2 = 0;
- }
- prop::SatLiteral lit2 = (*clause)[indices[1]];
- if( pols[1]==(num_nots_2==0) ){
- os << os_base_n.str() << " ";
- if( num_nots_2==1 ){
- os << "(not_not_intro _ " << ProofManager::getLitName(lit2) << ")";
- }else{
- os << ProofManager::getLitName(lit2);
- }
+ 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<parent_base.getNumChildren(); i++ ){
+ Node child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i];
+ bool child_pol = parent_base[i].getKind()!=kind::NOT;
+ if( parent_base.getKind()==kind::IMPLIES && i==0 ){
+ child_pol = !child_pol;
+ }
+ if (e_base==child_base &&
+ (e_pol==child_pol)==(parent_base.getKind()==kind::AND)) {
+ bool elimNn = ((parent_base.getKind()==kind::OR ||
+ (parent_base.getKind()==kind::IMPLIES && i==1)) && e_pol);
+ if (elimNn) {
+ out << "(not_not_elim _ ";
+ }
+ std::stringstream out_paren;
+ if (i+1 < parent_base.getNumChildren()) {
+ out << "(and_elim_1 _ _ ";
+ if( parent_base.getKind()==kind::OR ||
+ parent_base.getKind()==kind::IMPLIES ){
+ out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" )
+ << "_elim _ _ ";
+ out_paren << ")";
+ }
+ out_paren << ")";
+ }
+ for( unsigned j=0; j<i; j++ ){
+ out << "(and_elim_2 _ _ ";
+ if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
+ out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
+ out_paren << ")";
+ }
+ out_paren << ")";
+ }
+ out << out_parent.str();
+ out << out_paren.str();
+ if( elimNn ){
+ out << ")";
+ }
+ return true;
+ }
+ }
+ } else {
+ Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
+ << " is not correct type (" << parent << ")" << std::endl;
+ }
+ } else {
+ Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
+ << " is not input" << std::endl;
+ }
+ } else {
+ Trace("cnf-pf-debug") << "; isInputAssertion : " << e
+ << " has no parent" << std::endl;
+ }
+ return false;
+ } else {
+ out << ProofManager::getPreprocessedAssertionName(e);
+ return true;
+ }
+}
+
+
+
} /* CVC4 namespace */
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index d3e59ef93..675bd9b9d 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,11 +21,14 @@
#ifndef __CVC4__CNF_PROOF_H
#define __CVC4__CNF_PROOF_H
-#include <ext/hash_map>
+#include <ext/hash_map>
#include <ext/hash_set>
#include <iosfwd>
+#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<prop::SatVariable, Expr> SatVarToExpr;
+typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode;
+typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
+
+typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
+typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> 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<Node> d_currentAssertionStack;
+
+ /** Top of stack is top-level fact currently being converted to CNF **/
+ std::vector<Node> 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<Node, unsigned>& childIndex,
+ std::map<Node, bool>& 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<bool>(true);
+ Node false_node = NodeManager::currentNM()->mkConst<bool>(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<bool>(true)) ||
+ (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(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; i<parent_base.getNumChildren(); i++ ){
- Expr child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i];
- bool child_pol = parent_base[i].getKind()!=kind::NOT;
- if( parent_base.getKind()==kind::IMPLIES && i==0 ){
- child_pol = !child_pol;
- }
- if( e_base==child_base && (e_pol==child_pol)==(parent_base.getKind()==kind::AND) ){
- bool elimNn = ( ( parent_base.getKind()==kind::OR || ( parent_base.getKind()==kind::IMPLIES && i==1 ) ) && e_pol );
- if( elimNn ){
- out << "(not_not_elim _ ";
- }
- std::stringstream out_paren;
- if( i+1<parent_base.getNumChildren() ){
- out << "(and_elim_1 _ _ ";
- if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
- out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
- out_paren << ")";
- }
- out_paren << ")";
- }
- for( unsigned j=0; j<i; j++ ){
- out << "(and_elim_2 _ _ ";
- if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
- out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
- out_paren << ")";
- }
- out_paren << ")";
- }
- out << out_parent.str();
- out << out_paren.str();
- if( elimNn ){
- out << ")";
- }
- return true;
- }
- }
- }else{
- Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e << " is not correct type (" << parent << ")" << std::endl;
- }
- }else{
- Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e << " is not input" << std::endl;
- }
- }else{
- Trace("cnf-pf-debug") << "; isInputAssertion : " << e << " has no parent" << std::endl;
- }
- return false;
- }else{
- out << "A" << itp->second;
- return true;
+ // 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<Node, Node>::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<TypeNode> v;
+ v.push_back(NodeManager::currentNM()->integerType());
+ if(n.getConst<Kind>() == kind::SELECT) {
+ v.push_back(NodeManager::currentNM()->integerType());
+ v.push_back(NodeManager::currentNM()->integerType());
+ } else if(n.getConst<Kind>() == 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 Solver> class TSatProof;
+typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof;
+
class CnfProof;
+class RewriterProof;
+class TheoryProofEngine;
class TheoryProof;
+class UFProof;
+class ArrayProof;
+class BitVectorProof;
+
+template <class Solver> class LFSCSatProof;
+typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof;
-class LFSCSatProof;
class LFSCCnfProof;
-class LFSCTheoryProof;
+class LFSCTheoryProofEngine;
+class LFSCUFProof;
+class LFSCBitVectorProof;
+class LFSCRewriterProof;
+
+template <class Solver> 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<prop::SatVariable > VarSet;
+typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
+typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
+typedef std::hash_set<ClauseId> 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<Node>, 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<Node>, NodeHashFunction >::const_iterator begin_deps() const { return d_deps.begin(); }
- __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end_deps() const { return d_deps.end(); }
-
- clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
- clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
- size_t num_input_clauses() const { return d_inputClauses.size(); }
-
- 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<Node, Node> d_ops;
+ std::map<Node, Node> 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 <set>
+#include <vector>
+#include <sstream>
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+
+namespace utils {
+
+std::string toLFSCKind(Kind kind);
+
+inline unsigned getExtractHigh(Expr node) {
+ return node.getOperator().getConst<BitVectorExtract>().high;
+}
+
+inline unsigned getExtractLow(Expr node) {
+ return node.getOperator().getConst<BitVectorExtract>().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<bool>(true);
+}
+
+inline Expr mkFalse() {
+ return NodeManager::currentNM()->toExprManager()->mkConst<bool>(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<Expr>& children) {
+ return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
+}
+
+
+inline Expr mkOnes(unsigned size) {
+ BitVector val = mkBitVectorOnes(size);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+}
+
+inline Expr mkConst(unsigned size, unsigned int value) {
+ BitVector val(size, value);
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
+}
+
+inline Expr mkConst(const BitVector& value) {
+ return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(value);
+}
+
+inline Expr mkOr(const std::vector<Expr>& nodes) {
+ std::set<Expr> 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<Expr>::const_iterator it = all.begin();
+ std::set<Expr>::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<Expr>& conjunctions) {
+ std::set<Expr> 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<Expr>::const_iterator it = all.begin();
+ std::set<Expr>::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<Expr>& children) {
+ std::set<Expr> 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<Expr>::const_iterator it = all.begin();
+ std::set<Expr>::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<BitVector>().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 <stdint.h>
-
#include <ext/hash_map>
#include <ext/hash_set>
#include <iosfwd>
#include <set>
#include <sstream>
#include <vector>
-
#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 <class Solver> void printDebug(typename Solver::TLit l);
+template <class Solver> 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 <class Solver>
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 Solver>
class ResChain {
+public:
+ typedef std::vector< ResStep<Solver> > 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 <ClauseId, prop::SatClause* > IdToSatClause;
-typedef std::set < ClauseId > IdSet;
-typedef std::vector < Minisat::Lit > LitVector;
-typedef __gnu_cxx::hash_map<ClauseId, Minisat::Clause& > 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 Solver> class ProofProxy;
class CnfProof;
-class SatProof {
+template<class Solver>
+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<Solver>* > IdResMap;
+ typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap;
+ typedef std::vector < ResChain<Solver>* > ResStack;
+ //typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause;
+ typedef std::set < ClauseId > IdSet;
+ typedef std::vector < typename Solver::TLit > LitVector;
+ typedef __gnu_cxx::hash_map<ClauseId, typename Solver::TClause& > IdToMinisatClause;
+ typedef __gnu_cxx::hash_map<ClauseId, LitVector* > 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<Solver>* 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<Solver>* 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<Solver>* 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<Solver>* 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<Solver>* 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<ClauseId, int> d_glueMap;
+ struct Statistics {
+ IntStat d_numLearnedClauses;
+ IntStat d_numLearnedInProof;
+ IntStat d_numLemmasInProof;
+ AverageStat d_avgChainLength;
+ HistogramStat<uint64_t> d_resChainLengths;
+ HistogramStat<uint64_t> d_usedResChainLengths;
+ HistogramStat<uint64_t> d_clauseGlue;
+ HistogramStat<uint64_t> d_usedClauseGlue;
+ Statistics(const std::string& name);
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+};/* class TSatProof */
+
+
+template <class S>
+class ProofProxy {
private:
- void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
+ TSatProof<S>* d_proof;
public:
- LFSCSatProof(Minisat::Solver* solver, bool checkRes = false)
- : SatProof(solver, checkRes)
+ ProofProxy(TSatProof<S>* pf);
+ void updateCRef(typename S::TCRef oldref, typename S::TCRef newref);
+};/* class ProofProxy */
+
+
+template <class SatSolver>
+class LFSCSatProof : public TSatProof<SatSolver> {
+private:
+
+public:
+ LFSCSatProof(SatSolver* solver, const std::string& name, bool checkRes = false)
+ : TSatProof<SatSolver>(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<class Solver>
+prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
+
+
+/**
+* Convert from minisat clause to SatClause
+*
+* @param minisat_cl
+* @param sat_cl
+*/
+template<class Solver>
+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 <class Solver>
+void printLit (typename Solver::TLit l) {
+ Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
+}
+
+template <class Solver>
+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 <class Solver>
+void printClause (std::vector<typename Solver::TLit>& c) {
+ for (unsigned i = 0; i < c.size(); i++) {
+ Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
+ }
+}
+
+
+template <class Solver>
+void printLitSet(const std::set<typename Solver::TLit>& s) {
+ typename std::set < typename Solver::TLit>::const_iterator it = s.begin();
+ for(; it != s.end(); ++it) {
+ printLit<Solver>(*it);
+ Debug("proof:sat") << " ";
+ }
+ Debug("proof:sat") << std::endl;
+}
+
+// purely debugging functions
+template <class Solver>
+void printDebug (typename Solver::TLit l) {
+ Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl;
+}
+template <class Solver>
+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 <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+bool resolve(const typename Solver::TLit v,
+ std::set<typename Solver::TLit>& clause1,
+ std::set<typename Solver::TLit>& 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<Solver>(var);
+ Debug("proof:sat") << std::endl;
+ }
+ return false;
+ }
+ clause1.erase(var);
+ clause2.erase(~var);
+ typename std::set<typename Solver::TLit>::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<Solver>(var);
+ Debug("proof:sat") << std::endl;
+ }
+ return false;
+ }
+ clause1.erase(~var);
+ clause2.erase(var);
+ typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
+ for (; it!= clause2.end(); ++it) {
+ clause1.insert(*it);
+ }
+ }
+ return true;
+}
+
+/// ResChain
+template <class Solver>
+ResChain<Solver>::ResChain(ClauseId start) :
+ d_start(start),
+ d_steps(),
+ d_redundantLits(NULL)
+ {}
+template <class Solver>
+void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id, bool sign) {
+ ResStep<Solver> step(lit, id, sign);
+ d_steps.push_back(step);
+}
+
+template <class Solver>
+void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
+ if (d_redundantLits) {
+ d_redundantLits->insert(lit);
+ } else {
+ d_redundantLits = new LitSet();
+ d_redundantLits->insert(lit);
+ }
+}
+
+
+/// ProxyProof
+template <class Solver>
+ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof):
+ d_proof(proof)
+{}
+
+template <class Solver>
+void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) {
+ d_proof->updateCRef(oldref, newref);
+}
+
+
+/// SatProof
+template <class Solver>
+TSatProof<Solver>::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<Solver>(this);
+}
+
+template <class Solver>
+TSatProof<Solver>::~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 <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+bool TSatProof<Solver>::checkResolution(ClauseId id) {
+ if(d_checkRes) {
+ bool validRes = true;
+ Assert(d_resChains.find(id) != d_resChains.end());
+ ResChain<Solver>* res = d_resChains[id];
+ LitSet clause1;
+ createLitSet(res->getStart(), clause1);
+ typename ResChain<Solver>::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<Solver> (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<Solver>(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<Solver>(clause1);
+ Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
+ printClause<Solver>(c);
+ }
+ }
+ return validRes;
+
+ } else {
+ return true;
+ }
+}
+
+
+
+
+/// helper methods
+template <class Solver>
+ClauseId TSatProof<Solver>::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 <class Solver>
+ClauseId TSatProof<Solver>::getClauseId(typename Solver::TLit lit) {
+ Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
+ return d_unitId[toInt(lit)];
+}
+template <class Solver>
+typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) {
+ if (d_idClause.find(id) == d_idClause.end()) {
+ Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
+ << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
+ << (isUnit(id)? "Unit" : "") << std::endl;
+ }
+ Assert(d_idClause.find(id) != d_idClause.end());
+ return d_idClause[id];
+}
+
+template <class Solver>
+typename Solver::TClause& TSatProof<Solver>::getClause(typename Solver::TCRef ref) {
+ Assert(ref != Solver::TCRef_Undef);
+ Assert(ref >= 0 && ref < d_solver->ca.size());
+ return d_solver->ca[ref];
+}
+
+template <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) {
+ Assert(d_idUnit.find(id) != d_idUnit.end());
+ return d_idUnit[id];
+}
+template <class Solver>
+bool TSatProof<Solver>::isUnit(ClauseId id) {
+ return d_idUnit.find(id) != d_idUnit.end();
+}
+template <class Solver>
+bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) {
+ return d_unitId.find(toInt(lit)) != d_unitId.end();
+}
+template <class Solver>
+ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) {
+ Assert(isUnit(lit));
+ return d_unitId[toInt(lit)];
+}
+template <class Solver>
+bool TSatProof<Solver>::hasResolution(ClauseId id) {
+ return d_resChains.find(id) != d_resChains.end();
+}
+template <class Solver>
+bool TSatProof<Solver>::isInputClause(ClauseId id) {
+ return (d_inputClauses.find(id) != d_inputClauses.end());
+}
+template <class Solver>
+bool TSatProof<Solver>::isLemmaClause(ClauseId id) {
+ return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
+}
+
+template <class Solver>
+bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) {
+ return d_assumptionConflicts.find(id) != d_assumptionConflicts.end();
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::print(ClauseId id) {
+ if (d_deleted.find(id) != d_deleted.end()) {
+ Debug("proof:sat") << "del"<<id;
+ } else if (isUnit(id)) {
+ printLit<Solver>(getUnit(id));
+ } else if (id == d_emptyClauseId) {
+ Debug("proof:sat") << "empty "<< std::endl;
+ }
+ else {
+ typename Solver::TCRef ref = getClauseRef(id);
+ printClause<Solver>(getClause(ref));
+ }
+}
+template <class Solver>
+void TSatProof<Solver>::printRes(ClauseId id) {
+ Assert(hasResolution(id));
+ Debug("proof:sat") << "id "<< id <<": ";
+ printRes(d_resChains[id]);
+}
+template <class Solver>
+void TSatProof<Solver>::printRes(ResChain<Solver>* res) {
+ ClauseId start_id = res->getStart();
+
+ if(Debug.isOn("proof:sat")) {
+ Debug("proof:sat") << "(";
+ print(start_id);
+ }
+
+ typename ResChain<Solver>::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<Solver>(v);
+ Debug("proof:sat") << "] ";
+ print(id);
+ }
+ }
+ Debug("proof:sat") << ") \n";
+}
+
+/// registration methods
+template <class Solver>
+ ClauseId TSatProof<Solver>::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 <class Solver>
+ClauseId TSatProof<Solver>::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 <class Solver>
+void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) {
+ Assert (d_trueLit == ClauseIdUndef);
+ d_trueLit = registerUnitClause(lit, INPUT);
+}
+
+template <class Solver>
+void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) {
+ Assert (d_falseLit == ClauseIdUndef);
+ d_falseLit = registerUnitClause(lit, INPUT);
+}
+
+template <class Solver>
+ClauseId TSatProof<Solver>::getTrueUnit() const {
+ Assert (d_trueLit != ClauseIdUndef);
+ return d_trueLit;
+}
+
+template <class Solver>
+ClauseId TSatProof<Solver>::getFalseUnit() const {
+ Assert (d_falseLit != ClauseIdUndef);
+ return d_falseLit;
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) {
+ Assert (d_assumptions.find(var) == d_assumptions.end());
+ d_assumptions.insert(var);
+}
+
+template <class Solver>
+ClauseId TSatProof<Solver>::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<Solver>(*vec_confl);
+ Debug("proof:sat:detailed") << "\n";
+ }
+
+ d_assumptionConflictsDebug[new_id] = vec_confl;
+ return new_id;
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* 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 <class Solver>
+void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* 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 <class Solver>
+void TSatProof<Solver>::startResChain(typename Solver::TCRef start) {
+ ClauseId id = getClauseId(start);
+ ResChain<Solver>* res = new ResChain<Solver>(id);
+ d_resStack.push_back(res);
+}
+
+template <class Solver>
+void TSatProof<Solver>::startResChain(typename Solver::TLit start) {
+ ClauseId id = getUnitId(start);
+ ResChain<Solver>* res = new ResChain<Solver>(id);
+ d_resStack.push_back(res);
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit,
+ typename Solver::TCRef clause, bool sign) {
+ ClauseId id = registerClause(clause, LEARNT);
+ ResChain<Solver>* res = d_resStack.back();
+ res->addStep(lit, id, sign);
+}
+
+template <class Solver>
+void TSatProof<Solver>::endResChain(ClauseId id) {
+ Debug("proof:sat:detailed") <<"endResChain " << id << "\n";
+ Assert(d_resStack.size() > 0);
+ ResChain<Solver>* res = d_resStack.back();
+ registerResolution(id, res);
+ d_resStack.pop_back();
+}
+
+
+// template <class Solver>
+// void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) {
+// Assert(d_resStack.size() > 0);
+// ClauseId id = registerClause(clause, LEARNT);
+// ResChain<Solver>* res = d_resStack.back();
+// registerResolution(id, res);
+// d_resStack.pop_back();
+// }
+
+template <class Solver>
+void TSatProof<Solver>::endResChain(typename Solver::TLit lit) {
+ Assert(d_resStack.size() > 0);
+ ClauseId id = registerUnitClause(lit, LEARNT);
+ Debug("proof:sat:detailed") <<"endResChain unit " << id << "\n";
+ ResChain<Solver>* res = d_resStack.back();
+ d_glueMap[id] = 1;
+ registerResolution(id, res);
+ d_resStack.pop_back();
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::cancelResChain() {
+ Assert(d_resStack.size() > 0);
+ d_resStack.pop_back();
+}
+
+
+template <class Solver>
+void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) {
+ Assert(d_resStack.size() > 0);
+ ResChain<Solver>* res = d_resStack.back();
+ res->addRedundantLit(lit);
+}
+
+/// constructing resolutions
+template <class Solver>
+void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) {
+ ClauseId id = resolveUnit(~lit);
+ ResChain<Solver>* res = d_resStack.back();
+ res->addStep(lit, id, !sign(lit));
+}
+template <class Solver>
+void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) {
+ Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
+ resolveUnit(lit);
+}
+template <class Solver>
+ClauseId TSatProof<Solver>::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<Solver>* res = new ResChain<Solver>(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 <class Solver>
+void TSatProof<Solver>::toStream(std::ostream& out) {
+ Debug("proof:sat") << "TSatProof<Solver>::printProof\n";
+ Unimplemented("native proof printing not supported yet");
+}
+template <class Solver>
+ClauseId TSatProof<Solver>::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 <class Solver>
+void TSatProof<Solver>::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<Solver>* res = new ResChain<Solver>(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<Solver>* res = new ResChain<Solver>(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 <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+void TSatProof<Solver>::finishUpdateCRef() {
+ d_clauseId.swap(d_temp_clauseId);
+ d_temp_clauseId.clear();
+
+ d_idClause.swap(d_temp_idClause);
+ d_temp_idClause.clear();
+}
+template <class Solver>
+void TSatProof<Solver>::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<Solver>(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 <class Solver>
+void TSatProof<Solver>::constructProof(ClauseId conflict) {
+ collectClauses(conflict);
+}
+
+template <class Solver>
+std::string TSatProof<Solver>::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 <class Solver>
+prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
+ if (isUnit(id)) {
+ typename Solver::TLit lit = getUnit(id);
+ prop::SatLiteral sat_lit = toSatLiteral<Solver>(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<Solver>(minisat_cl, *clause);
+ return clause;
+}
+
+template <class Solver>
+void TSatProof<Solver>::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<Solver>* 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<Solver>::ResSteps steps = res->getSteps();
+ for(size_t i = 0; i < steps.size(); i++) {
+ collectClauses(steps[i].id);
+ }
+}
+
+template <class Solver>
+void TSatProof<Solver>::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 <class Solver>
+void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) {
+ Assert (d_glueMap.find(clause) == d_glueMap.end());
+ d_glueMap.insert(std::make_pair(clause, glue));
+}
+
+template <class Solver>
+TSatProof<Solver>::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 <class Solver>
+TSatProof<Solver>::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 <class Solver>
+void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
+ out << "(satlem_simplify _ _ _ ";
+
+ ResChain<Solver>* res = this->d_resChains[id];
+ typename ResChain<Solver>::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) << " "<<ProofManager::getVarName(v, this->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 <class Solver>
+void LFSCSatProof<Solver>::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<typename Solver::TLit>& confl = *(this->d_assumptionConflictsDebug[id]);
+
+ Assert (confl.size());
+
+ for (unsigned i = 0; i < confl.size(); ++i) {
+ prop::SatLiteral lit = toSatLiteral<Solver>(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<Solver>(confl[i]);
+ prop::SatVariable v = lit.getSatVariable();
+ out << "unit"<< v <<" ";
+ out << ProofManager::getVarName(v, this->d_name) <<")";
+ }
+ out <<"(\\ e e)\n";
+ paren <<")";
+}
+
+
+template <class Solver>
+void LFSCSatProof<Solver>::printResolutions(std::ostream& out, std::ostream& paren) {
+ Debug("bv-proof") << "; print resolutions" << std::endl;
+ std::set<ClauseId>::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 <class Solver>
+void LFSCSatProof<Solver>::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<TNode, TNodeHashFunction> 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"<<let_id << " ";
+ printTheoryTerm(current_expr, os, map);
+ paren <<")";
+ }
+ unsigned last_let_id = let_order.back().id;
+ Expr last = let_order.back().expr;
+ unsigned last_count = map.find(last)->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<Expr> 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<Expr> 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<Expr> 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"<<id;
+ return;
+ }
+ printTheoryTerm(term, os, map);
+}
+
+void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) {
+ if (term.isVariable()) {
+ os << ProofManager::sanitize(term);
return;
}
+ Kind k = term.getKind();
+
+ switch(k) {
case kind::ITE:
- os << (term.getType().isBoolean() ? "(ifte " : "(ite _ ");
- printTerm(term[0], os);
+ os << (term.getType().isBoolean() ? "(ifte ": "(ite _ ");
+
+ printBoundTerm(term[0], os, map);
os << " ";
- printTerm(term[1], os);
+ printBoundTerm(term[1], os, map);
os << " ";
- printTerm(term[2], os);
+ printBoundTerm(term[2], os, map);
os << ")";
return;
case kind::EQUAL:
os << "(";
os << "= ";
- os << term[0].getType() << " ";
- printTerm(term[0], os);
+ printSort(term[0].getType(), os);
+ printBoundTerm(term[0], os, map);
os << " ";
- printTerm(term[1], os);
+ printBoundTerm(term[1], os, map);
os << ")";
return;
case kind::DISTINCT:
- os << "(not (= ";
- os << term[0].getType() << " ";
- printTerm(term[0], os);
- os << " ";
- printTerm(term[1], os);
- os << "))";
- return;
+ // Distinct nodes can have any number of chidlren.
+ Assert (term.getNumChildren() >= 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<bool>() ? "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<Expr>& 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<lemma.size(); i++ ){
+ Node lit = Node::fromExpr( lemma[i] ).negate();
+ Trace("theory-proof-debug") << "; preregistering and asserting " << lit << std::endl;
+ NodeVisitor<MyPreRegisterVisitor>::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<Type> 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<bool>() ? "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<Expr>& 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 <ext/hash_set>
#include <iosfwd>
-#include "expr/expr.h"
-#include "util/proof.h"
namespace CVC4 {
- typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet;
- typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > 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<Expr, LetCount, ExprHashFunction> LetMap;
+typedef std::vector<LetOrderElement> Bindings;
+
+class TheoryProof;
+typedef unsigned ClauseId;
+
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef std::map<theory::TheoryId, TheoryProof* > 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<Expr>& 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<Expr>& 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<Expr>& 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 <stack>
+
+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<const theory::eq::EqProof *> 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<theory::eq::EqProof *> 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<const theory::eq::EqProof*> 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<Kind>());
+ } 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<Kind>());
+ } 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<Expr>& 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<Type> 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<Type, TypeHashFunction > 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<Expr>& lemma, std::ostream& os, std::ostream& paren);
+ virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+};
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UF__PROOF_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback