# Sboximplementation

**Repository Path**: xjh2000/Sboximplementation

## Basic Information

- **Project Name**: Sboximplementation
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2024-04-11
- **Last Updated**: 2024-04-11

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Experiment enveriment

> our python script depends on linux cmd, e.g mkdir,stp

## STP
STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis  tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

* Homepage:      https://stp.github.io/
* Ubuntu PPA:    https://launchpad.net/~simple-theorem-prover/+archive/ubuntu/ppa/+packages
* Docker image:  `docker pull msoos/stp`
---

os : ubuntu 22.04

Note: some version need compile dependence lib e.g. minisat cryptominisat


``` bash
sudo apt-get install cmake bison flex libboost-all-dev python-is-python3 perl 
git clone https://github.com/stp/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
mkdir build
cd build
cmake ..
cmake --build . 
sudo cmake --install .
command -v ldconfig && sudo ldconfig
```