mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Code Activity

Removing install details for optional engines

Browse source
This commit is contained in:
KrystalDelusion 2022-05-31 11:18:05 +12:00
parent fc9ff3d733
commit b18f22cf43
1 changed files with 8 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
docs/source/install.rst
View file

@ -95,87 +95,25 @@ https://github.com/Z3Prover/z3/wiki
Optional components Optional components
------------------- -------------------
Additional solver engines can be installed as per their instructions, links are
provided below.
Yices 2 Yices 2
^^^^^^^ ^^^^^^^
http://yices.csl.sri.com/
http://yices.csl.sri.com/ https://github.com/SRI-CSL/yices2
.. code-block:: text
git clone https://github.com/SRI-CSL/yices2
cd yices2
autoconf
./configure
make -j$(nproc)
sudo make install
super_prove super_prove
^^^^^^^^^^^ ^^^^^^^^^^^
https://github.com/sterin/super-prove-build
https://github.com/sterin/super-prove-build
.. code-block:: text
sudo apt-get install cmake ninja-build g++ python-dev python-setuptools \
python-pip git
git clone --recursive https://github.com/sterin/super-prove-build
cd super-prove-build
mkdir build
cd build
cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
ninja
ninja package
This creates a .tar.gz archive for the target system. Extract it to
``/usr/local/super_prove``
.. code-block:: text
sudo tar -C /usr/local -x super_prove-X-Y-Release.tar.gz
Then create a wrapper script ``/usr/local/bin/suprove`` with the following contents:
.. code-block:: text
#!/bin/bash
tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
exec /usr/local/super_prove/bin/${tool}.sh "$@"
And make this wrapper script executable:
.. code-block:: text
sudo chmod +x /usr/local/bin/suprove
Avy Avy
^^^ ^^^
https://arieg.bitbucket.io/avy/
https://arieg.bitbucket.io/avy/
.. code-block:: text
git clone https://bitbucket.org/arieg/extavy.git
cd extavy
git submodule update --init
mkdir build; cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make -j$(nproc)
sudo cp avy/src/{avy,avybmc} /usr/local/bin/
Boolector Boolector
^^^^^^^^^ ^^^^^^^^^
http://fmv.jku.at/boolector/
http://fmv.jku.at/boolector/ https://github.com/boolector/boolector
.. code-block:: text
git clone https://github.com/boolector/boolector
cd boolector
./contrib/setup-btor2tools.sh
./contrib/setup-lingeling.sh
./configure.sh
make -C build -j$(nproc)
sudo cp build/bin/{boolector,btor*} /usr/local/bin/
sudo cp deps/btor2tools/bin/btorsim /usr/local/bin/