clbbbb/lrat-check/cmd/main

README
- ::active_change_countAuditSnapshot::active_change_count
- ::active_containsAuditSnapshot::active_contains
- ::active_contains_allAuditSnapshot::active_contains_all
- ::active_countAuditSnapshot::active_count
- ::active_densityAuditSnapshot::active_density
- ::active_differenceAuditSnapshot::active_difference
- ::active_id_atAuditSnapshot::active_id_at
- ::active_id_checksumAuditSnapshot::active_id_checksum
- ::active_id_sumAuditSnapshot::active_id_sum
- ::active_idsAuditSnapshot::active_ids
- ::active_intersectionAuditSnapshot::active_intersection
- ::active_rangeAuditSnapshot::active_range
- ::added_clause_idsAuditSnapshot::added_clause_ids
- ::added_empty_clauseAuditSnapshot::added_empty_clause
- ::added_sinceAuditSnapshot::added_since
- ::addition_countAuditSnapshot::addition_count
- ::all_references_resolvedAuditSnapshot::all_references_resolved
- ::completion_ratioAuditSnapshot::completion_ratio
- ::deleted_clause_idsAuditSnapshot::deleted_clause_ids
- ::deleted_countAuditSnapshot::deleted_count
- ::deleted_reference_idsAuditSnapshot::deleted_reference_ids
- ::deleted_sinceAuditSnapshot::deleted_since
- ::empty_clause_was_addedAuditSnapshot::empty_clause_was_added
- ::empty_countAuditSnapshot::empty_count
- ::empty_id_atAuditSnapshot::empty_id_at
- ::empty_id_checksumAuditSnapshot::empty_id_checksum
- ::empty_id_sumAuditSnapshot::empty_id_sum
- ::empty_idsAuditSnapshot::empty_ids
- ::empty_ratioAuditSnapshot::empty_ratio
- ::fingerprintAuditSnapshot::fingerprint
- ::first_deleted_referenceAuditSnapshot::first_deleted_reference
- ::first_missingAuditSnapshot::first_missing
- ::has_active_clauseAuditSnapshot::has_active_clause
- ::has_any_activityAuditSnapshot::has_any_activity
- ::has_clause_lifetimesAuditSnapshot::has_clause_lifetimes
- ::has_deleted_referencesAuditSnapshot::has_deleted_references
- ::has_empty_clauseAuditSnapshot::has_empty_clause
- ::has_live_empty_clauseAuditSnapshot::has_live_empty_clause
- ::has_live_empty_clause_idAuditSnapshot::has_live_empty_clause_id
- ::has_missing_referencesAuditSnapshot::has_missing_references
- ::has_progressAuditSnapshot::has_progress
- ::has_reference_error_onAuditSnapshot::has_reference_error_on
- ::has_reference_errorsAuditSnapshot::has_reference_errors
- ::has_seen_idAuditSnapshot::has_seen_id
- ::is_after_endAuditSnapshot::is_after_end
- ::is_before_startAuditSnapshot::is_before_start
- ::is_completeAuditSnapshot::is_complete
- ::is_consistentAuditSnapshot::is_consistent
- ::is_empty_stateAuditSnapshot::is_empty_state
- ::is_prefix_ofAuditSnapshot::is_prefix_of
- ::is_structurally_cleanAuditSnapshot::is_structurally_clean
- ::is_terminalAuditSnapshot::is_terminal
- ::is_valid_limitAuditSnapshot::is_valid_limit
- ::last_idAuditSnapshot::last_id
- ::line_spanAuditSnapshot::line_span
- ::live_empty_countAuditSnapshot::live_empty_count
- ::live_empty_idsAuditSnapshot::live_empty_ids
- ::maximum_active_idAuditSnapshot::maximum_active_id
- ::minimum_active_idAuditSnapshot::minimum_active_id
- ::missing_idsAuditSnapshot::missing_ids
- ::processed_countAuditSnapshot::processed_count
- ::progress_textAuditSnapshot::progress_text
- ::reference_atAuditSnapshot::reference_at
- ::reference_error_countAuditSnapshot::reference_error_count
- ::reference_linesAuditSnapshot::reference_lines
- ::reference_ratioAuditSnapshot::reference_ratio
- ::reference_summaryAuditSnapshot::reference_summary
- ::references_on_lineAuditSnapshot::references_on_line
- ::same_active_stateAuditSnapshot::same_active_state
- ::same_empty_stateAuditSnapshot::same_empty_state
- ::state_labelAuditSnapshot::state_label
- ::step_kind_countAuditSnapshot::step_kind_count
- ::summaryAuditSnapshot::summary
T
CheckError
- ::defaultCheckLimits::default
T
CheckStats
- ::is_activeClauseLifetime::is_active
- ::is_unusedClauseLifetime::is_unused
- ::lifetime_stepsClauseLifetime::lifetime_steps
- ::was_referencedClauseLifetime::was_referenced
T
ConversionOptions
T
ConversionResult
T
DependencyEdge
- ::edge_countDependencyGraph::edge_count
- ::has_edgeDependencyGraph::has_edge
- ::incomingDependencyGraph::incoming
- ::leavesDependencyGraph::leaves
- ::negative_edge_countDependencyGraph::negative_edge_count
- ::node_countDependencyGraph::node_count
- ::outgoingDependencyGraph::outgoing
- ::rootsDependencyGraph::roots
T
Diagnostic
T
DiagnosticKind
T
DratStep
- ::clause_countFormula::clause_count
- ::clause_size_histogramFormula::clause_size_histogram
- ::contains_empty_clauseFormula::contains_empty_clause
- ::literal_occurrencesFormula::literal_occurrences
- ::validateFormula::validate
- ::variable_countFormula::variable_count
- ::variablesFormula::variables
T
FormulaMetrics
- ::active_clause_idsLifetimeReport::active_clause_ids
- ::clauseLifetimeReport::clause
- ::deleted_clause_idsLifetimeReport::deleted_clause_ids
- ::maximum_lifetime_stepsLifetimeReport::maximum_lifetime_steps
- ::maximum_usesLifetimeReport::maximum_uses
- ::mean_lifetime_stepsLifetimeReport::mean_lifetime_steps
- ::mean_uses_per_clauseLifetimeReport::mean_uses_per_clause
- ::mean_uses_per_used_clauseLifetimeReport::mean_uses_per_used_clause
- ::most_used_clauseLifetimeReport::most_used_clause
- ::never_used_active_idsLifetimeReport::never_used_active_ids
- ::summaryLifetimeReport::summary
- ::unused_clause_idsLifetimeReport::unused_clause_ids
- ::used_clause_countLifetimeReport::used_clause_count
T
LimitViolation
- ::clauseLiteralIndex::clause
- ::contains_idLiteralIndex::contains_id
- ::ids_forLiteralIndex::ids_for
- ::insertLiteralIndex::insert
- ::literal_countLiteralIndex::literal_count
- ::newLiteralIndex::new
- ::removeLiteralIndex::remove
- ::sizeLiteralIndex::size
- ::validateLiteralIndex::validate
T
LiteralState
- ::diagnostic_countPreflightReport::diagnostic_count
- ::is_okPreflightReport::is_ok
- ::summaryPreflightReport::summary
T
ProofFormat
T
ProofMetrics
- ::active_clausesProofSession::active_clauses
- ::active_countProofSession::active_count
- ::active_idsProofSession::active_ids
- ::active_literal_countProofSession::active_literal_count
- ::active_tautology_countProofSession::active_tautology_count
- ::add_clauseProofSession::add_clause
- ::add_clause_with_idProofSession::add_clause_with_id
- ::addition_countProofSession::addition_count
- ::contains_empty_clauseProofSession::contains_empty_clause
- ::delete_clauseProofSession::delete_clause
- ::deletion_countProofSession::deletion_count
- ::from_formulaProofSession::from_formula
- ::get_clauseProofSession::get_clause
- ::has_clauseProofSession::has_clause
- ::ids_for_literalProofSession::ids_for_literal
- ::index_is_consistentProofSession::index_is_consistent
- ::next_idProofSession::next_id
- ::reset_countersProofSession::reset_counters
- ::snapshotProofSession::snapshot
- ::variable_countProofSession::variable_count
- ::clause_literal_countProofSlice::clause_literal_count
- ::contains_emptyProofSlice::contains_empty
- ::dependency_graphProofSlice::dependency_graph
- ::empty_step_countProofSlice::empty_step_count
- ::find_idProofSlice::find_id
- ::first_idProofSlice::first_id
- ::hint_countProofSlice::hint_count
- ::is_emptyProofSlice::is_empty
- ::last_idProofSlice::last_id
- ::lengthProofSlice::length
- ::metricsProofSlice::metrics
- ::rat_step_countProofSlice::rat_step_count
- ::renderProofSlice::render
- ::with_limitProofSlice::with_limit
T
ProofStep
T
ProofSummary
T
ReplayError
- ::active_countReplayResult::active_count
- ::is_unsat_certificateReplayResult::is_unsat_certificate
V
added_clause_ids
V
all_resolvents
V
analyze_clause_lifetimes
V
apply_assignment
V
assign_literal
V
audit_all
V
audit_at_line
V
audit_prefix
V
build_dependency_graph
V
check_limits
V
clause_contains_literal
V
clause_equal
V
clause_is_tautology
V
clause_state
V
clause_subset
V
clause_subsumed
V
clause_variables
V
combine_preflight_reports
V
convert_drat
V
convert_drat_steps
V
convert_proof
V
default_conversion_options
V
deleted_clause_ids
V
dependency_depth
V
dependency_summary
V
diagnose_proof
V
diagnostic_kind_name
V
diagnostic_summary
V
diagnostics_have_errors
V
encode_binary_drat
V
encode_binary_lrat
V
formula_clause_ids
V
formula_contains_clause
V
formula_density
V
formula_has_unit_conflict
V
formula_is_simplified
V
formula_is_trivial
V
formula_max_clause_size
V
formula_min_clause_size
V
formula_resolvents
V
formula_state
V
formula_tautology_count
V
formula_unit_count
V
formula_unit_literals
V
index_clause_count
V
index_literal_count
V
is_hint_free
V
limit_violation_name
V
literal_state
V
measure_formula
V
measure_proof
V
normalize_clause
V
normalize_formula
V
parse_binary_drat
V
parse_binary_lrat
V
parse_cnf
V
parse_drat
V
parse_format
V
parse_proof
V
preflight_default
V
preflight_proof
V
process_proof
V
proof_additions
V
proof_clause_density
V
proof_deletions
V
proof_has_duplicate_addition_ids
V
proof_has_empty_addition
V
proof_has_forward_reference
V
proof_hint_density
V
proof_is_minimal_shape
V
proof_is_well_formed
V
proof_max_id
V
proof_metrics_summary
V
proof_reference_ratio
V
propagate_units
V
rat_candidates
V
referenced_clause_ids
V
remove_duplicate_clauses
V
remove_subsumed_clauses
V
render_clause
V
render_dimacs
V
render_drat
V
render_proof
V
replay
V
replay_error_name
V
replay_structure
V
resolve_clauses
V
simplify_formula
V
slice_proof
V
slices_have_contiguous_ranges
V
split_proof
V
summarize_proof
V
total_slice_steps
V
unit_literal
V
unit_simplify
V
verify
V
verify_formula
V
verify_input
V
verify_steps