From 3361081acd11178d0eb580ce91279a2ecaa7aa65 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 8 Oct 2013 16:50:28 -0400 Subject: [PATCH] fixed uf proof with holes bugs --- src/proof/cnf_proof.cpp | 75 +++++++++++++++++++++--------------- src/proof/cnf_proof.h | 15 ++++---- src/proof/proof_manager.cpp | 18 ++++++++- src/proof/proof_manager.h | 24 ++++++++---- src/proof/sat_proof.cpp | 52 +++++++++++++++++-------- src/proof/sat_proof.h | 4 +- src/proof/theory_proof.cpp | 15 ++++---- src/prop/minisat/minisat.cpp | 7 ++++ src/prop/minisat/minisat.h | 2 +- src/prop/sat_solver_types.h | 4 ++ 10 files changed, 143 insertions(+), 73 deletions(-) diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index caafa6b83..d73202147 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -41,33 +41,46 @@ void CnfProof::setTheoryProof(TheoryProof* theory_proof) { d_theoryProof = theory_proof; } -void CnfProof::addInputClause(ClauseId id, const ::Minisat::Clause& clause) { - d_inputClauses.insert(std::make_pair(id, clause)); -} - -void CnfProof::addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause) { - d_theoryLemmas.insert(std::make_pair(id, clause)); +void CnfProof::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { + for (unsigned i = 0; i < clause->size(); ++i) { + SatLiteral lit = clause->operator[](i); + addVariable(lit.getSatVariable()); + } + if (kind == INPUT) { + d_inputClauses.insert(std::make_pair(id, clause)); + return; + } + Assert (kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); } -void CnfProof::addVariable(unsigned var) { +void CnfProof::addVariable(prop::SatVariable var) { d_propVars.insert(var); - Expr atom = getAtom(var); + Expr atom = getAtom(var); getTheoryProof()->addAtom(atom); } -Expr CnfProof::getAtom(unsigned var) { - Minisat::Lit m_lit = Minisat::mkLit(var); - prop::SatLiteral sat_lit = prop::MinisatSatSolver::toSatLiteral(m_lit); - Expr atom = d_cnfStream->getNode(sat_lit).toExpr(); +Expr CnfProof::getAtom(prop::SatVariable var) { + prop::SatLiteral lit (var); + Expr atom = d_cnfStream->getNode(lit).toExpr(); return atom; } +CnfProof::~CnfProof() { + for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + delete it->second; + } + for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { + delete it->second; + } +} + void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end(); ++it) { Expr atom = getAtom(*it); os << "(decl_atom "; getTheoryProof()->printFormula(atom, os); - os << " (\\ " << ProofManager::getVarPrefix() <<*it << " (\\ " << ProofManager::getAtomPrefix() <<*it << "\n"; + os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n"; paren << ")))"; } } @@ -78,44 +91,44 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { } void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { + os << " ;; Input Clauses \n"; for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { ClauseId id = it->first; - const Minisat::Clause& clause = it->second; - os << " ;; input clause \n"; + const prop::SatClause* clause = it->second; os << "(satlem _ _ "; std::ostringstream clause_paren; - printClause(clause, os, clause_paren); + printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getInputClausePrefix() << id <<"\n"; + os << "( \\ " << ProofManager::printInputClauseName(id) << "\n"; paren << "))"; } } void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { - for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + os << " ;; Theory Lemmas \n"; + for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { ClauseId id = it->first; - const Minisat::Clause& clause = it->second; - os << " ;; theory lemma \n"; + const prop::SatClause* clause = it->second; os << "(satlem _ _ "; std::ostringstream clause_paren; - printClause(clause, os, clause_paren); + printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::getLemmaClausePrefix() << id <<"\n"; + os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n"; paren << "))"; } } -void LFSCCnfProof::printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren) { - for (int i = 0; i < clause.size(); ++i) { - Minisat::Lit lit = clause[i]; - unsigned var = Minisat::var(lit); - if (sign(lit)) { - os << "(asf _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " "; - 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::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " "; + paren << "))"; } else { - os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " "; - paren << ")"; + os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " "; + paren << "))"; } } } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 8acb7a50f..010b1429d 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -32,8 +32,8 @@ namespace prop { class CnfStream; } -typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause; -typedef __gnu_cxx::hash_set VarSet; +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_set VarSet; class TheoryProof; @@ -46,22 +46,21 @@ protected: TheoryProof* d_theoryProof; TheoryProof* getTheoryProof(); - Expr getAtom(unsigned var); + Expr getAtom(prop::SatVariable var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); - void addInputClause(ClauseId id, const ::Minisat::Clause& clause); - void addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause); - void addVariable(unsigned var); + void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + void addVariable(prop::SatVariable var); void setTheoryProof(TheoryProof* theory_proof); virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; - + virtual ~CnfProof(); }; class LFSCCnfProof: public CnfProof { void printInputClauses(std::ostream& os, std::ostream& paren); void printTheoryLemmas(std::ostream& os, std::ostream& paren); - void printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren); + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); public: LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) : CnfProof(cnfStream) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 7ca1a1e65..e1f85b93f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -24,6 +24,13 @@ namespace CVC4 { +std::string append(const std::string& str, uint64_t num) { + std::ostringstream os; + os << str << num; + return os.str(); +} + + bool ProofManager::isInitialized = false; ProofManager* ProofManager::proofManager = NULL; @@ -98,6 +105,15 @@ void ProofManager::initTheoryProof() { currentPM()->d_theoryProof = new LFSCTheoryProof(); } + +std::string ProofManager::printInputClauseName(ClauseId id) {return append("pb", id); } +std::string ProofManager::printLemmaClauseName(ClauseId id) { return append("lem", id); } +std::string ProofManager::printLearntClauseName(ClauseId id) { return append("cl", id); } +std::string ProofManager::printVarName(prop::SatVariable var) { return append("v", var); } +std::string ProofManager::printAtomName(prop::SatVariable var) { return append("a", var); } +std::string ProofManager::printLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } + + LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) , d_cnfProof(cnf) @@ -119,7 +135,7 @@ void LFSCProof::toStream(std::ostream& out) { d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); d_satProof->printResolutions(out, paren); - paren <<"))"; + paren <<")))\n;;"; out << paren.str(); } diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 4ae8a6dae..d4f1d6528 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -25,6 +25,7 @@ #include "proof/proof.h" #include "util/proof.h" + // forward declarations namespace Minisat { class Solver; @@ -35,6 +36,7 @@ namespace CVC4 { namespace prop { class CnfStream; } +typedef int ClauseId; class Proof; class SatProof; @@ -44,13 +46,20 @@ class TheoryProof; class LFSCSatProof; class LFSCCnfProof; class LFSCTheoryProof; - + +namespace prop { +typedef uint64_t SatVariable; +class SatLiteral; +} + // different proof modes enum ProofFormat { LFSC, NATIVE };/* enum ProofFormat */ +std::string append(const std::string& str, uint64_t num); + class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; @@ -74,12 +83,13 @@ public: static TheoryProof* getTheoryProof(); // variable prefixes - static std::string getInputClausePrefix() { return "pb"; } - static std::string getLemmaClausePrefix() { return "lem"; } - static std::string getLearntClausePrefix() { return "cl"; } - static std::string getVarPrefix() { return "v"; } - static std::string getAtomPrefix() { return "a"; } - static std::string getLitPrefix() {return "l"; } + static std::string printInputClauseName(ClauseId id); + static std::string printLemmaClauseName(ClauseId id); + static std::string printLearntClauseName(ClauseId id); + + static std::string printVarName(prop::SatVariable var); + static std::string printAtomName(prop::SatVariable var); + static std::string printLitName(prop::SatLiteral lit); };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index dc83e6aa3..e8c63bb74 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -19,10 +19,11 @@ #include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" +#include "prop/minisat/minisat.h" using namespace std; using namespace Minisat; - +using namespace CVC4::prop; namespace CVC4 { /// some helper functions @@ -277,7 +278,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { return d_unitId[toInt(lit)]; } -::Minisat::CRef SatProof::getClauseRef(ClauseId id) { +Minisat::CRef SatProof::getClauseRef(ClauseId id) { if (d_idClause.find(id) == d_idClause.end()) { Debug("proof:sat") << "proof:getClauseRef cannot find clause "<ca[ref]; } -::Minisat::Lit SatProof::getUnit(ClauseId id) { +Minisat::Lit SatProof::getUnit(ClauseId id) { Assert (d_idUnit.find(id) != d_idUnit.end()); return d_idUnit[id]; } @@ -379,7 +380,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { d_lemmaClauses.insert(newId); } } - Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " << kind << "\n"; + Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; return d_clauseId[clause]; } @@ -575,7 +576,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert (d_storedUnitConflict); conflict_id = d_unitConflictId; } else { - Assert (!d_storedUnitConflict); + Assert (!d_storedUnitConflict); conflict_id = registerClause(conflict_ref); //FIXME } @@ -625,6 +626,12 @@ void SatProof::markDeleted(CRef clause) { } void SatProof::constructProof() { + // if (isLemmaClause(d_conflictId)) { + // addClauseToCnfProof(d_emptyClauseId, THEORY_LEMMA); + // } + // if (isInputClause(d_emptyClauseId)) { + // addClauseToCnfProof(d_emptyClauseId, INPUT); + // } collectClauses(d_emptyClauseId); } @@ -643,18 +650,34 @@ void SatProof::constructProof() { std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << ProofManager::getInputClausePrefix()<push_back(sat_lit); + getCnfProof()->addClause(id, clause, kind); + return; + } + CRef ref = getClauseRef(id); + const Clause& minisat_cl = getClause(ref); + SatClause* clause = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *clause); + getCnfProof()->addClause(id, clause, kind); +} + void SatProof::collectClauses(ClauseId id) { if (d_seenLearnt.find(id) != d_seenLearnt.end()) { return; @@ -667,17 +690,14 @@ void SatProof::collectClauses(ClauseId id) { } if (isInputClause(id)) { - CRef input_ref = getClauseRef(id); - const Clause& cl = getClause(input_ref); - getCnfProof()->addInputClause(id, cl); + addClauseToCnfProof(id, INPUT); d_seenInput.insert(id); return; } else if (isLemmaClause(id)) { - CRef lemma_ref = getClauseRef(id); - const Clause& cl = getClause(lemma_ref); - getCnfProof()->addTheoryLemma(id, cl); - d_seenLemmas.insert(id); + addClauseToCnfProof(id, THEORY_LEMMA); + d_seenLemmas.insert(id); + return; } else { d_seenLearnt.insert(id); @@ -716,7 +736,7 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "< IdResMap; typedef std::hash_set < ClauseId > IdHashSet; typedef std::vector < ResChain* > ResStack; -typedef std::hash_set < unsigned > VarSet; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map IdToMinisatClause; @@ -255,6 +254,7 @@ protected: void collectClauses(ClauseId id); CnfProof* d_cnfProof; CnfProof* getCnfProof(); + void addClauseToCnfProof(ClauseId id, ClauseKind kind); public: void setCnfProof(CnfProof* cnfProof); virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 224c74e2c..948ced393 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -35,7 +35,9 @@ void TheoryProof::addDeclaration(Expr term) { d_sortDeclarations.insert(type); if (term.getKind() == kind::APPLY_UF) { Expr function = term.getOperator(); - d_termDeclarations.insert(function); + d_termDeclarations.insert(function); + Assert (term.getNumChildren() == 1); + addDeclaration(term[0]); } else { Assert (term.isVariable()); Assert (type.isSort()); @@ -48,10 +50,8 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { os << term; return; } - Assert (term.getKind() == kind::APPLY_UF); + Assert (term.getKind() == kind::APPLY_UF && term.getNumChildren() == 1); Expr func = term.getOperator(); - // only support unary functions so far - Assert (func.getNumChildren() == 1); os << "(apply _ _ " << func << " "; printTerm(term[0], os); os <<")"; @@ -61,6 +61,7 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { // should make this more general Assert (atom.getKind() == kind::EQUAL); os << "(= "; + os << atom[0].getType() <<" "; printTerm(atom[0], os); os << " "; printTerm(atom[1], os); @@ -70,7 +71,7 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { 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"; + os << "(% " << *it << " sort \n"; paren << ")"; } @@ -78,13 +79,13 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; - os << "(% " << term << "(term "; + os << "(% " << term << " (term "; paren <<")"; Type type = term.getType(); if (type.isFunction()) { FunctionType ftype = (FunctionType)type; - Assert (ftype.getArity() == 2); + Assert (ftype.getArity() == 1); Type arg_type = ftype.getArgTypes()[0]; Type result_type = ftype.getRangeType(); os << "(arrow " << arg_type << " " << result_type << "))\n"; diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 960f2ad62..98e43aaf0 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -103,6 +103,13 @@ void MinisatSatSolver::toSatClause(Minisat::vec& clause, Assert((unsigned)clause.size() == sat_clause.size()); } +void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ec49b5f71..27258b3c2 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -51,7 +51,7 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (Minisat::vec& clause, SatClause& sat_clause); - + static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); void addClause(SatClause& clause, bool removable); diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index ab2bcda47..8fee0d11e 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -135,6 +135,10 @@ public: return (size_t)d_value; } + uint64_t toInt() const { + return d_value; + } + /** * Returns true if the literal is undefined. */ -- 2.30.2