From: lianah <lianahady@gmail.com>
Date: Mon, 8 Apr 2013 19:31:08 +0000 (-0400)
Subject: added support for dumping the SAT problem the sat solver is working on
X-Git-Tag: cvc5-1.0.0~7305
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51d7754cce64a2688e6da536710704c62e61ca1d;p=cvc5.git

added support for dumping the SAT problem the sat solver is working on
---

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:
 
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;
diff --git a/src/prop/options b/src/prop/options
index cda99538c..e3a0f814a 100644
--- a/src/prop/options
+++ b/src/prop/options
@@ -28,4 +28,7 @@ option sat_refine_conflicts --refine-conflicts bool
 option minisatUseElim --minisat-elimination bool :default true :read-write 
  use Minisat elimination
 
+option minisatDumpDimacs --minisat-dump-dimacs bool :default false
+ instead of solving minisat dumps the asserted clauses in Dimacs format
+ 
 endmodule