Skip to content

Solver factory: all solvers are stack_decision_proceduret #8408

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

Solver factory: all solvers are stack_decision_proceduret #8408

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
8 changes: 1 addition & 7 deletions src/goto-checker/goto_symex_property_decider.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,18 +114,12 @@ decision_proceduret::resultt goto_symex_property_decidert::solve()
return solver->decision_procedure()();
}

decision_proceduret &
stack_decision_proceduret &
goto_symex_property_decidert::get_decision_procedure() const
{
return solver->decision_procedure();
}

stack_decision_proceduret &
goto_symex_property_decidert::get_stack_decision_procedure() const
{
return solver->stack_decision_procedure();
}

symex_target_equationt &goto_symex_property_decidert::get_equation() const
{
return equation;
Expand Down
5 changes: 1 addition & 4 deletions src/goto-checker/goto_symex_property_decider.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,7 @@ class goto_symex_property_decidert
decision_proceduret::resultt solve();

/// Returns the solver instance
decision_proceduret &get_decision_procedure() const;

/// Returns the solver instance
stack_decision_proceduret &get_stack_decision_procedure() const;
stack_decision_proceduret &get_decision_procedure() const;

/// Return the equation associated with this instance
symex_target_equationt &get_equation() const;
Expand Down
4 changes: 2 additions & 2 deletions src/goto-checker/multi_path_symex_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider.get_stack_decision_procedure()),
dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),

Check warning on line 116 in src/goto-checker/multi_path_symex_checker.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/multi_path_symex_checker.cpp#L116 

Added line #L116 was not covered by tests
equation);
}

Expand Down Expand Up @@ -161,7 +161,7 @@
options,
ui_message_handler,
equation,
property_decider.get_stack_decision_procedure());
property_decider.get_decision_procedure());

return fault_localizer(property_id);
}
Expand Down
8 changes: 4 additions & 4 deletions src/goto-checker/single_loop_incremental_symex_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@

// Freeze all symbols if we are using a prop_conv_solvert
prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
&property_decider.get_stack_decision_procedure());
&property_decider.get_decision_procedure());
if(prop_conv_solver != nullptr)
prop_conv_solver->set_all_frozen();
}
Expand Down Expand Up @@ -114,7 +114,7 @@
properties);

// We convert the assertions in a new context.
property_decider.get_stack_decision_procedure().push();
property_decider.get_decision_procedure().push();
equation.convert_assertions(
property_decider.get_decision_procedure(), false);
property_decider.convert_goals();
Expand Down Expand Up @@ -154,7 +154,7 @@

// Nothing else to do with the current set of assertions.
// Let's pop them.
property_decider.get_stack_decision_procedure().pop();
property_decider.get_decision_procedure().pop();
}

// Now we are finally done.
Expand Down Expand Up @@ -207,7 +207,7 @@
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider.get_stack_decision_procedure()),
dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),

Check warning on line 210 in src/goto-checker/single_loop_incremental_symex_checker.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/single_loop_incremental_symex_checker.cpp#L210 

Added line #L210 was not covered by tests
equation);
}

Expand Down
2 changes: 1 addition & 1 deletion src/goto-checker/single_path_symex_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider->get_stack_decision_procedure()),
dynamic_cast<boolbvt &>(property_decider->get_decision_procedure()),

Check warning on line 147 in src/goto-checker/single_path_symex_checker.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/single_path_symex_checker.cpp#L147 

Added line #L147 was not covered by tests
property_decider->get_equation());
}

Expand Down
20 changes: 5 additions & 15 deletions src/goto-checker/solver_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,41 +46,31 @@ solver_factoryt::solver_factoryt(
{
}

solver_factoryt::solvert::solvert(std::unique_ptr<decision_proceduret> p)
solver_factoryt::solvert::solvert(std::unique_ptr<stack_decision_proceduret> p)
: decision_procedure_ptr(std::move(p))
{
}

solver_factoryt::solvert::solvert(
std::unique_ptr<decision_proceduret> p1,
std::unique_ptr<stack_decision_proceduret> p1,
std::unique_ptr<propt> p2)
: prop_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
{
}

solver_factoryt::solvert::solvert(
std::unique_ptr<decision_proceduret> p1,
std::unique_ptr<stack_decision_proceduret> p1,
std::unique_ptr<std::ofstream> p2)
: ofstream_ptr(std::move(p2)), decision_procedure_ptr(std::move(p1))
{
}

decision_proceduret &solver_factoryt::solvert::decision_procedure() const
stack_decision_proceduret &solver_factoryt::solvert::decision_procedure() const
{
PRECONDITION(decision_procedure_ptr != nullptr);
return *decision_procedure_ptr;
}

stack_decision_proceduret &
solver_factoryt::solvert::stack_decision_procedure() const
{
PRECONDITION(decision_procedure_ptr != nullptr);
stack_decision_proceduret *solver =
dynamic_cast<stack_decision_proceduret *>(&*decision_procedure_ptr);
INVARIANT(solver != nullptr, "stack decision procedure required");
return *solver;
}

void solver_factoryt::set_decision_procedure_time_limit(
solver_resource_limitst &decision_procedure)
{
Expand All @@ -92,7 +82,7 @@ void solver_factoryt::set_decision_procedure_time_limit(
}

void solver_factoryt::solvert::set_decision_procedure(
std::unique_ptr<decision_proceduret> p)
std::unique_ptr<stack_decision_proceduret> p)
{
decision_procedure_ptr = std::move(p);
}
Expand Down
16 changes: 8 additions & 8 deletions src/goto-checker/solver_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ class message_handlert;
class namespacet;
class optionst;
class solver_resource_limitst;
class stack_decision_proceduret;

class solver_factoryt final
{
Expand All @@ -39,23 +38,24 @@ class solver_factoryt final
class solvert final
{
public:
explicit solvert(std::unique_ptr<decision_proceduret> p);
solvert(std::unique_ptr<decision_proceduret> p1, std::unique_ptr<propt> p2);
explicit solvert(std::unique_ptr<stack_decision_proceduret> p);
solvert(
std::unique_ptr<decision_proceduret> p1,
std::unique_ptr<stack_decision_proceduret> p1,
std::unique_ptr<propt> p2);
solvert(
std::unique_ptr<stack_decision_proceduret> p1,
std::unique_ptr<std::ofstream> p2);

decision_proceduret &decision_procedure() const;
stack_decision_proceduret &stack_decision_procedure() const;
stack_decision_proceduret &decision_procedure() const;

void set_decision_procedure(std::unique_ptr<decision_proceduret> p);
void set_decision_procedure(std::unique_ptr<stack_decision_proceduret> p);
void set_prop(std::unique_ptr<propt> p);
void set_ofstream(std::unique_ptr<std::ofstream> p);

// the objects are deleted in the opposite order they appear below
std::unique_ptr<std::ofstream> ofstream_ptr;
std::unique_ptr<propt> prop_ptr;
std::unique_ptr<decision_proceduret> decision_procedure_ptr;
std::unique_ptr<stack_decision_proceduret> decision_procedure_ptr;
};

/// Returns a solvert object
Expand Down
Loading