Soonho Kong

- [ ] `BranchRandom` class - [ ] Extend the brancher interface to accept `Config` so that we can pass a random seed - [ ] Add command-line option to...

This is not a standard (yet) but Z3 and optiMathSat support it.

After the strengthening step in searching for counterexamples, equality constraints become `false` and terminate the CE-search prematurely, which results in a pre-mature optimization output. We need to detect the problem...

Related #174, #175, #191 We're using `picosat_{push,pop}` which are experimental. We've already contacted the picosat team but I am not sure that when the problem can be resolved. My plan...

New webpage

1

The current one, http://dreal.github.io , is based on dReal3 and outdated. We need a new one for this version.

Add it in C++/Python

let + forall

4

From https://github.com/dreal/dreal4/pull/78#issuecomment-380218590 Input: ```smt2 (set-logic QF_NRA) (assert (forall ((x Real [0.0, 7.0])) (let ((y (+ x 1))) (>= y (* x 2))))) (check-sat) (exit) ``` Output: ``` Running local dreal...

See https://pybind11.readthedocs.io/en/stable/advanced/misc.html#generating-documentation-using-sphinx Related: https://github.com/dreal/dreal4/issues/100#issuecomment-419631897

- When a solver-status is `unsat` with the current assertions `{φ₁, ..., φₙ}`, adding further assertions `{φₙ₊₁, ...}` should return `unsat` immediately. - When an assertion `φᵢ` is added to...