Nikolaj Bjorner 9fc4015c46 remove ternary clause optimization ... Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.		2022-10-30 03:57:39 -07:00
..
sat_solver	added API to monitor clause inferences	2022-10-19 08:34:55 -07:00
smt	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
tactic	#6364 - remove option of redundant clauses from internalization	2022-10-24 00:38:31 -07:00
CMakeLists.txt	trying trim	2022-10-04 16:25:40 +02:00
dimacs.cpp	overhaul of proof format for new solver	2022-08-28 17:44:33 -07:00
dimacs.h	overhaul of proof format for new solver	2022-08-28 17:44:33 -07:00
sat_aig_cuts.cpp	remove '#include <iostream>' from headers and from unneeded places	2022-06-17 14:10:19 +01:00
sat_aig_cuts.h	running updates to bv_solver (#4674)	2020-09-07 20:35:32 -07:00
sat_aig_finder.cpp	More cases needed to find all ite clauses.	2020-02-19 09:03:58 -08:00
sat_aig_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_allocator.h	booyah	2020-07-04 15:56:30 -07:00
sat_anf_simplifier.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_anf_simplifier.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_asymm_branch.cpp	optimizations to bv-solver and euf-egraph (#4698)	2020-09-20 06:47:27 -07:00
sat_asymm_branch.h	booyah	2020-07-04 15:56:30 -07:00
sat_asymm_branch_params.pyg	bug fixes	2018-02-19 21:49:03 -08:00
sat_bcd.cpp	bcd	2020-01-16 20:37:22 -08:00
sat_bcd.h	bool_vector, some spacer tidy	2020-04-05 12:59:04 -07:00
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	booyah	2020-07-04 15:56:30 -07:00
sat_binspr.cpp	prepare for theory plugins	2020-09-02 10:42:18 -07:00
sat_binspr.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_clause.cpp	fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts	2019-02-22 11:14:20 +01:00
sat_clause.h	bv and gc of literals (#4692)	2020-09-17 14:24:07 -07:00
sat_clause_set.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
sat_clause_set.h	booyah	2020-07-04 15:56:30 -07:00
sat_clause_use_list.cpp	working on completing ATE/ALA for acce and abce	2018-01-29 20:32:06 -08:00
sat_clause_use_list.h	booyah	2020-07-04 15:56:30 -07:00
sat_cleaner.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_cleaner.h	booyah	2020-07-04 15:56:30 -07:00
sat_config.cpp	add examples with proof replay	2022-10-19 17:43:56 -07:00
sat_config.h	add examples with proof replay	2022-10-19 17:43:56 -07:00
sat_cut_simplifier.cpp	Use nullptr consistently instead of 0 or NULL.	2022-08-01 14:24:32 +03:00
sat_cut_simplifier.h	fixing #4670 (#4682)	2020-09-10 04:35:11 -07:00
sat_cutset.cpp	fix gcc 9/10 warnings	2020-05-23 16:39:09 +01:00
sat_cutset.h	remove unneeded constructors (last round)	2020-07-12 17:41:57 +01:00
sat_cutset_compute_shift.h	Make sure all headers do #pragma once. (#6188)	2022-07-23 10:41:14 -07:00
sat_ddfw.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_ddfw.h	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_drat.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_drat.h	remove deprecated theory aware drat functionality	2022-10-24 08:32:10 -07:00
sat_elim_eqs.cpp	fix bug in root setting exposed by incremental mode pb_solver	2022-01-18 10:55:27 +01:00
sat_elim_eqs.h	booyah	2020-07-04 15:56:30 -07:00
sat_elim_vars.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_elim_vars.h	booyah	2020-07-04 15:56:30 -07:00
sat_extension.h	wip - remove stale skaffolding for retrieving sub-hints.	2022-10-16 17:18:08 -07:00
sat_gc.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_integrity_checker.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_integrity_checker.h	booyah	2020-07-04 15:56:30 -07:00
sat_justification.h	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_local_search.cpp	#5324	2021-06-06 10:58:47 -07:00
sat_local_search.h	In src/sat/sat_local_search.*: Changed the return type of constraint_slack to int64_t instead of uint64_t to match the m_slack member of the constraint struct, which has type int64_t. (#5360)	2021-06-21 14:40:31 -07:00
sat_lookahead.cpp	Add support of the SunOS platform (Solaris, OpenSolaris, OpenIndiana) (#4757)	2020-10-27 11:39:21 -07:00
sat_lookahead.h	don't rename uint_set but keep the original name	2022-09-18 17:22:59 -07:00
sat_lut_finder.cpp	add simplifiation pass	2020-02-22 11:21:53 -08:00
sat_lut_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_model_converter.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_model_converter.h	flush gmc for sat-preprocessor model bug #4532	2020-07-26 14:30:48 -07:00
sat_mus.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_mus.h	booyah	2020-07-04 15:56:30 -07:00
sat_npn3_finder.cpp	No need to hash quaternaries for AND.	2020-03-01 04:10:25 -08:00
sat_npn3_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_parallel.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_parallel.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_params.pyg	wip - updates to proof logging and self-checking	2022-10-16 23:33:30 +02:00
sat_prob.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
sat_prob.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
sat_probing.cpp	fix #4868	2020-12-07 10:27:00 -08:00
sat_probing.h	optimizations to bv-solver and euf-egraph (#4698)	2020-09-20 06:47:27 -07:00
sat_proof_trim.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_proof_trim.h	fixes to trim	2022-10-07 09:58:12 +02:00
sat_scc.cpp	expose extract roots as separate	2022-01-31 11:56:44 -08:00
sat_scc.h	expose extract roots as separate	2022-01-31 11:56:44 -08:00
sat_scc_params.pyg	working on completing ATE/ALA for acce and abce	2018-01-29 20:32:06 -08:00
sat_simplifier.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_simplifier.h	#5445	2021-08-02 20:41:34 -07:00
sat_simplifier_params.pyg	Fix whitespace issues in *.pyg.	2019-08-15 10:19:33 -07:00
sat_solver.cpp	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_solver.h	remove ternary clause optimization	2022-10-30 03:57:39 -07:00
sat_solver_core.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
sat_types.h	remove ternary clause optimization	2022-10-30 03:57:39 -07: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	align parity with signs	2020-02-26 15:49:58 -08:00
sat_xor_finder.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00