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 theories developed with Isabelle demonstrates the potential of the procedure.
Document type :
Conference papers
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01212585
Contributor : Jasmin Blanchette <>
Submitted on : Wednesday, October 7, 2015 - 3:22:30 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Friday, January 8, 2016 - 10:15:43 AM

File

conf.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. CADE-25, Aug 2015, Berlin, Germany. ⟨10.1007/978-3-319-21401-6_13⟩. ⟨hal-01212585⟩

Share

Metrics

Record views

185

Files downloads

104