replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

solver: support let with multiple bindings 

This avoids deeply recursive expressions.
This commit is contained in:
Daniel Kroening 2019-10-10 17:27:05 +01:00
parent afac9c7224
commit f8cfad349b
2 changed files with 43 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/solvers/flattening/boolbv_let.cpp
View File

@ -8,25 +8,34 @@ Author: Daniel Kroening, kroening@kroening.com
#include "boolbv.h"
#include <util/range.h>
#include <util/std_expr.h>
#include <util/std_types.h>
bvt boolbvt::convert_let(const let_exprt &expr)
{
const bvt value_bv=convert_bv(expr.value());
const auto &variables = expr.variables();
const auto &values = expr.values();
// We expect the identifiers of the bound symbols to be unique,
// and thus, these can go straight into the symbol to literal map.
// This property also allows us to cache any subexpressions.
const irep_idt &id=expr.symbol().get_identifier();
for(auto &binding : make_range(variables).zip(values))
{
const bvt value_bv = convert_bv(binding.second);
// We expect the identifiers of the bound symbols to be unique,
// and thus, these can go straight into the symbol to literal map.
// This property also allows us to cache any subexpressions.
const irep_idt &id = binding.first.get_identifier();
// the symbol shall be visible during the recursive call
// to convert_bv
map.set_literals(id, binding.first.type(), value_bv);
}
// the symbol shall be visible during the recursive call
// to convert_bv
map.set_literals(id, expr.symbol().type(), value_bv);
bvt result_bv=convert_bv(expr.where());
// now remove, no longer needed
map.erase_literals(id, expr.symbol().type());
for(auto &variable : variables)
map.erase_literals(variable.get_identifier(), variable.type());
return result_bv;
}

36
src/solvers/prop/prop_conv_solver.cpp
View File

@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
#include "prop_conv_solver.h"
#include <util/range.h>
#include <algorithm>
bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
@ -308,23 +310,35 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
else if(expr.id() == ID_let)
{
const let_exprt &let_expr = to_let_expr(expr);
const auto &variables = let_expr.variables();
const auto &values = let_expr.values();
// first check whether this is all boolean
if(
let_expr.value().type().id() == ID_bool &&
let_expr.where().type().id() == ID_bool)
{
literalt value = convert(let_expr.value());
const bool all_boolean =
let_expr.where().type().id() == ID_bool &&
std::all_of(values.begin(), values.end(), [](const exprt &e) {
return e.type().id() == ID_bool;
});
if(all_boolean)
{
for(auto &binding : make_range(variables).zip(values))
{
literalt value_converted = convert(binding.second);
// We expect the identifier of the bound symbols to be unique,
// and thus, these can go straight into the symbol map.
// This property also allows us to cache any subexpressions.
const irep_idt &id = binding.first.get_identifier();
symbols[id] = value_converted;
}
// We expect the identifier of the bound symbols to be unique,
// and thus, these can go straight into the symbol map.
// This property also allows us to cache any subexpressions.
const irep_idt &id = let_expr.symbol().get_identifier();
symbols[id] = value;
literalt result = convert(let_expr.where());
// remove again
symbols.erase(id);
for(auto &variable : variables)
symbols.erase(variable.get_identifier());
return result;
}
}