A Decision Procedure for (Co)datatypes in SMT Solvers

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.


Editor(s):
Felty, Ap
Middeldorp, A
Published in:
Automated Deduction - Cade-25, 9195, 197-213
Presented at:
25th International Conference on Automated Deduction (CADE), Berlin, GERMANY, AUG 01-07, 2015
Year:
2015
Publisher:
Berlin, Springer-Verlag Berlin
ISSN:
0302-9743
ISBN:
978-3-319-21401-6
978-3-319-21400-9
Laboratories:




 Record created 2015-12-02, last modified 2018-09-13


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)