CVC4 - User contributions [en]

Building CVC4 from source

2019-01-26T18:00:55Z

Noetzli:

'''IMPORTANT: The following instructions only apply to CVC4 1.6 and older. For newer versions, refer to INSTALL.md included with the source.
'''

To compile CVC4 from a source package you must do the following:
# Install antlr
# Configure cvc4
# Compile cvc4
# Install cvc4 [optional]

To do so run the following commands in the CVC4 directory:

cd contrib
./get-antlr-3.4
cd ..
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3
make
make check [recommended]
make install [optional]

Below are more details instructions about the various dependencies and options.

=Common make Options=
* "''make install''" will install into the "--prefix" option you gave to
the configure script (''/usr/local'' by default).
./configure --prefix=~/install_targets/cvc4 ...
make install
* '''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 [[#Examples_and_tutorials_are_not_built_or_installed|below]].

For more information about the build system itself (probably not
necessary for casual users), see the [[#Appendix:_Build_architecture|Appendix]] at the bottom of this
file.

=Common configure Options=
*'''--prefix=PREFIX''' install architecture-independent files in PREFIX (by default /usr/local)
*'''--with-build={production,debug,default,competition}'''
*'''--with-antlr-dir=PATH'''
*'''--with-cln'''/'''--with-gmp''' selects the numbers package to use by default ([[#Optional requirements]])
*'''--enable-static-binary''' build a fully statically-linked binary. (This is recommended for Mac OS X users that want to be able to use gdb.)
*'''ANTLR=PATH''' location of the antlr3 script
*'''--with-boost=DIR''' installation location of the boost libraries (most users will not need this)

See '''./configure --help''' for more.

=Build dependencies=

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)
*'''libantlr3c v3.2 or v3.4''' (ANTLR parser generator C support library)
*'''The Boost C++ base libraries'''
*'''MacPorts''' [highly recommended if on a Mac; see [[#MacPorts]]]

The hardest to obtain and install is the libantlr3c requirement, and
is explained [[#Installing libantlr3c: ANTLR parser generator C support library|next]].

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, compile and install
libantlr3c into your cvc4 directory as ''cvc4/antlr-3.4/''.
cd contrib
./get-antlr-3.4

CVC4 must be configured with the antlr library installation directory, '''--with-antlr-dir''', and an antlr executable script file, '''ANTLR'''. If libantlr3c was installed via get-antlr-3.4, the following configure line should suffice for CVC44
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

For 64 bit machines, libantlr3c needs to be configured with 64 bit explicitly
./configure --enable-64bit ...
The get-antlr-3.4 script makes a guess at whether the machine is 64 bit and adds the appropriate flag.
To force the script to compile 32 bit:
MACHINE_TYPE="x86" ./get-antlr-3.4
To force the script to compile 64 bit:
MACHINE_TYPE="x86_64" ./get-antlr-3.4

For a longer discussion, instructions for manual installation, and more in depth troubleshooting, see [[Developer's Guide#ANTLR3]].

==MacPorts==

On a Mac, it is '''highly''' recommended that you use 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. The mac-build script should set you up
with all requirements, and will tell you how to configure CVC4 when it
completes successfully.

==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/.

==Building on FreeBSD==
CVC4's build process currently makes extensive use of bash, sed, and other common *nix tools. It has recently come to our attention by Kostas Oikonomou that some of these are problematic outside of the GNU toolkit. Users of systems that do not assume GNU implementation like FreeBSD may experience issues building CVC4. Until we have a more permanent solution, here are Kostas Oikonomou's notes on how to modify CVC4's source to get it to compile on such systems:

0. export CONFIG_SHELL=/usr/local/bin/bash
Edit 'configure' to set # !/usr/local/bin/bash

1. configure --prefix=/opt/cvc4 --enable-gpl --with-readline CC=clang CXX=clang++ LDFLAGS=-L/usr/local/lib CPPFLAGS=-I/usr/local/include

2a. Edit src/mksubdirs, src/theory/{mkrewriter,mktheorytraits} to change
!#/bin/bash to !#/usr/local/bin/bash
Similarly for src/base/{mktags,mktagheaders}, src/expr/{mkexpr,mkkind,mkmetakind}.

2b. src/options/mkoptions: same as above, plus all occurrences of expr -> gexpr.

3. Edit src/main/util.cpp:

stack_t ss;
ss.ss_sp = (char *) malloc(SIGSTKSZ);

4. make -j2

5. Edit test/regress/run_regression to fix the bash business.

6. make check

7. sudo gmake install

=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|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 [[#Building_with_CUDD_(optional)|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 custom CLN installations (optional)==

One option for compiling against a custom CLN installation is to provide the CLN_LIBS and CLN_CFLAGS arguments at configuration. Supposing you installed cln into CLN_DIR the following provides the necessary locations of the header and linking information.
./configure <other arguments> --with-cln CLN_LIBS="-L<CLN_DIR>/lib -lcln" \
CLN_CFLAGS="-I<CLN_DIR>/include"

==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'''
*'''Java Development Kit''' ([http://www.antlr.org/wiki/pages/viewpage.action?pageId=728 required for ANTLR3])

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 and JDK requirements 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/.

Building CVC4 from source

2019-01-26T18:00:21Z

Noetzli:

'''IMPORTANT: These instructions only apply to CVC4 1.6 and older. For newer versions, refer to INSTALL.md included with the source.
'''

To compile CVC4 from a source package you must do the following:
# Install antlr
# Configure cvc4
# Compile cvc4
# Install cvc4 [optional]

To do so run the following commands in the CVC4 directory:

cd contrib
./get-antlr-3.4
cd ..
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3
make
make check [recommended]
make install [optional]

Below are more details instructions about the various dependencies and options.

=Common make Options=
* "''make install''" will install into the "--prefix" option you gave to
the configure script (''/usr/local'' by default).
./configure --prefix=~/install_targets/cvc4 ...
make install
* '''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 [[#Examples_and_tutorials_are_not_built_or_installed|below]].

For more information about the build system itself (probably not
necessary for casual users), see the [[#Appendix:_Build_architecture|Appendix]] at the bottom of this
file.

=Common configure Options=
*'''--prefix=PREFIX''' install architecture-independent files in PREFIX (by default /usr/local)
*'''--with-build={production,debug,default,competition}'''
*'''--with-antlr-dir=PATH'''
*'''--with-cln'''/'''--with-gmp''' selects the numbers package to use by default ([[#Optional requirements]])
*'''--enable-static-binary''' build a fully statically-linked binary. (This is recommended for Mac OS X users that want to be able to use gdb.)
*'''ANTLR=PATH''' location of the antlr3 script
*'''--with-boost=DIR''' installation location of the boost libraries (most users will not need this)

See '''./configure --help''' for more.

=Build dependencies=

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)
*'''libantlr3c v3.2 or v3.4''' (ANTLR parser generator C support library)
*'''The Boost C++ base libraries'''
*'''MacPorts''' [highly recommended if on a Mac; see [[#MacPorts]]]

The hardest to obtain and install is the libantlr3c requirement, and
is explained [[#Installing libantlr3c: ANTLR parser generator C support library|next]].

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, compile and install
libantlr3c into your cvc4 directory as ''cvc4/antlr-3.4/''.
cd contrib
./get-antlr-3.4

CVC4 must be configured with the antlr library installation directory, '''--with-antlr-dir''', and an antlr executable script file, '''ANTLR'''. If libantlr3c was installed via get-antlr-3.4, the following configure line should suffice for CVC44
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

For 64 bit machines, libantlr3c needs to be configured with 64 bit explicitly
./configure --enable-64bit ...
The get-antlr-3.4 script makes a guess at whether the machine is 64 bit and adds the appropriate flag.
To force the script to compile 32 bit:
MACHINE_TYPE="x86" ./get-antlr-3.4
To force the script to compile 64 bit:
MACHINE_TYPE="x86_64" ./get-antlr-3.4

For a longer discussion, instructions for manual installation, and more in depth troubleshooting, see [[Developer's Guide#ANTLR3]].

==MacPorts==

On a Mac, it is '''highly''' recommended that you use 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. The mac-build script should set you up
with all requirements, and will tell you how to configure CVC4 when it
completes successfully.

==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/.

==Building on FreeBSD==
CVC4's build process currently makes extensive use of bash, sed, and other common *nix tools. It has recently come to our attention by Kostas Oikonomou that some of these are problematic outside of the GNU toolkit. Users of systems that do not assume GNU implementation like FreeBSD may experience issues building CVC4. Until we have a more permanent solution, here are Kostas Oikonomou's notes on how to modify CVC4's source to get it to compile on such systems:

0. export CONFIG_SHELL=/usr/local/bin/bash
Edit 'configure' to set # !/usr/local/bin/bash

1. configure --prefix=/opt/cvc4 --enable-gpl --with-readline CC=clang CXX=clang++ LDFLAGS=-L/usr/local/lib CPPFLAGS=-I/usr/local/include

2a. Edit src/mksubdirs, src/theory/{mkrewriter,mktheorytraits} to change
!#/bin/bash to !#/usr/local/bin/bash
Similarly for src/base/{mktags,mktagheaders}, src/expr/{mkexpr,mkkind,mkmetakind}.

2b. src/options/mkoptions: same as above, plus all occurrences of expr -> gexpr.

3. Edit src/main/util.cpp:

stack_t ss;
ss.ss_sp = (char *) malloc(SIGSTKSZ);

4. make -j2

5. Edit test/regress/run_regression to fix the bash business.

6. make check

7. sudo gmake install

=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|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 [[#Building_with_CUDD_(optional)|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 custom CLN installations (optional)==

One option for compiling against a custom CLN installation is to provide the CLN_LIBS and CLN_CFLAGS arguments at configuration. Supposing you installed cln into CLN_DIR the following provides the necessary locations of the header and linking information.
./configure <other arguments> --with-cln CLN_LIBS="-L<CLN_DIR>/lib -lcln" \
CLN_CFLAGS="-I<CLN_DIR>/include"

==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'''
*'''Java Development Kit''' ([http://www.antlr.org/wiki/pages/viewpage.action?pageId=728 required for ANTLR3])

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 and JDK requirements 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/.

User Manual

2019-01-26T17:31:50Z

Noetzli: /* Building CVC4 from source */

This manual includes information on installing and using CVC4. It is a work in progress.

=Getting CVC4=

Both pre-compiled binaries and the source code for CVC4 are available for download from [http://cvc4.cs.stanford.edu/downloads/builds/ http://cvc4.cs.stanford.edu/downloads/builds/].

==Getting CVC4 binaries==
The most recent binaries can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-dbg/ Debug] binaries (statically linked)

==Building CVC4 from source==
[http://cvc4.cs.stanford.edu/downloads/builds/src/ Sources are available] from the same site as the binaries. The source-code is also available in the [https://github.com/CVC4/CVC4 CVC4 source repository].

For a comprehensive list of dependencies and more detailed build instructions see [[Building CVC4 from source]].

=Using the CVC4 binary=

Once installed, the CVC4 driver binary ("cvc4") can be executed to directly 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 [[#CVC4's native input language|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==

Successful exit is marked by the exit code 0. Most "normal errors" return a 1 as the exit code, but out of memory conditions, terminating signals, and other conditions can produce different (nonzero) 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.

''Note on previous versions:'' Up to version 1.2 of CVC4, exit status depended on the result ("sat" results caused an exit code of 10, "unsat" of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

=CVC4's input languages=

When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:

* [[CVC4's native language | CVC4's native language]]
* SMT-LIB 2.0 (see [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's SMT-LIB tutorial])
* SMT-LIB 1.0

CVC4 tries to automatically recognize the input language based on the file's extension: .cvc for CVC4's native language, .smt2 for SMT-LIB 2.0 and .smt for SMT-LIB 1.0. If the file extension does not match one of the previously mentioned ones you can specify the input language via the command line flag --lang. To see all language options type:
$ cvc4 --lang help

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.

=Supported Theories=
The following theories are currently fully supported
* Booleans
* Uninterpreted functions
* Arrays [with extensionality]
* Inductive datatypes
* Tuples and record types
* Fixed width bitvectors
* Linear mixed real integer arithmetic
** Integer division and modulus by integer constants is supported by the "--rewrite-divk" flag
* [[sets|Finite sets]]
CVC4 supports first-order quantification and theory combinations of the above theories.

The following theories are currently partially supported and are undergoing development:
* Strings

Theories with '''highly limited''' support:
* CVC4's non-linear real and non-linear integer arithmetic support is currently unlikely to satisfy a user's needs. The current support is for parsing, rewrites, and a very limited class of proofs of unsatisifiability. The class of proofs is what is provable by linear arithmetic where each monomial (e.g. "xxy") is treated as a unique variable.

=The CVC4 library interface (API)=

There are a number of examples of using CVC4 as a library distributed with the source code of the project. There are given in the "/examples" directory.

==Using CVC4 in a C++ project==

A basic C++ example for using cvc4 is given in the file [https://github.com/CVC4/CVC4/blob/master/examples/simple_vc_cxx.cpp /examples/simple_vc_cxx.cpp].
The file goes through the examples for the basic interaction with CVC4:
# Constructing an ExprManager em
# Constructing an SmtEngine w.r.t. em.
# Getting a copy of the Type for mathematical integers from em, em.integerType().
# Constructing new Expressions
## Integer variables x and y: Expr x = em.mkVar("x", integer);
## The rational constant 0: em.mkConst(Rational(0));
## Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
# Querying the SmtEngine whether or not a formula is valid.

More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.

To compile simple_vc_cxx.cpp, there are different build instructions for whether or not you are compiling against a version of CVC4 in a local build directory or one installed via "make install" into a directory $PREFIX.

* Local Build Directory: If you have build cvc4 via the "make" command before, you can compile simple_vc_cxx.cpp via "make examples". The executable will then be "./builds/examples/simple_vc_cxx".

$ make examples
[...]
$ ./builds/examples/simple_vc_cxx
Checking validity of formula ((x > 0) AND (y > 0)) => (((2 * x) + y) >= 3) with CVC4.
CVC4 should report VALID.
Result from CVC4 is: valid
* Installed Copy: If you have installed CVC4 via "make install" into the directory $PREFIX (which you can configure via "./configure --prefix=$PREFIX" you will need to modify lines 21-22.
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
:First, uncomment line 21 and comment out line 22. You may now
You can now compile and run by executing
g++ -I$PREFIX/include -L$PREFIX/lib -lcvc4 examples/simple_vc_cxx.cpp -o simple_vc_cxx
./simple_vc_cxx
:You may need to add $PREFIX/lib is LD_LIBRARY_PATH or the equivalent.

==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===

=Advanced features=

This section describes some features of CVC4 of interest to developers and advanced users.

==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==

[to do]

==Changing the output language==

[to do]

==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).

==Parallel solving==

'''[Builds not ported to Stanford yet]''' The most recent binaries with support for parallel solving can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-dbg/ Debug] binaries (statically linked)

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 the theory of inductive
datatypes. This limitation will be addressed in a future release.

See more details and examples in the [[Tutorials#Parallel_Solving|tutorial]].

==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.

User Manual

2019-01-26T04:34:09Z

Noetzli: /* Getting CVC4 binaries */

This manual includes information on installing and using CVC4. It is a work in progress.

=Getting CVC4=

Both pre-compiled binaries and the source code for CVC4 are available for download from [http://cvc4.cs.stanford.edu/downloads/builds/ http://cvc4.cs.stanford.edu/downloads/builds/].

==Getting CVC4 binaries==
The most recent binaries can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-dbg/ Debug] binaries (statically linked)

==Building CVC4 from source==
[http://cvc4.cs.stanford.edu/downloads/builds/src/ Sources are available] from the same site as the binaries. The source-code is also available in the [https://github.com/CVC4/CVC4 CVC4 source repository].

To build CVC4 from source the following steps are required. After downloading the source files first install antlr by running the following script in the CVC4 contrib directory:
cd contrib
./get-antlr-3.4

The next step is to configure CVC4:
cd ..
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

And then finally compile it:
make
make check [recommended]
make install [optional]

For a comprehensive list of dependencies and more detailed build instructions see [[Building CVC4 from source]].

=Using the CVC4 binary=

Once installed, the CVC4 driver binary ("cvc4") can be executed to directly 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 [[#CVC4's native input language|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==

Successful exit is marked by the exit code 0. Most "normal errors" return a 1 as the exit code, but out of memory conditions, terminating signals, and other conditions can produce different (nonzero) 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.

''Note on previous versions:'' Up to version 1.2 of CVC4, exit status depended on the result ("sat" results caused an exit code of 10, "unsat" of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

=CVC4's input languages=

When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:

* [[CVC4's native language | CVC4's native language]]
* SMT-LIB 2.0 (see [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's SMT-LIB tutorial])
* SMT-LIB 1.0

CVC4 tries to automatically recognize the input language based on the file's extension: .cvc for CVC4's native language, .smt2 for SMT-LIB 2.0 and .smt for SMT-LIB 1.0. If the file extension does not match one of the previously mentioned ones you can specify the input language via the command line flag --lang. To see all language options type:
$ cvc4 --lang help

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.

=Supported Theories=
The following theories are currently fully supported
* Booleans
* Uninterpreted functions
* Arrays [with extensionality]
* Inductive datatypes
* Tuples and record types
* Fixed width bitvectors
* Linear mixed real integer arithmetic
** Integer division and modulus by integer constants is supported by the "--rewrite-divk" flag
* [[sets|Finite sets]]
CVC4 supports first-order quantification and theory combinations of the above theories.

The following theories are currently partially supported and are undergoing development:
* Strings

Theories with '''highly limited''' support:
* CVC4's non-linear real and non-linear integer arithmetic support is currently unlikely to satisfy a user's needs. The current support is for parsing, rewrites, and a very limited class of proofs of unsatisifiability. The class of proofs is what is provable by linear arithmetic where each monomial (e.g. "xxy") is treated as a unique variable.

=The CVC4 library interface (API)=

There are a number of examples of using CVC4 as a library distributed with the source code of the project. There are given in the "/examples" directory.

==Using CVC4 in a C++ project==

A basic C++ example for using cvc4 is given in the file [https://github.com/CVC4/CVC4/blob/master/examples/simple_vc_cxx.cpp /examples/simple_vc_cxx.cpp].
The file goes through the examples for the basic interaction with CVC4:
# Constructing an ExprManager em
# Constructing an SmtEngine w.r.t. em.
# Getting a copy of the Type for mathematical integers from em, em.integerType().
# Constructing new Expressions
## Integer variables x and y: Expr x = em.mkVar("x", integer);
## The rational constant 0: em.mkConst(Rational(0));
## Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
# Querying the SmtEngine whether or not a formula is valid.

More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.

To compile simple_vc_cxx.cpp, there are different build instructions for whether or not you are compiling against a version of CVC4 in a local build directory or one installed via "make install" into a directory $PREFIX.

* Local Build Directory: If you have build cvc4 via the "make" command before, you can compile simple_vc_cxx.cpp via "make examples". The executable will then be "./builds/examples/simple_vc_cxx".

$ make examples
[...]
$ ./builds/examples/simple_vc_cxx
Checking validity of formula ((x > 0) AND (y > 0)) => (((2 * x) + y) >= 3) with CVC4.
CVC4 should report VALID.
Result from CVC4 is: valid
* Installed Copy: If you have installed CVC4 via "make install" into the directory $PREFIX (which you can configure via "./configure --prefix=$PREFIX" you will need to modify lines 21-22.
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
:First, uncomment line 21 and comment out line 22. You may now
You can now compile and run by executing
g++ -I$PREFIX/include -L$PREFIX/lib -lcvc4 examples/simple_vc_cxx.cpp -o simple_vc_cxx
./simple_vc_cxx
:You may need to add $PREFIX/lib is LD_LIBRARY_PATH or the equivalent.

==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===

=Advanced features=

This section describes some features of CVC4 of interest to developers and advanced users.

==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==

[to do]

==Changing the output language==

[to do]

==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).

==Parallel solving==

'''[Builds not ported to Stanford yet]''' The most recent binaries with support for parallel solving can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-dbg/ Debug] binaries (statically linked)

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 the theory of inductive
datatypes. This limitation will be addressed in a future release.

See more details and examples in the [[Tutorials#Parallel_Solving|tutorial]].

==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.

User Manual

2019-01-26T04:33:27Z

Noetzli: /* Getting CVC4 binaries */

This manual includes information on installing and using CVC4. It is a work in progress.

=Getting CVC4=

Both pre-compiled binaries and the source code for CVC4 are available for download from [http://cvc4.cs.stanford.edu/downloads/builds/ http://cvc4.cs.stanford.edu/downloads/builds/].

==Getting CVC4 binaries==
The most recent binaries can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-dbg/ Debug] binaries (statically linked)

'''[Not ported to Stanford yet]''' To install CVC4 on an Ubuntu Machine follow the instructions below. First add the CVC4 repository to /etc/apt/sources.list by inserting the following two lines at the end of the file:
# CVC4 repository
deb http://cvc4.cs.nyu.edu/debian/ unstable/
deb-src http://cvc4.cs.nyu.edu/debian/ unstable/

To run CVC4 as a binary you only need the first line but to use the library API you will also need the source package.
Make sure to update the respository list by running:

sudo apt-get update

Now you can simply install CVC4 as you would any other piece of sofware using the command:
sudo apt-get install cvc4

If you want to use CVC4 as a library also install the following packages: libcvc4-dev, and libcvc4-parser-dev.

==Building CVC4 from source==
[http://cvc4.cs.stanford.edu/downloads/builds/src/ Sources are available] from the same site as the binaries. The source-code is also available in the [https://github.com/CVC4/CVC4 CVC4 source repository].

To build CVC4 from source the following steps are required. After downloading the source files first install antlr by running the following script in the CVC4 contrib directory:
cd contrib
./get-antlr-3.4

The next step is to configure CVC4:
cd ..
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

And then finally compile it:
make
make check [recommended]
make install [optional]

For a comprehensive list of dependencies and more detailed build instructions see [[Building CVC4 from source]].

=Using the CVC4 binary=

Once installed, the CVC4 driver binary ("cvc4") can be executed to directly 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 [[#CVC4's native input language|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==

Successful exit is marked by the exit code 0. Most "normal errors" return a 1 as the exit code, but out of memory conditions, terminating signals, and other conditions can produce different (nonzero) 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.

''Note on previous versions:'' Up to version 1.2 of CVC4, exit status depended on the result ("sat" results caused an exit code of 10, "unsat" of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

=CVC4's input languages=

When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:

* [[CVC4's native language | CVC4's native language]]
* SMT-LIB 2.0 (see [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's SMT-LIB tutorial])
* SMT-LIB 1.0

CVC4 tries to automatically recognize the input language based on the file's extension: .cvc for CVC4's native language, .smt2 for SMT-LIB 2.0 and .smt for SMT-LIB 1.0. If the file extension does not match one of the previously mentioned ones you can specify the input language via the command line flag --lang. To see all language options type:
$ cvc4 --lang help

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.

=Supported Theories=
The following theories are currently fully supported
* Booleans
* Uninterpreted functions
* Arrays [with extensionality]
* Inductive datatypes
* Tuples and record types
* Fixed width bitvectors
* Linear mixed real integer arithmetic
** Integer division and modulus by integer constants is supported by the "--rewrite-divk" flag
* [[sets|Finite sets]]
CVC4 supports first-order quantification and theory combinations of the above theories.

The following theories are currently partially supported and are undergoing development:
* Strings

Theories with '''highly limited''' support:
* CVC4's non-linear real and non-linear integer arithmetic support is currently unlikely to satisfy a user's needs. The current support is for parsing, rewrites, and a very limited class of proofs of unsatisifiability. The class of proofs is what is provable by linear arithmetic where each monomial (e.g. "xxy") is treated as a unique variable.

=The CVC4 library interface (API)=

There are a number of examples of using CVC4 as a library distributed with the source code of the project. There are given in the "/examples" directory.

==Using CVC4 in a C++ project==

A basic C++ example for using cvc4 is given in the file [https://github.com/CVC4/CVC4/blob/master/examples/simple_vc_cxx.cpp /examples/simple_vc_cxx.cpp].
The file goes through the examples for the basic interaction with CVC4:
# Constructing an ExprManager em
# Constructing an SmtEngine w.r.t. em.
# Getting a copy of the Type for mathematical integers from em, em.integerType().
# Constructing new Expressions
## Integer variables x and y: Expr x = em.mkVar("x", integer);
## The rational constant 0: em.mkConst(Rational(0));
## Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
# Querying the SmtEngine whether or not a formula is valid.

More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.

To compile simple_vc_cxx.cpp, there are different build instructions for whether or not you are compiling against a version of CVC4 in a local build directory or one installed via "make install" into a directory $PREFIX.

* Local Build Directory: If you have build cvc4 via the "make" command before, you can compile simple_vc_cxx.cpp via "make examples". The executable will then be "./builds/examples/simple_vc_cxx".

$ make examples
[...]
$ ./builds/examples/simple_vc_cxx
Checking validity of formula ((x > 0) AND (y > 0)) => (((2 * x) + y) >= 3) with CVC4.
CVC4 should report VALID.
Result from CVC4 is: valid
* Installed Copy: If you have installed CVC4 via "make install" into the directory $PREFIX (which you can configure via "./configure --prefix=$PREFIX" you will need to modify lines 21-22.
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
:First, uncomment line 21 and comment out line 22. You may now
You can now compile and run by executing
g++ -I$PREFIX/include -L$PREFIX/lib -lcvc4 examples/simple_vc_cxx.cpp -o simple_vc_cxx
./simple_vc_cxx
:You may need to add $PREFIX/lib is LD_LIBRARY_PATH or the equivalent.

==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===

=Advanced features=

This section describes some features of CVC4 of interest to developers and advanced users.

==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==

[to do]

==Changing the output language==

[to do]

==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).

==Parallel solving==

'''[Builds not ported to Stanford yet]''' The most recent binaries with support for parallel solving can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-dbg/ Debug] binaries (statically linked)

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 the theory of inductive
datatypes. This limitation will be addressed in a future release.

See more details and examples in the [[Tutorials#Parallel_Solving|tutorial]].

==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.

User Manual

2017-02-08T18:26:52Z

Noetzli:

This manual includes information on installing and using CVC4. It is a work in progress.

=Getting CVC4=

Both pre-compiled binaries and the source code for CVC4 are available for download from [http://cvc4.cs.stanford.edu/downloads/builds/ http://cvc4.cs.stanford.edu/downloads/builds/].

==Getting CVC4 binaries==
The most recent binaries can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-dbg/ Debug] binaries (statically linked)
* [http://cvc4.cs.stanford.edu/downloads/builds/debian/ Debian] packages

'''[Not ported to Stanford yet]''' To install CVC4 on an Ubuntu Machine follow the instructions below. First add the CVC4 repository to /etc/apt/source.list by inserting the following two lines at the end of the file:
# CVC4 repository
deb http://cvc4.cs.nyu.edu/debian/ unstable/
deb-src http://cvc4.cs.nyu.edu/debian/ unstable/

To run CVC4 as a binary you only need the first line but to use the library API you will also need the source package.
Make sure to update the respository list by running:

sudo apt-get update

Now you can simply install CVC4 as you would any other piece of sofware using the command:
sudo apt-get install cvc4

If you want to use CVC4 as a library also install the following packages: libcvc4-dev, and libcvc4-parser-dev.

==Building CVC4 from source==
[http://cvc4.cs.stanford.edu/downloads/builds/src/ Sources are available] from the same site as the binaries. The source-code is also available in the [https://github.com/CVC4/CVC4 CVC4 source repository].

To build CVC4 from source the following steps are required. After downloading the source files first install antlr by running the following script in the CVC4 contrib directory:
cd contrib
./get-antlr-3.4

The next step is to configure CVC4:
cd ..
./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3

And then finally compile it:
make
make check [recommended]
make install [optional]

For a comprehensive list of dependencies and more detailed build instructions see [[Building CVC4 from source]].

=Using the CVC4 binary=

Once installed, the CVC4 driver binary ("cvc4") can be executed to directly 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 [[#CVC4's native input language|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==

Successful exit is marked by the exit code 0. Most "normal errors" return a 1 as the exit code, but out of memory conditions, terminating signals, and other conditions can produce different (nonzero) 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.

''Note on previous versions:'' Up to version 1.2 of CVC4, exit status depended on the result ("sat" results caused an exit code of 10, "unsat" of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

=CVC4's input languages=

When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:

* [[CVC4's native language | CVC4's native language]]
* SMT-LIB 2.0 (see [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's SMT-LIB tutorial])
* SMT-LIB 1.0

CVC4 tries to automatically recognize the input language based on the file's extension: .cvc for CVC4's native language, .smt2 for SMT-LIB 2.0 and .smt for SMT-LIB 1.0. If the file extension does not match one of the previously mentioned ones you can specify the input language via the command line flag --lang. To see all language options type:
$ cvc4 --lang help

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.

=Supported Theories=
The following theories are currently fully supported
* Booleans
* Uninterpreted functions
* Arrays [with extensionality]
* Inductive datatypes
* Tuples and record types
* Fixed width bitvectors
* Linear mixed real integer arithmetic
** Integer division and modulus by integer constants is supported by the "--rewrite-divk" flag
* [[sets|Finite sets]]
CVC4 supports first-order quantification and theory combinations of the above theories.

The following theories are currently partially supported and are undergoing development:
* Strings

Theories with '''highly limited''' support:
* CVC4's non-linear real and non-linear integer arithmetic support is currently unlikely to satisfy a user's needs. The current support is for parsing, rewrites, and a very limited class of proofs of unsatisifiability. The class of proofs is what is provable by linear arithmetic where each monomial (e.g. "xxy") is treated as a unique variable.

=The CVC4 library interface (API)=

There are a number of examples of using CVC4 as a library distributed with the source code of the project. There are given in the "/examples" directory.

==Using CVC4 in a C++ project==

A basic C++ example for using cvc4 is given in the file [https://github.com/CVC4/CVC4/blob/master/examples/simple_vc_cxx.cpp /examples/simple_vc_cxx.cpp].
The file goes through the examples for the basic interaction with CVC4:
# Constructing an ExprManager em
# Constructing an SmtEngine w.r.t. em.
# Getting a copy of the Type for mathematical integers from em, em.integerType().
# Constructing new Expressions
## Integer variables x and y: Expr x = em.mkVar("x", integer);
## The rational constant 0: em.mkConst(Rational(0));
## Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
# Querying the SmtEngine whether or not a formula is valid.

More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.

To compile simple_vc_cxx.cpp, there are different build instructions for whether or not you are compiling against a version of CVC4 in a local build directory or one installed via "make install" into a directory $PREFIX.

* Local Build Directory: If you have build cvc4 via the "make" command before, you can compile simple_vc_cxx.cpp via "make examples". The executable will then be "./builds/examples/simple_vc_cxx".

$ make examples
[...]
$ ./builds/examples/simple_vc_cxx
Checking validity of formula ((x > 0) AND (y > 0)) => (((2 * x) + y) >= 3) with CVC4.
CVC4 should report VALID.
Result from CVC4 is: valid
* Installed Copy: If you have installed CVC4 via "make install" into the directory $PREFIX (which you can configure via "./configure --prefix=$PREFIX" you will need to modify lines 21-22.
//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
:First, uncomment line 21 and comment out line 22. You may now
You can now compile and run by executing
g++ -I$PREFIX/include -L$PREFIX/lib -lcvc4 examples/simple_vc_cxx.cpp -o simple_vc_cxx
./simple_vc_cxx
:You may need to add $PREFIX/lib is LD_LIBRARY_PATH or the equivalent.

==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===

=Advanced features=

This section describes some features of CVC4 of interest to developers and advanced users.

==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==

[to do]

==Changing the output language==

[to do]

==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).

==Parallel solving==

'''[Builds not ported to Stanford yet]''' The most recent binaries with support for parallel solving can be downloaded from our Nightly Builds pages:
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-opt/ Optimized] binaries (statically linked)
* [http://cvc4.cs.nyu.edu/cvc4-builds/portfolio-x86_64-linux-dbg/ Debug] binaries (statically linked)

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 the theory of inductive
datatypes. This limitation will be addressed in a future release.

See more details and examples in the [[Tutorials#Parallel_Solving|tutorial]].

==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.

How do I... ?

2017-02-01T18:33:21Z

Noetzli: /* Dealing with the services on the Church server */

This page is a repository for questions about working with CVC4. If you have a question, please add it here. If you have an answer, please add the answer to the [[Developer's Guide]], or another wiki page, and then link to it from here.

=Dealing with ANTLR3=

*[[Developer's Guide#ANTLR3|...get ANTLR3 to work?]]

=Dealing with the build process=

*[[Developer's Guide#Working with multiple, concurrent build profiles|...build a different CVC4 build profile than the "current" one?]]

=Dealing with Subversion=

*[[Developer's Guide#Accessing CVC4's repository|...check out CVC4 from the repository?]]
*[[Developer's Guide#Repository access from Eclipse|...access the repository from Eclipse?]]
*[[Developer's Guide#Browsing the repository|...browse CVC4 sources online?]]
*[[Developer's Guide#Accessing CVC4's repository|...update my working copy to the newest committed version?]]
*[[Developer's Guide#Working with files and directories|...rename a file or directory?]]
*[[Developer's Guide#Reverting a file in a working directory|...revert changes in my working directory?]]
*[[Developer's Guide#Reverting a commit|...revert changes that have already been committed to the repository?]]
*[[Developer's Guide#Accessing CVC4's repository|...see what I've changed in my working copy?]]
*[[Developer's Guide#Resolving conflicts in a working directory|...resolve a conflict?]]
*[[Developer's Guide#Creating a branch|...create a branch?]]
*[[Developer's Guide#Merging a branch back to the trunk|...merge a branch back into the trunk?]]
*[[Developer's Guide#Symbolically tagging a version|...symbolically tag a version?]]
*[[Developer's Guide#Marking a file as executable in Subversion|...make Subversion recognize that a file should be executable?]]

=Dealing with the source tree=

*[[Developer's Guide#Adding a new Theory|...add support for a new theory to CVC4?]]
*[[Developer's Guide#Adding source directories|...add a new source directory to the tree?]]
*[[Developer's Guide#Adding source and header files|...add a new source file to the tree?]]
*[[Developer's Guide#Adding copyrighted sources|...add a new source file/directory to the tree from another project (under different copyright)?]]
*[[Developer's Guide#update-copyright.pl|...update the copyright information at the top of each file in the tree?]]

=Dealing with tests=

*[[Developer's Guide#Unit testing|...add a new unit test?]]
*[[Developer's Guide#System testing|...add a new system regression?]]
*[[Developer's Guide#Regression testing|...add a new regression?]]
*[[Developer's Guide#Debugging unit tests|...attach a debugger to unit tests?]]
*[[Developer's Guide#Test rebuilding|...avoid rebuilding all tests after trivial code changes to the library?]]
*[[Developer's Guide#Compile-time errors in unit tests|...deal with this strange compile error on my unit test?]]

=Dealing with code coverage=

*[[Developer's Guide#Visualizing code coverage|...visualize code coverage?]]

=Dealing with performance=

*[[Developer's Guide#Profiling|...profile CVC4?]]

=Dealing with the main CVC4 driver program=

*[[Developer's Guide#Command-line options|...add a new command-line option?]]

=Dealing with code reviews=

*[[Developer's Guide#Code reviews|...perform a code review?]]

=Dealing with the services on the Church server=

'''NOTE: This information is deprecated but we might want to review it.'''

*[[Using SSL with Church|...encrypt my communications with the Church web server?]]
*[[Newswire#Adding items to the newswire|...add an item to Church's CVC4 newswire?]]
*[[Developer Meeting Minutes#Adding meeting minutes to the wiki|...add CVC4 meeting minutes to the wiki?]]
*[[Developer Meeting Minutes#Adding electronic notes to meeting minutes|...add electronic notes to CVC4 meeting minutes?]]
*[[Running a CVC4 Meeting|...run a CVC4 meeting?]]

= Dealing with adding a new theory =
For information on how to add a new theory see [[How to write a theory in CVC4]].

How do I... ?

2017-02-01T18:32:58Z

Noetzli: /* Dealing with the services on the Church server */

This page is a repository for questions about working with CVC4. If you have a question, please add it here. If you have an answer, please add the answer to the [[Developer's Guide]], or another wiki page, and then link to it from here.

=Dealing with ANTLR3=

*[[Developer's Guide#ANTLR3|...get ANTLR3 to work?]]

=Dealing with the build process=

*[[Developer's Guide#Working with multiple, concurrent build profiles|...build a different CVC4 build profile than the "current" one?]]

=Dealing with Subversion=

*[[Developer's Guide#Accessing CVC4's repository|...check out CVC4 from the repository?]]
*[[Developer's Guide#Repository access from Eclipse|...access the repository from Eclipse?]]
*[[Developer's Guide#Browsing the repository|...browse CVC4 sources online?]]
*[[Developer's Guide#Accessing CVC4's repository|...update my working copy to the newest committed version?]]
*[[Developer's Guide#Working with files and directories|...rename a file or directory?]]
*[[Developer's Guide#Reverting a file in a working directory|...revert changes in my working directory?]]
*[[Developer's Guide#Reverting a commit|...revert changes that have already been committed to the repository?]]
*[[Developer's Guide#Accessing CVC4's repository|...see what I've changed in my working copy?]]
*[[Developer's Guide#Resolving conflicts in a working directory|...resolve a conflict?]]
*[[Developer's Guide#Creating a branch|...create a branch?]]
*[[Developer's Guide#Merging a branch back to the trunk|...merge a branch back into the trunk?]]
*[[Developer's Guide#Symbolically tagging a version|...symbolically tag a version?]]
*[[Developer's Guide#Marking a file as executable in Subversion|...make Subversion recognize that a file should be executable?]]

=Dealing with the source tree=

*[[Developer's Guide#Adding a new Theory|...add support for a new theory to CVC4?]]
*[[Developer's Guide#Adding source directories|...add a new source directory to the tree?]]
*[[Developer's Guide#Adding source and header files|...add a new source file to the tree?]]
*[[Developer's Guide#Adding copyrighted sources|...add a new source file/directory to the tree from another project (under different copyright)?]]
*[[Developer's Guide#update-copyright.pl|...update the copyright information at the top of each file in the tree?]]

=Dealing with tests=

*[[Developer's Guide#Unit testing|...add a new unit test?]]
*[[Developer's Guide#System testing|...add a new system regression?]]
*[[Developer's Guide#Regression testing|...add a new regression?]]
*[[Developer's Guide#Debugging unit tests|...attach a debugger to unit tests?]]
*[[Developer's Guide#Test rebuilding|...avoid rebuilding all tests after trivial code changes to the library?]]
*[[Developer's Guide#Compile-time errors in unit tests|...deal with this strange compile error on my unit test?]]

=Dealing with code coverage=

*[[Developer's Guide#Visualizing code coverage|...visualize code coverage?]]

=Dealing with performance=

*[[Developer's Guide#Profiling|...profile CVC4?]]

=Dealing with the main CVC4 driver program=

*[[Developer's Guide#Command-line options|...add a new command-line option?]]

=Dealing with code reviews=

*[[Developer's Guide#Code reviews|...perform a code review?]]

=Dealing with the services on the Church server=

'''NOTE: This information is deprecated but we might want to review some of this information.'''

*[[Using SSL with Church|...encrypt my communications with the Church web server?]]
*[[Newswire#Adding items to the newswire|...add an item to Church's CVC4 newswire?]]
*[[Developer Meeting Minutes#Adding meeting minutes to the wiki|...add CVC4 meeting minutes to the wiki?]]
*[[Developer Meeting Minutes#Adding electronic notes to meeting minutes|...add electronic notes to CVC4 meeting minutes?]]
*[[Running a CVC4 Meeting|...run a CVC4 meeting?]]

= Dealing with adding a new theory =
For information on how to add a new theory see [[How to write a theory in CVC4]].