mirror of
https://github.com/TwilitRealm/dusklight
synced 2026-08-21 13:36:50 -04:00
187 lines
7.9 KiB
C++
187 lines
7.9 KiB
C++
// Algebraic simplification techniques treat all requirements as unrelated variables
|
|
// and allow us to turn our two-level DNF/sum-of-products form into a simpler
|
|
// multi-level expression.
|
|
|
|
// The approach taken here is mostly used in hardware logic synthesis, and described in:
|
|
|
|
// * https://faculty.sist.shanghaitech.edu.cn/faculty/zhoupq/Teaching/Spr16/07-Multi-Level-Logic-Synthesis.pdf
|
|
// * Some lecture slides about the topic. These make the concepts of kernels,
|
|
// algebraic division, and rectangles very accessible, but e.g. how to actually find rectangles is left open.
|
|
// * Rudell 1989, Logic Synthesis for VLSI Design
|
|
// https://www2.eecs.berkeley.edu/Pubs/TechRpts/1989/ERL-89-49.pdf (pp. 41-70)
|
|
// * Rudell's PhD thesis is where this stuff was originally researched.
|
|
// The pseudocode for generating prime rectangles is found there and quite useful.
|
|
|
|
// This approach does not exploit boolean properties like x & !x = false or x | !x = true
|
|
// but logic doesn't need this since we only have positive terms. The other thing
|
|
// these techniques don't handle are "implies" relations like Beetle x 2 => Beetle x 1,
|
|
// so we may use different techniques for those.
|
|
|
|
#pragma once
|
|
|
|
#include "bits.hpp"
|
|
#include <algorithm>
|
|
#include <iterator>
|
|
#include <functional>
|
|
|
|
struct FoundKernel
|
|
{
|
|
std::vector<BitVector> kernel;
|
|
BitVector coKernel;
|
|
};
|
|
|
|
randomizer::logic::requirement::Requirement DNFToExpr(BitIndex& bitIndex, DNF dnf);
|
|
|
|
randomizer::logic::requirement::Requirement createAnd(std::vector<randomizer::logic::requirement::Requirement> terms);
|
|
|
|
// Generates all prime rectangles in this matrix. A rectangle is a set of columns and rows
|
|
// such that for every row and column, matrix[row][colum] is not zero. A prime rectangle
|
|
// is a rectangle that is not included in any other rectangle.
|
|
template<typename Func>
|
|
void genRectangles(std::vector<int>& rows, std::vector<int>& cols, std::vector<std::vector<int>>& matrix, Func callback)
|
|
{
|
|
// generate trivial prime rectangles first
|
|
// trivial rectangles are rectangles with only
|
|
// one row or one column
|
|
for (const auto& row : rows)
|
|
{
|
|
// Find the ones in this row
|
|
std::vector<int> ones = {};
|
|
std::copy_if(cols.begin(), cols.end(), std::back_inserter(ones), [=](const int& c) { return matrix[row][c]; });
|
|
// if this row has ones and there's no other row that
|
|
// has ones in the same positions, this row is part of
|
|
// a trivial row prime rectangle
|
|
if (!ones.empty() and
|
|
std::none_of(
|
|
rows.begin(),
|
|
rows.end(),
|
|
[=](const int& r)
|
|
{ return r != row && std::all_of(ones.begin(), ones.end(), [=](const int& c) { return matrix[r][c]; }); }))
|
|
{
|
|
callback({row}, ones);
|
|
}
|
|
}
|
|
|
|
for (const auto& col : cols)
|
|
{
|
|
// Same as above
|
|
std::vector<int> ones = {};
|
|
std::copy_if(rows.begin(), rows.end(), std::back_inserter(ones), [=](const int& r) { return matrix[r][col]; });
|
|
|
|
if (!ones.empty() and
|
|
std::none_of(
|
|
rows.begin(),
|
|
rows.end(),
|
|
[=](const int& c)
|
|
{ return c != col && std::all_of(ones.begin(), ones.end(), [=](const int& r) { return matrix[r][c]; }); }))
|
|
{
|
|
callback(ones, {col});
|
|
}
|
|
}
|
|
|
|
genRectanglesRecursive(rows, cols, matrix, 0, {}, {}, callback);
|
|
}
|
|
|
|
// Recursively generates non-trivial prime rectangles based on the
|
|
// existing prime rectangle given by matrix and rect_cols. Rectangles generated
|
|
// by this function will have fewer rows but more columns than the passed rectangle.
|
|
|
|
// Args:
|
|
// all_rows: A list of all row indices, for convenience.
|
|
// all_cols: A list of all column indices, for convenience.
|
|
// matrix: The matrix being searched for rectangles.
|
|
// index: Grow the rectangle starting from this column
|
|
// rect_rows: Rows of the prime rectangle.
|
|
// rect_cols: Columns of the prime rectangle.
|
|
// callback: Called for every prime rectangle.
|
|
template<typename Func>
|
|
void genRectanglesRecursive(std::vector<int>& allRows,
|
|
std::vector<int>& allCols,
|
|
std::vector<std::vector<int>>& matrix,
|
|
const int& index,
|
|
std::vector<int> rectRows,
|
|
std::vector<int> rectCols,
|
|
Func callback)
|
|
{
|
|
// do not consider columns before the starting index, and require
|
|
// this column to have two or more ones (otherwise we'd generate a trivial rectangle)
|
|
for (const auto& c : allCols)
|
|
{
|
|
if (c >= index && std::count_if(allRows.begin(), allRows.end(), [=](const int& row) { return matrix[row][c]; }) >= 2)
|
|
{
|
|
// create submatrix, only keeping rows where the column has a one
|
|
// all other rows are zeroed
|
|
std::vector<std::vector<int>> m1 = {};
|
|
for (int rowIdx = 0; rowIdx < matrix.size(); rowIdx++)
|
|
{
|
|
auto& row = matrix[rowIdx];
|
|
m1.push_back(matrix[rowIdx][c] ? row : std::vector(row.size(), 0));
|
|
}
|
|
|
|
// create new rect rows based on this column. If we had an existing
|
|
// rectangle in the recursive case, this shrinks the rectangle, otherwise
|
|
// it creates the first rectangle
|
|
std::vector<int> rect1Rows;
|
|
std::copy_if(allRows.begin(),
|
|
allRows.end(),
|
|
std::back_inserter(rect1Rows),
|
|
[=](const int& row) { return matrix[row][c]; });
|
|
std::vector<int> rect1Cols = rectCols;
|
|
|
|
bool prune = false;
|
|
// add column c and all columns with EXACTLY the same number of ones
|
|
for (const auto& c1 : allCols)
|
|
{
|
|
if (std::count_if(allRows.begin(), allRows.end(), [=](const int& row) { return m1[row][c1]; }) ==
|
|
std::count_if(allRows.begin(), allRows.end(), [=](const int& row) { return matrix[row][c]; }))
|
|
{
|
|
if (c1 < c)
|
|
{
|
|
// "if a column of 1's occurs for a column index less than
|
|
// the starting index, then all rectangles in the current
|
|
// submatrix have already been examined when that column
|
|
// was processed" (Rudell)
|
|
prune = true;
|
|
break;
|
|
}
|
|
else
|
|
{
|
|
// add the column to our rectangle
|
|
rect1Cols.push_back(c1);
|
|
for (const auto& row : allRows)
|
|
{
|
|
m1[row][c1] = 0;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (!prune)
|
|
{
|
|
callback(rect1Rows, rect1Cols);
|
|
genRectanglesRecursive(allRows, allCols, m1, c, rect1Rows, rect1Cols, callback);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
std::vector<FoundKernel> findKernels(const std::vector<BitVector>& cubes,
|
|
const std::vector<int>& variables,
|
|
const BitVector& coKernelPath,
|
|
std::vector<BitVector>& seenCoKernels,
|
|
int minIdx = 0);
|
|
|
|
std::pair<std::vector<BitVector>, std::vector<BitVector>> algebraicDivision(const std::vector<BitVector>& expr,
|
|
const std::vector<BitVector>& divisor);
|
|
|
|
template<typename Container>
|
|
std::vector<randomizer::logic::requirement::Requirement> lookupRequirements(BitIndex& bitIndex, Container r)
|
|
{
|
|
std::vector<randomizer::logic::requirement::Requirement> reqs;
|
|
for (auto& bit : r)
|
|
{
|
|
reqs.push_back(bitIndex.reverseIndex[bit]);
|
|
}
|
|
return reqs;
|
|
}
|