Nikolaj Bjorner 0e6b3a922a Add commands for forcing preferences during search ... Add commands: (prefer <formula>) - will instruct case split queue to assign formula to true. - prefer commands added within a scope are forgotten after leaving the scope. (reset-preferences) - resets asserted preferences. Has to be invoked at base level. This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2		2025-10-02 10:47:10 -07:00
..
assertions	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
check_logic.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
check_logic.h	debug arith/mbi	2020-11-02 12:13:19 -08:00
check_sat_result.cpp	more detailed tracing of where unmaterialized exceptions happen	2024-11-19 18:15:50 -08:00
check_sat_result.h	more detailed tracing of where unmaterialized exceptions happen	2024-11-19 18:15:50 -08:00
CMakeLists.txt	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
combined_solver.cpp	Add virtual translate method to solver_factory class (#7780)	2025-08-14 11:54:34 -07:00
combined_solver.h	booyah	2020-07-04 15:56:30 -07:00
combined_solver_params.pyg	solver factories, cleanup solver API, simplified strategic solver, added combined solver	2012-12-11 17:47:27 -08:00
mus.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
mus.h	booyah	2020-07-04 15:56:30 -07:00
parallel_params.pyg	spell check from https://github.com/microsoft/z3guide/pull/165	2024-01-12 09:57:46 -08:00
parallel_tactical.cpp	use std::exception as base class to z3_exception	2024-11-04 11:08:15 -08:00
parallel_tactical.h	add missing tactic descriptions, add rewrite for tamagochi	2023-01-08 13:32:26 -08:00
preferred_value_propagator.h	Add commands for forcing preferences during search	2025-10-02 10:47:10 -07:00
progress_callback.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
simplifier_solver.cpp	remove a few useless dynamic casts	2025-09-13 21:06:55 +01:00
simplifier_solver.h	Add simplification customization for SMTLIB2	2023-01-30 22:38:51 -08:00
slice_solver.cpp	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
slice_solver.h	A slice solver option for interactive use case	2024-10-08 09:24:52 -07:00
smt_logics.cpp	remove a bunch of string copies	2025-08-03 10:41:38 +01:00
smt_logics.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
solver.cpp	#7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults	2025-02-10 11:57:14 -08:00
solver.h	Add virtual translate method to solver_factory class (#7780)	2025-08-14 11:54:34 -07:00
solver2tactic.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
solver2tactic.h	move model and proof converters to self-contained module	2022-11-03 05:23:01 -07:00
solver_na2as.cpp	display assumptions used	2025-09-11 10:20:55 -07:00
solver_na2as.h	remove default destructors & some default constructors	2024-09-04 22:30:23 +01:00
solver_pool.cpp	remove a few useless dynamic casts	2025-09-13 21:06:55 +01:00
solver_pool.h	booyah	2020-07-04 15:56:30 -07:00
solver_preprocess.cpp	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
solver_preprocess.h	add unconstrained elimination for sequences	2023-03-20 17:07:04 +01:00
tactic2solver.cpp	Add virtual translate method to solver_factory class (#7780)	2025-08-14 11:54:34 -07:00
tactic2solver.h	booyah	2020-07-04 15:56:30 -07:00