Closed soonhokong closed 9 years ago
2015 May version gives unsat
for this example. I've added a C version of the same example: https://github.com/dreal/dreal3/blob/master/src/tests/c_api/dreal_jl_01.c. It gives the right result (sat).
@soonhokong To fix this I tried to build the latest dReal (using build_dreal_only.sh) but get errors on compilation when it gets to building JSON stuff:
src/json.hpp:1286:44: error: no matching function for call to ‘std::vector<nlohmann::basic_json<> >::erase(__gnu_cxx::__normal_iterator<const nlohmann::basic_json<>*, std::vector<nlohmann::basic_json<> > >&)’
Whole error log is here https://gist.github.com/zenna/af996a4aeb997805d695
I had the same issue and reported it to https://github.com/nlohmann/json/issues/68. I updated https://github.com/dreal-deps/json to avoid the problem. Please do the following in the build directory:
rm -rf external/src/JSON*
rm -rf external/tmp/JSON*
make
If you still have a problem, please let me know.
Still getting the JSON error. Did you push your changes?
On 4 May 2015 at 19:19, Soonho Kong notifications@github.com wrote:
I had the same issue and reported it to nlohmann/json#68 https://github.com/nlohmann/json/issues/68. I updated https://github.com/dreal-deps/json to avoid the problem. Please do the following in the build directory:
rm -rf external/src/JSON rm -rf external/tmp/JSON make
If you still have a problem, please let me know.
— Reply to this email directly or view it on GitHub https://github.com/dreal/dReal.jl/issues/2#issuecomment-98882854.
I did something but it seems that it's not enough. Could you try to install g++-4.9 and use it? I found that that can be a workaround. If you're using Ubuntu, it is available via apt-get.
I found some problems when we handle unbounded problems. I think solving that problem will resolve this issue.
@zenna, could you take a look at my patch https://github.com/soonhokong/dReal.jl/commit/e2a180d5a93d441fcf959b55f7857f3c991ece18?
We have a mismatch between the C function declaration for opensmt_mk_int_var
and Julia's interface. Recently, I've changed opensmt_mk_int_var
to take long
arguments while Julia's interface is still expecting Cint
. As a result, when we pass [intmin, intmax]
to C API, the values got type casted and end up with empty
interval.
Looks good. Yes I should have fixed this earlier. Did this fix the issue?
For this particular example, yes, it fixed the problem. I haven't tested other examples, yet.
Dear @zenna,
For the first item, I just updated README.md by https://github.com/dreal/dReal.jl/commit/a28615c9d7cc12484026b93c4eaff7f3ba899487.
Yes. Merge them. Feel free to commit to directly to master.
On 6 May 2015 at 09:54, Soonho Kong notifications@github.com wrote:
For the first item, I just updated README.md by a28615c https://github.com/dreal/dReal.jl/commit/a28615c9d7cc12484026b93c4eaff7f3ba899487 .
— Reply to this email directly or view it on GitHub https://github.com/dreal/dReal.jl/issues/2#issuecomment-99471187.
Fixed by 1d340f62096b69c3161367ab9b4cdde1e1f8c443.
@zenna, FYI, I'm investigating this issue. It works fine with the released version (2015 Mar).