From 6776bb825895431f31b9403bc5be1597697c3ace Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Apr 2026 16:00:00 +0000 Subject: [PATCH 1/3] Extract map_theoryt 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 -> map_theoryt -> equalityt -> prop_conv_solvert Co-authored-by: Kiro --- src/solvers/Makefile | 1 + src/solvers/flattening/arrays.cpp | 410 +----------------------- src/solvers/flattening/arrays.h | 117 +------ src/solvers/flattening/map_theory.cpp | 436 ++++++++++++++++++++++++++ src/solvers/flattening/map_theory.h | 150 +++++++++ 5 files changed, 596 insertions(+), 518 deletions(-) create mode 100644 src/solvers/flattening/map_theory.cpp create mode 100644 src/solvers/flattening/map_theory.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 9f4bf192744..4bb20db57d0 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/map_theory.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 040ca999a6e..ffae74c530b 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "arrays.h" #include -#include #include +#include #include #include #include @@ -31,25 +31,9 @@ arrayst::arrayst( propt &_prop, message_handlert &_message_handler, bool _get_array_constraints) - : equalityt(_prop, _message_handler), - ns(_ns), - log(_message_handler), + : map_theoryt(_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 +77,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 +127,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 +535,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 1d2c4caccef..9b9287a927b 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -12,13 +12,7 @@ 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 "map_theory.h" class array_comprehension_exprt; class array_exprt; @@ -30,7 +24,7 @@ class symbol_exprt; class with_exprt; class update_exprt; -class arrayst:public equalityt +class arrayst : public map_theoryt { public: arrayst( @@ -39,113 +33,27 @@ 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 map_theoryt 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 /// two expressions in the union-find so that element-wise constraints /// propagate correctly. - 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( @@ -162,17 +70,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/map_theory.cpp b/src/solvers/flattening/map_theory.cpp new file mode 100644 index 00000000000..43a67c8602f --- /dev/null +++ b/src/solvers/flattening/map_theory.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 "map_theory.h" + +#include +#include + +#include +#include + +#ifdef DEBUG +# include + +# include +#endif + +map_theoryt::map_theoryt( + 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 map_theoryt::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 map_theoryt::collect_indices() +{ + for(std::size_t i = 0; i < arrays.size(); i++) + { + collect_indices(arrays[i]); + } +} + +void map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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/map_theory.h b/src/solvers/flattening/map_theory.h new file mode 100644 index 00000000000..f5ed1e411a6 --- /dev/null +++ b/src/solvers/flattening/map_theory.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_MAP_THEORY_H +#define CPROVER_SOLVERS_FLATTENING_MAP_THEORY_H + +#include + +#include "equality.h" + +#include +#include +#include + +class equal_exprt; +class index_exprt; +class symbol_exprt; + +class map_theoryt : public equalityt +{ +public: + map_theoryt( + const namespacet &_ns, + propt &_prop, + message_handlert &_message_handler, + bool _get_array_constraints = false); + + ~map_theoryt() 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 map_theoryt, 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_MAP_THEORY_H From c18eb8f333753be2014ac5d94adb0d53d580cab3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 10:14:30 +0000 Subject: [PATCH 2/3] =?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 map_theoryt 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. 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/map_theory.cpp | 253 +++++++++-------- src/solvers/flattening/map_theory.h | 113 ++++---- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/refine_arrays.cpp | 26 +- 18 files changed, 362 insertions(+), 381 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index ffae74c530b..af68bd90ee6 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -30,83 +30,80 @@ arrayst::arrayst( const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_array_constraints) - : map_theoryt(_ns, _prop, _message_handler, _get_array_constraints), + bool _get_constraints) + : map_theoryt(_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()); @@ -242,26 +236,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)); @@ -269,17 +264,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 { @@ -298,7 +294,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) @@ -322,7 +318,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) { @@ -355,17 +351,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(), @@ -373,31 +369,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; @@ -408,16 +404,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. @@ -438,54 +434,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) @@ -497,18 +493,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))); @@ -516,19 +513,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 9b9287a927b..db26e7adf22 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -31,44 +31,44 @@ class arrayst : public map_theoryt const namespacet &_ns, propt &_prop, message_handlert &message_handler, - bool get_array_constraints = false); + bool get_constraints = false); // NOLINTNEXTLINE(readability/identifiers) typedef map_theoryt 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 /// two expressions in the union-find so that element-wise constraints /// propagate correctly. - 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 68194f9d98f..da0aa38143c 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()); @@ -540,7 +540,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 7ad8a4ce548..9c8516cc681 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, pair.second); + record_let_binding(pair.first, pair.second); } } 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 b52c0da27f9..c4ac8eadf38 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/map_theory.cpp b/src/solvers/flattening/map_theory.cpp index 43a67c8602f..791a17ae898 100644 --- a/src/solvers/flattening/map_theory.cpp +++ b/src/solvers/flattening/map_theory.cpp @@ -27,35 +27,35 @@ map_theoryt::map_theoryt( 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 map_theoryt::record_array_index(const index_exprt &index) +void map_theoryt::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 map_theoryt::collect_indices() +void map_theoryt::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 map_theoryt::collect_indices(const exprt &expr) +void map_theoryt::collect_keys(const exprt &expr) { if(expr.id() != ID_index) { @@ -64,7 +64,7 @@ void map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::collect_arrays(const exprt &a) +void map_theoryt::collect_maps(const exprt &a) { const array_typet &array_type = to_array_type(a.type()); @@ -104,15 +104,15 @@ void map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::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 map_theoryt::add_array_constraint( - const lazy_constraintt &lazy, - bool refine) +/// adds map constraints (refine=true...lazily for the refinement loop) +void map_theoryt::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 map_theoryt::add_array_constraint( } } -void map_theoryt::add_array_Ackermann_constraints() +void map_theoryt::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 map_theoryt::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 map_theoryt::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,86 +295,86 @@ void map_theoryt::add_array_Ackermann_constraints() } } -/// merge the indices into the root -void map_theoryt::update_index_map(std::size_t i) +/// merge the keys into the root +void map_theoryt::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 map_theoryt::update_index_map(bool update_all) +void map_theoryt::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 map_theoryt::add_array_constraints_equality( - const index_sett &index_set, - const array_equalityt &array_equality) +void map_theoryt::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]++; } } @@ -388,42 +382,41 @@ std::string map_theoryt::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"; + case constraint_typet::MAP_ACKERMANN: + return "mapAckermann"; + case constraint_typet::MAP_WITH: + return "mapWith"; + case constraint_typet::MAP_IF: + return "mapIf"; + case constraint_typet::MAP_OF: + return "mapOf"; + case constraint_typet::MAP_TYPECAST: + return "mapTypecast"; + case constraint_typet::MAP_CONSTANT: + return "mapConstant"; + case constraint_typet::MAP_COMPREHENSION: + return "mapComprehension"; + case constraint_typet::MAP_EQUALITY: + return "mapEquality"; + case constraint_typet::MAP_LET: + return "mapLet"; default: UNREACHABLE; } } -void map_theoryt::display_array_constraint_count() +void map_theoryt::display_constraint_count() { json_objectt json_result; - json_objectt &json_array_theory = - json_result["arrayConstraints"].make_object(); + json_objectt &json_map_theory = json_result["mapConstraints"].make_object(); 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] = + json_map_theory[contraint_type_string] = json_numbert(std::to_string(it->second)); num_constraints += it->second; diff --git a/src/solvers/flattening/map_theory.h b/src/solvers/flattening/map_theory.h index f5ed1e411a6..20613267194 100644 --- a/src/solvers/flattening/map_theory.h +++ b/src/solvers/flattening/map_theory.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_MAP_THEORY_H #define CPROVER_SOLVERS_FLATTENING_MAP_THEORY_H @@ -32,60 +32,59 @@ class map_theoryt : public equalityt const namespacet &_ns, propt &_prop, message_handlert &_message_handler, - bool _get_array_constraints = false); + bool _get_constraints = false); ~map_theoryt() 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 map_theoryt, 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 map_theoryt : 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 52317c249cc4fbc666a540679dcdf55e62c09a69 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 12:16:10 +0000 Subject: [PATCH 3/3] Add Doxygen documentation to map_theoryt Document all public and protected methods, key data members, enums, and structs in map_theory.h with Doxygen comments following the CBMC coding standard. Co-authored-by: Kiro --- src/solvers/flattening/map_theory.h | 92 ++++++++++++++++++++++++++--- 1 file changed, 83 insertions(+), 9 deletions(-) diff --git a/src/solvers/flattening/map_theory.h b/src/solvers/flattening/map_theory.h index 20613267194..1ad6becd42e 100644 --- a/src/solvers/flattening/map_theory.h +++ b/src/solvers/flattening/map_theory.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 → map_theoryt → equalityt → prop_conv_solvert class map_theoryt : 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 map_theoryt( const namespacet &_ns, propt &_prop, @@ -36,45 +46,80 @@ class map_theoryt : public equalityt ~map_theoryt() 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 map_theoryt, 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 map_theoryt : 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 map_theoryt : 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 map_theoryt : 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 map_theoryt : 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();