VIPR to SMT parser

A parser written in Rust to convert VIPR certificate for MLIP to SMT solver for verification purposes.

About The Project

I develop a parser in Rust to verify the correctness of solutions generated by mixed-integer linear programming (MILP) solvers based on this paper with some substantial modifications:

• Written in Rust
• Introduced new algorithms to check derived constraints in a recurrence style to avoid Memory Limit Exception from SMT solver software
• Further check the validity of the VIPR certificate using SMT-COQ plugin from CVC4 (in progress)

(back to top)

Getting Started

Prerequisites and Installation

For this program to run, please install

• Rust
• Any SMT solver software, e.g. cvc5, z3, cvc4

(back to top)

Usage

1. Original Examples from VIPR paper

All experiments in the original VIPR paper are conducted using this project. You can find the details in the original VIPR paper's experiments section.

For all of the above experiments, I introduced 2 scripts, one for downloading all the experiments and one for running the test and output the results in a csv file.

• To download test cases, run ./download_test.sh
• To run test cases, run ./run_test.sh <block_size> <software> where
  • block_size is the number of derived constraints to be checked each time
  • software is the SMT solver software of your choice

2. Run your own VIPR file

If you want to do test your own problems, please refer to SCIP-extension.

Once you get your .vipr file, you can run the following command

cargo run -- -f <file_path> -m <block_size> -s <software>

where

• file_path is the path of your .vipr file
• block_size is the number of derived constraints to be checked each time
• software is the SMT solver software of your choice

(back to top)