8 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	a7010574c8	align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time.	2025-01-25 20:47:57 -08:00
Nikolaj Bjorner	d805322dfb	create separate file for expression based lookahead solver	2025-01-25 11:19:40 -08:00
Nikolaj Bjorner	f6e7dcff47	Fix crash exposed in QF_UFNIA	2025-01-24 15:31:10 -08:00
Nikolaj Bjorner	0e8969ce60	deal with compiler warnings and include value exchange prior to final check.	2025-01-24 09:40:33 -08:00
Nikolaj Bjorner	ce615ee116	avoid repeated clauses during scoring function	2025-01-23 10:51:12 -08:00
Nikolaj Bjorner	ec3915218d	modify backoff mechanisms and theory exchange	2025-01-22 20:32:30 -08:00
Nikolaj Bjorner	4fce314bf2	improve diagnostics for flips	2025-01-22 11:46:10 -08:00
Nikolaj Bjorner	22e4054674	add clausal lookahead to arithmetic solver as part of portfolio ... have legacy qfbv-sls solver use nnf pre-processing. It relies on it for correctness of the score updates.	2025-01-20 16:16:46 -08:00