From 5e857016577615783e307d93bf0ef014423538a2 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 13 Jan 2018 21:16:41 +0000 Subject: [PATCH 1/4] Catch Minisat::OutOfMemoryException --- src/solvers/sat/satcheck_minisat2.cpp | 87 +++++++++++++++++++-------- 1 file changed, 62 insertions(+), 25 deletions(-) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 3f7ecc5c59b..481f51514f6 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -69,8 +69,18 @@ template void satcheck_minisat2_baset::set_polarity(literalt a, bool value) { assert(!a.is_constant()); - add_variables(); - solver->setPolarity(a.var_no(), value); + + try + { + add_variables(); + solver->setPolarity(a.var_no(), value); + } + catch(Minisat::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } const std::string satcheck_minisat_no_simplifiert::solver_text() @@ -93,26 +103,35 @@ void satcheck_minisat2_baset::add_variables() template void satcheck_minisat2_baset::lcnf(const bvt &bv) { - add_variables(); - - forall_literals(it, bv) + try { - if(it->is_true()) - return; - else if(!it->is_false()) - assert(it->var_no()<(unsigned)solver->nVars()); - } + add_variables(); + + forall_literals(it, bv) + { + if(it->is_true()) + return; + else if(!it->is_false()) + assert(it->var_no() < (unsigned)solver->nVars()); + } - Minisat::vec c; + Minisat::vec c; - convert(bv, c); + convert(bv, c); - // Note the underscore. - // Add a clause to the solver without making superflous internal copy. + // Note the underscore. + // Add a clause to the solver without making superflous internal copy. - solver->addClause_(c); + solver->addClause_(c); - clause_counter++; + clause_counter++; + } + catch(Minisat::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } #ifndef _WIN32 @@ -243,13 +262,22 @@ void satcheck_minisat2_baset::set_assignment(literalt a, bool value) { assert(!a.is_constant()); - unsigned v=a.var_no(); - bool sign=a.sign(); + try + { + unsigned v = a.var_no(); + bool sign = a.sign(); - // MiniSat2 kills the model in case of UNSAT - solver->model.growTo(v+1); - value^=sign; - solver->model[v]=Minisat::lbool(value); + // MiniSat2 kills the model in case of UNSAT + solver->model.growTo(v + 1); + value ^= sign; + solver->model[v] = Minisat::lbool(value); + } + catch(Minisat::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } template @@ -307,10 +335,19 @@ satcheck_minisat_simplifiert::satcheck_minisat_simplifiert(): void satcheck_minisat_simplifiert::set_frozen(literalt a) { - if(!a.is_constant()) + try { - add_variables(); - solver->setFrozen(a.var_no(), true); + if(!a.is_constant()) + { + add_variables(); + solver->setFrozen(a.var_no(), true); + } + } + catch(Minisat::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); } } From 89fc48db26465f010b489ed56a05b5b7a9751e18 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 13 Jan 2018 21:26:58 +0000 Subject: [PATCH 2/4] Replace assertions by invariants --- src/solvers/sat/satcheck_minisat2.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 481f51514f6..3f50091bbb6 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -14,12 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#include #include #include #include -#include #include #include @@ -68,7 +66,7 @@ tvt satcheck_minisat2_baset::l_get(literalt a) const template void satcheck_minisat2_baset::set_polarity(literalt a, bool value) { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); try { @@ -112,7 +110,10 @@ void satcheck_minisat2_baset::lcnf(const bvt &bv) if(it->is_true()) return; else if(!it->is_false()) - assert(it->var_no() < (unsigned)solver->nVars()); + { + INVARIANT( + it->var_no() < (unsigned)solver->nVars(), "variable not added yet"); + } } Minisat::vec c; @@ -148,7 +149,7 @@ static void interrupt_solver(int signum) template propt::resultt satcheck_minisat2_baset::prop_solve() { - assert(status!=statust::ERROR); + PRECONDITION(status != statust::ERROR); { messaget::status() << @@ -260,7 +261,7 @@ propt::resultt satcheck_minisat2_baset::prop_solve() template void satcheck_minisat2_baset::set_assignment(literalt a, bool value) { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); try { @@ -353,7 +354,7 @@ void satcheck_minisat_simplifiert::set_frozen(literalt a) bool satcheck_minisat_simplifiert::is_eliminated(literalt a) const { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); return solver->isEliminated(a.var_no()); } From 84e04a71f8d9b82b59a5609bea65ea5ba20a28ef Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 13 Jan 2018 21:41:50 +0000 Subject: [PATCH 3/4] Catch Glucose::OutOfMemoryException --- src/solvers/sat/satcheck_glucose.cpp | 152 +++++++++++++++++---------- 1 file changed, 98 insertions(+), 54 deletions(-) diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp index fa146d09414..7b8fce79cff 100644 --- a/src/solvers/sat/satcheck_glucose.cpp +++ b/src/solvers/sat/satcheck_glucose.cpp @@ -65,8 +65,18 @@ template void satcheck_glucose_baset::set_polarity(literalt a, bool value) { assert(!a.is_constant()); - add_variables(); - solver->setPolarity(a.var_no(), value); + + try + { + add_variables(); + solver->setPolarity(a.var_no(), value); + } + catch(Glucose::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } const std::string satcheck_glucose_no_simplifiert::solver_text() @@ -89,26 +99,35 @@ void satcheck_glucose_baset::add_variables() template void satcheck_glucose_baset::lcnf(const bvt &bv) { - add_variables(); - - forall_literals(it, bv) + try { - if(it->is_true()) - return; - else if(!it->is_false()) - assert(it->var_no()<(unsigned)solver->nVars()); - } + add_variables(); - Glucose::vec c; + forall_literals(it, bv) + { + if(it->is_true()) + return; + else if(!it->is_false()) + assert(it->var_no() < (unsigned)solver->nVars()); + } + + Glucose::vec c; - convert(bv, c); + convert(bv, c); - // Note the underscore. - // Add a clause to the solver without making superflous internal copy. + // Note the underscore. + // Add a clause to the solver without making superflous internal copy. - solver->addClause_(c); + solver->addClause_(c); - clause_counter++; + clause_counter++; + } + catch(Glucose::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } template @@ -123,49 +142,56 @@ propt::resultt satcheck_glucose_baset::prop_solve() solver->nClauses() << " clauses" << eom; } - add_variables(); - - if(!solver->okay()) + try { - messaget::status() << - "SAT checker inconsistent: instance is UNSATISFIABLE" << eom; - } - else - { - // if assumptions contains false, we need this to be UNSAT - bool has_false=false; - - forall_literals(it, assumptions) - if(it->is_false()) - has_false=true; + add_variables(); - if(has_false) + if(!solver->okay()) { - messaget::status() << - "got FALSE as assumption: instance is UNSATISFIABLE" << eom; + messaget::status() + << "SAT checker inconsistent: instance is UNSATISFIABLE" << eom; } else { - Glucose::vec solver_assumptions; - convert(assumptions, solver_assumptions); + // if assumptions contains false, we need this to be UNSAT + bool has_false = false; + + forall_literals(it, assumptions) + if(it->is_false()) + has_false = true; - if(solver->solve(solver_assumptions)) + if(has_false) { - messaget::status() << - "SAT checker: instance is SATISFIABLE" << eom; - status=statust::SAT; - return resultt::P_SATISFIABLE; + messaget::status() + << "got FALSE as assumption: instance is UNSATISFIABLE" << eom; } else { - messaget::status() << - "SAT checker: instance is UNSATISFIABLE" << eom; + Glucose::vec solver_assumptions; + convert(assumptions, solver_assumptions); + + if(solver->solve(solver_assumptions)) + { + messaget::status() << "SAT checker: instance is SATISFIABLE" << eom; + status = statust::SAT; + return resultt::P_SATISFIABLE; + } + else + { + messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom; + } } } - } - status=statust::UNSAT; - return resultt::P_UNSATISFIABLE; + status = statust::UNSAT; + return resultt::P_UNSATISFIABLE; + } + catch(Glucose::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } template @@ -173,13 +199,22 @@ void satcheck_glucose_baset::set_assignment(literalt a, bool value) { assert(!a.is_constant()); - unsigned v=a.var_no(); - bool sign=a.sign(); + try + { + unsigned v = a.var_no(); + bool sign = a.sign(); - // MiniSat2 kills the model in case of UNSAT - solver->model.growTo(v+1); - value^=sign; - solver->model[v]=Glucose::lbool(value); + // MiniSat2 kills the model in case of UNSAT + solver->model.growTo(v + 1); + value ^= sign; + solver->model[v] = Glucose::lbool(value); + } + catch(Glucose::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); + } } template @@ -233,10 +268,19 @@ satcheck_glucose_simplifiert::satcheck_glucose_simplifiert(): void satcheck_glucose_simplifiert::set_frozen(literalt a) { - if(!a.is_constant()) + try { - add_variables(); - solver->setFrozen(a.var_no(), true); + if(!a.is_constant()) + { + add_variables(); + solver->setFrozen(a.var_no(), true); + } + } + catch(Glucose::OutOfMemoryException) + { + messaget::error() << "SAT checker ran out of memory" << eom; + status = statust::ERROR; + throw std::bad_alloc(); } } From ef45a1d9b1c2f0dc24ed38429dad1639b0fe6db3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 13 Jan 2018 21:44:44 +0000 Subject: [PATCH 4/4] Replace assertions by invariants --- src/solvers/sat/satcheck_glucose.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp index 7b8fce79cff..3de729ae0a0 100644 --- a/src/solvers/sat/satcheck_glucose.cpp +++ b/src/solvers/sat/satcheck_glucose.cpp @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#include #include +#include #include #include @@ -64,7 +64,7 @@ tvt satcheck_glucose_baset::l_get(literalt a) const template void satcheck_glucose_baset::set_polarity(literalt a, bool value) { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); try { @@ -108,7 +108,8 @@ void satcheck_glucose_baset::lcnf(const bvt &bv) if(it->is_true()) return; else if(!it->is_false()) - assert(it->var_no() < (unsigned)solver->nVars()); + INVARIANT( + it->var_no() < (unsigned)solver->nVars(), "variable not added yet"); } Glucose::vec c; @@ -133,7 +134,7 @@ void satcheck_glucose_baset::lcnf(const bvt &bv) template propt::resultt satcheck_glucose_baset::prop_solve() { - assert(status!=statust::ERROR); + PRECONDITION(status != statust::ERROR); // We start counting at 1, thus there is one variable fewer. { @@ -197,7 +198,7 @@ propt::resultt satcheck_glucose_baset::prop_solve() template void satcheck_glucose_baset::set_assignment(literalt a, bool value) { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); try { @@ -253,7 +254,7 @@ void satcheck_glucose_baset::set_assumptions(const bvt &bv) assumptions=bv; forall_literals(it, assumptions) - assert(!it->is_constant()); + INVARIANT(!it->is_constant(), "assumption literals must not be constant"); } satcheck_glucose_no_simplifiert::satcheck_glucose_no_simplifiert(): @@ -286,7 +287,7 @@ void satcheck_glucose_simplifiert::set_frozen(literalt a) bool satcheck_glucose_simplifiert::is_eliminated(literalt a) const { - assert(!a.is_constant()); + PRECONDITION(!a.is_constant()); return solver->isEliminated(a.var_no()); }