148 commits

Author	SHA1	Message	Date
Ken McMillan	1e8c04be8e	fixing templates for broken windows hash functions	2013-12-15 17:31:46 -08:00
Ken McMillan	ebc8a43fe3	removing address dependencies	2013-12-15 15:49:06 -08:00
Ken McMillan	3764064e98	fixed some address dependencies	2013-12-13 18:41:35 -08:00
Ken McMillan	2cc8132191	still simplifying quantified interpolants in duality	2013-12-12 18:25:24 -08:00
Ken McMillan	d45cbb3cb2	fixed interpolation bug	2013-12-10 16:26:35 -08:00
Ken McMillan	56b3406ee5	added mbqi.id option, working on quantifiers in duality	2013-12-10 11:41:25 -08:00
Ken McMillan	a3462ba6aa	working on duality	2013-11-27 17:39:49 -08:00
Ken McMillan	a93f8b04e5	working on duality and quantified arithmetic in interpolation	2013-11-21 18:10:21 -08:00
Nikolaj Bjorner	61385c8489	a.ctx -> self.ctx, thanks gario ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2013-11-20 09:54:37 -08:00
Ken McMillan	9cba5d7c85	working on quantifiers in interpolation	2013-11-14 10:18:44 -08:00
Ken McMillan	d73310cfa1	working on eq-propagate rule in interpolation	2013-11-12 12:38:30 -08:00
Ken McMillan	749f95c9d7	handle eq-propagate arithetic rule	2013-11-08 16:18:48 -08:00
Ken McMillan	763ae0d246	removed debugginf message in interpolation	2013-11-07 17:42:18 -08:00
Ken McMillan	a898bad961	fixed two interpolation bugs	2013-11-07 17:38:39 -08:00
Ken McMillan	b076c152b3	adding farkas axiom to interpolation	2013-11-07 16:17:56 -08:00
Ken McMillan	cf176af48e	looking for more farkas rules in interpolation	2013-11-07 15:40:44 -08:00
Ken McMillan	d9c69f5294	handling commutativity rule in interpolation	2013-11-07 15:13:39 -08:00
Ken McMillan	33f941aaec	interpolation fix	2013-11-06 12:20:55 -08:00
Ken McMillan	0696a7ef50	interpolation fix	2013-11-06 11:41:17 -08:00
Ken McMillan	fa05116e66	fixed vc++ compaibility issues	2013-11-05 14:45:44 -08:00
Ken McMillan	f83bca11a0	added interpolation options	2013-11-05 14:20:22 -08:00
Ken McMillan	49c72abb2d	new interpolation fixes; re-added fixedpoint-push/pop	2013-11-05 12:17:09 -08:00
Ken McMillan	7ca6c744fd	added binary interpolation	2013-11-01 15:58:59 -07:00
Ken McMillan	ac212ec54c	fixing interpolation bugs	2013-11-01 11:03:55 -07:00
Ken McMillan	81df4932fb	added quantifiers in new interpolation	2013-10-25 18:40:26 -07:00
Ken McMillan	79b0f83ab3	working on new interpolation	2013-10-25 13:58:56 -07:00
Ken McMillan	3a0947b3ba	merged with unstable	2013-10-18 17:26:41 -07:00
Ken McMillan	4ce39087db	something cl was complaining about	2013-09-15 14:00:45 -07:00
Ken McMillan	12533ad145	Merge /home/mcmillan/projects/z3_interp into interp	2013-09-15 13:40:39 -07:00
Ken McMillan	6091cb1825	fix lemma counting and nix NEW_EXTRACT_TH_LEMMA	2013-09-15 13:40:06 -07:00
Ken McMillan	2c9c5ba1f0	still working on interpolation of full z3 proofs	2013-09-15 13:33:20 -07:00
Ken McMillan	07bb534d65	some duality fixes	2013-08-16 18:38:24 -07:00
Ken McMillan	41f77ab57c	duality abort hack and debugging hacks	2013-06-27 17:29:12 -07:00
Ken McMillan	d8b31773b8	some debugging stuff	2013-06-27 17:27:36 -07:00
Ken McMillan	4d939c07a3	fixed bug in range computation	2013-06-27 11:28:38 -07:00
Ken McMillan	e939dd2bc5	still integrating duality	2013-04-30 13:07:49 -07:00
Ken McMillan	8488ca24d2	first commit of duality	2013-04-20 18:18:45 -07:00
Ken McMillan	e651f45bc0	added sequences to get-interpolant and compute-interpolant	2013-04-09 15:52:30 -07:00
U-REDMOND\kenmcmil	7a0d49cb32	porting to windows	2013-03-28 11:18:20 -07:00
U-REDMOND\kenmcmil	28266786f3	porting to windows	2013-03-27 12:17:52 -07:00
Ken McMillan	78848f3ddd	working on smt2 and api	2013-03-26 17:25:54 -07:00
Ken McMillan	2b93537366	debugging interpolation	2013-03-06 18:26:46 -08:00
Ken McMillan	ae9276ad9b	more work on interpolation	2013-03-05 21:56:09 -08:00
Kenneth McMillan	bc6b20d557	Merge branch 'interp' of https://git01.codeplex.com/z3 into interp	2013-03-04 19:53:53 -08:00
Kenneth McMillan	12d2d3beef	minor fixes for OSX	2013-03-04 19:53:46 -08:00
Ken McMillan	9792f6dd33	more work on incorporating iz3	2013-03-04 18:41:30 -08:00
Kenneth McMillan	e5f5e008aa	fixing file heads to match z3	2013-03-03 21:22:50 -08:00
Ken McMillan	68fb01c206	initial commit for interpolation	2013-03-03 20:45:58 -08:00