1483 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	42767b9aab	Merge branch 'master' into unit_prop_on_monomials	2023-09-26 23:55:37 -07:00
Nikolaj Bjorner	2297b0334b	re-introduce simple implementation of linear monomial propagation for evaluation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-26 23:53:14 -07:00
Nikolaj Bjorner	aaa587398e	add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-26 20:52:34 -07:00
Nikolaj Bjorner	4b85a105bb	Merge branch 'master' into unit_prop_on_monomials	2023-09-26 20:25:43 -07:00
Nikolaj Bjorner	9c63ea3135	port over cosmetics from unit_prop_on_monomials branch ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-26 20:24:49 -07:00
Nikolaj Bjorner	e8fcc876c9	Merge branch 'master' into unit_prop_on_monomials	2023-09-26 20:14:06 -07:00
Nikolaj Bjorner	ec2937e2de	port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-26 20:08:30 -07:00
Lev Nachmanson	368fe80b3d	fix the build	2023-09-25 16:55:02 -07:00
Lev Nachmanson	6ff4856e38	throttle monomial unit prop and and nl params	2023-09-25 16:47:34 -07:00
Lev Nachmanson	896aba31f8	move monomial propagation from theory_lra to nla_solver ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-25 14:20:24 -07:00
Nikolaj Bjorner	0a1ade6f95	move m_nla_lemma_vector to be internal to nla_core ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-25 12:40:52 -07:00
Lev Nachmanson	26a9b776c6	clean m_nla_lemma_vector in nla_solver ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2023-09-25 12:10:59 -07:00
Nikolaj Bjorner	db097bae05	use format from unit_prop_on_monomials branch ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-23 17:24:46 -07:00
Nikolaj Bjorner	886d3f4351	indentation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-22 16:55:34 -07:00
Nikolaj Bjorner	eac54ba084	indentation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-22 16:54:12 -07:00
Nikolaj Bjorner	940775d12d	indentation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2023-09-22 16:48:40 -07:00
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