---
title: "A Decision Procedure for (Co)datatypes in SMT Solvers"
authors:
  - "Andrew Reynolds"
  - "Jasmin Christian Blanchette"
doi: ""
url: "https://ijcai.org/proceedings/2016/631"
pdf: "https://ijcai.org/proceedings/2016/0631.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "4205-4208"
track: ""
keywords:
---

# A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds, Jasmin Christian Blanchette

*Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence*, pages 4205-4208.

## Abstract

Datatypes and codata types are useful to represent finite and potentially infinite objects. We describe a decision procedure to reason about such types. The procedure has been integrated into CVC4, a modern SMT (satisfiability modulo theories) solver, which can be used both as a constraint solver and as an automatic theorem prover. An evaluation based on formalizations developed in the Isabelle proof assistant shows the potential of the procedure.