[−] List of all items
Structs
- CnfFormula
- Lit
- Var
- analyze_conflict::AnalyzeConflict
- analyze_conflict::LevelAbstraction
- assumptions::Assumptions
- binary::BinaryClauses
- checker::Checker
- checker::CheckerData
- clause::Clause
- clause::activity::ClauseActivity
- clause::alloc::ClauseAlloc
- clause::alloc::ClauseRef
- clause::db::ClauseDb
- clause::header::ClauseHeader
- cnf::CnfFormula
- cnf::NewVarIter
- config::SolverConfig
- config::SolverConfigUpdate
- context::Context
- context::parts::AnalyzeConflictP
- context::parts::AssignmentP
- context::parts::AssumptionsP
- context::parts::BinaryClausesP
- context::parts::ClauseActivityP
- context::parts::ClauseAllocP
- context::parts::ClauseDbP
- context::parts::ImplGraphP
- context::parts::ModelP
- context::parts::ProofP
- context::parts::ScheduleP
- context::parts::SolverConfigP
- context::parts::SolverStateP
- context::parts::TmpDataP
- context::parts::TmpFlagsP
- context::parts::TrailP
- context::parts::VariablesP
- context::parts::VsidsP
- context::parts::WatchlistsP
- decision::vsids::Vsids
- dimacs::DimacsHeader
- dimacs::DimacsParser
- lit::Lit
- lit::Var
- model::Model
- proof::Proof
- proof::map_step::MapStep
- prop::assignment::Assignment
- prop::assignment::Trail
- prop::graph::ImplGraph
- prop::graph::ImplNode
- prop::watch::Watch
- prop::watch::Watchlists
- schedule::Schedule
- schedule::luby::LubySequence
- solver::Solver
- state::SolverState
- tmp::TmpData
- tmp::TmpFlags
- variables::Variables
- variables::data::VarData
- variables::var_map::VarBiMap
- variables::var_map::VarBiMapMut
- variables::var_map::VarMap
Enums
- ProofFormat
- assumptions::EnqueueAssumption
- cdcl::FoundConflict
- checker::CheckedProofStep
- checker::CheckerError
- checker::ProofTranscriptStep
- clause::db::Tier
- dimacs::ParserError
- proof::ProofFormat
- prop::graph::Conflict
- prop::graph::Reason
- solver::ProofFormat
- solver::SolverError
- state::SatState
- variables::data::SamplingMode
Traits
- ExtendFormula
- checker::ProofProcessor
- checker::ProofTranscriptProcessor
- cnf::ExtendFormula
- cnf::UniformTuple
Macros
Functions
- analyze_conflict::add_literal
- analyze_conflict::analyze_conflict
- analyze_conflict::minimize_clause
- assumptions::analyze_assumption_conflict
- assumptions::enqueue_assumption
- assumptions::set_assumptions
- binary::simplify_binary
- cdcl::conflict_step
- cdcl::find_conflict
- clause::activity::bump_clause_activity
- clause::activity::decay_clause_activities
- clause::activity::rescale_clause_activities
- clause::activity::rescale_limit
- clause::assess::assess_learned_clause
- clause::assess::bump_clause
- clause::assess::select_tier
- clause::db::add_clause
- clause::db::clauses_iter
- clause::db::delete_clause
- clause::db::filter_clauses
- clause::db::set_clause_tier
- clause::db::try_delete_clause
- clause::gc::collect_garbage
- clause::gc::collect_garbage_now
- clause::gc::mark_asserting_clauses
- clause::reduce::dedup_and_mark_by_tier
- clause::reduce::reduce_locals
- clause::reduce::reduce_mids
- cnf::strategy::cnf_formula
- cnf::strategy::vec_formula
- context::config_changed
- context::set_var_count
- decision::initialize_var
- decision::make_available
- decision::make_decision
- decision::remove_var
- dimacs::write_dimacs
- dimacs::write_dimacs_clauses
- dimacs::write_dimacs_header
- glue::compute_glue
- lit::strategy::lit
- lit::strategy::var
- load::load_clause
- model::reconstruct_global_model
- proof::add_clause
- proof::add_step
- proof::clause_count_delta
- proof::close_proof
- proof::drat::drat_step
- proof::drat::write_binary_literals
- proof::drat::write_binary_step
- proof::drat::write_literals
- proof::drat::write_step
- proof::flush_proof
- proof::handle_io_errors
- proof::handle_self_check_result
- proof::solve_finished
- proof::write_varisat_step
- prop::assignment::backtrack
- prop::assignment::enqueue_assignment
- prop::assignment::fast_option_eq
- prop::assignment::full_restart
- prop::assignment::restart
- prop::binary::propagate_binary
- prop::long::propagate_long
- prop::propagate
- prop::watch::enable_watchlists
- schedule::schedule_step
- unit_simplify::prove_units
- unit_simplify::resurrect_unit
- unit_simplify::unit_simplify
- variables::delete_global_if_unused
- variables::global_from_user
- variables::initialize_solver_var
- variables::new_user_var
- variables::observe_internal_vars
- variables::remove_solver_var
- variables::set_sampling_mode
- variables::solver_from_global
- variables::solver_from_user
- variables::solver_from_user_lits
Typedefs
Constants
- clause::header::ACTIVE_OFFSET
- clause::header::ACTIVE_WORD
- clause::header::ACTIVITY_WORD
- clause::header::DELETED_OFFSET
- clause::header::DELETED_WORD
- clause::header::GLUE_MASK
- clause::header::GLUE_OFFSET
- clause::header::GLUE_WORD
- clause::header::HEADER_LEN
- clause::header::MARK_OFFSET
- clause::header::MARK_WORD
- clause::header::TIER_MASK
- clause::header::TIER_OFFSET
- clause::header::TIER_WORD
- config::_DERIVE_Default_FOR_SolverConfig
- config::_IMPL_DESERIALIZE_FOR_SolverConfigUpdate
- config::_IMPL_SERIALIZE_FOR_SolverConfigUpdate
- context::parts::ProofP
- solver::_DERIVE_failure_Fail_FOR_SolverError
- solver::_DERIVE_failure_core_fmt_Display_FOR_SolverError
- variables::var_map::NO_VAR_IDX