Skip to content

Commit

Permalink
Update README with paper information
Browse files Browse the repository at this point in the history
  • Loading branch information
arijitsh authored Aug 11, 2024
1 parent f2bbd4c commit 9b232c6
Showing 1 changed file with 5 additions and 30 deletions.
35 changes: 5 additions & 30 deletions README.markdown
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,9 @@

CSB (Count and Sample on Bitvectors) is an approximate model counting and almost-uniform sampling tool aimed at solving constraints of bitvectors.

CSB uses [STP](https://github.com/stp/stp) as its frontend and is built on top of that. For counting it uses [ApproxMC](https://github.com/meelgroup/approxmc) (with [Arjun](https://github.com/meelgroup/arjun)). For sampling, it uses [UniSamp](https://www.cs.toronto.edu/~meel/Papers/lics22.pdf).
To learn more about CSB, please have a look at our [SMT Workshop '24 paper](https://ceur-ws.org/Vol-3725/short2.pdf).

CSB uses [STP](https://github.com/stp/stp) as its frontend and is built on top of that. For counting it uses [ApproxMC](https://github.com/meelgroup/approxmc) (with [Arjun](https://github.com/meelgroup/arjun)). For sampling, it uses [UniGen](https://github.com/meelgroup/unigen/).

## Build and install

Expand Down Expand Up @@ -62,42 +64,15 @@ Run with an SMT-LIB2 file:
./stp -c myproblem.smt2
```

### Python Interface for Almost-uniform Sampler:
```
In [1]: import stp
In [2]: a = stp.Solver()
In [3]: x = a.bitvec('x')
In [4]: y = a.bitvec('y')
In [5]: a.add(x + y < 20)
In [6]: a.add(x > 10)
In [7]: a.add(y > 10)
In [8]: a.useUnigen()
Out[8]: True
In [9]: a.check()
Out[9]: True
In [10]: a.model()
Out[10]: {'x': 2371135469, 'y': 1923831833}
```

### Python Interface for Approximate Counter:

```
In [8]: a.useApproxMC()
Out[8]: True
In [9]: a.count()
Out[9]: 180388626432
```

## Architecture

**CSB** converts bitvector constraints into SAT using [STP](https://github.com/stp/stp), integrating with [ApproxMC](https://github.com/meelgroup/approxmc) or [UniSamp](https://github.com/arijitsh/unigen/tree/unisamp) based on specific needs of counting or sampling. This tool is developed from a study on model counters and bitblasting tools, as detailed in [this study](https://arijitsh.github.io/papers/sharpsmt.pdf).

**CSB** converts bitvector constraints into SAT using [STP](https://github.com/stp/stp), integrating with [ApproxMC](https://github.com/meelgroup/approxmc) or [UniGen](https://github.com/meelgroup/unigen/) based on specific needs of counting or sampling. The benchmarks used for evaluating CSB in the SMT workshop paper are available [here](https://utoronto-my.sharepoint.com/:u:/g/personal/arijit_shaw_mail_utoronto_ca/EWcTcfGobH5Jl5SwjzRu6TQB169vWwTnjg-IXWiHJwmuDA?e=MFuxUM).


# Authors

* [Arijit Shaw](https://arijitsh.github.io)
* [Kuldeep S. Meel](https://www.cs.toronto.edu/~meel/)

Please refer to STP/UniSamp/ApproxMC for the respective authors.
Please refer to STP/UniGen/ApproxMC for the respective authors.

0 comments on commit 9b232c6

Please sign in to comment.