keep up with the recent MathProgBase.jl API changes

[soonhokong]

@zenna, could you review this PR?

[zenna]

Looks good. I've updated abstract domains too and will push both to Jula METADATA

[soonhokong]

Thanks!

[zenna]

But the tests are failing

[soonhokong]

@zenna, do you have a log? Do you mean the tests at Travis?

[soonhokong]

I found that there's a test failure at Travis. I'll check this after dinner this evening. Please let me know if you have other failures.

[zenna]

Well i'm just running them on my local machine. Pkg.test("DReal") or just run a file in the test directory. I`m looking at ex1.jl now. or ex1capi.jl (which is closer to the c). It returns sat when it should be sat. Calling check again returns unsat. I think we saw a problem like this before.

[zenna]

also opensmt_reset seems to not have any effect.

[zenna]

Which also was an unresolved issue #10

[soonhokong]

OK. I will fix things up this time.

[soonhokong]

@zenna,

It returns sat when it should be sat.

I believe that you meant "it returns UNSAT when it should be sat".

---

I'm looking at test/ex1capi.jl file. Between the push at line 109 and pop line 117, there is no assertions. As a result, at line 118, we still have three constraints in the stack:

leq  : x <=  y
leq2 : y <= z
leq3 : z <= x - 1

Note that the above set of constraints is already UNSAT.

At line 124, we add 4-th constraints leq4 : z <= x. So when we do check_sat at line 128, we are checking a conjunction of the following four constraints:

leq  : x <=  y
leq2 : y <= z
leq3 : z <= x - 1
leq4 : z <= x

So, I think the given UNSAT answer is actually correct. What do you think?

[soonhokong]

@zenna: BTW, you need a new version to get this UNSAT answer. I'll make another release and let DReal.jl point to that version.

In the meantime, it'd be great if you could review code in test/ex1capi.jl and double-check the anticipated result at line 130. For now, it's @test res == 1, and I think that it should be @test res == -1.

[soonhokong]

and because of the same reasoning, I think https://github.com/dreal/DReal.jl/blame/master/test/ex1.jl#L64 should be @test res == false.

[soonhokong]

Other than the two problems, Julia-0.4.5 reports an error at https://github.com/dreal/DReal.jl/blob/master/test/exintfloat.jl#L4-L15.

ERROR: LoadError: LoadError: invalid doc expression:

@doc "..." begin  # /usr0/home/soonhok/.julia/v0.4/DReal/test/exintfloat.jl, line 23:

When I comment them (the docstring starting and ending with """) out, it seems that we have no test failures anymore.

I'll check the reset_global_ctx in the meantime.

[zenna]

Right. But in my current build (I haven't pulled yet) after equation 3 we were getting SAT, returning ([-100 -99],[-98 -97],[-100 100]) for x y z which is clearly wrong, then when called again it would give UNSAT. Is this something you just fixed?

[soonhokong]

Is this something you just fixed?

Yes, this is fixed by https://github.com/dreal/dreal3/commit/ecc7472fe9d8c525b237b4a7ec361f62ce059671. I'll release a new shared library soon.

[soonhokong]

@zenna,

• I've replaced the last assert; push with push; assert.
• Can I switch the docstring in https://github.com/dreal/DReal.jl/blob/master/test/exintfloat.jl#L4-L15 into a comment?

[zenna]

Of course

[zenna]

As for updating I'm not sure that doing Pkg.update() will automatically redownload and the new version. I'll see to that later

[zenna]

I mean it will download the new julia lib but not dreal libraries afaik

[soonhokong]

Of course

Done by https://github.com/dreal/DReal.jl/commit/0a947ad6c0e6a87536bb3d6f3c4d3ac57c84a8de.

I mean it will download the new julia lib but not dreal libraries afaik

At least, in Travis-CI, it checks out the latest version (i.e. dReal-3.16.6). I'll make sure that we have no test failures there. I think we need to publish the new version of DReal.jl to Julia to make Pkg.update fully effective for a normal user. We can do that later when we're sure everything is squared.

[zenna]

Yes, but in Travis we're doing Pkg.add() which calls Pkg.build(), whereas Pkg.update() does not call Pkg.build(). It's Pkg.build() which does the downloading etc. This i imagine is a standard problem and I'm sure there's a standard solution so I just need to find out what that is

[zenna]

Ignore that. I was wrong

[soonhokong]

@zenna, I think I fixed the reset problem. Here are some notes:

• reset command clears not only assertions but also declarations. You need to re-declare variables once you do reset.
• I had to comment out Beales function in test/optimize.jl because this query returns UNSAT. I'll fix this problem and re-enable this piece later.
• Other than that, I've checked that Pkg.test("DReal") returned "Test Pass".
• julia-0.4.5 complains that we're using deprecated Push!(A). Could you check this?

There might be still remaining problems of reset. I'm running regression tests now. If you find any problems, please let me know.

[zenna]

Awesome.

I don't see these deprecation warnings. Any more information?

[soonhokong]

1. I commented out opensmt_set_verbosity when I run the test on my machine.
2. I got two warnings:

 * ode1capi.jl
WARNING: could not import DReal.opensmt_mk_sqrt into Main
WARNING: imported binding for pi overwritten in module Main
...

 * odeball.jl
Made integral constraint
WARNING: push!(A) has been deprecated
 in depwarn at deprecated.jl:73
 in push! at deprecated.jl:439
 in add! at /usr0/home/soonhok/.julia/v0.4/DReal/src/construct.jl:214
 in add! at /usr0/home/soonhok/.julia/v0.4/DReal/src/construct.jl:215
 in include at ./boot.jl:261
 in include_from_node1 at ./loading.jl:320
 [inlined code] from /usr0/home/soonhok/.julia/v0.4/DReal/test/runtests.jl:23
 in anonymous at no file:0
 in include at ./boot.jl:261
 in include_from_node1 at ./loading.jl:320
 in process_options at ./client.jl:280
 in _start at ./client.jl:378
while loading /usr0/home/soonhok/.julia/v0.4/DReal/test/odeball.jl, in expression starting on line 31

• Using julia version 0.4.5, Ubuntu 12.04 (64-bit)
• I run test/runtests.jl from terminal, not by Pkg.test("DReal")

[zenna]

ok I fixed those issues

[zenna]

There's also test/Soonho.jl which causes a crash on my machine. I think I made that a while ago to demonstrate to you. What's the latest on ForAllVar?

[soonhokong]

@zenna, thanks!!

There's also test/Soonho.jl which causes a crash on my machine. I think I made that a while ago to demonstrate to you. What's the latest on ForAllVar?

I'll check them soon!

[soonhokong]

BTW, following many people (incl. you and @scungao ), I finally have a test file named after me... what an honor..

[scungao]

hahaha champagne ordered

[soonhokong]

Build passed on Travis-ci! Thanks, @zenna!

https://travis-ci.org/dreal/DReal.jl

[zenna]

I published it in METADATA. forall1.jl is also showing the same problem as soonho.jl

[soonhokong]

I published it in METADATA.

Great!

forall1.jl is also showing the same problem as soonho.jl

I'll check this one as well.