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::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(prop::SatVariable var) {
- d_propVars.insert(var);
- Expr atom = getAtom(var);
- getTheoryProof()->addAtom(atom);
-}
Expr CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
}
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) {
+ ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
+ ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
+
+ for (;it != end; ++it) {
Expr atom = getAtom(*it);
os << "(decl_atom ";
- getTheoryProof()->printFormula(atom, os);
- os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n";
+ LFSCTheoryProof::printFormula(atom, os);
+ os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
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) {
+ os << " ;; Input 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;
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
os << " (clausify_false trust)" << clause_paren.str();
- os << "( \\ " << ProofManager::printInputClauseName(id) << "\n";
+ os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
paren << "))";
}
}
void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
os << " ;; Theory Lemmas \n";
- for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
+ ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
+ ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
+
+ for (; it != end; ++it) {
ClauseId id = it->first;
const prop::SatClause* clause = it->second;
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
os << " (clausify_false trust)" << clause_paren.str();
- os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n";
+ os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
paren << "))";
}
}
prop::SatLiteral lit = clause[i];
prop::SatVariable var = lit.getSatVariable();
if (lit.isNegated()) {
- os << "(ast _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+ os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
paren << "))";
} else {
- os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+ os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
paren << "))";
}
}
class CnfStream;
}
-typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
-typedef __gnu_cxx::hash_set<prop::SatVariable > 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(prop::SatVariable var);
public:
CnfProof(CVC4::prop::CnfStream* cnfStream);
- 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();
delete d_satProof;
delete d_cnfProof;
delete d_theoryProof;
- delete d_fullProof;
+ delete d_fullProof;
+ 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;
+ }
+ // FIXME: memory leak because there are deleted theory lemmas that were not used in the
+ // SatProof
}
ProofManager* ProofManager::currentPM() {
}
-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()); }
+std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); }
+std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); }
+std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); }
+std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); }
+std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+
+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) {
+ d_inputClauses.insert(std::make_pair(id, clause));
+ return;
+ }
+ Assert (kind == THEORY_LEMMA);
+ d_theoryLemmas.insert(std::make_pair(id, clause));
+}
+
+void ProofManager::addAssertion(Expr formula) {
+ d_inputFormulas.insert(formula);
+}
LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
, 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);
d_theoryProof->printAssertions(out, paren);
out << "(: (holds cln) \n";
d_cnfProof->printAtomMapping(out, 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 */
namespace prop {
typedef uint64_t SatVariable;
class SatLiteral;
+typedef std::vector<SatLiteral> SatClause;
}
// different proof modes
std::string append(const std::string& str, uint64_t num);
+typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+
+typedef int ClauseId;
+
+enum ClauseKind {
+ INPUT,
+ THEORY_LEMMA,
+ LEARNT
+};
+
class ProofManager {
- SatProof* d_satProof;
- CnfProof* d_cnfProof;
+ SatProof* d_satProof;
+ CnfProof* d_cnfProof;
TheoryProof* d_theoryProof;
+ // information that will need to be shared across proofs
+ IdToClause d_inputClauses;
+ IdToClause d_theoryLemmas;
+ ExprSet d_inputFormulas;
+ VarSet d_propVars;
+
Proof* d_fullProof;
ProofFormat d_format;
~ProofManager();
public:
static ProofManager* currentPM();
- static void initSatProof(Minisat::Solver* solver);
- static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
- static void initTheoryProof();
- static Proof* getProof();
- static SatProof* getSatProof();
- static CnfProof* getCnfProof();
+ // initialization
+ static void initSatProof(Minisat::Solver* solver);
+ static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
+ static void initTheoryProof();
+
+ static Proof* getProof();
+ static SatProof* getSatProof();
+ static CnfProof* getCnfProof();
static TheoryProof* getTheoryProof();
+ // iterators over data shared by proofs
+ typedef IdToClause::const_iterator clause_iterator;
+ typedef ExprSet::const_iterator assertions_iterator;
+ typedef VarSet::const_iterator var_iterator;
+
+ clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
+ clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
+
+ clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+ clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+
+ assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
+ assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+
+ var_iterator begin_vars() const { return d_propVars.begin(); }
+ var_iterator end_vars() const { return d_propVars.end(); }
+
+ void addAssertion(Expr formula);
+ void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+
// variable prefixes
- static std::string printInputClauseName(ClauseId id);
- static std::string printLemmaClauseName(ClauseId id);
- static std::string printLearntClauseName(ClauseId id);
+ static std::string getInputClauseName(ClauseId id);
+ static std::string getLemmaClauseName(ClauseId id);
+ static std::string getLearntClauseName(ClauseId id);
- static std::string printVarName(prop::SatVariable var);
- static std::string printAtomName(prop::SatVariable var);
- static std::string printLitName(prop::SatLiteral lit);
+ static std::string getVarName(prop::SatVariable var);
+ static std::string getAtomName(prop::SatVariable var);
+ static std::string getLitName(prop::SatLiteral lit);
};/* class ProofManager */
class LFSCProof : public Proof {
**/
#include "proof/sat_proof.h"
-#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/minisat.h"
d_storedUnitConflict(false),
d_seenLearnt(),
d_seenInput(),
- d_seenLemmas(),
- d_cnfProof(NULL)
+ d_seenLemmas()
{
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
* does resolve to the clause associated to id
std::string SatProof::clauseName(ClauseId id) {
ostringstream os;
if (isInputClause(id)) {
- os << ProofManager::printInputClauseName(id);
+ os << ProofManager::getInputClauseName(id);
return os.str();
} else
if (isLemmaClause(id)) {
- os << ProofManager::printLemmaClauseName(id);
+ os << ProofManager::getLemmaClauseName(id);
return os.str();
}else {
- os << ProofManager::printLearntClauseName(id);
+ os << ProofManager::getLearntClauseName(id);
return os.str();
}
}
-void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) {
+void SatProof::addToProofManager(ClauseId id, ClauseKind kind) {
if (isUnit(id)) {
Minisat::Lit lit = getUnit(id);
prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit);
prop::SatClause* clause = new SatClause();
clause->push_back(sat_lit);
- getCnfProof()->addClause(id, clause, kind);
+ ProofManager::currentPM()->addClause(id, clause, kind);
return;
}
if (isDeleted(id)) {
Assert (kind == THEORY_LEMMA);
SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
- getCnfProof()->addClause(id, clause, kind);
+ ProofManager::currentPM()->addClause(id, clause, kind);
return;
}
const Clause& minisat_cl = getClause(ref);
SatClause* clause = new SatClause();
MinisatSatSolver::toSatClause(minisat_cl, *clause);
- getCnfProof()->addClause(id, clause, kind);
+ ProofManager::currentPM()->addClause(id, clause, kind);
}
void SatProof::collectClauses(ClauseId id) {
}
if (isInputClause(id)) {
- addClauseToCnfProof(id, INPUT);
+ addToProofManager(id, INPUT);
d_seenInput.insert(id);
return;
}
else if (isLemmaClause(id)) {
- addClauseToCnfProof(id, THEORY_LEMMA);
+ addToProofManager(id, THEORY_LEMMA);
d_seenLemmas.insert(id);
return;
}
out << clauseName(start_id) << " ";
for(unsigned i = 0; i < steps.size(); i++) {
- out << clauseName(steps[i].id) << " "<<ProofManager::printVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
+ out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
}
if (id == d_emptyClauseId) {
#include <ext/hash_set>
#include <sstream>
#include "expr/expr.h"
-
+#include "proof/proof_manager.h"
namespace Minisat {
class Solver;
void printDebug(::Minisat::Lit l);
void printDebug(::Minisat::Clause& c);
-typedef int ClauseId;
struct ResStep {
::Minisat::Lit lit;
ClauseId id;
};/* class ProofProxy */
-enum ClauseKind {
- INPUT,
- THEORY_LEMMA,
- LEARNT
-};
-
class CnfProof;
class SatProof {
inline std::string clauseName(ClauseId id);
void collectClauses(ClauseId id);
- CnfProof* d_cnfProof;
- CnfProof* getCnfProof();
- void addClauseToCnfProof(ClauseId id, ClauseKind kind);
+ void addToProofManager(ClauseId id, ClauseKind kind);
public:
- void setCnfProof(CnfProof* cnfProof);
virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
};/* class SatProof */
**/
#include "proof/theory_proof.h"
-
+#include "proof/proof_manager.h"
using namespace CVC4;
TheoryProof::TheoryProof()
- : d_atomSet()
- , d_inputFormulas()
- , d_termDeclarations()
+ : d_termDeclarations()
, d_sortDeclarations()
, d_declarationCache()
{}
-void TheoryProof::addAtom(Expr atom) {
- d_atomSet.insert(atom);
- Assert (atom.getKind() == kind::EQUAL);
- addDeclaration(atom[0]);
- addDeclaration(atom[1]);
-}
-
-void TheoryProof::assertFormula(Expr formula) {
- d_inputFormulas.insert(formula);
- addDeclaration(formula);
-}
-
void TheoryProof::addDeclaration(Expr term) {
if (d_declarationCache.count(term))
return;
}
void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
- unsigned counter = 0;
- for (ExprSet::const_iterator it = d_inputFormulas.begin(); it != d_inputFormulas.end(); ++it) {
+ 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) {
+ addDeclaration(*it);
+ }
+ printDeclarations(os, paren);
+
+ it = ProofManager::currentPM()->begin_assertions();
+ for (; it != end; ++it) {
os << "(% A" << counter++ << " (th_holds ";
printFormula(*it, os);
os << ")\n";
namespace CVC4 {
- typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+
typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet;
-
+ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
class TheoryProof {
protected:
- ExprSet d_atomSet;
- ExprSet d_inputFormulas;
ExprSet d_termDeclarations;
SortSet d_sortDeclarations;
ExprSet d_declarationCache;
void addDeclaration(Expr atom);
public:
TheoryProof();
- void addAtom(Expr atom);
- void assertFormula(Expr formula);
- virtual void printFormula(Expr atom, std::ostream& os) = 0;
- virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0;
virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
};
class LFSCTheoryProof: public TheoryProof {
- void printTerm(Expr term, std::ostream& os);
+ static void printTerm(Expr term, std::ostream& os);
+ void printDeclarations(std::ostream& os, std::ostream& paren);
public:
- virtual void printFormula(Expr atom, std::ostream& os);
- virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+ static void printFormula(Expr atom, std::ostream& os);
virtual void printAssertions(std::ostream& os, std::ostream& paren);
};
} /* CVC4 namespace */
Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
#ifdef CVC4_PROOF
// if (options::proof()) { <-- SEGFAULT!!
- ProofManager::currentPM()->getTheoryProof()->assertFormula(ex);
+ ProofManager::currentPM()->addAssertion(ex);
//}
#endif
SmtScope smts(this);
Assert(ex.getExprManager() == d_exprManager);
#ifdef CVC4_PROOF
// if (options::proof()) { <-- SEGFAULT!!!
- ProofManager::currentPM()->getTheoryProof()->assertFormula(ex);
+ ProofManager::currentPM()->addAssertion(ex);
// }
#endif
SmtScope smts(this);
projects / cvc5.git / commitdiff