Skip to content

Catch Minisat/Glucose OutOfMemoryException #1732

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jan 15, 2018
Merged

Catch Minisat/Glucose OutOfMemoryException #1732

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
5e85701
Catch Minisat::OutOfMemoryException
peterschrammel Jan 13, 2018
89fc48d
Replace assertions by invariants
peterschrammel Jan 13, 2018
84e04a7
Catch Glucose::OutOfMemoryException
peterschrammel Jan 13, 2018
ef45a1d
Replace assertions by invariants
peterschrammel Jan 13, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
165 changes: 105 additions & 60 deletions src/solvers/sat/satcheck_glucose.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
#include <inttypes.h>
#endif

#include <cassert>
#include <stack>

#include <util/invariant.h>
#include <util/threeval.h>

#include <core/Solver.h>
Expand Down Expand Up @@ -64,9 +64,19 @@ tvt satcheck_glucose_baset<T>::l_get(literalt a) const
template<typename T>
void satcheck_glucose_baset<T>::set_polarity(literalt a, bool value)
{
assert(!a.is_constant());
add_variables();
solver->setPolarity(a.var_no(), value);
PRECONDITION(!a.is_constant());

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()
Expand All @@ -89,32 +99,42 @@ void satcheck_glucose_baset<T>::add_variables()
template<typename T>
void satcheck_glucose_baset<T>::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<Glucose::Lit> c;
forall_literals(it, bv)
{
if(it->is_true())
return;
else if(!it->is_false())
INVARIANT(
it->var_no() < (unsigned)solver->nVars(), "variable not added yet");
}

Glucose::vec<Glucose::Lit> 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<typename T>
propt::resultt satcheck_glucose_baset<T>::prop_solve()
{
assert(status!=statust::ERROR);
PRECONDITION(status != statust::ERROR);

// We start counting at 1, thus there is one variable fewer.
{
Expand All @@ -123,63 +143,79 @@ propt::resultt satcheck_glucose_baset<T>::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<Glucose::Lit> 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<Glucose::Lit> 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<typename T>
void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
{
assert(!a.is_constant());
PRECONDITION(!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<typename T>
Expand Down Expand Up @@ -218,7 +254,7 @@ void satcheck_glucose_baset<T>::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():
Expand All @@ -233,16 +269,25 @@ 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();
}
}

bool satcheck_glucose_simplifiert::is_eliminated(literalt a) const
{
assert(!a.is_constant());
PRECONDITION(!a.is_constant());

return solver->isEliminated(a.var_no());
}
Loading