From a67b0b34d868b6af02d5748b249fc476bb600ade Mon Sep 17 00:00:00 2001 From: Zhengyang Liu Date: Thu, 25 Apr 2024 00:08:45 +0000 Subject: [PATCH] [minotaur] update README.md --- README.md | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index e3bc5a8..eb25044 100644 --- a/README.md +++ b/README.md @@ -83,22 +83,27 @@ default; the pass can be enabled by setting environment variable export ENABLE_MINOTAUR=ON $HOME/minotaur/build/minotaur-cc [clang options] - ### Offline mode +#### Extract cuts from source + To extract cuts, one can just set the environment variable `MINOTAUR_NO_INFER` and run the same command as above. -On single LLVM IR, +For a single LLVM IR source, - export MINOTAUR_NO_INFER=ON - $HOME/llvm/build/bin/opt -load-pass-plugin $HOME/minotaur/build/minotaur.so -passes="minotaur" + MINOTAUR_NO_INFER=ON $HOME/llvm/build/bin/opt -load-pass-plugin $HOME/minotaur/build/minotaur.so -passes="minotaur" -On C/C++ programs, +For a single C/C++ source, - export MINOTAUR_NO_INFER=ON - export ENABLE_MINOTAUR=ON - $HOME/minotaur/build/minotaur-cc [clang options] + ENABLE_MINOTAUR=ON MINOTAUR_NO_INFER=ON $HOME/minotaur/build/minotaur-cc [clang options] + +For a C/C++ project, simply set CC and CXX to `minotaur-cc` and `minotaur-cxx`, and run `configure` as usual. Set `ENABLE_MINOTAUR` and `MINOTAUR_NO_INFER` to `ON` for `make`. + + CC=$HOME/minotaur/build/minotaur-cc CXX=$HOME/minotaur/build/minotaur-cxx ./configure + ENABLE_MINOTAUR=ON MINOTAUR_NO_INFER=ON make + +#### Run synthesis on cuts Run the `cache-infer` program to retrieve cuts from the cache and run synthesis on them.