00001 /*!\page INSTALL INSTALL 00002 00003 <h2> 00004 Building CVC Lite 00005 </h2> 00006 00007 To build CVC Lite, do the following in the root directory of the CVC Lite 00008 distribution: 00009 00010 <pre> 00011 00012 autoheader 00013 autoconf 00014 ./configure 00015 make 00016 00017 </pre> 00018 00019 If this fails, you may need to install gmp (see below). For other 00020 configuration options, type ./configure --help 00021 00022 The library is called libcvclite.a (libcvclite.so for the shared 00023 object library). After compilation, it is created in an 00024 architecture-dependent subdirectory of lib (e.g. lib/linux-i686/libcvclite.a). 00025 00026 The build will also produce an executable called cvcl which is stored 00027 in an architecture-dependent subdirectory of bin. 00028 00029 NOTE, that by default CVC Lite builds with debugging enabled 00030 (--with-build=debug), which can be 4x to 10x as slow as the optimized 00031 build (--with-build=optimized). Of course, the debug build is much more 00032 useful in finding and reporting bugs. 00033 00034 The subdirectory test contains an example program which uses libcvclite.a 00035 00036 <h2> 00037 Installing GMP 00038 </h2> 00039 00040 We recommend that CVC Lite be built with support for arbitrary precision 00041 arithmetic. For that, you need the GMP library. 00042 00043 In theory, any standard and sanely built GMP distribution should work. 00044 Many platforms come with gmp pre-installed. If you have to compile 00045 and install GMP, here are the generic instructions on how to do it: 00046 00047 1. Download the gmp source code from http://swox.com/gmp/ 00048 00049 2. Unpack the sources, and from the root-directory of the gmp source code, run 00050 00051 ./configure 00052 make 00053 00054 On some Solaris machines, you may need to configure GMP with 00055 00056 ./configure ABI=32 00057 00058 to make the resulting GMP library compatible with the CVC Lite 00059 libraries. The reason for this is that the default ABI that gcc 00060 chooses in CVC Lite compilation is not necessarily the default ABI 00061 that GMP configure script selects, and one of them may need to be 00062 adjusted. 00063 00064 3. Now, either install gmp system-wide (make install), or supply the 00065 appropriate --with-extra-libs and --with-extra-includes options to CVC Lite 00066 ./configure script (see the output of ./configure --help for more info). 00067 00068 00069 <h2> 00070 Installing CVC Lite 00071 </h2> 00072 00073 To install CVC Lite system-wide, run: 00074 00075 <pre> 00076 00077 make install 00078 00079 </pre> 00080 00081 This installs the libraries (libcvclite.{a,so}), the executable 00082 (cvcl), and the necessary header files in the system directory 00083 specified at ./configure time (default is /usr/local/). 00084 00085 By default, the following files will be installed: 00086 00087 <pre> 00088 00089 /usr/local/lib/libcvclite.{a,so} 00090 /usr/local/bin/cvcl 00091 /usr/local/include/*.h 00092 00093 </pre> 00094 00095 The include/ directory will contain vc.h and various other header 00096 files it depends on. 00097 00098 If you choose to install CVC Lite with 'stow' or 'depot' package 00099 managers, you can specify the package installation prefix as follows: 00100 00101 <pre> 00102 00103 make install prefix=/usr/local/stow/cvcl-1.0.0 00104 00105 </pre> 00106 00107 For more information on this distribution, see the \ref README file. 00108 00109 <h2> 00110 Documentation 00111 </h2> 00112 00113 To build HTML documentation, run 00114 00115 <pre> 00116 00117 make doc 00118 00119 </pre> 00120 00121 Then open doc/html/index.html in your favorite browser. 00122 00123 The input language of CVC Lite is for the most part the same as the presentation 00124 language of CVC which is documented at 00125 <a href="http://verify.stanford.edu/CVC">http://verify.stanford.edu/CVC</a>. 00126 00127 */