Here is a list of all class members with links to the classes they belong to:
- l -
- l_buf : internal_state
- l_desc : internal_state
- lab : coloring
- label : PLA_t, symbolic_label_struct
- lag : NodeLag_T_
- large : watch
- large_clauses_watched_after_binary_clauses : kissat
- largecount() : CaDiCaL::Closure, closure
- largecounts() : CaDiCaL::Closure
- Last() : CaDiCaL::Last
- last : CaDiCaL::Factoring, CaDiCaL::Internal, CaDiCaL::Queue, CaDiCaL::Sweeper, cadical_kitten, factoring, Gluco2::Clause, Gluco2::vec< T >, Gluco::Clause, Gluco::vec< T >, inflate_state, kissat, kitten, Minisat::Clause, Minisat::vec< T >, queue, sweeper
- last_col : sm_matrix_struct, sm_row_struct
- last_dlevel : solver_t_
- last_eob_len : internal_state
- last_flush : internal_state
- last_irredundant : kissat
- last_learned : kissat
- last_lit : internal_state
- last_part : cube_struct
- last_row : sm_col_struct, sm_matrix_struct
- last_word : cube_struct
- lastblockatrestart : Gluco2::Solver, Gluco::Solver
- lastErr : bzFile
- lastIndexRed : Gluco2::Solver, Gluco::Solver
- LastLit : Gia_ManUnr_t_
- lazy_propagated() : CaDiCaL::Closure
- lazy_propagated_idx : CaDiCaL::Closure
- lbd : clause, clause_t, Gluco2::Clause, Gluco::Clause
- lbd_freeze_clause : satoko_opts
- lbdQueue : Gluco2::Solver, Gluco::Solver
- lbLBDFrozenClause : Gluco2::Solver, Gluco::Solver
- lbLBDMinimizingClause : Gluco2::Solver, Gluco::Solver
- lbool() : Gluco2::lbool, Gluco::lbool, Minisat::lbool
- lbSizeMinimizingClause : Gluco2::Solver, Gluco::Solver
- lCand : Ivy_FraigMan_t_
- lci : Rpo_Man_t_
- lClasses : Ivy_FraigMan_t_
- lCubes : FxuMatrix, MvcCoverStruct
- LData : Rtm_Edg_t_
- lea() : Gluco2::ClauseAllocator, Gluco2::RegionAllocator< T >, Gluco::ClauseAllocator, Gluco::RegionAllocator< T >, Minisat::ClauseAllocator, Minisat::RegionAllocator< T >
- leakage : SC_Cell_
- leakageI : SC_Cell_
- learn() : CaDiCaL::Learner, CaDiCaL::Wrapper
- learn_binary_tmp_or_full_clause() : CaDiCaL::Closure
- learn_congruence_unit() : CaDiCaL::Closure
- learn_congruence_unit_falsifies_lrat_chain() : CaDiCaL::Closure
- learn_congruence_unit_when_lhs_set() : CaDiCaL::Closure
- learn_empty_clause() : CaDiCaL::Internal
- learn_external_reason_clause() : CaDiCaL::Internal
- learn_unit_clause() : CaDiCaL::Internal
- learned : CaDiCaL::proof_clause, CaDiCaL::Stats, CaDiCaL::sweep_proof_clause, cadical_kitten, kitten, statistics
- learner : CaDiCaL::External, CaDiCaL::Wrapper
- learning() : CaDiCaL::Learner, CaDiCaL::Wrapper
- learnt : Gluco2::Clause, Gluco::Clause, Minisat::Clause, satset_t
- learnt_live : sat_solver2_t
- learnt_ratio : satoko_opts
- learnts : Gluco2::Solver, Gluco::Solver, Minisat::Solver, solver_t_, stats_t
- learnts_literals : Gluco2::Solver, Gluco::Solver, Minisat::Solver, stats_t
- learntsize_adjust_cnt : Gluco2::Solver, Gluco::Solver, Minisat::Solver
- learntsize_adjust_confl : Gluco2::Solver, Gluco::Solver, Minisat::Solver
- learntsize_adjust_inc : Minisat::Solver
- learntsize_adjust_start_confl : Minisat::Solver
- learntsize_factor : Minisat::Solver
- learntsize_inc : Minisat::Solver
- left : avl_node_struct, ltlNode_t, rrr::SW
- LemmaCall : CaDiCaL::Solver
- len : ct_data_s, DState, EState
- len_pack : EState
- lenbits : inflate_state
- lencode : inflate_state
- length : inflate_state, sm_col_struct, sm_row_struct
- lens : inflate_state
- lev : _reo_unit, saucy, varinfo_t
- Level : Abc_Obj_t_, Aig_Obj_t_, Amap_Obj_t_, CaDiCaL::Level, Dar_LibDat_t_, Dec_Node_t_, Fpga_NodeStruct_t_, Fraig_NodeStruct_t_, Gia_Rsb2Man_t_, If_Obj_t_, Iso_Dat_t_, Iso_Obj_t_, Ivy_Eval_t_, Ivy_Obj_t_, Kit_Node_t_, LUT, Map_NodeStruct_t_, NewBdd::Man, Nwk_Obj_t_, rrr::NewBdd::Man, Rwr_Node_t_, Rwt_Node_t_, Tas_Var_t_
- level : assigned, CaDiCaL::Averages, CaDiCaL::Internal, CaDiCaL::Var, cadical_kitten, Gluco2::Solver, Gluco2::Solver::VarData, Gluco::Solver, Gluco::Solver::VarData, gz_state, internal_state, kissat, kitten, Minisat::Solver, Minisat::Solver::VarData
- LevelBasePartitioner() : rrr::LevelBasePartitioner< Ntk >
- LevelBest : Dar_Man_t_, Ref_Man_t_
- LevelMax : Abc_Ntk_t_, Acb_Ntk_t_
- levels : CaDiCaL::Internal, kissat, sat_solver2_t, sat_solver3_t, sat_solver_t, saucy_stats, solver_t_
- levelsreused : CaDiCaL::Stats
- lhs : CaDiCaL::Gate, CaDiCaL::sort_literals_by_var_rank_except, CaDiCaL::sort_literals_by_var_smaller_except, gate
- LidrupTracer() : CaDiCaL::LidrupTracer
- likely_phase() : CaDiCaL::Internal
- likely_to_be_kept_clause() : CaDiCaL::Internal
- lim : CaDiCaL::Internal
- LimAbs : Ga2_Man_t_
- Limit : Aig_Sto_t_, CaDiCaL::Limit, Spl_Man_t_
- limit : CaDiCaL::Delay, CaDiCaL::Factoring, CaDiCaL::Internal, CaDiCaL::Solver, CaDiCaL::Sweeper, CaDiCaL::Walker, DState, factoring, reluctant, sweeper, unsigned_fifo
- limit_conflicts() : CaDiCaL::Internal
- limit_decisions() : CaDiCaL::Internal
- limit_local_search() : CaDiCaL::Internal
- limit_preprocessing() : CaDiCaL::Internal
- limit_terminate() : CaDiCaL::Internal
- limited : kissat, reluctant
- limits : cadical_kitten, kissat, kitten
- LimPpi : Ga2_Man_t_
- LineCur : Io_ReadBlif_t_
- lineno() : CaDiCaL::File
- link() : CaDiCaL::Internal
- links : CaDiCaL::Internal, cadical_kitten, kissat, kitten
- Lit : xSAT_Clause_t_
- lit : binary_tagged_literal, CaDiCaL::Bin, CaDiCaL::definition_extractor, CaDiCaL::literal_occ, CaDiCaL::LitIdPair, CaDiCaL::sweep_binary, clause, definition_extractor, extension, Gluco2::Clause, Gluco::Clause, import, litwatch, Minisat::Clause
- lit0 : Gluco2::Solver::NodeData
- lit1 : CaDiCaL::CompactBinary, Gluco2::Solver::NodeData
- lit2 : CaDiCaL::CompactBinary
- Lit2Bvar() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
- lit2citten() : CaDiCaL::Internal
- lit_bufsize : internal_state
- lit_equivalence() : CaDiCaL::lit_equivalence
- lit_implication() : CaDiCaL::lit_implication
- LitA : Tab_Obj_t_
- LitB : Tab_Obj_t_
- LitC : Tab_Obj_t_
- LitClausePair() : CaDiCaL::LitClausePair
- LitCountMax : Fx_Man_t_, Fxch_Man_t_, FxuDataStruct
- literals : CaDiCaL::CheckerClause, CaDiCaL::Clause, CaDiCaL::IdrupClause, CaDiCaL::LidrupClause, CaDiCaL::LratCheckerClause, CaDiCaL::proof_clause, CaDiCaL::Stats, CaDiCaL::sweep_blocked_clause, CaDiCaL::sweep_proof_clause, Rpo_Man_t_
- literals_factored : CaDiCaL::Stats
- literals_unfactored : CaDiCaL::Stats
- literalsreused : CaDiCaL::Stats
- LitIdPair() : CaDiCaL::LitIdPair
- LitIrregular() : NewBdd::Man, rrr::NewBdd::Man
- LitIsCompl() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
- LitIsEq() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
- LitNot() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
- LitNotCond() : NewBdd::Man, NewTt::Man, rrr::NewBdd::Man
- litpair_rank() : CaDiCaL::litpair_rank
- litpair_smaller() : CaDiCaL::litpair_smaller
- litRedundant() : Gluco2::Solver, Gluco::Solver, Minisat::Solver
- LitRegular() : NewBdd::Man, rrr::NewBdd::Man
- Lits : Pdr_Set_t_
- lits : CaDiCaL::Closure, CaDiCaL::Internal, cadical_kitten, clause, clause_t, closure, kitten, klause, litpair, litriple
- LitShift : Sbm_Man_t_
- LitVecIsEq() : Transduction::ManUtil< Man, lit, LitMax >
- ll16 : DState
- ll4 : DState
- lLits : FxuCube, FxuVar
- lo : CaDiCaL::Option
- Load() : rrr::AndNetwork, Ttopt::TruthTable, Ttopt::TruthTableCare, Ttopt::TruthTableReo
- LoadIndices() : Ttopt::TruthTable, Ttopt::TruthTableCare, Ttopt::TruthTableReo
- loadJust() : Gluco2::Solver
- loadJust_rec() : Gluco2::Solver
- loads : sat_solver3_t, sat_solver_t
- loc : FM_cell
- local_search() : CaDiCaL::Internal
- local_search_round() : CaDiCaL::Internal
- LocalBatchSize : Cec5_Man_t_
- localsearch : CaDiCaL::Inc, CaDiCaL::Limit
- localsearching : CaDiCaL::Internal
- locked : FM_cell, Gluco2::Solver, Gluco::Solver, Minisat::Solver
- log : eSLIM::SelectionStrategy< T >
- LogN : Sbl_Man_t_, Sbm_Man_t_, Seg_Man_t_
- LogPage : Lf_Mem_t_
- LogPageSze : Vec_Mem_t_
- lookahead() : CaDiCaL::External, CaDiCaL::Internal, CaDiCaL::Solver, internal_state
- lookahead_flush_probes() : CaDiCaL::Internal
- lookahead_generate_probes() : CaDiCaL::Internal
- lookahead_locc() : CaDiCaL::Internal
- lookahead_next_probe() : CaDiCaL::Internal
- lookahead_populate_locc() : CaDiCaL::Internal
- lookahead_probing() : CaDiCaL::Internal
- lookingahead : CaDiCaL::Internal
- Lookup() : NewBdd::Cache, rrr::NewBdd::Cache
- lookup() : Gluco2::OccLists< Idx, Vec, Deleted >, Gluco::OccLists< Idx, Vec, Deleted >, Minisat::OccLists< Idx, Vec, Deleted >
- loop_done : qps_problem
- loop_fail : qps_problem
- loop_k : qps_problem
- loop_list : qps_problem
- loop_max : qps_problem
- loop_num : qps_problem
- loop_penalty : qps_problem
- low : MtrNode
- lower_bound : stats_struct
- lPairs : FxuDouble
- lrat : CaDiCaL::Internal
- lrat_chain : CaDiCaL::Closure, CaDiCaL::Internal
- lrat_chain_and_gate : CaDiCaL::Closure
- lrat_stack : CaDiCaL::Vivifier
- LratChecker() : CaDiCaL::LratChecker
- LratTracer() : CaDiCaL::LratTracer
- lrn : clause_t
- lSingles : FxuMatrix
- luby_restart : Minisat::Solver
- LUCKY : CaDiCaL::Internal
- lucky : CaDiCaL::Stats
- lucky_phases() : CaDiCaL::Internal
- lucky_propagate_discrepency() : CaDiCaL::Internal
- lut_size : acd::ac_decomposition_params, acd::acdXX_params
- LutMask : Exa3_Man_t_, Zyx_Man_t_
- LutMax : Fpga_LutLibStruct_t_, If_LibLut_t_, Mpm_LibLut_t_
- LutSize : If_DsdMan_t_, Mini_Lut_t_, Sbl_Man_t_
- LValue : Fpga_NodeStruct_t_, If_Obj_t_
- lVars : FxuMatrix
- lww : Ttopt::TruthTable
