Nikolaj Bjorner 2e00f2f32d Propagator (#5845) ... * user propagator without ids Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * user propagator without ids Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix signature Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * references #5818 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix c++ build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * switch to vs 2022 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * switch 2022 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Update propagator example (I) (#5835) * fix #5829 * na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * switch to vs 2022 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Adapted the example to the changes in the propagator Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> * context goes out of scope in stack allocation, so can't used scoped context when passing objects around * parameter check Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add rewriter Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Fixed bug in user-propagator "created" (#5843) Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>		2022-02-17 09:21:41 +02:00
..
assertions	add simplification with qe-lite as an option #5767	2022-01-12 03:41:21 -08: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	fix #4662	2020-08-27 15:05:35 -07:00
CMakeLists.txt	separate component for asserted_formulas to break dependency cycles	2021-03-17 15:51:38 -07:00
combined_solver.cpp	integrate v2 of lns	2021-02-04 15:47:40 -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_tactic.cpp	add tactic name	2021-12-07 13:37:57 -08:00
parallel_tactic.h	booyah	2020-07-04 15:56:30 -07:00
progress_callback.h	booyah	2020-07-04 15:56:30 -07: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	extract also units from search state	2022-02-07 06:16:22 +02:00
solver.h	extract also units from search state	2022-02-07 06:16:22 +02: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_params.pyg	remove incorrect and inefficient default model conversion	2021-07-15 18:47:25 +02:00
solver_pool.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
solver_pool.h	booyah	2020-07-04 15:56:30 -07:00
tactic2solver.cpp	Propagator (#5845)	2022-02-17 09:21:41 +02:00
tactic2solver.h	booyah	2020-07-04 15:56:30 -07:00