mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update sat solver signature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ff64adf292
commit
0c750bc714
|
@ -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()) {
|
||||
|
|
|
@ -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; }
|
||||
|
||||
|
|
Loading…
Reference in a new issue