10 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	bdb9106f99	Api (#7097) ... * rename ul_pair to column Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simple test passed * remove an assert * relax an assertion * remove an obsolete function Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * access a term by the term column * remove the column index from colunm.h * remove an unused method * remove debug code * fix the build of lp_tst Signed-off-by: Lev Nachmanson <levnach@hotmail.com> --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com>	2024-01-24 16:05:18 -08:00
Nikolaj Bjorner	4d1d067d42	fix divergence reported by Guido Martinez	2023-12-07 13:34:35 -08: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	fdedeed7ae	additional sign related fix for #4740 https://github.com/Z3Prover/z3/issues/4740#issuecomment-721508240 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-11-10 10:50:13 -08:00
Lev Nachmanson	e32a6714a5	call nlsat ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2020-05-11 19:12:02 -07:00
Lev Nachmanson	ec1f449d34	avoid patching vars in powers ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2020-04-01 12:31:32 -07:00
Nikolaj Bjorner	8a665e25ed	reverting signed mon_eq, try to rely on canonization state during add/pop ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-03-25 19:43:55 -07:00
Nikolaj Bjorner	cc74dd6373	emonics ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-03-25 19:43:55 -07:00
Nikolaj Bjorner	44d2f6da6c	fix #3261 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2020-03-25 19:43:55 -07:00
Lev Nachmanson	a0bdb8135d	rename monomial to monic ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2020-01-28 10:04:21 -08:00

Renamed from src/math/lp/monomial.h (Browse further)