pub(all) suberror AllenError {
  InvalidRelation(String)
  InvalidMask(Int)
  InvalidInterval(Int, Int)
  InvalidName(String)
  DuplicateName(String)
  UnknownName(String)
  InvalidIndex(Int)
  InvalidLimit(String)
  InvalidFormat(String)
  TooLarge(Int)
}

pub struct Algebra {
  // private fields
}

pub(all) struct ClosureReport {
  status : ClosureStatus
  network : Network
  operations : Int
  reductions : Array[Reduction]
  reduction_count : Int
  trace_complete : Bool
  conflict : Conflict?
}

pub(all) enum ClosureStatus {
  PathConsistent
  Contradiction
  PropagationLimit
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub(all) struct Conflict {
  left : String
  right : String
  via : String?
}

pub(all) struct Constraint {
  left : String
  right : String
  allowed : RelSet
  label : String
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub(all) enum CoreOutcome {
  ConflictCore(UnsatCore)
  SourceSatisfiable(Witness)
  CoreUnknown(SearchLimit)
}

pub(all) struct DomainChange {
  left : String
  right : String
  before : RelSet
  after : RelSet
  removed : RelSet
  added : RelSet
}

pub(all) enum Entailment {
  Proven
  Refuted(Witness)
  InconsistentInput
  EntailmentUnknown(SearchLimit)
}

pub struct Interval {
  // private fields
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub struct Network {
  // private fields
}

pub(all) struct NetworkStats {
  intervals : Int
  pairs : Int
  constrained_pairs : Int
  atomic_pairs : Int
  ambiguous_pairs : Int
  empty_domains : Int
  alternatives : Int
  source_constraints : Int
}

pub(all) struct ObservationConflict {
  left : String
  right : String
  expected : RelSet
  observed : Relation
}

pub(all) struct PossibilityReport {
  possible : RelSet
  impossible : RelSet
  unknown : RelSet
  models : Array[RelationModel]
  nodes : Int
  operations : Int
}

pub struct PropagationOptions {
  // private fields
}

pub(all) struct Reduction {
  left : Int
  right : Int
  via : Int
  before : RelSet
  after : RelSet
}

pub struct RelSet {
  // private fields
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub(all) enum Relation {
  Before
  Meets
  Overlaps
  Starts
  During
  Finishes
  Equal
  After
  MetBy
  OverlappedBy
  StartedBy
  Contains
  FinishedBy
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub(all) struct RelationModel {
  relation : Relation
  witness : Witness
}

pub(all) enum SearchLimit {
  NodeBudget
  OperationBudget
} derive(Eq, 
@moonbitlang/core/debug.Debug
Debug)

pub struct SearchOptions {
  // private fields
}

pub(all) enum SolveOutcome {
  Satisfiable(Witness)
  Unsatisfiable
  Unknown(SearchLimit)
}

pub(all) struct SolveReport {
  outcome : SolveOutcome
  nodes : Int
  operations : Int
  maximum_depth : Int
}

pub(all) struct UnsatCore {
  constraints : Array[Constraint]
  minimal : Bool
  checks : Int
  unresolved_checks : Int
}

pub struct Witness {
  // private fields
}

fn add_observations(net : Network, names : Array[String], spans : Array[Interval]) -> Network raise AllenError

fn check_observations(net : Network, names : Array[String], spans : Array[Interval]) -> Array[ObservationConflict] raise AllenError

fn compare_domains(before : Network, after : Network) -> Array[DomainChange] raise AllenError

fn entails(alg : Algebra, net : Network, left : String, right : String, claim : RelSet, options : SearchOptions) -> Entailment raise AllenError

fn explain_unsat(alg : Algebra, net : Network, options : SearchOptions, max_checks? : Int) -> CoreOutcome raise AllenError

fn is_path_consistent(alg : Algebra, net : Network) -> Bool

fn merge_networks(left : Network, right : Network) -> Network raise AllenError

fn network_from_json(value : Json) -> Network raise AllenError

fn observe(names : Array[String], spans : Array[Interval]) -> Network raise AllenError

fn parse_dsl(text : String) -> Network raise AllenError

fn parse_network_json(text : String) -> Network raise AllenError

fn parse_relation(text : String) -> Relation raise AllenError

fn parse_relset(text : String) -> RelSet raise AllenError

fn possible_relations(alg : Algebra, net : Network, left : String, right : String, options : SearchOptions) -> PossibilityReport raise AllenError

fn propagate(alg : Algebra, net : Network, options : PropagationOptions) -> ClosureReport

fn realize_atomic(net : Network) -> Witness? raise AllenError

fn relations() -> Array[Relation]

fn solve(alg : Algebra, net : Network, options : SearchOptions) -> SolveReport raise AllenError

fn verify_core(alg : Algebra, names : Array[String], core : UnsatCore, options : SearchOptions) -> SolveReport raise AllenError

fn verify_trace(alg : Algebra, initial : Network, report : ClosureReport) -> Bool