src/HOL/SMT/Tools/z3_interface.ML
Wed, 12 May 2010 23:53:57 +0200 boehmes added new SMT translation files which use a simpler intermediate term representation and a simpler translation of builtin symbols, have less overhead for renaming symbols and generating the signature, add come with a simpler separation of formulas and terms
Wed, 07 Apr 2010 20:40:42 +0200 boehmes shortened interface (do not export unused options and functions)
Tue, 16 Feb 2010 16:20:34 +0100 boehmes include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
Tue, 20 Oct 2009 14:22:02 +0200 boehmes eliminated extraneous wrapping of public records,
Fri, 18 Sep 2009 18:13:19 +0200 boehmes added new method "smt": an oracle-based connection to external SMT solvers
less more (0) tip