Tue, 26 Oct 2010 11:39:26 +0200 boehmes keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
Sun, 19 Sep 2010 11:33:39 +0200 boehmes properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
Mon, 13 Sep 2010 06:02:47 +0200 boehmes added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
less more (0) tip