Skip to content

Partial solver cleanup (straightforward changes) #1950

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 16 commits into from
Apr 23, 2018
Merged

Partial solver cleanup (straightforward changes) #1950

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
dc799e0
Assert replaced by unreachable
romainbrenguier Feb 7, 2018
8eb20f6
Use ranged for
romainbrenguier Feb 7, 2018
c1a93b3
Renaming `it` to symbol
romainbrenguier Feb 7, 2018
990f33e
Initialize at declaration instead of construction
romainbrenguier Feb 7, 2018
7db44fc
Remove virtual keyword where not needed
romainbrenguier Feb 7, 2018
a905a07
Replace throws by invariant or preconditions
romainbrenguier Feb 7, 2018
9179571
Remove useless includes
romainbrenguier Feb 7, 2018
ba13c94
Use auto for iterator types
romainbrenguier Feb 7, 2018
a0500f6
Use standard algorithm for finding an element
romainbrenguier Feb 7, 2018
13e87a9
Simplify dec_solve
romainbrenguier Feb 7, 2018
4987f3a
Remove useless comments
romainbrenguier Feb 7, 2018
5724a35
Simplify loop in prop_conv::get
romainbrenguier Feb 7, 2018
b18109f
Make make_(free_)bv_expr return exprt
romainbrenguier Feb 7, 2018
4365c28
Simplify boolbvt::set_to
romainbrenguier Feb 7, 2018
2d8be06
Rename `it` to pair in boolbvt::print_assignment
romainbrenguier Feb 7, 2018
4147243
Change set_variable_name API to consume irep_idt
romainbrenguier Apr 6, 2018
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
17 changes: 3 additions & 14 deletions src/cbmc/bv_cbmc.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,11 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
throw 0;
}

exprt new_cycle;
const exprt &old_cycle=expr.op0();
const exprt &cycle_var=expr.op1();
const exprt &bound=expr.op2();
const exprt &predicate=expr.op3();

make_free_bv_expr(expr.type(), new_cycle);
const exprt new_cycle = make_free_bv_expr(expr.type());
Copy link
Collaborator

Choose a reason for hiding this comment

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

This conflicts with a later declaration of new_cycle.


mp_integer bound_value;
if(to_integer(bound, bound_value))
Expand Down Expand Up @@ -98,18 +96,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)

bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr)
{
if(expr.operands().size()!=1)
{
error().source_location=expr.find_source_location();
error() << "waitfor_symbol expected to have one operand" << eom;
throw 0;
}

exprt result;
PRECONDITION(expr.operands().size() == 1);
const exprt &bound=expr.op0();

make_free_bv_expr(expr.type(), result);

const exprt result = make_free_bv_expr(expr.type());
// constraint: result<=bound

set_to_true(binary_relation_exprt(result, ID_le, bound));
Expand Down
59 changes: 17 additions & 42 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -631,54 +631,33 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)

void boolbvt::set_to(const exprt &expr, bool value)
{
if(expr.type().id()!=ID_bool)
{
error() << "boolbvt::set_to got non-boolean operand: "
<< expr.pretty() << eom;
throw 0;
}
PRECONDITION(expr.type().id() == ID_bool);

if(value)
{
if(expr.id()==ID_equal)
{
if(!boolbv_set_equality_to_true(to_equal_expr(expr)))
return;
}
}

return SUB::set_to(expr, value);
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
return;
SUB::set_to(expr, value);
}

void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
{
dest=exprt(ID_bv_literals, type);
exprt dest(ID_bv_literals, type);
irept::subt &bv_sub=dest.add(ID_bv).get_sub();

bv_sub.resize(bv.size());

for(std::size_t i=0; i<bv.size(); i++)
bv_sub[i].id(std::to_string(bv[i].get()));
return dest;
}

void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
exprt boolbvt::make_free_bv_expr(const typet &type)
{
std::size_t width=boolbv_width(type);

if(width==0)
{
error() << "failed to get width of " << type.pretty() << eom;
throw 0;
}

bvt bv;
bv.resize(width);

// make result free variables
Forall_literals(it, bv)
*it=prop.new_variable();

make_bv_expr(type, bv, dest);
const std::size_t width = boolbv_width(type);
PRECONDITION(width != 0);
bvt bv(width);
for(auto &lit : bv)
lit = prop.new_variable();
return make_bv_expr(type, bv);
}

bool boolbvt::is_unbounded_array(const typet &type) const
Expand Down Expand Up @@ -708,12 +687,8 @@ bool boolbvt::is_unbounded_array(const typet &type) const
void boolbvt::print_assignment(std::ostream &out) const
{
arrayst::print_assignment(out);

for(const auto &it : map.mapping)
{
out << it.first << "="
<< it.second.get_value(prop) << '\n';
}
for(const auto &pair : map.mapping)
out << pair.first << "=" << pair.second.get_value(prop) << '\n';
}

void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest)
Expand Down
6 changes: 3 additions & 3 deletions src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ class boolbvt:public arrayst
boolbv_mapt map;

// overloading
virtual literalt convert_rest(const exprt &expr) override;
literalt convert_rest(const exprt &expr) override;
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);

// NOLINTNEXTLINE(readability/identifiers)
Expand Down Expand Up @@ -176,8 +176,8 @@ class boolbvt:public arrayst
virtual bvt convert_function_application(
const function_application_exprt &expr);

virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
virtual void make_free_bv_expr(const typet &type, exprt &dest);
virtual exprt make_bv_expr(const typet &type, const bvt &bv);
virtual exprt make_free_bv_expr(const typet &type);

void convert_with(
const typet &type,
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/prop/prop.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ class propt:public messaget, public prop_assignmentt

// variables
virtual literalt new_variable()=0;
virtual void set_variable_name(literalt a, const std::string &name) { }
virtual void set_variable_name(literalt a, const irep_idt &name) { }
virtual size_t no_variables() const=0;
bvt new_variables(std::size_t width);

Expand Down
99 changes: 30 additions & 69 deletions src/solvers/prop/prop_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,40 +7,30 @@ Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/

#include "prop_conv.h"

#include <cassert>
#include <cstdlib>
#include <map>

#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/threeval.h>

#include "prop.h"
#include "literal_expr.h"
#include <algorithm>

/// determine whether a variable is in the final conflict
bool prop_convt::is_in_conflict(literalt l) const
{
assert(false);
UNREACHABLE;
return false;
}

void prop_convt::set_assumptions(const bvt &)
{
assert(false);
UNREACHABLE;
}

void prop_convt::set_frozen(const literalt)
{
assert(false);
UNREACHABLE;
}

void prop_convt::set_frozen(const bvt &bv)
{
for(unsigned i=0; i<bv.size(); i++)
if(!bv[i].is_constant())
set_frozen(bv[i]);
for(const auto &bit : bv)
if(!bit.is_constant())
set_frozen(bit);
}

bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
Expand All @@ -65,17 +55,14 @@ bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const

literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
{
std::pair<symbolst::iterator, bool> result=
auto result =
symbols.insert(std::pair<irep_idt, literalt>(identifier, literalt()));

if(!result.second)
return result.first->second;

// produce new variable
literalt literal=prop.new_variable();

// set the name of the new variable
prop.set_variable_name(literal, id2string(identifier));
prop.set_variable_name(literal, identifier);

// insert
result.first->second=literal;
Expand Down Expand Up @@ -183,10 +170,9 @@ literalt prop_conv_solvert::convert(const exprt &expr)
prop.set_frozen(literal);
return literal;
}
// check cache first

std::pair<cachet::iterator, bool> result=
cache.insert(std::pair<exprt, literalt>(expr, literalt()));
// check cache first
auto result = cache.insert({expr, literalt()});

if(!result.second)
return result.first->second;
Expand All @@ -208,13 +194,7 @@ literalt prop_conv_solvert::convert(const exprt &expr)

literalt prop_conv_solvert::convert_bool(const exprt &expr)
{
if(expr.type().id()!=ID_bool)
{
std::string msg="prop_convt::convert_bool got "
"non-boolean expression: ";
msg+=expr.pretty();
throw msg;
}
PRECONDITION(expr.type().id() == ID_bool);

const exprt::operandst &op=expr.operands();

Expand Down Expand Up @@ -280,8 +260,9 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor ||
expr.id()==ID_nor || expr.id()==ID_nand)
{
if(op.empty())
throw "operator `"+expr.id_string()+"' takes at least one operand";
INVARIANT(
!op.empty(),
"operator `" + expr.id_string() + "' takes at least one operand");

bvt bv;

Expand All @@ -304,16 +285,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
}
else if(expr.id()==ID_not)
{
if(op.size()!=1)
throw "not takes one operand";

INVARIANT(op.size() == 1, "not takes one operand");
return !convert(op.front());
}
else if(expr.id()==ID_equal || expr.id()==ID_notequal)
{
if(op.size()!=2)
throw "equality takes two operands";

INVARIANT(op.size() == 2, "equality takes two operands");
bool equal=(expr.id()==ID_equal);

if(op[0].type().id()==ID_bool &&
Expand Down Expand Up @@ -387,24 +364,14 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)

void prop_conv_solvert::set_to(const exprt &expr, bool value)
{
if(expr.type().id()!=ID_bool)
{
std::string msg="prop_convt::set_to got "
"non-boolean expression: ";
msg+=expr.pretty();
throw msg;
}
PRECONDITION(expr.type().id() == ID_bool);

bool boolean=true;

forall_operands(it, expr)
if(it->type().id()!=ID_bool)
{
boolean=false;
break;
}
const bool has_only_boolean_operands = std::all_of(
expr.operands().begin(),
expr.operands().end(),
[](const exprt &expr) { return expr.type().id() == ID_bool; });

if(boolean)
if(has_only_boolean_operands)
{
if(expr.id()==ID_not)
{
Expand Down Expand Up @@ -507,16 +474,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()

statistics() << "Solving with " << prop.solver_text() << eom;

propt::resultt result=prop.prop_solve();

switch(result)
switch(prop.prop_solve())
{
case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
default: return resultt::D_ERROR;
}

return resultt::D_ERROR;
}

exprt prop_conv_solvert::get(const exprt &expr) const
Expand All @@ -534,19 +497,17 @@ exprt prop_conv_solvert::get(const exprt &expr) const
}
}

exprt tmp=expr;

Forall_operands(it, tmp)
exprt tmp = expr;
for(auto &op : tmp.operands())
{
exprt tmp_op=get(*it);
it->swap(tmp_op);
exprt tmp_op = get(op);
op.swap(tmp_op);
}

return tmp;
}

void prop_conv_solvert::print_assignment(std::ostream &out) const
{
for(const auto &it : symbols)
out << it.first << " = " << prop.l_get(it.second) << "\n";
for(const auto &symbol : symbols)
out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
}
Loading