Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

std::runtime_error for optimization instance #176

Open
rainoftime opened this issue Mar 21, 2020 · 1 comment
Open

std::runtime_error for optimization instance #176

rainoftime opened this issue Mar 21, 2020 · 1 comment

Comments

@rainoftime
Copy link

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
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant