19292 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Jakob Rath	f321811b18	fix line endings	2023-07-20 17:40:20 +02:00
Jakob Rath	ef337f3a3f	shortcut in merge	2023-07-20 17:28:37 +02:00
Jakob Rath	3e23742bcf	mk_concat	2023-07-20 17:27:55 +02:00
Jakob Rath	b725b61c57	inv	2023-07-20 17:26:32 +02:00
Jakob Rath	e45d13ffdf	refactor creation of concat nodes	2023-07-20 17:11:01 +02:00
Jakob Rath	4b3cfa8c50	Add recognizers for different kinds of enodes	2023-07-20 17:06:23 +02:00
Jakob Rath	6d00d18ee4	use universal reference	2023-07-20 17:03:38 +02:00
Jakob Rath	e533c6c78d	extract method add_equation	2023-07-20 15:21:22 +02:00
Jakob Rath	4142201d88	fix disequality conflict shortcut	2023-07-20 15:10:58 +02:00
Jakob Rath	ec4be975ee	no need to handle both x=y and y=x	2023-07-20 14:54:21 +02:00
Jakob Rath	73757e3fa4	mk_extract	2023-07-19 19:37:21 +02:00
Jakob Rath	69e54b62c5	no need to store bit-width separately	2023-07-19 12:56:35 +02:00
Jakob Rath	114e7b73e5	move callback into member function	2023-07-19 12:51:35 +02:00
Jakob Rath	b67caf5fc3	fix get_name for variables	2023-07-19 12:40:18 +02:00
Jakob Rath	85d80a0ae1	track origin slice for concat nodes	2023-07-19 12:06:02 +02:00
Jakob Rath	af73f26941	slicing: track disequalities	2023-07-19 12:04:45 +02:00
Jakob Rath	970e68c70e	slicing: use proper bv sorts for expressions	2023-07-19 08:58:34 +02:00
Jakob Rath	66f813154b	basic slicing integration	2023-07-18 16:19:54 +02:00
Jakob Rath	28ed3bd7ab	fix backtracking of m_needs_congruence	2023-07-18 16:00:26 +02:00
Jakob Rath	a96df2292e	fix build	2023-07-18 15:13:53 +02:00
Jakob Rath	68b151b0d2	move some todos	2023-07-18 15:11:46 +02:00
Jakob Rath	4742985906	add proposed query interface	2023-07-18 15:07:53 +02:00
Jakob Rath	bac52313da	move function impl	2023-07-18 14:53:20 +02:00
Jakob Rath	c124cbae97	Add virtual concat terms on demand during propagation	2023-07-18 14:48:32 +02:00
Jakob Rath	4049716946	explain conflict	2023-07-18 11:26:18 +02:00
Jakob Rath	5e5164ed2c	add_value	2023-07-18 11:24:12 +02:00
Jakob Rath	0d80e47350	update deps handling (need to support pvars as well)	2023-07-18 11:22:02 +02:00
Jakob Rath	11d9e5c862	minor	2023-07-17 19:04:17 +02:00
Jakob Rath	d1cb02b735	use abstract sort also for value slices	2023-07-17 18:31:17 +02:00
Jakob Rath	a2fdb03625	propagate value when splitting a slice	2023-07-17 18:18:12 +02:00
Jakob Rath	490b77d8a1	mk_value_slice	2023-07-17 14:41:45 +02:00
Jakob Rath	30323a6ba1	update unit test	2023-07-17 14:41:45 +02:00
Jakob Rath	741e37c2d7	find is now get_root	2023-07-17 14:41:45 +02:00
Jakob Rath	b8d118a558	use enode* instead of custom slice index; extract explanations from egraph	2023-07-17 14:41:45 +02:00
Jakob Rath	82b1f9297b	utils	2023-07-17 14:41:45 +02:00
Jakob Rath	8c17e231ad	don't 'find' when creating subslice	2023-07-12 16:45:51 +02:00
Jakob Rath	0fb81fc437	use z3's egraph (wip)	2023-07-12 16:21:38 +02:00
Jakob Rath	d8d8c67a3b	slicing interface	2023-07-12 15:56:27 +02:00
Jakob Rath	1d3a31c323	Add getter for target and justification to enode	2023-07-12 15:47:33 +02:00
Jakob Rath	f61bf0843b	display	2023-07-12 15:46:40 +02:00
Jakob Rath	f12a7d62ab	Add flag "-Werror=return-type"	2023-07-12 15:38:44 +02:00
Jakob Rath	59c3234fb8	Merge branch 'master' into polysat	2023-07-10 09:45:55 +02:00
Jakob Rath	661bea91de	fix component dependencies	2023-07-10 09:45:21 +02:00
Nikolaj Bjorner	241e845da8	fix #6802 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-07-09 12:07:43 -07:00
THE Spellchecker	dc0887db5a	Typo Fixes (#6803)	2023-07-09 11:56:10 -07:00
Jakob Rath	51ce17bcd4	start using z3's egraph for slicing	2023-07-08 20:34:46 +02:00
Jakob Rath	b4edc4d20c	slicing checkpoint	2023-07-08 20:08:45 +02:00
Jakob Rath	28810e55a0	pdd_linear_iterator	2023-07-08 20:08:03 +02:00
Jakob Rath	397acd0089	use manager reference as before	2023-07-08 20:06:24 +02:00
Nikolaj Bjorner	28a0c2d18f	Merge branch 'master' of https://github.com/z3prover/z3	2023-07-07 17:23:08 -07:00