dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
150 stars 31 forks source link

std::runtime_error for optimization instance #176

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Hi, for the following optimization instance,

(set-logic QF_NRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const r0 Real)
(declare-const r6 Real)
(declare-const r7 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const v19 Bool)
(declare-const r10 Real)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const r11 Real)
(declare-const v27 Bool)
(assert (or v5 v18 v18))
(assert (or v19 v12 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(assert (or (or v5 v15 v14 v6 v13 v27 v3 v15) v17 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(assert (or v5 (or v5 v15 v14 v6 v13 v27 v3 v15) v2))
(assert (or v7 v5 v17))
(assert (or v7 v7 v2))
(assert (or v12 v19 v18))
(assert (or v7 v2 v17))
(assert (or v17 v18 v7))
(assert (or v12 v17 (>  3.0 7413753.0)))
(assert (or (>  3.0 7413753.0) (or v5 v15 v14 v6 v13 v27 v3 v15) v5))
(assert (or (>=  r9 (/ 0.323 r9)) v5 (or v5 v15 v14 v6 v13 v27 v3 v15)))
(minimize r0)
(maximize r6)
(minimize r8)
(maximize r9)
(check-sat)

dreal4 (Commit 0780274) throws an assertion violation

terminate called after throwing an instance of 'std::runtime_error'
  what():  Variable v2_ is of type BOOLEAN and it should not be used to construct a symbolic expression.
Aborted (core dumped)

Strangely, after removing the last objective (maximize r9), dreal can work well.

rainoftime commented 4 years ago

If there are Boolean variables, and the real invariable occurs in the assertion, then there will be this error