bazel build //:package collects what we need. After untar the package, we can do:

g++-4.9 --std=c++14 sat_checker.cc                      \
		`pkg-config --cflags --libs ibex`       \
		-I./usr/include -I./usr/include/dreal/  \
		-Lusr/lib -ldreal

TODOs:

• In OSX, we still need to fix the rpath of the generated library. We do this in make_package.sh but should be done inside of bazel.

• In Ubuntu, users need to set LD_LIBRARY_PATH. There is a way to avoid it and we can mention the technique and show it in an exmple.

• Need to set-up dreal.pc (pkg-config) file. So that one can do:

  g++-4.9 --std=c++14 sat_checker.cc `pkg-config --cflags --libs dreal`

• Given f = e1 rop e2, it should return a pair ({VALID, UNSAT, UNKNOWN} x Interval).

• Since IBEX does not handle e1 != e2, we need to add:

    const ibex::ExprNode* Convert(const Expression& e);
  

  to convert e1 - e2 and use it in Evaluator instead of f.

should be replaced with an integer variable with a side constraint \in [0, 1].

When trying to parse this file: uav_dreal_complete.txt
dreal4 errors out while dreal3 works (returns unsat)

possible solution: to use its C++ API

Ubuntu16 + gcc-5

===
npz3@godel:~/src/dreal4$ bazel  build --compiler gcc-5 //...
INFO: Analysed 391 targets (0 packages loaded).
INFO: Found 391 targets...
ERROR: /home/npz3/src/dreal4/test/BUILD:7:1: Linking of rule '//test:ibex_test' failed (Exit 1)
/usr/local/lib/libCoinUtils.so: undefined reference to `dgetrf_'
/usr/local/lib/libCoinUtils.so: undefined reference to `dgetrs_'
collect2: error: ld returned 1 exit status
INFO: Elapsed time: 10.557s, Critical Path: 9.09s
FAILED: Build did NOT complete successfully
===

probably via https://github.com/pybind/pybind11

+sharing

1. fix warnings from --test_verbose_timeout_warnings.
2. add smt2_test, dr_test where we can specify an explicit size.

Need to introduce term instead of having formula and expression at the parsing-level.

We're using NLOPT_LD_SLSQP (see https://nlopt.readthedocs.io/en/latest/NLopt_Algorithms) which is a gradient-based algorithm. Need to change the code to a gradient-free algorithm if a function is non-differentiable.

https://github.com/dreal/dreal4#how-to-use-dreal-as-a-library

Instead of ∃x. ∀y. f(x) <= f(y), we encode a problem into ∃x,z. [z = f(x) ∧ (∀y. z <= f(y))]. Here, z is the newly introduced variable.

I've observed a different behavior of dReal when it's run with valgrind. Here is a self-included example-program showing the issue:

#include <cfenv>
#include <limits>
#include <iostream>
#include <cmath>

using std::cout;
using std::endl;
using std::numeric_limits;

int main() {
  double x = M_PI;
  double y = M_E;
  cout.precision(numeric_limits<double>::max_digits10 + 2);
  fesetround(FE_DOWNWARD);
  cout << (x * y) / x << endl;
  fesetround(FE_UPWARD);
  cout << (x * y) / x << endl;
}

Without valgrind, we have:

2.718281828459044646
2.718281828459045979

With valgrind, we have:

2.71828182845904509
2.718281828459045091

This limitation is actually documented in the manual:

Rounding: Valgrind does observe the 4 IEEE-mandated rounding modes (to nearest, to +infinity, to -infinity, to zero) for the following conversions: float to integer, integer to float where there is a possibility of loss of precision, and float-to-float rounding. For all other FP operations, only the IEEE default mode (round to nearest) is supported.

http://valgrind.org/docs/manual/manual-core.html

For ∀y f(x, y), we will evaluate f(x, y) using the domain of y.
Find a counterexample,!f(a, b) and check ||f(I_x, b)|| < \delta.

See https://gist.github.com/soonho-tri/0b0339d0ef57fa6cf7b16fb83f7c2eae

• ibex/3rd/interval/stdfun/interval
• coinutils/coin (only OSX)

• checking satisfiability of a formula
• constrained/unconstrained optimization

For ceil(e), we can introduce an integer variable i with a constraint e <= i < e + 1. Then substitute ceil(e) with i in expressions.

We can do the similar thing for floor(e): e - 1 < i <= e.

This should eliminate some of false delta-sat results which involves strict inequalities.

There are cases where Nlopt simply hangs. Need to set a timeout. See https://nlopt.readthedocs.io/en/latest/NLopt_Guile_Reference/#stopping-criteria

Changing line 98 to return &ibex::ExprConstant::new_scalar(c); causes memory leaks. I'm investigating the issue.

There is no option to build a static-binary of dReal4 in the bazel build.

Can you provide this feature ?
As an alternate solution, can you provide the static-binary in the Download section?

https://github.com/dreal/dreal4/blob/master/dreal/solver/theory_solver.cc#L102-L109

Given ∃x.∀y.ϕ(x, y), we need to check ∃x.∃y.(¬ϕ(x, y))⁻⁽ᵟ⁺ᵉ⁾. If there is a counterexample, this evaluation should return something bigger than δ so that a branching will happen. If no counterexample is found, it should return 0.0 so that no branching will take place because of this constraint.

TODO

• Add support ite in parser/scanner.
• Add ITE-elim phase: Recursively rewriting F[ite(C, t₁, t₂)] => (C ⇒ F[t₁]) ∧ (C ⇒ F[t₂]).