diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-04 23:50:23 +0000 |
commit | dc4b8296ded0a2288fbfeb71b9ded9217bad6b86 (patch) | |
tree | 7bb1a9d305c46464e0470486e406cdffa9558644 /src/prop/sat.h | |
parent | fb7d93e00e70b36d12c1d5deec914426c982b3cf (diff) |
beautification of the prop engine
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 679b9da8c..195323755 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -16,10 +16,60 @@ #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H +#define __CVC4_USE_MINISAT + +#ifdef __CVC4_USE_MINISAT + +#include "prop/minisat/core/Solver.h" +#include "prop/minisat/core/SolverTypes.h" + namespace CVC4 { namespace prop { +/** The solver we are using */ +typedef minisat::Solver SatSolver; + +/** Type of the SAT variables */ +typedef minisat::Var SatVariable; + +/** Type of the Sat literals */ +typedef minisat::Lit SatLiteral; + +/** Type of the SAT clauses */ +typedef minisat::vec<SatLiteral> SatClause; + +/** + * Returns the variable of the literal. + * @param lit the literal + */ +inline SatVariable literalToVariable(SatLiteral lit) { + return minisat::var(lit); +} + +inline bool literalSign(SatLiteral lit) { + return minisat::sign(lit); +} + +inline std::ostream& operator << (std::ostream& out, SatLiteral lit) { + const char * s = (literalSign(lit)) ? "~" : " "; + out << s << literalToVariable(lit); + return out; +} + +inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { + out << "clause:"; + for(int i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; +} + + }/* CVC4::prop namespace */ }/* CVC4 namespace */ +#endif + + #endif /* __CVC4__PROP__SAT_H */ |