search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
335 stars 62 forks source link

Support lambda terms as SMT-LIB inputs #134

Closed shaobo-he closed 4 years ago

shaobo-he commented 4 years ago

Hello Boolector developers,

I'd like to know if Boolector supports lambda terms (e.g., those model memset/memcpy) in the SMT-LIB input scripts. For example, the following script,

(set-option :produce-models true)
(declare-fun heap ((_ BitVec 8)) (_ BitVec 8))
(declare-fun new-heap ((_ BitVec 8)) (_ BitVec 8))

; simulate memset
(assert (= new-heap
  (lambda ((x (_ BitVec 8)))
    (ite (and (bvule #x00 x) (bvule x #x02))
      #x03
      (heap x)))))

(assert (= (new-heap #x00) #x03))

(check-sat)
(get-model)

CVC4 reports sat on this script but Boolector says lambda is an undefined symbol.

aytey commented 4 years ago

As far as I understand it lambdas are not part of the current SMT-LIB 2.6 standard. There was a presentation last week on SMT-LIB 3.0, which does have lambdas, but that doesn't help you now.

It also seems like there were recent bugs in Z3 about supporting store over lambas: https://github.com/Z3Prover/z3/issues/2898 -- if you try this example with CVC4's master, it doesn't parse.

Anyway, given lambdas aren't part of 2.6, then I doubt Boolector will be changed to support them (see, e.g., https://github.com/Boolector/boolector/issues/119).

edit when you say "CVC4 reports SAT", are you using --uf-ho?

shaobo-he commented 4 years ago

@andrewvaughanj Thank you for your reply. I think my question is addressed so I closed this issue.

edit when you say "CVC4 reports SAT", are you using --uf-ho?

No, I didn't use any command line option.

aytey commented 4 years ago

No, I didn't use any command line option.

Weird. Doesn't work for me without it 🤷

Anyway, glad I "helped" 😂