This PR introduces functionality to detect equivalent lookup tables within a circuit, aiming to enhance the efficiency of the SMT solver by avoiding the addition of multiple identical lookup tables as interpreted functions.
The fixed element of the analyzer is now converted into an equivalent matrix using u64 instead of CellValue. This modification facilitates the use of HashSet operations on vectors of tuples, enabling efficient detection of identical sets of rows.
Two lookup tables are defined as equivalent if every row in one table can be found in the other, irrespective of the order or repetition of rows.
match_equivalent_lookup_tables and have_same_rows functions implement identify and match equivalent lookup tables. The computational complexity for these operations is O(N × M) Where N and M are the number of rows and columns, respectively.
The analyzer is adjusted to utilize a call to an existing equivalent lookup table rather than redefining it.
This enhancement prevents the unnecessary duplication of lookup tables in the SMT solver's interpreted functions, thereby streamlining solver operations and potentially reducing computation time.
To test the new functionality, new circuits with identical lookups but with different orders of rows are implemented and new tests are added to analyze these new circuits.
This PR introduces functionality to detect equivalent lookup tables within a circuit, aiming to enhance the efficiency of the SMT solver by avoiding the addition of multiple identical lookup tables as interpreted functions.
fixedelement of the analyzer is now converted into an equivalent matrix usingu64instead ofCellValue. This modification facilitates the use ofHashSetoperations on vectors of tuples, enabling efficient detection of identical sets of rows.match_equivalent_lookup_tablesandhave_same_rowsfunctions implement identify and match equivalent lookup tables. The computational complexity for these operations is O(N × M) Where N and M are the number of rows and columns, respectively.The analyzer is adjusted to utilize a call to an existing equivalent lookup table rather than redefining it.
This enhancement prevents the unnecessary duplication of lookup tables in the SMT solver's interpreted functions, thereby streamlining solver operations and potentially reducing computation time.
To test the new functionality, new circuits with identical lookups but with different orders of rows are implemented and new tests are added to analyze these new circuits.