cnf_stream.h \
cnf_stream.cpp \
sat_solver.h \
+ sat_solver_types.h \
sat_solver_factory.h \
sat_solver_factory.cpp \
sat_solver_registry.h \
using namespace CVC4;
using namespace prop;
-MinisatSatSolver::MinisatSatSolver() :
+BVMinisatSatSolver::BVMinisatSatSolver() :
d_minisat(new BVMinisat::SimpSolver())
{
d_statistics.init(d_minisat);
}
-MinisatSatSolver::~MinisatSatSolver() {
+BVMinisatSatSolver::~BVMinisatSatSolver() {
delete d_minisat;
}
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
Debug("sat::minisat") << "Add clause " << clause <<"\n";
BVMinisat::vec<BVMinisat::Lit> minisat_clause;
toMinisatClause(clause, minisat_clause);
d_minisat->addClause(minisat_clause);
}
-SatVariable MinisatSatSolver::newVar(bool freeze){
+SatVariable BVMinisatSatSolver::newVar(bool freeze){
return d_minisat->newVar(true, true, freeze);
}
-void MinisatSatSolver::markUnremovable(SatLiteral lit){
+void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
}
-void MinisatSatSolver::interrupt(){
+void BVMinisatSatSolver::interrupt(){
d_minisat->interrupt();
}
-SatValue MinisatSatSolver::solve(){
+SatValue BVMinisatSatSolver::solve(){
return toSatLiteralValue(d_minisat->solve());
}
-SatValue MinisatSatSolver::solve(long unsigned int& resource){
+SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
if(resource == 0) {
d_minisat->budgetOff();
return result;
}
-SatValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
Debug("sat::minisat") << "Solve with assumptions ";
context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
BVMinisat::vec<BVMinisat::Lit> assump;
}
-void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
+void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
// TODO add assertion to check the call was after an unsat call
for (int i = 0; i < d_minisat->conflict.size(); ++i) {
unsatCore.push_back(toSatLiteral(d_minisat->conflict[i]));
}
}
-SatValue MinisatSatSolver::value(SatLiteral l){
+SatValue BVMinisatSatSolver::value(SatLiteral l){
Unimplemented();
return SAT_VALUE_UNKNOWN;
}
-SatValue MinisatSatSolver::modelValue(SatLiteral l){
+SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
Unimplemented();
return SAT_VALUE_UNKNOWN;
}
-void MinisatSatSolver::unregisterVar(SatLiteral lit) {
+void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
// this should only be called when user context is implemented
// in the BVSatSolver
Unreachable();
}
-void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
+void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) {
// this should only be called when user context is implemented
// in the BVSatSolver
Unreachable();
}
-unsigned MinisatSatSolver::getAssertionLevel() const {
+unsigned BVMinisatSatSolver::getAssertionLevel() const {
// we have no user context implemented so far
return 0;
}
// converting from internal Minisat representation
-SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) {
+SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) {
if (var == var_Undef) {
return undefSatVariable;
}
return SatVariable(var);
}
-BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
+BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) {
if (lit == undefSatLiteral) {
return BVMinisat::lit_Undef;
}
return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
}
-SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
+SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
if (lit == BVMinisat::lit_Undef) {
return undefSatLiteral;
}
BVMinisat::sign(lit));
}
-SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
+SatValue BVMinisatSatSolver::toSatLiteralValue(bool res) {
if(res) return SAT_VALUE_TRUE;
else return SAT_VALUE_FALSE;
}
-SatValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
+SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
Assert(res == (BVMinisat::lbool((uint8_t)1)));
return SAT_VALUE_FALSE;
}
-void MinisatSatSolver::toMinisatClause(SatClause& clause,
+void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
for (unsigned i = 0; i < clause.size(); ++i) {
minisat_clause.push(toMinisatLit(clause[i]));
Assert(clause.size() == (unsigned)minisat_clause.size());
}
-void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
+void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
SatClause& sat_clause) {
for (int i = 0; i < clause.size(); ++i) {
sat_clause.push_back(toSatLiteral(clause[i]));
}
-// Satistics for MinisatSatSolver
+// Satistics for BVMinisatSatSolver
-MinisatSatSolver::Statistics::Statistics() :
+BVMinisatSatSolver::Statistics::Statistics() :
d_statStarts("theory::bv::bvminisat::starts"),
d_statDecisions("theory::bv::bvminisat::decisions"),
d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"),
StatisticsRegistry::registerStat(&d_statEliminatedVars);
}
-MinisatSatSolver::Statistics::~Statistics() {
+BVMinisatSatSolver::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_statStarts);
StatisticsRegistry::unregisterStat(&d_statDecisions);
StatisticsRegistry::unregisterStat(&d_statRndDecisions);
StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
}
-void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
+void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
d_statStarts.setData(minisat->starts);
d_statDecisions.setData(minisat->decisions);
d_statRndDecisions.setData(minisat->rnd_decisions);
namespace CVC4 {
namespace prop {
-class MinisatSatSolver: public BVSatSolverInterface {
+class BVMinisatSatSolver: public BVSatSolverInterface {
BVMinisat::SimpSolver* d_minisat;
public:
- MinisatSatSolver();
- ~MinisatSatSolver();
+ BVMinisatSatSolver();
+ ~BVMinisatSatSolver();
void addClause(SatClause& clause, bool removable);
SatVariable newVar(bool theoryAtom = false);
Statistics d_statistics;
};
-template class SatSolverConstructor<MinisatSatSolver>;
+template class SatSolverConstructor<BVMinisatSatSolver>;
}
}
// Get the explanation from the theory
SatClause explanation_cl;
- proxy->explainPropagation(DPLLMinisatSatSolver::toSatLiteral(l), explanation_cl);
+ proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
vec<Lit> explanation;
- DPLLMinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+ MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
// Sort the literals by trail index level
lemma_lt lt(*this);
int currentLevel = decisionLevel();
for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
variables_to_register[i].level = currentLevel;
- proxy->variableNotify(DPLLMinisatSatSolver::toSatVariable(variables_to_register[i].var));
+ proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var));
}
}
}
Lit nextLit;
#ifdef CVC4_REPLAY
- nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
if (nextLit != lit_Undef) {
return nextLit;
#endif /* CVC4_REPLAY */
// Theory requests
- nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
while (nextLit != lit_Undef) {
if(value(var(nextLit)) == l_Undef) {
Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
} else {
Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
}
- nextLit = DPLLMinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
+ nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionRequest());
}
Var next = var_Undef;
}
if (theory[var(p)]) {
// Enqueue to the theory
- proxy->enqueueTheoryLiteral(DPLLMinisatSatSolver::toSatLiteral(p));
+ proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
}
}
proxy->theoryPropagate(propagatedLiteralsClause);
vec<Lit> propagatedLiterals;
- DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
+ MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
int oldTrailSize = trail.size();
Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
}
#ifdef CVC4_REPLAY
- proxy->logDecision(DPLLMinisatSatSolver::toSatLiteral(next));
+ proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
#endif /* CVC4_REPLAY */
}
//// DPllMinisatSatSolver
-DPLLMinisatSatSolver::DPLLMinisatSatSolver() :
+MinisatSatSolver::MinisatSatSolver() :
d_minisat(NULL),
d_theoryProxy(NULL),
d_context(NULL)
{}
-DPLLMinisatSatSolver::~DPLLMinisatSatSolver() {
+MinisatSatSolver::~MinisatSatSolver() {
delete d_minisat;
}
-SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) {
+SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) {
if (var == var_Undef) {
return undefSatVariable;
}
return SatVariable(var);
}
-Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) {
+Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) {
if (lit == undefSatLiteral) {
return Minisat::lit_Undef;
}
return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
}
-SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
+SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) {
if (lit == Minisat::lit_Undef) {
return undefSatLiteral;
}
Minisat::sign(lit));
}
-SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
if(res) return SAT_VALUE_TRUE;
else return SAT_VALUE_FALSE;
}
-SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
+SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
Assert(res == (Minisat::lbool((uint8_t)1)));
}
-void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause,
+void MinisatSatSolver::toMinisatClause(SatClause& clause,
Minisat::vec<Minisat::Lit>& minisat_clause) {
for (unsigned i = 0; i < clause.size(); ++i) {
minisat_clause.push(toMinisatLit(clause[i]));
Assert(clause.size() == (unsigned)minisat_clause.size());
}
-void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
+void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
SatClause& sat_clause) {
for (int i = 0; i < clause.size(); ++i) {
sat_clause.push_back(toSatLiteral(clause[i]));
}
-void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
+void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
{
d_context = context;
d_statistics.init(d_minisat);
}
-void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
Minisat::vec<Minisat::Lit> minisat_clause;
toMinisatClause(clause, minisat_clause);
d_minisat->addClause(minisat_clause, removable);
}
-SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) {
+SatVariable MinisatSatSolver::newVar(bool theoryAtom) {
return d_minisat->newVar(true, true, theoryAtom);
}
-SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+SatValue MinisatSatSolver::solve(unsigned long& resource) {
Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
if(resource == 0) {
d_minisat->budgetOff();
return result;
}
-SatValue DPLLMinisatSatSolver::solve() {
+SatValue MinisatSatSolver::solve() {
d_minisat->budgetOff();
return toSatLiteralValue(d_minisat->solve());
}
-void DPLLMinisatSatSolver::interrupt() {
+void MinisatSatSolver::interrupt() {
d_minisat->interrupt();
}
-SatValue DPLLMinisatSatSolver::value(SatLiteral l) {
+SatValue MinisatSatSolver::value(SatLiteral l) {
return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
}
-SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+SatValue MinisatSatSolver::modelValue(SatLiteral l){
return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}
-bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
+bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const {
return true;
}
/** Incremental interface */
-unsigned DPLLMinisatSatSolver::getAssertionLevel() const {
+unsigned MinisatSatSolver::getAssertionLevel() const {
return d_minisat->getAssertionLevel();
}
-void DPLLMinisatSatSolver::push() {
+void MinisatSatSolver::push() {
d_minisat->push();
}
-void DPLLMinisatSatSolver::pop(){
+void MinisatSatSolver::pop(){
d_minisat->pop();
}
-void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) {
+void MinisatSatSolver::unregisterVar(SatLiteral lit) {
d_minisat->unregisterVar(toMinisatLit(lit));
}
-void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) {
+void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
d_minisat->renewVar(toMinisatLit(lit), level);
}
-/// Statistics for DPLLMinisatSatSolver
+/// Statistics for MinisatSatSolver
-DPLLMinisatSatSolver::Statistics::Statistics() :
+MinisatSatSolver::Statistics::Statistics() :
d_statStarts("sat::starts"),
d_statDecisions("sat::decisions"),
d_statRndDecisions("sat::rnd_decisions"),
StatisticsRegistry::registerStat(&d_statMaxLiterals);
StatisticsRegistry::registerStat(&d_statTotLiterals);
}
-DPLLMinisatSatSolver::Statistics::~Statistics() {
+MinisatSatSolver::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_statStarts);
StatisticsRegistry::unregisterStat(&d_statDecisions);
StatisticsRegistry::unregisterStat(&d_statRndDecisions);
StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
StatisticsRegistry::unregisterStat(&d_statTotLiterals);
}
-void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
+void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
d_statStarts.setData(d_minisat->starts);
d_statDecisions.setData(d_minisat->decisions);
d_statRndDecisions.setData(d_minisat->rnd_decisions);
namespace CVC4 {
namespace prop {
-class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
+class MinisatSatSolver : public DPLLSatSolverInterface {
/** The SatSolver used */
Minisat::SimpSolver* d_minisat;
public:
- DPLLMinisatSatSolver ();
- ~DPLLMinisatSatSolver();
+ MinisatSatSolver ();
+ ~MinisatSatSolver();
static SatVariable toSatVariable(Minisat::Var var);
static Minisat::Lit toMinisatLit(SatLiteral lit);
};
-template class SatSolverConstructor<DPLLMinisatSatSolver>;
+template class SatSolverConstructor<MinisatSatSolver>;
} // prop namespace
} // cvc4 namespace
#include "util/options.h"
#include "util/stats.h"
#include "context/cdlist.h"
+#include "prop/sat_solver_types.h"
namespace CVC4 {
namespace prop {
class TheoryProxy;
-/**
- * Boolean values of the SAT solver.
- */
-enum SatValue {
- SAT_VALUE_UNKNOWN,
- SAT_VALUE_TRUE,
- SAT_VALUE_FALSE
-};
-
-/**
- * A variable of the SAT solver.
- */
-typedef uint64_t SatVariable;
-
-/**
- * Undefined SAT solver variable.
- */
-const SatVariable undefSatVariable = SatVariable(-1);
-
-/**
- * A SAT literal is a variable or an negated variable.
- */
-class SatLiteral {
-
- /**
- * The value holds the variable and a bit noting if the variable is negated.
- */
- uint64_t d_value;
-
-public:
-
- /**
- * Construct an undefined SAT literal.
- */
- SatLiteral()
- : d_value(undefSatVariable)
- {}
-
- /**
- * Construct a literal given a possible negated variable.
- */
- SatLiteral(SatVariable var, bool negated = false) {
- d_value = var + var + (int)negated;
- }
-
- /**
- * Returns the variable of the literal.
- */
- SatVariable getSatVariable() const {
- return d_value >> 1;
- }
-
- /**
- * Returns true if the literal is a negated variable.
- */
- bool isNegated() const {
- return d_value & 1;
- }
-
- /**
- * Negate the given literal.
- */
- SatLiteral operator ~ () const {
- return SatLiteral(getSatVariable(), !isNegated());
- }
-
- /**
- * Compare two literals for equality.
- */
- bool operator == (const SatLiteral& other) const {
- return d_value == other.d_value;
- }
-
- /**
- * Compare two literals for dis-equality.
- */
- bool operator != (const SatLiteral& other) const {
- return !(*this == other);
- }
-
- /**
- * Returns a string representation of the literal.
- */
- std::string toString() const {
- std::ostringstream os;
- os << (isNegated()? "~" : "") << getSatVariable() << " ";
- return os.str();
- }
-
- /**
- * Returns the hash value of a literal.
- */
- size_t hash() const {
- return (size_t)d_value;
- }
-
- /**
- * Returns true if the literal is undefined.
- */
- bool isNull() const {
- return getSatVariable() == undefSatVariable;
- }
-};
-
-/**
- * A constant representing a undefined literal.
- */
-const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
-
-/**
- * Helper for hashing the literals.
- */
-struct SatLiteralHashFunction {
- inline size_t operator() (const SatLiteral& literal) const {
- return literal.hash();
- }
-};
-
-/**
- * A SAT clause is a vector of literals.
- */
-typedef std::vector<SatLiteral> SatClause;
-
class SatSolver {
public:
using namespace prop;
BVSatSolverInterface* SatSolverFactory::createMinisat() {
- return new MinisatSatSolver();
+ return new BVMinisatSatSolver();
}
DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
- return new DPLLMinisatSatSolver();
+ return new MinisatSatSolver();
}
SatSolver* SatSolverFactory::create(const char* name) {
--- /dev/null
+/********************* */
+/*! \file cnf_stream.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This class transforms a sequence of formulas into clauses.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositionally
+ ** equi-satisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Unlike other parts of the system it is aware of the PropEngine's
+ ** internals such as the representation and translation of [??? -Chris]
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
+ * Boolean values of the SAT solver.
+ */
+enum SatValue {
+ SAT_VALUE_UNKNOWN,
+ SAT_VALUE_TRUE,
+ SAT_VALUE_FALSE
+};
+
+/**
+ * A variable of the SAT solver.
+ */
+typedef uint64_t SatVariable;
+
+/**
+ * Undefined SAT solver variable.
+ */
+const SatVariable undefSatVariable = SatVariable(-1);
+
+/**
+ * A SAT literal is a variable or an negated variable.
+ */
+class SatLiteral {
+
+ /**
+ * The value holds the variable and a bit noting if the variable is negated.
+ */
+ uint64_t d_value;
+
+public:
+
+ /**
+ * Construct an undefined SAT literal.
+ */
+ SatLiteral()
+ : d_value(undefSatVariable)
+ {}
+
+ /**
+ * Construct a literal given a possible negated variable.
+ */
+ SatLiteral(SatVariable var, bool negated = false) {
+ d_value = var + var + (int)negated;
+ }
+
+ /**
+ * Returns the variable of the literal.
+ */
+ SatVariable getSatVariable() const {
+ return d_value >> 1;
+ }
+
+ /**
+ * Returns true if the literal is a negated variable.
+ */
+ bool isNegated() const {
+ return d_value & 1;
+ }
+
+ /**
+ * Negate the given literal.
+ */
+ SatLiteral operator ~ () const {
+ return SatLiteral(getSatVariable(), !isNegated());
+ }
+
+ /**
+ * Compare two literals for equality.
+ */
+ bool operator == (const SatLiteral& other) const {
+ return d_value == other.d_value;
+ }
+
+ /**
+ * Compare two literals for dis-equality.
+ */
+ bool operator != (const SatLiteral& other) const {
+ return !(*this == other);
+ }
+
+ /**
+ * Returns a string representation of the literal.
+ */
+ std::string toString() const {
+ std::ostringstream os;
+ os << (isNegated()? "~" : "") << getSatVariable() << " ";
+ return os.str();
+ }
+
+ /**
+ * Returns the hash value of a literal.
+ */
+ size_t hash() const {
+ return (size_t)d_value;
+ }
+
+ /**
+ * Returns true if the literal is undefined.
+ */
+ bool isNull() const {
+ return getSatVariable() == undefSatVariable;
+ }
+};
+
+/**
+ * A constant representing a undefined literal.
+ */
+const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable);
+
+/**
+ * Helper for hashing the literals.
+ */
+struct SatLiteralHashFunction {
+ inline size_t operator() (const SatLiteral& literal) const {
+ return literal.hash();
+ }
+};
+
+/**
+ * A SAT clause is a vector of literals.
+ */
+typedef std::vector<SatLiteral> SatClause;
+
+/**
+ * Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
+ * so that the SAT solver can (or should) remove them when the lifespan is over.
+ */
+enum SatSolverLifespan
+{
+ /**
+ * The object should stay forever and never be removed
+ */
+ SAT_LIFESPAN_PERMANENT,
+ /**
+ * The object can be removed at any point when it becomes unnecessary.
+ */
+ SAT_LIFESPAN_REMOVABLE,
+ /**
+ * The object must be removed as soon as the SAT solver exits the search context
+ * where the object got introduced.
+ */
+ SAT_LIFESPAN_SEARCH_CONTEXT_STRICT,
+ /**
+ * The object can be removed when SAT solver exits the search context where the object
+ * got introduced, but can be kept at the solver discretion.
+ */
+ SAT_LIFESPAN_SEARCH_CONTEXT_LENIENT,
+ /**
+ * The object must be removed as soon as the SAT solver exits the user-level context where
+ * the object got introduced.
+ */
+ SAT_LIFESPAN_USER_CONTEXT_STRICT,
+ /**
+ * The object can be removed when the SAT solver exits the user-level context where
+ * the object got introduced.
+ */
+ SAT_LIFESPAN_USER_CONTEXT_LENIENT
+};
+
+}
+}
+
+
projects / cvc5.git / commitdiff