12 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	c0f80f92ba	deal with compiler warnings (unused variables etc)	2023-02-18 17:53:37 -08:00
Nikolaj Bjorner	c5e33b79b5	wip - arith sls ... overhaul to tier inequalities with Boolean variables instead of literals	2023-02-18 14:11:48 -08:00
Nikolaj Bjorner	bd10ddf6ae	wip - local search - use dispatch model from bool local search instead of separate phases.	2023-02-16 09:17:11 -08:00
Nikolaj Bjorner	c1ecc49021	wip - local search - move to plugin model	2023-02-15 13:32:30 -08:00
Nikolaj Bjorner	44fcf60a72	wip experiments with sls	2023-02-14 15:06:26 -08:00
Nikolaj Bjorner	7956cf1201	annotate arith_sls	2023-02-12 20:55:44 -08:00
Nikolaj Bjorner	5e30323b1a	wip - bounded local search for arithmetic	2023-02-11 15:46:39 -08:00
Nikolaj Bjorner	7bef2f3e6f	wip - local search for euf/arithmetic	2023-02-11 09:33:43 -08:00
Nikolaj Bjorner	d22e4aa525	wip - integrating arithmetic local search	2023-02-11 09:33:42 -08:00
Nikolaj Bjorner	a8335f2d5e	use phase	2023-02-07 19:50:45 -08:00
Nikolaj Bjorner	b3ebce3966	fix compilation	2023-02-07 19:30:45 -08:00
Nikolaj Bjorner	96d815b904	adding arith sls	2023-02-07 19:27:19 -08:00