1467 commits

Author	SHA1	Message	Date
Lev Nachmanson	caa929f01f	do not use lemmase in monomial propagation	2023-09-22 14:27:26 -07:00
Nikolaj Bjorner	5d8779b05d	Merge branch 'master' into unit_prop_on_monomials	2023-09-22 09:46:41 -07:00
Nikolaj Bjorner	eff3f5f65e	port bug fixes from unit prop branch ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-22 09:45:58 -07:00
Lev Nachmanson	576309a16f	Revert "reject rows with columns with big numbers for lp bound propagation" ... This reverts commit c0b55d1435.	2023-09-21 16:30:43 -07:00
Lev Nachmanson	c0b55d1435	reject rows with columns with big numbers for lp bound propagation ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-21 15:53:53 -07:00
Lev Nachmanson	f423642e9b	try the lemma scheme	2023-09-21 12:18:21 -07:00
Lev Nachmanson	e31cecf5db	transfer propagate monomial bounds to nla_solver	2023-09-21 11:27:53 -07:00
Lev Nachmanson	536930b4a1	make m_ibounds inside of lp_bound_propagator ... a reference	2023-09-20 17:13:25 -07:00
Lev Nachmanson	20c02f4f45	fix a lambda bug ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-20 17:02:35 -07:00
Nikolaj Bjorner	f9de65a464	indetation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-20 15:22:28 -07:00
Nikolaj Bjorner	615aad7779	get rid of int*, use lambda scoping ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-20 15:18:37 -07:00
Lev Nachmanson	f2a0ddb385	Merge branch 'unit_prop_on_monomials' of https://github.com/z3prover/z3 into unit_prop_on_monomials	2023-09-19 15:47:01 -07:00
Lev Nachmanson	d77c91b1aa	trying to get else on a new line ... with clang-formatter	2023-09-19 15:46:59 -07:00
Nikolaj Bjorner	f07553ed3a	formatting updates ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-19 15:18:38 -07:00
Nikolaj Bjorner	db84d21e3b	Merge branch 'master' into unit_prop_on_monomials	2023-09-19 14:44:01 -07:00
Nikolaj Bjorner	fba5de3a25	remove unused code ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-19 14:43:02 -07:00
Nikolaj Bjorner	85db8163fa	move allocator to memory_manager and std_vector to vector ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-19 13:57:28 -07:00
Lev Nachmanson	c5cfd62e0a	remove dead code related to nla unit propagation ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-19 10:56:09 -07:00
Lev Nachmanson	cf63e75898	using structures from util in lp_bound_propagator ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-18 13:25:24 -07:00
Lev Nachmanson	af8d192392	add an include	2023-09-17 13:14:36 -07:00
Lev Nachmanson	10095a30b7	add an include file	2023-09-17 12:25:11 -07:00
Lev Nachmanson	66f6a0327f	change type of m_ibounds to std::vector	2023-09-17 11:00:48 -07:00
Lev Nachmanson	30b743d7b3	refactor propagat_monic	2023-09-17 10:45:54 -07:00
Lev Nachmanson	7353d7fb4d	fix dep calculations in lp_bound_propagator	2023-09-17 06:48:12 -07:00
Lev Nachmanson	77e56b0a69	debug	2023-09-16 13:54:14 -07:00
Lev Nachmanson	c240f62ca8	is_linear does not check for is_big	2023-09-15 17:44:10 -07:00
Lev Nachmanson	4cfba9787b	debug lp_bound_propagator	2023-09-15 17:41:10 -07:00
Lev Nachmanson	a55aa1a648	add a comment	2023-09-14 19:29:48 -07:00
Lev Nachmanson	b3673d491e	fix the build for gcc	2023-09-14 19:20:47 -07:00
Lev Nachmanson	cbad61ba2e	propagate monics with lp_bound_propagator	2023-09-13 14:27:34 -07:00
Lev Nachmanson	c309d52283	runs a simple test	2023-09-13 08:12:00 -07:00
Lev Nachmanson	c050af922f	fixing the bugs	2023-09-07 15:59:20 -07:00
Lev Nachmanson	c43b99daae	renaming ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-07 11:57:20 -07:00
Lev Nachmanson	47b64e689c	restore the lemma scheme ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-07 11:33:14 -07:00
Lev Nachmanson	288e66de59	restore m_crossed* and create lemmas ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-06 09:27:30 -07:00
Lev Nachmanson	41f59cb1ed	propagate monomial is nla	2023-09-05 18:49:59 -07:00
Lev Nachmanson	318d7d7564	fixes a bug	2023-09-01 11:32:26 -07:00
Lev Nachmanson	d3258e7084	propagate lineal monomial	2023-09-01 11:18:03 -07:00
Lev Nachmanson	5509b468e9	handle monomial_bounds::unit_propagate()	2023-08-31 17:35:41 -07:00
Nikolaj Bjorner	ff3268e636	move unit propagation into monomial_bounds ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-31 14:32:05 -07:00
Nikolaj Bjorner	c2cbe72b64	sketch linear monomial propagation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-31 11:49:05 -07:00
Nikolaj Bjorner	38b131386d	add stubs for monomial unit propagation	2023-08-30 17:21:48 -07:00
Nikolaj Bjorner	e8929041b8	fixing calls, signs	2023-08-22 09:29:12 -07:00
Lev Nachmanson	61a7c6b28d	init m_literal_vec ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-08-21 17:11:55 -07:00
Lev Nachmanson	9aeaed8f53	Merge branch 'master' into nl_branches	2023-08-21 16:15:20 -07:00
Lev Nachmanson	9b672bc5cc	remove tracking of bounds	2023-08-20 10:10:48 -07:00
Nikolaj Bjorner	5e3df9ee77	Arith min max (#6864) ... * prepare for dependencies Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * snapshot Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * pass in u_dependency_manager Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * address NYIs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more refactoring names Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * eq_explanation update Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add outline of bounds improvement functionality Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unit tests Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove unused structs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * convert more internals to use u_dependency instead of constraint_index Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * convert more internals to use u_dependency instead of constraint_index Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remember to push/pop scopes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use the main function for updating bounds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove reset of shared dep manager Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disable improve-bounds, add statistics Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-19 17:44:09 -07:00
Lev Nachmanson	610313946d	split free vars in nla	2023-08-18 12:36:14 -07:00
Lev Nachmanson	252a30e727	use param_ref in nla_solver (#6862) ... * use param_ref in nla_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add parameters Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add parameters Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * replace nla_setting by command line parameters * delete nla_setting.h --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-17 18:44:27 -07:00
Nikolaj Bjorner	51df7b75ce	fix 6800 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-08-17 15:18:22 -07:00