search

ahumenberger / Z3.jl

Julia interface to Z3
MIT License
57 stars 7 forks source link

Cannot find add_soft #14

Closed yangky11 closed 3 years ago

yangky11 commented 3 years ago

Hi,

I encountered the following error when trying to use add_soft.

julia> using Z3

julia> add_soft
ERROR: UndefVarError: add_soft not defined

I noticed that add_soft was added to z3jl.cpp relatively recently in [this commit] (https://github.com/Z3Prover/z3/commit/094e41d21d93fff2c8098374d91d9fae468c3e80#diff-12a201dd45ee5c62027a744bdb29a49fd835bf8b1b8c3c3bd205d6703274312c). So I guess maybe the update hasn't been properly propagated to Z3.jl. Any help is appreciated. Thanks!

For reference, here is how I built Z3 and Z3.jl:

  1. Clone the master branch of the Z3 repo.
  2. mkdir build && cd build
  3. cmake -DCMAKE_BUILD_TYPE=Release -DZ3_BUILD_JULIA_BINDINGS=True -DCMAKE_PREFIX_PATH=/path/to/libcxxwrap-julia-prefix .., where /path/to/libcxxwrap-julia-prefix is returned by CxxWrap.prefix_path() in Julia REPL.
  4. make -j4 && make install
  5. add Z3 in Julia REPL.
yangky11 commented 3 years ago

Looks like it's because build_tarballs.jl is outdated. It only supports Z3 4.8.8, and the installation on some platforms is not working.

Not sure how to fix it though.

yangky11 commented 3 years ago

I just found that add can serve as add_soft when provided with a weight argument. So maybe this is not an urgent issue. I'm working on upgrading z3_jll to 4.8.10 and will post an update later.