Skip to content

Commit 6776bb8

Browse files
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 <kiro-agent@users.noreply.github.com>
1 parent beacad5 commit 6776bb8

5 files changed

Lines changed: 596 additions & 518 deletions

File tree

src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ SRC = $(BOOLEFORCE_SRC) \
140140
flattening/bv_utils.cpp \
141141
flattening/c_bit_field_replacement_type.cpp \
142142
flattening/equality.cpp \
143+
flattening/map_theory.cpp \
143144
flattening/pointer_logic.cpp \
144145
floatbv/float_bv.cpp \
145146
floatbv/float_utils.cpp \

0 commit comments

Comments
 (0)