A Decision Procedure for (Co)datatypes in SMT Solvers - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

A Decision Procedure for (Co)datatypes in SMT Solvers

(1) , (2)


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 theories developed with Isabelle demonstrates the potential of the procedure.
Fichier principal
Vignette du fichier
conf.pdf (178.57 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01212585 , version 1 (07-10-2015)



Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. CADE-25 - The 25th jubilee edition of the International Conference on Automated Deduction, Aug 2015, Berlin, Germany. pp.197-213, ⟨10.1007/978-3-319-21401-6_13⟩. ⟨hal-01212585⟩
104 View
124 Download



Gmail Facebook Twitter LinkedIn More