19326 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Lev Nachmanson	09ec973998	print output file name ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:43 -10:00
Lev Nachmanson	594fa7423f	fix the build	2025-02-03 13:30:42 -10:00
Lev Nachmanson	a3b81b54db	init m_e_matrix on terms instead of the tableau ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	2bda4d1674	throttle dioph equalities ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	727ac149a7	change type of m_e_matrix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	282edcfadf	add a template instantiotion ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	4710260ede	handle empty rows in m_e_matrix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	b0be4d58c7	vector access bugs ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	f5f4c848ec	bug fixes with tableau ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	9c2ec9b47d	bug fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	9434847ce7	bug fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:42 -10:00
Lev Nachmanson	bc2c67c7ea	debug dio with static matrix	2025-02-03 13:30:42 -10:00
Lev Nachmanson	df577eecd6	unifying vectors into eprime_entry	2025-02-03 13:30:42 -10:00
Lev Nachmanson	f3b33888ab	dio with static_matrix initial setup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	60a38cdd22	do not use conflicts with fresh vars to create branches ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	dc15dbfc31	remove disabling return	2025-02-03 13:30:41 -10:00
Lev Nachmanson	5f0077626e	remove more warnings ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	fdae46fb60	remove a warning ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	2c7c708848	fix ubuntu's build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	fa907c5e8c	prepare using fresh vars in cuts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	110593f086	use cuts from proofs, remove gcc warnings ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	4e381609db	enable cuts from proofs ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	c30600c2ef	fixes in dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	5f70eb0524	do not eliminate fresh variables when tightening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	1769c6059e	fixed dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:41 -10:00
Lev Nachmanson	2ca7b31d13	comment out global_max_change ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	f05d1abccc	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	8d8ee99db3	test tightening with S ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	7d8212646d	handle sat with tightening	2025-02-03 13:30:40 -10:00
Lev Nachmanson	9118abebc7	cosmetics ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	e0185121c5	use u_dependency in eprime_pair ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	b20566a488	work on tighten_with_S ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	a1a9825e43	remove a throw ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	a75eff6525	bug fix ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	0c6dcfedb8	small optimization ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	9ec55de5c6	optimize dio changes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	7c9cb44c94	less eager dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:40 -10:00
Lev Nachmanson	4fea4259ec	fix the build	2025-02-03 13:30:40 -10:00
Lev Nachmanson	1a99fa56cb	handle zero rows correctly	2025-02-03 13:30:40 -10:00
Lev Nachmanson	178411ad0c	dio passes regression\smt2 tests with limited functionality ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:39 -10:00
Lev Nachmanson	dcd80ac95b	fix term_o init ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:39 -10:00
Lev Nachmanson	c29d04dc3c	debug dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:39 -10:00
Lev Nachmanson	1cb71b4648	debug dio	2025-02-03 13:30:39 -10:00
Lev Nachmanson	db899fd670	fix in substitution of fresh variables, clean column.h	2025-02-03 13:30:39 -10:00
Lev Nachmanson	5f71604198	bug fix in init and getting explanations ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:39 -10:00
Lev Nachmanson	0814fa40b0	create a conflict explanation ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:39 -10:00
Lev Nachmanson	53605d4e0a	a version with less pointers: got a conflict ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:30:00 -10:00
Lev Nachmanson	876cbc527d	in the middle	2025-02-03 13:24:33 -10:00
Lev Nachmanson	778db5e763	use std::list	2025-02-03 13:24:33 -10:00
Lev Nachmanson	c1e577e932	fix the crash	2025-02-03 13:24:33 -10:00