diff options
author | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
commit | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (patch) | |
tree | a1ea60d22fadc2d2ebefca3ab561fbcf74a6936b /src/proof/cnf_proof.cpp | |
parent | ba8efaff308ef1eb14ec40dd74e0e18c16126d2c (diff) |
fixed uf proof with holes bugs
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 75 |
1 files changed, 44 insertions, 31 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 << "))"; } } } |