34 commits

Author	SHA1	Message	Date
Ken McMillan	3d2ef8bb4a	fix for issue #109	2015-05-27 16:05:40 -07:00
Ken McMillan	caa616f11b	fix for github issue 83	2015-05-20 15:37:51 -07:00
Ken McMillan	ccc1f02216	fix for github issue 54	2015-05-19 18:47:13 -07:00
Ken McMillan	af444beb2e	re-indenting interp and duality	2015-04-15 12:22:50 -07:00
Ken McMillan	d42e3ce651	possible header problem for std::less	2015-04-02 13:10:23 -07:00
Ken McMillan	a6f58bdd17	fixes and performance improvements for interp and duality	2014-10-30 17:22:34 -07:00
Ken McMillan	c9e9b30af6	interp handle mystery arith lemmas	2014-05-13 17:28:22 -07:00
Ken McMillan	acf4ad0ab6	use new hashtable implementation in windows	2014-02-27 17:23:19 -08:00
Ken McMillan	75bb495585	merging interpolation and duality changes into unstable	2014-02-19 15:36:16 -08:00
Ken McMillan	f45ad4bdc0	disable silly warnings and add needed header for VS	2014-02-10 12:56:39 -08:00
Ken McMillan	ba193a59b1	some interpolation fixes, plus some options to remove features for testing in duality	2014-02-09 16:04:02 -08:00
Ken McMillan	466c35100d	Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable	2014-01-28 11:28:24 -08:00
Christoph M. Wintersteiger	f111dd4e61	Fixes for the build on OS X 10.9	2014-01-28 14:00:42 +00:00
Ken McMillan	f380e31a6b	runs the integer/cntrol svcomp examples from the Horn repo	2014-01-09 17:16:10 -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	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
Ken McMillan	749f95c9d7	handle eq-propagate arithetic rule	2013-11-08 16:18:48 -08: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	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	8488ca24d2	first commit of duality	2013-04-20 18:18:45 -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
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