DDDLIB: A library for solving quantified difference inequalities

Abstract

DDDLIB is a library for manipulating formulae in a firstorder logic over Boolean variables and inequalities of the form x1−x2 ≤ d, where x1, x2 are real variables and d is an integer constant. Formulae are represented in a semi-canonical data structure called difference decision diagrams (DDDs) which provide efficient algorithms for constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). The library is written in C andhas interfaces for C++, StandardML andOb jective Caml.