Crate oxidd_parser

Collection of parsers for various problem formats

Example

let parse_options = ParseOptionsBuilder::default().build().unwrap();
let Some(problem) = load_file("foo.dimacs", &parse_options) else {
    return; // an error message has been printed to stderr
};
match problem {
    Problem::CNF { clauses, .. } => println!("{clauses:?}"),
    Problem::Prop { ast, .. } => println!("{ast:?}"),
    _ => todo!("problem kind not yet supported"),
}

Feature flags

• load-file (enabled by default) — Convenience functions etc. to load a problem from file (load_file)

Modules

• dimacs
  A DIMACS CNF/SAT parser based on the paper “Satisfiability Suggested Format”
• load_file
  Convenience functions etc. to load a Problem from file

Structs

• ParseOptions
  Options for the parsers
• ParseOptionsBuilder
  Builder for ParseOptions.

Enums

• ClauseOrderNode
  Nodes in a pre-linearized binary clause order tree
• ParseOptionsBuilderError
  Error type for ParseOptionsBuilder
• Problem
  Different problem kinds that may be returned by the problem parsers
• Prop
  Propositional formula

Type Aliases

• Var
  Variable type
• VarOrder
  Variable order including variable names