Nikolaj Bjorner 48b13291d1 add bv-size reduce #6137 ... - add option smt.bv.reduce_size. - it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant. This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.		2022-08-16 16:35:14 -07:00
..
assertions	add bv-size reduce #6137	2022-08-16 16:35:14 -07:00
check_logic.cpp	move to separate axiom management	2021-02-23 18:09:45 -08:00
check_logic.h	debug arith/mbi	2020-11-02 12:13:19 -08:00
check_sat_result.cpp	#5746	2022-01-02 11:35:55 -08:00
check_sat_result.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
CMakeLists.txt	move solver-params to params	2022-08-08 11:34:41 +03:00
combined_solver.cpp	Remove empty leaf destructors. (#6211)	2022-07-30 10:07:03 +01: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	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
mus.h	booyah	2020-07-04 15:56:30 -07:00
parallel_params.pyg	Fix whitespace issues in *.pyg.	2019-08-15 10:19:33 -07:00
parallel_tactic.cpp	parallel-tactic: fix deadlocking race between shutdown and get_task (#6152)	2022-07-11 09:26:11 -07:00
parallel_tactic.h	booyah	2020-07-04 15:56:30 -07:00
progress_callback.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
smt_logics.cpp	#4869 load datatype parsing for HORN logic	2021-10-26 11:54:29 +02:00
smt_logics.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
solver.cpp	move solver-params to params	2022-08-08 11:34:41 +03:00
solver.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
solver2tactic.cpp	add tactic name	2021-12-07 13:37:57 -08:00
solver2tactic.h	booyah	2020-07-04 15:56:30 -07:00
solver_na2as.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
solver_na2as.h	booyah	2020-07-04 15:56:30 -07:00
solver_pool.cpp	improve pre-processing	2022-04-15 12:55:26 +02:00
solver_pool.h	booyah	2020-07-04 15:56:30 -07:00
tactic2solver.cpp	Remove empty leaf destructors. (#6211)	2022-07-30 10:07:03 +01:00
tactic2solver.h	booyah	2020-07-04 15:56:30 -07:00