sat_proof.cpp \
cnf_proof.h \
cnf_proof.cpp \
+ theory_proof.h \
+ theory_proof.cpp \
proof_manager.h \
proof_manager.cpp
**/
#include "proof/cnf_proof.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
+#include "prop/sat_solver_types.h"
+#include "prop/minisat/minisat.h"
+#include "prop/cnf_stream.h"
+
using namespace CVC4::prop;
namespace CVC4 {
-CnfProof::CnfProof(CnfStream* stream) :
- d_cnfStream(stream) {}
+CnfProof::CnfProof(CnfStream* stream)
+ : d_cnfStream(stream)
+ , d_theoryProof(NULL)
+{}
+
+TheoryProof* CnfProof::getTheoryProof() {
+ Assert (d_theoryProof);
+ return d_theoryProof;
+}
+
+void CnfProof::setTheoryProof(TheoryProof* theory_proof) {
+ Assert (d_theoryProof == NULL);
+ 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::addVariable(unsigned var) {
+ d_propVars.insert(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();
+ return atom;
+}
+
+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";
+ paren << ")))";
+ }
+}
+
+void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
+ printInputClauses(os, paren);
+ printTheoryLemmas(os, paren);
+}
+
+void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
+ 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";
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+ printClause(clause, os, clause_paren);
+ os << " (clausify_false trust)" << clause_paren.str();
+ os << "( \\ " << ProofManager::getInputClausePrefix() << 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) {
+ ClauseId id = it->first;
+ const Minisat::Clause& clause = it->second;
+ os << " ;; theory lemma \n";
+ os << "(satlem _ _ ";
+ std::ostringstream clause_paren;
+ printClause(clause, os, clause_paren);
+ os << " (clausify_false trust)" << clause_paren.str();
+ os << "( \\ " << ProofManager::getLemmaClausePrefix() << 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 << ")";
+ } else {
+ os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
+ paren << ")";
+ }
+ }
+}
+
} /* CVC4 namespace */
+
**
**/
-#include "cvc4_private.h"
-#include "util/proof.h"
#ifndef __CVC4__CNF_PROOF_H
#define __CVC4__CNF_PROOF_H
+#include "cvc4_private.h"
+#include "util/proof.h"
+#include "proof/sat_proof.h"
+
+#include <ext/hash_set>
+#include <ext/hash_map>
#include <iostream>
+
namespace CVC4 {
namespace prop {
class CnfStream;
}
+
+typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause;
+typedef __gnu_cxx::hash_set<unsigned > VarSet;
+
+class TheoryProof;
+
class CnfProof {
+protected:
CVC4::prop::CnfStream* d_cnfStream;
+ IdToClause d_inputClauses;
+ IdToClause d_theoryLemmas;
+ VarSet d_propVars;
+ TheoryProof* d_theoryProof;
+ TheoryProof* getTheoryProof();
+
+ Expr getAtom(unsigned 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 setTheoryProof(TheoryProof* theory_proof);
+ virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
+ virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
+
+};
+
+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);
+public:
+ LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
+ : CnfProof(cnfStream)
+ {}
+ virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
+ virtual void printClauses(std::ostream& os, std::ostream& paren);
};
} /* CVC4 namespace */
#include "util/proof.h"
#include "proof/sat_proof.h"
#include "proof/cnf_proof.h"
+#include "proof/theory_proof.h"
#include "util/cvc4_assert.h"
namespace CVC4 {
ProofManager::ProofManager(ProofFormat format):
d_satProof(NULL),
d_cnfProof(NULL),
+ d_theoryProof(NULL),
+ d_fullProof(NULL),
d_format(format)
-{}
+{
+ // FIXME this is until it actually has theory references
+ initTheoryProof();
+}
+
+ProofManager::~ProofManager() {
+ delete d_satProof;
+ delete d_cnfProof;
+ delete d_theoryProof;
+ delete d_fullProof;
+}
ProofManager* ProofManager::currentPM() {
if (isInitialized) {
}
Proof* ProofManager::getProof() {
- // for now, this is just the SAT proof
- return getSatProof();
+ if (currentPM()->d_fullProof != NULL)
+ return currentPM()->d_fullProof;
+ Assert (currentPM()->d_format == LFSC);
+
+ currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(),
+ (LFSCCnfProof*)getCnfProof(),
+ (LFSCTheoryProof*)getTheoryProof());
+ return currentPM()->d_fullProof;
}
SatProof* ProofManager::getSatProof() {
return currentPM()->d_cnfProof;
}
+TheoryProof* ProofManager::getTheoryProof() {
+ Assert (currentPM()->d_theoryProof);
+ return currentPM()->d_theoryProof;
+}
+
+
void ProofManager::initSatProof(Minisat::Solver* solver) {
Assert (currentPM()->d_satProof == NULL);
- switch(currentPM()->d_format) {
- case LFSC :
- currentPM()->d_satProof = new LFSCSatProof(solver);
- break;
- case NATIVE :
- currentPM()->d_satProof = new SatProof(solver);
- break;
- default:
- Assert(false);
- }
-
+ Assert(currentPM()->d_format == LFSC);
+ currentPM()->d_satProof = new LFSCSatProof(solver);
}
void ProofManager::initCnfProof(prop::CnfStream* cnfStream) {
Assert (currentPM()->d_cnfProof == NULL);
+ Assert (currentPM()->d_format == LFSC);
+ currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream);
+}
- switch(currentPM()->d_format) {
- case LFSC :
- currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME
- break;
- case NATIVE :
- currentPM()->d_cnfProof = new CnfProof(cnfStream);
- break;
- default:
- Assert(false);
- }
+void ProofManager::initTheoryProof() {
+ Assert (currentPM()->d_theoryProof == NULL);
+ Assert (currentPM()->d_format == LFSC);
+ currentPM()->d_theoryProof = new LFSCTheoryProof();
+}
+LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
+ : d_satProof(sat)
+ , d_cnfProof(cnf)
+ , d_theoryProof(theory)
+{
+ // link the proofs
+ d_satProof->setCnfProof(d_cnfProof);
+ d_cnfProof->setTheoryProof(d_theoryProof);
+ // build the resolution proof out of the traces
+ // this sets up the other proofs with the necessary information
+ d_satProof->constructProof();
}
+void LFSCProof::toStream(std::ostream& out) {
+ std::ostringstream paren;
+ out << "(check \n";
+ d_theoryProof->printDeclarations(out, paren);
+ out << "(: (holds cln) \n";
+ d_cnfProof->printAtomMapping(out, paren);
+ d_cnfProof->printClauses(out, paren);
+ d_satProof->printResolutions(out, paren);
+ paren <<"))";
+ out << paren.str();
+}
+
+// void ProofManager::declareAtom(Expr atom, SatLiteral lit) {
+// ::Minisat::Lit mlit = toMinisatLit(lit);
+// d_satProof->addLiteral(mlit);
+// d_cnfProof->declareAtom(atom, mlit);
+// }
+
+// void ProofManager::addInputClause(SatClause clause) {
+// d_satProof->registerClause(clause, true);
+// d_cnfProof->registerClause(clause, true);
+// }
} /* CVC4 namespace */
#include <iostream>
#include "proof/proof.h"
+#include "util/proof.h"
// forward declarations
namespace Minisat {
class Proof;
class SatProof;
class CnfProof;
+class TheoryProof;
+class LFSCSatProof;
+class LFSCCnfProof;
+class LFSCTheoryProof;
+
// different proof modes
enum ProofFormat {
LFSC,
class ProofManager {
SatProof* d_satProof;
CnfProof* d_cnfProof;
+ TheoryProof* d_theoryProof;
+
+ Proof* d_fullProof;
ProofFormat d_format;
static ProofManager* proofManager;
static bool isInitialized;
ProofManager(ProofFormat format = LFSC);
+ ~ProofManager();
public:
static ProofManager* currentPM();
-
static void initSatProof(Minisat::Solver* solver);
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
-
- static Proof* getProof();
+ static void initTheoryProof();
+ static Proof* getProof();
static SatProof* getSatProof();
static CnfProof* getCnfProof();
+ 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"; }
};/* class ProofManager */
+class LFSCProof : public Proof {
+ LFSCSatProof* d_satProof;
+ LFSCCnfProof* d_cnfProof;
+ LFSCTheoryProof* d_theoryProof;
+public:
+ LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
+ virtual void toStream(std::ostream& out);
+ virtual ~LFSCProof() {}
+};
+
}/* CVC4 namespace */
#endif /* __CVC4__PROOF_MANAGER_H */
**/
#include "proof/sat_proof.h"
+#include "proof/cnf_proof.h"
+#include "proof/proof_manager.h"
#include "prop/minisat/core/Solver.h"
using namespace std;
d_clauseId(),
d_idUnit(),
d_deleted(),
- d_inputClauses(),
+ d_inputClauses(),
+ d_lemmaClauses(),
d_resChains(),
d_resStack(),
d_checkRes(checkRes),
d_temp_idClause(),
d_unitConflictId(),
d_storedUnitConflict(false),
- d_atomToVar()
+ d_seenLearnt(),
+ d_seenInput(),
+ d_seenLemmas(),
+ d_cnfProof(NULL)
{
d_proxy = new ProofProxy(this);
}
+CnfProof* SatProof::getCnfProof() {
+ Assert (d_cnfProof);
+ return d_cnfProof;
+}
+
+void SatProof::setCnfProof(CnfProof* cnfProof) {
+ Assert (d_cnfProof == NULL);
+ d_cnfProof = cnfProof;
+}
/**
* Returns true if the resolution chain corresponding to id
return d_idClause[id];
}
-Clause& SatProof::getClause(ClauseId id) {
- return d_solver->ca[id];
+Clause& SatProof::getClause(CRef ref) {
+ return d_solver->ca[ref];
}
::Minisat::Lit SatProof::getUnit(ClauseId id) {
Assert (d_idUnit.find(id) != d_idUnit.end());
return (d_inputClauses.find(id) != d_inputClauses.end());
}
+bool SatProof::isLemmaClause(ClauseId id) {
+ return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
+}
+
void SatProof::print(ClauseId id) {
if (d_deleted.find(id) != d_deleted.end()) {
/// registration methods
-ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
Assert(clause != CRef_Undef);
ClauseIdMap::iterator it = d_clauseId.find(clause);
if (it == d_clauseId.end()) {
ClauseId newId = d_idCounter++;
d_clauseId[clause]= newId;
d_idClause[newId] =clause;
- if (isInput) {
+ 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);
+ }
}
- Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n";
+ Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " << kind << "\n";
return d_clauseId[clause];
}
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
UnitIdMap::iterator it = d_unitId.find(toInt(lit));
if (it == d_unitId.end()) {
ClauseId newId = d_idCounter++;
d_unitId[toInt(lit)] = newId;
d_idUnit[newId] = lit;
- if (isInput) {
+ 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);
+ }
+
}
- Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n";
+ Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
return d_unitId[toInt(lit)];
}
}
}
-/// store mapping from theory atoms to new variables
-void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) {
- Assert(d_atomToVar.find(atom) == d_atomToVar.end());
- d_atomToVar[atom] = literal;
+void SatProof::constructProof() {
+ collectClauses(d_emptyClauseId);
}
+// std::string SatProof::varName(::Minisat::Lit lit) {
+// ostringstream os;
+// if (sign(lit)) {
+// os << "(neg "<< ProofManager::getVarPrefix() <<var(lit) << ")" ;
+// }
+// else {
+// os << "(pos "<< ProofManager::getVarPrefix() <<var(lit) << ")";
+// }
+// return os.str();
+// }
-/// LFSCSatProof class
-
-std::string LFSCSatProof::varName(::Minisat::Lit lit) {
- ostringstream os;
- if (sign(lit)) {
- os << "(neg v"<<var(lit) << ")" ;
- }
- else {
- os << "(pos v"<<var(lit) << ")";
- }
- return os.str();
-}
-
-
-std::string LFSCSatProof::clauseName(ClauseId id) {
+std::string SatProof::clauseName(ClauseId id) {
ostringstream os;
if (isInputClause(id)) {
- os << "p"<<id;
+ os << ProofManager::getInputClausePrefix()<<id;
return os.str();
- } else {
- os << "l"<<id;
+ } else
+ if (isLemmaClause(id)) {
+ os << ProofManager::getLemmaClausePrefix()<<id;
+ return os.str();
+ }else {
+ os << ProofManager::getLearntClausePrefix()<<id;
return os.str();
}
}
-void LFSCSatProof::collectLemmas(ClauseId id) {
- if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+void SatProof::collectClauses(ClauseId id) {
+ if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
return;
}
if (d_seenInput.find(id) != d_seenInput.end()) {
return;
}
+ if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+ return;
+ }
if (isInputClause(id)) {
+ CRef input_ref = getClauseRef(id);
+ const Clause& cl = getClause(input_ref);
+ getCnfProof()->addInputClause(id, cl);
d_seenInput.insert(id);
return;
- } else {
+ }
+ else if (isLemmaClause(id)) {
+ CRef lemma_ref = getClauseRef(id);
+ const Clause& cl = getClause(lemma_ref);
+ getCnfProof()->addTheoryLemma(id, cl);
d_seenLemmas.insert(id);
+ }
+ else {
+ d_seenLearnt.insert(id);
}
Assert (d_resChains.find(id) != d_resChains.end());
ResChain* res = d_resChains[id];
ClauseId start = res->getStart();
- collectLemmas(start);
+ collectClauses(start);
ResSteps steps = res->getSteps();
for(unsigned i = 0; i < steps.size(); i++) {
- collectLemmas(steps[i].id);
+ collectClauses(steps[i].id);
}
}
+/// LFSCSatProof class
-
-void LFSCSatProof::printResolution(ClauseId id) {
- d_lemmaSS << "(satlem _ _ _ ";
+void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
+ out << "(satlem_simplify _ _ _ ";
ResChain* res = d_resChains[id];
ResSteps& steps = res->getSteps();
for (int i = steps.size()-1; i >= 0; i--) {
- d_lemmaSS << "(";
- d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ ";
+ out << "(";
+ out << (steps[i].sign? "R" : "Q") << " _ _ ";
}
ClauseId start_id = res->getStart();
- if(isInputClause(start_id)) {
- d_seenInput.insert(start_id);
- }
- d_lemmaSS << clauseName(start_id) << " ";
+ // WHY DID WE NEED THIS?
+ // if(isInputClause(start_id)) {
+ // d_seenInput.insert(start_id);
+ // }
+ out << clauseName(start_id) << " ";
for(unsigned i = 0; i < steps.size(); i++) {
- d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")";
+ out << clauseName(steps[i].id) << " "<<ProofManager::getVarPrefix() << var(steps[i].lit) <<")";
}
if (id == d_emptyClauseId) {
- d_lemmaSS <<"(\\empty empty)";
+ out <<"(\\empty empty)";
return;
}
- d_lemmaSS << "(\\" << clauseName(id) << "\n"; // bind to lemma name
- d_paren << "))"; // closing parethesis for lemma binding and satlem
+ out << "(\\" << clauseName(id) << "\n"; // bind to lemma name
+ 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;
- }
+// 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::printClauses() {
- for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
- printInputClause(*it);
- }
-}
-
-void LFSCSatProof::printVariables() {
- for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
- d_varSS << "(% v" << *it <<" var \n";
- d_paren << ")";
- }
-}
-
-
-void LFSCSatProof::flush(std::ostream& out) {
- out << d_atomsSS.str();
- out << "(check \n";
- d_paren <<")";
- out << d_varSS.str();
- out << d_clauseSS.str();
- out << "(: (holds cln) \n";
- out << d_lemmaSS.str();
- d_paren << "))";
- out << d_paren.str();
- out << "\n";
-}
-
-void LFSCSatProof::toStream(std::ostream& out) {
- Debug("proof:sat") << " LFSCSatProof::printProof \n";
-
- // first collect lemmas to print in reverse order
- collectLemmas(d_emptyClauseId);
- for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) {
+// 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) {
- printResolution(*it);
+ printResolution(*it, out, paren);
}
}
- printAtoms();
- // last resolution to be printed is the empty clause
- printResolution(d_emptyClauseId);
-
- printClauses();
- printVariables();
- flush(out);
+ printResolution(d_emptyClauseId, out, paren);
}
-void LFSCSatProof::printAtoms() {
- d_atomsSS << "; Mapping between boolean variables and theory atoms \n";
- for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) {
- d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n";
- }
-}
+// 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 */
typedef std::hash_set < ClauseId > IdHashSet;
typedef std::vector < ResChain* > ResStack;
-typedef std::hash_set < int > VarSet;
+typedef std::hash_set < unsigned > VarSet;
typedef std::set < ClauseId > IdSet;
typedef std::vector < ::Minisat::Lit > LitVector;
-typedef __gnu_cxx::hash_map<Expr, ::Minisat::Lit, ExprHashFunction > AtomToVar;
+typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
class SatProof;
void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
};/* class ProofProxy */
-class SatProof : public Proof {
+
+enum ClauseKind {
+ INPUT,
+ THEORY_LEMMA,
+ LEARNT
+};
+
+class CnfProof;
+
+class SatProof {
protected:
::Minisat::Solver* d_solver;
// clauses
UnitIdMap d_unitId;
IdHashSet d_deleted;
IdHashSet d_inputClauses;
-
+ IdHashSet d_lemmaClauses;
// resolutions
IdResMap d_resChains;
ResStack d_resStack;
// unit conflict
ClauseId d_unitConflictId;
bool d_storedUnitConflict;
-
- // atom mapping
- AtomToVar d_atomToVar;
public:
SatProof(::Minisat::Solver* solver, bool checkRes = false);
protected:
void printRes(ClauseId id);
void printRes(ResChain* res);
- bool isInputClause(ClauseId id);
+ bool isInputClause(ClauseId id);
+ bool isLemmaClause(ClauseId id);
bool isUnit(ClauseId id);
bool isUnit(::Minisat::Lit lit);
bool hasResolution(ClauseId id);
::Minisat::CRef getClauseRef(ClauseId id);
::Minisat::Lit getUnit(ClauseId id);
ClauseId getUnitId(::Minisat::Lit lit);
- ::Minisat::Clause& getClause(ClauseId id);
+ ::Minisat::Clause& getClause(::Minisat::CRef ref);
virtual void toStream(std::ostream& out);
bool checkResolution(ClauseId id);
void finalizeProof(::Minisat::CRef conflict);
/// clause registration methods
- ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
- ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
+ ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
+ ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
void storeUnitConflict(::Minisat::Lit lit);
void storeUnitResolution(::Minisat::Lit lit);
ProofProxy* getProxy() {return d_proxy; }
- /**
- * At mapping between literal and theory-atom it represents
- *
- * @param literal
- * @param atom
- */
- void storeAtom(::Minisat::Lit literal, Expr atom);
-};/* class SatProof */
-
-class LFSCSatProof: public SatProof {
-private:
- VarSet d_seenVars;
- std::ostringstream d_atomsSS;
- std::ostringstream d_varSS;
- std::ostringstream d_lemmaSS;
- std::ostringstream d_clauseSS;
- std::ostringstream d_paren;
- IdSet d_seenLemmas;
- IdHashSet d_seenInput;
+ /**
+ Constructs the SAT proof identifying the needed lemmas
+ */
+ void constructProof();
+
+protected:
+ IdSet d_seenLearnt;
+ IdHashSet d_seenInput;
+ IdHashSet d_seenLemmas;
+
inline std::string varName(::Minisat::Lit lit);
inline std::string clauseName(ClauseId id);
- void collectLemmas(ClauseId id);
- void printResolution(ClauseId id);
- void printInputClause(ClauseId id);
+ void collectClauses(ClauseId id);
+ CnfProof* d_cnfProof;
+ CnfProof* getCnfProof();
+public:
+ void setCnfProof(CnfProof* cnfProof);
+ virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
+};/* class SatProof */
- void printVariables();
- void printClauses();
- void flush(std::ostream& out);
- void printAtoms();
+class LFSCSatProof: public SatProof {
+private:
+ void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
public:
- LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
- SatProof(solver, checkRes),
- d_seenVars(),
- d_atomsSS(),
- d_varSS(),
- d_lemmaSS(),
- d_paren(),
- d_seenLemmas(),
- d_seenInput()
- {}
- virtual void toStream(std::ostream& out);
+ LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false)
+ : SatProof(solver, checkRes)
+ {}
+ virtual void printResolutions(std::ostream& out, std::ostream& paren);
};/* class LFSCSatProof */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_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-2013 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"
+
+using namespace CVC4;
+
+TheoryProof::TheoryProof()
+ : d_atomSet()
+{}
+void TheoryProof::addAtom(Expr atom) {
+ d_atomSet.insert(atom);
+ Assert (atom.getKind() == kind::EQUAL);
+ addDeclaration(atom[0]);
+ addDeclaration(atom[1]);
+}
+
+void TheoryProof::addDeclaration(Expr term) {
+ 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 {
+ Assert (term.isVariable());
+ Assert (type.isSort());
+ d_termDeclarations.insert(term);
+ }
+}
+
+void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
+ if (term.isVariable()) {
+ os << term;
+ return;
+ }
+ Assert (term.getKind() == kind::APPLY_UF);
+ Expr func = term.getOperator();
+ // only support unary functions so far
+ Assert (func.getNumChildren() == 1);
+ os << "(apply _ _ " << func << " ";
+ printTerm(term[0], os);
+ os <<")";
+}
+
+void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
+ // should make this more general
+ Assert (atom.getKind() == kind::EQUAL);
+ os << "(= ";
+ printTerm(atom[0], os);
+ os << " ";
+ printTerm(atom[1], os);
+ 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";
+ paren << ")";
+ }
+
+ // declaring the terms
+ for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
+ Expr term = *it;
+
+ os << "(% " << term << "(term ";
+ paren <<")";
+
+ Type type = term.getType();
+ if (type.isFunction()) {
+ FunctionType ftype = (FunctionType)type;
+ Assert (ftype.getArity() == 2);
+ Type arg_type = ftype.getArgTypes()[0];
+ Type result_type = ftype.getRangeType();
+ os << "(arrow " << arg_type << " " << result_type << "))\n";
+ } else {
+ Assert (term.isVariable());
+ Assert (type.isSort());
+ os << type << ")\n";
+ }
+ }
+}
--- /dev/null
+/********************* */
+/*! \file theory_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-2013 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.
+ **
+ **
+ **/
+
+
+#ifndef __CVC4__THEORY_PROOF_H
+#define __CVC4__THEORY_PROOF_H
+
+#include "cvc4_private.h"
+#include "util/proof.h"
+#include "expr/expr.h"
+#include <ext/hash_set>
+#include <iostream>
+
+namespace CVC4 {
+
+ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > AtomSet;
+ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > TermSet;
+ typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet;
+
+ class TheoryProof {
+ protected:
+ AtomSet d_atomSet;
+ TermSet d_termDeclarations;
+ SortSet d_sortDeclarations;
+ void addDeclaration(Expr atom);
+ public:
+ TheoryProof();
+ void addAtom(Expr atom);
+ virtual void printFormula(Expr atom, std::ostream& os) = 0;
+ virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0;
+ };
+
+ class LFSCTheoryProof: public TheoryProof {
+ void printTerm(Expr term, std::ostream& os);
+ public:
+ virtual void printFormula(Expr atom, std::ostream& os);
+ virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+ };
+} /* CVC4 namespace */
+#endif /* __CVC4__THEORY_PROOF_H */
// Make a new literal (variables are not considered theory literals)
SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
- PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); );
// Return the resulting literal
return lit;
}
// Assert the constants
uncheckedEnqueue(mkLit(varTrue, false));
uncheckedEnqueue(mkLit(varFalse, true));
- PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), true); )
- PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), true); )
+ PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); )
+ PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); )
}
// Construct the reason
CRef real_reason = ca.alloc(explLevel, explanation, true);
- PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); );
+ PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); );
vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
clauses_removable.push(real_reason);
attachClause(real_reason);
clauses_persistent.push(cr);
attachClause(cr);
- PROOF( ProofManager::getSatProof()->registerClause(cr, true); )
+ PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
}
// Check if it propagates
if(assigns[var(ps[0])] == l_Undef) {
assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
- PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } )
+ PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } )
return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef);
} else return ok;
}
}
lemma_ref = ca.alloc(clauseLevel, lemma, removable);
- PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); );
+ PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); );
if (removable) {
clauses_removable.push(lemma_ref);
} else {
projects / cvc5.git / commitdiff