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

VarSet

Variable set, potentially along with a variable order and variable names

Vec2d

Compact representation of a Vec<Vec<T>>

Vec2dIter

Iterator over the inner vectors of a Vec2d

Enums

AIGVar

Kinds of AIG vars

ParseOptionsBuilderError

Error type for ParseOptionsBuilder

Problem

Different problem kinds that may be returned by the problem parsers

Prop

Propositional formula

Tree

Rooted tree with values of type T at the leaves

Type Aliases

Var

Variable type