35 commits

Author	SHA1	Message	Date
Ken McMillan	95146483ea	add round-off to farkas resconstruction in interp	2014-05-13 18:15:51 -07:00
Ken McMillan	c9e9b30af6	interp handle mystery arith lemmas	2014-05-13 17:28:22 -07:00
Ken McMillan	aa35f988fc	fix for bad coefficient in AssignBounds	2014-05-13 14:58:32 -07:00
Ken McMillan	de81db9a3b	fixed several interpolation problems	2014-04-10 17:53:17 -07:00
Ken McMillan	fc62be37b6	getting rid of DOS line endings	2014-04-03 17:09:11 -07:00
Ken McMillan	732035bf63	merge interp/duality changes with unstable	2014-03-26 14:48:04 -07:00
Ken McMillan	663d110b72	interpolation fix	2014-03-16 12:09:53 -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	76fb66314b	interpolation fix for commutativity	2014-02-19 13:56:16 -08:00
Ken McMillan	928d419138	duality fixes	2014-02-17 12:15:11 -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	f380e31a6b	runs the integer/cntrol svcomp examples from the Horn repo	2014-01-09 17:16:10 -08:00
Ken McMillan	48e10a9e2d	dealing with incompleteness issues in duality	2013-12-19 11:05:56 -08:00
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	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	a3462ba6aa	working on duality	2013-11-27 17:39:49 -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	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	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	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