diff options
| author | lianah <lianahady@gmail.com> | 2013-04-08 15:31:08 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
| commit | 51d7754cce64a2688e6da536710704c62e61ca1d (patch) | |
| tree | 71874d6de1c2056732edbb8f2332e738274a8a1e /src/prop/minisat/core | |
| parent | 2f4162877ad455c8c80f60a9bedf0b779b44ecaa (diff) | |
added support for dumping the SAT problem the sat solver is working on
Diffstat (limited to 'src/prop/minisat/core')
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 9338f9b55..55780479a 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -173,6 +173,7 @@ public: bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state + void toDimacs (); void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec<Lit>& assumps); void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max); @@ -539,12 +540,14 @@ inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); as inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } +inline void Solver::toDimacs () { vec<Lit> as; toDimacs(stdout, as); } inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } + //================================================================================================= // Debug etc: |