Supplementary material for the paper "Computation in Real Closed Infinitesimal and
Transcendental Extensions of the Rationals".

Browsing the source code described in the paper

  • Go to cade24 branch
  • Click in Files
  • The main files are located in the sub-directory src/math/realclosure, they contain approximately 7000 lines of C++ code. The main module only depends on the Z3 interval arithmetic package (sub-directory src/math/interval), and basic data-structures and numeral types such as binary rationals (sub-directory src/util).

Download pre-compiled binaries for Windows

To be able to run the examples, you have to include the bin subdirectory in your PYTHONPATH environment variable.

Compilation instructions for Linux and OSX

  • Download the source code using the link above.
  • Go to the z3-cade24 directory.
  • If you have the Gnu Multiple precision library (GMP) installed in your system, use the option '-g'. GMP is faster than the Z3 big number package.
      ./configure -g
  • If you don't have GMP, then use
  • Then, execute
      cd build
  • To execute the examples, include the build directory in your 'PYTHONPATH'. For example, if z3-cade24 is in the directory '/home/grant/z3-cade24', and you use bash.
     export PYTHONPATH=/home/grant/z3-cade24
  • The installation is complete, you can execute the example '' in the examples zip file using

Last edited Feb 7, 2013 at 4:22 AM by leodemoura, version 24


No comments yet.