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.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Andrew Reynolds, Jasmin Christian Blanchette
• Keywords: CADE 2015, Logical Reasoning