Skip to content

Solver factory: set_decision_procedure_time_limit does not require dynamic_cast #8409

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
Aug 7, 2024
Merged

Solver factory: set_decision_procedure_time_limit does not require dynamic_cast #8409

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
20 changes: 2 additions & 18 deletions src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,26 +82,13 @@ solver_factoryt::solvert::stack_decision_procedure() const
}

void solver_factoryt::set_decision_procedure_time_limit(
decision_proceduret &decision_procedure)
solver_resource_limitst &decision_procedure)
{
const int timeout_seconds =
options.get_signed_int_option("solver-time-limit");

if(timeout_seconds > 0)
{
solver_resource_limitst *solver =
dynamic_cast<solver_resource_limitst *>(&decision_procedure);
if(solver == nullptr)
{
messaget log(message_handler);
log.warning() << "cannot set solver time limit on "
<< decision_procedure.decision_procedure_text()
<< messaget::eom;
return;
}

solver->set_time_limit_seconds(timeout_seconds);
}
decision_procedure.set_time_limit_seconds(timeout_seconds);
}

void solver_factoryt::solvert::set_decision_procedure(
Expand Down Expand Up @@ -531,7 +518,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
if(options.get_bool_option("fpa"))
smt2_dec->use_FPA_theory = true;

set_decision_procedure_time_limit(*smt2_dec);
return std::make_unique<solvert>(std::move(smt2_dec));
}
else if(filename == "-")
Expand All @@ -547,7 +533,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
if(options.get_bool_option("fpa"))
smt2_conv->use_FPA_theory = true;

set_decision_procedure_time_limit(*smt2_conv);
return std::make_unique<solvert>(std::move(smt2_conv));
}
else
Expand All @@ -565,7 +550,6 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver)
if(options.get_bool_option("fpa"))
smt2_conv->use_FPA_theory = true;

set_decision_procedure_time_limit(*smt2_conv);
return std::make_unique<solvert>(std::move(smt2_conv), std::move(out));
}
}
Expand Down
5 changes: 3 additions & 2 deletions src/goto-checker/solver_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ class cmdlinet;
class message_handlert;
class namespacet;
class optionst;
class solver_resource_limitst;
class stack_decision_proceduret;

class solver_factoryt final
Expand Down Expand Up @@ -81,8 +82,8 @@ class solver_factoryt final
/// Sets the timeout of \p decision_procedure if the `solver-time-limit`
/// option has a positive value (in seconds).
/// \note Most solvers silently ignore the time limit at the moment.
void
set_decision_procedure_time_limit(decision_proceduret &decision_procedure);
void set_decision_procedure_time_limit(
solver_resource_limitst &decision_procedure);

// consistency checks during solver creation
void no_beautification();
Expand Down