Revision as of 11:44, 24 October 2012 (view source) Taking (Talk | contribs) m (→‎Source repository) ← Older edit		Latest revision as of 10:31, 26 January 2019 (view source) Noetzli (Talk | contribs) (→‎Building CVC4 from source)
(169 intermediate revisions by 8 users not shown)
Line 1:		Line 1:
−	This manual includes lots of information about how to use CVC4.	+	This manual includes information on installing and using CVC4. It is a work in progress.
−	It is a work in-progress.	+	=Getting CVC4=
−	= What is 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/].
−	CVC4 is the last of a long line of SMT solvers that started with SVC and includes CVC, CVC-Lite and CVC3.	+	==Getting CVC4 binaries==
−	Technically, it is an automated validity checker for a many-sorted (i.e., typed) first-order logic with built-in theories.	+	The most recent binaries can be downloaded from our Nightly Builds pages:
−	The current built-in theories are the theories of:	+	* [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)
−	* equality over free (aka uninterpreted) function and predicate symbols,	+	==Building CVC4 from source==
−	* real and integer linear arithmetic (with some support for non-linear arithmetic),	+	[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].
−	* bit vectors,	+
−	* arrays,	+
−	* tuples,	+
−	* records,	+
−	* user-defined inductive data types.	+
−	CVC4 checks whether a given formula <math>\phi</math> is valid in the built-in theories under a given set <math>\Gamma</math> of assumptions, a ''context''.	+	For a comprehensive list of dependencies and more detailed build instructions see [[Building CVC4 from source]].
−	More precisely, it checks whether	+
−		+
−	<center>	+
−	<math>\Gamma\models_T \phi</math>	+
−	</center>	+
−		+
−	that is, whether <math>\phi</math> is a logical consequence in <math>T</math> of the set of formulas <math>\Gamma</math>, where <math>T</math> is the union of CVC4's built-in theories.	+
−		+
−	Roughly speaking, when <math>\phi</math> is a universal formula and <math>\Gamma</math> is a set of existential formulas (i.e., when <math>\phi</math> and <math>\Gamma</math> contain at most universal, respectively existential, quantifiers), CVC4 is a decision procedure:	+
−	it is guaranteed (modulo bugs and memory limits) to return a correct "valid" or "invalid" answer eventually.	+
−	In all other cases, CVC4 is deductively sound but incomplete:	+
−	it will never say that an invalid formula is valid,	+
−	but it may either never return or give up and return "unknown" for some formulas.	+
−		+
−	Currently, when CVC4 returns "valid" for a query formula <math>\phi</math> under a context <math>\Gamma</math>	+
−	it provides no evidence to back its claim.	+
−	Future versions will also return a ''proof certificate'',	+
−	a formal proof that <math>\Gamma'\models_T \phi</math> for some subset <math>\Gamma'</math> of <math>\Gamma</math>.	+
−		+
−	When CVC4 returns "invalid" it can return	+
−	both a ''counter-example'' to <math>\phi</math>'s validity under the context <math>\Gamma</math> and a ''counter-model''.	+
−	Both a counter-example and a counter-model are a set <math>\Delta</math> of additional formulas consistent with <math>\Gamma</math> in <math>T</math>, but entailing the negation of <math>\phi</math>.	+
−	Formally:	+
−		+
−	<center>	+
−	<math>\Gamma \cup \Delta \not\models_T \mathit{false}</math>	+
−	and	+
−	<math>\Gamma \cup \Delta \models_T \lnot \phi</math>.	+
−	</center>	+
−		+
−	The difference is that a counter-model is given as a set of equations providing a concrete assignment of values for the free symbols in <math>\Gamma</math> and <math>\phi</math>	+
−	(see the section on [[#CVC4's native input language|CVC4's native input language]] for more details).	+
−		+
−	=Obtaining and compiling CVC4=	+
−		+
−	CVC4 is distributed in the following ways:	+
−	* [[#Obtaining_binary_packages|Binary packages]]	+
−	* [[#Obtaining_source_packages|Source packages]]	+
−	* [[#Source_repository|Source repository checkout]]	+
−		+
−	==Obtaining binary packages==	+
−		+
−	[http://cvc4.cs.nyu.edu/builds/ Binary packages are available] for CVC4.	+
−		+
−	==Obtaining source packages==	+
−		+
−	[http://cvc4.cs.nyu.edu/builds/src/ Sources are available] from the same site as the binaries.	+
−		+
−	==Source repository==	+
−	The [http://cvc4.cs.nyu.edu/builds/src/ CVC4 source repository] is currently hosted by [http://cims.nyu.edu/ CIMS] and requires a CIMS account. Please contact a member of the development team for access. Please see the additional instructions for [[#Building_CVC4 from_a_repository_checkout]] here.	+
−		+
−	==Building from source==	+
−		+
−	===Quick-start instructions===	+
−	To compile from a source package:	+
−	# Install antlr	+
−	# Configure cvc4	+
−	# Compile cvc4	+
−	# Install cvc4 [optional]	+
−	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]	+
−		+
−	(To build from a repository checkout, see [[#Building_CVC4_from_a_repository_checkout|below]].)	+
−		+
−	===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.	+
−		+
−	===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-antlr3.4	+
−	To force the script to compile 64 bit:	+
−	MACHINE_TYPE="x86_64" ./get-antlr3.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/.	+
−		+
−	===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 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/.	+
	=Using the CVC4 binary=		=Using the CVC4 binary=
−	The CVC4 driver binary ("cvc4"), once installed, can be executed directly to enter into interactive mode:	+	Once installed, the CVC4 driver binary ("cvc4") can be executed to directly enter into interactive mode:
	$ cvc4		$ cvc4
Line 451:		Line 130:
	==Exit status==		==Exit status==
−	The exit status of CVC4 depends on the ''last'' QUERY or CHECK-SAT.  If you wish to call CVC4 from a program (e.g., a shell script) and care only about the satisfiability or validity of a single formula, you can pass the ''-q'' option (as described [[#Verbosity|above, under verbosity]]) and check the exit code.  With ''-q'', CVC4 should not produce any output unless it encounters a fatal error.	+	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.
−	QUERY asks a validity question, and CHECK-SAT a satisfiability question, and these are dual problems; hence the terminology is different, but really "sat" and "invalid" are the same internally, as are "unsat" and "valid":	+	''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.
−	<table border="1">	+	=CVC4's input languages=
−	<tr><th>Solver's last result</th><th>Exit code</th><th>Notes</th></tr>	+
−	<tr><td>'''sat''' or '''invalid'''</td><td>10</td></tr>	+
−	<tr><td>'''unsat''' or '''valid'''</td><td>20</td></tr>	+
−	<tr><td>'''unknown'''</td><td>0</td><td>could be for any reason: time limit exceeded, no memory, incompleteness..</td></tr>	+
−	<tr><td>''no result''</td><td>0</td><td>no query or check-sat command issued</td></tr>	+
−	<tr><td>parse errors</td><td>0 (in interactive mode)<br/>1 (otherwise)</td><td>see below</td></tr>	+
−	<tr><td>other errors</td><td>1 (usually)</td><td>see below</td></tr>	+
−	</table>	+
−	Most "normal errors" return a 1 as the exit code, but out of memory conditions, and others, can produce different exit codes.  In interactive mode, parse errors are ignored and the next line read; so in interactive mode, you may see an exit code of 0 even in the presence of such an error.	+	When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:
−	In SMT-LIB mode, an SMT-LIB command script that sets its status via "set-info :status" also affects the exit code.  So, for instance, the following SMT-LIB script returns an exit code of 10 even though it contains no "check-sat" command:	+	* [[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
−	(set-logic QF_UF)	+	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:
−	(set-info :status sat)	+	$ cvc4 --lang help
−	(exit)	+
−	Without the "set-info," it would have returned an exit code of 0.	+	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.
−	=CVC4's native input language=	+	=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 input language consists of a sequence of symbol declarations and commands, each followed by a semicolon (<code>;</code>).	+	The following theories are currently partially supported and are undergoing development:
		+	* Strings
−	Any text after the first occurrence of a percent character and to the end of the current line is a comment:	+	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.
−	%%% This is a presentation language comment	+	=The CVC4 library interface (API)=
−	== Type System ==	+	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.
−	CVC4's type system includes a set of built-in types which can be expanded with additional user-defined types.	+	==Using CVC4 in a C++ project==
−	The type system consists of ''first-order'' types, ''subtypes'' of first-order types, and ''higher-order'' types, all of which are interpreted as sets.	+	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].
−	For convenience, we will sometimes identify below the interpretation of a type with the type itself.	+	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.
−	First-order types consist of basic types and structured types. The basic types are <math>\mathrm{BOOLEAN}</math>, <math>\mathrm{REAL}</math>, <math>\mathrm{BITVECTOR}(n)</math> for all <math>n > 0</math>, as well as user-defined basic types (also called uninterpreted types).
−	The structured types are array, tuple, record types, and ML-style user-defined (inductive) datatypes.
−	Subtypes include the built-in subtype <math>\mathrm{INT}</math> of <math>\mathrm{REAL}</math> and are covered in the [[#Subtypes|Subtypes]] section.
−	Function types are the only higher-order types.	+	More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.
−	More precisely, they are just second-order types	+
−	since function symbols in CVC4, both built-in and user-defined, can take as argument or return only values of	+
−	a first-order type.	+
−	=== Basic Types ===	+	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.
−	==== The BOOLEAN Type ====	+	* 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".
−	The <math>\mathrm{BOOLEAN}</math> type is interpreted as the two-element set of Boolean values	+	$ make examples
−	<math>\{\mathrm{TRUE},\; \mathrm{FALSE}\}</math>.	+	[...]
		+	$ ./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.
−	Note that CVC4's use of this type differs from CVC3's where <math>\mathrm{BOOLEAN}</math> is used only as the type of formulas, but not as value type. CVC3 follows the two-tiered structure of classical first-order logic that distinguishes between formulas and terms, and allows terms to occur in formulas but not vice versa (with the exception of the IF-THEN-ELSE construct).
−	CVC4 drops the distinction between terms and formulas and defines the latter just as terms of type <math>\mathrm{BOOLEAN}</math>. As such, formulas can occur as subterms of possibly non-Boolean terms.
−
−	Example:
−
−	[To do]
−
−	==== The REAL Type ====
−
−	The <math>\mathrm{REAL}</math> type is interpreted as the set of real numbers.
−
−	Note that these are the (infinite precision) mathematical reals,
−	not the floating point numbers.
−	Support for floating point types is planned for future versions.
−
−	x, y : REAL;
−	QUERY (( x <= y ) AND ( y <= x )) => ( x = y );
−
−	==== The INT Type ====
−
−	The <math>\mathrm{INT}</math> type is interpreted as the set of integer numbers.  INT is a subtype of REAL.
−
−	Note that these are the (infinite precision) mathematical integers,
−	not Java/C/... int. (For this, see [[#Bitvectors]].)
−
−	x, y : INT;
−	QUERY ((2 * x + 4 * y <= 1) AND ( y >= x)) => (x <= 0);
−
−	==== Bit Vector Types ====
−
−	For every positive integer <math>n</math>, the type <math>\mathrm{BITVECTOR}(n)</math> is interpreted as the set of all bit vectors of size <math>n</math>.
−	A rich set of bit vector operators is supported.
−
−	==== User-defined Basic Types ====
−
−	Users can define new basic types.
−	Each of such types is interpreted as a set of unspecified cardinality
−	but disjoint from any other type.
−	<!--
−	Can we specify cardinalities?
−	-->
−	User-defined basic types are created by declarations like the following:
−
−	% User declarations of basic types:
−
−	MyBrandNewType: TYPE;
−
−	Apples, Oranges: TYPE;
−
−	=== Function Types ===
−
−	Function (<math>\to</math>) types are created by the mixfix type constructors
−	<center>
−	<math>
−	\begin{array}{l}
−	\_ \to \_ \\[1ex] (\ \_\ ,\ \_\ ) \to \_
−	\\[1ex] (\ \_\ ,\ \_\ ,\ \_\ ) \to \_
−	\\[1ex] \ldots
−	\end{array}
−	</math>
−	</center>
−	whose arguments can be instantiated by any value type.
−
−	% Function type declarations
−
−	UnaryFunType: TYPE = INT -> REAL;
−
−	BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL;
−
−	TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN;
−
−
−	A function type of the form <math>(T_1, \ldots, T_n) \to T</math> with <math>n > 0</math> is interpreted as the set of all ''total'' functions from the Cartesian product <math>T_1 \times \cdots \times T_n</math> to <math>T</math>.
−
−	The example above also shows how to introduce type names.
−	A name like <code>UnaryFunType</code> above is just an abbreviation for the type <math>\mathrm{INT} \to \mathrm{REAL}</math> and can be used interchangeably with it.
−
−	In general, any type defined by a type expression <code>E</code> can be given a name with the declaration:
−
−	name : TYPE = E;
−
−
−
−	=== Structured Types ===
−
−	All structured types are divided in following the families.
−
−	==== Array Types ====
−
−	Array types are created by the mixfix type constructors <math>\mathrm{ARRAY}\ \_\ \mathrm{OF}\ \_</math> whose arguments can be instantiated by any value type.
−
−	T1 : TYPE;
−
−	% Array types:
−
−	ArrayType1: TYPE = ARRAY T1 OF REAL;
−
−	ArrayType2: TYPE = ARRAY INT OF (ARRAY INT OF REAL);
−
−	ArrayType3: TYPE = ARRAY [INT, INT] OF INT;
−
−
−	An array type of the form <math>\mathrm{ARRAY}\ T_1\ \mathrm{OF}\ T_2</math> is interpreted as the set of all total maps from <math>T_1</math> to <math>T_2</math>. The main conceptual difference with the type <math>T_1 \to T_2</math> is that arrays, contrary to functions, are first-class objects of the language: they can be arguments or results of functions. Moreover, array types come equipped with an update operation.
−
−	==== Tuple Types ====
−
−	==== Record Types ====
−
−	==== Inductive Data Types ====
−
−	Inductive data types are created by declarations of the form
−	<center>
−	<math>
−	\begin{array}{l}
−	\mathrm{DATATYPE} \\
−	\ \ \mathit{type\_name}_1 = C_{1,1} \mid C_{1,2} \mid \cdots \mid C_{1,m_1}, \\
−	\ \ \mathit{type\_name}_2 = C_{2,1} \mid C_{2,2} \mid \cdots \mid C_{2,m_2}, \\
−	\ \ \vdots \\ \ \ \mathit{type\_name}_n = C_{n,1} \mid C_{n,2} \mid \cdots \mid C_{n,m_n} \\
−	\mathrm{END};
−	\end{array}
−	</math>
−	</center>
−	Each of the <math>C_{ij}</math> is either a constant symbol or an expression of the form
−
−	<center>
−	<math>\mathit{cons}(\ \mathit{sel}_1: T_1,\ \ldots,\ \mathit{sel}_k: T_k\ )
−	</math>
−	</center>
−	where <math>T_1, \ldots, T_k</math> are any first-order types or type names for first-order types,
−	including any <math>\mathit{type\_name}_i</math>.
−	Such declarations introduce for the data type:
−
−	* constructor symbols <math>cons</math> of type <math>(T_1, \ldots, T_k) \to \mathit{type\_name}_i</math>,
−	* selector symbols <math>\mathit{sel}_j</math> of type <math>\mathit{type\_name}_i \to T_j</math>, and
−	* tester symbols <math>\mathit{is\_cons}</math> of type <math>\mathit{type\_name}_i \to \mathrm{BOOLEAN}</math>.
−
−	Here are some examples of inductive data type declarations:
−
−	% simple enumeration type
−	% implicitly defined are the testers: is_red, is_yellow and is_blue
−	% (similarly for the other data types)
−
−	DATATYPE
−	PrimaryColor = red | yellow | blue
−	END;
−
−
−	% infinite set of pairwise distinct values ..., v(-1), v(0), v(1), ...
−
−	DATATYPE
−	Id = v (id: INT)
−	END;
−
−
−	% ML-style integer lists
−
−	DATATYPE
−	IntList = nil | cons (head: INT, tail: IntList)
−	END;
−
−
−	% ASTs
−
−	DATATYPE
−	Term = var (index: INT)
−	| apply (arg_1: Term, arg_2: Term)
−	| lambda (arg: INT, body: Term)
−	END;
−
−	% Trees
−
−	DATATYPE
−	Tree = tree (value: REAL, children: TreeList),
−	TreeList = nil_tl
−	| cons_tl (first_t1: Tree, rest_t1: TreeList)
−	END;
−
−	Constructor, selector and tester symbols defined for a data type have global scope. So, for instance, it is not possible for two different data types to use the same name for a constructor.
−
−	An inductive data type is interpreted as a term algebra constructed by the constructor symbols over some sets of generators. For example, the type <code>IntList</code> in the example above is interpreted as the set of all terms constructed with <code>nil</code> and <code>cons</code> over the integers.
−
−	Because of this semantics, CVC4 allows only ''inductive'' data types, that is, data types whose values are essentially (labeled, ordered) finite trees.
−	Infinite structures such as streams or even finite but cyclic ones such as circular lists are then excluded.
−	For instance, none of the following declarations define inductive databtypes, and are rejected by CVC4:
−
−	DATATYPE
−	IntStream = s (first:INT, rest: IntStream)
−	END;
−
−	DATATYPE
−	RationalTree = node1 (child: RationalTree)
−	| node2 (left_child: RationalTree, right_child:RationalTree)
−	END;
−
−	DATATYPE
−	T1 =  c1 (s1: T2),
−	T2 =  c2 (s2: T1)
−	END;
−
−	In concrete, a declaration of <math>n \geq 1</math> datatypes <math>T_1, \ldots, T_n</math> will be rejected if for any one of the types <math>T_1, \ldots, T_n</math>, it is impossible to build a finite term of that type using only the constructors of <math>T_1, \ldots, T_n</math> and free constants of type other than <math>T_1, \ldots, T_n</math>.
−
−	Inductive data types are the only types where the user also chooses names for the built-in operations to:
−
−	* construct a value of the type (with the constructors),
−	* extract components from a value (with the selectors), or
−	* check if a value was constructed with a certain constructor or not (with the testers).
−
−	For all the other types, CVC4 provides predefined names for the built-in operations on the type.
−
−	==== Tuple Types ====
−
−	== Type Checking ==
−
−	== Terms and Formulas ==
−
−	=== Logical Symbols ===
−
−	=== User-defined Functions and Types ===
−
−	=== Arithmetic ===
−
−	=== Bit vectors ===
−
−	=== Arrays ===
−
−	=== Data types ===
−
−	=== Tuples and Records ===
−
−
−	== Commands ==
−
−	=== QUERY ===
−
−
−	=== CHECKSAT ===
−
−	=== RESTART ===
−
−	== Instantiation Patterns ==
−
−	== Subtypes ==
−
−	=== Subtype Checking ===
−
−	=CVC4's support for the SMT-LIB language=
−
−	==SMT-LIB compliance==
−
−	Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
−	standard (http://smtlib.org/).  However, when parsing SMT-LIB input,
−	certain default settings don't match what is stated in the official
−	standard.  To make CVC4 adhere more strictly to the standard, use the
−	"--smtlib" command-line option.  Even with this setting, CVC4 is
−	somewhat lenient; some non-conforming input may still be parsed and
−	processed.
−
−	=The CVC4 library interface (API)=
−	==Using CVC4 in a C++ project==
	==Using CVC4 from Java==		==Using CVC4 from Java==
	==The compatibility interface==		==The compatibility interface==
Line 829:		Line 275:
	===If you were using CVC3 from Java===		===If you were using CVC3 from Java===
−	=Useful command-line options=	+	=Advanced features=
−	==Statistics==	+	This section describes some features of CVC4 of interest to developers and advanced users.
−	Statistics can be dumped on exit (both normal and abnormal exits) with	+	==Resource limits==
−	the --statistics command line option.	+
−		+
−	==Time and resource limits==	+
	CVC4 can be made to self-timeout after a given number of milliseconds.		CVC4 can be made to self-timeout after a given number of milliseconds.
Line 861:		Line 304:
	heap.		heap.
−	=Dumping API calls or preprocessed output=	+	==Dumping API calls or preprocessed output==
−	=Changing the output language=	+	[to do]
−	=Proof support=	+	==Changing the output language==
		+
		+	[to do]
		+
		+	==Proof support==
	CVC4 1.0 has limited support for proofs, and they are disabled by default.		CVC4 1.0 has limited support for proofs, and they are disabled by default.
Line 873:		Line 320:
	release).		release).
−	=Portfolio solving=	+	==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		If enabled at configure-time (./configure --with-portfolio), a second
Line 885:		Line 336:
	literals that are "local" to one thread.)		literals that are "local" to one thread.)
−	Currently, the portfolio **does not work** with quantifiers or with	+	Currently, the portfolio **does not work** with the theory of inductive
−	the theory of inductive datatypes. These limitations will be addressed	+	datatypes. This limitation will be addressed in a future release.
−	in a future release.	+
		+	See more details and examples in the [[Tutorials#Parallel_Solving|tutorial]].
−	=Emacs support=	+	==Emacs support==
	For a suggestion of editing CVC4 source code with emacs, see the file		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		contrib/editing-with-emacs.  For a CVC language mode (the native input
	language for CVC4), see contrib/cvc-mode.el.		language for CVC4), see contrib/cvc-mode.el.

---

Latest revision as of 10:31, 26 January 2019

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

Getting CVC4 binaries

The most recent binaries can be downloaded from our Nightly Builds pages:

• Optimized binaries (statically linked)
• Debug binaries (statically linked)

Building CVC4 from source

Sources are available from the same site as the binaries. The source-code is also available in the 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 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
• SMT-LIB 2.0 (see 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
• 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 /examples/simple_vc_cxx.cpp. The file goes through the examples for the basic interaction with CVC4:

1. Constructing an ExprManager em
2. Constructing an SmtEngine w.r.t. em.
3. Getting a copy of the Type for mathematical integers from em, em.integerType().
4. Constructing new Expressions
   1. Integer variables x and y: Expr x = em.mkVar("x", integer);
   2. The rational constant 0: em.mkConst(Rational(0));
   3. Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
5. 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:

• Optimized binaries (statically linked)
• 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 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.