add ditt、msv......

.gitignore

@@ -8,5 +8,6 @@ data/
 
 tmp/
 
+
 gmon.out
 

Dockerfile

@@ -3,6 +3,10 @@ FROM ubuntu:20.04
 ENV DEBIAN_FRONTEND=noninteractive
 ENV TZ=Asia/Shanghai
 
+# 替换为阿里云镜像源
+RUN sed -i 's/archive.ubuntu.com/mirrors.aliyun.com/g' /etc/apt/sources.list && \
+    sed -i 's/security.ubuntu.com/mirrors.aliyun.com/g' /etc/apt/sources.list
+
 RUN apt-get update && apt-get upgrade -y --no-install-recommends apt-utils
 
 # build essential
@@ -13,11 +17,15 @@ RUN apt-get install -y \
     curl \
     cmake \
     ninja-build \
-    git
+    git \
+    autoconf \
+    automake \
+    libcrypt-dev \
+    libc6-dev
 
 # toolkit related libraries
 RUN apt-get install -y \
-    libreadline6-dev \
+    libreadline-dev \
     tcl-dev \
     pkg-config \
     bison \
@@ -48,9 +56,14 @@ RUN add-apt-repository ppa:ubuntu-toolchain-r/test -y \
 # python and distutils
 RUN apt-get update && apt-get install -y \
     python3.8 \
+    python3.8-dev \
     python3.8-distutils \
     python3-pip
 
+# 新增：将python3软链接到python3.8
+RUN ln -sf /usr/bin/python3.8 /usr/bin/python3 && \
+    ln -sf /usr/bin/python3.8 /usr/bin/python
+
 RUN python3.8 -m pip install --upgrade pip setuptools wheel
 
 RUN python3.8 -m pip install matplotlib imageio
@@ -63,6 +76,33 @@ ENV PATH="/root/.cargo/bin:${PATH}"
 
 RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-10 60 --slave /usr/bin/g++ g++ /usr/bin/g++-10
 
+# Anaconda3 installation
+ENV CONDA_DIR=/opt/conda
+# 关键修改：将系统路径放在Anaconda路径之前
+ENV PATH="/usr/bin:/usr/sbin:/bin:/sbin:$CONDA_DIR/bin:/root/.cargo/bin"
+
+RUN wget --quiet https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh -O ~/miniconda.sh && \
+    /bin/bash ~/miniconda.sh -b -p $CONDA_DIR && \
+    rm ~/miniconda.sh && \
+    $CONDA_DIR/bin/conda tos accept --override-channels --channel https://repo.anaconda.com/pkgs/main && \
+    $CONDA_DIR/bin/conda tos accept --override-channels --channel https://repo.anaconda.com/pkgs/r && \
+    # Allow mamba installation
+    conda install -y mamba -n base -c conda-forge && \
+    # Clean up
+    conda clean -ya
+
+
+# 安装 Kissat SAT 求解器
+RUN git clone https://github.com/arminbiere/kissat.git && \
+    cd kissat && \
+    ./configure && \
+    make -j$(nproc) && \
+    cp build/kissat /usr/bin/ && \
+    cd .. && \
+    rm -rf kissat
+
+RUN kissat --version
+
 WORKDIR /workspace
 
-CMD ["bash"]
+CMD ["bash"]

README.md

@@ -18,6 +18,26 @@ $ cd /workspace
 $ mkdir -p build && cd build
 $ cmake -G Ninja ..
 $ ninja
+
+# 1. 克隆代码库
+git clone https://github.com/Logic-Factory/LogicFactory.git
+
+# 2. 进入目录并初始化子模块
+cd LogicFactory
+git submodule update --init --recursive
+
+# 3. 构建 Docker 镜像（无需修改）
+docker build -t logic-factory:latest .
+
+# 4. 运行容器（关键：添加 --gpus all 启用 GPU 访问）
+docker run -it --gpus all -v ../LogicFactory-hub-pku:/workspace logic-factory:latest
+#  ↑↑↑ 新增 --gpus all 选项，允许容器访问主机所有 GPU
+
+# 5. 进入容器后，正常构建（无需修改）
+cd /workspace
+mkdir -p build && cd build
+cmake -G Ninja ..
+ninja
 ```
 
 - method2: install dependencies and compile 

src/layer_logic/CMakeLists.txt

@@ -1,5 +1,21 @@
 message("lf_logic.")
 add_library(lf_logic INTERFACE)
+
+# 收集 layer_logic/api/lspku 目录下的所有 .cpp 文件
+file(GLOB_RECURSE LSPKU_SOURCES
+    "${CMAKE_CURRENT_SOURCE_DIR}/layer_logic/api/lspku/FastEx/share/**/*.cpp"
+    "${CMAKE_CURRENT_SOURCE_DIR}/layer_logic/api/lspku/PowerSyn/share/*.cpp"
+)
+
+# 打印收集到的文件数量和列表
+# message(STATUS "Found ${LSPKU_SOURCES} LSPKU source files:")
+# foreach(file ${LSPKU_SOURCES})
+#    message(STATUS "  - ${file}")
+# endforeach()
+
+# 将收集的源文件添加到 lf_logic 库
+target_sources(lf_logic INTERFACE ${LSPKU_SOURCES})
+
 target_link_libraries(lf_logic INTERFACE
     pugixml
     lorina
@@ -12,4 +28,19 @@ target_link_libraries(lf_logic INTERFACE
     lf_misc
     lf_arch
 )
-target_include_directories(lf_logic SYSTEM INTERFACE ${CMAKE_CURRENT_SOURCE_DIR})
+target_include_directories(lf_logic SYSTEM INTERFACE ${CMAKE_CURRENT_SOURCE_DIR})
+
+
+
+# 定义 RL 目录路径（便于维护）
+set(RL_DIR "${CMAKE_CURRENT_SOURCE_DIR}/layer_logic/api/lspku/PowerSyn/RL")
+
+# 自定义目标：使用 make 构建 RL 目录（而非 ninja）
+add_custom_target(run_sub_makefile
+    COMMAND make -C ${RL_DIR}  # 关键修改：用 make 替代 ${CMAKE_MAKE_PROGRAM}
+    COMMENT "Building RL subproject with make in: ${RL_DIR}"  # 增加构建日志提示
+    VERBATIM  # 确保路径含特殊字符时正确解析
+)
+
+# 保持依赖关系不变（lf_logic 依赖 run_sub_makefile 完成后再构建）
+add_dependencies(lf_logic run_sub_makefile)

src/layer_logic/layer_logic/api/lspku/FastEx/exact_synthesis_DITT/README.md

@@ -0,0 +1,83 @@
+# Exact DITT API Documentation
+
+## Introduction
+
+This document describes the application programming interfaces (APIs) provided by the `exact::DITT` class for encoding and decoding logic functions using the Decision Diagram with Trivial Transformations (DITT) method.
+
+## API Overview
+
+### Class: `exact::DITT`
+
+The `exact::DITT` class provides functionality for encoding logic functions into a logic formula and decoding the results from a solver.
+
+## Functions
+
+### Function: `encode`
+
+- **Description**: Encodes the logic functions into a logic formula.
+- **Return Value**: Returns an `exact::Encoding` object representing the encoded logic formula.
+- **Parameters**:
+  - `bool mark_variable`: Indicates whether to mark variables in the output.
+- **Usage**:
+  ```cpp
+  exact::DITT ditt_instance(functions, technology, r, non_trivial, all_steps, no_replication, lexicographical_step, lexicographical_op, ordered_symmetric);
+  exact::Encoding encoded_formula = ditt_instance.encode(true);
+  ```
+
+### Function: `decode`
+
+- **Description**: Decodes the results from a solver's output file and writes the decoded results to an output file.
+- **Parameters**:
+  - `std::string input_file`: Path to the input file containing the solver's output.
+  - `std::string output_file`: Path to the output file where the decoded results will be written.
+- **Usage**:
+  ```cpp
+  ditt_instance.decode("solver_output.txt", "decoded_results.blif");
+  ```
+
+## Example
+
+### Encoding Example
+
+```cpp
+#include "exact.h"
+
+int main() {
+    // Define your logic functions
+    std::vector<Boolean> functions = ...; // Replace with actual functions
+
+    // Create a DITT instance
+    exact::DITT ditt_instance(functions, exact::Technology(), 0, false, false, false, false, false, false);
+
+    // Encode the functions
+    exact::Encoding encoded_formula = ditt_instance.encode(true);
+
+    // Use the encoded formula (e.g., write to a file)
+    encoded_formula.write_to_file("encoded_formula.cnf");
+
+    return 0;
+}
+```
+
+### Decoding Example
+
+```cpp
+#include "exact.h"
+
+int main() {
+    // Create a DITT instance
+    exact::DITT ditt_instance(functions, exact::Technology(), 0, false, false, false, false, false, false);
+
+    // Decode the solver's output
+    ditt_instance.decode("solver_output.txt", "decoded_results.blif");
+
+    return 0;
+}
+```
+
+## Notes
+
+- **Input/Output Files**: Ensure the input and output file paths are correctly specified.
+- **Dependencies**: The `exact::DITT` class relies on other components like `exact::Encoding` and `exact::Technology` for proper functionality.
+
+By using the `exact::DITT` APIs, you can effectively encode and decode logic functions for use in your applications.

src/layer_logic/layer_logic/api/lspku/FastEx/exact_synthesis_MSV/README.md

@@ -0,0 +1,83 @@
+# Exact MSV API Documentation
+
+## Introduction
+
+This documentation outlines the APIs provided by the `exact::MSV` class for encoding and decoding logic functions using the Multiple Symmetry Verification (MSV) method.
+
+## API Overview
+
+### Class: `exact::MSV`
+
+The `exact::MSV` class offers methods to encode logic functions into a logic formula and decode the results from a solver.
+
+## Functions
+
+### Function: `encode`
+
+- **Description**: Encodes the logic functions into a logic formula.
+- **Return Value**: An `exact::Encoding` object that represents the encoded logic formula.
+- **Parameter**:
+  - `bool mark_variable`: A boolean indicating whether to mark variables in the output.
+- **Usage**:
+  ```cpp
+  exact::MSV msv_instance(functions, technology, r, non_trivial, all_steps, no_replication, lexicographical_step, lexicographical_op, ordered_symmetric);
+  exact::Encoding encoded_formula = msv_instance.encode(true);
+  ```
+
+### Function: `decode`
+
+- **Description**: Decodes the solver's output from a file and writes the decoded results to another file.
+- **Parameters**:
+  - `std::string input_file`: The path to the input file containing the solver's output.
+  - `std::string output_file`: The path to the output file where the decoded results will be saved.
+- **Usage**:
+  ```cpp
+  msv_instance.decode("solver_output.txt", "decoded_results.blif");
+  ```
+
+## Example
+
+### Encoding Example
+
+```cpp
+#include "exact.h"
+
+int main() {
+    // Define your logic functions
+    std::vector<Boolean> functions = ...; // Replace with actual functions
+
+    // Create an MSV instance
+    exact::MSV msv_instance(functions, exact::Technology(), 0, false, false, false, false, false, false);
+
+    // Encode the functions
+    exact::Encoding encoded_formula = msv_instance.encode(true);
+
+    // Use the encoded formula (e.g., write to a file)
+    encoded_formula.write_to_file("encoded_formula.cnf");
+
+    return 0;
+}
+```
+
+### Decoding Example
+
+```cpp
+#include "exact.h"
+
+int main() {
+    // Create an MSV instance
+    exact::MSV msv_instance(functions, exact::Technology(), 0, false, false, false, false, false, false);
+
+    // Decode the solver's output
+    msv_instance.decode("solver_output.txt", "decoded_results.blif");
+
+    return 0;
+}
+```
+
+## Notes
+
+- **File Paths**: Ensure that the input and output file paths are correctly specified.
+- **Dependencies**: The `exact::MSV` class depends on other components like `exact::Encoding` and `exact::Technology` for full functionality.
+
+By utilizing the `exact::MSV` APIs, you can efficiently encode and decode logic functions for use in various applications.