5 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	c75b8ec752	add option to control epsilon #7791 ... #7791 reports on using model values during lex optimization that break soft constraints. This is an artifact of using optimization where optimal values can be arbitrarily close to a rational. In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.	2025-08-17 16:51:00 -07:00
Nikolaj Bjorner	e54928679f	add option to selectively disable variable solving for only ground expressions ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2025-07-25 19:15:20 -07:00
Lev Nachmanson	d717dae3ac	remove the parameter for throttling nla lemmas	2025-06-26 16:33:16 -07:00
Lev Nachmanson	5bda42e104	rename new_lemma to lemma_builder ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-06-26 16:33:16 -07:00
Nikolaj Bjorner	c387b20ac6	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00

Renamed from src/smt/params/smt_params_helper.pyg (Browse further)