Crate oxidd_parser

Collection of parsers for various logical problem formats

Every format is parsed into a Circuit, i.e., a propositional formula with structure sharing, to enable (mostly) uniform handling of different formats in an application.

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
};
println!("circuit: {:?}", problem.circuit);
println!("additional details: {:?}", problem.details);

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”

nnf

Negation normal form parser for an extended version of c2d’s d-DNNF output format

Structs

AIGERDetails

Problem details such as latches, outputs, and bad states for an and-inverter graph

Circuit

Combinational circuit with negation as well as n-ary AND, OR, and XOR gates

CircuitGateIter

Iterator returned by Circuit::iter_gates()

Gate

Logical gate including the literals representing its inputs

Literal

A possibly negated variable

ParseOptions

Options for the parsers

ParseOptionsBuilder

Builder for ParseOptions.

Problem

Problem that may be returned by the problem parsers

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

FileType

File types

GateKind

Kind of a logical gate in a Circuit

ParseOptionsBuilderError

Error type for ParseOptionsBuilder

ProblemDetails

Details of a Problem in addition to the circuit structure

Tree

Rooted tree with values of type T at the leaves

Functions

load_file

Load and parse the file at path, reporting errors to stderr

parse

Parse input using the parser for the given file_type, emitting errors or warnings to writer

Type Aliases

Var

Variable type