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(cnf) => println!("{:?}", cnf.clauses()),
    Problem::Prop(prop) => println!("{:?}", prop.formula()),
    _ => 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

• aiger
  AIGER parser based on “The AIGER And-Inverter Graph (AIG) Format Version 20071012” and “AIGER 1.9 And Beyond”
• dimacs
  DIMACS CNF/SAT parser based on the paper “Satisfiability Suggested Format”
• load_file
  Convenience functions etc. to load a Problem from file

Structs

• AIG
  And-inverter graph
• CNFProblem
  CNF problem instance
• Literal
  A possibly negated variable
• ParseOptions
  Options for the parsers
• ParseOptionsBuilder
  Builder for ParseOptions.
• PropProblem
  Propositional formula problem
• Vec2d
  Compact representation of a Vec<Vec<T>>
• Vec2dIter
  Iterator over the inner vectors of a Vec2d

Enums

• AIGVar
  Kinds of AIG vars
• 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