Hi, I want to add DReal in julia but the package manager couldn't find it:
(@v1.5) pkg> add DReal
ERROR: The following package names could not be resolved:

• DReal (not found in project, manifest or registry)

Info about my environment:

julia> versioninfo()
Julia Version 1.5.3
Commit 788b2c77c1 (2020-11-09 13:37 UTC)
Platform Info:
OS: Linux (x86_64-pc-linux-gnu)
CPU: Intel(R) Core(TM) i7-10610U CPU @ 1.80GHz
WORD_SIZE: 64
LIBM: libopenlibm
LLVM: libLLVM-9.0.1 (ORCJIT, skylake)
Environment:
JULIA_NUM_THREADS = 4

a = Var(Int)
b = Var(Int)
c = Var(Int)

add!(((a^b) * c + 10*a + b) == 1)
add!((a < 10) & (b < 10))
add!(c == 5)


is_satisfiable()
false

but (0, 1, 5) is a solution.

Dear @zenna,

While testing the Julia interface, I've found a robustness problem. When I declare a variable twice, it terminates the whole Julia shell:

julia> x = Var(Int,"x")
opensmt_mk_int_var: x = [-9223372036854775808, 9223372036854775807]
# OpenSMTContext::Declaring function x of sort () Int
# Error: symbol already declared  x (triggered at /usr0/home/soonhok/work/dreal3/src/opensmt/egraph/EgraphStore.C, 653)

I think it should return the previously declared variable, possibly update the domain with new information. Do you agree? If so, I can make this change.

Do you see any other robustness issues? Please feel free to enumerate them here, I'll fix them later.

Everything is installed correctly on my Ubuntu 16.04.4 machine, using Julia version 0.6.2.

In the Julia REPL, I encounter the following issue:

julia> using DReal
julia> x = Var(Int, "x")
ERROR: UndefVarError: Var not defined

Any ideas?

@soonhokong Calling opensmt_check switches between true and false without any constraints being added.

using dReal
beale(x::Array) =  (1.5 - x[1] + x[1]x[2])^2 +
                (2.25 - x[1] + x[1]x[2]^2)^2 +
                (2.625 - x[1] + x[1]x[2]^3)^2
x = Var(Float64,"x",-5.12,5.12)
y = Var(Float64,"y",-5.12,5.12)
f = Var(Float64,"f",-10.,10.)
constraint = beale([x,y])
print(constraint)
add!(f == constraint)
@show is_satisfiable()
@show is_satisfiable()

(+ (^ (+ (* (^ y 3) x) (+ 2.625 (* -1 x))) 2) (+ (^ (+ (* (^ y 2) x) (+ 2.25 (* -1 x))) 2) (^ (+ (* y x) (+ 1.5 (* -1 x))) 2)))
is_satisfiable() => true
is_satisfiable() => false

Add bindeps to do automatic installation of binaries.

@scungao was correctly surprised the Boolean types work because actually they don't seem to be. The C-API gives back a=1,b=1 for a formula not a or not b. Any thoughts @soonhokong?

using dReal
using Base.Test
a = Var(Bool,"a")
b = Var(Bool,"b")
add!(!a | !b)
model_a,model_b =  model(a,b)
@test !model_a | !model_b

@zenna, FYI, I'm investigating this issue. It works fine with the released version (2015 Mar).

using dReal
x = Var(Int,"x")
y = Var(Int,"y")
add!((x > 2) & (y < 10) & (x + 2*y == 7))
is_satisfiable()

As described in https://discourse.julialang.org/t/ann-plans-for-removing-packages-that-do-not-yet-support-1-0-from-the-general-registry/ we are planning on removing packages that do not support 1.0 from the General registry. This package has been detected to not support 1.0 and is thus slated to be removed. The removal of packages from the registry will happen approximately a month after this issue is open.

To transition to the new Pkg system using Project.toml, see https://github.com/JuliaRegistries/Registrator.jl#transitioning-from-require-to-projecttoml.
To then tag a new version of the package, see https://github.com/JuliaRegistries/Registrator.jl#via-the-github-app.

If you believe this package has erroneously been detected as not supporting 1.0 or have any other questions, don't hesitate to discuss it here or in the thread linked at the top of this post.

A reference: https://github.com/JuliaLang/BinDeps.jl

FYI, dReal.jl requires the following five shared libraries now:

• libprim.so : filibxx, LGPL2
• libClp.so: Coin-or Linear Programming, EPL
• libibex.so : IBEX, LGPL3
• libcapd.so : CAPD4.0, GPL3
• libdreal.so : dReal, GPL3

@zenna and @iamed2, let's finish the integration here.

@scungao and @soonhokong . I added a function for binary-search based optimisation in dReal(in dReal.jl/src/optimize.jl and there are examples in /test). If you would like any enhancements or changes, we can discuss them here.

@soonhokong I tried Installing dReal.jl using the shared lib tar as per the instructions in the Readme and get an unable to load shared libraries. On closer inspection:

julia> compat_dlopen("libprim.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
Ptr{Void} @0x000000000959ea40

julia> compat_dlopen("libClp.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
ERROR: could not load module libClp.so: /usr/lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.20' not found (required by /home/zenna/Downloads/dReal-3.15.05-linux/lib/libCoinUtils.so.0)
 in dlopen at c.jl:17

julia> compat_dlopen("libibex.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
ERROR: could not load module libibex.so: /usr/lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.20' not found (required by /home/zenna/Downloads/dReal-3.15.05-linux/lib/libibex.so)
 in dlopen at c.jl:17

julia> compat_dlopen("libgflags.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
ERROR: could not load module libgflags.so: /usr/lib/x86_64-linux-gnu/libstdc++.so.6: version `CXXABI_1.3.8' not found (required by /home/zenna/Downloads/dReal-3.15.05-linux/lib/libgflags.so)
 in dlopen at c.jl:17

julia> compat_dlopen("libglog.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
ERROR: could not load module libglog.so: libunwind.so.7: cannot open shared object file: No such file or directory
 in dlopen at c.jl:17

julia> compat_dlopen("libcapd.so", RTLD_LAZY|RTLD_DEEPBIND|RTLD_GLOBAL)
Ptr{Void} @0x000000000653ab70

Very cool to see this hooked up through MathProgBase. I'm not familiar at all with SMT solvers, could you explain or point me to a reference on which classes of problems DReal can solve? Can it solve nonconvex problems to a global optimum?

Also, let us know of any difficulties you've had with the MathProgBase interface and if there are structures which you'd like to communicate which aren't currently supported. I'm guessing that the boolean logic aspect is missing.

CC @IainNZ @joehuchette @tkelman

The problem description and code that produces the correct solution is at https://gist.github.com/sbromberger/252b011d628d20c21afb.

The implementation using DReal is at https://gist.github.com/sbromberger/1b982453ce5497c88b80

I get the following result:

julia> @time is_satisfiable()
944.193124 seconds (1.82 k allocations: 99.145 KB)
false

The correct solution is

[a,b,c,d,e,f,g,h,j,k,l,m,n,p,q,r] == [9,12,16,15,11,2,1,10,4,3,6,8,5,7,13,14]

julia> using dReal

julia> x = Var(Int,"x")
Ex{Int64}(Ptr{Void} @0x00000000078b1ec0,Set{ASCIIString}({"x"}))

julia> y = Var(Int,"y")
Ex{Int64}(Ptr{Void} @0x000000000727ae30,Set{ASCIIString}({"y"}))

julia> add!((x > 2) & (y < 10) & (x + 2*y == 7))
ERROR: ccall: could not find function opensmt_mk_num in library libdreal
in > at /home/evan/.julia/v0.3/dReal/src/construct.jl:32
in > at /home/evan/.julia/v0.3/dReal/src/construct.jl:41

see #3 (comment)

Hi,
I just installed dreal (using the instructions here: http://dreal.github.io/) and DReal.jl (using the instructions at https://github.com/dreal/DReal.jl) and the installation went smooth. However, when I tried using DReal, I got a bunch of errors:
ERROR: LoadError: LoadError: UndefVarError: model not defined
in include at /Applications/Julia-0.4.5.app/Contents/Resources/julia/lib/julia/sys.dylib
in include_from_node1 at /Applications/Julia-0.4.5.app/Contents/Resources/julia/lib/julia/sys.dylib
in include at /Applications/Julia-0.4.5.app/Contents/Resources/julia/lib/julia/sys.dylib
in include_from_node1 at /Applications/Julia-0.4.5.app/Contents/Resources/julia/lib/julia/sys.dylib
in require at /Applications/Julia-0.4.5.app/Contents/Resources/julia/lib/julia/sys.dylib
while loading /Users/dvij/.julia/v0.4/DReal/src/SolverInterface.jl, in expression starting on line 42
while loading /Users/dvij/.julia/v0.4/DReal/src/DReal.jl, in expression starting on line 84

I'm using MacOSX El Capitan on a 64 bit MacBook Pro.

Any ideas on how to fix this?

Thanks,
Dj