19507 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Lev Nachmanson	7fe703e229	simplify column ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	8d747865ae	cosmetics ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	deac00ada3	persist dio handler ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	2c8a6f83e4	change int_solver to call find_cube and hnf_cut, conditionally ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	39da4f6dbd	remove an assert ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	28d41783b8	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	397fdf657d	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	63980f3bfd	fixes in dio branching ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	6bc7662580	passes z3test	2025-02-11 12:23:00 -10:00
Lev Nachmanson	174185582a	collect the explanation correctly	2025-02-11 12:23:00 -10:00
Lev Nachmanson	bc0fdfe158	remove dead code ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	c300843585	cancel bugs fixes ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	e4f3b5753f	solving regressions/smt2/b1.smt2	2025-02-11 12:23:00 -10:00
Lev Nachmanson	71c433908c	work on incremental version ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	d68ebeeb9f	use var_register in dioph_eq ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	480c48f93d	document dioph_eq ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	02a509b6e8	remove a global debug variable ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	acc2149270	remove redundant m_row_index from entry ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	d4390731f9	take dependencies from open_ml ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3fcc5a2227	fixes in tigthening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	9164672d42	check feasibility immediately after tightening a bound ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	58e57352c2	implement explain()	2025-02-11 12:23:00 -10:00
Lev Nachmanson	b30272feed	add missing explanations ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	e0a08f16d3	fix the build ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	30f5599064	use fixed vars to explain tightening ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Lev Nachmanson	36293ac773	test that pivoting is correct in dioph_eq.cpp	2025-02-11 12:23:00 -10:00
Lev Nachmanson	0db0efce9f	print output file name ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
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