Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

How to do next after (./configure.sh --python; cd build; make) #133

Closed HugeChaos closed 3 years ago

HugeChaos commented 4 years ago

Hi, I have finished the following statements:

./configure.sh --python cd build make

What should I do if I want use it in python interface. Thank you!

aytey commented 4 years ago

Which part are you having trouble with?

After building, you need to make sure that build/lib is on PYTHONPATH (such that you import pyboolector):

[avj@tempvm build]$ pwd
/home/avj/clones/boolector/build
[avj@tempvm build]$ export PYTHONPATH=$(readlink -f ./lib)
[avj@tempvm build]$ echo -e "import pyboolector\nprint(dir(pyboolector)[:5])" | python
['BTOR_OPT_ACKERMANN', 'BTOR_OPT_AIGPROP_USE_BANDIT', 'BTOR_OPT_AIGPROP_USE_RESTARTS', 'BTOR_OPT_AUTO_CLEANUP', 'BTOR_OPT_AUTO_CLEANUP_INTERNAL']
aytey commented 3 years ago

@HugeChaos you all good with this or do you have any further questions?

aniemetz commented 3 years ago

Closed due to inactivity.

EpicOrange commented 2 years ago

After adding build/lib to PYTHONPATH, importing gives me something like

>>> import pyboolector
ImportError: dynamic module does not define module export function (PyInit_pyboolector)

My steps were:

cd ~/git
git clone https://github.com/Boolector/boolector
cd boolector
./contrib/setup-cadical.sh
./contrib/setup-btor2tools.sh
pip3 install Cython
./configure.sh --python
cd build
make -j4 boolector pyboolector
export PYTHONPATH="~/git/boolector/build/lib:$PYTHONPATH"
python3

I'm using Python 3.10 on an aarch64 Mac. Any idea where to look for things going wrong?

mpreiner commented 2 years ago

Hmm, what's the output of configure.sh? Maybe try to force Python 3 with the --py3 configure flag.