Implementing polymorphism in SMT solvers
SMT '08/BPR '08 Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pp. 1-5, 2008.
polymorphic constraintmatching modulesmt solverstype variablesmt solverMore(6+)
Based on our experience with the development of Alt-Ergo, we show the small number of modifications needed to bring parametric polymorphism to our SMT solver. The first one occurs in the typing module where unification is now necessary for solving polymorphic constraints over types. The second one consists in extending triggers' definitio...More
Full Text (Upload PDF)
PPT (Upload PPT)