Skip to Main content Skip to Navigation
Journal articles

A Decision Procedure for (Co)datatypes in SMT Solvers

Abstract : We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from formalizations developed with Isabelle demonstrates the potential of the procedure.
Document type :
Journal articles
Complete list of metadata

Cited literature [40 references]  Display  Hide  Download

https://hal.inria.fr/hal-01643154
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 21, 2017 - 10:36:25 AM
Last modification on : Monday, July 16, 2018 - 6:36:03 PM

File

jour.pdf
Files produced by the author(s)

Identifiers

Citation

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. Journal of Automated Reasoning, Springer Verlag, 2017, 58 (3), pp.341 - 362. ⟨10.1007/s10817-016-9372-6⟩. ⟨hal-01643154⟩

Share

Metrics

Record views

228

Files downloads

264