"LoadError: UndefVarError: `ExprAllocated` not defined"

[realharryhero]

I downloaded the package according to the install instructions, while in the ~/MetaQNL directory that I cloned onto my Ubuntu 22.04 computer, but when I run julia --project=. scripts/train.jl --dataset MiniSCAN --weight-candidate 0.4 --weight-existing 0.3 --maxsat-solver Z3 to experiment with MiniSCAN the following error occurs:

ERROR: LoadError: UndefVarError: `ExprAllocated` not defined
Stacktrace:
  [1] getproperty(x::Module, f::Symbol)
    @ Base ./Base.jl:31
  [2] top-level scope
    @ ~/MetaQNL/src/optimization/maxsat_solvers.jl:40
  [3] include(mod::Module, _path::String)
    @ Base ./Base.jl:495
  [4] include(x::String)
    @ MetaQNL.Optimization ~/MetaQNL/src/optimization/optimization.jl:1
  [5] top-level scope
    @ ~/MetaQNL/src/optimization/metainduce_trainer.jl:1
  [6] include(mod::Module, _path::String)
    @ Base ./Base.jl:495
  [7] include(x::String)
    @ MetaQNL.Optimization ~/MetaQNL/src/optimization/optimization.jl:1
  [8] top-level scope
    @ ~/MetaQNL/src/optimization/optimization.jl:20
  [9] include(mod::Module, _path::String)
    @ Base ./Base.jl:495
 [10] include(x::String)
    @ MetaQNL ~/MetaQNL/src/MetaQNL.jl:3
 [11] top-level scope
    @ ~/MetaQNL/src/MetaQNL.jl:12
 [12] include(mod::Module, _path::String)
    @ Base ./Base.jl:495
 [13] _require(pkg::Base.PkgId, env::String)
    @ Base ./loading.jl:2014
 [14] __require_prelocked(uuidkey::Base.PkgId, env::String)
    @ Base ./loading.jl:1812
 [15] #invoke_in_world#3
    @ ./essentials.jl:926 [inlined]
 [16] invoke_in_world
    @ ./essentials.jl:923 [inlined]
 [17] _require_prelocked(uuidkey::Base.PkgId, env::String)
    @ Base ./loading.jl:1803
 [18] macro expansion
    @ ./loading.jl:1790 [inlined]
 [19] macro expansion
    @ ./lock.jl:267 [inlined]
 [20] __require(into::Module, mod::Symbol)
    @ Base ./loading.jl:1753
 [21] #invoke_in_world#3
    @ ./essentials.jl:926 [inlined]
 [22] invoke_in_world
    @ ./essentials.jl:923 [inlined]
 [23] require(into::Module, mod::Symbol)
    @ Base ./loading.jl:1746
in expression starting at /home/mfan/MetaQNL/src/optimization/maxsat_solvers.jl:40
in expression starting at /home/mfan/MetaQNL/src/optimization/metainduce_trainer.jl:1
in expression starting at /home/mfan/MetaQNL/src/optimization/optimization.jl:1
in expression starting at /home/mfan/MetaQNL/src/MetaQNL.jl:3
in expression starting at /home/mfan/MetaQNL/scripts/train.jl:3

Looking at /home/mfan/MetaQNL/src/optimization/maxsat_solvers.jl:40 and the Z3 (and Z3Py) API, the ExprAllocated attribute does not seem to be mentioned. Perhaps does it have something to do with the Z3 solver? Thank you!

[realharryhero]

@yangky11 Could you check this out? Thank you!

[yangky11]

Hi,

Thanks for your interest in our work. I'm happy to take a look. However, due to limited bandwidth, I probably will be able to do that in a week or so.

[yangky11]

It looks like the error is due to some breaking changes in Z3.jl, I just pinned z3@v0.4.3 in a recent commit. Maybe try it out?

[realharryhero]

It works very well from the tests I’ve done so far! Thank you very much for your time and help! :D

On Mon, Jun 3, 2024 at 11:09 PM Kaiyu Yang @.***> wrote:

It looks like the error is due to some breaking changes in Z3.jl https://github.com/ahumenberger/Z3.jl, I just pinned @.*** in a recent commit https://github.com/princeton-vl/MetaQNL/commit/6932ab605a257a23ec2a8aca549ebda65e3e2686. Maybe try it out?

— Reply to this email directly, view it on GitHub https://github.com/princeton-vl/MetaQNL/issues/20#issuecomment-2146484121, or unsubscribe https://github.com/notifications/unsubscribe-auth/A4JCDFCDKSZYOE4IW3OH5NDZFUVWBAVCNFSM6AAAAABIUPGQNWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNBWGQ4DIMJSGE . You are receiving this because you authored the thread.Message ID: @.***>