Difference between revisions of "User Manual"
(→CVC4's native input language) |
(First draft of intro section) |
||
| Line 2: | Line 2: | ||
It is a work in-progress. | It is a work in-progress. | ||
| + | |||
| + | = What is CVC4? = | ||
| + | |||
| + | CVC4 is the last of a long line of SMT solvers that started with SVC and includes CVC, CVC-lite and CVC3. | ||
| + | |||
| + | Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories. The current built-in theories are the theories of: | ||
| + | |||
| + | * equality over free (aka uninterpreted) function and predicate symbols, | ||
| + | * real and integer linear arithmetic (with some support for non-linear arithmetic), | ||
| + | * bit vectors, | ||
| + | * arrays, | ||
| + | * tuples, | ||
| + | * records, | ||
| + | * user-defined inductive data types. | ||
| + | |||
| + | CVC4 checks whether a given formula <math>\phi</math> is valid in the built-in theories under a given set <math>\Gamma</math> of assumptions. More precisely, it checks whether | ||
| + | |||
| + | <math>\Gamma\models_T \phi</math> | ||
| + | |||
| + | that is, whether <math>\phi</math> is a logical consequence of the union <math>T</math> of the built-in theories and the set of formulas <math>\Gamma</math>. | ||
| + | |||
| + | Roughly speaking, when <math>\phi</math> is universal and all the formulas in <math>\Gamma</math> are existential (i.e., when <math>\phi</math> and <math>\Gamma</math> contain at most universal, respectively existential, quantifiers), CVC4 is in fact a decision procedure: it is always guaranteed (modulo bugs and memory limits) to return a correct "valid" or "invalid" answer. In all other cases, CVC4 is deductively sound but incomplete: it will never say that an invalid formula is valid but it may either never return or give up and return "unknown" in some cases when <math>\Gamma \models_T \phi</math>. | ||
| + | |||
| + | When CVC3 returns "valid" it can return a formal proof of the validity of $\phi$ under the logical context $\Gamma$, together with the subset $\Gamma'$ of $\Gamma$ used in the proof, such that $\Gamma'\models_T \phi$. | ||
| + | |||
| + | When CVC3 returns "invalid" it can return, in the current terminology, both a counter-example to $\phi$'s validity under $\Gamma$ and a counter-model. Both a counter-example and a counter-models are a set $\Delta$ of additional formulas consistent with $\Gamma$ in $T$, but entailing the negation of $\phi$. In formulas: | ||
| + | $\Gamma \cup \Delta \not\models_T \mathit{false}$ and $\Gamma \cup \Delta \models_T \lnot \phi$. | ||
| + | |||
| + | The difference is that a counter-model is given as a set of equations providing a concrete assignment of values for the free symbols in $\Gamma$ and $\phi$ (see QUERY for more details). | ||
| + | |||
| + | CVC3 can be used in two modes: as a library or as a command-line executable (implemented as a command-line interface to the library). Interfaces to the library are available in C/C++, Java and .NET. This manual mainly describes the command-line interface on a unix-type platform. | ||
=Obtaining and compiling CVC4= | =Obtaining and compiling CVC4= | ||
Revision as of 15:41, 15 October 2012
This manual includes lots of information about how to use CVC4.
It is a work in-progress.
Contents
- 1 What is CVC4?
- 2 Obtaining and compiling CVC4
- 2.1 Obtaining binary packages
- 2.2 Obtaining sources
- 2.3 Building from source
- 3 Using the CVC4 binary
- 4 CVC4's native input language
- 5 CVC4's support for the SMT-LIB language
- 6 The CVC4 library interface (API)
- 7 Upgrading from CVC3 to CVC4
- 8 Useful command-line options
- 9 Dumping API calls or preprocessed output
- 10 Changing the output language
- 11 Proof support
- 12 Portfolio solving
- 13 Emacs support
What is CVC4?
CVC4 is the last of a long line of SMT solvers that started with SVC and includes CVC, CVC-lite and CVC3.
Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories. The current built-in theories are the theories of:
- equality over free (aka uninterpreted) function and predicate symbols,
- real and integer linear arithmetic (with some support for non-linear arithmetic),
- bit vectors,
- arrays,
- tuples,
- records,
- user-defined inductive data types.
CVC4 checks whether a given formula 
is valid in the built-in theories under a given set 
of assumptions. More precisely, it checks whether
that is, whether is a logical consequence of the union 
of the built-in theories and the set of formulas .
Roughly speaking, when is universal and all the formulas in are existential (i.e., when and contain at most universal, respectively existential, quantifiers), CVC4 is in fact a decision procedure: it is always guaranteed (modulo bugs and memory limits) to return a correct "valid" or "invalid" answer. In all other cases, CVC4 is deductively sound but incomplete: it will never say that an invalid formula is valid but it may either never return or give up and return "unknown" in some cases when .
When CVC3 returns "valid" it can return a formal proof of the validity of $\phi$ under the logical context $\Gamma$, together with the subset $\Gamma'$ of $\Gamma$ used in the proof, such that $\Gamma'\models_T \phi$.
When CVC3 returns "invalid" it can return, in the current terminology, both a counter-example to $\phi$'s validity under $\Gamma$ and a counter-model. Both a counter-example and a counter-models are a set $\Delta$ of additional formulas consistent with $\Gamma$ in $T$, but entailing the negation of $\phi$. In formulas: $\Gamma \cup \Delta \not\models_T \mathit{false}$ and $\Gamma \cup \Delta \models_T \lnot \phi$.
The difference is that a counter-model is given as a set of equations providing a concrete assignment of values for the free symbols in $\Gamma$ and $\phi$ (see QUERY for more details).
CVC3 can be used in two modes: as a library or as a command-line executable (implemented as a command-line interface to the library). Interfaces to the library are available in C/C++, Java and .NET. This manual mainly describes the command-line interface on a unix-type platform.
Obtaining and compiling CVC4
Obtaining binary packages
Binary packages are available for CVC4.
Obtaining sources
Sources are available from the same site as the binaries.
Building from source
Quick-start instructions
./configure make make check [optional but a good idea!]
(To build from a repository checkout, see below.)
You can then "make install" to install in the prefix you gave to the configure script (/usr/local by default). You should run "make check" before installation to ensure that CVC4 has been built correctly. In particular, GCC version 4.5.1 seems to have a bug in the optimizer that results in incorrect behavior (and wrong results) in many builds. This is a known problem for Minisat, and since Minisat is at the core of CVC4, a problem for CVC4. "make check" easily detects this problem (by showing a number of FAILed test cases). It is ok if the unit tests aren't run as part of "make check", but all system tests and regression tests should pass without incident.
To build API documentation, use "make doc". Documentation is produced under builds/doc/ but is not installed by "make install".
Examples and tutorials are not installed with "make install." See below.
For more information about the build system itself (probably not necessary for casual users), see the Appendix at the bottom of this file.
Build dependences
The following tools and libraries are required to run CVC4. Versions given are minimum versions; more recent versions should be compatible.
- GNU C and C++ (gcc and g++), reasonably recent versions
- GNU Make
- GNU Bash
- GMP v4.2 (GNU Multi-Precision arithmetic library)
- MacPorts [only if on a Mac; see below]
- libantlr3c v3.2 or v3.4 (ANTLR parser generator C support library)
- The Boost C++ base libraries
The hardest to obtain and install is the libantlr3c requirement, so that one is explained next.
On a Mac, you need to additionally install MacPorts (see http://www.macports.org/). Doing so is easy. Then, simply run the script contrib/mac-build, which installs a few ports from the MacPorts repository, then compiles and installs antlr3c using the get-antlr-3.4 script (as described next). The mac-build script should set you up with all requirements, and will tell you how to configure CVC4 when it completes successfully.
If "make" is non-GNU on your system, make sure to invoke "gmake" (or whatever GNU Make is installed as). If your usual shell is not Bash, the configure script should auto-correct this. If it does not, you'll see strange shell syntax errors, and you may need to explicitly set SHELL or CONFIG_SHELL to the location of bash on your system.
Installing libantlr3c: ANTLR parser generator C support library
For libantlr3c, you can use the convenience script in contrib/get-antlr-3.4 in the source distribution---this will download, patch, and install libantlr3c. On a 32-bit machine, or if you have difficulty building libantlr3c (or difficulty getting CVC4 to link against it later), you may need to remove the --enable-64bit part in the script. (If you're curious, manual instructions are available.)
Installing the Boost C++ base libraries
A Boost package is available on most Linux distributions; check yours for a package named something like libboost-dev or boost-devel. There are a number of additional Boost packages in some distributions, but this "basic" one should be sufficient for building CVC4.
Should you want to install Boost manually, or to learn more about the Boost project, please visit http://www.boost.org/.
Optional requirements
None of these is required, but can improve CVC4 as described below:
- Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
- Optional: CLN v1.3 or newer (Class Library for Numbers)
- Optional: CUDD v2.4.2 or newer (Colorado University Decision Diagram package)
- Optional: GNU Readline library (for an improved interactive experience)
- Optional: The Boost C++ threading library (libboost_thread)
- Optional: CxxTest unit testing framework
SWIG is necessary to build the Java API (and of course a JDK is necessary, too). SWIG 1.x won't work; you'll need 2.0, and the more recent the better. On Mac, we've seen SWIG segfault when generating CVC4 language bindings; version 2.0.8 or higher is recommended to avoid this. See Language bindings below for build instructions.
CLN is an alternative multiprecision arithmetic package that can offer better performance and memory footprint than GMP. CLN is covered by the GNU General Public License, version 3; so if you choose to use CVC4 with CLN support, you are licensing CVC4 under that same license. (Usually CVC4's license is more permissive than GPL is; see the file COPYING in the CVC4 source distribution for details.) Please visit http://www.ginac.de/CLN/ for more details about CLN.
CUDD is a decision diagram package that changes the behavior of the CVC4 arithmetic solver in some cases; it may or may not improve the arithmetic solver's performance. See below for instructions on obtaining and building CUDD.
The GNU Readline library is optionally used to provide command editing, tab completion, and history functionality at the CVC prompt (when running in interactive mode). Check your distribution for a package named "libreadline-dev" or "readline-devel" or similar.
The Boost C++ threading library (often packaged independently of the Boost base library) is needed to run CVC4 in "portfolio" (multithreaded) mode. Check your distribution for a package named "libboost-thread-dev" or similar.
CxxTest is necessary to run CVC4's unit tests (included with the distribution). Running these is not really required for users of CVC4; "make check" will skip unit tests if CxxTest isn't available, and go on to run the extensive system- and regression-tests in the source tree. However, if you're interested, you can download CxxTest at http://cxxtest.com/ .
Building with CUDD (optional)
CUDD, if desired, must be installed delicately. The CVC4 configure script attempts to auto-detect the locations and names of CUDD headers and libraries the way that the Fedora RPMs install them, the way that our NYU-provided Debian packages install them, and the way they exist when you download and build the CUDD sources directly. If you install from Fedora RPMs or our Debian packages, the process should be completely automatic, since the libraries and headers are installed in a standard location. If you download the sources yourself, you need to build them in a special way. Fortunately, the "contrib/build-cudd-2.4.2-with-libtool.sh" script in the CVC4 source tree does exactly what you need: it patches the CUDD makefiles to use libtool, builds the libtool libraries, then reverses the patch to leave the makefiles as they were. Once you run this script on an unpacked CUDD 2.4.2 source distribution, then CVC4's configure script should pick up the libraries if you provide --with-cudd-dir=/PATH/TO/CUDD/SOURCES.
If you want to force linking to CUDD, provide --with-cudd to the configure script; this makes it a hard requirement rather than an optional add-on.
The NYU-provided Debian packaging of CUDD 2.4.2 and CUDD 2.5.0 are here (along with the CVC4 Debian packages):
deb http://cvc4.cs.nyu.edu/debian/ unstable/
On Debian (and Debian-derived distributions like Ubuntu), you only need to drop that one line in your /etc/apt/sources.list file, then install with your favorite package manager.
The Debian source package "cudd", available from the same repository, includes a diff of all changes made to cudd makefiles.
Language bindings
There are several options available for using CVC4 from the API.
First, CVC4 offers a complete and flexible API for manipulating expressions, maintaining a stack of assertions, and checking satisfiability, and related things. The C++ libraries (libcvc4.so and libcvc4parser.so) and required headers are installed normally via a "make install". This API is also available from Java (via CVC4.jar and libcvc4jni.so) by configuring with --enable-language-bindings=java. You'll also need SWIG 2.0 installed (and you might need to help configure find it if you installed it in a nonstandard place with --with-swig-dir=/path/to/swig/installation). You may also need to give the configure script the path to your Java headers (in particular, jni.h). You might do so with (for example):
./configure --enable-language-bindings=java \
JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h> and link against libcvc4compat.so) that attempts to maintain source-level backwards-compatibility with the CVC3 C++ API. The compatibility library is built by default, and --enable-language-bindings=java enables the Java compatibility library (CVC4compat.jar and libcvc4compatjni.so). --enable-language-bindings=c enables the C compatibility library (#include <cvc4/bindings/compat/c/c_interface.h> and link against libcvc4bindings_c_compat.so), and if you want both C and Java bindings, use --enable-language-bindings=c,java. These compatibility language bindings do NOT require SWIG.
The examples/ directory in the source distribution includes some basic examples (the "simple vc" and "simple vc compat" family of examples) of all these interfaces.
In principle, since we use SWIG to generate the native Java API, we could support other languages as well. However, using CVC4 from other languages is not supported, nor expected to work, at this time. If you're interested in helping to develop, maintain, and test a language binding, please contact us via the users' mailing list at cvc-users@cs.nyu.edu.
Building CVC4 from a repository checkout
The following tools and libraries are additionally required to build CVC4 from from a repository checkout rather than from a prepared source tarball.
- Automake v1.11
- Autoconf v2.61
- Libtool v2.2
- ANTLR3 v3.2 or v3.4
First, use "./autogen.sh" to create the configure script. Then proceed as normal for any distribution tarball. The parsers are pre-generated for the tarballs, but don't exist in the repository; hence the extra ANTLR3 requirement to generate the source code for the parsers, when building from the repository.
Examples and tutorials are not built or installed
Examples are not built by "make" or "make install". See examples/README in the source distribution for information on what to find in the examples/ directory, as well as information about building and installing them.
Appendix: Build architecture
The build system is generated by automake, libtool, and autoconf. It is somewhat nonstandard, though, which (for one thing) requires that GNU Make be used. If you ./configure in the top-level source directory, the objects will actually all appear in builds/${arch}/${build_id}. This is to allow multiple, separate builds in the same place (e.g., an assertions-enabled debugging build alongside a production build), without changing directories at the shell. The "current" build is maintained, and you can still use (e.g.) "make -C src/main" to rebuild objects in just one subdirectory.
You can also create your own build directory inside or outside of the source tree and configure from there. All objects will then be built in that directory, and you'll ultimately find the "cvc4" binary in src/main/, and the libraries under src/ and src/parser/.
Using the CVC4 binary
The CVC4 driver binary ("cvc4"), once installed, can be executed directly to enter into interactive mode:
$ cvc4 cvc4 1.0 assertions:off CVC4>
You can then enter commands into CVC4 interactively:
CVC4> OPTION "incremental"; CVC4> OPTION "produce-models"; CVC4> TRANSFORM 25*25; 625 CVC4> x, y : INT; CVC4> QUERY x = y; invalid CVC4> COUNTERMODEL; x : INT = -1; y : INT = 0; CVC4> ASSERT x >= 0; CVC4> QUERY x = y; invalid CVC4> COUNTERMODEL; x : INT = 0; y : INT = 1; CVC4>
The above example shows two useful options, incremental and produce-models.
- The incremental option allows you to issue multiple QUERY (or CHECKSAT) commands, and allows the use of the PUSH and POP commands. Without this option, CVC4 optimizes itself for a single QUERY or CHECKSAT command (though you may issue any number of ASSERT commands). The incremental option may also be given by passing the -i command line option to CVC4.
- The produce-models option allows you to query the model (here, with the COUNTERMODEL command) after an "invalid" QUERY (or "satisfiable" CHECK-SAT). Without it, CVC4 doesn't do the bookkeeping necessary to support model generation. The produce-models option may also be given by passing the -m command line option to CVC4.
So, if you invoke CVC4 with -im, you don't need to pass those options at all:
$ cvc4 -im cvc4 1.0 assertions:off CVC4> x, y : INT; CVC4> QUERY x = y; invalid CVC4> COUNTERMODEL; x : INT = -1; y : INT = 0; CVC4> ASSERT x >= 0; CVC4> QUERY x = y; invalid CVC4> COUNTERMODEL; x : INT = 0; y : INT = 1; CVC4>
By default, CVC4 operates in CVC-language mode. If you enter something that looks like SMT-LIB, it will suggest that you use the "--lang smt" command-line option for SMT-LIB mode:
CVC4> (declare-fun x () Int) Parse Error: <shell>:1.7: In CVC4 presentation language mode, but SMT-LIB format detected. Use --lang smt for SMT-LIB support. CVC4>
Verbosity
CVC4 has various levels of verbosity. By default, CVC4 is pretty quiet, only reporting serious warnings and notices. If you're curious about what it's doing, you can pass CVC4 the -v option:
$ cvc4 -v file.smt2 Invoking: (set-logic AUFLIRA) Invoking: (set-info :smt-lib-version 2.000000) Invoking: (set-info :category "crafted") Invoking: (set-info :status unsat) Invoking: (declare-fun x () Real) etc...
For even more verbosity, you can pass CVC4 an additional -v:
$ cvc4 -vv file.smt2 Invoking: (set-logic AUFLIRA) Invoking: (set-info :smt-lib-version 2.000000) Invoking: (set-info :category "crafted") Invoking: (set-info :status unsat) Invoking: (declare-fun x () Real) etc... expanding definitions... constraining subtypes... applying substitutions... simplifying assertions... doing static learning... etc...
Internally, verbosity is just an integer value. It starts at 0, and with every -v on the command line it is incremented; with every -q, decremented. It can also be set directly. From CVC language:
CVC4> OPTION "verbosity" 2;
Or from SMT-LIB language:
CVC4> (set-option :verbosity 2)
Getting statistics
Statistics can be dumped on exit (both normal and abnormal exits) with the --statistics command line option.
$ cvc4 --statistics foo.smt2 sat sat::decisions, 0 sat::propagations, 3 sat::starts, 1 theory::uf::TheoryUF::functionTermsCount, 2 theory::uf::TheoryUF::mergesCount, 2 theory::uf::TheoryUF::termsCount, 6 theory<THEORY_UF>::propagations, 1 driver::filename, foo.smt2 driver::sat/unsat, sat driver::totalTime, 0.02015373 [many others]
Many statistics name-value pairs follow, one comma-separated pair per line.
Exit status
The exit status of CVC4 depends on the last QUERY or CHECK-SAT. If you wish to call CVC4 from a program (e.g., a shell script) and care only about the satisfiability or validity of a single formula, you can pass the -q option (as described above, under verbosity) and check the exit code. With -q, CVC4 should not produce any output unless it encounters a fatal error.
QUERY asks a validity question, and CHECK-SAT a satisfiability question, and these are dual problems; hence the terminology is different, but really "sat" and "invalid" are the same internally, as are "unsat" and "valid":
| Solver's last result | Exit code | Notes |
|---|---|---|
| sat or invalid | 10 | |
| unsat or valid | 20 | |
| unknown | 0 | could be for any reason: time limit exceeded, no memory, incompleteness.. |
| no result | 0 | no query or check-sat command issued |
| parse errors | 0 (in interactive mode) 1 (otherwise) | see below |
| other errors | 1 (usually) | see below |
Most "normal errors" return a 1 as the exit code, but out of memory conditions, and others, can produce different exit codes. In interactive mode, parse errors are ignored and the next line read; so in interactive mode, you may see an exit code of 0 even in the presence of such an error.
In SMT-LIB mode, an SMT-LIB command script that sets its status via "set-info :status" also affects the exit code. So, for instance, the following SMT-LIB script returns an exit code of 10 even though it contains no "check-sat" command:
(set-logic QF_UF) (set-info :status sat) (exit)
Without the "set-info," it would have returned an exit code of 0.
CVC4's native input language
Test
CVC4's support for the SMT-LIB language
SMT-LIB compliance
Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0 standard (http://smtlib.org/). However, when parsing SMT-LIB input, certain default settings don't match what is stated in the official standard. To make CVC4 adhere more strictly to the standard, use the "--smtlib" command-line option. Even with this setting, CVC4 is somewhat lenient; some non-conforming input may still be parsed and processed.
The CVC4 library interface (API)
Using CVC4 in a C++ project
Using CVC4 from Java
The compatibility interface
Upgrading from CVC3 to CVC4
Features not supported by CVC4 (yet)
Type Correctness Conditions (TCCs)
Type Correctness Conditions (TCCs), and the checking of such, are not supported by CVC4 1.0. Thus, a function defined only on integers can be applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain, but may produce strange results. For example:
f : INT -> INT; ASSERT f(1/3) = 0; ASSERT f(2/3) = 1; CHECKSAT; % sat COUNTEREXAMPLE; % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
CVC3 can be used to produce TCCs for this input (with the +dump-tcc option). The TCC can be checked by CVC3 or another solver. (CVC3 can also check TCCs while solving with +tcc.)
If you were using the text interfaces of CVC3
The native language of all solvers in the CVC family, referred to as the "presentation language," has undergone some revisions for CVC4. The most notable is that CVC4 does _not_ add counterexample assertions to the current assertion set after a SAT/INVALID result. For example:
x, y : INT; ASSERT x = 1 OR x = 2; ASSERT y = 1 OR y = 2; ASSERT x /= y; CHECKSAT; % sat QUERY x = 1; % invalid QUERY x = 2; % invalid
Here, CVC4 responds "invalid" to the second and third queries, because each has a counterexample (x=2 is a counterexample to the first, and x=1 is a counterexample to the second). However, CVC3 will respond with "valid" to one of these two, as the first query (the CHECKSAT) had the side-effect of locking CVC3 into one of the two cases; the later queries are effectively querying the counterexample that was found by the first. CVC4 removes this side-effect of the CHECKSAT and QUERY commands.
CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not support decimals.
CVC4 does not have support for the IS_INTEGER predicate.
If you were using the library ("in-memory") interface of CVC3
If you were using CVC3 from C
If you were using CVC3 from Java
Useful command-line options
Statistics
Statistics can be dumped on exit (both normal and abnormal exits) with the --statistics command line option.
Time and resource limits
CVC4 can be made to self-timeout after a given number of milliseconds. Use the --tlimit command line option to limit the entire run of CVC4, or use --tlimit-per to limit each individual query separately. Preprocessing time is not counted by the time limit, so for some large inputs which require aggressive preprocessing, you may notice that --tlimit does not work very well. If you suspect this might be the case, you can use "-vv" (double verbosity) to see what CVC4 is doing.
Time-limited runs are not deterministic; two consecutive runs with the same time limit might produce different results (i.e., one may time out and responds with "unknown", while the other completes and provides an answer). To ensure that results are reproducible, use --rlimit or --rlimit-per. These options take a "resource count" (presently, based on the number of SAT conflicts) that limits the search time. A word of caution, though: there is no guarantee that runs of different versions of CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different features enabled, or for different architectures) will interpret the resource count in the same manner.
CVC4 does not presently have a way to limit its memory use; you may opt to run it from a shell after using "ulimit" to limit the size of the heap.
Dumping API calls or preprocessed output
Changing the output language
Proof support
CVC4 1.0 has limited support for proofs, and they are disabled by default. (Run the configure script with --enable-proof to enable proofs). Proofs are exported in LFSC format and are limited to the propositional backbone of the discovered proof (theory lemmas are stated without proof in this release).
Portfolio solving
If enabled at configure-time (./configure --with-portfolio), a second CVC4 binary will be produced ("pcvc4"). This binary has support for running multiple instances of CVC4 in different threads. Use --threads=N to specify the number of threads, and use --thread0="options for thread 0" --thread1="options for thread 1", etc., to specify a configuration for the threads. Lemmas are *not* shared between the threads by default; to adjust this, use the --filter-lemma-length=N option to share lemmas of N literals (or smaller). (Some lemmas are ineligible for sharing because they include literals that are "local" to one thread.)
Currently, the portfolio **does not work** with quantifiers or with the theory of inductive datatypes. These limitations will be addressed in a future release.
Emacs support
For a suggestion of editing CVC4 source code with emacs, see the file contrib/editing-with-emacs. For a CVC language mode (the native input language for CVC4), see contrib/cvc-mode.el.
