Nikolaj Bjorner e4697fe18e remove set cardinality operators from array theory. Make final-check use priority levels ... Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation. To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.		2026-02-18 20:56:51 -08:00
..
sat_solver	remove a few useless dynamic casts	2025-09-13 21:06:55 +01:00
smt	remove set cardinality operators from array theory. Make final-check use priority levels	2026-02-18 20:56:51 -08:00
tactic	remove a few useless dynamic casts	2025-09-13 21:06:55 +01:00
CMakeLists.txt	remove unused bdd based variable elimination	2025-04-14 16:07:41 -07:00
dimacs.cpp	deal with compiler warnings and include value exchange prior to final check.	2025-01-24 09:40:33 -08:00
dimacs.h	inherit more exceptions from std::exception	2024-11-04 13:52:14 -08:00
sat_aig_cuts.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_aig_cuts.h
sat_aig_finder.cpp	Typo Fixes (#6803)	2023-07-09 11:56:10 -07:00
sat_aig_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_allocator.h
sat_anf_simplifier.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_anf_simplifier.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_asymm_branch.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_asymm_branch.h
sat_asymm_branch_params.pyg
sat_bcd.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_bcd.h
sat_big.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_big.h
sat_clause.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_clause.h	remove unneeded iterator functions	2024-09-23 12:59:04 +01:00
sat_clause_set.cpp
sat_clause_set.h
sat_clause_use_list.cpp	fixes to build warnings	2024-09-30 08:23:31 -07:00
sat_clause_use_list.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_cleaner.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_cleaner.h
sat_config.cpp	remove binspr experiment	2025-01-12 13:39:26 -08:00
sat_config.h	remove binspr experiment	2025-01-12 13:39:26 -08:00
sat_cut_simplifier.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_cut_simplifier.h
sat_cutset.cpp	remove a few string copies	2023-12-20 16:55:09 +00:00
sat_cutset.h	Use noexcept more. (#7058)	2023-12-16 12:14:53 +00:00
sat_cutset_compute_shift.h	Make sure all headers do #pragma once. (#6188)	2022-07-23 10:41:14 -07:00
sat_ddfw_wrapper.cpp	flip tabu on predicate being repaired, add model rotation code	2025-01-02 14:39:36 -08:00
sat_ddfw_wrapper.h	flip tabu on predicate being repaired, add model rotation code	2025-01-02 14:39:36 -08:00
sat_drat.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_drat.h	remove deprecated theory aware drat functionality	2022-10-24 08:32:10 -07:00
sat_elim_eqs.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_elim_eqs.h
sat_extension.h	fix build	2023-12-02 19:52:59 -08:00
sat_gc.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_integrity_checker.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_integrity_checker.h	fixes to trim	2023-07-03 19:26:19 +02:00
sat_justification.h	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_local_search.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_local_search.h	remove default destructors	2024-10-02 22:20:12 +01:00
sat_lookahead.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_lookahead.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_lut_finder.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_lut_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_model_converter.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_model_converter.h	remove default destructors	2024-10-02 22:20:12 +01:00
sat_mus.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_mus.h	remove default destructors & some default constructors	2024-09-04 22:30:23 +01:00
sat_npn3_finder.cpp
sat_npn3_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_parallel.cpp	set clean shutdown for local search and re-enable local search when it parallelizes with PB solver	2024-06-30 16:06:51 -07:00
sat_parallel.h	set clean shutdown for local search and re-enable local search when it parallelizes with PB solver	2024-06-30 16:06:51 -07:00
sat_prob.cpp	create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier	2023-08-03 09:48:07 -07:00
sat_prob.h	fix #6599	2023-02-18 14:18:02 -08:00
sat_probing.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_probing.h
sat_proof_trim.cpp	fix bug in trim code missing dependecy	2025-06-07 15:39:05 -07:00
sat_proof_trim.h	fixup dependencies for trim'	2023-07-17 11:00:02 -07:00
sat_scc.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_scc.h	expose extract roots as separate	2022-01-31 11:56:44 -08:00
sat_scc_params.pyg
sat_simplifier.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_simplifier.h	fix #7532	2025-01-27 10:51:12 -08:00
sat_simplifier_params.pyg	remove unused bdd based variable elimination	2025-04-14 16:07:41 -07:00
sat_solver.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_solver.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_solver_core.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
sat_types.h	fixes and tests for arith-sls	2023-02-28 17:40:09 -08:00
sat_watched.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_watched.h	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_xor_finder.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
sat_xor_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00