diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 22:50:17 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-14 22:50:17 +0000 |
commit | 07e1a1668a27e90563f23bcf5abb5cb7fe30da86 (patch) | |
tree | 6af918e2d1c753b1254fbfb20677618a489ecd01 /src/prop/sat.h | |
parent | 06b5f38e17a1275e966e50c2d74274ef4d4d4697 (diff) |
Adding debugging code in PropEngine/CnfStream
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 33ab674c9..42f454820 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -54,6 +54,8 @@ typedef minisat::Lit SatLiteral; /** Type of the SAT clauses */ typedef minisat::vec<SatLiteral> SatClause; +typedef minisat::lbool SatLiteralValue; + /** * Returns the variable of the literal. * @param lit the literal @@ -71,6 +73,15 @@ hashSatLiteral(const SatLiteral& literal) { return (size_t) minisat::toInt(literal); } +inline std::string stringOfLiteralValue(SatLiteralValue val) { + if( val == minisat::l_False ) { + return "0"; + } else if (val == minisat::l_True ) { + return "1"; + } else { // unknown + return "_"; + } +} #endif /* __CVC4_USE_MINISAT */ /** Interface encapsulating the "input" to the solver, e.g., from the @@ -146,6 +157,8 @@ public: void enqueueTheoryLiteral(const SatLiteral& l); void setCnfStream(CnfStream* cnfStream); + + SatLiteralValue value(SatLiteral l); }; /* Functions that delegate to the concrete SAT solver. */ @@ -185,6 +198,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } +inline SatLiteralValue SatSolver::value(SatLiteral l) { + return d_minisat->modelValue(l); +} + #endif /* __CVC4_USE_MINISAT */ inline size_t @@ -207,6 +224,11 @@ inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { return out; } +inline std::ostream& operator <<(std::ostream& out, const SatLiteralValue& val) { + out << stringOfLiteralValue(val); + return out; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ |