16137 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	9a681b1a37	reorg sls ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-04-09 10:44:53 -07:00
Nikolaj Bjorner	bab7ca2b70	fixes to bv-sls	2024-04-07 14:24:13 -07:00
Nikolaj Bjorner	d7c0e17f96	fixes to tighten-range	2024-04-02 21:12:09 -07:00
Nikolaj Bjorner	2ce202db75	add special handling of lshr, ashr	2024-04-02 21:09:18 -07:00
Nuno Lopes	918ac2b176	fix #7196: make the code C++23 compatible ... Nikolaj is now more bleeding edge than I am... I must be getting old? (˘･_･˘)	2024-04-01 17:25:50 +01:00
Nikolaj Bjorner	84092cbd96	add engine-init to control model transfer ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-30 15:12:32 -07:00
Nikolaj Bjorner	51f1e2655c	updates to sls ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-30 12:59:05 -07:00
Steven Moy	111fcb9366	Implement API to set exit action to exception (#7192) ... * Implement API to set exit action to exception * Turn on exit_action_to_throw_exception upon API context creation	2024-03-27 19:06:58 -07:00
Nikolaj Bjorner	c18a42cf5b	change signed projection to include root object.	2024-03-23 16:14:24 -04:00
Nikolaj Bjorner	6455de9dd3	fix #7179 ... Ensure that flat associative rewriting is disabled if rewriter.flat is set to false.	2024-03-21 09:39:13 -07:00
Nikolaj Bjorner	530c6fc625	fix ##7175 - don't add user macros/functions when smtlib2_compliant=true ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-20 22:05:30 -07:00
Nikolaj Bjorner	f840d5d965	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-20 21:29:13 -07:00
Nikolaj Bjorner	70d2263a85	cast, updated nlexplain	2024-03-20 21:29:08 -07:00
Lev Nachmanson	730f9ad9b7	Nikolaj's fix in add_zero_assumption ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2024-03-20 09:39:20 -10:00
向阳	a9054bc73b	fix warning C4244 in util.h (#7171) ... Add a static cast to avoid warning C4244 on MSVC	2024-03-20 09:31:23 +00: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
Jakob Rath	5704e8d154	fix intblast is_bounded (#7163)	2024-03-14 08:48:38 -07:00
Nikolaj Bjorner	0b3bbc2972	#7158 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-11 18:19:43 -07:00
someplaceguy	7bbe3fb2b6	fix (get-proof) command to respect option pp.simplify_implies (#7157)	2024-03-09 15:13:42 -08:00
Nikolaj Bjorner	361e04a18e	port fixes to intblast ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-09 10:27:12 -08:00
Nikolaj Bjorner	dcaacf5e9b	add rewrite glue for instantiating equalities, #7154 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-07 15:21:26 -08:00
Nikolaj Bjorner	620efbb67b	add aacrhc ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-06 13:53:47 -08:00
Steven Moy	e8c8d8aa7d	Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149)	2024-03-05 13:38:12 -08:00
Nikolaj Bjorner	d6f522e205	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	531bda39ac	fix alias bug	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	657aaf9a0f	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	8679c08010	fix test ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	22616da63b	updates	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	5be8872d6a	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	dfd5c27fec	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	803f0f0c65	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	5455603910	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	9888d87294	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	f46c3782d6	bugfixes	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	d774f07eb3	add eval field to sls-valuation to track temporary values.	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	8f139e862c	updates to multiplication	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	2590d672f4	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	58474df438	na ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:31 -08:00
Nikolaj Bjorner	0e5b504c30	remove bw setting	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	a328366c7d	move to single path mode for search ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	8f85df05ed	fb ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	c451e4e50b	na	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	63804c5296	na	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	74e73f2b84	reorg to use datatypes	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	48026edd7f	move to hide bits ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	acc9c21653	move to hide bits ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	cfa6bd4534	update python build dependencies ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	5379fabf9d	include thread ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00
Nikolaj Bjorner	b14499f230	prepare for sls experiment ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-05 12:28:30 -08:00