Clause2Inv

Clause2Inv, LLM clause generator and clause combination algorithm.

Table of Contents

• Installation and Setup
• Project Structure
• Usage
• Example
• Contributing

Installation and Setup

Prerequisites

• Python Version: 3.8
• Dependencies: The following Python libraries are required:
  • numpy
  • openai
  • pandas
  • pyjson5
  • rich
  • scikit-learn
  • scipy
  • socksio
  • tqdm
  • z3-solver

Install all dependencies with:

conda env create -f env.yml

Project Structure

Clause2Inv/
│
├── README.md               	# readme
├── env.yml                	# conda env file
├── generator/                	# LLM
└── combinator/                 # Algorithm
    ├── linear.sh          	# Run linear problem
    ├── run_linear.py         	# Run linear benchmark
    ├── checker.py      	# Algorithm detail
    ├── output_linear/          # Output files
    └── ...          		# Other files

Usage

Running the Main Program

Ensure you're in the project's clause2inv/combinator directory, then execute the first problem of linear benchmark as follows:

./linear 1

Example

Below is an example command to run the linear benchmark:

python run_linear.py

Contributing

We welcome contributions! Feel free to submit pull requests or contact the project maintainers with suggestions.