summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/cnf_proof.cpp75
-rw-r--r--src/proof/cnf_proof.h15
-rw-r--r--src/proof/proof_manager.cpp18
-rw-r--r--src/proof/proof_manager.h24
-rw-r--r--src/proof/sat_proof.cpp52
-rw-r--r--src/proof/sat_proof.h4
-rw-r--r--src/proof/theory_proof.cpp15
-rw-r--r--src/prop/minisat/minisat.cpp7
-rw-r--r--src/prop/minisat/minisat.h2
-rw-r--r--src/prop/sat_solver_types.h4
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<unsigned > VarSet;
+typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef __gnu_cxx::hash_set<prop::SatVariable > 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 "<<id<<" "
<< ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
@@ -290,7 +291,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
Clause& SatProof::getClause(CRef ref) {
return d_solver->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()<<id;
+ os << ProofManager::printInputClauseName(id);
return os.str();
} else
if (isLemmaClause(id)) {
- os << ProofManager::getLemmaClausePrefix()<<id;
+ os << ProofManager::printLemmaClauseName(id);
return os.str();
}else {
- os << ProofManager::getLearntClausePrefix()<<id;
+ os << ProofManager::printLearntClauseName(id);
return os.str();
}
}
+void SatProof::addClauseToCnfProof(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);
+ 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) << " "<<ProofManager::getVarPrefix() << var(steps[i].lit) <<")";
+ out << clauseName(steps[i].id) << " "<<ProofManager::printVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
}
if (id == d_emptyClauseId) {
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 0ab86b554..5a1fa4680 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -36,7 +36,7 @@ namespace Minisat {
#include "prop/minisat/core/SolverTypes.h"
#include "util/proof.h"
-
+#include "prop/sat_solver_types.h"
namespace std {
using namespace __gnu_cxx;
}/* std namespace */
@@ -89,7 +89,6 @@ typedef std::hash_map < ClauseId, ResChain*> 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<ClauseId, ::Minisat::Clause& > 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<Minisat::Lit>& 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::Lit>& minisat_clause);
static void toSatClause (Minisat::vec<Minisat::Lit>& 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.
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback