Cargo Features
[dependencies]
splr = { version = "0.17.2", default-features = false, features = ["assign_rate", "best_phases_tracking", "bi_clause_completion", "boundary_check", "chrono_BT", "no_clause_elimination", "clause_rewarding", "clause_vivification", "debug_propagation", "dynamic_restart_threshold", "EMA_calibration", "EVSIDS", "incremental_solver", "just_used", "LRB_rewarding", "maintain_watch_cache", "no_IO", "platform_wasm", "reason_side_rewarding", "rephase", "reward_annealing", "stochastic_local_search", "support_user_assumption", "suppress_reason_chain", "trace_elimination", "trace_equivalency", "trail_saving", "two_mode_reduction", "unsafe_access"] }- default = LRB_rewarding, clause_vivification, dynamic_restart_threshold, reason_side_rewarding, rephase, reward_annealing, trail_saving, two_mode_reduction, unsafe_access
-
These default features are set whenever
splris added withoutdefault-features = false - assign_rate
-
for debug and study
- best_phases_tracking rephase
-
save the best-so-far assignment, used by 'rephase'
- bi_clause_completion
-
this will increase memory pressure
- boundary_check
-
for debug
Affects
assign::Var.propagated_at,assign::Var.timestamp,assign::Var.state,assign::Assign,assign::DebugReportIF,cdb::ClauseIF.timestamp,cdb::ClauseIF.set_birth,cdb::ClauseDBIF.watch_cache_contains,cdb::ClauseDBIF.watch_caches,cdb::ClauseDBIF.is_garbage_collected,cdb::Clause.birth,cdb::Clause.moved_at,types::Propagate,types::VarState… - chrono_BT
-
NOT WORK
- no_clause_elimination incremental_solver?
-
pre(in)-processor setting
- clause_rewarding
-
clauses have activities w/ decay rate
- clause_vivification default
-
pre(in)-processor setting
- debug_propagation
-
for debug
- dynamic_restart_threshold default
-
control restart spans like Glucose
- EMA_calibration
-
each exponential moving average has a calbration value
- EVSIDS
-
Eponential Variable State Independent Decaying Sum
- incremental_solver = no_clause_elimination
-
Affects
cdb::ClauseDBIF.make_permanent_immortal,solver::SolverIter… - just_used
-
Var and clause have 'just_used' flags
- LRB_rewarding default
-
Vearning Rate Based rewarding, a new var activity criteria
- maintain_watch_cache
-
for DEBUG
- no_IO
-
to embed Splr into non-std environments
Affects
unsat_certificate::CertificationStore… - platform_wasm = instant
- reason_side_rewarding default
-
an idea used in Learning-rate based rewarding
- rephase default stochastic_local_search? = best_phases_tracking
-
Affects
assign::AssignIF.best_phases_invalid,select::VarSelectIF.best_phases_ref,select::VarSelectIF.override_rephasing_target,select::VarSelectIF.select_rephasing_target,select::VarSelectIF.check_consistency_of_best_phases… - reward_annealing default
-
use bigger and smaller decay rates cycliclly
- stochastic_local_search = rephase
- support_user_assumption
-
NOT WORK (defined in Glucose)
Affects
state::State.conflicts… - suppress_reason_chain
-
make direct links between a dicision var and its implications
- trace_analysis trace_elimination
-
for debug
- trace_equivalency
-
for debug
- trail_saving default
-
reduce propagation cost by reusing propagation chain
- two_mode_reduction default
-
exploration mode and exploitation mode since 0.17
- unsafe_access default
-
access elements of vectors without boundary checking
Features from optional dependencies
In crates that don't use the dep: syntax, optional dependencies automatically become Cargo features. These features may have been created by mistake, and this functionality may be removed in the future.