cnf_stream.h \
cnf_stream.cpp \
sat_solver.h \
- sat_solver.cpp
-
+ sat_solver_factory.h \
+ sat_solver_factory.cpp
+
SUBDIRS = minisat bvminisat
d_minisat->interrupt();
}
-SatLiteralValue MinisatSatSolver::solve(){
+SatValue MinisatSatSolver::solve(){
return toSatLiteralValue(d_minisat->solve());
}
-SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){
+SatValue MinisatSatSolver::solve(long unsigned int& resource){
Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
if(resource == 0) {
d_minisat->budgetOff();
}
BVMinisat::vec<BVMinisat::Lit> empty;
unsigned long conflictsBefore = d_minisat->conflicts;
- SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+ SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
d_minisat->clearInterrupt();
resource = d_minisat->conflicts - conflictsBefore;
Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
return result;
}
-SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){
+SatValue MinisatSatSolver::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;
}
Debug("sat::minisat") <<"\n";
- SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump));
+ SatValue result = toSatLiteralValue(d_minisat->solve(assump));
return result;
}
}
}
-SatLiteralValue MinisatSatSolver::value(SatLiteral l){
+SatValue MinisatSatSolver::value(SatLiteral l){
Unimplemented();
- return SatValUnknown;
+ return SAT_VALUE_UNKNOWN;
}
-SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){
+SatValue MinisatSatSolver::modelValue(SatLiteral l){
Unimplemented();
- return SatValUnknown;
+ return SAT_VALUE_UNKNOWN;
}
void MinisatSatSolver::unregisterVar(SatLiteral lit) {
BVMinisat::sign(lit));
}
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) {
- if(res) return SatValTrue;
- else return SatValFalse;
+SatValue MinisatSatSolver::toSatLiteralValue(bool res) {
+ if(res) return SAT_VALUE_TRUE;
+ else return SAT_VALUE_FALSE;
}
-SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
- if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue;
- if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown;
+SatValue MinisatSatSolver::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 SatValFalse;
+ return SAT_VALUE_FALSE;
}
void MinisatSatSolver::toMinisatClause(SatClause& clause,
void interrupt();
- SatLiteralValue solve();
- SatLiteralValue solve(long unsigned int&);
- SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions);
+ SatValue solve();
+ SatValue solve(long unsigned int&);
+ SatValue solve(const context::CDList<SatLiteral> & assumptions);
void getUnsatCore(SatClause& unsatCore);
- SatLiteralValue value(SatLiteral l);
- SatLiteralValue modelValue(SatLiteral l);
+ SatValue value(SatLiteral l);
+ SatValue modelValue(SatLiteral l);
void unregisterVar(SatLiteral lit);
void renewVar(SatLiteral lit, int level = -1);
static SatVariable toSatVariable(BVMinisat::Var var);
static BVMinisat::Lit toMinisatLit(SatLiteral lit);
static SatLiteral toSatLiteral(BVMinisat::Lit lit);
- static SatLiteralValue toSatLiteralValue(bool res);
- static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res);
+ static SatValue toSatLiteralValue(bool res);
+ static SatValue toSatLiteralValue(BVMinisat::lbool res);
static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
Minisat::sign(lit));
}
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
- if(res) return SatValTrue;
- else return SatValFalse;
+SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) {
+ if(res) return SAT_VALUE_TRUE;
+ else return SAT_VALUE_FALSE;
}
-SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) {
- if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue;
- if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown;
+SatValue DPLLMinisatSatSolver::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)));
- return SatValFalse;
+ return SAT_VALUE_FALSE;
}
}
-SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
+SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) {
Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
if(resource == 0) {
d_minisat->budgetOff();
}
Minisat::vec<Minisat::Lit> empty;
unsigned long conflictsBefore = d_minisat->conflicts;
- SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
+ SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
d_minisat->clearInterrupt();
resource = d_minisat->conflicts - conflictsBefore;
Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
return result;
}
-SatLiteralValue DPLLMinisatSatSolver::solve() {
+SatValue DPLLMinisatSatSolver::solve() {
d_minisat->budgetOff();
return toSatLiteralValue(d_minisat->solve());
}
d_minisat->interrupt();
}
-SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) {
+SatValue DPLLMinisatSatSolver::value(SatLiteral l) {
return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
}
-SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
+SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){
return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
}
static SatVariable toSatVariable(Minisat::Var var);
static Minisat::Lit toMinisatLit(SatLiteral lit);
static SatLiteral toSatLiteral(Minisat::Lit lit);
- static SatLiteralValue toSatLiteralValue(bool res);
- static SatLiteralValue toSatLiteralValue(Minisat::lbool res);
+ static SatValue toSatLiteralValue(bool res);
+ static SatValue toSatLiteralValue(Minisat::lbool res);
static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
static void toSatClause (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
SatVariable newVar(bool theoryAtom = false);
- SatLiteralValue solve();
- SatLiteralValue solve(long unsigned int&);
+ SatValue solve();
+ SatValue solve(long unsigned int&);
void interrupt();
- SatLiteralValue value(SatLiteral l);
+ SatValue value(SatLiteral l);
- SatLiteralValue modelValue(SatLiteral l);
+ SatValue modelValue(SatLiteral l);
bool properExplanation(SatLiteral lit, SatLiteral expl) const;
#include "prop/prop_engine.h"
#include "prop/theory_proxy.h"
#include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
#include "theory/theory_engine.h"
#include "theory/theory_registrar.h"
SatLiteral l = curr.second.literal;
if(!l.isNegated()) {
Node n = curr.first;
- SatLiteralValue value = d_satSolver->modelValue(l);
+ SatValue value = d_satSolver->modelValue(l);
Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
}
}
d_interrupted = false;
// Check the problem
- SatLiteralValue result = d_satSolver->solve(resource);
+ SatValue result = d_satSolver->solve(resource);
millis = d_satTimer.elapsed();
- if( result == SatValUnknown ) {
+ if( result == SAT_VALUE_UNKNOWN ) {
Result::UnknownExplanation why =
d_satTimer.expired() ? Result::TIMEOUT :
(d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT);
return Result(Result::SAT_UNKNOWN, why);
}
- if( result == SatValTrue && Debug.isOn("prop") ) {
+ if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) {
printSatisfyingAssignment();
}
Debug("prop") << "PropEngine::checkSat() => " << result << endl;
- if(result == SatValTrue && d_theoryEngine->isIncomplete()) {
+ if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
}
- return Result(result == SatValTrue ? Result::SAT : Result::UNSAT);
+ return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
}
Node PropEngine::getValue(TNode node) const {
SatLiteral lit = d_cnfStream->getLiteral(node);
- SatLiteralValue v = d_satSolver->value(lit);
- if(v == SatValTrue) {
+ SatValue v = d_satSolver->value(lit);
+ if(v == SAT_VALUE_TRUE) {
return NodeManager::currentNM()->mkConst(true);
- } else if(v == SatValFalse) {
+ } else if(v == SAT_VALUE_FALSE) {
return NodeManager::currentNM()->mkConst(false);
} else {
- Assert(v == SatValUnknown);
+ Assert(v == SAT_VALUE_UNKNOWN);
return Node::null();
}
}
SatLiteral lit = d_cnfStream->getLiteral(node);
- SatLiteralValue v = d_satSolver->value(lit);
- if(v == SatValTrue) {
+ SatValue v = d_satSolver->value(lit);
+ if(v == SAT_VALUE_TRUE) {
value = true;
return true;
- } else if(v == SatValFalse) {
+ } else if(v == SAT_VALUE_FALSE) {
value = false;
return true;
} else {
- Assert(v == SatValUnknown);
+ Assert(v == SAT_VALUE_UNKNOWN);
return false;
}
}
+++ /dev/null
-/********************* */
-/*! \file sat.cpp
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: dejan, taking, mdeters, lianah
- ** Minor contributors (to current version): none
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "prop/prop_engine.h"
-#include "prop/sat_solver.h"
-#include "context/context.h"
-#include "theory/theory_engine.h"
-#include "expr/expr_stream.h"
-#include "prop/theory_proxy.h"
-
-#include "prop/minisat/minisat.h"
-#include "prop/bvminisat/bvminisat.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace prop {
-
-string SatLiteral::toString() {
- ostringstream os;
- os << (isNegated()? "~" : "") << getSatVariable() << " ";
- return os.str();
-}
-
-BVSatSolverInterface* SatSolverFactory::createMinisat() {
- return new MinisatSatSolver();
-}
-
-DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(){
- return new DPLLMinisatSatSolver();
-}
-
-
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
** SAT Solver.
**/
-#include "cvc4_private.h"
+#include "cvc4_public.h"
#ifndef __CVC4__PROP__SAT_MODULE_H
#define __CVC4__PROP__SAT_MODULE_H
class TheoryProxy;
-enum SatLiteralValue {
- SatValUnknown,
- SatValTrue,
- SatValFalse
+/**
+ * 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;
-// special constant
+
+/**
+ * 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:
- SatLiteral() :
- d_value(undefSatVariable)
+
+ /**
+ * Construct an undefined SAT literal.
+ */
+ SatLiteral()
+ : d_value(undefSatVariable)
{}
- SatLiteral(SatVariable var, bool negated = false) { d_value = var + var + (int)negated; }
- SatLiteral operator~() {
+ /**
+ * 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());
}
- bool operator==(const SatLiteral& other) const {
+
+ /**
+ * Compare two literals for equality.
+ */
+ bool operator == (const SatLiteral& other) const {
return d_value == other.d_value;
}
- bool operator!=(const SatLiteral& other) const {
+
+ /**
+ * Compare two literals for dis-equality.
+ */
+ bool operator != (const SatLiteral& other) const {
return !(*this == other);
}
- std::string toString();
- bool isNegated() const { return d_value & 1; }
- size_t toHash() const {return (size_t)d_value; }
- bool isNull() const { return d_value == (uint64_t)-1; }
- SatVariable getSatVariable() const {return d_value >> 1; }
+
+ /**
+ * 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;
+ }
};
-// special constant
+/**
+ * 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.toHash();
+ return literal.hash();
}
};
+/**
+ * A SAT clause is a vector of literals.
+ */
typedef std::vector<SatLiteral> SatClause;
class SatSolver {
+
public:
- /** Virtual destructor to make g++ happy */
+
+ /** Virtual destructor */
virtual ~SatSolver() { }
/** Assert a clause in the solver. */
/** Check the satisfiability of the added clauses */
- virtual SatLiteralValue solve() = 0;
+ virtual SatValue solve() = 0;
/** Check the satisfiability of the added clauses */
- virtual SatLiteralValue solve(long unsigned int&) = 0;
+ virtual SatValue solve(long unsigned int&) = 0;
/** Interrupt the solver */
virtual void interrupt() = 0;
/** Call value() during the search.*/
- virtual SatLiteralValue value(SatLiteral l) = 0;
+ virtual SatValue value(SatLiteral l) = 0;
/** Call modelValue() when the search is done.*/
- virtual SatLiteralValue modelValue(SatLiteral l) = 0;
+ virtual SatValue modelValue(SatLiteral l) = 0;
virtual void unregisterVar(SatLiteral lit) = 0;
class BVSatSolverInterface: public SatSolver {
public:
- virtual SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions) = 0;
+ virtual SatValue solve(const context::CDList<SatLiteral> & assumptions) = 0;
virtual void markUnremovable(SatLiteral lit) = 0;
};
-class SatSolverFactory {
-public:
- static BVSatSolverInterface* createMinisat();
- static DPLLSatSolverInterface* createDPLLMinisat();
-};
-
}/* prop namespace */
inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
return out;
}
-inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) {
+inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
std::string str;
switch(val) {
- case prop::SatValUnknown:
+ case prop::SAT_VALUE_UNKNOWN:
str = "_";
break;
- case prop::SatValTrue:
+ case prop::SAT_VALUE_TRUE:
str = "1";
break;
- case prop::SatValFalse:
+ case prop::SAT_VALUE_FALSE:
str = "0";
break;
default:
--- /dev/null
+/********************* */
+/*! \file sat_solver_factory.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** 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 SAT Solver creation facility.
+ **
+ ** SAT Solver.
+ **/
+
+#include "prop/sat_solver_factory.h"
+#include "prop/minisat/minisat.h"
+#include "prop/bvminisat/bvminisat.h"
+
+using namespace CVC4;
+using namespace prop;
+
+BVSatSolverInterface* SatSolverFactory::createMinisat() {
+ return new MinisatSatSolver();
+}
+
+DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
+ return new DPLLMinisatSatSolver();
+}
+
+
+
+
--- /dev/null
+/********************* */
+/*! \file sat_solver_factory.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** 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 SAT Solver.
+ **
+ ** SAT Solver creation facility
+ **/
+
+#pragma once
+
+#include "cvc4_public.h"
+
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace prop {
+
+class SatSolverFactory {
+public:
+ static BVSatSolverInterface* createMinisat();
+ static DPLLSatSolverInterface* createDPLLMinisat();
+};
+
+}
+}
+
+
+
#include "theory/rewriter.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
using namespace std;
bool Bitblaster::solve() {
Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
- return SatValTrue == d_satSolver->solve(d_assertedAtoms);
+ return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms);
}
void Bitblaster::getConflict(std::vector<TNode>& conflict) {
void interrupt() {
}
- SatLiteralValue solve() {
- return SatValUnknown;
+ SatValue solve() {
+ return SAT_VALUE_UNKNOWN;
}
- SatLiteralValue solve(long unsigned int& resource) {
- return SatValUnknown;
+ SatValue solve(long unsigned int& resource) {
+ return SAT_VALUE_UNKNOWN;
}
- SatLiteralValue value(SatLiteral l) {
- return SatValUnknown;
+ SatValue value(SatLiteral l) {
+ return SAT_VALUE_UNKNOWN;
}
- SatLiteralValue modelValue(SatLiteral l) {
- return SatValUnknown;
+ SatValue modelValue(SatLiteral l) {
+ return SAT_VALUE_UNKNOWN;
}
bool properExplanation(SatLiteral lit, SatLiteral expl) const {
projects / cvc5.git / commitdiff