GiNaCRA: A C++ Library for Real Algebraic Computations?

Abstract. We present the growing C++ library GiNaCRA, which provides efficient and easy-to-integrate data structures and methods for real al-gebra. It is based on the C++ library GiNaC, supporting the symbolic representation and manipulation of polynomials. In contrast to other similar tools, our open source library aids exact, real algebraic computa-tions based on an appropriate data type representing real zeros of poly-nomials. The only non-standard library GiNaCRA depends on is GiNaC, which makes the installation and usage of our library simple. Our long-term goal is to integrate decision procedures for real algebra within the Satisfiability-Modulo-Theories (SMT) context and thereby provide tool support for many applied formal methods.