19480 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Lev Nachmanson	8904a50103	fix the build	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5f5f1d4fd1	init m_e_matrix on terms instead of the tableau ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	392c24a145	throttle dioph equalities ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	128d5b4fa0	change type of m_e_matrix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a63e0d801e	add a template instantiotion ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0f03e7560d	handle empty rows in m_e_matrix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ba7268c895	vector access bugs ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	66f88206f5	bug fixes with tableau ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	62ea6fbe98	bug fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ac491989b8	bug fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	536c51f600	debug dio with static matrix	2025-02-11 12:23:00 -10:00
Lev Nachmanson	28fbc810e6	unifying vectors into eprime_entry	2025-02-11 12:23:00 -10:00
Lev Nachmanson	42bdc893a9	dio with static_matrix initial setup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	9e8b17b5f8	do not use conflicts with fresh vars to create branches ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	eaf2f7f165	remove disabling return	2025-02-11 12:23:00 -10:00
Lev Nachmanson	8aeba62802	remove more warnings ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	552a504f72	remove a warning ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	4bd815852d	fix ubuntu's build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	ea50208ad6	prepare using fresh vars in cuts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	06faf03eaa	use cuts from proofs, remove gcc warnings ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	2ebb957cc8	enable cuts from proofs ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	44fd0e48a8	fixes in dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a8e667c643	do not eliminate fresh variables when tightening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	52b0b8d5d5	fixed dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5ac428fcc9	comment out global_max_change ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	89e4f59df2	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	798f0e2e8a	test tightening with S ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	193116bf84	handle sat with tightening	2025-02-11 12:23:00 -10:00
Lev Nachmanson	b1be8c0957	cosmetics ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5db46c1d81	use u_dependency in eprime_pair ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	1408fe60ab	work on tighten_with_S ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	f0b5cd1066	remove a throw ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	be8f3e9c3e	bug fix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0b1e923d2a	small optimization ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	66c6bad01c	optimize dio changes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	18c75e6333	less eager dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	bbeecc6f7c	fix the build	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3d5ee82bd1	handle zero rows correctly	2025-02-11 12:23:00 -10:00
Lev Nachmanson	78a58b06aa	dio passes regression\smt2 tests with limited functionality ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	245d448c66	fix term_o init ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a796d48264	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	df18885f97	debug dio	2025-02-11 12:23:00 -10:00
Lev Nachmanson	cd13890650	fix in substitution of fresh variables, clean column.h	2025-02-11 12:23:00 -10:00
Lev Nachmanson	f5e646cbcb	bug fix in init and getting explanations ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	59e2dab69a	create a conflict explanation ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	52653e6e43	a version with less pointers: got a conflict ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	5a36e02c58	in the middle	2025-02-11 12:23:00 -10:00
Lev Nachmanson	122e0135d2	use std::list	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3b22d3b19d	fix the crash	2025-02-11 12:23:00 -10:00
Lev Nachmanson	abf29b57aa	crash ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00