Wed, 08 Dec 2010 08:33:02 +0100 | boehmes | be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts) | file | diff | annotate |
Tue, 07 Dec 2010 14:53:12 +0100 | boehmes | centralized handling of built-in types and constants; | file | diff | annotate |
Wed, 17 Nov 2010 08:14:56 +0100 | boehmes | use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable) | file | diff | annotate |
Fri, 12 Nov 2010 15:56:11 +0100 | boehmes | preliminary support for newer versions of Z3 | file | diff | annotate |
Wed, 25 Aug 2010 18:36:22 +0200 | wenzelm | renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing; | file | diff | annotate |
Wed, 12 May 2010 23:54:04 +0200 | boehmes | layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable | file | diff | annotate |