From 0c750bc714888b58d9337fe2cb6aa10b9fccb4c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 28 Jul 2014 12:19:46 -0700 Subject: [PATCH] update sat solver signature Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 ++-- src/sat/sat_solver.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0e9f50828..9cd6f6add 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -685,8 +685,8 @@ namespace sat { // Search // // ----------------------- - lbool solver::check() { - IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";); + lbool solver::check(unsigned num_lits, literal const* lits) { + IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver using the efficient SAT solver)\n";); SASSERT(scope_lvl() == 0); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index b18bae06a..9cd62a47f 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -250,7 +250,7 @@ namespace sat { // // ----------------------- public: - lbool check(); + lbool check(unsigned num_lits = 0, literal const* lits = 0); model const & get_model() const { return m_model; } model_converter const & get_model_converter() const { return m_mc; }