From: lianah 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& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec& assumps); void toDimacs (FILE* f, Clause& c, vec& map, Var& max); @@ -539,12 +540,14 @@ inline bool Solver::solve (const vec& assumps){ budgetOff(); as inline lbool Solver::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } +inline void Solver::toDimacs () { vec as; toDimacs(stdout, as); } inline void Solver::toDimacs (const char* file){ vec as; toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p){ vec as; as.push(p); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec as; as.push(p); as.push(q); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec 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 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