dreal3

dreal3 copied to clipboard

[dop] --stat option

1

- time - memory - # of vars - # of generated CEs (via over-approximation) - # of generated CEs (via under-approximation) - # of branches

soonhokong

set-option print-success true has no effect

4

Is there any plan to add print-success? It could be interesting for tools interacting with solvers _via_ system pipes.

AdrienChampion

Sent an email with a report https://gist.github.com/soonhokong/f5cb88085621f37d4a88. Related issue: https://github.com/dreal/dreal/issues/37

soonhokong

Bounded uncontrollable variables in dReal3

10

It is sometimes useful to allow (bounded) uncontrollable variables, such as (continuously provided) input from another component. For example, consider a thermostat system with the flow: ``` d/dt[x] = K...

kquine

nnarodytska

soonhokong

- Need to add problem definition as a header - In dReal2, we have `HOLE`s in a proof to plug in sub-proofs. Need to think about a nicer way of...

soonhokong

something like https://github.com/progschj/ThreadPool

soonhokong

use the protocol established for parallel contractor. send 'terminate' signal after some time.

soonhokong