129 commits

Author	SHA1	Message	Date
Ken McMillan	fcada914d5	duality fix	2014-03-26 14:10:21 -07:00
Ken McMillan	fb2caf99e6	duality fix	2014-03-21 10:35:33 -07:00
Nikolaj Bjorner	88df909a6c	merge with unstable ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2014-03-20 14:09:18 -07:00
Ken McMillan	3e91037a4d	duality fixes	2014-03-19 12:37:05 -07:00
Ken McMillan	2417b75d8d	duality: added restarts	2014-03-16 15:37:19 -07:00
Ken McMillan	675820ff67	merged changes from linux	2014-03-14 14:51:39 -07:00
Ken McMillan	bbab6be280	duality: eager deduction and history-based conjectures	2014-03-14 13:40:31 -07:00
Ken McMillan	180f55bbda	adding support for non-extensional arrays in duality	2014-03-11 18:20:42 -07:00
Ken McMillan	83a774ac79	duality fix plus mbqi option	2014-03-04 18:38:08 -08:00
Ken McMillan	acf4ad0ab6	use new hashtable implementation in windows	2014-02-27 17:23:19 -08:00
Ken McMillan	08d892bbdb	interpolation fixes	2014-02-27 17:21:47 -08:00
Christoph M. Wintersteiger	d51d9b18f9	Bugfixes for compilation in Cygwin (WIN32 -> _WINDOWS) ... Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>	2014-02-21 13:00:02 +00:00
Ken McMillan	75bb495585	merging interpolation and duality changes into unstable	2014-02-19 15:36:16 -08:00
Ken McMillan	65c54b87d0	duality fix	2014-02-19 13:57:27 -08:00
Ken McMillan	928d419138	duality fixes	2014-02-17 12:15:11 -08:00
Ken McMillan	cb3dc63e68	some interpolation fixes; make duality a bit more persistent in checking interpolant	2014-02-14 15:52:07 -08:00
Nikolaj Bjorner	c42ee3bb01	Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt	2014-02-11 15:44:12 -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	19830bcd33	fix a few warnings	2014-01-28 11:43:00 -08:00
Ken McMillan	f380e31a6b	runs the integer/cntrol svcomp examples from the Horn repo	2014-01-09 17:16:10 -08:00
Nikolaj Bjorner	23e811d136	merge with unstable ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2014-01-05 20:44:56 -08:00
Ken McMillan	11ba2178a9	speeding up interpolation in RPFP_caching	2013-12-24 17:20:12 -08:00
Ken McMillan	1b9f1ea6b3	remove assert on failed label compuation in duality	2013-12-23 11:47:24 -08:00
Ken McMillan	673ba137e5	added qe_lite preprocessing pass to duality	2013-12-23 11:17:38 -08:00
Ken McMillan	9e88691c69	optimizing solver performance in duality	2013-12-22 18:33:40 -08:00
Ken McMillan	c98b853917	speeding up Generalize and adding Lazy Propagation	2013-12-21 16:54:35 -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	852f53d6a6	fixed memory error	2013-12-15 17:24:51 -08:00
Ken McMillan	ebc8a43fe3	removing address dependencies	2013-12-15 15:49:06 -08:00
Ken McMillan	eee2d7af94	porting to linux	2013-12-14 12:47:02 -08:00
Ken McMillan	3764064e98	fixed some address dependencies	2013-12-13 18:41:35 -08:00
Ken McMillan	bb61f17989	trying to figure out address dependency	2013-12-13 13:45:40 -08:00
Ken McMillan	ac9a7748e8	trying to fix address depedency in duality_solver.cpp	2013-12-13 13:14:04 -08:00
Ken McMillan	0449598530	fussing more with qe in duality	2013-12-13 12:41:51 -08:00
Ken McMillan	a410e7f716	fussing with qe in duality	2013-12-13 12:21:54 -08:00
Ken McMillan	bfa6c99676	still trying to get stl to work	2013-12-12 18:38:09 -08:00
Ken McMillan	cf3ede92ad	fix for broken windows stl	2013-12-12 18:35:43 -08:00
Ken McMillan	2cc8132191	still simplifying quantified interpolants in duality	2013-12-12 18:25:24 -08:00
Ken McMillan	ea8eb74744	simplifying quantified interpolants in duality	2013-12-11 16:25:59 -08:00
Ken McMillan	d45cbb3cb2	fixed interpolation bug	2013-12-10 16:26:35 -08:00
Ken McMillan	7043386915	enabled extensional arrays in duality and added theory axioms lazily in GreedyReduce	2013-12-10 14:34:14 -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	8320144af0	fixed bug in duality logging	2013-11-15 11:24:02 -08:00
Ken McMillan	c4f7b4d0d4	remove duality junk on stdout	2013-11-09 13:55:01 -08:00
Ken McMillan	12533ad145	Merge /home/mcmillan/projects/z3_interp into interp	2013-09-15 13:40:39 -07:00
Ken McMillan	07bb534d65	some duality fixes	2013-08-16 18:38:24 -07:00