9 commits

Author	SHA1	Message	Date
Copilot	ebc0688470	Refactor mk_and/mk_or call sites to use vector overloads (#8286) ... * Initial plan * Refactor mk_and and mk_or call sites to use overloaded methods Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h) * Fix compilation errors from mk_and/mk_or refactoring Fixed type mismatches by: - Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads) - Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and) - Verified build succeeds and Z3 works correctly Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix test files to use correct mk_and/mk_or overloads Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>	2026-01-22 13:21:22 -08:00
Nikolaj Bjorner	5e3df9ee77	Arith min max (#6864) ... * prepare for dependencies Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * snapshot Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * pass in u_dependency_manager Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * address NYIs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring names Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * eq_explanation update Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add outline of bounds improvement functionality Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unit tests Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove unused structs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * convert more internals to use u_dependency instead of constraint_index Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * convert more internals to use u_dependency instead of constraint_index Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remember to push/pop scopes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use the main function for updating bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove reset of shared dep manager Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disable improve-bounds, add statistics Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-19 17:44:09 -07:00
Nuno Lopes	c3407fc304	fix build of tests	2022-06-17 17:11:18 +01:00
Nikolaj Bjorner	fd799089b7	fix build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2021-09-20 11:19:26 -07:00
Nikolaj Bjorner	4a6083836a	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
Nikolaj Bjorner	c43852a266	fix unit test ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-01-05 17:52:44 -08:00
Nikolaj Bjorner	1d0572354b	add bit-matrix, avoid flattening and/or after bit-blasting, split pdd_grobner into solver/simplifier, add xlin, add smtfd option for incremental mode logic ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-01-01 20:14:20 -08:00
Nikolaj Bjorner	09dbacdf50	remove unused functionality ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-01-01 20:14:20 -08:00
Nikolaj Bjorner	6b4ddf352d	port fixes from lev's branch. Rename pdd_grobner to pdd_solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-01-01 20:14:20 -08:00

Renamed from src/test/pdd_grobner.cpp (Browse further)