Need help with running SMTLIB example

Question

Need help with running SMTLIB example

Kakadu opened this issue 4 years ago · 7 comments

I have issues with running my example in SMTLIB format with boolector. I'm using version 3.2.1. Z3 works fin on this

✗ cat demo_smt/2.smt2
(declare-fun a () (_ BitVec 4))
(declare-fun b () (_ BitVec 4))

(assert (exists ((x (_ BitVec 4))) (bvult a  (bvshl b x))))


(apply (using-params qe :qe-nonlinear true))

✗ boolector --smt1 demo_smt/2.smt2
[btor>main] CAUGHT SIGNAL 11
unknown
[1]    19121 segmentation fault  boolector --smt1 demo_smt/2.smt2

✗ boolector --smt2 demo_smt/2.smt2
boolector: demo_smt/2.smt2:7:2: expected command at 'apply'

✗ z3 demo_smt/2.smt2              
(goals
(goal
  (let ((a!1 (not (bvule (concat ((_ extract 1 0) b) #b00) a)))
        (a!2 (not (bvule (concat ((_ extract 0 0) b) #b000) a)))
        (a!3 (not (bvule (concat ((_ extract 2 0) b) #b0) a))))
    (or (not (bvule b a)) a!1 a!2 a!3))
  :precision precise :depth 1)
)

Please, help!

Answer 1 · 2021-04-14T14:27:14.000Z

(apply is a non-standard "Z3 extension" to allow you to specify the "tactics" you wish to use when solving -- you shouldn't (blindly) expect it to be supported by other solvers.

You can probably just remove this when solving with Boolector to get the outcome you want (as long as that outcome is sat/unsat).

Answer 2 · 2021-04-14T15:13:23.000Z

@andrewvaughanj, in my case I want boolector to eliminate quantifiers in the formula. Is it possible to do this without diving into C?

Answer 3 · 2021-04-14T15:55:06.000Z

"Quantifier elimination" is an "implementation specific" behaviour -- yes, you can ask Z3 upfront to eliminate quantifiers from the formula via Z3's SMTLIB extensions, but that doesn't mean that all SMT solvers that support SMTLIB will support that behaviour.

You can take a look at some of Boolector's options for quantifiers here:

https://boolector.github.io/docs/cboolector_options.html

Answer 4 · 2021-04-14T16:29:19.000Z

It's sad that boolector doesn't support this out of box.

Answer 5 · 2021-04-14T16:48:32.000Z

@Kakadu sorry if this is a silly question, but why do you care how an instance is solved as long as it is solved?

This is genuinely out of curiosity; as a user of Boolector, I only care about "knobs and switches" when things aren't going how I'd like -- for 99.99% of the rest of the time, I just treat it like a black-box.

Answer 6 · 2021-04-14T17:53:24.000Z

It's Ph.D.-related. I have an approach which tends to synthesize short stuff (formulas in our case) earlier, and I want to apply it to quantifier elimination problem in the domain of bitvectors. (I hope it will work better then bitblasting) I tried Z3+SMTLIB, I know somebody who did it with boolector+C, maybe I will manage CVC4 to do it too. If you have a good test suite for this kind of a problem somewherre, it will be appreciated.

…

***@***.***(https://github.com/Kakadu) sorry if this is a silly question, but why do you care how an instance is solved as long as it is solved? This is genuinely out of curiosity; as a user of Boolector, I only care about "knobs and switches" when things aren't going how they'd like -- for 99.99% of the rest of the time, I just treat it like a black-box. — You are receiving this because you were mentioned. Reply to this email directly, [view it on GitHub](#171 (comment)), or [unsubscribe](https://github.com/notifications/unsubscribe-auth/AADK7UXBNU2INPAEMHNS4WLTIXBO7ANCNFSM425MRU2Q).

Answer 7 · 2021-04-14T18:24:06.000Z

Boolector does not implement any quantifier elimination techniques and there are also no plans to add some in the future.