15969 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	b170f10148	reorder template definition ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-10-02 13:41:02 -07:00
Nikolaj Bjorner	d686e92bfa	disambiguate ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-10-02 10:45:16 -07:00
Nikolaj Bjorner	93ff89bf98	add == for const_ref and ref to disambiguate equality.	2024-10-02 10:45:16 -07:00
Nikolaj Bjorner	c7af97364a	fixes for #7402 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-10-01 15:15:47 -07:00
Nikolaj Bjorner	328616b8b2	fix build warnings	2024-09-30 17:25:19 -07:00
Nikolaj Bjorner	8c39863019	fix typo in arch for setup.py ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-30 16:17:40 -07:00
Nikolaj Bjorner	4cefc513eb	add sequoia to os versions #7407 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-30 16:05:53 -07:00
Nikolaj Bjorner	19f63cd6e3	add sequoia to os versions #7407 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-30 15:57:49 -07:00
Nikolaj Bjorner	86b97186b0	fix build warnings	2024-09-30 15:51:48 -07:00
Nikolaj Bjorner	551cc53a2f	fix un-intialized variable warnings	2024-09-30 15:08:33 -07:00
Nikolaj Bjorner	2c94a3a1b3	fix build warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-30 13:09:01 -07:00
Nikolaj Bjorner	7da58b9e84	fix build warnings	2024-09-30 10:34:26 -07:00
Nikolaj Bjorner	5413018d86	Update euf_ac_plugin.cpp	2024-09-30 08:43:17 -07:00
Nikolaj Bjorner	826835fd7c	fixes to build warnings	2024-09-30 08:23:31 -07:00
Nikolaj Bjorner	11bb19d99b	make default tactic cases lazy	2024-09-27 15:11:43 +01:00
Nikolaj Bjorner	40b0210dda	fixes to lazy tactic uses ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-27 14:33:09 +01:00
Nikolaj Bjorner	01cf0427b4	fix #7404, relates to #7400.	2024-09-27 11:36:10 +01:00
Nikolaj Bjorner	d047b86439	pypi publish ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-26 21:35:28 +01:00
Nikolaj Bjorner	f4452a0348	pypi publish ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-26 21:34:55 +01:00
Nikolaj Bjorner	3df7299d1e	update signature of operator== ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-26 14:47:51 +01:00
Kevin Gibbons	77aa5280df	wasm: increase timeout in tests (#7401)	2024-09-25 18:33:14 +01:00
Kevin Gibbons	103c5ad71c	wasm: attempt to GC in tests (#7400)	2024-09-25 15:53:36 +01:00
Nikolaj Bjorner	eb5d036786	fix #7392 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-25 10:21:54 +01:00
Nikolaj Bjorner	2655301afc	comment out simple proofs unit test ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-24 23:01:12 +01:00
Páll Haraldsson	994056f347	C API now used by Julia. (#7387) ... See: https://github.com/ahumenberger/Z3.jl/releases/tag/v1.0.0	2024-09-24 15:17:00 +01:00
Nikolaj Bjorner	716a815ce1	update lock file ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-24 11:29:35 +01:00
Nikolaj Bjorner	a831fe9609	fix some build warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-24 11:15:47 +01:00
Nikolaj Bjorner	afaa48d72a	sample fix script ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-23 19:06:51 +01:00
Lev Nachmanson	fa1a2cdc1e	disable simple check in nlsat ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2024-09-23 10:10:46 -07:00
Nikolaj Bjorner	0604d23c57	Check if model_converter is non-null before initializing values in sat_tactic	2024-09-23 13:50:32 +01:00
Nikolaj Bjorner	5a6dc18d0d	Override convert_initialize_value method in bit_blaster_model_converter.cpp	2024-09-23 13:46:50 +01:00
Nikolaj Bjorner	5c583299f1	Remove unnecessary const qualifiers from comparison operator overloads in z3++.h	2024-09-23 13:38:07 +01:00
Nikolaj Bjorner	eb8c63080a	Refactor and fix uninitialized variables and improve function consistency across multiple modules	2024-09-23 13:34:33 +01:00
Nuno Lopes	499ed5d844	remove unneeded iterator functions	2024-09-23 12:59:04 +01:00
Nuno Lopes	737c2208fa	delete more default constructors ... reduces code size by 0.1%	2024-09-23 12:59:04 +01:00
Nikolaj Bjorner	4b4a28239f	Add const qualifiers to comparison operators and update iterator equality checks in various classes	2024-09-23 11:45:11 +01:00
Nuno Lopes	a62fede64b	remove a few default constructors	2024-09-23 08:17:58 +01:00
Nuno Lopes	22d9bfad35	fix warning with iterators due to non-const comparator	2024-09-23 08:10:56 +01:00
Nikolaj Bjorner	1e580a7f12	update to c++20, remove debug output ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-22 21:30:44 +01:00
Nikolaj Bjorner	96c1375786	#7391 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-22 19:35:03 +01:00
Nikolaj Bjorner	a9f8ec1bcb	updated handling of value initialization for bit-vectors	2024-09-22 21:30:11 +03:00
Nikolaj Bjorner	ba5cec7704	additional rewrites for bv2int	2024-09-22 21:29:12 +03:00
Nikolaj Bjorner	fa7fc8ef5e	Refactor bv_rewriter functions using unified variable assignment and early break logic	2024-09-22 13:04:49 +03:00
Nikolaj Bjorner	d66609ea14	fix #7389 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-09-22 02:41:11 +03:00
Nikolaj Bjorner	0c48a50d59	Add support for initializing variable values in solver and optimize contexts in Z3	2024-09-20 18:28:26 +03:00
Lev Nachmanson	342dccdc02	correctly process cancellation in gomory cuts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2024-09-19 14:11:27 -07:00
Nikolaj Bjorner	b99c4a47a4	Add override specifiers to methods in set_initial_value_cmd class for clarity and consistency	2024-09-19 15:11:59 +03:00
Nikolaj Bjorner	8349ee0069	Add support for const array in all logics as per issue #7383	2024-09-19 11:44:18 +03:00
Nikolaj Bjorner	4896edfb04	Add tracking of values size in scoped_state push method in opt_context	2024-09-19 11:27:17 +03:00
Nikolaj Bjorner	a3f35b6830	Add command to set initial value hints for solver in various components	2024-09-18 17:48:03 +03:00