search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

C-API: Some functions are missing an implementation #295

Closed marcogario closed 8 years ago

marcogario commented 8 years ago

The following functions appear in dreal_c.h but do not have an implementation in dreal_c.cpp:

double dreal_get_bound_lb(dreal_context, dreal_expr);
double dreal_get_bound_ub(dreal_context, dreal_expr);
void dreal_set_bound_lb(dreal_context, dreal_expr, double);
void dreal_set_bound_ub(dreal_context, dreal_expr, double);
void dreal_prefer(dreal_expr a);
void dreal_print_proof(dreal_context, const char *);
void dreal_print_interpolant(dreal_context, const char *);
// This last one has a different signature:
dreal_expr dreal_mk_forall_unbounded_int_var(dreal_context, char const *, long, long);

This is a problem because I am writing a Python wrapper for dReal, and when opening the shared object I get an error that those functions do not exist. I am currently not using any of those, therefore I am not sure whether the solution is to implement them or to remove them from he API.

Using commit 31cff4f761ca9058941f2c20584d205648b1f453

soonho-tri commented 8 years ago

Closed by a1ecbac5017d7d2671dc6acc1e41a141b2d8cb3a and 203c99729dbec7a24b36babe84c527d9eab9d666.

soonho-tri commented 8 years ago
  1. {get,set}_bound_{lb,ub} functions are removed from our internal data structures and now obsolete. I just removed them from C API.

  2. I fixed the following one:

    // This last one has a different signature:
dreal_expr dreal_mk_forall_unbounded_int_var(dreal_context, char const *, long, long);
  3. The other functions -- dreal_prefer, dreal_print_proof, and dreal_print_interpolant -- will be added later.
marcogario commented 8 years ago

Thank you very much for the quick response!

soonho-tri commented 8 years ago

@marcogario, thanks for finding the problems.

BTW, do you plan to open-source the python binding?

marcogario commented 8 years ago

Sure, this will be part of pySMT (http://github.com/pysmt/pysmt) . If you are interested in including them in the main distribution of dReal, I will be very glad to open a PR as soon as I am done. This would be good for us, so that we know that we are in sync. Nevertheless, for some other solvers we keep the bindings in our own repository (e.g., repycudd and pypicosat).

soonho-tri commented 8 years ago

@marcogario, I see. Please feel free to contact me if you find a problem in working on the dReal binding. I'm very happy to help.

I think it's great to have the Python binding inside of dReal repository. But I'll discuss it with other members.

scungao commented 8 years ago

Thanks a lot for the good work @marcogario. We could probably fork pySMT in https://github.com/dreal-deps and create options for people who need it to install it at compile time.