19510 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Lev Nachmanson	5b0b224a5c	try sorting terms before tightening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	dcd5783232	remove the fresh definition when removing its column ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	17d68c18aa	comment change ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	d90b94d0e2	stricter is_in_sync paying attenion to m_row2fresh_defs ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	134bed826a	throttle the branching in dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	bd8cf29df7	ignore large changed_columns ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3ac11cd136	fix assert ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	cf4e402a0f	avoid usisg indexed_vector for term operations	2025-02-11 12:23:00 -10:00
Lev Nachmanson	440d78f237	disallow duplicates in a queue ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	7e02dfe484	add stats on m_dio_branching_conflicts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0bf3ca87e7	call normalize_e_by_gcd() only when moving an entry from F to S	2025-02-11 12:23:00 -10:00
Lev Nachmanson	99538567a7	rebase with master ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a19e10912f	make dio less aggressive, allow other cuts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	fee707842d	register m_added_terms in m_changed_terms	2025-02-11 12:23:00 -10:00
Lev Nachmanson	21f67ef942	out of bounds fixes	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3b3d8cee03	use m_chandedNterms to tighten terms	2025-02-11 12:23:00 -10:00
Lev Nachmanson	65bdd58d3e	remove struct entry	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a9098a5785	optimise l terms addition ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3e7e903d19	use the trail to undo add_term ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	9c510018b3	fix the debug build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	058b9e4a6d	optimise rewrite_eqs to avoid fresh variables ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ed3df333b3	make rewrite_eq boolean, and relax an ASSERT ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ca7c128d3f	clean up fresh definitions on a pop ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	b027761845	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	bb869fd020	don't store fresh definitions in m_e_matrix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	e5ffc3cfae	cleanup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	d7de7eb732	remove recalculated entries from S ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ef55de1646	fix out of bounds bug ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3990df6d91	substitute variables with a queue on the recalculated entries ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	78d91f3794	simplify dio handler by using bijection m_k2s ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	33f5e303f8	use entry_status for FRESH entries	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0e71adfa35	fix some warnings ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	7bba8bc0c9	fix some warnings	2025-02-11 12:23:00 -10:00
Lev Nachmanson	abac52e1d7	remove var_register_dio.h ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	89eec4cc80	test dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5a72117528	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0027ae21e8	bug fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5158797233	refine trail iterations with lar.m_terms ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	9a9ccf19c5	introdure lar_term.ext_coeffs(), dio passes some tests ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	083926c658	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a0ece6dd2c	cleanup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ceeece6770	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ac5c50f179	fix ubuntu build in dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	c1ece49694	track changed columns in dio\ ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	008e9229a5	use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	57b665d075	work on incremental dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	28556ce625	cleanup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	862dc91cb2	work on incremental dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	fd3bd088a4	remove some warnings	2025-02-11 12:23:00 -10:00
Lev Nachmanson	9a96aa94e6	test ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00