From f8cfad349b1f7fed7f9524a8dcc3d970f92361c3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 10 Oct 2019 17:27:05 +0100 Subject: [PATCH 1/3] solver: support let with multiple bindings This avoids deeply recursive expressions. --- src/solvers/flattening/boolbv_let.cpp | 27 ++++++++++++++------- src/solvers/prop/prop_conv_solver.cpp | 34 +++++++++++++++++++-------- 2 files changed, 42 insertions(+), 19 deletions(-) diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp index d14aa8487c6..66a56fa459c 100644 --- a/src/solvers/flattening/boolbv_let.cpp +++ b/src/solvers/flattening/boolbv_let.cpp @@ -8,25 +8,34 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" +#include #include #include 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; } diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index dc206b0db83..3bd5ae652b8 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "prop_conv_solver.h" +#include + #include 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) + 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) { - literalt value = convert(let_expr.value()); + 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; } } From 1872c07d29d01ea8f847528872d568e5108e0bc7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 10 Oct 2019 17:35:52 +0100 Subject: [PATCH 2/3] smt2 backend: support let with multiple bindings This avoids deeply recursive expressions. --- src/solvers/smt2/smt2_conv.cpp | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c68ff60fc2d..d0c6b502843 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -1855,11 +1856,28 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_let) { const let_exprt &let_expr=to_let_expr(expr); - out << "(let (("; - convert_expr(let_expr.symbol()); - out << ' '; - convert_expr(let_expr.value()); - out << ")) "; + const auto &variables = let_expr.variables(); + const auto &values = let_expr.values(); + + out << "(let ("; + 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()); out << ')'; // let } From cd0d0f6c95c298305d696fbbff82934dac43719f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 10 Oct 2019 23:46:01 +0100 Subject: [PATCH 3/3] smt2 parser: use let with multiple bindings This avoids deeply recursive expressions. --- src/solvers/smt2/smt2_parser.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index fcf85854fd0..0e7c9e386c9 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -208,21 +208,18 @@ exprt smt2_parsert::let_expression() b.first = add_fresh_id(b.first, b.second); } - exprt expr=expression(); + exprt where = expression(); if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' after let"); - exprt result=expr; + binding_exprt::variablest variables; + exprt::operandst values; - // go backwards, build let_expr - for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++) + for(const auto &b : bindings) { - const let_exprt let( - symbol_exprt(r_it->first, r_it->second.type()), - r_it->second, - result); - result=let; + variables.push_back(symbol_exprt(b.first, b.second.type())); + values.push_back(b.second); } // we keep these in the id_map in order to retain globally @@ -231,7 +228,7 @@ exprt smt2_parsert::let_expression() // restore renamings renaming_map=old_renaming_map; - return result; + return let_exprt(variables, values, where); } exprt smt2_parsert::quantifier_expression(irep_idt id)