CVC3  2.4.1
INSTALL
Go to the documentation of this file.
1 /*!
2 
3 \page INSTALL INSTALL
4 
5 <strong>Contents:</strong>
6 
7 <ul>
8 <li>\ref quickstart</li>
9 <li>\ref requirements</li>
10 <li>\ref advanced</li>
11 <li>\ref installing</li>
12 <li>\ref documentation</li>
13 <li>\ref faq</li>
14 <li>\ref help</li>
15 </ul>
16 
17 \section quickstart Quick Start
18 
19 You can download a source distribution of %CVC3 from the
20 <a href="http://www.cs.nyu.edu/acsys/cvc3/download.html">CVC3 downloads
21 page</a>. Save the source archive as <code>cvc3.tar.gz</code> in the
22 directory of your choice and extract the contents using your favorite
23 archive program (you can use <code>tar xzvf cvc3.tar.gz</code> from a
24 terminal). This will create a directory containing the source of
25 %CVC3, normally called <code>cvc3-XXX</code>. In the following we will
26 denote the this directory as <code>$CVC3_SRC</code>. To build %CVC3,
27 open your favorite terminal program and run the following sequence of
28 commands
29 
30 <pre>
31  cd $CVC3_SRC
32  ./configure
33  make
34 </pre>
35 
36 If any part of the build process fails, please read the following section for more information.
37 
38 A successful build will create a library <code>libcvc3</code> in the
39 <code>$CVC3_SRC/lib</code> directory, and an executable
40 <code>cvc3</code> in the <code>$CVC3_SRC/bin</code> directory (these
41 are symbolic links to the actual files which are stored in
42 architecture- and configuration-dependent subdirectories). The
43 directory <code>$CVC3_SRC/test</code> contains an example program
44 using the %CVC3 library <code>libcvc3</code>. To try it out, run the
45 following commands in the terminal:
46 
47 <pre>
48  cd test
49  make
50  bin/test
51 </pre>
52 
53 By default, <code>make</code> will build optimized code, static
54 libraries, and a static executable. To build the "debug" version (much
55 slower but with more error checking) use the following configuration
56 command instead:
57 
58 <pre>
59  ./configure --with-build=debug
60 </pre>
61 
62 In case you prefer to build shared libraries (and thus a much smaller
63 executable), use the following configuration command:
64 
65 <pre>
66  ./configure --enable-dynamic
67 </pre>
68 
69 If you do choose to buld the shared libraries, you must set your
70 <code>LD_LIBRARY_PATH</code> environment variable to
71 <code>$CVC3_SRC/lib</code> before running %CVC3 or using the shared
72 libraries.
73 
74 Alternatively, these and other options can be changed by editing the
75 <code>Makefile.local</code> file after running
76 <code>configure</code>. However, be aware that re-running
77 <code>configure</code> will overwrite any changes you have made to
78 <code>Makefile.local</code>.
79 
80 \section requirements Requirements
81 
82 %CVC3 has the following build dependencies:
83 
84 <ul>
85 <li><a href="http://www.gnu.org/software/gcc/">GCC</a> version 3.0 or later</li>
86 <li><a href="http://www.gnu.org/software/bash/">Bash</a></li>
87 <li><a href="http://flex.sourceforge.net/">Flex</a></li>
88 <li><a href="http://www.gnu.org/software/bison/">Bison</a></li>
89 <li><a href="http://gmplib.org/">GMP</a> <em>(recommended)</em></li>
90 <li>A <a href="http://python.org/">Python</a> interpreter
91 <em>(optional, for Java support)</em></li>
92 <li>A <a href="http://java.sun.com/">Java</a> compiler
93 <em>(optional, for Java support)</em></li>
94 </ul>
95 
96 All of these tools are available from common package repositories
97 (e.g., Debian, Ubuntu, Red Hat, Cygwin).
98 
99 \section advanced Advanced Configuration
100 
101 The configure script checks for the components needed to build %CVC3.
102 If for some reason, the configure script is missing or doesn't run on
103 your platform, you can recreate it from <code>configure.ac</code> by
104 running <code>autoconf</code>.
105 
106 As the configure script runs, if something is not found, it
107 complains. configure looks for components in standard locations and
108 also uses several environment variables that you can set to help it
109 find things. In particular, you can set <code>CPPFLAGS</code> to
110 &quot;<code>-I $includeDir</code>&quot; if you have headers in a nonstandard
111 directory <code>$includeDir</code>, and <code>LDFLAGS</code> to
112 &quot;<code>-L $libDir</code>&quot; if you have libraries in a nonstandard
113 directory <code>$libDir</code>. Alternatively you can pass these
114 directories to the <code>configure</code> script using the following
115 command
116 
117 <pre>
118  ./configure --with-extra-includes=$includeDir --with-extra-libs=$libDir
119 </pre>
120 
121 Run <code>./configure --help</code> for a list of all such environment
122 variables and options.
123 
124 <h3>
125 GMP
126 </h3>
127 
128 One of the components %CVC3 depends on is the GNU Multiple Precision (GMP)
129 library. Many Unix-like distributions include gmp packages.
130 
131 If you do not have GMP installed or your installation does not work, we
132 recommend that you install it manually:
133 
134 1. Download the GMP source code from http://gmplib.org/
135 
136 2. Unpack the sources, and from the root-directory of the GMP source code, run
137 
138 <pre>
139  ./configure
140  make
141 </pre>
142 
143  On some Solaris machines, you may need to configure GMP with
144 
145 <pre>
146  ./configure ABI=32
147 </pre>
148 
149  to make the resulting GMP library compatible with the %CVC3
150  libraries. The reason for this is that the default ABI that gcc
151  chooses in %CVC3 compilation is not necessarily the default ABI
152  that the GMP configure script selects, and one of them may need to be
153  adjusted.
154 
155 3. Now, either install GMP system-wide (make install), or supply the
156  appropriate values for CPPFLAGS and LDFLAGS to the %CVC3 configure script.
157 
158 If for some reason, you do not want to use GMP, you can configure %CVC3 to use
159 native arithmetic by running:
160 
161 <pre>
162  ./configure --with-arith=native
163 </pre>
164 
165 If you compile %CVC3 with native arithmetic, it is possible that %CVC3 may fail
166 as the result of arithmetic overflow. If an overflow occurs, you will get
167 an error message and %CVC3 will abort.
168 
169 <h3>
170 Java interface
171 </h3>
172 
173 <em><strong>Note: The Java interface is experimental. The API may
174 change in future releases.</strong></em>
175 
176 To build the Java interface to %CVC3, use the
177 <code>--enable-java</code> configuration option. The configuration
178 script refers to the environment variables <code>JAVAC</code>,
179 <code>JAVAH</code>, <code>JAR</code>, and <code>CXX</code> to set up
180 the standard Java and C++ compiler commands. It refers to the
181 environment variable <code>JFLAGS</code> for default Java compiler
182 flags. It refers to the variable <code>javadir</code> for the
183 installation directory of the CVC3 Java library.
184 
185 The configuration options <code>--with-java-home</code> and
186 <code>--with-java-includes</code> can be used to specify the path to
187 the directories containing the JDK installation and JNI header files,
188 respectively.
189 
190 You must build %CVC3 as a dynamic library to use the Java
191 interface. For example, you might configure the build by running the
192 following in the top-level %CVC3 directory:
193 
194 <pre>
195  ./configure --enable-dynamic --enable-java
196 </pre>
197 
198 <b>Note:</b> The Java interface depends on the "build type" (e.g.,
199 "optimized", "debug") of %CVC3. If you choose to re-configure and
200 re-build %CVC3 with a different build type, you must run "make clean"
201 in the current directory and re-build the interface (cleaning and
202 rebuilding the entire %CVC3 package will suffice).
203 
204 <h4>
205 Using the Java interface
206 </h4>
207 
208 To access the library, you must add the file
209 <code>libcvc3-X.Y.Z.jar</code> (where "X.Y.Z" is the CVC3 version) to
210 the classpath (e.g., by setting the <code>CLASSPATH</code> environment
211 variable) and both <code>libcvc3.so</code> and
212 <code>libcvc3jni.so</code> to the runtime library path (e.g., by
213 setting the <code>LD_LIBRARY_PATH</code> environment variable
214 java.library.path JVM variable).
215 
216 For example, to compile the class Client.java:
217 
218 <pre>
219  javac -cp lib/libcvc3-X.Y.Z.jar Client.java
220 </pre>
221 
222 To run:
223 
224 <pre>
225  export LD_LIBRARY_PATH=/path/to/cvc3/libs
226  java -Djava.library.path=/path/to/cvc3/libs -cp lib/libcvc3-X.Y.Z.jar Client
227 </pre>
228 
229 <!-- !!! THE .NET INTERFACE IS NO LONGER SUPPORTED !!!
230 <h3>
231 .NET interface
232 </h3>
233 
234 <em><strong>Note: The .NET interface is experimental. The API may
235 change in future releases.</strong></em>
236 
237 A .NET interface to the %CVC3 library can be built using Visual Studio
238 2005 or later. To build the interface:
239 
240 <ol>
241 <li>The lexers and parsers for the supported input languages need to be generated outside of Visual Studio. This can be done in two ways:
242  <ul>
243  <li>Use the lexer/parser files created by a Cygwin build. It suffices to run Make in <code>src/parser</code>:
244 <pre>
245 ./configure
246 cd src/parser
247 make
248 </pre>
249 </li>
250 
251  <li>Run the script <code>make_parser.bat</code> in directory <code>src/parser</code> with the native Windows versions of <a href="http://gnuwin32.sourceforge.net/packages/flex.htm">Flex</a> and <a href="http://gnuwin32.sourceforge.net/packages/bison.htm">Bison</a>.</li>
252  </ul>
253 </li>
254 <li>Open the solution file <code>windows/cvc3.sln</code> in Visual Studio. The solution file contains the following projects (each with Debug/Release versions):
255  <ul>
256 <li>cvc3lib: the C++ %CVC3 library</li>
257 <li>cvc3: the %CVC3 command-line program</li>
258 <li>cvc3test: tests for cvc3lib</li>
259 <li>cvc3libcli: the .NET %CVC3 library</li>
260 <li>cvc3cli: a C# clone of the %CVC3 command-line program</li>
261 <li>cvc3testcli: tests for cvc3libcli</li>
262  </ul>
263 </li>
264 </ol>
265 
266 Each project can be built as usual with Visual Studio. Binaries will
267 be put in the folders <code>windows/release</code> (for Release
268 builds) and <code>windows/debug</code> (for Debug builds).
269 
270 For more information, see the file <code>windows/INSTALL</code>.
271 
272 <b>Note:</b> the .NET interface can only be used on Microsoft's CLR,
273 because Visual Studio produces <a
274 href="http://mono-project.com/CPlusPlus">mixed-mode assemblies</a>.
275 -->
276 
277 <h3>
278 Mac OS X
279 </h3>
280 
281 Mac OS X uses <code>DYLD_LIBRARY_PATH</code> in place of
282 <code>LD_LIBRARY_PATH</code>.
283 
284 On Intel Macs, by default, %CVC3 compiles in 32-bit or 64-bit mode
285 based on the compiler's default. If you want to build as one or
286 the other in particular (for example, to match your libgmp
287 installation), put CXXFLAGS=-m32 (and JREFLAGS=-d32, if you are
288 compiling the Java bindings) in the environment when you run
289 configure.
290 
291 To run regression testing (make regress), you'll need GNU time.
292 We suggest you install MacPorts (from macports.org) and then the
293 "gtime" package.
294 
295 You'll need also a libgmp installation. libgmp can be downloaded from
296 gmplib.org. If you install it in a nonstandard location (with
297 ./configure --prefix=...) you'll need to give this location to CVC3
298 when you configure it:
299 
300  ./configure --with-extra-includes=...--with-extra-libs=...
301 
302 or it may not find your installation of libgmp.
303 
304 <h3>
305  Cygwin
306 </h3>
307 
308 In order to use GMP on Cygwin, make sure the following packages are
309 installed: gmp, libgmp-devel, libgmp3, bison, flex, and make, as well
310 as standard UNIX tools.
311 
312 On Windows, it's common to have directory names with embedded spaces.
313 This can be problematic for the CVC3 build system. Therefore on
314 Cygwin we recommend symbolically linking to names without embedded
315 spaces, something like the following:
316 
317 <pre>
318  $ pwd
319  /home/ACSys Group
320  $ ln -s 'ACSys Group' /home/acsys
321  $ export HOME=/home/acsys
322  $ cd
323  $ pwd
324  /home/acsys
325  $ cd cvc3
326  $ ./configure --prefix=/home/acsys/cvc3.installation ...etc...
327 </pre>
328 
329 On Windows, Sun's JDK doesn't install the Java compiler "javac" into the
330 standard path for executables. If you want to build Java bindings,
331 you'll need to point CVC3 to it. Again using symbolic linking as above:
332 
333 <pre>
334  $ pwd
335  /home/acsys/cvc3
336  $ ln -s '/cygdrive/c/Program Files' /programs
337  $ ./configure --enable-java --with-java-home=/programs/Java/jdk1.6.0_16 ...
338 </pre>
339 
340 Such symbolic linking (and in general using cygwin full paths) may cause
341 problems with non-cygwin programs. In particular, if you have Windows
342 emacs installed (instead of cygwin's emacs), you have a version of etags
343 that may give errors at the end of the install. These errors (about source
344 files not existing when in fact they do) shouldn't break the build (make
345 won't complain and bomb out; it's just that these are at the very end of
346 the build, so it looks like they are causing problems) and can be safely
347 ignored.
348 
349 <h3>
350  <a name="64-bit Platforms">64-bit Platforms</a>
351 </h3>
352 
353 When building %CVC3 on 64-bit platforms, you must compile %CVC3 in the
354 same mode as any libraries it uses. For example, if GMP is compiled in
355 64-bit mode, then %CVC3 must compiled in 64-bit mode as well. The
356 configuration script will try to infer the correct compilation
357 settings. You can run <code>./config.guess</code> to see the default
358 platform type:
359 
360  $ ./config.guess
361  i686-pc-linux-gnu
362 
363 You can use the <code>--build</code> argument to
364 <code>configure</code> to override the default. For example, to
365 compile in 64-bit mode on a x86-64 CPU, you can use <code>./configure
366 --build=x86_64-pc-linux-gnu</code>.
367 
368 <h3>
369  LLVM
370 </h3>
371 
372 <em><strong>Note: Compiling %CVC3 with LLVM is not supported and
373 may cause runtime errors.</strong></em>
374 
375 To compile with LLVM, run configure with the options:
376 
377 <pre>
378 ./configure CXX=llvm-gcc LIBS='-lstdc++'
379 </pre>
380 
381 <h3>
382 Other Configuration Options
383 </h3>
384 
385 Other configuration options include where to install the results of
386 "make install" (see below), what type of build to use (optimized,
387 debug, gprof, or gcov), and whether to use static or dynamic
388 libraries. For help on these options, type
389 
390 <pre>
391 ./configure --help
392 </pre>
393 
394 configure creates the file Makefile.local which stores all of the
395 configuration information. If you want to customize your build
396 without re-running configure, or if you want to customize it in a way
397 that configure does not allow, you can do it by editing
398 Makefile.local. For example, you can build a debug, gprof version by
399 editing Makefile.local and setting OPTIMIZED to 0 and GPROF to 1 (by
400 default, gprof runs with an optimized executable). Note that for most
401 configuration options, the objects, libraries, and executables are
402 stored in a configuration-dependent directory, with only symbolic
403 links being stored in the main bin and lib directories. This allows
404 you to easily maintain multiple configurations and multiple platforms
405 using the same source tree.
406 
407 <h4>
408  Additional make options
409 </h4>
410 
411 To rebuild dependencies, type:
412 
413 <pre>
414  make depend
415 </pre>
416 
417 To remove just the executable or libraries in the current
418 configuration, type:
419 
420 <pre>
421  make spotty
422 </pre>
423 
424 To remove in addition all object files and makefile dependencies for
425 the current configuration, type:
426 
427 <pre>
428  make clean
429 </pre>
430 
431 To remove all files that are not part of the distribution (including
432 all object, library, and executables built for any configuration or
433 platform), type:
434 
435 <pre>
436  make distclean
437 </pre>
438 
439 To build a tarball distribution of the current source tree, type:
440 
441 <pre>
442  make dist
443 </pre>
444 
445 \section installing Installing CVC3
446 
447 To install %CVC3 system-wide, (assuming you have already run configure)
448 run:
449 
450 <pre>
451  make install
452 </pre>
453 
454 Installation depends on two configuration options: <code>prefix</code>
455 and <code>exec_prefix</code>. By default, both are set to
456 <code>/usr/local</code>, but these can be overridden by specifying the
457 correct arguments to configure or by editing
458 <code>Makefile.local</code>.
459 
460 Installation copies all necessary header files to
461 <code>$prefix/include/cvc3</code>. It installs the library
462 <code>libcvc3</code> in <code>$exec_prefix/lib</code> and the
463 executable <code>cvc3</code> in <code>$exec_prefix/bin</code>. By
464 default, a static library and executable are installed. If you want
465 to install shared library versions, configure for shared libraries as
466 described above.
467 
468 
469 \section documentation Documentation
470 
471 To build HTML documentation, run
472 
473 <pre>
474 
475  make doc
476 
477 </pre>
478 
479 Then open <code>doc/html/index.html</code> in your favorite browser.
480 
481 \section faq Frequently Asked Questions
482 
483 <h3>
484 Configuration Errors
485 </h3>
486 
487 <h4>
488 <code>libgmp.a is not found</code>
489 </h4>
490 
491 Make sure the GMP library is in your <code>LD_LIBRARY_PATH</code> and
492 <code>gmp.h</code> is in your <code>CPATH</code> (or use the
493 <code>--with-extra-lib</code> and <code>--with-extra-include</code>
494 arguments to <code>./configure</code>).
495 
496 If your paths are properly configured and you are compiling for a
497 64-bit architecture, you may have a 32/64-bit mismatch. Check the
498 binary type of the GMP library using the <code>file</code>
499 utility. For example, running <code>file</code> on a 32-bit Linux GMP
500 shared library will return:
501 
502 <pre>
503  $ file /usr/lib/libgmp.so.3.4.2
504  /usr/lib/libgmp.so.3.4.2: ELF 32-bit LSB shared object, Intel 80386, version 1 (SYSV), dynamically linked, stripped
505 </pre>
506 
507 You can use the <code>--build</code> arguments to
508 <code>./configure</code> to set the target binary type for %CVC3. For
509 example, <code>./configure --build=i686-linux-gnu</code> or
510 <code>./configure --build=x86_64-linux-gnu</code>.
511 
512 <h4>
513 <code>Unable to locate Java directories</code>
514 </h4>
515 
516 Set the <code>JAVA_HOME</code> environment variable or use the
517 <code>--with-java-home</code> argument to
518 <code>./configure</code>. Some typical <code>JAVA_HOME</code> settings
519 are as follows (where <em>X.Y.Z</em> is the version number of the installed
520 Java runtime).
521 
522 <table>
523 <tr>
524 <th> Platform </th><th> <code>JAVA_HOME</code> </th><th> Notes
525 </th></tr>
526 <tr>
527 <td> Debian/Ubuntu Linux </td>
528 <td> <code>/usr/lib/jvm/default-java</code> </td>
529 <td> Install the <code>default-jre</code> or
530 <code>default-jre-headless</code> package </td></tr>
531 <tr>
532 <td> Fedora Linux </td>
533 <td> <code>/usr/java/jre<em>X.Y.Z</em></code> </td>
534 <td> </td></tr>
535 <tr>
536 <td> Mac OS X </td>
537 <td> <code>/System/Library/Frameworks/JavaVM.framework/Home</code> </td>
538 <td> </td></tr>
539 <tr>
540 <td> Windows </td>
541 <td> <code>C:\\Program Files\\Java\\jdk<em>X.Y.Z</em></code> </td>
542 <td> </td></tr>
543 </table>
544 
545 <h3>
546 Runtime Errors (CVC3 library)
547 </h3>
548 
549 <h4>Segmentation fault when running a dynamically-linked executable.</h4>
550 
551 This can be caused by a mismatched "build type". The debug and
552 optimized version of the %CVC3 shared library are not binary
553 compatible. If you are linking against a debug version of the shared
554 library, you must define the symbol _CVC3_DEBUG_MODE during
555 compilation. E.g., add <code>-D_CVC3_DEBUG_MODE</code> to
556 <code>CXXARGS</code>.
557 
558 <h4>Fatal error: <code>Mis-handled the ref. counting</code></h4>
559 
560 This can be cause by a number of problems. Make sure that all <code>Expr</code>
561 objects are out of scope or have been manually deleted before deleting
562 the <code>ValidityChecker</code>.
563 
564 <h4>
565 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path</code>
566 </h4>
567 
568 The Java runtime was not able to find the %CVC3 JNI library. Use
569 <code>java -Djava.library.path=PATH_TO_CVC3JNI</code>, where
570 <code>PATH_TO_CVC3JNI</code> is the directory containing the file
571 <code>libcvc3jni.so</code>.
572 
573 <h4>
574 <code>Exception in thread "main" java.lang.UnsatisfiedLinkError: libcvc3jni.so.<em>x.y.z</em></code>
575 </h4>
576 
577 The Java runtime was not able to satisfy the link dependencies of the
578 %CVC3 JNI library. Make sure that the %CVC3 and GMP libraries are in
579 your <code>LD_LIBRARY_PATH</code>.
580 
581 If your paths are properly configured and you are compiling for a
582 64-bit architecture, you may have a 32/64-bit mismatch. Make sure the
583 JVM is running in the same mode as the %CVC3 library using the
584 <code>-d32</code> or <code>-d64</code> argument to <code>java</code>.
585 
586 <h4>
587 On Mac:
588 <code>terminate called after throwing an instance of 'CVC3::TypecheckException'</code>
589 </h4>
590 
591 This appears to be a bug in certain versions of GCC distributed by
592 Apple. Upgrade to XCode 3.1.2 or later (GCC version "4.0.1 (Apple
593 Inc. build 5490)") or configure with <code>CXXFLAGS=-01</code>.
594 
595 \section help Getting help
596 
597 If you find a problem with the instructions in this installation guide, please
598 send email to <a href="mailto:cvc-bugs@cs.nyu.edu">cvc-bugs@cs.nyu.edu</a>.
599 
600 */