DDDLIB: A Library For Solving Quantified Difference Inequalities

DDDLIB is a library for manipulating expressions in a first-order logic over Boolean variables and inequalities of the form x1-x2<=d, where x1,x2 are real variables and d is an integer constant. expressions are represented in a semi-canonical data structure called difference decision diagrams (ddds) which provide efficient algorithms for constructing expressions 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 and has interfaces for c++, moscow ml and ocaml.