From 08c8433e4ab849024930a8c4dbe8756e13d08099 Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 9 Oct 2013 13:48:26 -0400 Subject: [PATCH] fixed uf proof bug: now storing deleted theory lemmas --- src/proof/sat_proof.cpp | 89 ++++++--------------------------- src/proof/sat_proof.h | 10 ++-- src/proof/theory_proof.cpp | 34 +++++++++---- src/prop/minisat/core/Solver.cc | 3 +- src/smt/smt_engine.cpp | 17 ++++--- 5 files changed, 55 insertions(+), 98 deletions(-) diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index e8c63bb74..e1534a635 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -621,32 +621,20 @@ void SatProof::markDeleted(CRef 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); + d_deleted.insert(id); + if (isLemmaClause(id)) { + const Clause& minisat_cl = getClause(clause); + SatClause* sat_cl = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + } } } void SatProof::constructProof() { - // if (isLemmaClause(d_conflictId)) { - // addClauseToCnfProof(d_emptyClauseId, THEORY_LEMMA); - // } - // if (isInputClause(d_emptyClauseId)) { - // addClauseToCnfProof(d_emptyClauseId, INPUT); - // } collectClauses(d_emptyClauseId); } -// std::string SatProof::varName(::Minisat::Lit lit) { -// ostringstream os; -// if (sign(lit)) { -// os << "(neg "<< ProofManager::getVarPrefix() <addClause(id, clause, kind); return; } + + if (isDeleted(id)) { + Assert (kind == THEORY_LEMMA); + SatClause* clause = d_deletedTheoryLemmas.find(id)->second; + getCnfProof()->addClause(id, clause, kind); + return; + } + CRef ref = getClauseRef(id); const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); @@ -748,54 +744,6 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren << "))"; // closing parethesis for lemma binding and satlem } - -// void LFSCSatProof::printInputClause(ClauseId id) { -// if (isUnit(id)) { -// ::Minisat::Lit lit = getUnit(id); -// d_clauseSS << "(% " << clauseName(id) << " (holds (clc "; -// d_clauseSS << varName(lit) << "cln ))"; -// d_paren << ")"; -// return; -// } - -// ostringstream os; -// CRef ref = getClauseRef(id); -// Assert (ref != CRef_Undef); -// Clause& c = getClause(ref); - -// d_clauseSS << "(% " << clauseName(id) << " (holds "; -// os << ")"; // closing paren for holds -// d_paren << ")"; // closing paren for (% - -// for(int i = 0; i < c.size(); i++) { -// d_clauseSS << " (clc " << varName(c[i]) <<" "; -// os <<")"; -// d_seenVars.insert(var(c[i])); -// } -// d_clauseSS << "cln"; -// d_clauseSS << os.str() << "\n"; -// } - - -// void LFSCSatProof::printInputClauses() { -// for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) { -// printInputClause(*it); -// } -// } - - -// void LFSCSatProof::flush(std::ostream& out) { -// out << "(check \n"; -// d_paren <<")"; -// out << d_varSS.str(); -// out << d_clauseSS.str(); -// out << "(: (holds cln) \n"; -// out << d_learntSS.str(); -// d_paren << "))"; -// out << d_paren.str(); -// out << "\n"; -// } - void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) { if(*it != d_emptyClauseId) { @@ -805,13 +753,6 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { printResolution(d_emptyClauseId, out, paren); } -// void LFSCSatProof::printVariables(std::ostream& out, std::ostream& paren) { -// for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) { -// out << "(% " << ProofManager::getVarPrefix() << *it <<" var \n"; -// paren << ")"; -// } -// } - } /* CVC4 namespace */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 5a1fa4680..c4936fd88 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -81,14 +81,14 @@ public: LitSet* getRedundant() { return d_redundantLits; } };/* class ResChain */ -typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap; +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::vector < ResChain* > ResStack; - +typedef std::hash_map IdToSatClause; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map IdToMinisatClause; @@ -116,11 +116,12 @@ class SatProof { protected: ::Minisat::Solver* d_solver; // clauses - IdClauseMap d_idClause; + IdCRefMap d_idClause; ClauseIdMap d_clauseId; IdUnitMap d_idUnit; UnitIdMap d_unitId; IdHashSet d_deleted; + IdToSatClause d_deletedTheoryLemmas; IdHashSet d_inputClauses; IdHashSet d_lemmaClauses; // resolutions @@ -136,7 +137,7 @@ protected: // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdClauseMap d_temp_idClause; + IdCRefMap d_temp_idClause; // unit conflict ClauseId d_unitConflictId; @@ -223,6 +224,7 @@ public: * @param clause */ void markDeleted(::Minisat::CRef 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 diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index ecd9f9810..5b5a2ae15 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -65,19 +65,17 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { os << term; return; } - std::ostringstream paren; + Assert (term.getKind() == kind::APPLY_UF); Expr func = term.getOperator(); - os << "(apply _ _ " << func << " "; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + os<< "(apply _ _ "; + } + os << func << " "; for (unsigned i = 0; i < term.getNumChildren(); ++i) { printTerm(term[i], os); - if (i < term.getNumChildren() - 1) { - os << "(apply _ _ " << func << " "; - paren << ")"; - } - os << ")" ; + os << ")"; } - os << paren.str(); } std::string toLFSCKind(Kind kind) { @@ -95,7 +93,7 @@ std::string toLFSCKind(Kind kind) { void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { // should make this more general and overall sane - Assert (atom.getType().isBoolean()); + Assert (atom.getType().isBoolean() && "Only printing booleans." ); Kind kind = atom.getKind(); // this is the only predicate we have if (kind == kind::EQUAL) { @@ -106,6 +104,13 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { os <<" "; printTerm(atom[1], os); os <<")"; + } else if ( kind == kind::DISTINCT) { + os <<"(not (= "; + os << atom[0].getType() <<" "; + printTerm(atom[0], os); + os <<" "; + printTerm(atom[1], os); + os <<"))"; } else if ( kind == kind::OR || kind == kind::AND || kind == kind::XOR || @@ -134,8 +139,15 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { } os <<")"; } - } else { - Assert (false); + } else if (kind == kind::CONST_BOOLEAN) { + if (atom.getConst()) + os << "true"; + else + os << "false"; + } + else { + std::cout << kind << "\n"; + Assert (false && "Unsupported kind"); } } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 45127a182..16fa3ba60 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -369,9 +369,8 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { - PROOF( ProofManager::getSatProof()->markDeleted(cr); ) - const Clause& c = ca[cr]; + PROOF( ProofManager::getSatProof()->markDeleted(cr); ) Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5a3334d64..160a16652 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3105,11 +3105,11 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { Assert(ex.isNull() || ex.getExprManager() == d_exprManager); - // PROOF ( - ProofManager* pm = ProofManager::currentPM(); - TheoryProof* pf = pm->getTheoryProof(); - pf->assertFormula(ex); - // ); +#ifdef CVC4_PROOF + // if (options::proof()) { <-- SEGFAULT!! + ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + //} +#endif SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -3253,8 +3253,11 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); - //PROOF ( - ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); //); +#ifdef CVC4_PROOF + // if (options::proof()) { <-- SEGFAULT!!! + ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + // } +#endif SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); -- 2.30.2