Skip to content

increase verbosity level of CNF statistics #3749

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 1 commit into from
Jan 10, 2019
Merged

increase verbosity level of CNF statistics #3749

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions src/solvers/sat/pbs_dimacs_cnf.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -218,8 +218,8 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
pbfile.close();

// We start counting at 1, thus there is one variable fewer.
messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
<< " clauses" << eom;
messaget::statistics() << (no_variables() - 1) << " variables, "
<< clauses.size() << " clauses" << eom;

const bool result = pbs_solve();

Expand Down
4 changes: 2 additions & 2 deletions src/solvers/sat/satcheck_cadical.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,8 +69,8 @@ propt::resultt satcheck_cadicalt::prop_solve()
{
INVARIANT(status != statust::ERROR, "there cannot be an error");

messaget::status() << (no_variables() - 1) << " variables, " << clause_counter
<< " clauses" << eom;
messaget::statistics() << (no_variables() - 1) << " variables, "
<< clause_counter << " clauses" << eom;

if(status == statust::UNSAT)
{
Expand Down
7 changes: 2 additions & 5 deletions src/solvers/sat/satcheck_glucose.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,11 +137,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
PRECONDITION(status != statust::ERROR);

// We start counting at 1, thus there is one variable fewer.
{
messaget::status() <<
(no_variables()-1) << " variables, " <<
solver->nClauses() << " clauses" << eom;
}
messaget::statistics() << (no_variables() - 1) << " variables, "
<< solver->nClauses() << " clauses" << eom;

try
{
Expand Down
7 changes: 2 additions & 5 deletions src/solvers/sat/satcheck_ipasir.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,11 +97,8 @@ propt::resultt satcheck_ipasirt::prop_solve()
{
INVARIANT(status!=statust::ERROR, "there cannot be an error");

{
messaget::status() <<
(no_variables()-1) << " variables, " <<
clause_counter << " clauses" << eom;
}
messaget::statistics() << (no_variables() - 1) << " variables, "
<< clause_counter << " clauses" << eom;

// use the internal representation, as ipasir does not support reporting the
// status
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sat/satcheck_lingeling.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ propt::resultt satcheck_lingelingt::prop_solve()
std::string msg=
std::to_string(no_variables()-1)+" variables, "+
std::to_string(clause_counter)+" clauses";
messaget::status() << msg << messaget::eom;
messaget::statistics() << msg << messaget::eom;
}

std::string msg;
Expand Down
7 changes: 2 additions & 5 deletions src/solvers/sat/satcheck_minisat.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,11 +154,8 @@ propt::resultt satcheck_minisat1_baset::prop_solve()
{
PRECONDITION(status != ERROR);

{
messaget::status() <<
(_no_variables-1) << " variables, " <<
solver->nClauses() << " clauses" << messaget::eom;
}
messaget::statistics() << (_no_variables - 1) << " variables, "
<< solver->nClauses() << " clauses" << messaget::eom;

add_variables();

Expand Down
7 changes: 2 additions & 5 deletions src/solvers/sat/satcheck_minisat2.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,11 +167,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
{
PRECONDITION(status != statust::ERROR);

{
messaget::status() <<
(no_variables()-1) << " variables, " <<
solver->nClauses() << " clauses" << eom;
}
messaget::statistics() << (no_variables() - 1) << " variables, "
<< solver->nClauses() << " clauses" << eom;

try
{
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sat/satcheck_picosat.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ propt::resultt satcheck_picosatt::prop_solve()
std::string msg=
std::to_string(_no_variables-1)+" variables, "+
std::to_string(picosat_added_original_clauses(picosat))+" clauses";
messaget::status() << msg << messaget::eom;
messaget::statistics() << msg << messaget::eom;
}

std::string msg;
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sat/satcheck_zchaff.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ propt::resultt satcheck_zchaff_baset::prop_solve()
std::string msg=
std::to_string(solver->num_variables())+" variables, "+
std::to_string(solver->clauses().size())+" clauses";
messaget::status() << msg << messaget::eom;
messaget::statistics() << msg << messaget::eom;
}

SAT_StatusT result=(SAT_StatusT)solver->solve();
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/sat/satcheck_zcore.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ propt::resultt satcheck_zcoret::prop_solve()
std::string msg=
std::to_string(no_variables()-1)+" variables, "+
std::to_string(no_clauses())+" clauses";
messaget::status() << msg << messaget::eom;
messaget::statistics() << msg << messaget::eom;
}

// get the core
Expand Down