From fd64fae72f150758445f14c8ee6f56d410a5f8d5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Apr 2026 16:00:00 +0000 Subject: [PATCH 1/6] Extract mapst base class from arrayst Separate map-theoretic reasoning (index tracking, equality tracking, Ackermann constraints, read-over-weakeq, extensionality, CDCL(T) propagation, constraint counting) from array-specific encoding (with/if/of/comprehension constraints, lazy selects, 2D inlining). Inheritance chain: arrayst -> mapst -> equalityt -> prop_conv_solvert Co-authored-by: Kiro --- src/solvers/Makefile | 1 + src/solvers/flattening/arrays.cpp | 411 +--------------------------- src/solvers/flattening/arrays.h | 118 +------- src/solvers/flattening/maps.cpp | 436 ++++++++++++++++++++++++++++++ src/solvers/flattening/maps.h | 150 ++++++++++ 5 files changed, 596 insertions(+), 520 deletions(-) create mode 100644 src/solvers/flattening/maps.cpp create mode 100644 src/solvers/flattening/maps.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 9f4bf192744..7ff19b4a7a5 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -140,6 +140,7 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/bv_utils.cpp \ flattening/c_bit_field_replacement_type.cpp \ flattening/equality.cpp \ + flattening/maps.cpp \ flattening/pointer_logic.cpp \ floatbv/float_bv.cpp \ floatbv/float_utils.cpp \ diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 4aaae42cf6c..10425308ef5 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -9,8 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arrays.h" #include -#include -#include +#include #include #include #include @@ -31,25 +30,9 @@ arrayst::arrayst( propt &_prop, message_handlert &_message_handler, bool _get_array_constraints) - : equalityt(_prop, _message_handler), - ns(_ns), - log(_message_handler), + : mapst(_ns, _prop, _message_handler, _get_array_constraints), message_handler(_message_handler) { - lazy_arrays = false; // will be set to true when --refine is used - incremental_cache = false; // for incremental solving - // get_array_constraints is true when --show-array-constraints is used - get_array_constraints = _get_array_constraints; -} - -void arrayst::record_array_index(const index_exprt &index) -{ - // we are not allowed to put the index directly in the - // entry for the root of the equivalence class - // because this map is accessed during building the error trace - std::size_t number=arrays.number(index.array()); - if(index_map[number].insert(index.index()).second) - update_indices.insert(number); } literalt arrayst::record_array_equality( @@ -93,200 +76,6 @@ void arrayst::record_array_let_binding( prop.l_set_to_true(eq_lit); } -void arrayst::collect_indices() -{ - for(std::size_t i=0; i(a)) - { - arrays.make_union(a, let_expr->where()); - collect_arrays(let_expr->where()); - } - else - { - DATA_INVARIANT( - false, - "unexpected array expression (collect_arrays): '" + a.id_string() + "'"); - } -} - -/// adds array constraints (refine=true...lazily for the refinement loop) -void arrayst::add_array_constraint(const lazy_constraintt &lazy, bool refine) -{ - if(lazy_arrays && refine) - { - // lazily add the constraint - if(incremental_cache) - { - if(expr_map.find(lazy.lazy) == expr_map.end()) - { - lazy_array_constraints.push_back(lazy); - expr_map[lazy.lazy] = true; - } - } - else - { - lazy_array_constraints.push_back(lazy); - } - } - else - { - // add the constraint eagerly - prop.l_set_to_true(convert(lazy.lazy)); - } -} - void arrayst::add_array_constraints() { collect_indices(); @@ -337,151 +126,6 @@ void arrayst::add_array_constraints() add_array_Ackermann_constraints(); } -void arrayst::add_array_Ackermann_constraints() -{ - // this is quadratic! - -#ifdef DEBUG - std::cout << "arrays.size(): " << arrays.size() << '\n'; -#endif - - // iterate over arrays - for(std::size_t i=0; iis_constant() && i2->is_constant()) - continue; - - // index equality - const equal_exprt indices_equal( - *i1, typecast_exprt::conditional_cast(*i2, i1->type())); - - literalt indices_equal_lit=convert(indices_equal); - - if(indices_equal_lit!=const_literal(false)) - { - const typet &subtype = - to_array_type(arrays[i].type()).element_type(); - index_exprt index_expr1(arrays[i], *i1, subtype); - - index_exprt index_expr2=index_expr1; - index_expr2.index()=*i2; - - equal_exprt values_equal(index_expr1, index_expr2); - - // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN, - implies_exprt(literal_exprt(indices_equal_lit), values_equal)); - add_array_constraint(lazy, true); // added lazily - array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; - -#if 0 // old code for adding, not significantly faster - prop.lcnf(!indices_equal_lit, convert(values_equal)); -#endif - } - } - } -} - -/// merge the indices into the root -void arrayst::update_index_map(std::size_t i) -{ - if(arrays.is_root_number(i)) - return; - - std::size_t root_number=arrays.find_number(i); - INVARIANT(root_number!=i, "is_root_number incorrect?"); - - index_sett &root_index_set=index_map[root_number]; - index_sett &index_set=index_map[i]; - - root_index_set.insert(index_set.begin(), index_set.end()); -} - -void arrayst::update_index_map(bool update_all) -{ - // iterate over non-roots - // possible reasons why update is needed: - // -- there are new equivalence classes in arrays - // -- there are new indices for arrays that are not the root - // of an equivalence class - // (and we cannot do that in record_array_index()) - // -- equivalence classes have been merged - if(update_all) - { - for(std::size_t i=0; i x[i]=y[i] - - for(const auto &index : index_set) - { - const typet &element_type1 = - to_array_type(array_equality.f1.type()).element_type(); - index_exprt index_expr1(array_equality.f1, index, element_type1); - - const typet &element_type2 = - to_array_type(array_equality.f2.type()).element_type(); - index_exprt index_expr2(array_equality.f2, index, element_type2); - - DATA_INVARIANT( - index_expr1.type()==index_expr2.type(), - "array elements should all have same type"); - - array_equalityt equal; - equal.f1 = index_expr1; - equal.f2 = index_expr2; - equal.l = array_equality.l; - equal_exprt equality_expr(index_expr1, index_expr2); - - // add constraint - // equality constraints are not added lazily - // convert must be done to guarantee correct update of the index_set - prop.lcnf(!array_equality.l, convert(equality_expr)); - array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; - } -} - void arrayst::add_array_constraints( const index_sett &index_set, const exprt &expr) @@ -890,54 +534,3 @@ void arrayst::add_array_constraints_if( #endif } } - -std::string arrayst::enum_to_string(constraint_typet type) -{ - switch(type) - { - case constraint_typet::ARRAY_ACKERMANN: - return "arrayAckermann"; - case constraint_typet::ARRAY_WITH: - return "arrayWith"; - case constraint_typet::ARRAY_IF: - return "arrayIf"; - case constraint_typet::ARRAY_OF: - return "arrayOf"; - case constraint_typet::ARRAY_TYPECAST: - return "arrayTypecast"; - case constraint_typet::ARRAY_CONSTANT: - return "arrayConstant"; - case constraint_typet::ARRAY_COMPREHENSION: - return "arrayComprehension"; - case constraint_typet::ARRAY_EQUALITY: - return "arrayEquality"; - case constraint_typet::ARRAY_LET: - return "arrayLet"; - default: - UNREACHABLE; - } -} - -void arrayst::display_array_constraint_count() -{ - json_objectt json_result; - json_objectt &json_array_theory = - json_result["arrayConstraints"].make_object(); - - size_t num_constraints = 0; - - array_constraint_countt::iterator it = array_constraint_count.begin(); - while(it != array_constraint_count.end()) - { - std::string contraint_type_string = enum_to_string(it->first); - json_array_theory[contraint_type_string] = - json_numbert(std::to_string(it->second)); - - num_constraints += it->second; - it++; - } - - json_result["numOfConstraints"] = - json_numbert(std::to_string(num_constraints)); - log.status() << ",\n" << json_result; -} diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 1ebb1a457cb..f12d527fd20 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -12,25 +12,18 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_ARRAYS_H #define CPROVER_SOLVERS_FLATTENING_ARRAYS_H -#include -#include -#include - -#include - -#include "equality.h" +#include "maps.h" class array_comprehension_exprt; class array_exprt; class array_of_exprt; class equal_exprt; class if_exprt; -class index_exprt; class symbol_exprt; class with_exprt; class update_exprt; -class arrayst:public equalityt +class arrayst : public mapst { public: arrayst( @@ -39,19 +32,10 @@ class arrayst:public equalityt message_handlert &message_handler, bool get_array_constraints = false); - void finish_eager_conversion() override - { - finish_eager_conversion_arrays(); - SUB::finish_eager_conversion(); - if(get_array_constraints) - display_array_constraint_count(); - } - // NOLINTNEXTLINE(readability/identifiers) - typedef equalityt SUB; + typedef mapst SUB; - literalt record_array_equality(const equal_exprt &expr); - void record_array_index(const index_exprt &expr); + literalt record_array_equality(const equal_exprt &expr) override; /// Record that \p symbol is equal to \p value for the purposes of the /// array theory. For unbounded-array-typed bindings this connects the @@ -59,95 +43,18 @@ class arrayst:public equalityt /// propagate correctly. /// \pre \p value must be free of byte_update operators; lower them at the /// call site (collect_arrays otherwise fails a DATA_INVARIANT). - void record_array_let_binding(const symbol_exprt &symbol, const exprt &value); + void record_array_let_binding(const symbol_exprt &symbol, const exprt &value) + override; protected: - const namespacet &ns; - messaget log; message_handlert &message_handler; - virtual void finish_eager_conversion_arrays() + void finish_eager_conversion_arrays() override { add_array_constraints(); } - struct array_equalityt - { - literalt l; - exprt f1, f2; - }; - - // the list of all equalities between arrays - // references to objects in this container need to be stable as - // elements are added while references are held - typedef std::list array_equalitiest; - array_equalitiest array_equalities; - - // this is used to find the clusters of arrays being compared - union_find arrays; - - // this tracks the array indicies for each array - typedef std::set index_sett; - // references to values in this container need to be stable as - // elements are added while references are held - typedef std::map index_mapt; - index_mapt index_map; - - // adds array constraints lazily - enum class lazy_typet - { - ARRAY_ACKERMANN, - ARRAY_WITH, - ARRAY_IF, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_COMPREHENSION, - ARRAY_LET - }; - - struct lazy_constraintt - { - lazy_typet type; - exprt lazy; - - lazy_constraintt(lazy_typet _type, const exprt &_lazy) - { - type = _type; - lazy = _lazy; - } - }; - - bool lazy_arrays; - bool incremental_cache; - bool get_array_constraints; - std::list lazy_array_constraints; - void add_array_constraint(const lazy_constraintt &lazy, bool refine = true); - std::map expr_map; - - enum class constraint_typet - { - ARRAY_ACKERMANN, - ARRAY_WITH, - ARRAY_IF, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_COMPREHENSION, - ARRAY_EQUALITY, - ARRAY_LET - }; - - typedef std::map array_constraint_countt; - array_constraint_countt array_constraint_count; - void display_array_constraint_count(); - std::string enum_to_string(constraint_typet); - - // adds all the constraints eagerly void add_array_constraints(); - void add_array_Ackermann_constraints(); - void add_array_constraints_equality( - const index_sett &index_set, const array_equalityt &array_equality); void add_array_constraints( const index_sett &index_set, const exprt &expr); void add_array_constraints_if( @@ -164,17 +71,6 @@ class arrayst:public equalityt void add_array_constraints_comprehension( const index_sett &index_set, const array_comprehension_exprt &expr); - - void update_index_map(bool update_all); - void update_index_map(std::size_t i); - std::set update_indices; - void collect_arrays(const exprt &a); - void collect_indices(); - void collect_indices(const exprt &a); - std::unordered_set array_comprehension_args; - - virtual bool is_unbounded_array(const typet &type) const=0; - // (maybe this function should be partially moved here from boolbv) }; #endif // CPROVER_SOLVERS_FLATTENING_ARRAYS_H diff --git a/src/solvers/flattening/maps.cpp b/src/solvers/flattening/maps.cpp new file mode 100644 index 00000000000..22cbbe3fb89 --- /dev/null +++ b/src/solvers/flattening/maps.cpp @@ -0,0 +1,436 @@ +/*******************************************************************\ + +Module: Map Theory (base class for array theory) + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Map Theory — method implementations + +#include "maps.h" + +#include +#include + +#include +#include + +#ifdef DEBUG +# include + +# include +#endif + +mapst::mapst( + const namespacet &_ns, + propt &_prop, + message_handlert &_message_handler, + bool _get_array_constraints) + : equalityt(_prop, _message_handler), + ns(_ns), + log(_message_handler), + lazy_arrays(false), + incremental_cache(false), + get_array_constraints(_get_array_constraints) +{ +} + +void mapst::record_array_index(const index_exprt &index) +{ + // we are not allowed to put the index directly in the + // entry for the root of the equivalence class + // because this map is accessed during building the error trace + std::size_t number = arrays.number(index.array()); + if(index_map[number].insert(index.index()).second) + update_indices.insert(number); +} + +void mapst::collect_indices() +{ + for(std::size_t i = 0; i < arrays.size(); i++) + { + collect_indices(arrays[i]); + } +} + +void mapst::collect_indices(const exprt &expr) +{ + if(expr.id() != ID_index) + { + if(expr.id() == ID_array_comprehension) + array_comprehension_args.insert( + to_array_comprehension_expr(expr).arg().get_identifier()); + + for(const auto &op : expr.operands()) + collect_indices(op); + } + else + { + const index_exprt &e = to_index_expr(expr); + + if( + e.index().id() == ID_symbol && + array_comprehension_args.count( + to_symbol_expr(e.index()).get_identifier()) != 0) + { + return; + } + + collect_indices(e.index()); // necessary? + + const typet &array_op_type = e.array().type(); + + if(array_op_type.id() == ID_array) + { + const array_typet &array_type = to_array_type(array_op_type); + + if(is_unbounded_array(array_type)) + { + record_array_index(e); + } + } + } +} + +void mapst::collect_arrays(const exprt &a) +{ + const array_typet &array_type = to_array_type(a.type()); + + if(a.id() == ID_with) + { + const with_exprt &with_expr = to_with_expr(a); + + DATA_INVARIANT_WITH_DIAGNOSTICS( + array_type == with_expr.old().type(), + "collect_arrays got 'with' without matching types", + irep_pretty_diagnosticst{a}); + + arrays.make_union(a, with_expr.old()); + collect_arrays(with_expr.old()); + + // make sure this shows as an application + index_exprt index_expr(with_expr.old(), with_expr.where()); + record_array_index(index_expr); + } + else if(a.id() == ID_update) + { + const update_exprt &update_expr = to_update_expr(a); + + DATA_INVARIANT_WITH_DIAGNOSTICS( + array_type == update_expr.old().type(), + "collect_arrays got 'update' without matching types", + irep_pretty_diagnosticst{a}); + + arrays.make_union(a, update_expr.old()); + collect_arrays(update_expr.old()); + +#if 0 + // make sure this shows as an application + index_exprt index_expr(update_expr.old(), update_expr.index()); + record_array_index(index_expr); +#endif + } + else if(a.id() == ID_if) + { + const if_exprt &if_expr = to_if_expr(a); + + DATA_INVARIANT_WITH_DIAGNOSTICS( + array_type == if_expr.true_case().type(), + "collect_arrays got if without matching types", + irep_pretty_diagnosticst{a}); + + DATA_INVARIANT_WITH_DIAGNOSTICS( + array_type == if_expr.false_case().type(), + "collect_arrays got if without matching types", + irep_pretty_diagnosticst{a}); + + arrays.make_union(a, if_expr.true_case()); + arrays.make_union(a, if_expr.false_case()); + collect_arrays(if_expr.true_case()); + collect_arrays(if_expr.false_case()); + } + else if(a.id() == ID_symbol) + { + } + else if(a.id() == ID_nondet_symbol) + { + } + else if(a.id() == ID_member) + { + const auto &struct_op = to_member_expr(a).struct_op(); + + DATA_INVARIANT( + struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol, + "unexpected array expression: member with '" + struct_op.id_string() + + "'"); + } + else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant) + { + } + else if(a.id() == ID_array_of) + { + } + else if( + a.id() == ID_byte_update_little_endian || + a.id() == ID_byte_update_big_endian) + { + DATA_INVARIANT( + false, "byte_update should be removed before collect_arrays"); + } + else if(a.id() == ID_typecast) + { + const auto &typecast_op = to_typecast_expr(a).op(); + + // cast between array types? + DATA_INVARIANT( + typecast_op.type().id() == ID_array, + "unexpected array type cast from " + typecast_op.type().id_string()); + + arrays.make_union(a, typecast_op); + collect_arrays(typecast_op); + } + else if(a.id() == ID_index) + { + // nested unbounded arrays + const auto &array_op = to_index_expr(a).array(); + arrays.make_union(a, array_op); + collect_arrays(array_op); + } + else if(a.id() == ID_array_comprehension) + { + } + else if(auto let_expr = expr_try_dynamic_cast(a)) + { + arrays.make_union(a, let_expr->where()); + collect_arrays(let_expr->where()); + } + else + { + DATA_INVARIANT( + false, + "unexpected array expression (collect_arrays): '" + a.id_string() + "'"); + } +} + +/// adds array constraints (refine=true...lazily for the refinement loop) +void mapst::add_array_constraint( + const lazy_constraintt &lazy, + bool refine) +{ + if(lazy_arrays && refine) + { + // lazily add the constraint + if(incremental_cache) + { + if(expr_map.find(lazy.lazy) == expr_map.end()) + { + lazy_array_constraints.push_back(lazy); + expr_map[lazy.lazy] = true; + } + } + else + { + lazy_array_constraints.push_back(lazy); + } + } + else + { + // add the constraint eagerly + prop.l_set_to_true(convert(lazy.lazy)); + } +} + +void mapst::add_array_Ackermann_constraints() +{ + // this is quadratic! + +#ifdef DEBUG + std::cout << "arrays.size(): " << arrays.size() << '\n'; +#endif + + // iterate over arrays + for(std::size_t i = 0; i < arrays.size(); i++) + { + const index_sett &index_set = index_map[arrays.find_number(i)]; + +#ifdef DEBUG + std::cout << "index_set.size(): " << index_set.size() << '\n'; +#endif + + // iterate over indices, 2x! + for(index_sett::const_iterator i1 = index_set.begin(); + i1 != index_set.end(); + i1++) + for(index_sett::const_iterator i2 = i1; i2 != index_set.end(); i2++) + if(i1 != i2) + { + if(i1->is_constant() && i2->is_constant()) + continue; + + // index equality + const equal_exprt indices_equal( + *i1, typecast_exprt::conditional_cast(*i2, i1->type())); + + literalt indices_equal_lit = convert(indices_equal); + + if(indices_equal_lit != const_literal(false)) + { + const typet &subtype = + to_array_type(arrays[i].type()).element_type(); + index_exprt index_expr1(arrays[i], *i1, subtype); + + index_exprt index_expr2 = index_expr1; + index_expr2.index() = *i2; + + equal_exprt values_equal(index_expr1, index_expr2); + + // add constraint + lazy_constraintt lazy( + lazy_typet::ARRAY_ACKERMANN, + implies_exprt(literal_exprt(indices_equal_lit), values_equal)); + add_array_constraint(lazy, true); // added lazily + array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; + +#if 0 // old code for adding, not significantly faster + prop.lcnf(!indices_equal_lit, convert(values_equal)); +#endif + } + } + } +} + +/// merge the indices into the root +void mapst::update_index_map(std::size_t i) +{ + if(arrays.is_root_number(i)) + return; + + std::size_t root_number = arrays.find_number(i); + INVARIANT(root_number != i, "is_root_number incorrect?"); + + index_sett &root_index_set = index_map[root_number]; + index_sett &index_set = index_map[i]; + + root_index_set.insert(index_set.begin(), index_set.end()); +} + +void mapst::update_index_map(bool update_all) +{ + // iterate over non-roots + // possible reasons why update is needed: + // -- there are new equivalence classes in arrays + // -- there are new indices for arrays that are not the root + // of an equivalence class + // (and we cannot do that in record_array_index()) + // -- equivalence classes have been merged + if(update_all) + { + for(std::size_t i = 0; i < arrays.size(); i++) + update_index_map(i); + } + else + { + for(const auto &index : update_indices) + update_index_map(index); + + update_indices.clear(); + } + +#ifdef DEBUG + // print index sets + for(const auto &index_entry : index_map) + for(const auto &index : index_entry.second) + std::cout << "Index set (" << index_entry.first << " = " + << arrays.find_number(index_entry.first) << " = " + << format(arrays[arrays.find_number(index_entry.first)]) + << "): " << format(index) << '\n'; + std::cout << "-----\n"; +#endif +} + +void mapst::add_array_constraints_equality( + const index_sett &index_set, + const array_equalityt &array_equality) +{ + // add constraints x=y => x[i]=y[i] + + for(const auto &index : index_set) + { + const typet &element_type1 = + to_array_type(array_equality.f1.type()).element_type(); + index_exprt index_expr1(array_equality.f1, index, element_type1); + + const typet &element_type2 = + to_array_type(array_equality.f2.type()).element_type(); + index_exprt index_expr2(array_equality.f2, index, element_type2); + + DATA_INVARIANT( + index_expr1.type() == index_expr2.type(), + "array elements should all have same type"); + + array_equalityt equal; + equal.f1 = index_expr1; + equal.f2 = index_expr2; + equal.l = array_equality.l; + equal_exprt equality_expr(index_expr1, index_expr2); + + // add constraint + // equality constraints are not added lazily + // convert must be done to guarantee correct update of the index_set + prop.lcnf(!array_equality.l, convert(equality_expr)); + array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; + } +} + +std::string mapst::enum_to_string(constraint_typet type) +{ + switch(type) + { + case constraint_typet::ARRAY_ACKERMANN: + return "arrayAckermann"; + case constraint_typet::ARRAY_WITH: + return "arrayWith"; + case constraint_typet::ARRAY_IF: + return "arrayIf"; + case constraint_typet::ARRAY_OF: + return "arrayOf"; + case constraint_typet::ARRAY_TYPECAST: + return "arrayTypecast"; + case constraint_typet::ARRAY_CONSTANT: + return "arrayConstant"; + case constraint_typet::ARRAY_COMPREHENSION: + return "arrayComprehension"; + case constraint_typet::ARRAY_EQUALITY: + return "arrayEquality"; + case constraint_typet::ARRAY_LET: + return "arrayLet"; + default: + UNREACHABLE; + } +} + +void mapst::display_array_constraint_count() +{ + json_objectt json_result; + json_objectt &json_array_theory = + json_result["arrayConstraints"].make_object(); + + size_t num_constraints = 0; + + array_constraint_countt::iterator it = array_constraint_count.begin(); + while(it != array_constraint_count.end()) + { + std::string contraint_type_string = enum_to_string(it->first); + json_array_theory[contraint_type_string] = + json_numbert(std::to_string(it->second)); + + num_constraints += it->second; + it++; + } + + json_result["numOfConstraints"] = + json_numbert(std::to_string(num_constraints)); + log.status() << ",\n" << json_result; +} diff --git a/src/solvers/flattening/maps.h b/src/solvers/flattening/maps.h new file mode 100644 index 00000000000..9b3767dc3a1 --- /dev/null +++ b/src/solvers/flattening/maps.h @@ -0,0 +1,150 @@ +/*******************************************************************\ + +Module: Map Theory (base class for array theory) + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Map Theory — base class for arrayst, providing map-theoretic +/// reasoning (index tracking, equality tracking, Ackermann constraints). + +#ifndef CPROVER_SOLVERS_FLATTENING_MAPS_H +#define CPROVER_SOLVERS_FLATTENING_MAPS_H + +#include + +#include "equality.h" + +#include +#include +#include + +class equal_exprt; +class index_exprt; +class symbol_exprt; + +class mapst : public equalityt +{ +public: + mapst( + const namespacet &_ns, + propt &_prop, + message_handlert &_message_handler, + bool _get_array_constraints = false); + + ~mapst() override = default; + + // -- Pure virtual: implemented by arrayst -- + virtual literalt record_array_equality(const equal_exprt &expr) = 0; + virtual void + record_array_let_binding(const symbol_exprt &s, const exprt &v) = 0; + + // -- Virtual: default in mapst, may be overridden -- + virtual void record_array_index(const index_exprt &expr); + +protected: + const namespacet &ns; + messaget log; + + // -- Array equality tracking -- + struct array_equalityt + { + literalt l; + exprt f1, f2; + }; + typedef std::list array_equalitiest; + array_equalitiest array_equalities; + + // -- Arrays union-find -- + union_find arrays; + + // -- Index tracking -- + typedef std::set index_sett; + typedef std::map index_mapt; + index_mapt index_map; + std::set update_indices; + std::unordered_set array_comprehension_args; + + void collect_indices(); + void collect_indices(const exprt &a); + virtual void collect_arrays(const exprt &a); + void update_index_map(bool update_all); + void update_index_map(std::size_t i); + + virtual bool is_unbounded_array(const typet &type) const = 0; + + // -- Lazy constraint management -- + enum class lazy_typet + { + ARRAY_ACKERMANN, + ARRAY_WITH, + ARRAY_IF, + ARRAY_OF, + ARRAY_TYPECAST, + ARRAY_CONSTANT, + ARRAY_COMPREHENSION, + ARRAY_LET + }; + + struct lazy_constraintt + { + lazy_typet type; + exprt lazy; + + lazy_constraintt(lazy_typet _type, const exprt &_lazy) + : type(_type), lazy(_lazy) + { + } + }; + + std::list lazy_array_constraints; + bool lazy_arrays; + bool incremental_cache; + bool get_array_constraints; + std::map expr_map; + + void add_array_constraint(const lazy_constraintt &lazy, bool refine = true); + + // -- Ackermann constraints -- + void add_array_Ackermann_constraints(); + void add_array_constraints_equality( + const index_sett &index_set, + const array_equalityt &array_equality); + + // -- Constraint counting -- + enum class constraint_typet + { + ARRAY_ACKERMANN, + ARRAY_WITH, + ARRAY_IF, + ARRAY_OF, + ARRAY_TYPECAST, + ARRAY_CONSTANT, + ARRAY_COMPREHENSION, + ARRAY_EQUALITY, + ARRAY_LET + }; + typedef std::map array_constraint_countt; + array_constraint_countt array_constraint_count; + std::string enum_to_string(constraint_typet type); + void display_array_constraint_count(); + + // -- Eager conversion -- + void finish_eager_conversion() override + { + finish_eager_conversion_arrays(); + equalityt::finish_eager_conversion(); + if(get_array_constraints) + display_array_constraint_count(); + } + + virtual void finish_eager_conversion_arrays() + { + collect_indices(); + update_index_map(true); + } +}; + +#endif // CPROVER_SOLVERS_FLATTENING_MAPS_H From 868a212639f92df694cdca5185141066a4472d1c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 10:14:30 +0000 Subject: [PATCH 2/6] =?UTF-8?q?Use=20map-theory=20terminology:=20index?= =?UTF-8?q?=E2=86=92key,=20index=5Fmap=E2=86=92domain=5Fmap,=20remove=20'a?= =?UTF-8?q?rray'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In a map theory the tracked expressions are 'keys' and their collection per equivalence class is the 'domain'. Rename identifiers, type aliases, function names, and comments accordingly: index_sett → key_sett index_mapt → domain_mapt index_map → domain_map update_indices → update_keys collect_indices() → collect_keys() update_index_map() → update_domain_map() record_array_index()→ record_array_key() Rename all mapst members, methods, types, enum values, and comments to use map-theory terminology instead of array-specific terms: Types: array_equalityt → map_equalityt array_equalitiest → map_equalitiest array_constraint_countt → map_constraint_countt Members: array_equalities → map_equalities arrays (union-find) → maps lazy_array_constraints → lazy_constraints lazy_arrays → lazy_dispatch get_array_constraints → get_constraints array_constraint_count → constraint_count Methods: record_array_equality → record_equality record_array_let_binding→ record_let_binding record_array_key → record_key collect_arrays → collect_maps is_unbounded_array → is_unbounded_map add_array_constraint → add_map_constraint add_array_Ackermann_constraints → add_Ackermann_constraints add_array_constraints_equality → add_map_equality_constraints display_array_constraint_count → display_constraint_count finish_eager_conversion_arrays → finish_eager_conversion_maps Enum values: ARRAY_* → MAP_* C-level IR names (index_exprt, ID_index, etc.) are unchanged as they refer to the array-indexing operation, not the map-theory concept. Array-specific IR names (array_typet, index_exprt, ID_array, array_comprehension_args, etc.) and arrayst-specific method names (add_array_constraints, etc.) are unchanged. Note that the JSON output of '--show-array-constraints --json-ui' is intentionally NOT renamed: the user-visible strings stay 'arrayConstraints', 'arrayEquality', 'arrayWith', etc. The constraints this option reports are recorded by 'arrayst' (not by 'mapst'), the CLI option name says 'array', and any consumer of the JSON output shouldn't be forced to track an internal terminology change. The mapping from internal MAP_* enum tags to 'arrayX' strings lives in 'enum_to_string'; a comment there explains the asymmetry. Co-authored-by: Kiro --- src/solvers/flattening/arrays.cpp | 260 +++++++++--------- src/solvers/flattening/arrays.h | 30 +- src/solvers/flattening/boolbv.cpp | 4 +- src/solvers/flattening/boolbv.h | 6 +- src/solvers/flattening/boolbv_array_of.cpp | 2 +- .../flattening/boolbv_byte_extract.cpp | 2 +- src/solvers/flattening/boolbv_byte_update.cpp | 3 +- src/solvers/flattening/boolbv_equality.cpp | 7 +- src/solvers/flattening/boolbv_get.cpp | 18 +- src/solvers/flattening/boolbv_index.cpp | 4 +- src/solvers/flattening/boolbv_let.cpp | 4 +- src/solvers/flattening/boolbv_with.cpp | 2 +- src/solvers/flattening/bv_pointers.cpp | 5 +- src/solvers/flattening/bv_pointers.h | 2 +- src/solvers/flattening/maps.cpp | 236 ++++++++-------- src/solvers/flattening/maps.h | 113 ++++---- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/refine_arrays.cpp | 26 +- 18 files changed, 357 insertions(+), 369 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 10425308ef5..bf19ebd3140 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -29,83 +29,80 @@ arrayst::arrayst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_array_constraints) - : mapst(_ns, _prop, _message_handler, _get_array_constraints), + bool _get_constraints) + : mapst(_ns, _prop, _message_handler, _get_constraints), message_handler(_message_handler) { } -literalt arrayst::record_array_equality( - const equal_exprt &equality) +literalt arrayst::record_equality(const equal_exprt &equality) { const exprt &op0=equality.op0(); const exprt &op1=equality.op1(); DATA_INVARIANT_WITH_DIAGNOSTICS( op0.type() == op1.type(), - "record_array_equality got equality without matching types", + "record_equality got equality without matching types", irep_pretty_diagnosticst{equality}); DATA_INVARIANT( op0.type().id() == ID_array, - "record_array_equality parameter should be array-typed"); + "record_equality parameter should be array-typed"); - array_equalities.push_back(array_equalityt()); + map_equalities.push_back(map_equalityt()); - array_equalities.back().f1=op0; - array_equalities.back().f2=op1; - array_equalities.back().l=SUB::equality(op0, op1); + map_equalities.back().f1 = op0; + map_equalities.back().f2 = op1; + map_equalities.back().l = SUB::equality(op0, op1); - arrays.make_union(op0, op1); - collect_arrays(op0); - collect_arrays(op1); + maps.make_union(op0, op1); + collect_maps(op0); + collect_maps(op1); - return array_equalities.back().l; + return map_equalities.back().l; } -void arrayst::record_array_let_binding( - const symbol_exprt &symbol, - const exprt &value) +void arrayst::record_let_binding(const symbol_exprt &symbol, const exprt &value) { DATA_INVARIANT( symbol.type().id() == ID_array, - "record_array_let_binding parameter should be array-typed"); + "record_let_binding parameter should be array-typed"); const equal_exprt eq{symbol, value}; - const literalt eq_lit = record_array_equality(eq); + const literalt eq_lit = record_equality(eq); prop.l_set_to_true(eq_lit); } void arrayst::add_array_constraints() { - collect_indices(); - // at this point all indices should in the index set + collect_keys(); + // at this point all keys should be in the key set - // reduce initial index map - update_index_map(true); + // reduce initial domain map + update_domain_map(true); // add constraints for if, with, array_of, lambda std::set roots_to_process, updated_roots; - for(std::size_t i=0; i updated_indices; + std::unordered_set updated_keys; index_exprt index_expr( expr, expr.where(), to_array_type(expr.type()).element_type()); @@ -241,26 +235,27 @@ void arrayst::add_array_constraints_with( irep_pretty_diagnosticst{expr}); lazy_constraintt lazy( - lazy_typet::ARRAY_WITH, equal_exprt(index_expr, expr.new_value())); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_WITH]++; + lazy_typet::MAP_WITH, equal_exprt(index_expr, expr.new_value())); + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_WITH]++; - updated_indices.insert(expr.where()); + updated_keys.insert(expr.where()); - // For all other indices use the existing value, i.e., add constraints + // For all other keys use the existing value, i.e., add constraints // x[I]=y[I] for I!=i,j,... - for(auto other_index : index_set) + for(auto other_key : key_set) { - if(updated_indices.find(other_index) == updated_indices.end()) + if(updated_keys.find(other_key) == updated_keys.end()) { // we first build the guard exprt::operandst disjuncts; - disjuncts.reserve(updated_indices.size()); - for(const auto &index : updated_indices) + disjuncts.reserve(updated_keys.size()); + for(const auto &upd_key : updated_keys) { disjuncts.push_back(equal_exprt{ - index, typecast_exprt::conditional_cast(other_index, index.type())}); + upd_key, + typecast_exprt::conditional_cast(other_key, upd_key.type())}); } literalt guard_lit = convert(disjunction(disjuncts)); @@ -268,17 +263,18 @@ void arrayst::add_array_constraints_with( if(guard_lit!=const_literal(true)) { const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, other_index, element_type); - index_exprt index_expr2(expr.old(), other_index, element_type); + index_exprt index_expr1(expr, other_key, element_type); + index_exprt index_expr2(expr.old(), other_key, element_type); equal_exprt equality_expr(index_expr1, index_expr2); // add constraint - lazy_constraintt lazy(lazy_typet::ARRAY_WITH, or_exprt(equality_expr, - literal_exprt(guard_lit))); + lazy_constraintt lazy( + lazy_typet::MAP_WITH, + or_exprt(equality_expr, literal_exprt(guard_lit))); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_WITH]++; + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_WITH]++; #if 0 // old code for adding, not significantly faster { @@ -297,7 +293,7 @@ void arrayst::add_array_constraints_with( } void arrayst::add_array_constraints_update( - const index_sett &, + const key_sett &, const update_exprt &) { // we got x=UPDATE(y, [i], v) @@ -321,7 +317,7 @@ void arrayst::add_array_constraints_update( // use other array index applications for "else" case // add constraint x[I]=y[I] for I!=i - for(auto other_index : index_set) + for(auto other_index : key_set) { if(other_index!=index) { @@ -354,17 +350,17 @@ void arrayst::add_array_constraints_update( } void arrayst::add_array_constraints_array_of( - const index_sett &index_set, + const key_sett &key_set, const array_of_exprt &expr) { // we got x=array_of[v] // get other array index applications // and add constraint x[i]=v - for(const auto &index : index_set) + for(const auto &key : key_set) { const typet &element_type = expr.type().element_type(); - index_exprt index_expr(expr, index, element_type); + index_exprt index_expr(expr, key, element_type); DATA_INVARIANT( index_expr.type() == expr.what().type(), @@ -372,31 +368,31 @@ void arrayst::add_array_constraints_array_of( // add constraint lazy_constraintt lazy( - lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what())); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_OF]++; + lazy_typet::MAP_OF, equal_exprt(index_expr, expr.what())); + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_OF]++; } } void arrayst::add_array_constraints_array_constant( - const index_sett &index_set, + const key_sett &key_set, const array_exprt &expr) { // we got x = { v, ... } - add constraint x[i] = v const exprt::operandst &operands = expr.operands(); - for(const auto &index : index_set) + for(const auto &key : key_set) { const typet &element_type = expr.type().element_type(); - const index_exprt index_expr{expr, index, element_type}; + const index_exprt index_expr{expr, key, element_type}; - if(index.is_constant()) + if(key.is_constant()) { - // We have a constant index - just pick the element at that index from the - // array constant. + // We have a constant key - just pick the element at that position from + // the array constant. const std::optional i = - numeric_cast(to_constant_expr(index)); + numeric_cast(to_constant_expr(key)); // if the access is out of bounds, we leave it unconstrained if(!i.has_value() || *i >= operands.size()) continue; @@ -407,16 +403,16 @@ void arrayst::add_array_constraints_array_constant( "array operand type should match array element type"); // add constraint - lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT, - equal_exprt{index_expr, v}}; - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; + lazy_constraintt lazy{ + lazy_typet::MAP_CONSTANT, equal_exprt{index_expr, v}}; + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_CONSTANT]++; } else { - // We have a non-constant index into an array constant. We need to build a - // case statement testing the index against all possible values. Whenever - // neighbouring array elements are the same, we can test the index against + // We have a non-constant key into an array constant. We need to build a + // case statement testing the key against all possible values. Whenever + // neighbouring array elements are the same, we can test the key against // the range rather than individual elements. This should be particularly // helpful when we have arrays of zeros, as is the case for initializers. @@ -437,54 +433,54 @@ void arrayst::add_array_constraints_array_constant( if(range.first == range.second) { index_constraint = - equal_exprt{index, from_integer(range.first, index.type())}; + equal_exprt{key, from_integer(range.first, key.type())}; } else { index_constraint = and_exprt{ binary_predicate_exprt{ - from_integer(range.first, index.type()), ID_le, index}, + from_integer(range.first, key.type()), ID_le, key}, binary_predicate_exprt{ - index, ID_le, from_integer(range.second, index.type())}}; + key, ID_le, from_integer(range.second, key.type())}}; } lazy_constraintt lazy{ - lazy_typet::ARRAY_CONSTANT, - implies_exprt{index_constraint, - equal_exprt{index_expr, operands[range.first]}}}; - add_array_constraint(lazy, true); // added lazily - array_constraint_count[constraint_typet::ARRAY_CONSTANT]++; + lazy_typet::MAP_CONSTANT, + implies_exprt{ + index_constraint, equal_exprt{index_expr, operands[range.first]}}}; + add_map_constraint(lazy, true); // added lazily + constraint_count[constraint_typet::MAP_CONSTANT]++; } } } } void arrayst::add_array_constraints_comprehension( - const index_sett &index_set, + const key_sett &key_set, const array_comprehension_exprt &expr) { // we got x=lambda(i: e) // get all other array index applications // and add constraints x[j]=e[i/j] - for(const auto &index : index_set) + for(const auto &key : key_set) { - index_exprt index_expr{expr, index}; + index_exprt index_expr{expr, key}; exprt comprehension_body = expr.body(); - replace_expr(expr.arg(), index, comprehension_body); + replace_expr(expr.arg(), key, comprehension_body); // add constraint lazy_constraintt lazy( - lazy_typet::ARRAY_COMPREHENSION, + lazy_typet::MAP_COMPREHENSION, equal_exprt(index_expr, comprehension_body)); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++; + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_COMPREHENSION]++; } } void arrayst::add_array_constraints_if( - const index_sett &index_set, + const key_sett &key_set, const if_exprt &expr) { // we got x=(c?a:b) @@ -496,18 +492,19 @@ void arrayst::add_array_constraints_if( // first do true case - for(const auto &index : index_set) + for(const auto &key : key_set) { const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr.true_case(), index, element_type); + index_exprt index_expr1(expr, key, element_type); + index_exprt index_expr2(expr.true_case(), key, element_type); // add implication - lazy_constraintt lazy(lazy_typet::ARRAY_IF, - or_exprt(literal_exprt(!cond_lit), - equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_IF]++; + lazy_constraintt lazy( + lazy_typet::MAP_IF, + or_exprt( + literal_exprt(!cond_lit), equal_exprt(index_expr1, index_expr2))); + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -515,19 +512,18 @@ void arrayst::add_array_constraints_if( } // now the false case - for(const auto &index : index_set) + for(const auto &key : key_set) { const typet &element_type = to_array_type(expr.type()).element_type(); - index_exprt index_expr1(expr, index, element_type); - index_exprt index_expr2(expr.false_case(), index, element_type); + index_exprt index_expr1(expr, key, element_type); + index_exprt index_expr2(expr.false_case(), key, element_type); // add implication lazy_constraintt lazy( - lazy_typet::ARRAY_IF, - or_exprt(literal_exprt(cond_lit), - equal_exprt(index_expr1, index_expr2))); - add_array_constraint(lazy, false); // added immediately - array_constraint_count[constraint_typet::ARRAY_IF]++; + lazy_typet::MAP_IF, + or_exprt(literal_exprt(cond_lit), equal_exprt(index_expr1, index_expr2))); + add_map_constraint(lazy, false); // added immediately + constraint_count[constraint_typet::MAP_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2))); diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index f12d527fd20..f7f2a0d6ad4 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -30,12 +30,12 @@ class arrayst : public mapst const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_array_constraints = false); + bool get_constraints = false); // NOLINTNEXTLINE(readability/identifiers) typedef mapst SUB; - literalt record_array_equality(const equal_exprt &expr) override; + literalt record_equality(const equal_exprt &expr) override; /// Record that \p symbol is equal to \p value for the purposes of the /// array theory. For unbounded-array-typed bindings this connects the @@ -43,33 +43,33 @@ class arrayst : public mapst /// propagate correctly. /// \pre \p value must be free of byte_update operators; lower them at the /// call site (collect_arrays otherwise fails a DATA_INVARIANT). - void record_array_let_binding(const symbol_exprt &symbol, const exprt &value) - override; + void + record_let_binding(const symbol_exprt &symbol, const exprt &value) override; protected: message_handlert &message_handler; - void finish_eager_conversion_arrays() override + void finish_eager_conversion_maps() override { add_array_constraints(); } void add_array_constraints(); - void add_array_constraints( - const index_sett &index_set, const exprt &expr); - void add_array_constraints_if( - const index_sett &index_set, const if_exprt &exprt); - void add_array_constraints_with( - const index_sett &index_set, const with_exprt &expr); + void add_array_constraints(const key_sett &key_set, const exprt &expr); + void add_array_constraints_if(const key_sett &key_set, const if_exprt &exprt); + void + add_array_constraints_with(const key_sett &key_set, const with_exprt &expr); void add_array_constraints_update( - const index_sett &index_set, const update_exprt &expr); + const key_sett &key_set, + const update_exprt &expr); void add_array_constraints_array_of( - const index_sett &index_set, const array_of_exprt &exprt); + const key_sett &key_set, + const array_of_exprt &exprt); void add_array_constraints_array_constant( - const index_sett &index_set, + const key_sett &key_set, const array_exprt &exprt); void add_array_constraints_comprehension( - const index_sett &index_set, + const key_sett &key_set, const array_comprehension_exprt &expr); }; diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index bdeb176dd8f..522f7e64181 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -511,7 +511,7 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) type.id() != ID_bool) { // see if it is an unbounded array - if(is_unbounded_array(type)) + if(is_unbounded_map(type)) return true; const bvt &bv1=convert_bv(expr.rhs()); @@ -539,7 +539,7 @@ void boolbvt::set_to(const exprt &expr, bool value) SUB::set_to(expr, value); } -bool boolbvt::is_unbounded_array(const typet &type) const +bool boolbvt::is_unbounded_map(const typet &type) const { if(type.id()!=ID_array) return false; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 67c23ff8de3..2f9890db39b 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -53,8 +53,8 @@ class boolbvt:public arrayst const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_array_constraints = false) - : arrayst(_ns, _prop, message_handler, get_array_constraints), + bool get_constraints = false) + : arrayst(_ns, _prop, message_handler, get_constraints), unbounded_array(unbounded_arrayt::U_NONE), bv_width(_ns), bv_utils(_prop), @@ -267,7 +267,7 @@ class boolbvt:public arrayst exprt get_value(const exprt &expr) const; // unbounded arrays - bool is_unbounded_array(const typet &type) const override; + bool is_unbounded_map(const typet &type) const override; // quantifier instantiations class quantifiert diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp index 7a2ba2fa6f6..66066bf6f8a 100644 --- a/src/solvers/flattening/boolbv_array_of.cpp +++ b/src/solvers/flattening/boolbv_array_of.cpp @@ -20,7 +20,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr) const array_typet &array_type = expr.type(); - if(is_unbounded_array(array_type)) + if(is_unbounded_map(array_type)) return conversion_failed(expr); std::size_t width=boolbv_width(array_type); diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 01cb688063f..6b531f301c5 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -34,7 +34,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) { // array logic does not handle byte operators, thus lower when operating on // unbounded arrays - if(is_unbounded_array(expr.op().type())) + if(is_unbounded_map(expr.op().type())) { return convert_bv(lower_byte_extract(expr, ns)); } diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 3d94761b5a8..d06556a0f8a 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -17,8 +17,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) // if we update (from) an unbounded array, lower the expression as the array // logic does not handle byte operators if( - is_unbounded_array(expr.op().type()) || - is_unbounded_array(expr.value().type())) + is_unbounded_map(expr.op().type()) || is_unbounded_map(expr.value().type())) { return convert_bv(lower_byte_update(expr, ns)); } diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index 8e604fe9ac1..d308577296d 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -22,17 +22,16 @@ literalt boolbvt::convert_equality(const equal_exprt &expr) irep_pretty_diagnosticst{expr.rhs()}); // see if it is an unbounded array - if(is_unbounded_array(expr.lhs().type())) + if(is_unbounded_map(expr.lhs().type())) { // flatten byte_update/byte_extract operators if needed if(has_byte_operator(expr)) { - return record_array_equality( - to_equal_expr(lower_byte_operators(expr, ns))); + return record_equality(to_equal_expr(lower_byte_operators(expr, ns))); } - return record_array_equality(expr); + return record_equality(expr); } const bvt &lhs_bv = convert_bv(expr.lhs()); diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index b8cec54a8b5..21f4bc5c6f4 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -108,7 +108,7 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) { const auto &array_type = to_array_type(type); - if(is_unbounded_array(type)) + if(is_unbounded_map(type)) return bv_get_unbounded_array(expr); const typet &subtype = array_type.element_type(); @@ -328,20 +328,18 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const typedef std::map valuest; valuest values; - const auto opt_num = arrays.get_number(expr); + const auto opt_num = maps.get_number(expr); if(opt_num.has_value()) { // get root - const auto number = arrays.find_number(*opt_num); + const auto number = maps.find_number(*opt_num); - CHECK_RETURN(number < index_map.size()); - index_mapt::const_iterator it=index_map.find(number); - CHECK_RETURN(it != index_map.end()); - const index_sett &index_set=it->second; + CHECK_RETURN(number < domain_map.size()); + domain_mapt::const_iterator it = domain_map.find(number); + CHECK_RETURN(it != domain_map.end()); + const key_sett &key_set = it->second; - for(index_sett::const_iterator it1= - index_set.begin(); - it1!=index_set.end(); + for(key_sett::const_iterator it1 = key_set.begin(); it1 != key_set.end(); it1++) { index_exprt index(expr, *it1); diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index 2e400a57345..74aeb42716d 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -34,7 +34,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) // see if the array size is constant - if(is_unbounded_array(array_type)) + if(is_unbounded_map(array_type)) { // use array decision procedure @@ -65,7 +65,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) // free variables bv = prop.new_variables(boolbv_width(expr.type())); - record_array_index(expr); + record_key(expr); // record type if array is a symbol if(array.id() == ID_symbol || array.id() == ID_nondet_symbol) diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp index e9fe4632967..2e937aa6aa6 100644 --- a/src/solvers/flattening/boolbv_let.cpp +++ b/src/solvers/flattening/boolbv_let.cpp @@ -75,12 +75,12 @@ bvt boolbvt::convert_let(const let_exprt &expr) { if( pair.first.type().id() == ID_array && - is_unbounded_array(to_array_type(pair.first.type()))) + is_unbounded_map(to_array_type(pair.first.type()))) { const exprt lowered_value = has_byte_operator(pair.second) ? lower_byte_operators(pair.second, ns) : pair.second; - record_array_let_binding(pair.first, lowered_value); + record_let_binding(pair.first, lowered_value); } } diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index c7c335ff96c..887f4216be8 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -115,7 +115,7 @@ void boolbvt::convert_with_array( { // can't do this DATA_INVARIANT_WITH_DIAGNOSTICS( - !is_unbounded_array(type), + !is_unbounded_map(type), "convert_with_array called for unbounded array", irep_pretty_diagnosticst{type}); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 52482e8b060..fdcbdb9279c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -228,9 +228,8 @@ bv_pointerst::bv_pointerst( const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_array_constraints) - : boolbvt(_ns, _prop, message_handler, get_array_constraints), - pointer_logic(_ns) + bool get_constraints) + : boolbvt(_ns, _prop, message_handler, get_constraints), pointer_logic(_ns) { } diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 4486351fde0..5b3b669e2e4 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -20,7 +20,7 @@ class bv_pointerst:public boolbvt const namespacet &, propt &, message_handlert &, - bool get_array_constraints = false); + bool get_constraints = false); void finish_eager_conversion() override; diff --git a/src/solvers/flattening/maps.cpp b/src/solvers/flattening/maps.cpp index 22cbbe3fb89..8c60b7634f3 100644 --- a/src/solvers/flattening/maps.cpp +++ b/src/solvers/flattening/maps.cpp @@ -27,35 +27,35 @@ mapst::mapst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_array_constraints) + bool _get_constraints) : equalityt(_prop, _message_handler), ns(_ns), log(_message_handler), - lazy_arrays(false), + lazy_dispatch(false), incremental_cache(false), - get_array_constraints(_get_array_constraints) + get_constraints(_get_constraints) { } -void mapst::record_array_index(const index_exprt &index) +void mapst::record_key(const index_exprt &index) { - // we are not allowed to put the index directly in the + // we are not allowed to put the key directly in the // entry for the root of the equivalence class // because this map is accessed during building the error trace - std::size_t number = arrays.number(index.array()); - if(index_map[number].insert(index.index()).second) - update_indices.insert(number); + std::size_t number = maps.number(index.array()); + if(domain_map[number].insert(index.index()).second) + update_keys.insert(number); } -void mapst::collect_indices() +void mapst::collect_keys() { - for(std::size_t i = 0; i < arrays.size(); i++) + for(std::size_t i = 0; i < maps.size(); i++) { - collect_indices(arrays[i]); + collect_keys(maps[i]); } } -void mapst::collect_indices(const exprt &expr) +void mapst::collect_keys(const exprt &expr) { if(expr.id() != ID_index) { @@ -64,7 +64,7 @@ void mapst::collect_indices(const exprt &expr) to_array_comprehension_expr(expr).arg().get_identifier()); for(const auto &op : expr.operands()) - collect_indices(op); + collect_keys(op); } else { @@ -78,7 +78,7 @@ void mapst::collect_indices(const exprt &expr) return; } - collect_indices(e.index()); // necessary? + collect_keys(e.index()); // necessary? const typet &array_op_type = e.array().type(); @@ -86,15 +86,15 @@ void mapst::collect_indices(const exprt &expr) { const array_typet &array_type = to_array_type(array_op_type); - if(is_unbounded_array(array_type)) + if(is_unbounded_map(array_type)) { - record_array_index(e); + record_key(e); } } } } -void mapst::collect_arrays(const exprt &a) +void mapst::collect_maps(const exprt &a) { const array_typet &array_type = to_array_type(a.type()); @@ -104,15 +104,15 @@ void mapst::collect_arrays(const exprt &a) DATA_INVARIANT_WITH_DIAGNOSTICS( array_type == with_expr.old().type(), - "collect_arrays got 'with' without matching types", + "collect_maps got 'with' without matching types", irep_pretty_diagnosticst{a}); - arrays.make_union(a, with_expr.old()); - collect_arrays(with_expr.old()); + maps.make_union(a, with_expr.old()); + collect_maps(with_expr.old()); // make sure this shows as an application index_exprt index_expr(with_expr.old(), with_expr.where()); - record_array_index(index_expr); + record_key(index_expr); } else if(a.id() == ID_update) { @@ -120,16 +120,16 @@ void mapst::collect_arrays(const exprt &a) DATA_INVARIANT_WITH_DIAGNOSTICS( array_type == update_expr.old().type(), - "collect_arrays got 'update' without matching types", + "collect_maps got 'update' without matching types", irep_pretty_diagnosticst{a}); - arrays.make_union(a, update_expr.old()); - collect_arrays(update_expr.old()); + maps.make_union(a, update_expr.old()); + collect_maps(update_expr.old()); #if 0 // make sure this shows as an application index_exprt index_expr(update_expr.old(), update_expr.index()); - record_array_index(index_expr); + record_key(index_expr); #endif } else if(a.id() == ID_if) @@ -138,18 +138,18 @@ void mapst::collect_arrays(const exprt &a) DATA_INVARIANT_WITH_DIAGNOSTICS( array_type == if_expr.true_case().type(), - "collect_arrays got if without matching types", + "collect_maps got if without matching types", irep_pretty_diagnosticst{a}); DATA_INVARIANT_WITH_DIAGNOSTICS( array_type == if_expr.false_case().type(), - "collect_arrays got if without matching types", + "collect_maps got if without matching types", irep_pretty_diagnosticst{a}); - arrays.make_union(a, if_expr.true_case()); - arrays.make_union(a, if_expr.false_case()); - collect_arrays(if_expr.true_case()); - collect_arrays(if_expr.false_case()); + maps.make_union(a, if_expr.true_case()); + maps.make_union(a, if_expr.false_case()); + collect_maps(if_expr.true_case()); + collect_maps(if_expr.false_case()); } else if(a.id() == ID_symbol) { @@ -163,8 +163,7 @@ void mapst::collect_arrays(const exprt &a) DATA_INVARIANT( struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol, - "unexpected array expression: member with '" + struct_op.id_string() + - "'"); + "unexpected map expression: member with '" + struct_op.id_string() + "'"); } else if(a.is_constant() || a.id() == ID_array || a.id() == ID_string_constant) { @@ -176,63 +175,60 @@ void mapst::collect_arrays(const exprt &a) a.id() == ID_byte_update_little_endian || a.id() == ID_byte_update_big_endian) { - DATA_INVARIANT( - false, "byte_update should be removed before collect_arrays"); + DATA_INVARIANT(false, "byte_update should be removed before collect_maps"); } else if(a.id() == ID_typecast) { const auto &typecast_op = to_typecast_expr(a).op(); - // cast between array types? + // cast between map types? DATA_INVARIANT( typecast_op.type().id() == ID_array, - "unexpected array type cast from " + typecast_op.type().id_string()); + "unexpected map type cast from " + typecast_op.type().id_string()); - arrays.make_union(a, typecast_op); - collect_arrays(typecast_op); + maps.make_union(a, typecast_op); + collect_maps(typecast_op); } else if(a.id() == ID_index) { - // nested unbounded arrays + // nested unbounded maps const auto &array_op = to_index_expr(a).array(); - arrays.make_union(a, array_op); - collect_arrays(array_op); + maps.make_union(a, array_op); + collect_maps(array_op); } else if(a.id() == ID_array_comprehension) { } else if(auto let_expr = expr_try_dynamic_cast(a)) { - arrays.make_union(a, let_expr->where()); - collect_arrays(let_expr->where()); + maps.make_union(a, let_expr->where()); + collect_maps(let_expr->where()); } else { DATA_INVARIANT( false, - "unexpected array expression (collect_arrays): '" + a.id_string() + "'"); + "unexpected map expression (collect_maps): '" + a.id_string() + "'"); } } -/// adds array constraints (refine=true...lazily for the refinement loop) -void mapst::add_array_constraint( - const lazy_constraintt &lazy, - bool refine) +/// adds map constraints (refine=true...lazily for the refinement loop) +void mapst::add_map_constraint(const lazy_constraintt &lazy, bool refine) { - if(lazy_arrays && refine) + if(lazy_dispatch && refine) { // lazily add the constraint if(incremental_cache) { if(expr_map.find(lazy.lazy) == expr_map.end()) { - lazy_array_constraints.push_back(lazy); + lazy_constraints.push_back(lazy); expr_map[lazy.lazy] = true; } } else { - lazy_array_constraints.push_back(lazy); + lazy_constraints.push_back(lazy); } } else @@ -242,34 +238,33 @@ void mapst::add_array_constraint( } } -void mapst::add_array_Ackermann_constraints() +void mapst::add_Ackermann_constraints() { // this is quadratic! #ifdef DEBUG - std::cout << "arrays.size(): " << arrays.size() << '\n'; + std::cout << "maps.size(): " << maps.size() << '\n'; #endif - // iterate over arrays - for(std::size_t i = 0; i < arrays.size(); i++) + // iterate over maps + for(std::size_t i = 0; i < maps.size(); i++) { - const index_sett &index_set = index_map[arrays.find_number(i)]; + const key_sett &key_set = domain_map[maps.find_number(i)]; #ifdef DEBUG - std::cout << "index_set.size(): " << index_set.size() << '\n'; + std::cout << "key_set.size(): " << key_set.size() << '\n'; #endif - // iterate over indices, 2x! - for(index_sett::const_iterator i1 = index_set.begin(); - i1 != index_set.end(); + // iterate over keys, 2x! + for(key_sett::const_iterator i1 = key_set.begin(); i1 != key_set.end(); i1++) - for(index_sett::const_iterator i2 = i1; i2 != index_set.end(); i2++) + for(key_sett::const_iterator i2 = i1; i2 != key_set.end(); i2++) if(i1 != i2) { if(i1->is_constant() && i2->is_constant()) continue; - // index equality + // key equality const equal_exprt indices_equal( *i1, typecast_exprt::conditional_cast(*i2, i1->type())); @@ -277,9 +272,8 @@ void mapst::add_array_Ackermann_constraints() if(indices_equal_lit != const_literal(false)) { - const typet &subtype = - to_array_type(arrays[i].type()).element_type(); - index_exprt index_expr1(arrays[i], *i1, subtype); + const typet &subtype = to_array_type(maps[i].type()).element_type(); + index_exprt index_expr1(maps[i], *i1, subtype); index_exprt index_expr2 = index_expr1; index_expr2.index() = *i2; @@ -288,10 +282,10 @@ void mapst::add_array_Ackermann_constraints() // add constraint lazy_constraintt lazy( - lazy_typet::ARRAY_ACKERMANN, + lazy_typet::MAP_ACKERMANN, implies_exprt(literal_exprt(indices_equal_lit), values_equal)); - add_array_constraint(lazy, true); // added lazily - array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++; + add_map_constraint(lazy, true); // added lazily + constraint_count[constraint_typet::MAP_ACKERMANN]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -301,117 +295,123 @@ void mapst::add_array_Ackermann_constraints() } } -/// merge the indices into the root -void mapst::update_index_map(std::size_t i) +/// merge the keys into the root +void mapst::update_domain_map(std::size_t i) { - if(arrays.is_root_number(i)) + if(maps.is_root_number(i)) return; - std::size_t root_number = arrays.find_number(i); + std::size_t root_number = maps.find_number(i); INVARIANT(root_number != i, "is_root_number incorrect?"); - index_sett &root_index_set = index_map[root_number]; - index_sett &index_set = index_map[i]; + key_sett &root_key_set = domain_map[root_number]; + key_sett &key_set = domain_map[i]; - root_index_set.insert(index_set.begin(), index_set.end()); + root_key_set.insert(key_set.begin(), key_set.end()); } -void mapst::update_index_map(bool update_all) +void mapst::update_domain_map(bool update_all) { // iterate over non-roots // possible reasons why update is needed: - // -- there are new equivalence classes in arrays - // -- there are new indices for arrays that are not the root + // -- there are new equivalence classes in maps + // -- there are new keys for maps that are not the root // of an equivalence class - // (and we cannot do that in record_array_index()) + // (and we cannot do that in record_key()) // -- equivalence classes have been merged if(update_all) { - for(std::size_t i = 0; i < arrays.size(); i++) - update_index_map(i); + for(std::size_t i = 0; i < maps.size(); i++) + update_domain_map(i); } else { - for(const auto &index : update_indices) - update_index_map(index); + for(const auto &key : update_keys) + update_domain_map(key); - update_indices.clear(); + update_keys.clear(); } #ifdef DEBUG - // print index sets - for(const auto &index_entry : index_map) - for(const auto &index : index_entry.second) - std::cout << "Index set (" << index_entry.first << " = " - << arrays.find_number(index_entry.first) << " = " - << format(arrays[arrays.find_number(index_entry.first)]) - << "): " << format(index) << '\n'; + // print key sets + for(const auto &domain_entry : domain_map) + for(const auto &key : domain_entry.second) + std::cout << "Key set (" << domain_entry.first << " = " + << maps.find_number(domain_entry.first) << " = " + << format(maps[maps.find_number(domain_entry.first)]) + << "): " << format(key) << '\n'; std::cout << "-----\n"; #endif } -void mapst::add_array_constraints_equality( - const index_sett &index_set, - const array_equalityt &array_equality) +void mapst::add_map_equality_constraints( + const key_sett &key_set, + const map_equalityt &equality) { // add constraints x=y => x[i]=y[i] - for(const auto &index : index_set) + for(const auto &key : key_set) { const typet &element_type1 = - to_array_type(array_equality.f1.type()).element_type(); - index_exprt index_expr1(array_equality.f1, index, element_type1); + to_array_type(equality.f1.type()).element_type(); + index_exprt index_expr1(equality.f1, key, element_type1); const typet &element_type2 = - to_array_type(array_equality.f2.type()).element_type(); - index_exprt index_expr2(array_equality.f2, index, element_type2); + to_array_type(equality.f2.type()).element_type(); + index_exprt index_expr2(equality.f2, key, element_type2); DATA_INVARIANT( index_expr1.type() == index_expr2.type(), - "array elements should all have same type"); + "map elements should all have same type"); - array_equalityt equal; + map_equalityt equal; equal.f1 = index_expr1; equal.f2 = index_expr2; - equal.l = array_equality.l; + equal.l = equality.l; equal_exprt equality_expr(index_expr1, index_expr2); // add constraint // equality constraints are not added lazily - // convert must be done to guarantee correct update of the index_set - prop.lcnf(!array_equality.l, convert(equality_expr)); - array_constraint_count[constraint_typet::ARRAY_EQUALITY]++; + // convert must be done to guarantee correct update of the key_set + prop.lcnf(!equality.l, convert(equality_expr)); + constraint_count[constraint_typet::MAP_EQUALITY]++; } } std::string mapst::enum_to_string(constraint_typet type) { + // The internal enum tags are MAP_X, but the JSON strings are kept as + // arrayX/arrayConstraints because the constraints reported by + // --show-array-constraints are array-specific (arrayst is the only + // implementation that records them, and the CLI option name says + // 'array'). Decoupling here preserves backward compatibility for + // consumers of --show-array-constraints --json-ui output. switch(type) { - case constraint_typet::ARRAY_ACKERMANN: + case constraint_typet::MAP_ACKERMANN: return "arrayAckermann"; - case constraint_typet::ARRAY_WITH: + case constraint_typet::MAP_WITH: return "arrayWith"; - case constraint_typet::ARRAY_IF: + case constraint_typet::MAP_IF: return "arrayIf"; - case constraint_typet::ARRAY_OF: + case constraint_typet::MAP_OF: return "arrayOf"; - case constraint_typet::ARRAY_TYPECAST: + case constraint_typet::MAP_TYPECAST: return "arrayTypecast"; - case constraint_typet::ARRAY_CONSTANT: + case constraint_typet::MAP_CONSTANT: return "arrayConstant"; - case constraint_typet::ARRAY_COMPREHENSION: + case constraint_typet::MAP_COMPREHENSION: return "arrayComprehension"; - case constraint_typet::ARRAY_EQUALITY: + case constraint_typet::MAP_EQUALITY: return "arrayEquality"; - case constraint_typet::ARRAY_LET: + case constraint_typet::MAP_LET: return "arrayLet"; default: UNREACHABLE; } } -void mapst::display_array_constraint_count() +void mapst::display_constraint_count() { json_objectt json_result; json_objectt &json_array_theory = @@ -419,8 +419,8 @@ void mapst::display_array_constraint_count() size_t num_constraints = 0; - array_constraint_countt::iterator it = array_constraint_count.begin(); - while(it != array_constraint_count.end()) + map_constraint_countt::iterator it = constraint_count.begin(); + while(it != constraint_count.end()) { std::string contraint_type_string = enum_to_string(it->first); json_array_theory[contraint_type_string] = diff --git a/src/solvers/flattening/maps.h b/src/solvers/flattening/maps.h index 9b3767dc3a1..c1447030fd9 100644 --- a/src/solvers/flattening/maps.h +++ b/src/solvers/flattening/maps.h @@ -8,7 +8,7 @@ Author: Michael Tautschnig /// \file /// Map Theory — base class for arrayst, providing map-theoretic -/// reasoning (index tracking, equality tracking, Ackermann constraints). +/// reasoning (key tracking, equality tracking, Ackermann constraints). #ifndef CPROVER_SOLVERS_FLATTENING_MAPS_H #define CPROVER_SOLVERS_FLATTENING_MAPS_H @@ -32,60 +32,59 @@ class mapst : public equalityt const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_array_constraints = false); + bool _get_constraints = false); ~mapst() override = default; // -- Pure virtual: implemented by arrayst -- - virtual literalt record_array_equality(const equal_exprt &expr) = 0; - virtual void - record_array_let_binding(const symbol_exprt &s, const exprt &v) = 0; + virtual literalt record_equality(const equal_exprt &expr) = 0; + virtual void record_let_binding(const symbol_exprt &s, const exprt &v) = 0; // -- Virtual: default in mapst, may be overridden -- - virtual void record_array_index(const index_exprt &expr); + virtual void record_key(const index_exprt &expr); protected: const namespacet &ns; messaget log; - // -- Array equality tracking -- - struct array_equalityt + // -- Map equality tracking -- + struct map_equalityt { literalt l; exprt f1, f2; }; - typedef std::list array_equalitiest; - array_equalitiest array_equalities; + typedef std::list map_equalitiest; + map_equalitiest map_equalities; - // -- Arrays union-find -- - union_find arrays; + // -- Maps union-find -- + union_find maps; - // -- Index tracking -- - typedef std::set index_sett; - typedef std::map index_mapt; - index_mapt index_map; - std::set update_indices; + // -- Key tracking -- + typedef std::set key_sett; + typedef std::map domain_mapt; + domain_mapt domain_map; + std::set update_keys; std::unordered_set array_comprehension_args; - void collect_indices(); - void collect_indices(const exprt &a); - virtual void collect_arrays(const exprt &a); - void update_index_map(bool update_all); - void update_index_map(std::size_t i); + void collect_keys(); + void collect_keys(const exprt &a); + virtual void collect_maps(const exprt &a); + void update_domain_map(bool update_all); + void update_domain_map(std::size_t i); - virtual bool is_unbounded_array(const typet &type) const = 0; + virtual bool is_unbounded_map(const typet &type) const = 0; // -- Lazy constraint management -- enum class lazy_typet { - ARRAY_ACKERMANN, - ARRAY_WITH, - ARRAY_IF, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_COMPREHENSION, - ARRAY_LET + MAP_ACKERMANN, + MAP_WITH, + MAP_IF, + MAP_OF, + MAP_TYPECAST, + MAP_CONSTANT, + MAP_COMPREHENSION, + MAP_LET }; struct lazy_constraintt @@ -99,51 +98,51 @@ class mapst : public equalityt } }; - std::list lazy_array_constraints; - bool lazy_arrays; + std::list lazy_constraints; + bool lazy_dispatch; bool incremental_cache; - bool get_array_constraints; + bool get_constraints; std::map expr_map; - void add_array_constraint(const lazy_constraintt &lazy, bool refine = true); + void add_map_constraint(const lazy_constraintt &lazy, bool refine = true); // -- Ackermann constraints -- - void add_array_Ackermann_constraints(); - void add_array_constraints_equality( - const index_sett &index_set, - const array_equalityt &array_equality); + void add_Ackermann_constraints(); + void add_map_equality_constraints( + const key_sett &key_set, + const map_equalityt &equality); // -- Constraint counting -- enum class constraint_typet { - ARRAY_ACKERMANN, - ARRAY_WITH, - ARRAY_IF, - ARRAY_OF, - ARRAY_TYPECAST, - ARRAY_CONSTANT, - ARRAY_COMPREHENSION, - ARRAY_EQUALITY, - ARRAY_LET + MAP_ACKERMANN, + MAP_WITH, + MAP_IF, + MAP_OF, + MAP_TYPECAST, + MAP_CONSTANT, + MAP_COMPREHENSION, + MAP_EQUALITY, + MAP_LET }; - typedef std::map array_constraint_countt; - array_constraint_countt array_constraint_count; + typedef std::map map_constraint_countt; + map_constraint_countt constraint_count; std::string enum_to_string(constraint_typet type); - void display_array_constraint_count(); + void display_constraint_count(); // -- Eager conversion -- void finish_eager_conversion() override { - finish_eager_conversion_arrays(); + finish_eager_conversion_maps(); equalityt::finish_eager_conversion(); - if(get_array_constraints) - display_array_constraint_count(); + if(get_constraints) + display_constraint_count(); } - virtual void finish_eager_conversion_arrays() + virtual void finish_eager_conversion_maps() { - collect_indices(); - update_index_map(true); + collect_keys(); + update_domain_map(true); } }; diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index c26bb556f41..bdeebe14ca0 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -49,7 +49,7 @@ class bv_refinementt:public bv_pointerst protected: // Refine array - void finish_eager_conversion_arrays() override; + void finish_eager_conversion_maps() override; // Refine arithmetic bvt convert_mult(const mult_exprt &expr) override; diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 1456410dc7f..809601077d4 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -17,17 +17,17 @@ Author: Daniel Kroening, kroening@kroening.com #include -/// generate array constraints -void bv_refinementt::finish_eager_conversion_arrays() +/// generate map constraints +void bv_refinementt::finish_eager_conversion_maps() { - collect_indices(); - // at this point all indices should in the index set + collect_keys(); + // at this point all keys should be in the key set // just build the data structure - update_index_map(true); + update_domain_map(true); // we don't actually add any constraints - lazy_arrays=config_.refine_arrays; + lazy_dispatch = config_.refine_arrays; add_array_constraints(); freeze_lazy_constraints(); } @@ -52,11 +52,9 @@ void bv_refinementt::arrays_overapproximated() std::list::iterator list_it; }; std::vector to_check; - to_check.reserve(lazy_array_constraints.size()); + to_check.reserve(lazy_constraints.size()); - for(auto it = lazy_array_constraints.begin(); - it != lazy_array_constraints.end(); - ++it) + for(auto it = lazy_constraints.begin(); it != lazy_constraints.end(); ++it) { const exprt ¤t = it->lazy; @@ -105,7 +103,7 @@ void bv_refinementt::arrays_overapproximated() case decision_proceduret::resultt::D_UNSATISFIABLE: prop.l_set_to_true(convert(entry.constraint)); nb_active++; - lazy_array_constraints.erase(entry.list_it); + lazy_constraints.erase(entry.list_it); break; case decision_proceduret::resultt::D_ERROR: INVARIANT(false, "error in array over approximation check"); @@ -114,7 +112,7 @@ void bv_refinementt::arrays_overapproximated() log.debug() << "BV-Refinement: " << nb_active << " array expressions become active" << messaget::eom; - log.debug() << "BV-Refinement: " << lazy_array_constraints.size() + log.debug() << "BV-Refinement: " << lazy_constraints.size() << " inactive array expressions" << messaget::eom; if(nb_active > 0) progress=true; @@ -124,10 +122,10 @@ void bv_refinementt::arrays_overapproximated() /// freeze symbols for incremental solving void bv_refinementt::freeze_lazy_constraints() { - if(!lazy_arrays) + if(!lazy_dispatch) return; - for(const auto &constraint : lazy_array_constraints) + for(const auto &constraint : lazy_constraints) { // Freeze all symbols in the constraint for(const auto &symbol : find_symbols(constraint.lazy)) From 7ef84389454e96cc87e5d2be4a68d0bcdbf6c76b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 12:16:10 +0000 Subject: [PATCH 3/6] Add Doxygen documentation to mapst Document all public and protected methods, key data members, enums, and structs in maps.h with Doxygen comments following the CBMC coding standard. Co-authored-by: Kiro --- src/solvers/flattening/maps.h | 92 +++++++++++++++++++++++++++++++---- 1 file changed, 83 insertions(+), 9 deletions(-) diff --git a/src/solvers/flattening/maps.h b/src/solvers/flattening/maps.h index c1447030fd9..d5280111b62 100644 --- a/src/solvers/flattening/maps.h +++ b/src/solvers/flattening/maps.h @@ -25,9 +25,19 @@ class equal_exprt; class index_exprt; class symbol_exprt; +/// Base class for map-theoretic reasoning (key tracking, equality tracking, +/// Ackermann constraints, constraint counting). Subclassed by \ref arrayst, +/// which adds array-specific encoding (with/if/of/comprehension constraints). +/// +/// Inheritance chain: arrayst → mapst → equalityt → prop_conv_solvert class mapst : public equalityt { public: + /// \param _ns: namespace for type lookups + /// \param _prop: propositional solver backend + /// \param _message_handler: message handler for logging + /// \param _get_constraints: when true, collect and display constraint + /// statistics after eager conversion mapst( const namespacet &_ns, propt &_prop, @@ -36,45 +46,80 @@ class mapst : public equalityt ~mapst() override = default; - // -- Pure virtual: implemented by arrayst -- + /// Record that two map expressions are equal and return a literal + /// representing that equality. Implemented by \ref arrayst. virtual literalt record_equality(const equal_exprt &expr) = 0; + + /// Record that \p s is a let-bound alias for \p v. For map-typed bindings + /// this connects the two expressions in the union-find so that element-wise + /// constraints propagate correctly. Implemented by \ref arrayst. virtual void record_let_binding(const symbol_exprt &s, const exprt &v) = 0; - // -- Virtual: default in mapst, may be overridden -- + /// Register a key expression (an index into a map) so that the map theory + /// generates the appropriate read-over-write and Ackermann constraints for + /// it. The key is recorded against the map's equivalence-class + /// representative in \ref domain_map. virtual void record_key(const index_exprt &expr); protected: const namespacet &ns; messaget log; - // -- Map equality tracking -- + /// Tracks an equality between two map expressions together with the + /// propositional literal that represents it. struct map_equalityt { literalt l; exprt f1, f2; }; typedef std::list map_equalitiest; + /// All recorded map equalities. Uses a list so that references remain + /// stable as new equalities are added. map_equalitiest map_equalities; - // -- Maps union-find -- + /// Union-find grouping map expressions into equivalence classes. union_find maps; - // -- Key tracking -- typedef std::set key_sett; typedef std::map domain_mapt; + /// Maps each equivalence-class number to the set of keys (index + /// expressions) that have been observed for that class. domain_mapt domain_map; + /// Equivalence-class numbers whose key sets have been modified since the + /// last call to \ref update_domain_map. std::set update_keys; + /// Identifiers of array-comprehension bound variables, used to avoid + /// recording comprehension parameters as concrete keys. std::unordered_set array_comprehension_args; + /// Walk every map expression in \ref maps and collect all keys that appear + /// in sub-expressions. void collect_keys(); + + /// Recursively collect keys from the sub-expressions of \p a. + /// \param a: expression to scan for index sub-expressions void collect_keys(const exprt &a); + + /// Recursively traverse a map expression \p a, unifying it with its + /// sub-maps in the union-find and recording any keys that appear. + /// \param a: a map-typed expression (with, if, update, typecast, …) virtual void collect_maps(const exprt &a); + + /// Merge key sets of non-root equivalence classes into their roots. + /// When \p update_all is true every class is processed; otherwise only + /// the classes listed in \ref update_keys are processed. + /// \param update_all: if true, process all classes; otherwise only dirty ones void update_domain_map(bool update_all); + + /// Merge the key set of equivalence class \p i into its root's key set. + /// \param i: equivalence-class number to merge void update_domain_map(std::size_t i); + /// Return true if \p type is an unbounded (variable-length) map type. + /// Implemented by the derived class. virtual bool is_unbounded_map(const typet &type) const = 0; - // -- Lazy constraint management -- + /// Classification of lazily deferred constraints. enum class lazy_typet { MAP_ACKERMANN, @@ -87,6 +132,7 @@ class mapst : public equalityt MAP_LET }; + /// A constraint together with its classification, used for lazy dispatch. struct lazy_constraintt { lazy_typet type; @@ -98,21 +144,41 @@ class mapst : public equalityt } }; + /// Constraints that have been deferred for later refinement. std::list lazy_constraints; + /// When true, constraints passed to \ref add_map_constraint with + /// refine=true are deferred rather than added eagerly. bool lazy_dispatch; + /// When true, duplicate lazy constraints are suppressed via \ref expr_map. bool incremental_cache; + /// When true, constraint statistics are collected and displayed after + /// eager conversion. bool get_constraints; + /// Cache used by incremental mode to suppress duplicate lazy constraints. std::map expr_map; + /// Add a map-theory constraint. When \ref lazy_dispatch is true and + /// \p refine is true the constraint is deferred; otherwise it is + /// converted and asserted immediately. + /// \param lazy: the constraint to add + /// \param refine: if true and lazy mode is active, defer the constraint void add_map_constraint(const lazy_constraintt &lazy, bool refine = true); - // -- Ackermann constraints -- + /// Add Ackermann constraints for every pair of keys in each equivalence + /// class: if two keys are equal then the corresponding map lookups must + /// yield equal values. Complexity is quadratic in the size of each key + /// set. void add_Ackermann_constraints(); + + /// For a recorded map equality f1 = f2, add element-wise constraints + /// f1[k] = f2[k] for every key k in \p key_set. + /// \param key_set: the set of keys to instantiate + /// \param equality: the map equality whose literal guards the constraints void add_map_equality_constraints( const key_sett &key_set, const map_equalityt &equality); - // -- Constraint counting -- + /// Classification of constraints for statistics reporting. enum class constraint_typet { MAP_ACKERMANN, @@ -126,11 +192,17 @@ class mapst : public equalityt MAP_LET }; typedef std::map map_constraint_countt; + /// Per-type constraint counts, populated when \ref get_constraints is true. map_constraint_countt constraint_count; + + /// Return a human-readable string for a constraint type enum value. std::string enum_to_string(constraint_typet type); + + /// Emit the collected constraint counts as a JSON object to the status log. void display_constraint_count(); - // -- Eager conversion -- + /// Finish eager conversion: first convert maps, then equalities, then + /// optionally display constraint statistics. void finish_eager_conversion() override { finish_eager_conversion_maps(); @@ -139,6 +211,8 @@ class mapst : public equalityt display_constraint_count(); } + /// Collect all keys and build the initial domain map. Overridden by + /// \ref arrayst to also add array-specific constraints. virtual void finish_eager_conversion_maps() { collect_keys(); From 90cf83759956f35b4324f9ed7e362eb22f086ab5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 May 2026 08:56:13 +0000 Subject: [PATCH 4/6] Move is_unbounded_array and collect_keys from mapst to arrayst A map is unbounded by definition; the unboundedness check that the prior commits called 'is_unbounded_map' actually distinguishes between arrays the array theory should manage and bounded arrays that the flattening layer bit-blasts directly. That distinction is array- specific and has no place on a mapst base. Rename the method back to 'is_unbounded_array' and move both its declaration and its only override down to arrayst / boolbvt. The same applies to 'collect_keys': it walks an expression looking specifically for 'index_exprt' over array_typet operands, tracks 'array_comprehension_args' for ID_array_comprehension, and uses 'is_unbounded_array' to decide whether to record the index. None of that is map-theoretic. Move both overloads of 'collect_keys' (and 'array_comprehension_args') from mapst to arrayst. The remaining mapst primitives ('record_key', 'update_domain_map', 'add_Ackermann_constraints', 'add_map_equality_constraints') stay where they are: they are genuinely about maps (key sets, equivalence classes, Ackermann implications) and do not depend on array shape. Side-effect: 'finish_eager_conversion_maps' becomes pure virtual on mapst, since its previous default body called the now-moved 'collect_keys'. Both existing overrides ('arrayst::add_array_constraints' and 'bv_refinementt::finish_eager_conversion_maps') already provided their own implementation, so no caller is affected. Co-authored-by: Kiro --- src/solvers/flattening/arrays.cpp | 47 +++++++++++++++++++ src/solvers/flattening/arrays.h | 21 +++++++++ src/solvers/flattening/boolbv.cpp | 4 +- src/solvers/flattening/boolbv.h | 2 +- src/solvers/flattening/boolbv_array_of.cpp | 2 +- .../flattening/boolbv_byte_extract.cpp | 2 +- src/solvers/flattening/boolbv_byte_update.cpp | 37 ++++++++------- src/solvers/flattening/boolbv_equality.cpp | 2 +- src/solvers/flattening/boolbv_get.cpp | 2 +- src/solvers/flattening/boolbv_index.cpp | 2 +- src/solvers/flattening/boolbv_let.cpp | 2 +- src/solvers/flattening/boolbv_with.cpp | 2 +- src/solvers/flattening/maps.cpp | 47 ------------------- src/solvers/flattening/maps.h | 28 +++-------- 14 files changed, 103 insertions(+), 97 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index bf19ebd3140..ac228936bec 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -73,6 +73,53 @@ void arrayst::record_let_binding(const symbol_exprt &symbol, const exprt &value) prop.l_set_to_true(eq_lit); } +void arrayst::collect_keys() +{ + for(std::size_t i = 0; i < maps.size(); i++) + { + collect_keys(maps[i]); + } +} + +void arrayst::collect_keys(const exprt &expr) +{ + if(expr.id() != ID_index) + { + if(expr.id() == ID_array_comprehension) + array_comprehension_args.insert( + to_array_comprehension_expr(expr).arg().get_identifier()); + + for(const auto &op : expr.operands()) + collect_keys(op); + } + else + { + const index_exprt &e = to_index_expr(expr); + + if( + e.index().id() == ID_symbol && + array_comprehension_args.count( + to_symbol_expr(e.index()).get_identifier()) != 0) + { + return; + } + + collect_keys(e.index()); // necessary? + + const typet &array_op_type = e.array().type(); + + if(array_op_type.id() == ID_array) + { + const array_typet &array_type = to_array_type(array_op_type); + + if(is_unbounded_array(array_type)) + { + record_key(e); + } + } + } +} + void arrayst::add_array_constraints() { collect_keys(); diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index f7f2a0d6ad4..e7d236ba8b6 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "maps.h" +#include + class array_comprehension_exprt; class array_exprt; class array_of_exprt; @@ -49,6 +51,25 @@ class arrayst : public mapst protected: message_handlert &message_handler; + /// Identifiers of array-comprehension bound variables, used to avoid + /// recording comprehension parameters as concrete keys. + std::unordered_set array_comprehension_args; + + /// Walk every map expression in \ref maps and collect all keys that appear + /// in sub-expressions. + void collect_keys(); + + /// Recursively collect keys from the sub-expressions of \p a. + /// \param a: expression to scan for index sub-expressions + void collect_keys(const exprt &a); + + /// Return true if \p type is an unbounded (variable-length) array type. + /// Implemented by the derived class \ref boolbvt. A map is unbounded by + /// definition; this hook is only meaningful for arrays, where bounded + /// (fixed-size) instances are bit-blasted directly without going through + /// the array theory. + virtual bool is_unbounded_array(const typet &type) const = 0; + void finish_eager_conversion_maps() override { add_array_constraints(); diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 522f7e64181..bdeb176dd8f 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -511,7 +511,7 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) type.id() != ID_bool) { // see if it is an unbounded array - if(is_unbounded_map(type)) + if(is_unbounded_array(type)) return true; const bvt &bv1=convert_bv(expr.rhs()); @@ -539,7 +539,7 @@ void boolbvt::set_to(const exprt &expr, bool value) SUB::set_to(expr, value); } -bool boolbvt::is_unbounded_map(const typet &type) const +bool boolbvt::is_unbounded_array(const typet &type) const { if(type.id()!=ID_array) return false; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 2f9890db39b..324124d0172 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -267,7 +267,7 @@ class boolbvt:public arrayst exprt get_value(const exprt &expr) const; // unbounded arrays - bool is_unbounded_map(const typet &type) const override; + bool is_unbounded_array(const typet &type) const override; // quantifier instantiations class quantifiert diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp index 66066bf6f8a..7a2ba2fa6f6 100644 --- a/src/solvers/flattening/boolbv_array_of.cpp +++ b/src/solvers/flattening/boolbv_array_of.cpp @@ -20,7 +20,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr) const array_typet &array_type = expr.type(); - if(is_unbounded_map(array_type)) + if(is_unbounded_array(array_type)) return conversion_failed(expr); std::size_t width=boolbv_width(array_type); diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 6b531f301c5..01cb688063f 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -34,7 +34,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) { // array logic does not handle byte operators, thus lower when operating on // unbounded arrays - if(is_unbounded_map(expr.op().type())) + if(is_unbounded_array(expr.op().type())) { return convert_bv(lower_byte_extract(expr, ns)); } diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index d06556a0f8a..d5b5c468c82 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -6,39 +6,40 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "boolbv.h" - #include #include #include +#include "boolbv.h" + bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) { // if we update (from) an unbounded array, lower the expression as the array // logic does not handle byte operators if( - is_unbounded_map(expr.op().type()) || is_unbounded_map(expr.value().type())) + is_unbounded_array(expr.op().type()) || + is_unbounded_array(expr.value().type())) { return convert_bv(lower_byte_update(expr, ns)); } const exprt &op = expr.op(); - const exprt &offset_expr=expr.offset(); - const exprt &value=expr.value(); + const exprt &offset_expr = expr.offset(); + const exprt &value = expr.value(); PRECONDITION( expr.id() == ID_byte_update_little_endian || expr.id() == ID_byte_update_big_endian); const bool little_endian = expr.id() == ID_byte_update_little_endian; - bvt bv=convert_bv(op); + bvt bv = convert_bv(op); - const bvt &value_bv=convert_bv(value); - std::size_t update_width=value_bv.size(); + const bvt &value_bv = convert_bv(value); + std::size_t update_width = value_bv.size(); std::size_t byte_width = expr.get_bits_per_byte(); - if(update_width>bv.size()) - update_width=bv.size(); + if(update_width > bv.size()) + update_width = bv.size(); // see if the byte number is constant @@ -48,7 +49,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) // yes! const mp_integer offset = *index * byte_width; - if(offset+update_width>mp_integer(bv.size()) || offset<0) + if(offset + update_width > mp_integer(bv.size()) || offset < 0) { // out of bounds } @@ -78,23 +79,23 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) } // byte_update with variable index - for(std::size_t offset=0; offset update_keys; - /// Identifiers of array-comprehension bound variables, used to avoid - /// recording comprehension parameters as concrete keys. - std::unordered_set array_comprehension_args; - - /// Walk every map expression in \ref maps and collect all keys that appear - /// in sub-expressions. - void collect_keys(); - - /// Recursively collect keys from the sub-expressions of \p a. - /// \param a: expression to scan for index sub-expressions - void collect_keys(const exprt &a); /// Recursively traverse a map expression \p a, unifying it with its /// sub-maps in the union-find and recording any keys that appear. @@ -115,10 +104,6 @@ class mapst : public equalityt /// \param i: equivalence-class number to merge void update_domain_map(std::size_t i); - /// Return true if \p type is an unbounded (variable-length) map type. - /// Implemented by the derived class. - virtual bool is_unbounded_map(const typet &type) const = 0; - /// Classification of lazily deferred constraints. enum class lazy_typet { @@ -211,13 +196,12 @@ class mapst : public equalityt display_constraint_count(); } - /// Collect all keys and build the initial domain map. Overridden by - /// \ref arrayst to also add array-specific constraints. - virtual void finish_eager_conversion_maps() - { - collect_keys(); - update_domain_map(true); - } + /// Collect all keys, build the initial domain map, and add any + /// theory-specific constraints. The default of "collect_keys then + /// update_domain_map" cannot live here anymore because key collection is + /// theory-specific (e.g. \ref arrayst skips bounded-array operands), so + /// derived classes are required to provide their own implementation. + virtual void finish_eager_conversion_maps() = 0; }; #endif // CPROVER_SOLVERS_FLATTENING_MAPS_H From 01b69b6004e7a12af9d91844405a93fa574975e4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 May 2026 09:06:23 +0000 Subject: [PATCH 5/6] mapst / arrayst: cleanups, renames, dead-code removal Mechanical, behaviour-preserving tidying of the new mapst class and its arrayst subclass: * Drop dead arrayst::message_handler member. The base equalityt already takes a message_handler via the messaget log, so storing it again on arrayst was redundant; nothing read the field. * Drop dead incremental_cache flag and the expr_map cache it guarded. No code path ever set incremental_cache to true, so the cache was unused. * Fix typo 'contraint_type_string' -> 'constraint_type_string' in display_constraint_count. * Align maps.cpp's author tag with maps.h (Michael Tautschnig). The .cpp file was extracted in this PR; the leftover Daniel Kroening tag came from the arrays.cpp ancestry. * Add explicit '#include ' to maps.h. domain_mapt and map_constraint_countt are std::map aliases; the include only came in transitively via util/union_find.h. * Drop spurious 'virtual' on record_key and collect_maps. Neither is overridden in any subclass (arrayst doesn't override either), so the keyword is misleading and prevents devirtualisation. * Rename 'update_keys' -> 'dirty_classes'. The set holds equivalence-class numbers (returned by union_find::number()), not keys; the original 'update_indices' had the same flaw and the rename in this PR was the chance to fix it. * Rename 'lazy_dispatch' -> 'defer_constraints'. The boolean controls whether refine=true constraints passed to add_map_constraint are deferred for the refinement loop; 'defer_constraints' makes that role obvious at the call sites. * Rename '_get_constraints' / 'get_constraints' constructor parameter and member to 'collect_constraint_stats'. The old name read like a getter and clashed visually with the neighbouring 'constraint_count'. Propagated through arrayst, boolbvt, bv_pointerst, bv_pointers_widet, and the one solver_factoryt call site that still used the old 'get_array_constraints' shape. Co-authored-by: Kiro --- src/cprover/bv_pointers_wide.cpp | 4 +-- src/cprover/bv_pointers_wide.h | 2 +- src/goto-checker/solver_factory.cpp | 4 +-- src/solvers/flattening/arrays.cpp | 7 +++-- src/solvers/flattening/arrays.h | 4 +-- src/solvers/flattening/boolbv.h | 4 +-- src/solvers/flattening/bv_pointers.cpp | 5 ++-- src/solvers/flattening/bv_pointers.h | 2 +- src/solvers/flattening/maps.cpp | 34 ++++++++---------------- src/solvers/flattening/maps.h | 31 ++++++++++----------- src/solvers/refinement/refine_arrays.cpp | 4 +-- 11 files changed, 42 insertions(+), 59 deletions(-) diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index bb9e01dc6de..95473226739 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -155,8 +155,8 @@ bv_pointers_widet::bv_pointers_widet( const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_array_constraints) - : boolbvt(_ns, _prop, message_handler, get_array_constraints), + bool collect_constraint_stats) + : boolbvt(_ns, _prop, message_handler, collect_constraint_stats), pointer_logic(_ns) { } diff --git a/src/cprover/bv_pointers_wide.h b/src/cprover/bv_pointers_wide.h index 1c1f0be60fb..02359d5edb2 100644 --- a/src/cprover/bv_pointers_wide.h +++ b/src/cprover/bv_pointers_wide.h @@ -23,7 +23,7 @@ class bv_pointers_widet : public boolbvt const namespacet &, propt &, message_handlert &, - bool get_array_constraints = false); + bool collect_constraint_stats = false); void finish_eager_conversion() override; diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 3e18d046812..80bbd6070e0 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -356,10 +356,10 @@ std::unique_ptr solver_factoryt::get_default() { auto sat_solver = get_sat_solver(message_handler, options); - bool get_array_constraints = + bool collect_constraint_stats = options.get_bool_option("show-array-constraints"); auto bv_pointers = std::make_unique( - ns, *sat_solver, message_handler, get_array_constraints); + ns, *sat_solver, message_handler, collect_constraint_stats); if(options.get_option("arrays-uf") == "never") bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE; diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index ac228936bec..3483aa7c1c1 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -29,9 +29,8 @@ arrayst::arrayst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_constraints) - : mapst(_ns, _prop, _message_handler, _get_constraints), - message_handler(_message_handler) + bool _collect_constraint_stats) + : mapst(_ns, _prop, _message_handler, _collect_constraint_stats) { } @@ -147,7 +146,7 @@ void arrayst::add_array_constraints() add_array_constraints(domain_map[maps.find_number(i)], a); // we have to update before it gets used in the next add_* call - for(const std::size_t u : update_keys) + for(const std::size_t u : dirty_classes) updated_roots.insert(maps.find_number(u)); update_domain_map(false); } diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index e7d236ba8b6..43e7949b140 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -32,7 +32,7 @@ class arrayst : public mapst const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_constraints = false); + bool collect_constraint_stats = false); // NOLINTNEXTLINE(readability/identifiers) typedef mapst SUB; @@ -49,8 +49,6 @@ class arrayst : public mapst record_let_binding(const symbol_exprt &symbol, const exprt &value) override; protected: - message_handlert &message_handler; - /// Identifiers of array-comprehension bound variables, used to avoid /// recording comprehension parameters as concrete keys. std::unordered_set array_comprehension_args; diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 324124d0172..ababbe9e750 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -53,8 +53,8 @@ class boolbvt:public arrayst const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_constraints = false) - : arrayst(_ns, _prop, message_handler, get_constraints), + bool collect_constraint_stats = false) + : arrayst(_ns, _prop, message_handler, collect_constraint_stats), unbounded_array(unbounded_arrayt::U_NONE), bv_width(_ns), bv_utils(_prop), diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index fdcbdb9279c..66b0bc13852 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -228,8 +228,9 @@ bv_pointerst::bv_pointerst( const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_constraints) - : boolbvt(_ns, _prop, message_handler, get_constraints), pointer_logic(_ns) + bool collect_constraint_stats) + : boolbvt(_ns, _prop, message_handler, collect_constraint_stats), + pointer_logic(_ns) { } diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 5b3b669e2e4..f70f30862b3 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -20,7 +20,7 @@ class bv_pointerst:public boolbvt const namespacet &, propt &, message_handlert &, - bool get_constraints = false); + bool collect_constraint_stats = false); void finish_eager_conversion() override; diff --git a/src/solvers/flattening/maps.cpp b/src/solvers/flattening/maps.cpp index 4ae32815255..13a8ec44bb0 100644 --- a/src/solvers/flattening/maps.cpp +++ b/src/solvers/flattening/maps.cpp @@ -2,7 +2,7 @@ Module: Map Theory (base class for array theory) -Author: Daniel Kroening, kroening@kroening.com +Author: Michael Tautschnig \*******************************************************************/ @@ -27,13 +27,12 @@ mapst::mapst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_constraints) + bool _collect_constraint_stats) : equalityt(_prop, _message_handler), ns(_ns), log(_message_handler), - lazy_dispatch(false), - incremental_cache(false), - get_constraints(_get_constraints) + defer_constraints(false), + collect_constraint_stats(_collect_constraint_stats) { } @@ -44,7 +43,7 @@ void mapst::record_key(const index_exprt &index) // because this map is accessed during building the error trace std::size_t number = maps.number(index.array()); if(domain_map[number].insert(index.index()).second) - update_keys.insert(number); + dirty_classes.insert(number); } void mapst::collect_maps(const exprt &a) @@ -168,21 +167,10 @@ void mapst::collect_maps(const exprt &a) /// adds map constraints (refine=true...lazily for the refinement loop) void mapst::add_map_constraint(const lazy_constraintt &lazy, bool refine) { - if(lazy_dispatch && refine) + if(defer_constraints && refine) { // lazily add the constraint - if(incremental_cache) - { - if(expr_map.find(lazy.lazy) == expr_map.end()) - { - lazy_constraints.push_back(lazy); - expr_map[lazy.lazy] = true; - } - } - else - { - lazy_constraints.push_back(lazy); - } + lazy_constraints.push_back(lazy); } else { @@ -279,10 +267,10 @@ void mapst::update_domain_map(bool update_all) } else { - for(const auto &key : update_keys) + for(const auto &key : dirty_classes) update_domain_map(key); - update_keys.clear(); + dirty_classes.clear(); } #ifdef DEBUG @@ -375,8 +363,8 @@ void mapst::display_constraint_count() map_constraint_countt::iterator it = constraint_count.begin(); while(it != constraint_count.end()) { - std::string contraint_type_string = enum_to_string(it->first); - json_array_theory[contraint_type_string] = + std::string constraint_type_string = enum_to_string(it->first); + json_array_theory[constraint_type_string] = json_numbert(std::to_string(it->second)); num_constraints += it->second; diff --git a/src/solvers/flattening/maps.h b/src/solvers/flattening/maps.h index 974c7a52ee4..862967f45c9 100644 --- a/src/solvers/flattening/maps.h +++ b/src/solvers/flattening/maps.h @@ -18,8 +18,8 @@ Author: Michael Tautschnig #include "equality.h" #include +#include #include -#include class equal_exprt; class index_exprt; @@ -36,13 +36,13 @@ class mapst : public equalityt /// \param _ns: namespace for type lookups /// \param _prop: propositional solver backend /// \param _message_handler: message handler for logging - /// \param _get_constraints: when true, collect and display constraint - /// statistics after eager conversion + /// \param _collect_constraint_stats: when true, collect and display + /// constraint statistics after eager conversion mapst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_constraints = false); + bool _collect_constraint_stats = false); ~mapst() override = default; @@ -59,7 +59,7 @@ class mapst : public equalityt /// generates the appropriate read-over-write and Ackermann constraints for /// it. The key is recorded against the map's equivalence-class /// representative in \ref domain_map. - virtual void record_key(const index_exprt &expr); + void record_key(const index_exprt &expr); protected: const namespacet &ns; @@ -87,16 +87,16 @@ class mapst : public equalityt domain_mapt domain_map; /// Equivalence-class numbers whose key sets have been modified since the /// last call to \ref update_domain_map. - std::set update_keys; + std::set dirty_classes; /// Recursively traverse a map expression \p a, unifying it with its /// sub-maps in the union-find and recording any keys that appear. /// \param a: a map-typed expression (with, if, update, typecast, …) - virtual void collect_maps(const exprt &a); + void collect_maps(const exprt &a); /// Merge key sets of non-root equivalence classes into their roots. /// When \p update_all is true every class is processed; otherwise only - /// the classes listed in \ref update_keys are processed. + /// the classes listed in \ref dirty_classes are processed. /// \param update_all: if true, process all classes; otherwise only dirty ones void update_domain_map(bool update_all); @@ -133,16 +133,12 @@ class mapst : public equalityt std::list lazy_constraints; /// When true, constraints passed to \ref add_map_constraint with /// refine=true are deferred rather than added eagerly. - bool lazy_dispatch; - /// When true, duplicate lazy constraints are suppressed via \ref expr_map. - bool incremental_cache; + bool defer_constraints; /// When true, constraint statistics are collected and displayed after /// eager conversion. - bool get_constraints; - /// Cache used by incremental mode to suppress duplicate lazy constraints. - std::map expr_map; + bool collect_constraint_stats; - /// Add a map-theory constraint. When \ref lazy_dispatch is true and + /// Add a map-theory constraint. When \ref defer_constraints is true and /// \p refine is true the constraint is deferred; otherwise it is /// converted and asserted immediately. /// \param lazy: the constraint to add @@ -177,7 +173,8 @@ class mapst : public equalityt MAP_LET }; typedef std::map map_constraint_countt; - /// Per-type constraint counts, populated when \ref get_constraints is true. + /// Per-type constraint counts, populated when \ref collect_constraint_stats + /// is true. map_constraint_countt constraint_count; /// Return a human-readable string for a constraint type enum value. @@ -192,7 +189,7 @@ class mapst : public equalityt { finish_eager_conversion_maps(); equalityt::finish_eager_conversion(); - if(get_constraints) + if(collect_constraint_stats) display_constraint_count(); } diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index 809601077d4..87804b5255b 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -27,7 +27,7 @@ void bv_refinementt::finish_eager_conversion_maps() update_domain_map(true); // we don't actually add any constraints - lazy_dispatch = config_.refine_arrays; + defer_constraints = config_.refine_arrays; add_array_constraints(); freeze_lazy_constraints(); } @@ -122,7 +122,7 @@ void bv_refinementt::arrays_overapproximated() /// freeze symbols for incremental solving void bv_refinementt::freeze_lazy_constraints() { - if(!lazy_dispatch) + if(!defer_constraints) return; for(const auto &constraint : lazy_constraints) From 62919826a7ca213959db2230bbf7e15bb943686b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 May 2026 09:24:38 +0000 Subject: [PATCH 6/6] Consolidate lazy_typet and constraint_typet into map_constraint_kindt MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The two parallel enums on mapst — lazy_typet (used to classify deferred constraints in the refinement loop) and constraint_typet (used for per-kind statistics in --show-array-constraints) — were near-duplicates, differing only by the additional MAP_EQUALITY entry in constraint_typet. Maintaining them in lock-step invited forgotten-tag bugs, and every constraint-adding call site had to mention both names: lazy_constraintt lazy(lazy_typet::MAP_X, body); add_map_constraint(lazy, refine); ++constraint_count[constraint_typet::MAP_X]; Replace both with a single map_constraint_kindt enum that carries all nine kinds (MAP_EQUALITY is never enqueued lazily, but having it in the same enum is harmless because lazy enqueueing is decided per add_map_constraint call, not per enum value). Add an inline helper void add_constraint( map_constraint_kindt kind, const exprt &body, bool refine = false); that does the lazy_constraintt construction, the add_map_constraint call, and the constraint_count bump in one go. Rewrite the eleven call sites (ten in arrays.cpp's add_array_constraints_* helpers, plus the Ackermann site in maps.cpp::add_Ackermann_constraints) to use it. The MAP_EQUALITY counter in add_map_equality_constraints stays as a direct constraint_count[]++ because that constraint is asserted via prop.lcnf, not via add_map_constraint. Net result: one enum to keep in sync, one call per constraint site, and ~30 lines saved across the refactored files. The user-visible JSON output of '--show-array-constraints' is unaffected: enum_to_string still maps MAP_X to 'arrayX' strings. Co-authored-by: Kiro --- src/solvers/flattening/arrays.cpp | 94 ++++++++++++------------------- src/solvers/flattening/maps.cpp | 31 +++++----- src/solvers/flattening/maps.h | 47 +++++++++------- 3 files changed, 79 insertions(+), 93 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 3483aa7c1c1..ec63568f250 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -36,8 +36,8 @@ arrayst::arrayst( literalt arrayst::record_equality(const equal_exprt &equality) { - const exprt &op0=equality.op0(); - const exprt &op1=equality.op1(); + const exprt &op0 = equality.op0(); + const exprt &op1 = equality.op1(); DATA_INVARIANT_WITH_DIAGNOSTICS( op0.type() == op1.type(), @@ -170,13 +170,13 @@ void arrayst::add_array_constraints() void arrayst::add_array_constraints(const key_sett &key_set, const exprt &expr) { - if(expr.id()==ID_with) + if(expr.id() == ID_with) return add_array_constraints_with(key_set, to_with_expr(expr)); - else if(expr.id()==ID_update) + else if(expr.id() == ID_update) return add_array_constraints_update(key_set, to_update_expr(expr)); - else if(expr.id()==ID_if) + else if(expr.id() == ID_if) return add_array_constraints_if(key_set, to_if_expr(expr)); - else if(expr.id()==ID_array_of) + else if(expr.id() == ID_array_of) return add_array_constraints_array_of(key_set, to_array_of_expr(expr)); else if(expr.id() == ID_array) return add_array_constraints_array_constant(key_set, to_array_expr(expr)); @@ -197,12 +197,13 @@ void arrayst::add_array_constraints(const key_sett &key_set, const exprt &expr) to_member_expr(expr).struct_op().id() == ID_nondet_symbol)) { } - else if(expr.id()==ID_byte_update_little_endian || - expr.id()==ID_byte_update_big_endian) + else if( + expr.id() == ID_byte_update_little_endian || + expr.id() == ID_byte_update_big_endian) { INVARIANT(false, "byte_update should be removed before arrayst"); } - else if(expr.id()==ID_typecast) + else if(expr.id() == ID_typecast) { // we got a=(type[])b const auto &expr_typecast_op = to_typecast_expr(expr).op(); @@ -215,17 +216,16 @@ void arrayst::add_array_constraints(const key_sett &key_set, const exprt &expr) index_exprt index_expr2(expr_typecast_op, key, element_type); DATA_INVARIANT( - index_expr1.type()==index_expr2.type(), + index_expr1.type() == index_expr2.type(), "array elements should all have same type"); // add constraint - lazy_constraintt lazy( - lazy_typet::MAP_TYPECAST, equal_exprt(index_expr1, index_expr2)); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_TYPECAST]++; + add_constraint( + map_constraint_kindt::MAP_TYPECAST, + equal_exprt(index_expr1, index_expr2)); } } - else if(expr.id()==ID_index) + else if(expr.id() == ID_index) { } else if(auto let_expr = expr_try_dynamic_cast(expr)) @@ -248,11 +248,8 @@ void arrayst::add_array_constraints(const key_sett &key_set, const exprt &expr) index_exprt where_indexed{where, key}; // add constraint - lazy_constraintt lazy{ - lazy_typet::MAP_LET, equal_exprt{index_expr, where_indexed}}; - - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_LET]++; + add_constraint( + map_constraint_kindt::MAP_LET, equal_exprt{index_expr, where_indexed}); } } else @@ -280,10 +277,8 @@ void arrayst::add_array_constraints_with( "with-expression operand should match array element type", irep_pretty_diagnosticst{expr}); - lazy_constraintt lazy( - lazy_typet::MAP_WITH, equal_exprt(index_expr, expr.new_value())); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_WITH]++; + add_constraint( + map_constraint_kindt::MAP_WITH, equal_exprt(index_expr, expr.new_value())); updated_keys.insert(expr.where()); @@ -306,7 +301,7 @@ void arrayst::add_array_constraints_with( literalt guard_lit = convert(disjunction(disjuncts)); - if(guard_lit!=const_literal(true)) + if(guard_lit != const_literal(true)) { const typet &element_type = to_array_type(expr.type()).element_type(); index_exprt index_expr1(expr, other_key, element_type); @@ -315,13 +310,10 @@ void arrayst::add_array_constraints_with( equal_exprt equality_expr(index_expr1, index_expr2); // add constraint - lazy_constraintt lazy( - lazy_typet::MAP_WITH, + add_constraint( + map_constraint_kindt::MAP_WITH, or_exprt(equality_expr, literal_exprt(guard_lit))); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_WITH]++; - #if 0 // old code for adding, not significantly faster { literalt equality_lit=convert(equality_expr); @@ -413,10 +405,8 @@ void arrayst::add_array_constraints_array_of( "array_of operand type should match array element type"); // add constraint - lazy_constraintt lazy( - lazy_typet::MAP_OF, equal_exprt(index_expr, expr.what())); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_OF]++; + add_constraint( + map_constraint_kindt::MAP_OF, equal_exprt(index_expr, expr.what())); } } @@ -449,10 +439,8 @@ void arrayst::add_array_constraints_array_constant( "array operand type should match array element type"); // add constraint - lazy_constraintt lazy{ - lazy_typet::MAP_CONSTANT, equal_exprt{index_expr, v}}; - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_CONSTANT]++; + add_constraint( + map_constraint_kindt::MAP_CONSTANT, equal_exprt{index_expr, v}); } else { @@ -490,12 +478,11 @@ void arrayst::add_array_constraints_array_constant( key, ID_le, from_integer(range.second, key.type())}}; } - lazy_constraintt lazy{ - lazy_typet::MAP_CONSTANT, + add_constraint( + map_constraint_kindt::MAP_CONSTANT, implies_exprt{ - index_constraint, equal_exprt{index_expr, operands[range.first]}}}; - add_map_constraint(lazy, true); // added lazily - constraint_count[constraint_typet::MAP_CONSTANT]++; + index_constraint, equal_exprt{index_expr, operands[range.first]}}, + true); // added lazily } } } @@ -516,12 +503,9 @@ void arrayst::add_array_constraints_comprehension( replace_expr(expr.arg(), key, comprehension_body); // add constraint - lazy_constraintt lazy( - lazy_typet::MAP_COMPREHENSION, + add_constraint( + map_constraint_kindt::MAP_COMPREHENSION, equal_exprt(index_expr, comprehension_body)); - - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_COMPREHENSION]++; } } @@ -530,7 +514,7 @@ void arrayst::add_array_constraints_if( const if_exprt &expr) { // we got x=(c?a:b) - literalt cond_lit=convert(expr.cond()); + literalt cond_lit = convert(expr.cond()); // get other array index applications // and add c => x[i]=a[i] @@ -545,12 +529,10 @@ void arrayst::add_array_constraints_if( index_exprt index_expr2(expr.true_case(), key, element_type); // add implication - lazy_constraintt lazy( - lazy_typet::MAP_IF, + add_constraint( + map_constraint_kindt::MAP_IF, or_exprt( literal_exprt(!cond_lit), equal_exprt(index_expr1, index_expr2))); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2))); @@ -565,11 +547,9 @@ void arrayst::add_array_constraints_if( index_exprt index_expr2(expr.false_case(), key, element_type); // add implication - lazy_constraintt lazy( - lazy_typet::MAP_IF, + add_constraint( + map_constraint_kindt::MAP_IF, or_exprt(literal_exprt(cond_lit), equal_exprt(index_expr1, index_expr2))); - add_map_constraint(lazy, false); // added immediately - constraint_count[constraint_typet::MAP_IF]++; #if 0 // old code for adding, not significantly faster prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2))); diff --git a/src/solvers/flattening/maps.cpp b/src/solvers/flattening/maps.cpp index 13a8ec44bb0..1cd6a78aecb 100644 --- a/src/solvers/flattening/maps.cpp +++ b/src/solvers/flattening/maps.cpp @@ -222,11 +222,10 @@ void mapst::add_Ackermann_constraints() equal_exprt values_equal(index_expr1, index_expr2); // add constraint - lazy_constraintt lazy( - lazy_typet::MAP_ACKERMANN, - implies_exprt(literal_exprt(indices_equal_lit), values_equal)); - add_map_constraint(lazy, true); // added lazily - constraint_count[constraint_typet::MAP_ACKERMANN]++; + add_constraint( + map_constraint_kindt::MAP_ACKERMANN, + implies_exprt(literal_exprt(indices_equal_lit), values_equal), + true); // added lazily #if 0 // old code for adding, not significantly faster prop.lcnf(!indices_equal_lit, convert(values_equal)); @@ -315,11 +314,11 @@ void mapst::add_map_equality_constraints( // equality constraints are not added lazily // convert must be done to guarantee correct update of the key_set prop.lcnf(!equality.l, convert(equality_expr)); - constraint_count[constraint_typet::MAP_EQUALITY]++; + constraint_count[map_constraint_kindt::MAP_EQUALITY]++; } } -std::string mapst::enum_to_string(constraint_typet type) +std::string mapst::enum_to_string(map_constraint_kindt type) { // The internal enum tags are MAP_X, but the JSON strings are kept as // arrayX/arrayConstraints because the constraints reported by @@ -329,23 +328,23 @@ std::string mapst::enum_to_string(constraint_typet type) // consumers of --show-array-constraints --json-ui output. switch(type) { - case constraint_typet::MAP_ACKERMANN: + case map_constraint_kindt::MAP_ACKERMANN: return "arrayAckermann"; - case constraint_typet::MAP_WITH: + case map_constraint_kindt::MAP_WITH: return "arrayWith"; - case constraint_typet::MAP_IF: + case map_constraint_kindt::MAP_IF: return "arrayIf"; - case constraint_typet::MAP_OF: + case map_constraint_kindt::MAP_OF: return "arrayOf"; - case constraint_typet::MAP_TYPECAST: + case map_constraint_kindt::MAP_TYPECAST: return "arrayTypecast"; - case constraint_typet::MAP_CONSTANT: + case map_constraint_kindt::MAP_CONSTANT: return "arrayConstant"; - case constraint_typet::MAP_COMPREHENSION: + case map_constraint_kindt::MAP_COMPREHENSION: return "arrayComprehension"; - case constraint_typet::MAP_EQUALITY: + case map_constraint_kindt::MAP_EQUALITY: return "arrayEquality"; - case constraint_typet::MAP_LET: + case map_constraint_kindt::MAP_LET: return "arrayLet"; default: UNREACHABLE; diff --git a/src/solvers/flattening/maps.h b/src/solvers/flattening/maps.h index 862967f45c9..cc3640a5b4b 100644 --- a/src/solvers/flattening/maps.h +++ b/src/solvers/flattening/maps.h @@ -104,8 +104,10 @@ class mapst : public equalityt /// \param i: equivalence-class number to merge void update_domain_map(std::size_t i); - /// Classification of lazily deferred constraints. - enum class lazy_typet + /// Classification of map-theory constraints. Used both for lazy dispatch + /// of refinement-loop constraints (\ref lazy_constraints) and for + /// per-kind statistics (\ref constraint_count). + enum class map_constraint_kindt { MAP_ACKERMANN, MAP_WITH, @@ -114,16 +116,17 @@ class mapst : public equalityt MAP_TYPECAST, MAP_CONSTANT, MAP_COMPREHENSION, + MAP_EQUALITY, MAP_LET }; /// A constraint together with its classification, used for lazy dispatch. struct lazy_constraintt { - lazy_typet type; + map_constraint_kindt type; exprt lazy; - lazy_constraintt(lazy_typet _type, const exprt &_lazy) + lazy_constraintt(map_constraint_kindt _type, const exprt &_lazy) : type(_type), lazy(_lazy) { } @@ -145,6 +148,23 @@ class mapst : public equalityt /// \param refine: if true and lazy mode is active, defer the constraint void add_map_constraint(const lazy_constraintt &lazy, bool refine = true); + /// Convenience wrapper that adds a constraint of the given \p kind and + /// bumps the per-kind counter in a single call. Equivalent to + /// add_map_constraint(lazy_constraintt(kind, body), refine); + /// ++constraint_count[kind]; + /// Use this in preference to spelling out both calls at every site. + /// \param kind: classification of the constraint being added + /// \param body: the constraint expression + /// \param refine: if true and lazy mode is active, defer the constraint + void add_constraint( + map_constraint_kindt kind, + const exprt &body, + bool refine = false) + { + add_map_constraint(lazy_constraintt{kind, body}, refine); + ++constraint_count[kind]; + } + /// Add Ackermann constraints for every pair of keys in each equivalence /// class: if two keys are equal then the corresponding map lookups must /// yield equal values. Complexity is quadratic in the size of each key @@ -159,26 +179,13 @@ class mapst : public equalityt const key_sett &key_set, const map_equalityt &equality); - /// Classification of constraints for statistics reporting. - enum class constraint_typet - { - MAP_ACKERMANN, - MAP_WITH, - MAP_IF, - MAP_OF, - MAP_TYPECAST, - MAP_CONSTANT, - MAP_COMPREHENSION, - MAP_EQUALITY, - MAP_LET - }; - typedef std::map map_constraint_countt; + typedef std::map map_constraint_countt; /// Per-type constraint counts, populated when \ref collect_constraint_stats /// is true. map_constraint_countt constraint_count; - /// Return a human-readable string for a constraint type enum value. - std::string enum_to_string(constraint_typet type); + /// Return a human-readable string for a constraint kind enum value. + std::string enum_to_string(map_constraint_kindt kind); /// Emit the collected constraint counts as a JSON object to the status log. void display_constraint_count();