replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4400 from peterschrammel/satcheck-messaget 

Satcheck doesn't inherit from messaget anymore
This commit is contained in:
Peter Schrammel 2019-03-19 17:57:44 +00:00 committed by GitHub
parent 6533631183 f2c1da9c3e
commit 92a94019fd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 49 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/solvers/sat/satcheck_booleforce.cpp
View File

@ -103,7 +103,7 @@ propt::resultt satcheck_booleforce_baset::do_prop_solve()
break;
}
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
}
if(result==BOOLEFORCE_UNSATISFIABLE)

17
src/solvers/sat/satcheck_cadical.cpp
View File

@ -69,28 +69,29 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
{
INVARIANT(status != statust::ERROR, "there cannot be an error");
messaget::statistics() << (no_variables() - 1) << " variables, "
<< clause_counter << " clauses" << eom;
log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
<< " clauses" << messaget::eom;
if(status == statust::UNSAT)
{
messaget::status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
<< eom;
log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
switch(solver->solve())
{
case 10:
messaget::status() << "SAT checker: instance is SATISFIABLE" << eom;
log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
status = statust::SAT;
return resultt::P_SATISFIABLE;
case 20:
messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom;
log.status() << "SAT checker: instance is UNSATISFIABLE"
<< messaget::eom;
break;
default:
messaget::status() << "SAT checker: solving returned without solution"
<< eom;
log.status() << "SAT checker: solving returned without solution"
<< messaget::eom;
throw analysis_exceptiont(
"solving inside CaDiCaL SAT solver has been interrupted");
}

28
src/solvers/sat/satcheck_glucose.cpp
View File

@ -73,7 +73,7 @@ void satcheck_glucose_baset<T>::set_polarity(literalt a, bool value)
}
catch(Glucose::OutOfMemoryException)
{
messaget::error() << "SAT checker ran out of memory" << eom;
log.error() << "SAT checker ran out of memory" << messaget::eom;
status = statust::ERROR;
throw std::bad_alloc();
}
@ -125,7 +125,7 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
}
catch(Glucose::OutOfMemoryException)
{
messaget::error() << "SAT checker ran out of memory" << eom;
log.error() << "SAT checker ran out of memory" << messaget::eom;
status = statust::ERROR;
throw std::bad_alloc();
}
@ -137,8 +137,8 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
PRECONDITION(status != statust::ERROR);
// We start counting at 1, thus there is one variable fewer.
messaget::statistics() << (no_variables() - 1) << " variables, "
<< solver->nClauses() << " clauses" << eom;
log.statistics() << (no_variables() - 1) << " variables, "
<< solver->nClauses() << " clauses" << messaget::eom;
try
{
@ -146,8 +146,8 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
if(!solver->okay())
{
messaget::status()
<< "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
@ -160,8 +160,8 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
if(has_false)
{
messaget::status()
<< "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
@ -170,13 +170,15 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
if(solver->solve(solver_assumptions))
{
messaget::status() << "SAT checker: instance is SATISFIABLE" << eom;
log.status() << "SAT checker: instance is SATISFIABLE"
<< messaget::eom;
status = statust::SAT;
return resultt::P_SATISFIABLE;
}
else
{
messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom;
log.status() << "SAT checker: instance is UNSATISFIABLE"
<< messaget::eom;
}
}
}
@ -186,7 +188,7 @@ propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
}
catch(Glucose::OutOfMemoryException)
{
messaget::error() << "SAT checker ran out of memory" << eom;
log.error() << "SAT checker ran out of memory" << messaget::eom;
status = statust::ERROR;
throw std::bad_alloc();
}
@ -209,7 +211,7 @@ void satcheck_glucose_baset<T>::set_assignment(literalt a, bool value)
}
catch(Glucose::OutOfMemoryException)
{
messaget::error() << "SAT checker ran out of memory" << eom;
log.error() << "SAT checker ran out of memory" << messaget::eom;
status = statust::ERROR;
throw std::bad_alloc();
}
@ -284,7 +286,7 @@ void satcheck_glucose_simplifiert::set_frozen(literalt a)
}
catch(Glucose::OutOfMemoryException)
{
messaget::error() << "SAT checker ran out of memory" << eom;
log.error() << "SAT checker ran out of memory" << messaget::eom;
status = statust::ERROR;
throw std::bad_alloc();
}

23
src/solvers/sat/satcheck_ipasir.cpp
View File

@ -97,15 +97,15 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
{
INVARIANT(status!=statust::ERROR, "there cannot be an error");
messaget::statistics() << (no_variables() - 1) << " variables, "
<< clause_counter << " clauses" << eom;
log.statistics() << (no_variables() - 1) << " variables, " << clause_counter
<< " clauses" << messaget::eom;
// use the internal representation, as ipasir does not support reporting the
// status
if(status==statust::UNSAT)
{
messaget::status() <<
"SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
log.status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
@ -116,8 +116,8 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
if(has_false)
{
messaget::status() <<
"got FALSE as assumption: instance is UNSATISFIABLE" << eom;
log.status() << "got FALSE as assumption: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
@ -129,20 +129,19 @@ propt::resultt satcheck_ipasirt::do_prop_solve()
int solver_state=ipasir_solve(solver);
if(10==solver_state)
{
messaget::status() <<
"SAT checker: instance is SATISFIABLE" << eom;
log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
status=statust::SAT;
return resultt::P_SATISFIABLE;
}
else if(20==solver_state)
{
messaget::status() <<
"SAT checker: instance is UNSATISFIABLE" << eom;
log.status() << "SAT checker: instance is UNSATISFIABLE"
<< messaget::eom;
}
else
{
messaget::status() <<
"SAT checker: solving returned without solution" << eom;
log.status() << "SAT checker: solving returned without solution"
<< messaget::eom;
throw analysis_exceptiont(
"solving inside IPASIR SAT solver has been interrupted");
}

6
src/solvers/sat/satcheck_lingeling.cpp
View File

@ -72,7 +72,7 @@ propt::resultt satcheck_lingelingt::do_prop_solve()
std::string msg=
std::to_string(no_variables()-1)+" variables, "+
std::to_string(clause_counter)+" clauses";
messaget::statistics() << msg << messaget::eom;
log.statistics() << msg << messaget::eom;
}
std::string msg;
@ -86,7 +86,7 @@ propt::resultt satcheck_lingelingt::do_prop_solve()
if(res==10)
{
msg="SAT checker: instance is SATISFIABLE";
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
status=SAT;
return P_SATISFIABLE;
}
@ -94,7 +94,7 @@ propt::resultt satcheck_lingelingt::do_prop_solve()
{
INVARIANT(res == 20, "result value is either 10 or 20");
msg="SAT checker: instance is UNSATISFIABLE";
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
}
status=UNSAT;

8
src/solvers/sat/satcheck_minisat.cpp
View File

@ -154,8 +154,8 @@ propt::resultt satcheck_minisat1_baset::do_prop_solve()
{
PRECONDITION(status != ERROR);
messaget::statistics() << (_no_variables - 1) << " variables, "
<< solver->nClauses() << " clauses" << messaget::eom;
log.statistics() << (_no_variables - 1) << " variables, "
<< solver->nClauses() << " clauses" << messaget::eom;
add_variables();
@ -179,7 +179,7 @@ propt::resultt satcheck_minisat1_baset::do_prop_solve()
if(solver->solve(MiniSat_assumptions))
{
msg="SAT checker: instance is SATISFIABLE";
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
status=SAT;
return P_SATISFIABLE;
}
@ -187,7 +187,7 @@ propt::resultt satcheck_minisat1_baset::do_prop_solve()
msg="SAT checker: instance is UNSATISFIABLE";
}
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
status=UNSAT;
return P_UNSATISFIABLE;
}

6
src/solvers/sat/satcheck_picosat.cpp
View File

@ -73,7 +73,7 @@ propt::resultt satcheck_picosatt::do_prop_solve()
std::string msg=
std::to_string(_no_variables-1)+" variables, "+
std::to_string(picosat_added_original_clauses(picosat))+" clauses";
messaget::statistics() << msg << messaget::eom;
log.statistics() << msg << messaget::eom;
}
std::string msg;
@ -85,7 +85,7 @@ propt::resultt satcheck_picosatt::do_prop_solve()
if(res==PICOSAT_SATISFIABLE)
{
msg="SAT checker: instance is SATISFIABLE";
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
status=SAT;
return P_SATISFIABLE;
}
@ -95,7 +95,7 @@ propt::resultt satcheck_picosatt::do_prop_solve()
res == PICOSAT_UNSATISFIABLE,
"picosat result should report either sat or unsat");
msg="SAT checker: instance is UNSATISFIABLE";
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
}
status=UNSAT;

4
src/solvers/sat/satcheck_zchaff.cpp
View File

@ -81,7 +81,7 @@ propt::resultt satcheck_zchaff_baset::do_prop_solve()
std::string msg=
std::to_string(solver->num_variables())+" variables, "+
std::to_string(solver->clauses().size())+" clauses";
messaget::statistics() << msg << messaget::eom;
log.statistics() << msg << messaget::eom;
}
SAT_StatusT result=(SAT_StatusT)solver->solve();
@ -120,7 +120,7 @@ propt::resultt satcheck_zchaff_baset::do_prop_solve()
break;
}
messaget::status() << msg << messaget::eom;
log.status() << msg << messaget::eom;
}
if(result==SATISFIABLE)

2
src/solvers/sat/satcheck_zcore.cpp
View File

@ -41,7 +41,7 @@ propt::resultt satcheck_zcoret::do_prop_solve()
std::string msg=
std::to_string(no_variables()-1)+" variables, "+
std::to_string(no_clauses())+" clauses";
messaget::statistics() << msg << messaget::eom;
log.statistics() << msg << messaget::eom;
}
// get the core