Support for "Bool" sorts?

[danbryce]

Should I expect dReal to support Boolean variables? The following SMT2 returns unsat:

(set-logic QF_NRA_ODE) (declare-fun a () Bool) (declare-fun b () Bool) (assert (or a b)) (check-sat) (exit)

[soonhokong]

It does support (bounded) Int sorts and you can encode binary variables using them..

[danbryce]

That is what I suspected. I'm surprised it doesn't "just work". If OpenSMT supports Bool, then the rest of dReal shouldn't even be aware of the Bool variables. I would imagine that only MiniSAT cares.

[scungao]

I thought we do have the Bool sort.

On Jan 13, 2015, at 19:13, Daniel Bryce notifications@github.com wrote:

That is what I suspected. I'm surprised it doesn't "just work". If OpenSMT supports Bool, then the rest of dReal shouldn't even be aware of the Bool variables. I would imagine that only MiniSAT cares.

— Reply to this email directly or view it on GitHub.

[soonhokong]

I also remember it worked with Bool sorts.

For this example, we have "Unfeasibility detected before solving" from realpaver side. I guess it's because it detects no variables and constraints.

[danbryce]

I had a problem with several numeric constraints and booleans. When looking at the debugging it appeared that the sat solver was only deciding the numeric literals and not the Boolean ones. It's as if it replaced booleans by logic true.

Dan

On Jan 13, 2015, at 7:27 PM, Soonho Kong notifications@github.com wrote:

I also remember it worked with Bool sorts.

For this example, we have "Unfeasibility detected before solving" from realpaver side. I guess it's because it detects no variables and constraints.

— Reply to this email directly or view it on GitHub.

[scungao]

Could you put the example here or send to us?

On Jan 13, 2015, at 20:34, Daniel Bryce notifications@github.com wrote:

I had a problem with several numeric constraints and booleans. When looking at the debugging it appeared that the sat solver was only deciding the numeric literals and not the Boolean ones. It's as if it replaced booleans by logic true.

Dan

On Jan 13, 2015, at 7:27 PM, Soonho Kong notifications@github.com wrote:

I also remember it worked with Bool sorts.

For this example, we have "Unfeasibility detected before solving" from realpaver side. I guess it's because it detects no variables and constraints.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

[danbryce]

(set-logic QF_NRA_ODE) (declare-fun time_0 () Real) (declare-fun time_1 () Real) (declare-fun duration_generate_gen_time_0 () Real) (declare-fun generate_gen_start_time_0 () Bool) (declare-fun duration_generate_gen_time_1 () Real) (declare-fun generate_gen_end_time_1 () Bool) (declare-fun refueling_gen_time_0 () Bool) (declare-fun generator-ran_time_0 () Bool) (declare-fun refueling_gen_time_1 () Bool) (declare-fun generator-ran_time_1 () Bool) (declare-fun fuellevel_gen_time_0 () Real) (declare-fun fuellevel_gen_time_1 () Real) (declare-fun fuellevel_gen () Real) (declare-fun capacity_gen_time_0 () Real) (declare-fun capacity_gen_time_1 () Real) (declare-fun capacity_gen () Real) (declare-fun gamma_generate_gen_fuellevel_gen_time_0 () Real) (declare-fun gamma_generate_gen_fuellevel_gen_time_1 () Real) (declare-fun gamma_generate_gen_fuellevel_gen () Real) (define-ode flow_0 ((= d/dt[fuellevel_gen](+ gamma_generate_gen_fuellevel_gen))(= d/dt[capacity_gen] 0)(= d/dt[gamma_generate_gen_fuellevel_gen] 0))) (assert (<= 0 time_0)) (assert (<= time_0 1000)) (assert (<= 0 time_1)) (assert (<= time_1 1000)) (assert (<= 0 duration_generate_gen_time_0)) (assert (<= duration_generate_gen_time_0 1000)) (assert (<= 0 duration_generate_gen_time_1)) (assert (<= duration_generate_gen_time_1 1000)) (assert (<= -10000 fuellevel_gen_time_0)) (assert (<= fuellevel_gen_time_0 10000)) (assert (<= -10000 fuellevel_gen_time_1)) (assert (<= fuellevel_gen_time_1 10000)) (assert (<= -10000 fuellevel_gen)) (assert (<= fuellevel_gen 10000)) (assert (<= -10000 capacity_gen_time_0)) (assert (<= capacity_gen_time_0 10000)) (assert (<= -10000 capacity_gen_time_1)) (assert (<= capacity_gen_time_1 10000)) (assert (<= -10000 capacity_gen)) (assert (<= capacity_gen 10000)) (assert (and

(= fuellevel_gen_time_0 1000)(= capacity_gen_time_0 1600)

(or (and (generator-ran_time_0))(and (generator-ran_time_1)))

(=> (generate_gen_start_time_0) (= duration_generate_gen_time_0 1000))

(=> (and (generate_gen_start_time_0) (generate_gen_end_time_1)) (= (- time_1 time_0) (duration_generate_gen_time_0)))

(=> (and (generate_gen_end_time_1) (generate_gen_start_time_0)) (forall_t 0 [time_0 time_1](>= fuellevel_gen 0)))

(=> (and (or (generate_gen_start_time_0)) (or (generate_gen_end_time_1))) (= (gamma_generate_gen_fuellevel_gen_time_0) 1))

(=> (generate_gen_start_time_0) (or (generate_gen_end_time_1)))

(=> (generate_gen_end_time_1) (or (generate_gen_start_time_0)))

(= [fuellevel_gen_time_1 capacity_gen_time_1 gamma_generate_gen_fuellevel_gen_time_1 ](integral time_0 time_1 [fuellevel_gen_time_0 capacity_gen_time_0 gamma_generate_gen_fuellevel_gen_time_0 ] flow_0))

(<= time_0 time_1)

)) (check-sat) (exit)