Merge pull request #5160 from diffblue/let_with_multiple_bindings
Let with multiple bindings
This commit is contained in:
commit
835af93ff2
|
@ -8,25 +8,34 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
|
|
||||||
#include "boolbv.h"
|
#include "boolbv.h"
|
||||||
|
|
||||||
|
#include <util/range.h>
|
||||||
#include <util/std_expr.h>
|
#include <util/std_expr.h>
|
||||||
#include <util/std_types.h>
|
#include <util/std_types.h>
|
||||||
|
|
||||||
bvt boolbvt::convert_let(const let_exprt &expr)
|
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,
|
for(auto &binding : make_range(variables).zip(values))
|
||||||
// and thus, these can go straight into the symbol to literal map.
|
{
|
||||||
// This property also allows us to cache any subexpressions.
|
const bvt value_bv = convert_bv(binding.second);
|
||||||
const irep_idt &id=expr.symbol().get_identifier();
|
|
||||||
|
// 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());
|
bvt result_bv=convert_bv(expr.where());
|
||||||
|
|
||||||
// now remove, no longer needed
|
// 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;
|
return result_bv;
|
||||||
}
|
}
|
||||||
|
|
|
@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
|
|
||||||
#include "prop_conv_solver.h"
|
#include "prop_conv_solver.h"
|
||||||
|
|
||||||
|
#include <util/range.h>
|
||||||
|
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
|
|
||||||
bool prop_conv_solvert::is_in_conflict(const exprt &expr) const
|
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)
|
else if(expr.id() == ID_let)
|
||||||
{
|
{
|
||||||
const let_exprt &let_expr = to_let_expr(expr);
|
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
|
// first check whether this is all boolean
|
||||||
if(
|
const bool all_boolean =
|
||||||
let_expr.value().type().id() == ID_bool &&
|
let_expr.where().type().id() == ID_bool &&
|
||||||
let_expr.where().type().id() == ID_bool)
|
std::all_of(values.begin(), values.end(), [](const exprt &e) {
|
||||||
{
|
return e.type().id() == ID_bool;
|
||||||
literalt value = convert(let_expr.value());
|
});
|
||||||
|
|
||||||
|
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());
|
literalt result = convert(let_expr.where());
|
||||||
|
|
||||||
// remove again
|
// remove again
|
||||||
symbols.erase(id);
|
for(auto &variable : variables)
|
||||||
|
symbols.erase(variable.get_identifier());
|
||||||
|
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
#include <util/invariant.h>
|
#include <util/invariant.h>
|
||||||
#include <util/mathematical_expr.h>
|
#include <util/mathematical_expr.h>
|
||||||
#include <util/pointer_offset_size.h>
|
#include <util/pointer_offset_size.h>
|
||||||
|
#include <util/range.h>
|
||||||
#include <util/std_expr.h>
|
#include <util/std_expr.h>
|
||||||
#include <util/std_types.h>
|
#include <util/std_types.h>
|
||||||
#include <util/string2int.h>
|
#include <util/string2int.h>
|
||||||
|
@ -1855,11 +1856,28 @@ void smt2_convt::convert_expr(const exprt &expr)
|
||||||
else if(expr.id()==ID_let)
|
else if(expr.id()==ID_let)
|
||||||
{
|
{
|
||||||
const let_exprt &let_expr=to_let_expr(expr);
|
const let_exprt &let_expr=to_let_expr(expr);
|
||||||
out << "(let ((";
|
const auto &variables = let_expr.variables();
|
||||||
convert_expr(let_expr.symbol());
|
const auto &values = let_expr.values();
|
||||||
out << ' ';
|
|
||||||
convert_expr(let_expr.value());
|
out << "(let (";
|
||||||
out << ")) ";
|
bool first = true;
|
||||||
|
|
||||||
|
for(auto &binding : make_range(variables).zip(values))
|
||||||
|
{
|
||||||
|
if(first)
|
||||||
|
first = false;
|
||||||
|
else
|
||||||
|
out << ' ';
|
||||||
|
|
||||||
|
out << '(';
|
||||||
|
convert_expr(binding.first);
|
||||||
|
out << ' ';
|
||||||
|
convert_expr(binding.second);
|
||||||
|
out << ')';
|
||||||
|
}
|
||||||
|
|
||||||
|
out << ") "; // bindings
|
||||||
|
|
||||||
convert_expr(let_expr.where());
|
convert_expr(let_expr.where());
|
||||||
out << ')'; // let
|
out << ')'; // let
|
||||||
}
|
}
|
||||||
|
|
|
@ -208,21 +208,18 @@ exprt smt2_parsert::let_expression()
|
||||||
b.first = add_fresh_id(b.first, b.second);
|
b.first = add_fresh_id(b.first, b.second);
|
||||||
}
|
}
|
||||||
|
|
||||||
exprt expr=expression();
|
exprt where = expression();
|
||||||
|
|
||||||
if(next_token() != smt2_tokenizert::CLOSE)
|
if(next_token() != smt2_tokenizert::CLOSE)
|
||||||
throw error("expected ')' after let");
|
throw error("expected ')' after let");
|
||||||
|
|
||||||
exprt result=expr;
|
binding_exprt::variablest variables;
|
||||||
|
exprt::operandst values;
|
||||||
|
|
||||||
// go backwards, build let_expr
|
for(const auto &b : bindings)
|
||||||
for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
|
|
||||||
{
|
{
|
||||||
const let_exprt let(
|
variables.push_back(symbol_exprt(b.first, b.second.type()));
|
||||||
symbol_exprt(r_it->first, r_it->second.type()),
|
values.push_back(b.second);
|
||||||
r_it->second,
|
|
||||||
result);
|
|
||||||
result=let;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
// we keep these in the id_map in order to retain globally
|
// we keep these in the id_map in order to retain globally
|
||||||
|
@ -231,7 +228,7 @@ exprt smt2_parsert::let_expression()
|
||||||
// restore renamings
|
// restore renamings
|
||||||
renaming_map=old_renaming_map;
|
renaming_map=old_renaming_map;
|
||||||
|
|
||||||
return result;
|
return let_exprt(variables, values, where);
|
||||||
}
|
}
|
||||||
|
|
||||||
exprt smt2_parsert::quantifier_expression(irep_idt id)
|
exprt smt2_parsert::quantifier_expression(irep_idt id)
|
||||||
|
|
Loading…
Reference in New Issue