19410 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Lev Nachmanson	5e23e778f4	work on incremental dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:30 -10:00
Lev Nachmanson	b2964f8d1e	cleanup ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:30 -10:00
Lev Nachmanson	af857810e8	work on incremental dio ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:30 -10:00
Lev Nachmanson	4dd701a5b4	remove some warnings	2025-02-03 13:33:29 -10:00
Lev Nachmanson	0d3abbb5e0	test ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:29 -10:00
Lev Nachmanson	f2b05af67e	test	2025-02-03 13:33:28 -10:00
Lev Nachmanson	000fab630c	fix a bug in dio	2025-02-03 13:33:27 -10:00
Lev Nachmanson	a737483ba0	fix a bug in dio	2025-02-03 13:33:26 -10:00
Lev Nachmanson	c112df5d41	simplify column ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:26 -10:00
Lev Nachmanson	0958806d4a	cosmetics ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:26 -10:00
Lev Nachmanson	90dbc623fd	persist dio handler ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:26 -10:00
Lev Nachmanson	7d8e192344	change int_solver to call find_cube and hnf_cut, conditionally ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:26 -10:00
Lev Nachmanson	44d75da7a5	remove an assert ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:26 -10:00
Lev Nachmanson	28bafa301e	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:25 -10:00
Lev Nachmanson	b933a0d6e0	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:25 -10:00
Lev Nachmanson	e32ebf109b	fixes in dio branching ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:25 -10:00
Lev Nachmanson	781471aa6f	passes z3test	2025-02-03 13:33:25 -10:00
Lev Nachmanson	f336b0d599	collect the explanation correctly	2025-02-03 13:33:24 -10:00
Lev Nachmanson	ada3be2679	remove dead code ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:24 -10:00
Lev Nachmanson	6af8fbb629	cancel bugs fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:24 -10:00
Lev Nachmanson	7f7dc8750f	solving regressions/smt2/b1.smt2	2025-02-03 13:33:24 -10:00
Lev Nachmanson	08a1ddf79f	work on incremental version ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:24 -10:00
Lev Nachmanson	b47a2687ad	use var_register in dioph_eq ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:23 -10:00
Lev Nachmanson	cdb18ac685	document dioph_eq ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:23 -10:00
Lev Nachmanson	eb0aeab2a3	remove a global debug variable ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:22 -10:00
Lev Nachmanson	b99439599b	remove redundant m_row_index from entry ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:22 -10:00
Lev Nachmanson	12ceb1ef26	take dependencies from open_ml ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:22 -10:00
Lev Nachmanson	2a81a1f043	fixes in tigthening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:21 -10:00
Lev Nachmanson	bb77ff537b	check feasibility immediately after tightening a bound ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:21 -10:00
Lev Nachmanson	0077a689bd	implement explain()	2025-02-03 13:33:21 -10:00
Lev Nachmanson	1eecedf8cb	add missing explanations ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:20 -10:00
Lev Nachmanson	143f22e0a5	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:20 -10:00
Lev Nachmanson	472306c0b2	use fixed vars to explain tightening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-03 13:33:20 -10:00
Lev Nachmanson	24aeaed50a	test that pivoting is correct in dioph_eq.cpp	2025-02-03 13:33:14 -10:00
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