Skip to content
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

TG-634 Functional style for string refinement #1404

Merged
merged 28 commits into from
Sep 20, 2017
Merged

TG-634 Functional style for string refinement #1404

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
f99c8ff
Replace exceptions with optional
Sep 12, 2017
c5fa708
Refactor integer conversions
Sep 12, 2017
bf47f81
Use expr_cast in string_exprt casts
Sep 12, 2017
317c1c6
Group bv_refinement config variables
Sep 12, 2017
150bab1
Group string_refinement arguments
Sep 12, 2017
9fff116
Remove constructor boilerplate
Sep 12, 2017
2b2a841
Convert display_index_set to a free function
Sep 12, 2017
8e69d6d
Make functions static
Sep 15, 2017
cfb47db
Remove unused functions from string_refinement header
Sep 15, 2017
01b8301
static is_valid_string_constraint
Sep 15, 2017
bcd6111
Static is_axiom_sat
Sep 15, 2017
666c146
make static check_axioms
Sep 15, 2017
2eed573
Static add_axioms for strings
Sep 15, 2017
65ad3db
Public methods made public
Sep 15, 2017
e5e1ff4
static index_set functions
Sep 15, 2017
a4c8cf5
Static index set functions
Sep 15, 2017
918297c
static concretize length
Sep 15, 2017
78303df
Static concretize strings, lengths and results
Sep 15, 2017
229568a
static Instantiate not contains
Sep 15, 2017
7f11ccf
static set_char_array_equality
Sep 15, 2017
f5c1b29
static get_array
Sep 15, 2017
1531f0e
static debug_model
Sep 15, 2017
d03866d
static add axioms for string assings
Sep 15, 2017
bee20f1
Remove unused add_lemma parameter
Sep 16, 2017
9b8a025
Fix get lambdas
Sep 19, 2017
b544a4b
Fix unit test build
Sep 19, 2017
751e8f5
Adhere to lintage
Sep 19, 2017
05d5a9b
Address commenters' suggestions
Sep 19, 2017
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: 9 additions & 11 deletions src/solvers/refinement/bv_refinement.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,9 @@ Author: Daniel Kroening, [email protected]

class bv_refinementt:public bv_pointerst
{
public:
struct infot
private:
struct configt
{
const namespacet *ns=nullptr;
propt *prop=nullptr;
ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
/// Max number of times we refine a formula node
unsigned max_node_refinement=5;
Expand All @@ -33,6 +31,12 @@ class bv_refinementt:public bv_pointerst
/// Enable arithmetic refinement
bool refine_arithmetic=true;
};
public:
struct infot:public configt
{
const namespacet *ns=nullptr;
Copy link
Member

Choose a reason for hiding this comment

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

Making this hold a reference would be better instead of reintroducing pointers...

Copy link
Contributor Author

@LAJW LAJW Sep 20, 2017 •
edited
Loading

Choose a reason for hiding this comment

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

This is the solution to the problem of functions requiring too many arguments. Either we'd use this (essence pattern) or the builder pattern. Both of which use null pointers to hold the default value for a reference (but builder is more verbose, restricted to constructors only and not composable).

The only solution that allows usage of both arguments and references at the same time, are C++20 named arguments.

propt *prop=nullptr;
};

explicit bv_refinementt(const infot &info);

Expand Down Expand Up @@ -103,18 +107,12 @@ class bv_refinementt:public bv_pointerst

// MEMBERS

// Maximum number of times we refine a formula node
const unsigned max_node_refinement;
// Refinement toggles
const bool do_array_refinement;
const bool do_arithmetic_refinement;
bool progress;
std::vector<approximationt> approximations;
bvt parent_assumptions;

protected:
// use gui format
ui_message_handlert::uit ui;
configt config_;
};

#endif // CPROVER_SOLVERS_REFINEMENT_BV_REFINEMENT_H
9 changes: 3 additions & 6 deletions src/solvers/refinement/bv_refinement_loop.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,8 @@ Author: Daniel Kroening, [email protected]

bv_refinementt::bv_refinementt(const infot &info):
bv_pointerst(*info.ns, *info.prop),
max_node_refinement(info.max_node_refinement),
do_array_refinement(info.refine_arrays),
do_arithmetic_refinement(info.refine_arithmetic),
progress(false),
ui(info.ui)
config_(info)
Copy link
Member

Choose a reason for hiding this comment

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

The underscore seems unnecessary.

{
// check features we need
PRECONDITION(prop.has_set_assumptions());
Expand All @@ -44,11 +41,11 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
status() << "BV-Refinement: iteration " << iteration << eom;

// output the very same information in a structured fashion
if(ui==ui_message_handlert::uit::XML_UI)
if(config_.ui==ui_message_handlert::uit::XML_UI)
{
xmlt xml("refinement-iteration");
xml.data=std::to_string(iteration);
Copy link
Member

Choose a reason for hiding this comment

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

(improvement) replace cout by status() << xml;

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Replaced.

Copy link
Contributor

Choose a reason for hiding this comment

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

does this not require a status() << preformatted_output() << xml @peterschrammel?

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 don't think it's relevant, there was no preprocessing before.

std::cout << xml << '\n';
status() << xml << '\n';
}

switch(prop_solve())
Expand Down
10 changes: 5 additions & 5 deletions src/solvers/refinement/refine_arithmetic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ void bv_refinementt::approximationt::add_under_assumption(literalt l)

bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
{
if(!do_arithmetic_refinement)
if(!config_.refine_arithmetic)
return SUB::convert_floatbv_op(expr);

if(ns.follow(expr.type()).id()!=ID_floatbv ||
Expand All @@ -52,7 +52,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)

bvt bv_refinementt::convert_mult(const exprt &expr)
{
if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
return SUB::convert_mult(expr);

// we catch any multiplication
Expand Down Expand Up @@ -100,7 +100,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)

bvt bv_refinementt::convert_div(const div_exprt &expr)
{
if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
return SUB::convert_div(expr);

// we catch any division
Expand All @@ -118,7 +118,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)

bvt bv_refinementt::convert_mod(const mod_exprt &expr)
{
if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
return SUB::convert_mod(expr);

// we catch any mod
Expand Down Expand Up @@ -228,7 +228,7 @@ void bv_refinementt::check_SAT(approximationt &a)

// if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }

if(a.over_state<max_node_refinement)
if(a.over_state<config_.max_node_refinement)
{
bvt r;
float_utilst float_utils(prop);
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/refinement/refine_arrays.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,15 +29,15 @@ void bv_refinementt::post_process_arrays()
update_index_map(true);

// we don't actually add any constraints
lazy_arrays=do_array_refinement;
lazy_arrays=config_.refine_arrays;
add_array_constraints();
freeze_lazy_constraints();
}

/// check whether counterexample is spurious
void bv_refinementt::arrays_overapproximated()
{
if(!do_array_refinement)
if(!config_.refine_arrays)
return;

unsigned nb_active=0;
Expand Down
8 changes: 6 additions & 2 deletions src/solvers/refinement/string_constraint_generator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,14 +40,13 @@ class string_constraint_generatort final
/// Arguments pack for the string_constraint_generator constructor
struct infot
{
const namespacet *ns=nullptr;
/// Max length of non-deterministic strings
size_t string_max_length=std::numeric_limits<size_t>::max();
/// Prefer printable characters in non-deterministic strings
bool string_printable=false;
};

explicit string_constraint_generatort(const infot& info);
string_constraint_generatort(const infot& info, const namespacet& ns);

/// Axioms are of three kinds: universally quantified string constraint,
/// not contains string constraints and simple formulas.
Expand Down Expand Up @@ -81,6 +80,11 @@ class string_constraint_generatort final

symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);

/// remove functions applications and create the necessary axioms
/// \par parameters: an expression containing function applications
/// \return an expression containing no function application
exprt substitute_function_applications(const exprt& expr);

private:
symbol_exprt fresh_boolean(const irep_idt &prefix);
string_exprt fresh_string(const refined_string_typet &type);
Expand Down
20 changes: 18 additions & 2 deletions src/solvers/refinement/string_constraint_generator_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,10 +28,10 @@ Author: Romain Brenguier, [email protected]
#include <util/ssa_expr.h>

string_constraint_generatort::string_constraint_generatort(
const string_constraint_generatort::infot& info):
const string_constraint_generatort::infot& info, const namespacet& ns):
max_string_length(info.string_max_length),
m_force_printable_characters(info.string_printable),
m_ns(*info.ns) { }
m_ns(ns) { }

const std::vector<exprt> &string_constraint_generatort::get_axioms() const
{
Expand Down Expand Up @@ -628,3 +628,19 @@ exprt string_constraint_generatort::add_axioms_for_to_char_array(
string_exprt str=get_string_expr(args(f, 1)[0]);
return str.content();
}

exprt string_constraint_generatort::substitute_function_applications(
const exprt &expr)
{
exprt copy=expr;
for(exprt &operand : copy.operands())
operand=substitute_function_applications(exprt(operand));

if(copy.id()==ID_function_application)
{
function_application_exprt f=to_function_application_expr(copy);
return this->add_axioms_for_function_application(f);
}

return copy;
}
Loading