Skip to content

Commit

Permalink
instructions for compiling with unisamp
Browse files Browse the repository at this point in the history
  • Loading branch information
arijitsh committed Nov 30, 2023
1 parent 8adf7de commit 4413e46
Showing 1 changed file with 13 additions and 2 deletions.
15 changes: 13 additions & 2 deletions README.markdown
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,16 @@ STP is a constraint solver (or SMT solver) aimed at solving constraints of bitve
For a quick install:

```
sudo apt-get install git cmake bison flex libboost-all-dev python2 perl
git clone https://github.com/stp/stp
sudo apt-get install git cmake bison flex libboost-all-dev python2 perl build-essential
sudo apt-get install zlib1g-dev libboost-program-options-dev libboost-serialization-dev
git clone https://github.com/meelgroup/stp
cd stp
git submodule init && git submodule update
./scripts/deps/setup-gtest.sh
./scripts/deps/setup-outputcheck.sh
./scripts/deps/setup-cms.sh
./scripts/deps/setup-minisat.sh
./scripts/deps/setup-unigen.sh
mkdir build
cd build
cmake ..
Expand All @@ -46,6 +48,15 @@ For more detailed instructions, see towards the end of the page.

The [SMT-LIB2](https://smtlib.cs.uiowa.edu/language.shtml) format is the recommended file format, because it is parsed by all modern bitvector solvers. Only quantifier-free bitvectors and arrays are implemented from the SMT-LIB2 format.

### Usage as Almost-uniform Sampler:

Run with an SMT-LIB2 file:

```
./stp --unisamp myproblem.smt2
```


### Usage

Run with an SMT-LIB2 file:
Expand Down

0 comments on commit 4413e46

Please sign in to comment.