diff --git a/README.markdown b/README.markdown index 92df6906..6c7b89a9 100644 --- a/README.markdown +++ b/README.markdown @@ -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 @@ -62,36 +64,9 @@ 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 @@ -99,5 +74,5 @@ Out[9]: 180388626432 * [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.