Skip to content

Stop propt inheriting from messaget [blocks: #3800] #3249

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
Feb 1, 2019
Merged

Stop propt inheriting from messaget [blocks: #3800] #3249

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
19 changes: 7 additions & 12 deletions src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,15 +149,14 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
!options.get_bool_option("sat-preprocessor")) // no simplifier
{
// simplifier won't work with beautification
solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
solver->set_prop(
util_make_unique<satcheck_no_simplifiert>(message_handler));
}
else // with simplifier
{
solver->set_prop(util_make_unique<satcheckt>());
solver->set_prop(util_make_unique<satcheckt>(message_handler));
}

solver->prop().set_message_handler(message_handler);

auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());

if(options.get_option("arrays-uf") == "never")
Expand All @@ -176,8 +175,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
no_beautification();
no_incremental_check();

auto prop = util_make_unique<dimacs_cnft>();
prop->set_message_handler(message_handler);
auto prop = util_make_unique<dimacs_cnft>(message_handler);

std::string filename = options.get_option("outfile");

Expand All @@ -192,13 +190,11 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
if(options.get_bool_option("sat-preprocessor"))
{
no_beautification();
return util_make_unique<satcheckt>();
return util_make_unique<satcheckt>(message_handler);
}
return util_make_unique<satcheck_no_simplifiert>();
return util_make_unique<satcheck_no_simplifiert>(message_handler);
}();

prop->set_message_handler(message_handler);

bv_refinementt::infot info;
info.ns = &ns;
info.prop = prop.get();
Expand All @@ -225,8 +221,7 @@ solver_factoryt::get_string_refinement()
{
string_refinementt::infot info;
info.ns = &ns;
auto prop = util_make_unique<satcheck_no_simplifiert>();
prop->set_message_handler(message_handler);
auto prop = util_make_unique<satcheck_no_simplifiert>(message_handler);
info.prop = prop.get();
info.refinement_bound = DEFAULT_MAX_NB_REFINEMENT;
info.output_xml = output_xml_in_refinement;
Expand Down
14 changes: 7 additions & 7 deletions src/solvers/flattening/arrays.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ literalt arrayst::record_array_equality(
// check types
if(!base_type_eq(op0.type(), op1.type(), ns))
{
prop.error() << equality.pretty() << messaget::eom;
error() << equality.pretty() << messaget::eom;
DATA_INVARIANT(
false,
"record_array_equality got equality without matching types");
Expand Down Expand Up @@ -116,7 +116,7 @@ void arrayst::collect_arrays(const exprt &a)
// check types
if(!base_type_eq(array_type, with_expr.old().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
error() << a.pretty() << messaget::eom;
DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
}

Expand All @@ -134,7 +134,7 @@ void arrayst::collect_arrays(const exprt &a)
// check types
if(!base_type_eq(array_type, update_expr.old().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
error() << a.pretty() << messaget::eom;
DATA_INVARIANT(
false,
"collect_arrays got 'update' without matching types");
Expand All @@ -156,14 +156,14 @@ void arrayst::collect_arrays(const exprt &a)
// check types
if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
error() << a.pretty() << messaget::eom;
DATA_INVARIANT(false, "collect_arrays got if without matching types");
}

// check types
if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
{
prop.error() << a.pretty() << messaget::eom;
error() << a.pretty() << messaget::eom;
DATA_INVARIANT(false, "collect_arrays got if without matching types");
}

Expand Down Expand Up @@ -511,7 +511,7 @@ void arrayst::add_array_constraints_with(

if(index_expr.type()!=value.type())
{
prop.error() << expr.pretty() << messaget::eom;
error() << expr.pretty() << messaget::eom;
DATA_INVARIANT(
false,
"with-expression operand should match array element type");
Expand Down Expand Up @@ -580,7 +580,7 @@ void arrayst::add_array_constraints_update(

if(index_expr.type()!=value.type())
{
prop.error() << expr.pretty() << messaget::eom;
prop.message.error() << expr.pretty() << messaget::eom;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change (inside a #if 0 block) looks suspicious: I believe this should be just error().

DATA_INVARIANT(
false,
"update operand should match array element type");
Expand Down
7 changes: 5 additions & 2 deletions src/solvers/prop/prop.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,11 @@ Author: Daniel Kroening, [email protected]

/*! \brief TO_BE_DOCUMENTED
*/
class propt:public messaget
class propt
{
public:
propt() { }
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, don't you need to consume a message_handlert here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wasn't there before so adding one instead of constructing a new one could potentially change the behavior.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it makes things safer, so I'd happily take that change.


virtual ~propt() { }

// boolean operators
Expand Down Expand Up @@ -113,12 +114,14 @@ class propt:public messaget
// Resource limits:
virtual void set_time_limit_seconds(uint32_t)
{
warning() << "CPU limit ignored (not implemented)" << eom;
log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
}

protected:
// to avoid a temporary for lcnf(...)
bvt lcnf_bv;

messaget log;
};

#endif // CPROVER_SOLVERS_PROP_PROP_H
12 changes: 5 additions & 7 deletions src/solvers/qbf/qbf_quantor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,10 +34,8 @@ const std::string qbf_quantort::solver_text()
propt::resultt qbf_quantort::prop_solve()
{
{
messaget::status() <<
"Quantor: " <<
no_variables() << " variables, " <<
no_clauses() << " clauses" << eom;
log.status() << "Quantor: " << no_variables() << " variables, "
<< no_clauses() << " clauses" << messaget::eom;
}

std::string qbf_tmp_file="quantor.qdimacs";
Expand Down Expand Up @@ -87,19 +85,19 @@ propt::resultt qbf_quantort::prop_solve()

if(!result_found)
{
messaget::error() << "Quantor failed: unknown result" << eom;
log.error() << "Quantor failed: unknown result" << messaget::eom;
return resultt::P_ERROR;
}
}

if(result)
{
messaget::status() << "Quantor: TRUE" << eom;
log.status() << "Quantor: TRUE" << messaget::eom;
return resultt::P_SATISFIABLE;
}
else
{
messaget::status() << "Quantor: FALSE" << eom;
log.status() << "Quantor: FALSE" << messaget::eom;
return resultt::P_UNSATISFIABLE;
}

Expand Down
12 changes: 5 additions & 7 deletions src/solvers/qbf/qbf_qube.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,8 @@ propt::resultt qbf_qubet::prop_solve()
return resultt::P_SATISFIABLE;

{
messaget::status() <<
"QuBE: " <<
no_variables() << " variables, " <<
no_clauses() << " clauses" << eom;
log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
<< " clauses" << messaget::eom;
}

std::string qbf_tmp_file="qube.qdimacs";
Expand Down Expand Up @@ -95,19 +93,19 @@ propt::resultt qbf_qubet::prop_solve()

if(!result_found)
{
messaget::error() << "QuBE failed: unknown result" << eom;
log.error() << "QuBE failed: unknown result" << messaget::eom;
return resultt::P_ERROR;
}
}

if(result)
{
messaget::status() << "QuBE: TRUE" << eom;
log.status() << "QuBE: TRUE" << messaget::eom;
return resultt::P_SATISFIABLE;
}
else
{
messaget::status() << "QuBE: FALSE" << eom;
log.status() << "QuBE: FALSE" << messaget::eom;
return resultt::P_UNSATISFIABLE;
}

Expand Down
15 changes: 7 additions & 8 deletions src/solvers/qbf/qbf_qube_core.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,8 @@ propt::resultt qbf_qube_coret::prop_solve()
return resultt::P_SATISFIABLE;

{
messaget::status() << "QuBE: "
<< no_variables() << " variables, "
<< no_clauses() << " clauses" << eom;
log.status() << "QuBE: " << no_variables() << " variables, " << no_clauses()
<< " clauses" << messaget::eom;
}

std::string result_tmp_file="qube.out";
Expand Down Expand Up @@ -98,33 +97,33 @@ propt::resultt qbf_qube_coret::prop_solve()

if(!result_found)
{
messaget::error() << "QuBE failed: unknown result" << eom;
log.error() << "QuBE failed: unknown result" << messaget::eom;
return resultt::P_ERROR;
}
}

int remove_result=remove(result_tmp_file.c_str());
if(remove_result!=0)
{
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
return resultt::P_ERROR;
}

remove_result=remove(qbf_tmp_file.c_str());
if(remove_result!=0)
{
messaget::error() << "Remove failed: " << std::strerror(errno) << eom;
log.error() << "Remove failed: " << std::strerror(errno) << messaget::eom;
return resultt::P_ERROR;
}

if(result)
{
messaget::status() << "QuBE: TRUE" << eom;
log.status() << "QuBE: TRUE" << messaget::eom;
return resultt::P_SATISFIABLE;
}
else
{
messaget::status() << "QuBE: FALSE" << eom;
log.status() << "QuBE: FALSE" << messaget::eom;
return resultt::P_UNSATISFIABLE;
}
}
Expand Down
12 changes: 5 additions & 7 deletions src/solvers/qbf/qbf_skizzo.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,8 @@ propt::resultt qbf_skizzot::prop_solve()
return resultt::P_SATISFIABLE;

{
messaget::status() <<
"Skizzo: " <<
no_variables() << " variables, " <<
no_clauses() << " clauses" << eom;
log.status() << "Skizzo: " << no_variables() << " variables, "
<< no_clauses() << " clauses" << messaget::eom;
}

std::string qbf_tmp_file="sKizzo.qdimacs";
Expand Down Expand Up @@ -95,19 +93,19 @@ propt::resultt qbf_skizzot::prop_solve()

if(!result_found)
{
messaget::error() << "Skizzo failed: unknown result" << eom;
log.error() << "Skizzo failed: unknown result" << messaget::eom;
return resultt::P_ERROR;
}
}

if(result)
{
messaget::status() << "Skizzo: TRUE" << eom;
log.status() << "Skizzo: TRUE" << messaget::eom;
return resultt::P_SATISFIABLE;
}
else
{
messaget::status() << "Skizzo: FALSE" << eom;
log.status() << "Skizzo: FALSE" << messaget::eom;
return resultt::P_UNSATISFIABLE;
}

Expand Down
5 changes: 5 additions & 0 deletions src/solvers/sat/dimacs_cnf.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,11 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
{
}

dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
{
log.set_message_handler(message_handler);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is going to be a bit painful, but let's please try to use the constructor all the way, i.e., it would be dimacs_cnft(message_handler) above.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That sounds like a good idea but this would go a bit beyond scope of a refactoring PR, and my initial statement "No functional changes." wouldn't be strictly true anymore.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, if we have no bugs (surely true) then it wouldn't entail any functional changes, because each time we construct a dimacs_cnft we surely also initialized its message handler.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It we leave it initialized, doesn't it just means that some messages wouldn't get printed? This would be difficult to detect. It's also a bit difficult to manually check, as a lot of classes inherit from dimacs_cnft...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think any introduced functional change is a strict improvement here. Any class deriving should be forced to call a constructor that takes a message handler.

}

void dimacs_cnft::set_assignment(literalt, bool)
{
UNIMPLEMENTED;
Expand Down
1 change: 1 addition & 0 deletions src/solvers/sat/dimacs_cnf.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ class dimacs_cnft:public cnf_clause_listt
{
public:
dimacs_cnft();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove this constructor.

explicit dimacs_cnft(message_handlert &);
virtual ~dimacs_cnft() { }

virtual void write_dimacs_cnf(std::ostream &out);
Expand Down
17 changes: 9 additions & 8 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 @@ -128,7 +128,7 @@ bool pbs_dimacs_cnft::pbs_solve()

if(file.fail())
{
error() << "Unable to read SAT results!" << eom;
log.error() << "Unable to read SAT results!" << messaget::eom;
return false;
}

Expand Down Expand Up @@ -194,7 +194,8 @@ bool pbs_dimacs_cnft::pbs_solve()
#endif
if(strstr(line.c_str(), "time out") != nullptr)
{
status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." << eom;
log.status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT."
<< messaget::eom;
return satisfied;
}
sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
Expand All @@ -218,21 +219,21 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
pbfile.close();

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

const bool result = pbs_solve();

if(!result)
{
messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom;
log.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
}
else
{
messaget::status() << "PBS checker: system is SATISFIABLE";
log.status() << "PBS checker: system is SATISFIABLE";
if(optimize)
messaget::status() << " (distance " << opt_sum << ")";
messaget::status() << eom;
log.status() << " (distance " << opt_sum << ")";
log.status() << messaget::eom;
}

if(result)
Expand Down
Loading