16092 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	182979771f	disable verbose ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-21 10:41:31 -07:00
Jakob Rath	934b2ad5ef	update target selection to what was intended	2024-03-21 13:53:26 +01:00
Jakob Rath	342db52558	fix	2024-03-21 12:03:52 +01:00
Jakob Rath	acd05686e4	relevant level should be based on what's to appear in the lemma	2024-03-21 11:05:55 +01:00
Jakob Rath	7d1a57b6e9	remove commented code	2024-03-20 15:38:42 +01:00
Jakob Rath	7922ee3e82	debug output	2024-03-20 15:37:34 +01:00
Jakob Rath	fd9c931168	skip entry for origin variable	2024-03-20 15:37:03 +01:00
Jakob Rath	23ca9d9fc5	select targets, try generic/specific version of projection	2024-03-20 15:26:33 +01:00
Jakob Rath	de809932eb	refactor, minor fixes	2024-03-20 14:33:30 +01:00
Jakob Rath	ef6b5f82d1	relax level constraint	2024-03-20 13:39:16 +01:00
Jakob Rath	91a9feb5a8	warnings	2024-03-20 12:16:24 +01:00
Jakob Rath	f47fbdd714	Move interval projection out of viable	2024-03-20 12:11:14 +01:00
Jakob Rath	5339a2f70f	Don't access solver_interface directly	2024-03-20 10:16:40 +01:00
Jakob Rath	a34bb99db3	Use variable from violated interval as origin	2024-03-20 10:15:25 +01:00
Jakob Rath	3a11350142	Move helper functions	2024-03-20 10:10:27 +01:00
Nikolaj Bjorner	6eeb022048	fix encoding for sdiv exposed by zQkAOXjEDwgm ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-19 16:00:09 -07:00
Nikolaj Bjorner	ffe7b46e74	unsigned cast ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-19 15:02:42 -07:00
Jakob Rath	f5eb457bee	fix propagate_from_containing_slice dependency	2024-03-19 16:13:28 +01:00
Jakob Rath	489a1495d2	dep	2024-03-19 14:23:44 +01:00
Jakob Rath	adc5313916	remove debug output	2024-03-19 10:11:06 +01:00
Jakob Rath	148eafaaf0	Merge remote-tracking branch 'origin/master' into poly	2024-03-19 09:50:24 +01:00
cctv130	18365907a2	Update util.h (#7169)	2024-03-17 20:29:27 -07:00
Nikolaj Bjorner	b8a69987c3	fix #7165	2024-03-17 16:33:40 -07:00
Nikolaj Bjorner	fb824bee54	inline unfolding if it is linear or constant.	2024-03-16 13:02:26 -07:00
Nikolaj Bjorner	3555b25317	Merge branch 'poly' of https://github.com/z3prover/z3 into poly	2024-03-15 08:55:16 -07:00
Nikolaj Bjorner	e4cc6e29ca	fix case when interval is full	2024-03-15 08:55:07 -07:00
Jakob Rath	aa1285288e	Fix integration of propagate_from_containing_slice	2024-03-15 15:08:12 +01:00
Jakob Rath	dfb200a3c9	propagation from containing slice depends on concrete values	2024-03-15 12:31:31 +01:00
Jakob Rath	5704e8d154	fix intblast is_bounded (#7163)	2024-03-14 08:48:38 -07:00
Jakob Rath	2102db2df8	Fix viable entry reduction (case new_lo == new_hi)	2024-03-14 15:09:21 +01:00
Jakob Rath	f6c99585f3	fix warning	2024-03-14 15:08:00 +01:00
Nikolaj Bjorner	82dc254d0e	Merge branch 'poly' of https://github.com/z3prover/z3 into poly	2024-03-13 16:20:54 -07:00
Nikolaj Bjorner	c2f8dd9a02	use -> types ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-13 16:20:51 -07:00
Nikolaj Bjorner	1f0a6c051a	update slice/offset claim structures to allow for equal variable. ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-13 11:49:11 -07:00
Nikolaj Bjorner	1e9381c2f6	update slice/offset claim structures to allow for equal variable. ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-13 11:48:09 -07:00
Jakob Rath	5d1602b6c7	print validation failures	2024-03-13 14:12:10 +01:00
Jakob Rath	7da7e99ca2	try_umul_blast	2024-03-13 14:01:07 +01:00
Jakob Rath	8a16631fd1	fix intblast is_bounded	2024-03-13 12:37:37 +01:00
Jakob Rath	d07d57c240	remove leftovers from earlier commit	2024-03-13 09:42:08 +01:00
Jakob Rath	22d80277ae	signed_constraint ==	2024-03-12 16:26:27 +01:00
Jakob Rath	35e3211ca8	display	2024-03-12 16:24:28 +01:00
Jakob Rath	450ed26440	implement 'is_full' case	2024-03-12 16:23:39 +01:00
Jakob Rath	df85eeb581	viable explanation depends on assignment	2024-03-12 16:20:44 +01:00
Jakob Rath	58c14ba2f9	write validation in bv format too	2024-03-12 16:18:39 +01:00
Jakob Rath	37bf5fefca	fix extract axiom	2024-03-12 13:47:23 +01:00
Nikolaj Bjorner	0b3bbc2972	#7158 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-11 18:19:43 -07:00
Jakob Rath	7311af699c	fix	2024-03-11 15:02:55 +01:00
Jakob Rath	d11c2b3265	Add ule_constraint simplification	2024-03-11 14:20:29 +01:00
Nikolaj Bjorner	2fdf2233f9	move side effect out of print statement	2024-03-11 04:08:07 -07:00
someplaceguy	7bbe3fb2b6	fix (get-proof) command to respect option pp.simplify_implies (#7157)	2024-03-09 15:13:42 -08:00