🥮 mooncakes.io

    lrat-check

    MoonBit DRAT/LRAT verification and checked certificate conversion

    sat
    drat
    lrat
    proof
    verification
    binary
    Download zip
    Author
    Version
    0.2.0
    License
    Apache-2.0
    Repository
    Last updated
    15 days ago
    Downloads
    32

    #clbbbb/lrat-check

    AuditSnapshot

    source
    pub(all) struct AuditSnapshot {
      processed_steps : Int
      additions : Int
      deletions : Int
      active_clause_ids : Array[Int]
      seen_clause_ids : Array[Int]
      empty_clause_ids : Array[Int]
      missing_references : Array[(Int, Int)]
      deleted_references : Array[(Int, Int)]
      last_step_id : Int
    }

    An audit snapshot describes the proof state after a prefix of parsed proof steps. It is structural: it does not claim that the hints prove each step.

    AuditSnapshot::active_change_count

    source
    fn AuditSnapshot::active_change_count(self : AuditSnapshot, earlier : AuditSnapshot) -> Int

    AuditSnapshot::active_contains

    source
    fn AuditSnapshot::active_contains(self : AuditSnapshot, id : Int) -> Bool

    AuditSnapshot::active_contains_all

    source
    fn AuditSnapshot::active_contains_all(self : AuditSnapshot, ids : Array[Int]) -> Bool

    AuditSnapshot::active_count

    source
    fn AuditSnapshot::active_count(self : AuditSnapshot) -> Int

    AuditSnapshot::active_density

    source
    fn AuditSnapshot::active_density(self : AuditSnapshot) -> Int

    AuditSnapshot::active_difference

    source
    fn AuditSnapshot::active_difference(self : AuditSnapshot, ids : Array[Int]) -> Array[Int]

    AuditSnapshot::active_id_at

    source
    fn AuditSnapshot::active_id_at(self : AuditSnapshot, position : Int) -> Int?

    AuditSnapshot::active_id_checksum

    source
    fn AuditSnapshot::active_id_checksum(self : AuditSnapshot) -> Int

    AuditSnapshot::active_id_sum

    source
    fn AuditSnapshot::active_id_sum(self : AuditSnapshot) -> Int

    AuditSnapshot::active_ids

    source
    fn AuditSnapshot::active_ids(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::active_intersection

    source
    fn AuditSnapshot::active_intersection(self : AuditSnapshot, ids : Array[Int]) -> Array[Int]

    AuditSnapshot::active_range

    source
    fn AuditSnapshot::active_range(self : AuditSnapshot) -> (Int, Int)?

    AuditSnapshot::added_clause_ids

    source
    fn AuditSnapshot::added_clause_ids(self : AuditSnapshot, steps : Array[ProofStep]) -> Array[Int]

    AuditSnapshot::added_empty_clause

    source
    fn AuditSnapshot::added_empty_clause(self : AuditSnapshot, id : Int) -> Bool

    AuditSnapshot::added_since

    source
    fn AuditSnapshot::added_since(self : AuditSnapshot, earlier : AuditSnapshot) -> Int

    AuditSnapshot::addition_count

    source
    fn AuditSnapshot::addition_count(self : AuditSnapshot) -> Int

    AuditSnapshot::all_references_resolved

    source
    fn AuditSnapshot::all_references_resolved(self : AuditSnapshot) -> Bool

    AuditSnapshot::completion_ratio

    source
    fn AuditSnapshot::completion_ratio(self : AuditSnapshot, total : Int) -> Int

    AuditSnapshot::deleted_clause_ids

    source
    fn AuditSnapshot::deleted_clause_ids(self : AuditSnapshot, steps : Array[ProofStep]) -> Array[Int]

    AuditSnapshot::deleted_count

    source
    fn AuditSnapshot::deleted_count(self : AuditSnapshot) -> Int

    AuditSnapshot::deleted_reference_ids

    source
    fn AuditSnapshot::deleted_reference_ids(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::deleted_since

    source
    fn AuditSnapshot::deleted_since(self : AuditSnapshot, earlier : AuditSnapshot) -> Int

    AuditSnapshot::empty_clause_was_added

    source
    fn AuditSnapshot::empty_clause_was_added(self : AuditSnapshot) -> Bool

    AuditSnapshot::empty_count

    source
    fn AuditSnapshot::empty_count(self : AuditSnapshot) -> Int

    AuditSnapshot::empty_id_at

    source
    fn AuditSnapshot::empty_id_at(self : AuditSnapshot, position : Int) -> Int?

    AuditSnapshot::empty_id_checksum

    source
    fn AuditSnapshot::empty_id_checksum(self : AuditSnapshot) -> Int

    AuditSnapshot::empty_id_sum

    source
    fn AuditSnapshot::empty_id_sum(self : AuditSnapshot) -> Int

    AuditSnapshot::empty_ids

    source
    fn AuditSnapshot::empty_ids(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::empty_ratio

    source
    fn AuditSnapshot::empty_ratio(self : AuditSnapshot) -> Int

    AuditSnapshot::fingerprint

    source
    fn AuditSnapshot::fingerprint(self : AuditSnapshot) -> String

    AuditSnapshot::first_deleted_reference

    source
    fn AuditSnapshot::first_deleted_reference(self : AuditSnapshot) -> (Int, Int)?

    AuditSnapshot::first_missing

    source
    fn AuditSnapshot::first_missing(self : AuditSnapshot) -> (Int, Int)?

    AuditSnapshot::has_active_clause

    source
    fn AuditSnapshot::has_active_clause(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_any_activity

    source
    fn AuditSnapshot::has_any_activity(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_clause_lifetimes

    source
    fn AuditSnapshot::has_clause_lifetimes(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_deleted_references

    source
    fn AuditSnapshot::has_deleted_references(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_empty_clause

    source
    fn AuditSnapshot::has_empty_clause(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_live_empty_clause

    source
    fn AuditSnapshot::has_live_empty_clause(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_live_empty_clause_id

    source
    fn AuditSnapshot::has_live_empty_clause_id(self : AuditSnapshot, id : Int) -> Bool

    AuditSnapshot::has_missing_references

    source
    fn AuditSnapshot::has_missing_references(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_progress

    source
    fn AuditSnapshot::has_progress(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_reference_error_on

    source
    fn AuditSnapshot::has_reference_error_on(self : AuditSnapshot, line : Int) -> Bool

    AuditSnapshot::has_reference_errors

    source
    fn AuditSnapshot::has_reference_errors(self : AuditSnapshot) -> Bool

    AuditSnapshot::has_seen_id

    source
    fn AuditSnapshot::has_seen_id(self : AuditSnapshot, id : Int) -> Bool

    AuditSnapshot::is_after_end

    source
    fn AuditSnapshot::is_after_end(self : AuditSnapshot, total : Int) -> Bool

    AuditSnapshot::is_before_start

    source
    fn AuditSnapshot::is_before_start(self : AuditSnapshot) -> Bool

    AuditSnapshot::is_complete

    source
    fn AuditSnapshot::is_complete(self : AuditSnapshot, steps : Array[ProofStep]) -> Bool

    AuditSnapshot::is_consistent

    source
    fn AuditSnapshot::is_consistent(self : AuditSnapshot) -> Bool

    AuditSnapshot::is_empty_state

    source
    fn AuditSnapshot::is_empty_state(self : AuditSnapshot) -> Bool

    AuditSnapshot::is_prefix_of

    source
    fn AuditSnapshot::is_prefix_of(self : AuditSnapshot, other : AuditSnapshot) -> Bool

    AuditSnapshot::is_structurally_clean

    source
    fn AuditSnapshot::is_structurally_clean(self : AuditSnapshot) -> Bool

    AuditSnapshot::is_terminal

    source
    fn AuditSnapshot::is_terminal(self : AuditSnapshot, total : Int) -> Bool

    AuditSnapshot::is_valid_limit

    source
    fn AuditSnapshot::is_valid_limit(self : AuditSnapshot, total : Int) -> Bool

    AuditSnapshot::last_id

    source
    fn AuditSnapshot::last_id(self : AuditSnapshot) -> Int

    AuditSnapshot::line_span

    source
    fn AuditSnapshot::line_span(self : AuditSnapshot) -> (Int, Int)?

    AuditSnapshot::live_empty_count

    source
    fn AuditSnapshot::live_empty_count(self : AuditSnapshot) -> Int

    AuditSnapshot::live_empty_ids

    source
    fn AuditSnapshot::live_empty_ids(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::maximum_active_id

    source
    fn AuditSnapshot::maximum_active_id(self : AuditSnapshot) -> Int

    AuditSnapshot::minimum_active_id

    source
    fn AuditSnapshot::minimum_active_id(self : AuditSnapshot) -> Int

    AuditSnapshot::missing_ids

    source
    fn AuditSnapshot::missing_ids(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::processed_count

    source
    fn AuditSnapshot::processed_count(self : AuditSnapshot) -> Int

    AuditSnapshot::progress_text

    source
    fn AuditSnapshot::progress_text(self : AuditSnapshot, total : Int) -> String

    AuditSnapshot::reference_at

    source
    fn AuditSnapshot::reference_at(self : AuditSnapshot, position : Int) -> (Int, Int)?

    AuditSnapshot::reference_error_count

    source
    fn AuditSnapshot::reference_error_count(self : AuditSnapshot) -> Int

    AuditSnapshot::reference_lines

    source
    fn AuditSnapshot::reference_lines(self : AuditSnapshot) -> Array[Int]

    AuditSnapshot::reference_ratio

    source
    fn AuditSnapshot::reference_ratio(self : AuditSnapshot) -> Int

    AuditSnapshot::reference_summary

    source
    fn AuditSnapshot::reference_summary(self : AuditSnapshot) -> String

    AuditSnapshot::references_on_line

    source
    fn AuditSnapshot::references_on_line(self : AuditSnapshot, line : Int) -> Int

    AuditSnapshot::same_active_state

    source
    fn AuditSnapshot::same_active_state(self : AuditSnapshot, other : AuditSnapshot) -> Bool

    AuditSnapshot::same_empty_state

    source
    fn AuditSnapshot::same_empty_state(self : AuditSnapshot, other : AuditSnapshot) -> Bool

    AuditSnapshot::state_label

    source
    fn AuditSnapshot::state_label(self : AuditSnapshot) -> String

    AuditSnapshot::step_kind_count

    source
    fn AuditSnapshot::step_kind_count(self : AuditSnapshot) -> Int

    AuditSnapshot::summary

    source
    fn AuditSnapshot::summary(self : AuditSnapshot) -> String

    CheckError

    source
    pub(all) enum CheckError {
      BadNumber(Int)
      BadCnf(Int)
      BadProof(Int)
      BadHint(Int, Int)
      MissingEmptyClause
      BadBinary(Int)
      ResourceLimit(Int)
      UnsupportedOutputFormat
    }

    All input errors carry a one-based line number when one is available.

    CheckLimits

    source
    pub(all) struct CheckLimits {
      max_steps : Int
      max_clause_literals : Int
      max_hints_per_step : Int
      max_clause_id : Int
    }

    Limits used by callers before accepting untrusted certificates.

    CheckLimits::default

    source
    fn CheckLimits::default() -> CheckLimits

    CheckStats

    source
    pub(all) struct CheckStats {
      initial_clauses : Int
      additions : Int
      deletions : Int
      rat_additions : Int
    }

    ClauseLifetime

    source
    pub(all) struct ClauseLifetime {
      id : Int
      initial : Bool
      added_at : Int
      deleted_at : Int?
      use_count : Int
      last_used_at : Int?
    }

    Lifetime and reference counts for one clause ID in a proof trace.

    ClauseLifetime::is_active

    source
    fn ClauseLifetime::is_active(self : ClauseLifetime) -> Bool

    ClauseLifetime::is_unused

    source
    fn ClauseLifetime::is_unused(self : ClauseLifetime) -> Bool

    ClauseLifetime::lifetime_steps

    source
    fn ClauseLifetime::lifetime_steps(self : ClauseLifetime, end_step : Int) -> Int

    ClauseLifetime::was_referenced

    source
    fn ClauseLifetime::was_referenced(self : ClauseLifetime) -> Bool

    ConversionOptions

    source
    pub(all) struct ConversionOptions {
      max_work : Int
      honor_unit_deletions : Bool
    }

    ConversionResult

    source
    pub(all) struct ConversionResult {
      proof : Array[ProofStep]
      stats : CheckStats
      work : Int
    }

    DependencyEdge

    source
    pub(all) struct DependencyEdge {
      from : Int
      to : Int
      negative : Bool
    }

    A directed dependency edge from a derived clause to a referenced clause.

    DependencyGraph

    source
    pub(all) struct DependencyGraph {
      edges : Array[DependencyEdge]
      nodes : Array[Int]
    }

    A compact proof dependency graph.

    DependencyGraph::edge_count

    source
    fn DependencyGraph::edge_count(self : DependencyGraph) -> Int

    DependencyGraph::has_edge

    source
    fn DependencyGraph::has_edge(self : DependencyGraph, from : Int, to : Int) -> Bool

    DependencyGraph::incoming

    source
    fn DependencyGraph::incoming(self : DependencyGraph, id : Int) -> Array[DependencyEdge]

    DependencyGraph::leaves

    source
    fn DependencyGraph::leaves(self : DependencyGraph) -> Array[Int]

    DependencyGraph::negative_edge_count

    source
    fn DependencyGraph::negative_edge_count(self : DependencyGraph) -> Int

    DependencyGraph::node_count

    source
    fn DependencyGraph::node_count(self : DependencyGraph) -> Int

    DependencyGraph::outgoing

    source
    fn DependencyGraph::outgoing(self : DependencyGraph, id : Int) -> Array[DependencyEdge]

    DependencyGraph::roots

    source
    fn DependencyGraph::roots(self : DependencyGraph) -> Array[Int]

    Diagnostic

    source
    pub(all) struct Diagnostic {
      kind : DiagnosticKind
      line : Int
      id : Int
      message : String
    }

    DiagnosticKind

    source
    pub(all) enum DiagnosticKind {
      MissingClause
      DeletedBeforeUse
      NonMonotonicId
      DuplicateAdditionId
      EmptyProof
      NoEmptyAddition
      ExcessiveHints
    }

    Diagnostic categories are stable enough for command-line consumers.

    DratStep

    source
    pub(all) struct DratStep {
      delete : Bool
      clause : Array[Int]
      line : Int
    }

    DRAT has no clause IDs or propagation hints. The first literal remains the RAT pivot; only deletion lookup uses a sorted content key.

    Formula

    source
    pub(all) struct Formula {
      variable_count : Int
      clauses : Array[Array[Int]]
    }

    Formula::clause_count

    source
    fn Formula::clause_count(self : Formula) -> Int

    Formula::clause_size_histogram

    source
    fn Formula::clause_size_histogram(self : Formula) -> Map[Int, Int]

    Formula::contains_empty_clause

    source
    fn Formula::contains_empty_clause(self : Formula) -> Bool

    Formula::literal_occurrences

    source
    fn Formula::literal_occurrences(self : Formula) -> Array[(Int, Int)]

    Count literal occurrences. The result is indexed by variable number and stores positive and negative occurrences separately.

    Formula::validate

    source
    fn Formula::validate(self : Formula) -> Result[Unit, CheckError]

    Check a formula independently of proof execution. This is useful before accepting a formula from a network or a build artifact.

    Formula::variable_count

    source
    fn Formula::variable_count(self : Formula) -> Int

    Formula::variables

    source
    fn Formula::variables(self : Formula) -> Array[Int]

    FormulaMetrics

    source
    pub(all) struct FormulaMetrics {
      variables : Int
      clauses : Int
      literals : Int
      units : Int
      tautologies : Int
      minimum_clause_size : Int
      maximum_clause_size : Int
    }

    Aggregate measurements used by proof dashboards and regression tests.

    LifetimeReport

    source
    pub(all) struct LifetimeReport {
      clauses : Array[ClauseLifetime]
      total_references : Int
      references_to_missing_ids : Int
      references_after_deletion : Int
      peak_active_clauses : Int
    }

    Aggregate clause-lifetime measurements. Positions are proof-step indices; initial clauses have added_at == 0.

    LifetimeReport::active_clause_ids

    source
    fn LifetimeReport::active_clause_ids(self : LifetimeReport) -> Array[Int]

    LifetimeReport::clause

    source
    fn LifetimeReport::clause(self : LifetimeReport, id : Int) -> ClauseLifetime?

    LifetimeReport::deleted_clause_ids

    source
    fn LifetimeReport::deleted_clause_ids(self : LifetimeReport) -> Array[Int]

    LifetimeReport::maximum_lifetime_steps

    source
    fn LifetimeReport::maximum_lifetime_steps(self : LifetimeReport, end_step : Int) -> Int

    LifetimeReport::maximum_uses

    source
    fn LifetimeReport::maximum_uses(self : LifetimeReport) -> Int

    LifetimeReport::mean_lifetime_steps

    source
    fn LifetimeReport::mean_lifetime_steps(self : LifetimeReport, end_step : Int) -> Int

    LifetimeReport::mean_uses_per_clause

    source
    fn LifetimeReport::mean_uses_per_clause(self : LifetimeReport) -> Int

    LifetimeReport::mean_uses_per_used_clause

    source
    fn LifetimeReport::mean_uses_per_used_clause(self : LifetimeReport) -> Int

    LifetimeReport::most_used_clause

    source
    fn LifetimeReport::most_used_clause(self : LifetimeReport) -> ClauseLifetime?

    LifetimeReport::never_used_active_ids

    source
    fn LifetimeReport::never_used_active_ids(self : LifetimeReport) -> Array[Int]

    LifetimeReport::summary

    source
    fn LifetimeReport::summary(self : LifetimeReport) -> String

    LifetimeReport::unused_clause_ids

    source
    fn LifetimeReport::unused_clause_ids(self : LifetimeReport) -> Array[Int]

    LifetimeReport::used_clause_count

    source
    fn LifetimeReport::used_clause_count(self : LifetimeReport) -> Int

    LimitViolation

    source
    pub(all) enum LimitViolation {
      TooManySteps(Int)
      TooManyClauseLiterals(Int)
      TooManyHints(Int)
      ClauseIdTooLarge(Int)
    }

    LiteralIndex

    source
    pub(all) struct LiteralIndex {
      by_literal : Map[Int, Array[Int]]
      clauses : Map[Int, Array[Int]]
    }

    An inverted index from a literal to the active clause IDs containing it. The index is deliberately separate from the checker so callers can reuse it for proof inspection and incremental formula tools.

    LiteralIndex::clause

    source
    fn LiteralIndex::clause(self : LiteralIndex, id : Int) -> Array[Int]?

    LiteralIndex::contains_id

    source
    fn LiteralIndex::contains_id(self : LiteralIndex, id : Int) -> Bool

    LiteralIndex::ids_for

    source
    fn LiteralIndex::ids_for(self : LiteralIndex, literal : Int) -> Array[Int]

    LiteralIndex::insert

    source
    fn LiteralIndex::insert(self : LiteralIndex, id : Int, clause : Array[Int]) -> Bool

    LiteralIndex::literal_count

    source
    fn LiteralIndex::literal_count(self : LiteralIndex) -> Int

    LiteralIndex::new

    source
    fn LiteralIndex::new(formula : Formula) -> LiteralIndex

    LiteralIndex::remove

    source
    fn LiteralIndex::remove(self : LiteralIndex, id : Int) -> Bool

    LiteralIndex::size

    source
    fn LiteralIndex::size(self : LiteralIndex) -> Int

    LiteralIndex::validate

    source
    fn LiteralIndex::validate(self : LiteralIndex) -> Bool

    LiteralState

    source
    pub(all) enum LiteralState {
      True
      False
      Unknown
    }

    A three-valued literal result used by diagnostic propagation helpers.

    PreflightReport

    source
    pub(all) struct PreflightReport {
      ok : Bool
      diagnostics : Array[Diagnostic]
      limits_checked : Bool
      forward_references : Int
      referenced_ids : Int
    }

    A non-semantic preflight result for rejecting obviously malformed proofs.

    PreflightReport::diagnostic_count

    source
    fn PreflightReport::diagnostic_count(self : PreflightReport) -> Int

    PreflightReport::is_ok

    source
    fn PreflightReport::is_ok(self : PreflightReport) -> Bool

    PreflightReport::summary

    source
    fn PreflightReport::summary(self : PreflightReport) -> String

    ProofFormat

    source
    pub(all) enum ProofFormat {
      LratText
      LratBinary
      DratText
      DratBinary
    }

    ProofMetrics

    source
    pub(all) struct ProofMetrics {
      steps : Int
      additions : Int
      deletions : Int
      maximum_id : Int
      total_clause_literals : Int
      total_hints : Int
      maximum_clause_size : Int
      maximum_hint_size : Int
      empty_additions : Int
      rat_steps : Int
    }

    Measurements for comparing certificates across solver versions.

    ProofSession

    source
    pub(all) struct ProofSession {
      variable_count : Int
      active : Map[Int, Array[Int]]
      index : LiteralIndex
      next_id : Int
      additions : Int
      deletions : Int
    }

    Mutable state for replaying a certificate incrementally. The session does not decide whether a learned clause is sound; callers should call verify_addition or use verify before committing untrusted steps.

    ProofSession::active_clauses

    source
    fn ProofSession::active_clauses(self : ProofSession) -> Array[(Int, Array[Int])]

    ProofSession::active_count

    source
    fn ProofSession::active_count(self : ProofSession) -> Int

    ProofSession::active_ids

    source
    fn ProofSession::active_ids(self : ProofSession) -> Array[Int]

    ProofSession::active_literal_count

    source
    fn ProofSession::active_literal_count(self : ProofSession) -> Int

    ProofSession::active_tautology_count

    source
    fn ProofSession::active_tautology_count(self : ProofSession) -> Int

    ProofSession::add_clause

    source
    fn ProofSession::add_clause(self : ProofSession, clause : Array[Int]) -> Int

    ProofSession::add_clause_with_id

    source
    fn ProofSession::add_clause_with_id(self : ProofSession, id : Int, clause : Array[Int]) -> Bool

    ProofSession::addition_count

    source
    fn ProofSession::addition_count(self : ProofSession) -> Int

    ProofSession::contains_empty_clause

    source
    fn ProofSession::contains_empty_clause(self : ProofSession) -> Bool

    ProofSession::delete_clause

    source
    fn ProofSession::delete_clause(self : ProofSession, id : Int) -> Bool

    ProofSession::deletion_count

    source
    fn ProofSession::deletion_count(self : ProofSession) -> Int

    ProofSession::from_formula

    source
    fn ProofSession::from_formula(formula : Formula) -> ProofSession

    ProofSession::get_clause

    source
    fn ProofSession::get_clause(self : ProofSession, id : Int) -> Array[Int]?

    ProofSession::has_clause

    source
    fn ProofSession::has_clause(self : ProofSession, id : Int) -> Bool

    ProofSession::ids_for_literal

    source
    fn ProofSession::ids_for_literal(self : ProofSession, literal : Int) -> Array[Int]

    ProofSession::index_is_consistent

    source
    fn ProofSession::index_is_consistent(self : ProofSession) -> Bool

    ProofSession::next_id

    source
    fn ProofSession::next_id(self : ProofSession) -> Int

    ProofSession::reset_counters

    source
    fn ProofSession::reset_counters(self : ProofSession) -> Unit

    ProofSession::snapshot

    source
    fn ProofSession::snapshot(self : ProofSession) -> ProofSession

    ProofSession::variable_count

    source
    fn ProofSession::variable_count(self : ProofSession) -> Int

    ProofSlice

    source
    pub(all) struct ProofSlice {
      start : Int
      stop : Int
      steps : Array[ProofStep]
    }

    A contiguous view of proof steps, useful for debugging a failing range.

    ProofSlice::clause_literal_count

    source
    fn ProofSlice::clause_literal_count(self : ProofSlice) -> Int

    ProofSlice::contains_empty

    source
    fn ProofSlice::contains_empty(self : ProofSlice) -> Bool

    ProofSlice::dependency_graph

    source
    fn ProofSlice::dependency_graph(self : ProofSlice) -> DependencyGraph

    ProofSlice::empty_step_count

    source
    fn ProofSlice::empty_step_count(self : ProofSlice) -> Int

    ProofSlice::find_id

    source
    fn ProofSlice::find_id(self : ProofSlice, id : Int) -> ProofStep?

    ProofSlice::first_id

    source
    fn ProofSlice::first_id(self : ProofSlice) -> Int?

    ProofSlice::hint_count

    source
    fn ProofSlice::hint_count(self : ProofSlice) -> Int

    ProofSlice::is_empty

    source
    fn ProofSlice::is_empty(self : ProofSlice) -> Bool

    ProofSlice::last_id

    source
    fn ProofSlice::last_id(self : ProofSlice) -> Int?

    ProofSlice::length

    source
    fn ProofSlice::length(self : ProofSlice) -> Int

    ProofSlice::metrics

    source
    fn ProofSlice::metrics(self : ProofSlice) -> ProofMetrics

    ProofSlice::rat_step_count

    source
    fn ProofSlice::rat_step_count(self : ProofSlice) -> Int

    ProofSlice::render

    source
    fn ProofSlice::render(self : ProofSlice) -> String

    ProofSlice::with_limit

    source
    fn ProofSlice::with_limit(self : ProofSlice, limit : Int) -> ProofSlice

    ProofStep

    source
    pub(all) struct ProofStep {
      id : Int
      delete : Bool
      clause : Array[Int]
      hints : Array[Int]
      line : Int
    }

    A parsed proof step, useful for tools that want to inspect a certificate without executing it. delete distinguishes an LRAT deletion record.

    ProofSummary

    source
    pub(all) struct ProofSummary {
      step_count : Int
      addition_count : Int
      deletion_count : Int
      maximum_id : Int
      has_empty_addition : Bool
      rat_candidate_count : Int
      hint_count : Int
      deleted_clause_reference_count : Int
    }

    A compact, serializable summary for CI integrations.

    ReplayError

    source
    pub(all) enum ReplayError {
      InvalidFormula
      InvalidProof
      NonMonotonicId(Int)
      DuplicateClause(Int)
      UnknownDeletion(Int)
      InvalidLiteral(Int, Int)
      InvalidClause(Int)
      MissingFinalEmptyClause
    }

    Errors produced while replaying the structural lifetime of a proof.

    ReplayResult

    source
    pub(all) struct ReplayResult {
      final_empty : Bool
      additions : Int
      deletions : Int
      active_clauses : Int
    }

    ReplayResult::active_count

    source
    fn ReplayResult::active_count(self : ReplayResult) -> Int

    ReplayResult::is_unsat_certificate

    source
    fn ReplayResult::is_unsat_certificate(self : ReplayResult) -> Bool

    added_clause_ids

    source
    fn added_clause_ids(steps : Array[ProofStep]) -> Array[Int]

    all_resolvents

    source
    fn all_resolvents(left : Array[Int], right : Array[Int]) -> Array[Array[Int]]

    analyze_clause_lifetimes

    source
    fn analyze_clause_lifetimes(formula : Formula, steps : Array[ProofStep]) -> LifetimeReport

    Measure clause use and deletion across the supplied trace. This is a structural profiler and intentionally does not verify LRAT hint semantics.

    apply_assignment

    source
    fn apply_assignment(formula : Formula, assignment : Map[Int, Bool]) -> Formula

    assign_literal

    source
    fn assign_literal(assignment : Map[Int, Bool], literal : Int) -> Bool

    audit_all

    source
    fn audit_all(formula : Formula, steps : Array[ProofStep]) -> AuditSnapshot

    audit_at_line

    source
    fn audit_at_line(formula : Formula, steps : Array[ProofStep], line : Int) -> AuditSnapshot

    audit_prefix

    source
    fn audit_prefix(formula : Formula, steps : Array[ProofStep], step_limit : Int) -> AuditSnapshot

    Run a structural audit through at most step_limit entries. The first tuple member in each reference array is the source line; the second is the referenced clause ID. Initial CNF clauses use IDs 1 through M.

    build_dependency_graph

    source
    fn build_dependency_graph(steps : Array[ProofStep]) -> DependencyGraph

    check_limits

    source
    fn check_limits(steps : Array[ProofStep], limits : CheckLimits) -> Result[Unit, LimitViolation]

    clause_contains_literal

    source
    fn clause_contains_literal(clause : Array[Int], literal : Int) -> Bool

    clause_equal

    source
    fn clause_equal(left : Array[Int], right : Array[Int]) -> Bool

    clause_is_tautology

    source
    fn clause_is_tautology(clause : Array[Int]) -> Bool

    clause_state

    source
    fn clause_state(assignment : Map[Int, Bool], clause : Array[Int]) -> LiteralState

    clause_subset

    source
    fn clause_subset(subset : Array[Int], superset : Array[Int]) -> Bool

    clause_subsumed

    source
    fn clause_subsumed(formula : Formula, target : Array[Int]) -> Bool

    A clause is redundant when another clause subsumes it.

    clause_variables

    source
    fn clause_variables(clause : Array[Int]) -> Array[Int]

    combine_preflight_reports

    source
    fn combine_preflight_reports(left : PreflightReport, right : PreflightReport) -> PreflightReport

    convert_drat

    source
    fn convert_drat(cnf : String, proof : String) -> Result[ConversionResult, CheckError]

    convert_drat_steps

    source
    fn convert_drat_steps(formula : Formula, steps : Array[DratStep], options : ConversionOptions) -> Result[ConversionResult, CheckError]

    Forward DRAT checking and LRAT hint generation. Duplicate clauses are tracked as distinct IDs; one deletion removes one occurrence. Absent deletions are ignored. By default unit deletions follow DRAT-trim's ignored-unit policy; set honor_unit_deletions for literal deletion semantics.

    convert_proof

    source
    fn convert_proof(cnf : String, input : Bytes, from : ProofFormat, to : ProofFormat) -> Result[Bytes, CheckError]

    All four inputs can produce textual or binary LRAT. An output certificate is emitted only after verifying the supplied formula as UNSAT.

    default_conversion_options

    source
    fn default_conversion_options() -> ConversionOptions

    deleted_clause_ids

    source
    fn deleted_clause_ids(steps : Array[ProofStep]) -> Array[Int]

    dependency_depth

    source
    fn dependency_depth(graph : DependencyGraph, node : Int) -> Int

    dependency_summary

    source
    fn dependency_summary(graph : DependencyGraph) -> String

    diagnose_proof

    source
    fn diagnose_proof(steps : Array[ProofStep]) -> Array[Diagnostic]

    diagnostic_kind_name

    source
    fn diagnostic_kind_name(kind : DiagnosticKind) -> String

    diagnostic_summary

    source
    fn diagnostic_summary(findings : Array[Diagnostic]) -> String

    diagnostics_have_errors

    source
    fn diagnostics_have_errors(findings : Array[Diagnostic]) -> Bool

    encode_binary_drat

    source
    fn encode_binary_drat(steps : Array[DratStep]) -> Result[Bytes, CheckError]

    encode_binary_lrat

    source
    fn encode_binary_lrat(steps : Array[ProofStep]) -> Result[Bytes, CheckError]

    Syntax-only conversion. convert_proof verifies the supplied CNF as well.

    formula_clause_ids

    source
    fn formula_clause_ids(formula : Formula) -> Array[Int]

    formula_contains_clause

    source
    fn formula_contains_clause(formula : Formula, target : Array[Int]) -> Bool

    formula_density

    source
    fn formula_density(formula : Formula) -> Int

    formula_has_unit_conflict

    source
    fn formula_has_unit_conflict(formula : Formula) -> Bool

    formula_is_simplified

    source
    fn formula_is_simplified(formula : Formula) -> Bool

    formula_is_trivial

    source
    fn formula_is_trivial(formula : Formula) -> Bool

    formula_max_clause_size

    source
    fn formula_max_clause_size(formula : Formula) -> Int

    formula_min_clause_size

    source
    fn formula_min_clause_size(formula : Formula) -> Int

    formula_resolvents

    source
    fn formula_resolvents(formula : Formula, left_id : Int, right_id : Int) -> Array[Array[Int]]

    formula_state

    source
    fn formula_state(assignment : Map[Int, Bool], formula : Formula) -> LiteralState

    formula_tautology_count

    source
    fn formula_tautology_count(formula : Formula) -> Int

    formula_unit_count

    source
    fn formula_unit_count(formula : Formula) -> Int

    formula_unit_literals

    source
    fn formula_unit_literals(formula : Formula) -> Array[Int]

    index_clause_count

    source
    fn index_clause_count(index : LiteralIndex) -> Int

    index_literal_count

    source
    fn index_literal_count(index : LiteralIndex) -> Int

    is_hint_free

    source
    fn is_hint_free(steps : Array[ProofStep]) -> Bool

    Detect a proof that mentions no hints. Such a proof can only derive the empty clause from an already contradictory input formula.

    limit_violation_name

    source
    fn limit_violation_name(violation : LimitViolation) -> String

    literal_state

    source
    fn literal_state(assignment : Map[Int, Bool], literal : Int) -> LiteralState

    measure_formula

    source
    fn measure_formula(formula : Formula) -> FormulaMetrics

    measure_proof

    source
    fn measure_proof(steps : Array[ProofStep]) -> ProofMetrics

    normalize_clause

    source
    fn normalize_clause(clause : Array[Int]) -> Array[Int]

    Return a sorted copy of a clause, preserving literal uniqueness.

    normalize_formula

    source
    fn normalize_formula(formula : Formula) -> Formula

    parse_binary_drat

    source
    fn parse_binary_drat(bytes : Bytes) -> Result[Array[DratStep], CheckError]

    parse_binary_lrat

    source
    fn parse_binary_lrat(bytes : Bytes, initial_id : Int) -> Result[Array[ProofStep], CheckError]

    CaDiCaL >=1.9.0 signed-ID binary LRAT. Deletions have no record ID; initial_id must be the number of original CNF clauses.

    parse_cnf

    source
    fn parse_cnf(input : String) -> Result[Formula, CheckError]

    Read strict DIMACS CNF. Clause literals can span lines; comments and the header occupy complete lines. Original clause IDs are 1 through M.

    parse_drat

    source
    fn parse_drat(text : String) -> Result[Array[DratStep], CheckError]

    parse_format

    source
    fn parse_format(name : String) -> ProofFormat?

    parse_proof

    source
    fn parse_proof(text : String) -> Result[Array[ProofStep], CheckError]

    Parse proof text into immutable step values. Semantic checking remains the responsibility of verify_formula, so this function is also useful for diagnostics and proof statistics.

    preflight_default

    source
    fn preflight_default(steps : Array[ProofStep]) -> PreflightReport

    preflight_proof

    source
    fn preflight_proof(steps : Array[ProofStep], limits : CheckLimits) -> PreflightReport

    process_proof

    source
    fn process_proof(cnf : String, input : Bytes, format : ProofFormat, options : ConversionOptions) -> Result[ConversionResult, CheckError]

    Core processing uses no file I/O, for the CLI, JavaScript and Wasm callers.

    proof_additions

    source
    fn proof_additions(steps : Array[ProofStep]) -> Int

    proof_clause_density

    source
    fn proof_clause_density(metrics : ProofMetrics) -> Int

    proof_deletions

    source
    fn proof_deletions(steps : Array[ProofStep]) -> Int

    proof_has_duplicate_addition_ids

    source
    fn proof_has_duplicate_addition_ids(steps : Array[ProofStep]) -> Bool

    proof_has_empty_addition

    source
    fn proof_has_empty_addition(steps : Array[ProofStep]) -> Bool

    proof_has_forward_reference

    source
    fn proof_has_forward_reference(steps : Array[ProofStep]) -> Bool

    proof_hint_density

    source
    fn proof_hint_density(metrics : ProofMetrics) -> Int

    proof_is_minimal_shape

    source
    fn proof_is_minimal_shape(metrics : ProofMetrics) -> Bool

    proof_is_well_formed

    source
    fn proof_is_well_formed(steps : Array[ProofStep]) -> Bool

    proof_max_id

    source
    fn proof_max_id(steps : Array[ProofStep]) -> Int

    proof_metrics_summary

    source
    fn proof_metrics_summary(metrics : ProofMetrics) -> String

    proof_reference_ratio

    source
    fn proof_reference_ratio(report : PreflightReport, steps : Array[ProofStep]) -> Int

    propagate_units

    source
    fn propagate_units(assignment : Map[Int, Bool], formula : Formula) -> Bool

    Perform ordinary unit propagation until a fixed point. The return value is false when a clause becomes contradictory.

    rat_candidates

    source
    fn rat_candidates(index : LiteralIndex, pivot : Int) -> Array[Int]

    Return active clause IDs that need RAT checking for a pivot.

    referenced_clause_ids

    source
    fn referenced_clause_ids(steps : Array[ProofStep]) -> Array[Int]

    Return IDs referenced by a proof in first-seen order. This helps a caller preflight a certificate before allocating its full checking state.

    remove_duplicate_clauses

    source
    fn remove_duplicate_clauses(formula : Formula) -> Formula

    remove_subsumed_clauses

    source
    fn remove_subsumed_clauses(formula : Formula) -> Formula

    render_clause

    source
    fn render_clause(clause : Array[Int]) -> String

    render_dimacs

    source
    fn render_dimacs(formula : Formula) -> String

    render_drat

    source
    fn render_drat(steps : Array[DratStep]) -> String

    render_proof

    source
    fn render_proof(steps : Array[ProofStep]) -> String

    Render a parsed proof with canonical whitespace. The output is intended for diagnostics and fixtures, not as a replacement for a proof optimizer.

    replay

    source
    fn replay(cnf : String, proof : String) -> Result[ReplayResult, ReplayError]

    replay_error_name

    source
    fn replay_error_name(error : ReplayError) -> String

    replay_structure

    source
    fn replay_structure(formula : Formula, steps : Array[ProofStep]) -> Result[ReplayResult, ReplayError]

    Replay additions and deletions without checking RAT hints. This is useful for separating lifetime/format errors from semantic proof errors.

    resolve_clauses

    source
    fn resolve_clauses(left : Array[Int], right : Array[Int], pivot : Int) -> Array[Int]?

    simplify_formula

    source
    fn simplify_formula(formula : Formula) -> Formula

    slice_proof

    source
    fn slice_proof(steps : Array[ProofStep], start : Int, stop : Int) -> ProofSlice

    slices_have_contiguous_ranges

    source
    fn slices_have_contiguous_ranges(slices : Array[ProofSlice]) -> Bool

    split_proof

    source
    fn split_proof(steps : Array[ProofStep], width : Int) -> Array[ProofSlice]

    summarize_proof

    source
    fn summarize_proof(steps : Array[ProofStep]) -> ProofSummary

    total_slice_steps

    source
    fn total_slice_steps(slices : Array[ProofSlice]) -> Int

    unit_literal

    source
    fn unit_literal(assignment : Map[Int, Bool], clause : Array[Int]) -> Int?

    unit_simplify

    source
    fn unit_simplify(formula : Formula) -> Result[Formula, Unit]

    verify

    source
    fn verify(cnf : String, proof : String) -> Result[CheckStats, CheckError]

    verify_formula

    source
    fn verify_formula(formula : Formula, proof : String) -> Result[CheckStats, CheckError]

    Verify a textual LRAT proof against an already parsed formula. A proof succeeds only after a valid empty clause has been added.

    verify_input

    source
    fn verify_input(cnf : String, input : Bytes, format : ProofFormat) -> Result[CheckStats, CheckError]

    verify_steps

    source
    fn verify_steps(formula : Formula, steps : Array[ProofStep]) -> Result[CheckStats, CheckError]

    Check parsed records with the same semantics for all supported encodings.

    Source Files

    Powered by MoonBit

    Site sourceReport issueModulesSkillsCLIBuild queueStatistics

    © 2026 mooncakes.io