Here is a list of all functions with links to the classes they belong to:

- s -

• Sange() : CaDiCaL::Sange
• sat_solver_jftr() : Gluco2::Solver
• sat_solver_mark_cone() : Gluco2::Solver, Gluco::Solver
• sat_solver_reset() : Gluco2::Solver
• sat_solver_set_jftr() : Gluco2::Solver
• sat_solver_set_var_fanin_lit() : Gluco2::Solver, Gluco::Solver
• sat_solver_start_new_round() : Gluco2::Solver, Gluco::Solver
• satisfied() : CaDiCaL::Internal, Gluco2::Solver, Gluco::Solver, Minisat::Solver
• SatSolver() : rrr::SatSolver< Ntk >
• Save() : rrr::AndNetwork, Ttopt::TruthTable, Ttopt::TruthTableCare, Ttopt::TruthTableReo
• save_add_clear_core() : CaDiCaL::Internal
• save_core() : CaDiCaL::Internal
• SaveIndices() : Ttopt::TruthTable, Ttopt::TruthTableCare, Ttopt::TruthTableReo
• scale() : CaDiCaL::Internal
• scheduable_variable() : CaDiCaL::Internal
• schedule_all_other_not_scheduled_yet() : CaDiCaL::Internal
• schedule_factorization() : CaDiCaL::Internal
• schedule_inner() : CaDiCaL::Internal
• schedule_literal() : CaDiCaL::Closure
• schedule_outer() : CaDiCaL::Internal
• schedule_sweeping() : CaDiCaL::Internal
• scheduled_variable() : CaDiCaL::Internal
• Scheduler() : rrr::Scheduler< Ntk, Opt, Par >::CompareJobPointers, rrr::Scheduler< Ntk, Opt, Par >::Job, rrr::Scheduler< Ntk, Opt, Par >
• score() : CaDiCaL::Internal, CaDiCaL::Walker
• score_smaller() : CaDiCaL::score_smaller
• search() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
• search_assign() : CaDiCaL::Internal
• search_assign_driving() : CaDiCaL::Internal
• search_assign_external() : CaDiCaL::Internal
• search_assume_decision() : CaDiCaL::Internal
• search_condeq() : CaDiCaL::Closure
• search_limits_hit() : CaDiCaL::Internal
• second_literal_in_binary_clause() : CaDiCaL::Internal
• second_literal_in_binary_clause_lrat() : CaDiCaL::Internal
• seed() : CaDiCaL::Random
• SelectionStrategy() : eSLIM::SelectionStrategy< T >
• self_subsuming_factor() : CaDiCaL::Internal
• set() : CaDiCaL::Config, CaDiCaL::Options, CaDiCaL::Signal, CaDiCaL::Solver
• set_long_option() : CaDiCaL::Solver
• set_mode() : CaDiCaL::Internal
• set_mu1_reason() : CaDiCaL::Closure
• set_mu2_reason() : CaDiCaL::Closure
• set_mu4_reason() : CaDiCaL::Closure
• set_parent_reason_literal() : CaDiCaL::Internal
• set_probehbr_lrat() : CaDiCaL::Internal
• set_tainted_literal() : CaDiCaL::Internal
• set_val() : CaDiCaL::Internal
• setbit() : CaDiCaL::Internal
• setCanBeDel() : Gluco2::Clause, Gluco::Clause
• setConfBudget() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
• setDecisionVar() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
• setExc() : Rewire::Miaig
• setFrozen() : Gluco2::SimpSolver, Gluco::SimpSolver, Minisat::SimpSolver
• setIncrementalMode() : Gluco2::Solver, Gluco::Solver
• setItpcSize() : Gluco2::Solver
• setJust() : Gluco2::Solver
• setLBD() : Gluco2::Clause, Gluco::Clause
• setName() : Rewire::Miaig
• setNewRound() : Gluco2::Solver
• setPolarity() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
• SetPrintLine() : rrr::Optimizer< Ntk, Ana >, rrr::Optimizer< Ntk, Ana >::Stats
• setPropBudget() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
• SetRef() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
• setSeed() : eSLIM::SelectionStrategy< T >
• setSizeWithoutSelectors() : Gluco2::Clause, Gluco::Clause
• SetValue() : Ttopt::TruthTableRewrite
• setVarFaninLits() : Gluco2::Solver
• share() : Rewire::Miaig
• ShiftToMajority() : Ttopt::TruthTableRewrite
• shrink() : CaDiCaL::heap< C >, Gluco2::Clause, Gluco2::vec< T >, Gluco::Clause, Gluco::vec< T >, Minisat::Clause, Minisat::vec< T >
• shrink_() : Gluco2::vec< T >, Gluco::vec< T >, Minisat::vec< T >
• shrink_along_reason() : CaDiCaL::Internal
• shrink_and_gate() : CaDiCaL::Closure
• shrink_and_minimize_clause() : CaDiCaL::Internal
• shrink_block() : CaDiCaL::Internal
• shrink_clause() : CaDiCaL::Internal
• shrink_literal() : CaDiCaL::Internal
• shrink_next() : CaDiCaL::Internal
• shrink_trail_larger() : CaDiCaL::shrink_trail_larger
• shrink_trail_negative_rank() : CaDiCaL::shrink_trail_negative_rank
• shrunken_block_no_uip() : CaDiCaL::Internal
• shrunken_block_uip() : CaDiCaL::Internal
• shuffle_queue() : CaDiCaL::Internal
• shuffle_scores() : CaDiCaL::Internal
• SiftReo() : Ttopt::TruthTable
• signature() : CaDiCaL::Solver
• simplify() : CaDiCaL::Solver, Gluco2::Solver, Gluco::Solver, Minisat::Solver
• simplify_and_add_to_proof_chain() : CaDiCaL::Closure
• simplify_and_gate() : CaDiCaL::Closure
• simplify_and_sort_xor_lrat_clauses() : CaDiCaL::Closure
• simplify_gate() : CaDiCaL::Closure
• simplify_gates() : CaDiCaL::Closure
• simplify_ite_gate() : CaDiCaL::Closure
• simplify_ite_gate_condition_set() : CaDiCaL::Closure
• simplify_ite_gate_produce_unit_lrat() : CaDiCaL::Closure
• simplify_ite_gate_then_else_set() : CaDiCaL::Closure
• simplify_ite_gate_to_and() : CaDiCaL::Closure
• simplify_unit_xor_lrat_clauses() : CaDiCaL::Closure
• simplify_xor_clause() : CaDiCaL::Closure
• simplify_xor_gate() : CaDiCaL::Closure
• SimpSolver() : Gluco2::SimpSolver, Gluco::SimpSolver, Minisat::SimpSolver
• Simulator() : rrr::Simulator< Ntk >
• size() : CaDiCaL::File, CaDiCaL::heap< C >, Gluco2::bqueue< T >, Gluco2::Clause, Gluco2::CMap< T >, Gluco2::Heap2< Comp, Obj >, Gluco2::Heap< Comp >, Gluco2::Queue< T >, Gluco2::RegionAllocator< T >, Gluco2::vec< T >, Gluco::bqueue< T >, Gluco::Clause, Gluco::CMap< T >, Gluco::Heap< Comp >, Gluco::Queue< T >, Gluco::RegionAllocator< T >, Gluco::vec< T >, Minisat::Clause, Minisat::CMap< T >, Minisat::Heap< Comp >, Minisat::Queue< T >, Minisat::RegionAllocator< T >, Minisat::vec< T >, Reap
• sizeWithoutSelectors() : Gluco2::Clause, Gluco::Clause
• skip_and_gate() : CaDiCaL::Closure
• skip_xor_gate() : CaDiCaL::Closure
• smudge() : Gluco2::OccLists< Idx, Vec, Deleted >, Gluco::OccLists< Idx, Vec, Deleted >, Minisat::OccLists< Idx, Vec, Deleted >
• sol() : CaDiCaL::External
• solve() : CaDiCaL::External, CaDiCaL::Internal, CaDiCaL::Solver, eSLIM::CadicalSolver, eSLIM::KissatSolver, Gluco2::SimpSolver, Gluco2::Solver, Gluco::SimpSolver, Gluco::Solver, Minisat::SimpSolver, Minisat::Solver
• solve_() : Gluco2::SimpSolver, Gluco2::Solver, Gluco::SimpSolver, Gluco::Solver, Minisat::SimpSolver, Minisat::Solver
• solve_query() : CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, CaDiCaL::Proof, CaDiCaL::Tracer
• solve_time() : CaDiCaL::Internal
• solveLimited() : Gluco2::SimpSolver, Gluco2::Solver, Gluco::SimpSolver, Gluco::Solver, Minisat::SimpSolver, Minisat::Solver
• Solver() : CaDiCaL::Solver, Gluco2::Solver, Gluco::Solver, Minisat::Solver
• sort_and_reuse_assumptions() : CaDiCaL::Internal
• sort_assumptions_positive_rank() : CaDiCaL::sort_assumptions_positive_rank
• sort_assumptions_smaller() : CaDiCaL::sort_assumptions_smaller
• sort_literals_by_var() : CaDiCaL::Closure
• sort_literals_by_var_except() : CaDiCaL::Closure
• sort_literals_by_var_rank() : CaDiCaL::sort_literals_by_var_rank
• sort_literals_by_var_rank_except() : CaDiCaL::sort_literals_by_var_rank_except
• sort_literals_by_var_smaller() : CaDiCaL::sort_literals_by_var_smaller
• sort_literals_by_var_smaller_except() : CaDiCaL::sort_literals_by_var_smaller_except
• sort_watches() : CaDiCaL::Internal
• SortFanins() : rrr::AndNetwork
• stabilizing() : CaDiCaL::Internal
• State() : Transduction::Transduction< Man, Param, lit, LitMax >
• state() : CaDiCaL::Solver
• static_truth_table() : kitty::static_truth_table< NumVars, false >
• statistics() : CaDiCaL::Solver
• Stats() : CaDiCaL::Stats
• StatTracer() : CaDiCaL::StatTracer
• status() : CaDiCaL::Solver
• StreamBuffer() : Gluco2::StreamBuffer, Gluco::StreamBuffer, Minisat::StreamBuffer
• strengthen() : CaDiCaL::IdrupTracer, CaDiCaL::LidrupTracer, CaDiCaL::Proof, CaDiCaL::Tracer, CaDiCaL::VeripbTracer, Gluco2::Clause, Gluco::Clause, Minisat::Clause
• strengthen_clause() : CaDiCaL::Internal, CaDiCaL::Proof
• strengthenClause() : Gluco2::SimpSolver, Gluco::SimpSolver, Minisat::SimpSolver
• StringOption() : Gluco2::StringOption, Gluco::StringOption, Minisat::StringOption
• substitute() : Gluco2::SimpSolver, Gluco::SimpSolver, Minisat::SimpSolver
• substitute_connected_clauses() : CaDiCaL::Internal
• substituted() : CaDiCaL::Flags
• subsume() : CaDiCaL::Internal
• subsume_check() : CaDiCaL::Internal
• subsume_clause() : CaDiCaL::Closure, CaDiCaL::Internal
• subsume_less_noccs() : CaDiCaL::subsume_less_noccs
• subsume_round() : CaDiCaL::Internal
• subsumes() : Gluco2::Clause, Gluco::Clause, Minisat::Clause
• Swap() : Ttopt::TruthTable, Ttopt::TruthTableCare, Ttopt::TruthTableReo
• swap() : CaDiCaL::Arena, CaDiCaL::lit_equivalence, CaDiCaL::lit_implication
• swap_averages() : CaDiCaL::Internal
• SwapIndex() : Ttopt::TruthTable
• Sweep() : rrr::AndNetwork
• sweep() : CaDiCaL::Internal
• sweep_add_clause() : CaDiCaL::Internal
• sweep_backbone_candidate() : CaDiCaL::Internal
• sweep_clause() : CaDiCaL::Internal
• sweep_dense_mode_and_watch_irredundant() : CaDiCaL::Internal
• sweep_dense_propagate() : CaDiCaL::Internal
• sweep_empty_clause() : CaDiCaL::Internal
• sweep_equivalence_candidates() : CaDiCaL::Internal
• sweep_extract_fixed() : CaDiCaL::Internal
• sweep_flip() : CaDiCaL::Internal
• sweep_flip_and_implicant() : CaDiCaL::Internal
• sweep_refine() : CaDiCaL::Internal
• sweep_refine_backbone() : CaDiCaL::Internal
• sweep_refine_partition() : CaDiCaL::Internal
• sweep_remove() : CaDiCaL::Internal
• sweep_repr() : CaDiCaL::Internal
• sweep_set_cadical_kitten_ticks_limit() : CaDiCaL::Internal
• sweep_solve() : CaDiCaL::Internal
• sweep_sparse_mode() : CaDiCaL::Internal
• sweep_substitute_lrat() : CaDiCaL::Internal
• sweep_substitute_new_equivalences() : CaDiCaL::Internal
• sweep_update_noccs() : CaDiCaL::Internal
• sweep_variable() : CaDiCaL::Internal
• Sweeper() : CaDiCaL::Sweeper