| active(int lit) | CaDiCaL::Internal | inline |
| active() const | CaDiCaL::Internal | inline |
| add_core(Sweeper &sweeper, unsigned core_idx) | CaDiCaL::Internal | |
| add_external_clause(int propagated_lit=0, bool no_backtrack=false) | CaDiCaL::Internal | |
| add_factored_divider(Quotient *, int) | CaDiCaL::Internal | |
| add_factored_quotient(Quotient *, int not_fresh) | CaDiCaL::Internal | |
| add_literal_to_environment(Sweeper &sweeper, unsigned depth, int) | CaDiCaL::Internal | |
| add_new_original_clause(int64_t) | CaDiCaL::Internal | |
| add_observed_var(int ilit) | CaDiCaL::Internal | |
| add_original_lit(int lit) | CaDiCaL::Internal | |
| add_self_subsuming_factor(Quotient *, Quotient *) | CaDiCaL::Internal | |
| add_sweep_binary(sweep_proof_clause, int lit, int other) | CaDiCaL::Internal | |
| already_solved() | CaDiCaL::Internal | |
| analyze() | CaDiCaL::Internal | |
| analyze_literal(int lit, int &open, int &resolvent_size, int &antecedent_size) | CaDiCaL::Internal | inline |
| analyze_reason(int lit, Clause *, int &open, int &resolvent_size, int &antecedent_size) | CaDiCaL::Internal | inline |
| analyzed | CaDiCaL::Internal | |
| apply_factoring(Factoring &factoring, Quotient *q) | CaDiCaL::Internal | |
| arena | CaDiCaL::Internal | |
| arenaing() | CaDiCaL::Internal | |
| ask_decision() | CaDiCaL::Internal | |
| ask_external_clause() | CaDiCaL::Internal | |
| assign_original_unit(int64_t, int) | CaDiCaL::Internal | |
| assign_unit(int lit) | CaDiCaL::Internal | |
| assignment_level(int lit, Clause *) | CaDiCaL::Internal | inline |
| assume(int) | CaDiCaL::Internal | |
| assume_analyze_literal(int lit) | CaDiCaL::Internal | |
| assume_analyze_reason(int lit, Clause *reason) | CaDiCaL::Internal | |
| assumed(int lit) | CaDiCaL::Internal | inline |
| assumptions | CaDiCaL::Internal | |
| asymmetric_literal_addition(int lit, Coveror &) | CaDiCaL::Internal | inline |
| averages | CaDiCaL::Internal | |
| backtrack(int target_level=0) | CaDiCaL::Internal | |
| backtrack_without_updating_phases(int target_level=0) | CaDiCaL::Internal | |
| backward_false_satisfiable() | CaDiCaL::Internal | |
| backward_true_satisfiable() | CaDiCaL::Internal | |
| best_assigned | CaDiCaL::Internal | |
| best_quotient(Factoring &, size_t *) | CaDiCaL::Internal | |
| better_decision(int lit, int other) | CaDiCaL::Internal | |
| big | CaDiCaL::Internal | |
| bins(int lit) | CaDiCaL::Internal | inline |
| BLOCK enum value | CaDiCaL::Internal | |
| block() | CaDiCaL::Internal | |
| block_candidates(Blocker &, int lit) | CaDiCaL::Internal | |
| block_impossible(Blocker &, int lit) | CaDiCaL::Internal | |
| block_literal(Blocker &, int lit) | CaDiCaL::Internal | |
| block_literal_with_at_least_two_negative_occs(Blocker &, int lit) | CaDiCaL::Internal | |
| block_literal_with_one_negative_occ(Blocker &, int lit) | CaDiCaL::Internal | |
| block_pure_literal(Blocker &, int lit) | CaDiCaL::Internal | |
| block_reschedule(Blocker &, int lit) | CaDiCaL::Internal | |
| block_reschedule_clause(Blocker &, int lit, Clause *) | CaDiCaL::Internal | |
| block_schedule(Blocker &) | CaDiCaL::Internal | |
| blocked_clause(Quotient *q, int) | CaDiCaL::Internal | |
| btab | CaDiCaL::Internal | |
| build_chain_for_empty() | CaDiCaL::Internal | |
| build_chain_for_units(int lit, Clause *reason, bool forced) | CaDiCaL::Internal | |
| build_lrat_for_clause(const vector< vector< Clause * > > &dfs_chains, bool invert=false) | CaDiCaL::Internal | |
| bump_also_all_reason_literals() | CaDiCaL::Internal | inline |
| bump_also_reason_literal(int lit) | CaDiCaL::Internal | inline |
| bump_also_reason_literals(int lit, int depth_limit, size_t size_limit) | CaDiCaL::Internal | inline |
| bump_clause(Clause *) | CaDiCaL::Internal | inline |
| bump_clause2(Clause *) | CaDiCaL::Internal | |
| bump_queue(int idx) | CaDiCaL::Internal | |
| bump_variable(int lit) | CaDiCaL::Internal | |
| bump_variable_score(int lit) | CaDiCaL::Internal | |
| bump_variable_score_inc() | CaDiCaL::Internal | |
| bump_variables() | CaDiCaL::Internal | |
| bumped(int lit) | CaDiCaL::Internal | inline |
| cache_lines(size_t bytes) | CaDiCaL::Internal | inline |
| cache_lines(size_t n, size_t bytes) | CaDiCaL::Internal | inline |
| cadical_kitten_ticks_limit_hit(Sweeper &sweeper, const char *when) | CaDiCaL::Internal | |
| calculate_minimize_chain(int lit, std::vector< int > &stack) | CaDiCaL::Internal | |
| can_sweep_clause(Clause *c) | CaDiCaL::Internal | |
| cdcl_loop_with_inprocessing() | CaDiCaL::Internal | |
| check() | CaDiCaL::Internal | |
| check_clause_stats() | CaDiCaL::Internal | |
| check_var_stats() | CaDiCaL::Internal | |
| check_watched_literal_invariants() | CaDiCaL::Internal | |
| citten | CaDiCaL::Internal | |
| citten2lit(unsigned ulit) | CaDiCaL::Internal | inline |
| citten_clear_track_log_terminate() | CaDiCaL::Internal | |
| clause | CaDiCaL::Internal | |
| clause_contains_fixed_literal(Clause *) | CaDiCaL::Internal | |
| clause_id | CaDiCaL::Internal | |
| clause_variable_ratio() const | CaDiCaL::Internal | inline |
| clauses | CaDiCaL::Internal | |
| clean_probehbr_lrat() | CaDiCaL::Internal | |
| clear_analyzed_levels() | CaDiCaL::Internal | |
| clear_analyzed_literals() | CaDiCaL::Internal | |
| clear_core(Sweeper &sweeper, unsigned core_idx) | CaDiCaL::Internal | |
| clear_flauses(vector< Clause * > &) | CaDiCaL::Internal | |
| clear_minimized_literals() | CaDiCaL::Internal | |
| clear_noccs() | CaDiCaL::Internal | |
| clear_nounted(vector< int > &) | CaDiCaL::Internal | |
| clear_occs() | CaDiCaL::Internal | |
| clear_phases(vector< signed char > &) | CaDiCaL::Internal | |
| clear_sign_marked_literals() | CaDiCaL::Internal | |
| clear_sweeper(Sweeper &sweeper) | CaDiCaL::Internal | |
| clear_unit_analyzed_literals() | CaDiCaL::Internal | |
| clear_watches() | CaDiCaL::Internal | |
| close_trace(bool stats=false) | CaDiCaL::Internal | |
| collect_instantiation_candidates(Instantiator &) | CaDiCaL::Internal | |
| compact() | CaDiCaL::Internal | |
| compacting() | CaDiCaL::Internal | |
| compute_elim_score(unsigned lit) | CaDiCaL::Internal | inline |
| compute_tier_limits(Vivifier &) | CaDiCaL::Internal | |
| conclude_unsat() | CaDiCaL::Internal | |
| concluded | CaDiCaL::Internal | |
| conclusion | CaDiCaL::Internal | |
| CONDITION enum value | CaDiCaL::Internal | |
| condition(bool update_limits=true) | CaDiCaL::Internal | |
| condition_assign(int lit) | CaDiCaL::Internal | |
| condition_round(long unassigned_literal_propagation_limit) | CaDiCaL::Internal | |
| condition_unassign(int lit) | CaDiCaL::Internal | |
| conditioning() | CaDiCaL::Internal | |
| conflict | CaDiCaL::Internal | |
| conflict_id | CaDiCaL::Internal | |
| CONGRUENCE enum value | CaDiCaL::Internal | |
| congruence_delay | CaDiCaL::Internal | |
| connect_binary_watches() | CaDiCaL::Internal | |
| connect_proof_tracer(Tracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Internal | |
| connect_proof_tracer(InternalTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Internal | |
| connect_proof_tracer(StatTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Internal | |
| connect_proof_tracer(FileTracer *tracer, bool antecedents, bool finalize_clauses=false) | CaDiCaL::Internal | |
| connect_propagator() | CaDiCaL::Internal | |
| connect_watches(bool irredundant_only=false) | CaDiCaL::Internal | |
| consider_to_vivify_clause(Clause *candidate) | CaDiCaL::Internal | |
| constrain(int) | CaDiCaL::Internal | |
| constraint | CaDiCaL::Internal | |
| control | CaDiCaL::Internal | |
| copy_clause(Clause *) | CaDiCaL::Internal | |
| copy_non_garbage_clauses() | CaDiCaL::Internal | |
| copy_phases(vector< signed char > &) | CaDiCaL::Internal | |
| COVER enum value | CaDiCaL::Internal | |
| cover() | CaDiCaL::Internal | |
| cover_clause(Clause *c, Coveror &) | CaDiCaL::Internal | |
| cover_propagate_asymmetric(int lit, Clause *ignore, Coveror &) | CaDiCaL::Internal | |
| cover_propagate_covered(int lit, Coveror &) | CaDiCaL::Internal | |
| cover_push_extension(int lit, Coveror &) | CaDiCaL::Internal | inline |
| cover_round() | CaDiCaL::Internal | |
| covered_literal_addition(int lit, Coveror &) | CaDiCaL::Internal | inline |
| deallocate_clause(Clause *) | CaDiCaL::Internal | |
| decide() | CaDiCaL::Internal | |
| decide_phase(int idx, bool target) | CaDiCaL::Internal | |
| DECOMP enum value | CaDiCaL::Internal | |
| decompose() | CaDiCaL::Internal | |
| decompose_analyze_binary_chain(DFS *dfs, int) | CaDiCaL::Internal | |
| decompose_analyze_binary_clauses(DFS *dfs, int from) | CaDiCaL::Internal | |
| decompose_conflicting_scc_lrat(DFS *dfs, vector< int > &) | CaDiCaL::Internal | |
| decompose_round() | CaDiCaL::Internal | |
| DEDUP enum value | CaDiCaL::Internal | |
| delay | CaDiCaL::Internal | |
| delaying_sweep | CaDiCaL::Internal | |
| delaying_vivify_irredundant | CaDiCaL::Internal | |
| delete_clause(Clause *) | CaDiCaL::Internal | |
| delete_garbage_clauses() | CaDiCaL::Internal | |
| delete_sweep_binary(const sweep_binary &sb) | CaDiCaL::Internal | |
| delete_unfactored(Quotient *q) | CaDiCaL::Internal | |
| demote_clause(Clause *) | CaDiCaL::Internal | inline |
| determine_actual_backtrack_level(int jump) | CaDiCaL::Internal | inline |
| did_external_prop | CaDiCaL::Internal | |
| disconnect_proof_tracer(Tracer *tracer) | CaDiCaL::Internal | |
| disconnect_proof_tracer(StatTracer *tracer) | CaDiCaL::Internal | |
| disconnect_proof_tracer(FileTracer *tracer) | CaDiCaL::Internal | |
| dummy_binary | CaDiCaL::Internal | |
| dump(Clause *) | CaDiCaL::Internal | |
| dump() | CaDiCaL::Internal | |
| eagerly_remove_from_occurences(Clause *c) | CaDiCaL::Internal | |
| eagerly_subsume_recently_learned_clauses(Clause *) | CaDiCaL::Internal | |
| ELIM enum value | CaDiCaL::Internal | |
| elim(bool update_limits=true) | CaDiCaL::Internal | |
| elim_add_resolvents(Eliminator &, int pivot) | CaDiCaL::Internal | inline |
| elim_backward_clause(Eliminator &, Clause *) | CaDiCaL::Internal | |
| elim_backward_clauses(Eliminator &) | CaDiCaL::Internal | |
| elim_on_the_fly_self_subsumption(Eliminator &, Clause *, int) | CaDiCaL::Internal | |
| elim_propagate(Eliminator &, int unit) | CaDiCaL::Internal | |
| elim_resolvents_are_bounded(Eliminator &, int pivot) | CaDiCaL::Internal | |
| elim_round(bool &completed, bool &) | CaDiCaL::Internal | |
| elim_update_added_clause(Eliminator &, Clause *) | CaDiCaL::Internal | |
| elim_update_removed_clause(Eliminator &, Clause *, int except=0) | CaDiCaL::Internal | |
| elim_update_removed_lit(Eliminator &, int lit) | CaDiCaL::Internal | |
| elimfast() | CaDiCaL::Internal | |
| elimfast_add_resolvents(Eliminator &, int pivot) | CaDiCaL::Internal | inline |
| elimfast_resolvents_are_bounded(Eliminator &, int pivot) | CaDiCaL::Internal | |
| elimfast_round(bool &completed, bool &) | CaDiCaL::Internal | |
| enlarge(int new_max_var) | CaDiCaL::Internal | |
| enlarge_vals(size_t new_vsize) | CaDiCaL::Internal | |
| error(const char *,...) CADICAL_ATTRIBUTE_FORMAT(2 | CaDiCaL::Internal | |
| error_message | CaDiCaL::Internal | |
| error_message_end() | CaDiCaL::Internal | |
| error_message_start() | CaDiCaL::Internal | |
| explain_external_propagations() | CaDiCaL::Internal | |
| explain_reason(int lit, Clause *, int &open) | CaDiCaL::Internal | |
| ext_clause_forgettable | CaDiCaL::Internal | |
| external | CaDiCaL::Internal | |
| external_check_solution() | CaDiCaL::Internal | |
| external_prop | CaDiCaL::Internal | |
| external_prop_is_lazy | CaDiCaL::Internal | |
| external_propagate() | CaDiCaL::Internal | |
| external_reason | CaDiCaL::Internal | |
| externalize(int lit) | CaDiCaL::Internal | inline |
| extract_gates() | CaDiCaL::Internal | |
| FACTOR enum value | CaDiCaL::Internal | |
| factor() | CaDiCaL::Internal | |
| factor_mode() | CaDiCaL::Internal | |
| factorize_next(Factoring &, int, unsigned) | CaDiCaL::Internal | |
| failed(int lit) | CaDiCaL::Internal | |
| failed_constraint() | CaDiCaL::Internal | |
| failed_literal(int lit) | CaDiCaL::Internal | |
| failing() | CaDiCaL::Internal | |
| file_tracers | CaDiCaL::Internal | |
| finalize(int) | CaDiCaL::Internal | |
| find_and_gate(Eliminator &, int pivot) | CaDiCaL::Internal | |
| find_binary_clause(int, int) | CaDiCaL::Internal | |
| find_clause(const vector< int > &) | CaDiCaL::Internal | |
| find_conflict_level(int &forced) | CaDiCaL::Internal | inline |
| find_definition(Eliminator &, int) | CaDiCaL::Internal | |
| find_equivalence(Eliminator &, int pivot) | CaDiCaL::Internal | |
| find_gate_clauses(Eliminator &, int pivot) | CaDiCaL::Internal | |
| find_if_then_else(Eliminator &, int pivot) | CaDiCaL::Internal | |
| find_ternary_clause(int, int, int) | CaDiCaL::Internal | |
| find_xor_gate(Eliminator &, int pivot) | CaDiCaL::Internal | |
| finish_added_clause_with_id(int64_t id, bool restore=false) | CaDiCaL::Internal | |
| first_factor(Factoring &, int) | CaDiCaL::Internal | |
| fixed(int lit) | CaDiCaL::Internal | inline |
| flags(int lit) | CaDiCaL::Internal | inline |
| flags(int lit) const | CaDiCaL::Internal | inline |
| flip(int lit) | CaDiCaL::Internal | |
| flip_backbone_literals(struct Sweeper &sweeper) | CaDiCaL::Internal | |
| flip_partition_literals(struct Sweeper &sweeper) | CaDiCaL::Internal | |
| flippable(int lit) | CaDiCaL::Internal | |
| flush_all_occs_and_watches() | CaDiCaL::Internal | |
| flush_elimfast_occs(int lit) | CaDiCaL::Internal | |
| flush_occs(int lit) | CaDiCaL::Internal | |
| flush_probes() | CaDiCaL::Internal | |
| flush_trace(bool stats=false) | CaDiCaL::Internal | |
| flush_unmatched_clauses(Quotient *) | CaDiCaL::Internal | |
| flush_vivification_schedule(std::vector< Clause * > &, int64_t &) | CaDiCaL::Internal | |
| flush_watches(int lit, Watches &) | CaDiCaL::Internal | inline |
| flushing() | CaDiCaL::Internal | |
| force_backtrack(size_t new_level) | CaDiCaL::Internal | |
| force_lrat() | CaDiCaL::Internal | |
| force_no_backtrack | CaDiCaL::Internal | |
| force_saved_phase | CaDiCaL::Internal | |
| forced_backt_allowed | CaDiCaL::Internal | |
| forward_false_satisfiable() | CaDiCaL::Internal | |
| forward_true_satisfiable() | CaDiCaL::Internal | |
| frat | CaDiCaL::Internal | |
| freeze(int lit) | CaDiCaL::Internal | inline |
| from_propagator | CaDiCaL::Internal | |
| frozen(int lit) | CaDiCaL::Internal | inline |
| frozentab | CaDiCaL::Internal | |
| ftab | CaDiCaL::Internal | |
| garbage_collection() | CaDiCaL::Internal | |
| generate_cubes(int, int) | CaDiCaL::Internal | |
| generate_probes() | CaDiCaL::Internal | |
| get_clause(Clause *, vector< int > &) | CaDiCaL::Internal | |
| get_new_extension_variable() | CaDiCaL::Internal | |
| get_parent_reason_literal(int lit) | CaDiCaL::Internal | inline |
| get_probehbr_lrat(int lit, int uip) | CaDiCaL::Internal | |
| get_ternary_clause(Clause *, int &, int &, int &) | CaDiCaL::Internal | |
| getbit(int lit, int bit) const | CaDiCaL::Internal | inline |
| getfact(int lit, int fact) const | CaDiCaL::Internal | inline |
| gtab | CaDiCaL::Internal | |
| handle_external_clause(Clause *) | CaDiCaL::Internal | |
| hyper_binary_resolve(Clause *) | CaDiCaL::Internal | inline |
| hyper_ternary_resolve(Clause *, int, Clause *) | CaDiCaL::Internal | |
| i2e | CaDiCaL::Internal | |
| ignore | CaDiCaL::Internal | |
| implied(std::vector< int > &entrailed) | CaDiCaL::Internal | |
| in_mode(Mode m) const | CaDiCaL::Internal | inline |
| inc | CaDiCaL::Internal | |
| incomplete_variables() | CaDiCaL::Internal | |
| increase_elimination_bound() | CaDiCaL::Internal | |
| ineliminating() | CaDiCaL::Internal | |
| init_averages() | CaDiCaL::Internal | |
| init_backbone_and_partition(Sweeper &sweeper) | CaDiCaL::Internal | |
| init_bins() | CaDiCaL::Internal | |
| init_citten() | CaDiCaL::Internal | |
| init_enqueue(int idx) | CaDiCaL::Internal | inline |
| init_noccs() | CaDiCaL::Internal | |
| init_occs() | CaDiCaL::Internal | |
| init_preprocessing_limits() | CaDiCaL::Internal | |
| init_probehbr_lrat() | CaDiCaL::Internal | |
| init_queue(int old_max_var, int new_max_var) | CaDiCaL::Internal | |
| init_report_limits() | CaDiCaL::Internal | |
| init_scores(int old_max_var, int new_max_var) | CaDiCaL::Internal | |
| init_search_limits() | CaDiCaL::Internal | |
| init_sweeper(Sweeper &sweeper) | CaDiCaL::Internal | |
| init_vars(int new_max_var) | CaDiCaL::Internal | |
| init_watches() | CaDiCaL::Internal | |
| inprobe(bool update_limits=true) | CaDiCaL::Internal | |
| inprobing() | CaDiCaL::Internal | |
| inst_assign(int lit) | CaDiCaL::Internal | inline |
| inst_chain | CaDiCaL::Internal | |
| inst_propagate() | CaDiCaL::Internal | |
| instantiate(Instantiator &) | CaDiCaL::Internal | |
| instantiate_candidate(int lit, Clause *) | CaDiCaL::Internal | |
| Internal() | CaDiCaL::Internal | |
| internal | CaDiCaL::Internal | |
| irredundant() const | CaDiCaL::Internal | inline |
| is_autarky_literal(int lit) const | CaDiCaL::Internal | inline |
| is_binary_clause(Clause *c, int &, int &) | CaDiCaL::Internal | |
| is_blocked_clause(Clause *c, int pivot) | CaDiCaL::Internal | |
| is_clause(Clause *, const vector< int > &) | CaDiCaL::Internal | |
| is_conditional_literal(int lit) const | CaDiCaL::Internal | inline |
| is_decision(int ilit) | CaDiCaL::Internal | |
| is_external_forgettable(int64_t id) | CaDiCaL::Internal | |
| is_in_candidate_clause(int lit) const | CaDiCaL::Internal | inline |
| is_valid_limit(const char *name) | CaDiCaL::Internal | static |
| iterate() | CaDiCaL::Internal | |
| iterating | CaDiCaL::Internal | |
| last | CaDiCaL::Internal | |
| learn_empty_clause() | CaDiCaL::Internal | |
| learn_external_reason_clause(int lit, int falsified_elit=0, bool no_backtrack=false) | CaDiCaL::Internal | |
| learn_unit_clause(int lit) | CaDiCaL::Internal | |
| level | CaDiCaL::Internal | |
| levels | CaDiCaL::Internal | |
| likely_phase(int idx) | CaDiCaL::Internal | |
| likely_to_be_kept_clause(Clause *c) | CaDiCaL::Internal | inline |
| lim | CaDiCaL::Internal | |
| limit(const char *name, int) | CaDiCaL::Internal | |
| limit_conflicts(int) | CaDiCaL::Internal | |
| limit_decisions(int) | CaDiCaL::Internal | |
| limit_local_search(int) | CaDiCaL::Internal | |
| limit_preprocessing(int) | CaDiCaL::Internal | |
| limit_terminate(int) | CaDiCaL::Internal | |
| link(int lit) | CaDiCaL::Internal | inline |
| links | CaDiCaL::Internal | |
| lit2citten(int lit) | CaDiCaL::Internal | inline |
| lits | CaDiCaL::Internal | |
| local_search() | CaDiCaL::Internal | |
| local_search_round(int round) | CaDiCaL::Internal | |
| localsearching | CaDiCaL::Internal | |
| lookahead() | CaDiCaL::Internal | |
| lookahead_flush_probes() | CaDiCaL::Internal | |
| lookahead_generate_probes() | CaDiCaL::Internal | |
| lookahead_locc(const std::vector< int > &) | CaDiCaL::Internal | |
| lookahead_next_probe() | CaDiCaL::Internal | |
| lookahead_populate_locc() | CaDiCaL::Internal | |
| lookahead_probing() | CaDiCaL::Internal | |
| lookingahead | CaDiCaL::Internal | |
| lrat | CaDiCaL::Internal | |
| lrat_chain | CaDiCaL::Internal | |
| LUCKY enum value | CaDiCaL::Internal | |
| lucky_phases() | CaDiCaL::Internal | |
| lucky_propagate_discrepency(int) | CaDiCaL::Internal | inline |
| mark(int lit) | CaDiCaL::Internal | inline |
| mark(Clause *) | CaDiCaL::Internal | |
| mark2(int lit) | CaDiCaL::Internal | inline |
| mark2(Clause *) | CaDiCaL::Internal | |
| mark67(int lit) | CaDiCaL::Internal | inline |
| mark_active(int) | CaDiCaL::Internal | |
| mark_added(int lit, int size, bool redundant) | CaDiCaL::Internal | inline |
| mark_added(Clause *) | CaDiCaL::Internal | |
| mark_as_conditional_literal(int lit) | CaDiCaL::Internal | inline |
| mark_binary_literals(Eliminator &, int pivot) | CaDiCaL::Internal | |
| mark_block(int lit) | CaDiCaL::Internal | inline |
| mark_clause() | CaDiCaL::Internal | |
| mark_clauses_to_be_flushed() | CaDiCaL::Internal | |
| mark_decomposed(int lit) | CaDiCaL::Internal | inline |
| mark_duplicated_binary_clauses_as_garbage() | CaDiCaL::Internal | |
| mark_elim(int lit) | CaDiCaL::Internal | inline |
| mark_eliminated(int) | CaDiCaL::Internal | |
| mark_eliminated_clauses_as_garbage(Eliminator &, int pivot, bool &) | CaDiCaL::Internal | |
| mark_factor(int lit) | CaDiCaL::Internal | inline |
| mark_fixed(int) | CaDiCaL::Internal | |
| mark_garbage(Clause *) | CaDiCaL::Internal | |
| mark_garbage_external_forgettable(int64_t id) | CaDiCaL::Internal | |
| mark_in_candidate_clause(int lit) | CaDiCaL::Internal | inline |
| mark_incomplete(Sweeper &sweeper) | CaDiCaL::Internal | |
| mark_pure(int) | CaDiCaL::Internal | |
| mark_redundant_clauses_with_eliminated_variables_as_garbage() | CaDiCaL::Internal | |
| mark_removed(int lit) | CaDiCaL::Internal | inline |
| mark_removed(Clause *, int except=0) | CaDiCaL::Internal | |
| mark_satisfied_clauses_as_garbage() | CaDiCaL::Internal | |
| mark_shrinkable_as_removable(int, std::vector< int >::size_type) | CaDiCaL::Internal | |
| mark_skip(int lit) | CaDiCaL::Internal | inline |
| mark_substituted(int) | CaDiCaL::Internal | |
| mark_subsume(int lit) | CaDiCaL::Internal | inline |
| mark_ternary(int lit) | CaDiCaL::Internal | inline |
| mark_useless_redundant_clauses_as_garbage() | CaDiCaL::Internal | |
| marked(int lit) const | CaDiCaL::Internal | inline |
| marked2(int lit) const | CaDiCaL::Internal | inline |
| marked67(int lit) const | CaDiCaL::Internal | inline |
| marked_block(int lit) const | CaDiCaL::Internal | inline |
| marked_decomposed(int lit) | CaDiCaL::Internal | inline |
| marked_failed | CaDiCaL::Internal | |
| marked_skip(int lit) | CaDiCaL::Internal | inline |
| marked_subsume(int lit) const | CaDiCaL::Internal | inline |
| markfact(int lit, int fact) | CaDiCaL::Internal | inline |
| marks | CaDiCaL::Internal | |
| match_ternary_clause(Clause *, int, int, int) | CaDiCaL::Internal | |
| max_used | CaDiCaL::Internal | |
| max_var | CaDiCaL::Internal | |
| melt(int lit) | CaDiCaL::Internal | inline |
| mini_chain | CaDiCaL::Internal | |
| minimize_and_shrink_block(std::vector< int >::reverse_iterator &, unsigned int &, unsigned int &, const int) | CaDiCaL::Internal | |
| minimize_chain | CaDiCaL::Internal | |
| minimize_clause() | CaDiCaL::Internal | |
| minimize_literal(int lit, int depth=0) | CaDiCaL::Internal | |
| minimize_sort_clause() | CaDiCaL::Internal | |
| minimized | CaDiCaL::Internal | |
| Mode enum name | CaDiCaL::Internal | |
| mode | CaDiCaL::Internal | |
| most_occurring_literal() | CaDiCaL::Internal | |
| move_literals_to_watch() | CaDiCaL::Internal | |
| negative_horn_satisfiable() | CaDiCaL::Internal | |
| new_clause(bool red, int glue=0) | CaDiCaL::Internal | |
| new_clause_as(const Clause *orig) | CaDiCaL::Internal | |
| new_driving_clause(const int glue, int &jump) | CaDiCaL::Internal | |
| new_factor_clause() | CaDiCaL::Internal | |
| new_hyper_binary_resolved_clause(bool red, int glue) | CaDiCaL::Internal | |
| new_hyper_ternary_resolved_clause(bool red) | CaDiCaL::Internal | |
| new_hyper_ternary_resolved_clause_and_watch(bool red, bool) | CaDiCaL::Internal | |
| new_learned_redundant_clause(int glue) | CaDiCaL::Internal | |
| new_proof_on_demand() | CaDiCaL::Internal | |
| new_quotient(Factoring &, int) | CaDiCaL::Internal | |
| new_resolved_irredundant_clause() | CaDiCaL::Internal | |
| new_trail_level(int lit) | CaDiCaL::Internal | |
| newest_clause | CaDiCaL::Internal | |
| next_decision_variable() | CaDiCaL::Internal | |
| next_decision_variable_on_queue() | CaDiCaL::Internal | |
| next_decision_variable_with_best_score() | CaDiCaL::Internal | |
| next_factor(Factoring &, unsigned *) | CaDiCaL::Internal | |
| next_probe() | CaDiCaL::Internal | |
| next_scheduled(Sweeper &sweeper) | CaDiCaL::Internal | |
| no_conflict_until | CaDiCaL::Internal | |
| noccs(int lit) | CaDiCaL::Internal | inline |
| notified | CaDiCaL::Internal | |
| notify_assignments() | CaDiCaL::Internal | |
| notify_backtrack(size_t new_level) | CaDiCaL::Internal | |
| notify_decision() | CaDiCaL::Internal | |
| ntab | CaDiCaL::Internal | |
| num_assigned | CaDiCaL::Internal | |
| observed(int ilit) const | CaDiCaL::Internal | |
| occs(int lit) | CaDiCaL::Internal | inline |
| occurring() const | CaDiCaL::Internal | inline |
| on_the_fly_strengthen(Clause *conflict, int lit) | CaDiCaL::Internal | |
| opts | CaDiCaL::Internal | |
| original | CaDiCaL::Internal | |
| original_id | CaDiCaL::Internal | |
| otab | CaDiCaL::Internal | |
| otfs_find_backtrack_level(int &forced) | CaDiCaL::Internal | inline |
| otfs_strengthen_clause(Clause *, int, int, const std::vector< int > &) | CaDiCaL::Internal | |
| otfs_subsume_clause(Clause *subsuming, Clause *subsumed) | CaDiCaL::Internal | inline |
| parents | CaDiCaL::Internal | |
| parse_dimacs(FILE *) | CaDiCaL::Internal | |
| parse_dimacs(const char *) | CaDiCaL::Internal | |
| parse_solution(const char *) | CaDiCaL::Internal | |
| phase(int lit) | CaDiCaL::Internal | |
| phases | CaDiCaL::Internal | |
| positive_horn_satisfiable() | CaDiCaL::Internal | |
| prefix | CaDiCaL::Internal | |
| preprocess() | CaDiCaL::Internal | |
| preprocess_quickly() | CaDiCaL::Internal | |
| preprocess_round(int round) | CaDiCaL::Internal | |
| preprocessing | CaDiCaL::Internal | |
| print_resource_usage() | CaDiCaL::Internal | |
| print_statistics() | CaDiCaL::Internal | |
| private_steps | CaDiCaL::Internal | |
| PROBE enum value | CaDiCaL::Internal | |
| probe() | CaDiCaL::Internal | |
| probe_assign(int lit, int parent) | CaDiCaL::Internal | inline |
| probe_assign_decision(int lit) | CaDiCaL::Internal | |
| probe_assign_unit(int lit) | CaDiCaL::Internal | |
| probe_dominator(int a, int b) | CaDiCaL::Internal | |
| probe_dominator_lrat(int dom, Clause *reason) | CaDiCaL::Internal | |
| probe_lrat_for_units(int lit) | CaDiCaL::Internal | inline |
| probe_post_dominator_lrat(vector< Clause * > &, int, int) | CaDiCaL::Internal | |
| probe_propagate() | CaDiCaL::Internal | |
| probe_propagate2() | CaDiCaL::Internal | inline |
| probe_reason | CaDiCaL::Internal | |
| probehbr_chains | CaDiCaL::Internal | |
| probes | CaDiCaL::Internal | |
| process_time() const | CaDiCaL::Internal | |
| produce_failed_assumptions() | CaDiCaL::Internal | |
| promote_clause(Clause *, int new_glue) | CaDiCaL::Internal | |
| promote_clause_glue_only(Clause *, int new_glue) | CaDiCaL::Internal | |
| proof | CaDiCaL::Internal | |
| propagate() | CaDiCaL::Internal | |
| propagate_assumptions() | CaDiCaL::Internal | |
| propagate_out_of_order_units() | CaDiCaL::Internal | |
| propagated | CaDiCaL::Internal | |
| propagated2 | CaDiCaL::Internal | |
| propergate() | CaDiCaL::Internal | |
| propergated | CaDiCaL::Internal | |
| propfixed(int lit) | CaDiCaL::Internal | inline |
| protect_reasons() | CaDiCaL::Internal | |
| protected_reasons | CaDiCaL::Internal | |
| ptab | CaDiCaL::Internal | |
| push_literals_of_block(const std::vector< int >::reverse_iterator &, const std::vector< int >::reverse_iterator &, int, unsigned) | CaDiCaL::Internal | |
| queue | CaDiCaL::Internal | |
| reactivate(int lit) | CaDiCaL::Internal | |
| real_time() const | CaDiCaL::Internal | |
| reap | CaDiCaL::Internal | |
| recompute_glue(Clause *) | CaDiCaL::Internal | |
| recompute_tier() | CaDiCaL::Internal | |
| reduce() | CaDiCaL::Internal | |
| reducing() | CaDiCaL::Internal | |
| redundant() const | CaDiCaL::Internal | inline |
| release_quotients(Factoring &) | CaDiCaL::Internal | |
| release_sweeper(Sweeper &sweeper) | CaDiCaL::Internal | |
| relevanttab | CaDiCaL::Internal | |
| reluctant | CaDiCaL::Internal | |
| remove_falsified_literals(Clause *) | CaDiCaL::Internal | |
| remove_garbage_binaries() | CaDiCaL::Internal | |
| remove_observed_var(int ilit) | CaDiCaL::Internal | |
| renotify_full_trail() | CaDiCaL::Internal | |
| renotify_trail_after_ilb() | CaDiCaL::Internal | |
| renotify_trail_after_local_search() | CaDiCaL::Internal | |
| rephase() | CaDiCaL::Internal | |
| rephase_best() | CaDiCaL::Internal | |
| rephase_flipping() | CaDiCaL::Internal | |
| rephase_inverted() | CaDiCaL::Internal | |
| rephase_original() | CaDiCaL::Internal | |
| rephase_random() | CaDiCaL::Internal | |
| rephase_walk() | CaDiCaL::Internal | |
| rephased | CaDiCaL::Internal | |
| rephasing() | CaDiCaL::Internal | |
| report(char type, int verbose_level=0) | CaDiCaL::Internal | |
| report_solving(int) | CaDiCaL::Internal | |
| reported | CaDiCaL::Internal | |
| require_mode(Mode m) const | CaDiCaL::Internal | inline |
| rescale_variable_scores() | CaDiCaL::Internal | |
| reschedule_previously_remaining(Sweeper &sweeper) | CaDiCaL::Internal | |
| reserve_ids(int number) | CaDiCaL::Internal | |
| reserved_ids | CaDiCaL::Internal | |
| reset_assumptions() | CaDiCaL::Internal | |
| reset_bins() | CaDiCaL::Internal | |
| reset_citten() | CaDiCaL::Internal | |
| reset_concluded() | CaDiCaL::Internal | |
| reset_constraint() | CaDiCaL::Internal | |
| reset_factor_mode() | CaDiCaL::Internal | |
| reset_limits() | CaDiCaL::Internal | |
| reset_mode(Mode m) | CaDiCaL::Internal | inline |
| reset_noccs() | CaDiCaL::Internal | |
| reset_occs() | CaDiCaL::Internal | |
| reset_shrinkable() | CaDiCaL::Internal | |
| reset_solving() | CaDiCaL::Internal | |
| reset_subsume_bits() | CaDiCaL::Internal | |
| reset_watches() | CaDiCaL::Internal | |
| resize_factoring(Factoring &factoring, int lit) | CaDiCaL::Internal | |
| resize_unit_clauses_idx() | CaDiCaL::Internal | |
| resolve_clauses(Eliminator &, Clause *, int pivot, Clause *, bool) | CaDiCaL::Internal | |
| restart() | CaDiCaL::Internal | |
| restarting() | CaDiCaL::Internal | |
| restore_clauses() | CaDiCaL::Internal | |
| reuse_trail() | CaDiCaL::Internal | |
| rtab | CaDiCaL::Internal | |
| run_factorization(int64_t limit) | CaDiCaL::Internal | |
| satisfied() | CaDiCaL::Internal | |
| save_add_clear_core(Sweeper &sweeper) | CaDiCaL::Internal | |
| save_core(Sweeper &sweeper, unsigned core) | CaDiCaL::Internal | |
| saved_decisions | CaDiCaL::Internal | |
| scale(double v) const | CaDiCaL::Internal | |
| scheduable_variable(Sweeper &sweeper, int idx, size_t *occ_ptr) | CaDiCaL::Internal | |
| schedule_all_other_not_scheduled_yet(Sweeper &sweeper) | CaDiCaL::Internal | |
| schedule_factorization(Factoring &) | CaDiCaL::Internal | |
| schedule_inner(Sweeper &sweeper, int idx) | CaDiCaL::Internal | |
| schedule_outer(Sweeper &sweeper, int idx) | CaDiCaL::Internal | |
| schedule_sweeping(Sweeper &sweeper) | CaDiCaL::Internal | |
| scheduled_variable(Sweeper &sweeper, int idx) | CaDiCaL::Internal | |
| score(int lit) | CaDiCaL::Internal | inline |
| score_inc | CaDiCaL::Internal | |
| scores | CaDiCaL::Internal | |
| SEARCH enum value | CaDiCaL::Internal | |
| search_assign(int lit, Clause *) | CaDiCaL::Internal | inline |
| search_assign_driving(int lit, Clause *reason) | CaDiCaL::Internal | |
| search_assign_external(int lit) | CaDiCaL::Internal | |
| search_assume_decision(int decision) | CaDiCaL::Internal | |
| search_limits_hit() | CaDiCaL::Internal | inline |
| searching_lucky_phases | CaDiCaL::Internal | |
| second_literal_in_binary_clause(Eliminator &, Clause *, int first) | CaDiCaL::Internal | |
| second_literal_in_binary_clause_lrat(Clause *, int first) | CaDiCaL::Internal | |
| self_subsuming_factor(Quotient *) | CaDiCaL::Internal | |
| set_mode(Mode m) | CaDiCaL::Internal | inline |
| set_parent_reason_literal(int lit, int reason) | CaDiCaL::Internal | inline |
| set_probehbr_lrat(int lit, int uip) | CaDiCaL::Internal | |
| set_tainted_literal() | CaDiCaL::Internal | |
| set_val(int lit, signed char val) | CaDiCaL::Internal | inline |
| setbit(int lit, int bit) | CaDiCaL::Internal | inline |
| shrink_along_reason(int, int, bool, bool &, unsigned) | CaDiCaL::Internal | inline |
| shrink_and_minimize_clause() | CaDiCaL::Internal | |
| shrink_block(std::vector< int >::reverse_iterator &, std::vector< int >::reverse_iterator &, int, unsigned &, unsigned &, const int, unsigned) | CaDiCaL::Internal | |
| shrink_clause(Clause *, int new_size) | CaDiCaL::Internal | |
| shrink_literal(int, int, unsigned) | CaDiCaL::Internal | inline |
| shrink_next(int, unsigned &, unsigned &) | CaDiCaL::Internal | inline |
| shrinkable | CaDiCaL::Internal | |
| shrunken_block_no_uip(const std::vector< int >::reverse_iterator &, const std::vector< int >::reverse_iterator &, unsigned &, const int) | CaDiCaL::Internal | inline |
| shrunken_block_uip(int, int, std::vector< int >::reverse_iterator &, std::vector< int >::reverse_iterator &, std::vector< int >::size_type, const int) | CaDiCaL::Internal | |
| shuffle_queue() | CaDiCaL::Internal | |
| shuffle_scores() | CaDiCaL::Internal | |
| sign_marked | CaDiCaL::Internal | |
| SIMPLIFY enum value | CaDiCaL::Internal | |
| solve(bool preprocess_only=false) | CaDiCaL::Internal | |
| solve_time() | CaDiCaL::Internal | |
| sort_and_reuse_assumptions() | CaDiCaL::Internal | |
| sort_watches() | CaDiCaL::Internal | |
| stab | CaDiCaL::Internal | |
| stabilizing() | CaDiCaL::Internal | |
| stable | CaDiCaL::Internal | |
| stat_tracers | CaDiCaL::Internal | |
| stats | CaDiCaL::Internal | |
| strengthen_clause(Clause *, int) | CaDiCaL::Internal | |
| substitute_connected_clauses(Sweeper &sweeper, int lit, int other, int64_t id) | CaDiCaL::Internal | |
| SUBSUME enum value | CaDiCaL::Internal | |
| subsume() | CaDiCaL::Internal | |
| subsume_check(Clause *subsuming, Clause *subsumed) | CaDiCaL::Internal | inline |
| subsume_clause(Clause *subsuming, Clause *subsumed) | CaDiCaL::Internal | inline |
| subsume_round() | CaDiCaL::Internal | |
| swap_averages() | CaDiCaL::Internal | |
| SWEEP enum value | CaDiCaL::Internal | |
| sweep() | CaDiCaL::Internal | |
| sweep_add_clause(Sweeper &sweeper, unsigned depth) | CaDiCaL::Internal | |
| sweep_backbone_candidate(Sweeper &sweeper, int lit) | CaDiCaL::Internal | |
| sweep_clause(Sweeper &sweeper, unsigned depth, Clause *) | CaDiCaL::Internal | |
| sweep_dense_mode_and_watch_irredundant() | CaDiCaL::Internal | |
| sweep_dense_propagate(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_empty_clause(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_equivalence_candidates(Sweeper &sweeper, int lit, int other) | CaDiCaL::Internal | |
| sweep_extract_fixed(Sweeper &sweeper, int lit) | CaDiCaL::Internal | |
| sweep_flip(int) | CaDiCaL::Internal | |
| sweep_flip_and_implicant(int) | CaDiCaL::Internal | |
| sweep_incomplete | CaDiCaL::Internal | |
| sweep_refine(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_refine_backbone(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_refine_partition(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_remove(Sweeper &sweeper, int lit) | CaDiCaL::Internal | |
| sweep_repr(Sweeper &sweeper, int lit) | CaDiCaL::Internal | |
| sweep_schedule | CaDiCaL::Internal | |
| sweep_set_cadical_kitten_ticks_limit(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_solve() | CaDiCaL::Internal | |
| sweep_sparse_mode() | CaDiCaL::Internal | |
| sweep_substitute_lrat(Clause *c, int64_t id) | CaDiCaL::Internal | |
| sweep_substitute_new_equivalences(Sweeper &sweeper) | CaDiCaL::Internal | |
| sweep_update_noccs(Clause *c) | CaDiCaL::Internal | |
| sweep_variable(Sweeper &sweeper, int idx) | CaDiCaL::Internal | |
| tainted_literal | CaDiCaL::Internal | |
| target_assigned | CaDiCaL::Internal | |
| terminate() | CaDiCaL::Internal | inline |
| terminated_asynchronously(int factor=1) | CaDiCaL::Internal | inline |
| terminating_asked() | CaDiCaL::Internal | |
| termination_forced | CaDiCaL::Internal | |
| TERNARY enum value | CaDiCaL::Internal | |
| ternary() | CaDiCaL::Internal | |
| ternary_find_binary_clause(int, int) | CaDiCaL::Internal | |
| ternary_find_ternary_clause(int, int, int) | CaDiCaL::Internal | |
| ternary_idx(int idx, int64_t &steps, int64_t &htrs) | CaDiCaL::Internal | |
| ternary_lit(int pivot, int64_t &steps, int64_t &htrs) | CaDiCaL::Internal | |
| ternary_round(int64_t &steps, int64_t &htrs) | CaDiCaL::Internal | |
| tied_next_factor_score(int) | CaDiCaL::Internal | |
| tier1 | CaDiCaL::Internal | |
| tier2 | CaDiCaL::Internal | |
| time() | CaDiCaL::Internal | inline |
| trace(File *) | CaDiCaL::Internal | |
| tracers | CaDiCaL::Internal | |
| trail | CaDiCaL::Internal | |
| TRANSRED enum value | CaDiCaL::Internal | |
| transred() | CaDiCaL::Internal | |
| traverse_clauses(ClauseIterator &) | CaDiCaL::Internal | |
| traverse_constraint(ClauseIterator &) | CaDiCaL::Internal | |
| trivially_false_satisfiable() | CaDiCaL::Internal | |
| trivially_true_satisfiable() | CaDiCaL::Internal | |
| try_to_eliminate_variable(Eliminator &, int pivot, bool &) | CaDiCaL::Internal | |
| try_to_fasteliminate_variable(Eliminator &, int pivot, bool &) | CaDiCaL::Internal | |
| try_to_satisfy_formula_by_saved_phases() | CaDiCaL::Internal | |
| try_to_subsume_clause(Clause *, vector< Clause * > &shrunken) | CaDiCaL::Internal | inline |
| u2i(unsigned u) | CaDiCaL::Internal | inline |
| unassign(int lit) | CaDiCaL::Internal | inline |
| unit_analyzed | CaDiCaL::Internal | |
| unit_chain | CaDiCaL::Internal | |
| unit_clauses(int uidx) | CaDiCaL::Internal | inline |
| unit_clauses_idx | CaDiCaL::Internal | |
| unit_id(int lit) const | CaDiCaL::Internal | inline |
| unlucky(int res) | CaDiCaL::Internal | |
| unmark(int lit) | CaDiCaL::Internal | inline |
| unmark(vector< int > &lits) | CaDiCaL::Internal | inline |
| unmark(Clause *) | CaDiCaL::Internal | |
| unmark67(int lit) | CaDiCaL::Internal | inline |
| unmark_as_conditional_literal(int lit) | CaDiCaL::Internal | inline |
| unmark_binary_literals(Eliminator &) | CaDiCaL::Internal | |
| unmark_block(int lit) | CaDiCaL::Internal | inline |
| unmark_clause() | CaDiCaL::Internal | |
| unmark_decomposed(int lit) | CaDiCaL::Internal | inline |
| unmark_gate_clauses(Eliminator &) | CaDiCaL::Internal | |
| unmark_in_candidate_clause(int lit) | CaDiCaL::Internal | inline |
| unmarkfact(int lit, int fact) | CaDiCaL::Internal | inline |
| unphase(int lit) | CaDiCaL::Internal | |
| unprotect_reasons() | CaDiCaL::Internal | |
| unsat | CaDiCaL::Internal | |
| unsat_constraint | CaDiCaL::Internal | |
| unschedule_sweeping(Sweeper &sweeper, unsigned swept, unsigned scheduled) | CaDiCaL::Internal | |
| unsetbit(int lit, int bit) | CaDiCaL::Internal | inline |
| unwatch_clause(Clause *c) | CaDiCaL::Internal | inline |
| update_decision_rate_average() | CaDiCaL::Internal | |
| update_factor_candidate(Factoring &, int) | CaDiCaL::Internal | |
| update_factored(Factoring &factoring, Quotient *q) | CaDiCaL::Internal | |
| update_queue_unassigned(int idx) | CaDiCaL::Internal | inline |
| update_reason_references() | CaDiCaL::Internal | |
| update_target_and_best() | CaDiCaL::Internal | |
| use_scores() const | CaDiCaL::Internal | inline |
| val(int lit) const | CaDiCaL::Internal | inline |
| vals | CaDiCaL::Internal | |
| var(int lit) | CaDiCaL::Internal | inline |
| vars | CaDiCaL::Internal | |
| verror(const char *, va_list &) | CaDiCaL::Internal | |
| vidx(int lit) const | CaDiCaL::Internal | inline |
| VIVIFY enum value | CaDiCaL::Internal | |
| vivify() | CaDiCaL::Internal | |
| vivify_analyze(Clause *start, bool &, Clause **, const Clause *const, int implied, bool &) | CaDiCaL::Internal | |
| vivify_analyze_redundant(Vivifier &, Clause *start, bool &) | CaDiCaL::Internal | |
| vivify_assign(int lit, Clause *) | CaDiCaL::Internal | inline |
| vivify_assume(int lit) | CaDiCaL::Internal | |
| vivify_build_lrat(int, Clause *, std::vector< std::tuple< int, Clause *, bool > > &) | CaDiCaL::Internal | |
| vivify_chain_for_units(int lit, Clause *reason) | CaDiCaL::Internal | inline |
| vivify_clause(Vivifier &, Clause *candidate) | CaDiCaL::Internal | |
| vivify_deduce(Clause *candidate, Clause *conflct, int implied, Clause **, bool &) | CaDiCaL::Internal | |
| vivify_increment_stats(const Vivifier &vivifier) | CaDiCaL::Internal | inline |
| vivify_initialize(Vivifier &vivifier, int64_t &ticks) | CaDiCaL::Internal | |
| vivify_instantiate(const std::vector< int > &, Clause *, std::vector< std::tuple< int, Clause *, bool > > &lrat_stack, int64_t &ticks) | CaDiCaL::Internal | |
| vivify_prioritize_leftovers(char, size_t prioritized, std::vector< Clause * > &schedule) | CaDiCaL::Internal | inline |
| vivify_propagate(int64_t &) | CaDiCaL::Internal | |
| vivify_round(Vivifier &, int64_t delta) | CaDiCaL::Internal | |
| vivify_shrinkable(const std::vector< int > &sorted, Clause *c) | CaDiCaL::Internal | |
| vivify_sort_watched(Clause *c) | CaDiCaL::Internal | |
| vivify_strengthen(Clause *candidate) | CaDiCaL::Internal | |
| vivify_subsume_clause(Clause *subsuming, Clause *subsumed) | CaDiCaL::Internal | inline |
| vlit(int lit) const | CaDiCaL::Internal | inline |
| vsize | CaDiCaL::Internal | |
| vtab | CaDiCaL::Internal | |
| WALK enum value | CaDiCaL::Internal | |
| walk() | CaDiCaL::Internal | |
| walk_break_value(int lit) | CaDiCaL::Internal | |
| walk_flip_lit(Walker &, int lit) | CaDiCaL::Internal | |
| walk_pick_clause(Walker &) | CaDiCaL::Internal | |
| walk_pick_lit(Walker &, Clause *) | CaDiCaL::Internal | |
| walk_round(int64_t limit, bool prev) | CaDiCaL::Internal | |
| walk_save_minimum(Walker &) | CaDiCaL::Internal | inline |
| warning(const char *,...) CADICAL_ATTRIBUTE_FORMAT(2 | CaDiCaL::Internal | |
| watch_clause(Clause *c) | CaDiCaL::Internal | inline |
| watch_literal(int lit, int blit, Clause *c) | CaDiCaL::Internal | inline |
| watches(int lit) | CaDiCaL::Internal | inline |
| watching() const | CaDiCaL::Internal | inline |
| wrapped_learn_external_reason_clause(int lit) | CaDiCaL::Internal | |
| wtab | CaDiCaL::Internal | |
| ~Internal() | CaDiCaL::Internal | |
