search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.91k stars 262 forks source link

Is there an option to generate constrained Horn clauses? #4580

Closed Columpio closed 1 year ago

Columpio commented 1 year ago

I am looking for an option of the Dafny to extract constraint Horn clauses in smt2 format, so that you could run Spacer on it.

zafer-esen commented 1 year ago

I don't believe there is currently any support for constrained Horn clauses (CHCs) in Dafny / Boogie. The closest thing I could find is this discussion in the Corral repository. It looks like there was support for Duality, but that was dropped.

It might be possible to revive that code in Boogie, but that would probably require a lot of work to get it working with Spacer, as highlighted in that discussion.

Columpio commented 1 year ago

It's a pity. Anyway, thank you for the answer.