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/simp | |
| parent | 2f4162877ad455c8c80f60a9bedf0b779b44ecaa (diff) | |
added support for dumping the SAT problem the sat solver is working on
Diffstat (limited to 'src/prop/minisat/simp')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 9c3e59954..0e0e5d3ae 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -113,6 +113,10 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + if (options::minisatDumpDimacs()) { + toDimacs(); + return l_Undef; + } popTrail(); vec<Var> extra_frozen; |