Skip to content

Commit

Permalink
Remove dynamic_cast from counterexample beautification code path
Browse files Browse the repository at this point in the history
We know at solver-construction time whether we have one deriving from
boolbvt.
  • Loading branch information
tautschnig committed Aug 21, 2024
1 parent 89a0470 commit ede4a3a
Show file tree
Hide file tree
Showing 7 changed files with 45 additions and 35 deletions.
5 changes: 5 additions & 0 deletions src/goto-checker/goto_symex_property_decider.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,11 @@ goto_symex_property_decidert::get_decision_procedure() const
return solver->decision_procedure();
}

boolbvt &goto_symex_property_decidert::get_boolbv_decision_procedure() const

Check warning on line 123 in src/goto-checker/goto_symex_property_decider.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/goto_symex_property_decider.cpp#L123

Added line #L123 was not covered by tests
{
return solver->boolbv_decision_procedure();

Check warning on line 125 in src/goto-checker/goto_symex_property_decider.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/goto_symex_property_decider.cpp#L125

Added line #L125 was not covered by tests
}

symex_target_equationt &goto_symex_property_decidert::get_equation() const
{
return equation;
Expand Down
3 changes: 3 additions & 0 deletions src/goto-checker/goto_symex_property_decider.h
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,9 @@ class goto_symex_property_decidert
/// Returns the solver instance
stack_decision_proceduret &get_decision_procedure() const;

/// Returns the solver instance
boolbvt &get_boolbv_decision_procedure() const;

/// Return the equation associated with this instance
symex_target_equationt &get_equation() const;

Expand Down
3 changes: 1 addition & 2 deletions src/goto-checker/multi_path_symex_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -113,8 +113,7 @@ goto_tracet multi_path_symex_checkert::build_shortest_trace() const
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),
equation);
property_decider.get_boolbv_decision_procedure(), equation);

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
}

goto_tracet goto_trace;
Expand Down
3 changes: 1 addition & 2 deletions src/goto-checker/single_loop_incremental_symex_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -207,8 +207,7 @@ goto_tracet single_loop_incremental_symex_checkert::build_shortest_trace() const
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider.get_decision_procedure()),
equation);
property_decider.get_boolbv_decision_procedure(), equation);

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
}

goto_tracet goto_trace;
Expand Down
2 changes: 1 addition & 1 deletion src/goto-checker/single_path_symex_checker.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ goto_tracet single_path_symex_checkert::build_shortest_trace() const
{
// NOLINTNEXTLINE(whitespace/braces)
counterexample_beautificationt{ui_message_handler}(
dynamic_cast<boolbvt &>(property_decider->get_decision_procedure()),
property_decider->get_boolbv_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
54 changes: 29 additions & 25 deletions src/goto-checker/solver_factory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ Author: Daniel Kroening, Peter Schrammel
#include <solvers/sat/satcheck.h>
#include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
#include <solvers/smt2_incremental/smt_solver_process.h>
#include <solvers/stack_decision_procedure.h>
#include <solvers/strings/string_refinement.h>

#include <iostream>
Expand Down Expand Up @@ -65,10 +64,28 @@ solver_factoryt::solvert::solvert(
{
}

solver_factoryt::solvert::solvert(
std::unique_ptr<boolbvt> p1,

Check warning on line 68 in src/goto-checker/solver_factory.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/solver_factory.cpp#L68

Added line #L68 was not covered by tests
std::unique_ptr<propt> p2)
: prop_ptr(std::move(p2)), decision_procedure_is_boolbvt_ptr(std::move(p1))
{
}

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

Check warning on line 78 in src/goto-checker/solver_factory.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/solver_factory.cpp#L77-L78

Added lines #L77 - L78 were not covered by tests
if(decision_procedure_ptr)
return *decision_procedure_ptr;
else

Check warning on line 81 in src/goto-checker/solver_factory.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/solver_factory.cpp#L81

Added line #L81 was not covered by tests
return *decision_procedure_is_boolbvt_ptr;
}

boolbvt &solver_factoryt::solvert::boolbv_decision_procedure() const

Check warning on line 85 in src/goto-checker/solver_factory.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/solver_factory.cpp#L85

Added line #L85 was not covered by tests
{
PRECONDITION(decision_procedure_is_boolbvt_ptr != nullptr);
return *decision_procedure_is_boolbvt_ptr;

Check warning on line 88 in src/goto-checker/solver_factory.cpp

View check run for this annotation

Codecov / codecov/patch

src/goto-checker/solver_factory.cpp#L87-L88

Added lines #L87 - L88 were not covered by tests
}

void solver_factoryt::set_decision_procedure_time_limit(
Expand All @@ -81,22 +98,6 @@ void solver_factoryt::set_decision_procedure_time_limit(
decision_procedure.set_time_limit_seconds(timeout_seconds);
}

void solver_factoryt::solvert::set_decision_procedure(
std::unique_ptr<stack_decision_proceduret> p)
{
decision_procedure_ptr = std::move(p);
}

void solver_factoryt::solvert::set_prop(std::unique_ptr<propt> p)
{
prop_ptr = std::move(p);
}

void solver_factoryt::solvert::set_ofstream(std::unique_ptr<std::ofstream> p)
{
ofstream_ptr = std::move(p);
}

std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_solver()
{
if(options.get_bool_option("dimacs"))
Expand Down Expand Up @@ -339,8 +340,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()

set_decision_procedure_time_limit(*bv_pointers);

return std::make_unique<solvert>(
std::move(bv_pointers), std::move(sat_solver));
std::unique_ptr<boolbvt> boolbv = std::move(bv_pointers);
return std::make_unique<solvert>(std::move(boolbv), std::move(sat_solver));
}

std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
Expand All @@ -352,7 +353,7 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()

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

auto bv_dimacs =
std::unique_ptr<boolbvt> bv_dimacs =
std::make_unique<bv_dimacst>(ns, *prop, message_handler, filename);

return std::make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
Expand All @@ -367,7 +368,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_external_sat()
auto prop =
std::make_unique<external_satt>(message_handler, external_sat_solver);

auto bv_pointers = std::make_unique<bv_pointerst>(ns, *prop, message_handler);
std::unique_ptr<boolbvt> bv_pointers =
std::make_unique<bv_pointerst>(ns, *prop, message_handler);

return std::make_unique<solvert>(std::move(bv_pointers), std::move(prop));
}
Expand All @@ -390,7 +392,8 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
info.message_handler = &message_handler;

auto decision_procedure = std::make_unique<bv_refinementt>(info);
std::unique_ptr<boolbvt> decision_procedure =
std::make_unique<bv_refinementt>(info);
set_decision_procedure_time_limit(*decision_procedure);
return std::make_unique<solvert>(
std::move(decision_procedure), std::move(prop));
Expand All @@ -415,7 +418,8 @@ solver_factoryt::get_string_refinement()
info.refine_arithmetic = options.get_bool_option("refine-arithmetic");
info.message_handler = &message_handler;

auto decision_procedure = std::make_unique<string_refinementt>(info);
std::unique_ptr<boolbvt> decision_procedure =
std::make_unique<string_refinementt>(info);
set_decision_procedure_time_limit(*decision_procedure);
return std::make_unique<solvert>(
std::move(decision_procedure), std::move(prop));
Expand Down
10 changes: 5 additions & 5 deletions src/goto-checker/solver_factory.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Daniel Kroening, Peter Schrammel
#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H

#include <solvers/prop/prop.h>
#include <solvers/flattening/boolbv.h>
#include <solvers/smt2/smt2_dec.h>

#include <memory>
Expand Down Expand Up @@ -45,17 +45,17 @@ class solver_factoryt final
solvert(
std::unique_ptr<stack_decision_proceduret> p1,
std::unique_ptr<std::ofstream> p2);
solvert(std::unique_ptr<boolbvt> p1, std::unique_ptr<propt> p2);

stack_decision_proceduret &decision_procedure() const;
boolbvt &boolbv_decision_procedure() const;

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);

private:
// 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<stack_decision_proceduret> decision_procedure_ptr;
std::unique_ptr<boolbvt> decision_procedure_is_boolbvt_ptr;
};

/// Returns a solvert object
Expand Down

0 comments on commit ede4a3a

Please sign in to comment.