Nikolaj Bjorner adad468cd7 allow copy within a user scope #6827 ... this will allow copying the solver state within a scope. The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.		2023-07-31 19:46:08 -07:00
..
assertions	allow copy within a user scope #6827	2023-07-31 19:46:08 -07:00
check_logic.cpp	Typo Fixes (#6803)	2023-07-09 11:56:10 -07:00
check_logic.h	debug arith/mbi	2020-11-02 12:13:19 -08:00
check_sat_result.cpp	Typo Fixes (#6803)	2023-07-09 11:56:10 -07:00
check_sat_result.h	fixes to mbqi in the new core based on #6575	2023-02-10 16:56:06 -08:00
CMakeLists.txt	create simplifier_solver wrapper to supply simplifier layer	2023-01-30 16:12:25 -08:00
combined_solver.cpp	experimental feature to access congruence closure of SimpleSolver	2022-12-30 21:41:27 -08: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_tactical.cpp	fix #6528	2023-01-10 14:42:23 -08:00
parallel_tactical.h	add missing tactic descriptions, add rewrite for tamagochi	2023-01-08 13:32:26 -08:00
progress_callback.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
simplifier_solver.cpp	Some UP bugfixes in the new core (#6673)	2023-04-08 12:50:46 -07:00
simplifier_solver.h	Add simplification customization for SMTLIB2	2023-01-30 22:38:51 -08: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 model and proof converters to self-contained module	2022-11-03 05:23:01 -07:00
solver.h	experimental feature to access congruence closure of SimpleSolver	2022-12-30 21:41:27 -08:00
solver2tactic.cpp	move model and proof converters to self-contained module	2022-11-03 05:23:01 -07:00
solver2tactic.h	move model and proof converters to self-contained module	2022-11-03 05:23:01 -07:00
solver_na2as.cpp	update proof formats for new core	2022-09-28 10:40:43 -07:00
solver_na2as.h	update proof formats for new core	2022-09-28 10:40:43 -07:00
solver_pool.cpp	experimental feature to access congruence closure of SimpleSolver	2022-12-30 21:41:27 -08:00
solver_pool.h	booyah	2020-07-04 15:56:30 -07:00
solver_preprocess.cpp	add unconstrained elimination for sequences	2023-03-20 17:07:04 +01:00
solver_preprocess.h	add unconstrained elimination for sequences	2023-03-20 17:07:04 +01:00
tactic2solver.cpp	allow copy within a user scope #6827	2023-07-31 19:46:08 -07:00
tactic2solver.h	booyah	2020-07-04 15:56:30 -07:00