keep up with the recent MathProgBase.jl API changes #23

soonhokong · 2016-06-06T20:47:03Z

@zenna, could you review this PR?

…d, use Union{args...} instead."

Close #22 See http://mathprogbasejl.readthedocs.io/en/latest/nlp.html?highlight=loadnonlinearproblem

zenna · 2016-06-06T22:23:54Z

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

soonhokong · 2016-06-06T22:30:15Z

Thanks!

zenna · 2016-06-06T22:40:05Z

But the tests are failing

soonhokong · 2016-06-06T22:42:37Z

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

soonhokong · 2016-06-06T22:48:29Z

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 · 2016-06-06T22:55:56Z

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 · 2016-06-06T22:57:49Z

also opensmt_reset seems to not have any effect.

zenna · 2016-06-06T22:58:33Z

Which also was an unresolved issue #10

soonhokong · 2016-06-06T23:01:18Z

OK. I will fix things up this time.

soonhokong · 2016-06-08T04:01:39Z

@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 · 2016-06-08T04:05:45Z

@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 · 2016-06-08T04:29:08Z

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 · 2016-06-08T04:37:06Z

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 · 2016-06-08T09:27:41Z

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 · 2016-06-08T11:22:49Z

Is this something you just fixed?

Yes, this is fixed by dreal/dreal3@ecc7472. I'll release a new shared library soon.

Related PR: dreal/DReal.jl#23 (comment)

soonhokong · 2016-06-08T12:14:16Z

@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 · 2016-06-08T12:24:18Z

Of course

zenna · 2016-06-08T12:25:26Z

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 · 2016-06-08T12:25:47Z

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

soonhokong · 2016-06-08T12:44:15Z

Of course

Done by 0a947ad.

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 · 2016-06-08T12:57:38Z

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 · 2016-06-08T14:00:54Z

Ignore that. I was wrong

soonhokong · 2016-06-09T21:13:10Z

@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 · 2016-06-09T23:54:19Z

Awesome.

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

soonhokong · 2016-06-10T00:03:34Z

I commented out opensmt_set_verbosity when I run the test on my machine.
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 · 2016-06-10T00:28:00Z

ok I fixed those issues

zenna · 2016-06-10T00:29:20Z

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 · 2016-06-10T01:01:56Z

@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 · 2016-06-10T01:05:50Z

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

scungao · 2016-06-10T01:07:05Z

hahaha champagne ordered

soonhokong · 2016-06-10T02:27:27Z

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

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

zenna · 2016-06-10T07:53:46Z

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

soonhokong · 2016-06-10T08:19:46Z

I published it in METADATA.

Great!

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

I'll check this one as well.

soonhokong added 2 commits June 6, 2016 16:40

fix(src/construct.jl): suppress "WARNING: Union(args...) is deprecate…

4287516

…d, use Union{args...} instead."

fix(SolverInterface.jl): update to use the latest APIs

04bc633

Close #22 See http://mathprogbasejl.readthedocs.io/en/latest/nlp.html?highlight=loadnonlinearproblem

zenna merged commit e57b16f into dreal:master Jun 6, 2016

soonhokong added a commit to dreal/dreal3 that referenced this pull request Jun 8, 2016

test(c_api): add zenna_{04,05}

af6583e

Related PR: dreal/DReal.jl#23 (comment)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

keep up with the recent MathProgBase.jl API changes #23

keep up with the recent MathProgBase.jl API changes #23

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

zenna commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

soonhokong commented Jun 8, 2016 •

edited

Loading

soonhokong commented Jun 8, 2016 •

edited

Loading

soonhokong commented Jun 8, 2016

soonhokong commented Jun 8, 2016 •

edited

Loading

zenna commented Jun 8, 2016

soonhokong commented Jun 8, 2016

soonhokong commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

soonhokong commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

soonhokong commented Jun 9, 2016

zenna commented Jun 9, 2016

soonhokong commented Jun 10, 2016

zenna commented Jun 10, 2016

zenna commented Jun 10, 2016

soonhokong commented Jun 10, 2016

soonhokong commented Jun 10, 2016

scungao commented Jun 10, 2016

soonhokong commented Jun 10, 2016 •

edited

Loading

zenna commented Jun 10, 2016

soonhokong commented Jun 10, 2016

keep up with the recent MathProgBase.jl API changes #23

keep up with the recent MathProgBase.jl API changes #23

Conversation

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

soonhokong commented Jun 6, 2016

zenna commented Jun 6, 2016

zenna commented Jun 6, 2016

zenna commented Jun 6, 2016

soonhokong commented Jun 6, 2016

soonhokong commented Jun 8, 2016 • edited Loading

soonhokong commented Jun 8, 2016 • edited Loading

soonhokong commented Jun 8, 2016

soonhokong commented Jun 8, 2016 • edited Loading

zenna commented Jun 8, 2016

soonhokong commented Jun 8, 2016

soonhokong commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

soonhokong commented Jun 8, 2016

zenna commented Jun 8, 2016

zenna commented Jun 8, 2016

soonhokong commented Jun 9, 2016

zenna commented Jun 9, 2016

soonhokong commented Jun 10, 2016

zenna commented Jun 10, 2016

zenna commented Jun 10, 2016

soonhokong commented Jun 10, 2016

soonhokong commented Jun 10, 2016

scungao commented Jun 10, 2016

soonhokong commented Jun 10, 2016 • edited Loading

zenna commented Jun 10, 2016

soonhokong commented Jun 10, 2016

soonhokong commented Jun 8, 2016 •

edited

Loading

soonhokong commented Jun 8, 2016 •

edited

Loading

soonhokong commented Jun 8, 2016 •

edited

Loading

soonhokong commented Jun 10, 2016 •

edited

Loading