DDDLIB: A Library For Solving Quantified Difference Inequalities
TR-2002-12, Author: Jesper Møller
Jesper Møller February 2002
Abstract
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.
Technical report TR-2002-12 in IT University Technical Report Series, February 2002.
Available as
PDF.