QF_BV: "syntax error, unexpected TK_SYM"

[Ayrat Khalimov]

Hi openSMT devs and users,

Does OpenSMT support QF_BV logic?

I encountered the following problem with query in smt2 with QF_BV logic:

./opensmt bitrev0032.smt2

At line 12: syntax error, unexpected TK_SYM, expecting '_'

I also tried to solve this query with Z3 - OK (unsat). So the query should be correct.

(the query was taken from smtlib benchmarks, the same error for other queries from QF_BV folder of smtlib benchmarks)

In the attachment - example QF_BV query in smtlib2 format.

The openSMT version is: 1.0.1 (unsable).

--

Best regards, 

Ayrat Khalimov

[Mike Whalen]

Ayrat,

The bitvector code is in there, but commented out in v1.0.1. I'm
not sure when it is expected to be integrated back into the tool.
Sorry for this non-answer answer ;-).

Mike

Michael Whalen
Program Director, UMSEC
200 Union St. 4-192
Minneapolis, MN 55455
Office: 612-624-5130
Cell: 651-442-8834

> --
> You received this message because you are subscribed to the Google Groups
> "opensmt" group.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to
> opensmt+u...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/opensmt?hl=en.
>

[Roberto Bruttomesso]

Hi Ayrat,

Mike is correct (thanks Mike) -- to bring back to life bit-vectors is
planned for this summer, together with a native unification with an
SMT-based model checker around opensmt

Cheers,
R

--
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70

[linas]

Hi,

On Jun 9, 2:55 am, Roberto Bruttomesso <roberto.bruttome...@gmail.com>
wrote:

> Mike is correct (thanks Mike) -- to bring back to life bit-vectors is
> planned for this summer, together with a native unification with an
> SMT-based model checker around opensmt

I too would be interested in having working SMT-LIB v2.0 and
bitvectors!

In the meantime, is there a suggested work-around? DIMACS format?
I notice that there's code for SMT-LIB 1.2, which does seem to handle
bitvectors, but its stubbed out ...

Also: FYI, the wikipedia article now contains a huge table:
http://en.wikipedia.org/wiki/Satisfiability_modulo_theories

openSMT is now listed in it; please verify for correctness/
completeness.

-- linas