<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: The CVC3 User's Manual</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li class="current"><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">The <a class="el" href="namespaceCVC3.html">CVC3</a> User's Manual </div> </div>
</div><!--header-->
<div class="contents">
<div class="textblock"><p><b>Contents</b></p>
<ul>
<li>
<a class="el" href="user_doc.html#user_doc_what_is_cvc3">What is CVC3?</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_command_line">Running CVC3 from a Command Line</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang">Presentation Input Language</a> <ul>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_types">Type system</a> <ul>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_real_type">REAL Type</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_bitvec_types">Bit Vector Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_unint_types">User-defined Atomic Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_bool_type">BOOLEAN Type</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_fun_types">Function Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_array_types">Array Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_tuple_types">Tuple Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_record_types">Record Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_data_types">Inductive Data Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_typing">Type Checking</a> </li>
</ul>
</li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr">Terms and Formulas</a> <ul>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_logic">Logical Symbols</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_unint">User-defined Functions and Types</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_arith">Arithmetic</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_bit">Bit vectors</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_arr">Arrays</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_dat">Datatypes</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_expr_rec_tup">Tuples and Records</a> </li>
</ul>
</li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_commands">Commands</a> <ul>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_commands_query">QUERY</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_commands_checksat">CHECKSAT</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_commands_restart">RESTART</a> </li>
</ul>
</li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_patterns">Instantiation Patterns</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_subtypes">Subtypes</a> <ul>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_subtyping">Subtype Checking</a> </li>
<li>
<a class="el" href="user_doc.html#user_doc_pres_lang_tccs">Type Correctness Conditions</a> </li>
</ul>
</li>
</ul>
</li>
<li>
<a class="el" href="user_doc.html#user_doc_smtlib_lang">SMT-LIB Input Language</a> </li>
</ul>
<h1><a class="anchor" id="user_doc_what_is_cvc3"></a>
What is CVC3?</h1>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> is an automated <em>validity checker</em> for a many-sorted (i.e., typed) first-order logic with <em>built-in theories</em>, including some support for quantifiers, partial functions, and predicate subtypes. The current built-in theories are the theories of: </p>
<ul>
<li>
equality over <em>free</em> (aka <em>uninterpreted</em>) function and predicate symbols, </li>
<li>
real and integer linear arithmetic (with some support for non-linear arithmetic), </li>
<li>
bit vectors, </li>
<li>
arrays, </li>
<li>
tuples, </li>
<li>
records, </li>
<li>
user-defined inductive datatypes. </li>
</ul>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> checks whether a given formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is valid in the built-in theories under a given set <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> of assumptions. More precisely, it checks whether </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[\Gamma\models_T \phi\]" src="form_2.png"/>
</p>
<p> that is, whether <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is a logical consequence of the union <img class="formulaInl" alt="$T$" src="form_3.png"/> of the built-in theories and the set of formulas <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>.</p>
<p>Roughly speaking, when <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is <em>universal</em> and all the formulas in <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> are <em>existential</em> (i.e., when <img class="formulaInl" alt="$\phi$" src="form_0.png"/> and <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> contain at most universal, respectively existential, quantifiers), <a class="el" href="namespaceCVC3.html">CVC3</a> is in fact a decision procedure: it is always guaranteed (well, modulo bugs and memory limits) to return a correct "valid" or "invalid" answer. In all other cases, <a class="el" href="namespaceCVC3.html">CVC3</a> is sound but incomplete: it will never say that an invalid formula is valid but it may either never return or give up and return "unknown" in some cases when <img class="formulaInl" alt="$\Gamma \models_T \phi$" src="form_4.png"/>.</p>
<p>When <a class="el" href="namespaceCVC3.html">CVC3</a> returns "valid" it can return a formal proof of the validity of <img class="formulaInl" alt="$\phi$" src="form_0.png"/> under the <em>logical context</em> <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>, together with the subset <img class="formulaInl" alt="$\Gamma'$" src="form_5.png"/> of <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> used in the proof, such that <img class="formulaInl" alt="$\Gamma'\models_T \phi$" src="form_6.png"/>.</p>
<p>When <a class="el" href="namespaceCVC3.html">CVC3</a> returns "invalid" it can return, in the current terminology, both a <em>counter-example</em> to <img class="formulaInl" alt="$\phi$" src="form_0.png"/>'s validity under <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> and a <em>counter-model</em>. Both a counter-example and a counter-models are a set <img class="formulaInl" alt="$\Delta$" src="form_7.png"/> of additional formulas consistent with <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> in <img class="formulaInl" alt="$T$" src="form_3.png"/>, but entailing the negation of <img class="formulaInl" alt="$\phi$" src="form_0.png"/>. In formulas: </p>
<center> <img class="formulaInl" alt="$\Gamma \cup \Delta \not\models_T \mathit{false}$" src="form_8.png"/> and <img class="formulaInl" alt="$\Gamma \cup \Delta \models_T \lnot \phi$" src="form_9.png"/>. </center><p>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 <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> and <img class="formulaInl" alt="$\phi$" src="form_0.png"/> (see <a class="el" href="user_doc.html#user_doc_pres_lang_commands_query">QUERY</a> for more details).</p>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> can be used in two modes: as a library or as a command-line executable (implemented as a command-line interface to the library). Interfaces to the library are available in C/C++, Java and .NET. This manual mainly describes the command-line interface on a unix-type platform.</p>
<h1><a class="anchor" id="user_doc_command_line"></a>
Running CVC3 from a Command Line</h1>
<p>Assuming you have properly installed <a class="el" href="namespaceCVC3.html">CVC3</a> on your machine (check the <a class="el" href="INSTALL.html">INSTALL</a> section for that), you will have an executable file called <code>cvc3</code>. It reads the input (a sequence of commands) from the standard input and prints the results on the standard output. Errors and some other messages (e.g. debugging traces) are printed on the standard error.</p>
<p>Typically, the input to <code>cvc3</code> is saved in a file and redirected to the executable, or given on a command line:</p>
<pre class="fragment"># Reading from standard input:
cvc3 < input-file.cvc
# Reading directly from file:
cvc3 input-file.cvc
</pre><p>Notice that, for efficiency, <a class="el" href="namespaceCVC3.html">CVC3</a> uses input buffers, and the input is not always processed immediately after each command. Therefore, if you want to type the commands interactively and receive immediate feedback, use the <code>+interactive</code> option (can be shortened to <code>+int</code>):</p>
<pre class="fragment"> cvc3 +int
</pre><p>Run <code>cvc3 -h</code> for more information on the available options.</p>
<p>The command line front-end of <a class="el" href="namespaceCVC3.html">CVC3</a> supports two input languages. </p>
<ul>
<li>
<a class="el" href="namespaceCVC3.html">CVC3</a>'s own <em>presentation language</em> whose syntax was initially inspired by the PVS and SAL systems and is almost identical to the input language of CVC and CVC Lite, the predecessors of <a class="el" href="namespaceCVC3.html">CVC3</a>; </li>
<li>
the standard language promoted by the <a href="http://www.SMT-LIB.org">SMT-LIB initiative</a> for SMT-LIB benchmarks. </li>
</ul>
<p>We describe the input languages next, concentrating mostly on the first.</p>
<h1><a class="anchor" id="user_doc_pres_lang"></a>
Presentation Input Language</h1>
<p>The input language consists of a sequence of symbol declarations and commands, each followed by a semicolon (<code>;</code>).</p>
<p>Any text after the first occurrence of a percent character and to the end of the current line is a comment:</p>
<pre class="fragment">%%% This is a CVC3 comment
</pre><h2><a class="anchor" id="user_doc_pres_lang_types"></a>
Type system</h2>
<p><a class="el" href="namespaceCVC3.html">CVC3</a>'s type system includes a set of built-in types which can be expanded with additional user-defined types.</p>
<p>The type system consists of <em>value</em> types, <em>non-value</em> types and <em>subtypes</em> of value types, all of which are interpreted as sets. For convenience, we will sometimes identify below the interpretation of a type with the type itself.</p>
<p>Value types consist of <em>atomic</em> types and <em>structured</em> types. The atomic types are <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/>, <img class="formulaInl" alt="$\mathrm{BITVECTOR}(n)$" src="form_11.png"/> for all <img class="formulaInl" alt="$n > 0$" src="form_12.png"/>, as well as user-defined atomic types (also called <em>uninterpreted</em> types). The structured types are <em>array</em>, <em>tuple</em>, and <em>record</em> types, as well as ML-style user-defined (inductive) <em>datatypes</em>.</p>
<p>Non-value types consist of the type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> and <em>function</em> types. Subtypes include the built-in subtype <img class="formulaInl" alt="$\mathrm{INT}$" src="form_14.png"/> of <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/> and are covered in the <a class="el" href="user_doc.html#user_doc_pres_lang_subtypes">Subtypes</a> section below.</p>
<h3><a class="anchor" id="user_doc_pres_lang_real_type"></a>
REAL Type</h3>
<p>The <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/> type is interpreted as the set of rational numbers. The name <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/> is justified by the fact that a <a class="el" href="namespaceCVC3.html">CVC3</a> formula is valid in the theory of rational numbers iff it is valid in the theory of real numbers.</p>
<h3><a class="anchor" id="user_doc_pres_lang_bitvec_types"></a>
Bit Vector Types</h3>
<p>For every positive numeral <em>n</em>, the type <img class="formulaInl" alt="$\mathrm{BITVECTOR}(n)$" src="form_11.png"/> is interpreted as the set of all bit vectors of size <em>n</em>.</p>
<h3><a class="anchor" id="user_doc_pres_lang_unint_types"></a>
User-defined Atomic Types</h3>
<p>User-defined atomic types are each interpreted as a set of unspecified cardinality but disjoint from any other type. They are created by declarations like the following:</p>
<pre class="fragment">% User declarations of atomic types:
MyBrandNewType: TYPE;
Apples, Oranges: TYPE;
</pre><h3><a class="anchor" id="user_doc_pres_lang_bool_type"></a>
BOOLEAN Type</h3>
<p>The <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> type is, perhaps confusingly, the type of <a class="el" href="namespaceCVC3.html">CVC3</a> formulas, not the two-element set of Boolean values. The fact that <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> is not a value type in practice means that it is not possible for function symbols in <a class="el" href="namespaceCVC3.html">CVC3</a> to have a arguments of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>. The reason is that <a class="el" href="namespaceCVC3.html">CVC3</a> 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. (An exception is the IF-THEN-ELSE construct, see later.) The only difference is that, syntactically, formulas in <a class="el" href="namespaceCVC3.html">CVC3</a> are terms of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>. A function symbol <code>f</code> then <em>can</em> have <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> as its return type. But that is just <a class="el" href="namespaceCVC3.html">CVC3</a>'s way, inherited from the previous systems of the CVC family, to say that <code>f</code> is a predicate symbol.</p>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> does have a type that behaves like a Boolean Value type, that is, a value type with only two elements and with the usual Boolean operations defined on it: it is <code>BITVECTOR(1)</code>.</p>
<h3><a class="anchor" id="user_doc_pres_lang_fun_types"></a>
Function Types</h3>
<p>All structured types are actually <em>families</em> of types. Function ( <img class="formulaInl" alt="$\to$" src="form_15.png"/>) types are created by the mixfix type constructors</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \begin{array}{l} \_ \to \_ \\[1ex] (\ \_\ ,\ \_\ ) \to \_ \\[1ex] (\ \_\ ,\ \_\ ,\ \_\ ) \to \_ \\[1ex] \ldots \end{array} \]" src="form_16.png"/>
</p>
<p>whose arguments can be instantiated by any value (sub)type, with the addition that the last argument can also be <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>.</p>
<pre class="fragment">% Function type declarations
UnaryFunType: TYPE = INT -> REAL;
BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL;
TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN;
</pre><p>A function type of the form <img class="formulaInl" alt="$(T_1, \ldots, T_n) \to T$" src="form_17.png"/> with <img class="formulaInl" alt="$n > 0$" src="form_12.png"/> is interpreted as the set of all total functions from the Cartesian product <img class="formulaInl" alt="$T_1 \times \cdots \times T_n$" src="form_18.png"/> to <img class="formulaInl" alt="$T$" src="form_3.png"/> when <img class="formulaInl" alt="$T$" src="form_3.png"/> is not <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>. Otherwise, it is interpreted as the set of all relations over <img class="formulaInl" alt="$T_1 \times \cdots \times T_n$" src="form_18.png"/></p>
<p>The example above also shows how to introduce <em>type names</em>. A name like <code>UnaryFunType</code> above is just an abbreviation for the type <img class="formulaInl" alt="$\mathrm{INT} \to \mathrm{REAL}$" src="form_19.png"/> and can be used interchangeably with it.</p>
<p><br/>
In general, any type defined by a type expression <code>E</code> can be given a name with the declaration:</p>
<pre class="fragment">name : TYPE = E;
</pre><h3><a class="anchor" id="user_doc_pres_lang_array_types"></a>
Array Types</h3>
<p>Array types are created by the mixfix type constructors <img class="formulaInl" alt="$\mathrm{ARRAY}\ \_\ \mathrm{OF}\ \_$" src="form_20.png"/> whose arguments can be instantiated by any value type.</p>
<pre class="fragment">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;
</pre><p>An array type of the form <img class="formulaInl" alt="$\mathrm{ARRAY}\ T_1\ \mathrm{OF}\ T_2$" src="form_21.png"/> is interpreted as the set of all total maps from <img class="formulaInl" alt="$T_1$" src="form_22.png"/> to <img class="formulaInl" alt="$T_2$" src="form_23.png"/>. The main conceptual difference with the type <img class="formulaInl" alt="$T_1 \to T_2$" src="form_24.png"/> 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.</p>
<h3><a class="anchor" id="user_doc_pres_lang_tuple_types"></a>
Tuple Types</h3>
<p>Tuple types are created by the mixfix type constructors</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \begin{array}{l} [\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ \ ,\ \_\ ] \\[1ex] \ldots \end{array} \]" src="form_25.png"/>
</p>
<p>whose arguments can be instantiated by any value type.</p>
<pre class="fragment">% Tuple declaration
TupleType: TYPE = [ REAL, ArrayType1, [INT, INT] ];</pre><p>A tuple type of the form <img class="formulaInl" alt="$[T_1, \ldots, T_n]$" src="form_26.png"/> is interpreted as the Cartesian product <img class="formulaInl" alt="$T_1 \times \cdots \times T_n$" src="form_18.png"/>. Note that while the types <img class="formulaInl" alt="$(T_1, \ldots, T_n) \to T$" src="form_17.png"/> and <img class="formulaInl" alt="$[T_1 \times \cdots \times T_n] \to T$" src="form_27.png"/> are semantically equivalent, they are operationally different in <a class="el" href="namespaceCVC3.html">CVC3</a>. The first is the type of functions that take <em>n</em> arguments, while the second is the type of functions of <em>1</em> argument of type n-tuple.</p>
<h3><a class="anchor" id="user_doc_pres_lang_record_types"></a>
Record Types</h3>
<p>Similar to, but more general than tuple types, record types are created by type constructors of the form</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ [\#\ l_1: \_\ ,\ \ldots\ ,\ l_n: \_\ \#] \]" src="form_28.png"/>
</p>
<p>where <img class="formulaInl" alt="$n > 0$" src="form_12.png"/>, <img class="formulaInl" alt="$l_1,\ldots, l_n$" src="form_29.png"/> are field labels, and the arguments can be instantiated with any value types.</p>
<pre class="fragment">% Record declaration
RecordType: TYPE = [# number: INT, value: REAL, info: TupleType #];
</pre><p>The order of the fields in a record type is meaningful. In other words, permuting the field names gives a different type. Note that records are</p>
<p>non-recursive. For instance, it is not possible to declare a record type called <code>Person</code> containing a field of type <code>Person</code>. Recursive types are provided in <a class="el" href="namespaceCVC3.html">CVC3</a> as ML-style datatypes.</p>
<h3><a class="anchor" id="user_doc_pres_lang_data_types"></a>
Inductive Data Types</h3>
<p>Inductive datatypes are created by declarations of the form</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \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} \]" src="form_30.png"/>
</p>
<p>Each of the <img class="formulaInl" alt="$C_{ij}$" src="form_31.png"/> is either a constant symbol or an expression of the form</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathit{cons}(\ \mathit{sel}_1: T_1,\ \ldots,\ \mathit{sel}_k: T_k\ ) \]" src="form_32.png"/>
</p>
<p>where <img class="formulaInl" alt="$T_1, \ldots, T_k$" src="form_33.png"/> are any value types or type names for value types, including any <img class="formulaInl" alt="$\mathit{type\_name}_i$" src="form_34.png"/>. Such declarations introduce for the datatype:</p>
<ul>
<li><em>constructor</em> symbols <img class="formulaInl" alt="$cons$" src="form_35.png"/> of type <img class="formulaInl" alt="$(T_1, \ldots, T_k) \to \mathit{type\_name}_i$" src="form_36.png"/>,</li>
<li><em>selector</em> symbols <img class="formulaInl" alt="$\mathit{sel}_j$" src="form_37.png"/> of type <img class="formulaInl" alt="$\mathit{type\_name}_i \to T_j$" src="form_38.png"/>, and</li>
<li><em>tester</em> symbols <img class="formulaInl" alt="$\mathit{is\_cons}$" src="form_39.png"/> of type <img class="formulaInl" alt="$\mathit{type\_name}_i \to \mathrm{BOOLEAN}$" src="form_40.png"/>.</li>
</ul>
<p>Here are some examples of datatype declarations:</p>
<pre class="fragment">% simple enumeration type
% implicitly defined are the testers: is_red, is_yellow and is_blue
% (similarly for the other datatypes)
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;
</pre><p>Constructor, selector and tester symbols defined for a datatype have global scope. So, for instance, it is not possible for two different datatypes to use the same name for a constructor.</p>
<p>A datatype is interpreted as a term algebra constructed by the constructor symbols over some sets of generators. For example, the datatype <code>IntList</code> is interpreted as the set of all terms constructed with <code>nil</code> and <code>cons</code> over the integers.</p>
<p>Because of this semantics, <a class="el" href="namespaceCVC3.html">CVC3</a> allows only <em>inductive</em> datatypes, that is, datatypes 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 datatypes, and are rejected by <a class="el" href="namespaceCVC3.html">CVC3</a>:</p>
<pre class="fragment">DATATYPE
IntStream = s (first:INT, rest: IntStream)
END;
DATATYPE
RationalTree = node1 (first_child1: RationalTree)
| node2 (first_child2: RationalTree, second_child2:RationalTree)
END;
DATATYPE
T1 = c1 (s1: T2),
T2 = c2 (s2: T1)
END;
</pre><p>In concrete, a declaration of <img class="formulaInl" alt="$n \geq 1$" src="form_41.png"/> datatypes <img class="formulaInl" alt="$T_1, \ldots, T_n$" src="form_42.png"/> will be rejected if for any one of the types <img class="formulaInl" alt="$T_1, \ldots, T_n$" src="form_42.png"/>, it is impossible to build a finite term of that type using only the constructors of <img class="formulaInl" alt="$T_1, \ldots, T_n$" src="form_42.png"/> and free constants of type other than <img class="formulaInl" alt="$T_1, \ldots, T_n$" src="form_42.png"/>.</p>
<p>Datatypes are the only types for which the user also chooses names for the built-in operations defined on the type for:</p>
<ul>
<li>constructing a value (with the constructors),</li>
<li>extracting components from a value (with the selectors), or</li>
<li>checking if a value was constructed with a certain constructor or not (with the testers).</li>
</ul>
<p>For all the other types, <a class="el" href="namespaceCVC3.html">CVC3</a> provides predefined names for the built-in operations on the type.</p>
<h3><a class="anchor" id="user_doc_pres_lang_typing"></a>
Type Checking</h3>
<p>In essence, <a class="el" href="namespaceCVC3.html">CVC3</a> terms are statically typed at the level of types–as opposed to <em>sub</em>types–according to the usual rules of first-order many-sorted logic (the typing rules for formulas are analogous):</p>
<ul>
<li>each variable has one associated (non-function) type,</li>
<li>each constant symbol has one associated (non-function) type,</li>
<li>each function symbol has one or more associated function types,</li>
<li>the type of a term consisting just of a variable or a constant symbol is the type associated to that variable or constant symbol,</li>
<li>the term obtained by applying a function symbol <img class="formulaInl" alt="$f$" src="form_43.png"/> to the terms <img class="formulaInl" alt="$t_1, \ldots, t_n$" src="form_44.png"/> is <img class="formulaInl" alt="$T$" src="form_3.png"/> if <img class="formulaInl" alt="$f$" src="form_43.png"/> has type <img class="formulaInl" alt="$(T_1, \ldots, T_n) \to T$" src="form_17.png"/> and each <img class="formulaInl" alt="$t_i$" src="form_45.png"/> has type <img class="formulaInl" alt="$T_i$" src="form_46.png"/>.</li>
</ul>
<p>Attempting to enter an ill-typed term will result in an error.</p>
<p>The main difference with standard many-sorted logic is that some built-in symbols are parametrically polymorphic. For instance the function symbol for extracting the element of any array has type <img class="formulaInl" alt="$(\mathit{ARRAY}\ T_1\ \mathit{OF}\ T_2,\; T_1) \to T_2$" src="form_47.png"/> for all types <img class="formulaInl" alt="$T_1, T_2$" src="form_48.png"/> not containing function or predicate types.</p>
<h2><a class="anchor" id="user_doc_pres_lang_expr"></a>
Terms and Formulas</h2>
<p>In addition to type expressions, <a class="el" href="namespaceCVC3.html">CVC3</a> has expressions for terms and formulas (i.e., terms of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>). By and large, these are standard first-order terms built out of (typed) variables, predefined theory-specific operators, free (i.e., user-defined) function symbols, and quantifiers. Extensions include an if-then-else operator, lambda abstractions, and local symbol declarations, as illustrated below. Note that these extensions still keep <a class="el" href="namespaceCVC3.html">CVC3</a>'s language first-order. In particular, lambda abstractions are restricted to take and return only terms of a value type. Similarly, quantifiers can only quantify variables of a value type.</p>
<p>Free function symbols include <em>constant</em> symbols and <em>predicate</em> symbols, respectively nullary function symbols and function symbols with a <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> return type. Free symbols are introduced with global declarations of the form <img class="formulaInl" alt="$f_1, \ldots, f_m: T;$" src="form_49.png"/> where <img class="formulaInl" alt="$m > 0$" src="form_50.png"/>, <img class="formulaInl" alt="$f_i$" src="form_51.png"/> are the names of the symbols and <img class="formulaInl" alt="$T$" src="form_3.png"/> is their type:</p>
<pre class="fragment">% integer constants
a, b, c: INT;
% real constants
x,y,z: REAL;
% unary function
f1: REAL -> REAL;
% binary function
f2: (REAL, INT) -> REAL;
% unary function with a tuple argument
f3: [INT, REAL] -> BOOLEAN;
% binary predicate
p: (INT, REAL) -> BOOLEAN;
% Propositional "variables"
P,Q; BOOLEAN;
</pre><p>Like type declarations, such free symbol declarations have global scope and must be unique. In other words, it is not possible to globally declare a symbol more than once. This entails among other things that free symbols cannot be overloaded with different types.</p>
<p>As with types, a new free symbol can be defined as the name of a term of the corresponding type. With constant symbols this is done with a declaration of the form <img class="formulaInl" alt="$f:T = t;$" src="form_52.png"/> :</p>
<pre class="fragment">c: INT;
i: INT = 5 + 3*c;
j: REAL = 3/4;
t: [REAL, INT] = (2/3, -4);
r: [# key: INT, value: REAL #] = (# key := 4, value := (c + 1)/2 #);
f: BOOLEAN = FORALL (x:INT): x <= 0 OR x > c ;
</pre><p>A restriction on constants of type <img class="formulaInl" alt="$\mathit{BOOLEAN}$" src="form_53.png"/> is that their value can only be a <em>closed</em> formula, that is, a formula with no free variables.</p>
<p>A term and its name can be used interchangeably in later expressions. Named terms are often useful for shared subterms (terms used several times in different places) since their use can make the input exponentially more concise. Named terms are processed very efficiently by <a class="el" href="namespaceCVC3.html">CVC3</a>. It is much more efficient to associate a complex term with a name directly rather than to declare a constant and later assert that it is equal to the same term. This point will be explained in more detail later in section <a class="el" href="user_doc.html#user_doc_pres_lang_commands">Commands</a>.</p>
<p>More generally, in <a class="el" href="namespaceCVC3.html">CVC3</a> one can associate a term to function symbols of any arity. For non-constant function symbols this is done with a declaration of the form </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ f:(T_1, \ldots, T_n) \to T = \mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t\;; \]" src="form_54.png"/>
</p>
<p> where <img class="formulaInl" alt="$t$" src="form_55.png"/> is any term of type <img class="formulaInl" alt="$T$" src="form_3.png"/> with free variables in <img class="formulaInl" alt="$\{x_1, \ldots, x_n\}$" src="form_56.png"/>. The lambda binder has the usual semantics and conforms to the usual lexical scoping rules: within the term <img class="formulaInl" alt="$t$" src="form_55.png"/> the declaration of the symbols <img class="formulaInl" alt="$x_1, \ldots, x_n$" src="form_57.png"/> as local variables of respective type <img class="formulaInl" alt="$T_1, \ldots, T_n$" src="form_42.png"/> hides any previous, global declaration of those symbols.</p>
<p>As a general shorthand, when <img class="formulaInl" alt="$k$" src="form_58.png"/> consecutive types <img class="formulaInl" alt="$T_i, \ldots, T_{i+k-1}$" src="form_59.png"/> in the lambda expression <img class="formulaInl" alt="$\mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t$" src="form_60.png"/> are identical, the syntax <img class="formulaInl" alt="$\mathrm{LAMBDA}(x_1:T_1, \ldots, x_i,\ldots, x_{i+k-1}:T_i,\ldots, x:T_n): t$" src="form_61.png"/> is also allowed.</p>
<pre class="fragment">% Global declaration of x as a unary function symbol
x: REAL -> REAL;
% Local declarations of x as a constant symbol
f: REAL -> REAL = LAMBDA (x: REAL): 2*x + 3;
p: (INT, INT) -> BOOLEAN = LAMBDA (x,i: INT): i*x - 1 > 0;
g: (REAL, INT) -> [REAL, INT] = LAMBDA (x: REAL, i:INT): (x + 1, i - 3);
</pre><p>Constant and function symbols can also be declared <em>locally</em> anywhere within a term by means of a <em>let</em> binder. This is done with a declaration of the form </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \begin{array}{rl} \mathrm{LET} & f_1 = t_1, \\ & \vdots \\ & f_n = t_m \\ \mathrm{IN} & t ; \end{array} \]" src="form_62.png"/>
</p>
<p> for constant symbols, and of the form </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \begin{array}{rlcl} \mathrm{LET} & f_1 & = &\mathrm{LAMBDA}(x^1_1:T^1_1, \ldots, x^{n_1}_1:T^{n_1}_1):\; t_1, \\ & & \vdots & \\ & f_m & = & \mathrm{LAMBDA}(x^1_m:T^1_m, \ldots, x^{n_m}_m:T^{n_m}_m):\; t_m \\ \mathrm{IN} & t ; \end{array} \]" src="form_63.png"/>
</p>
<p> for non-constant symbols. Let binders can be nested arbitrarily and follow the usual lexical scoping rules.</p>
<pre class="fragment">t: REAL =
LET g = LAMBDA(x:INT): x + 1,
x1 = 42,
x2 = 2*x1 + 7/2
IN
(LET x3 = g(x1) IN x3 + x2) / x1;
</pre><p>Note that the same symbol <code>=</code> is used, unambiguously, in the syntax of global declarations, let declarations, and as a predicate symbol.</p>
<p>In addition to user-defined symbols, <a class="el" href="namespaceCVC3.html">CVC3</a> terms can use a number of predefined symbols: the logical symbols as well as <em>theory</em> symbols, function symbols belonging to one of the built-in theories. They are described next, with the theory symbols grouped by theory.</p>
<h3><a class="anchor" id="user_doc_pres_lang_expr_logic"></a>
Logical Symbols</h3>
<p>The logical symbols in <a class="el" href="namespaceCVC3.html">CVC3</a>'s language include the equality and disequality predicate symbols, respectively written as <code>=</code> and <code>/=</code>, the multiarity disequality symbol <code>DISTINCT</code>, together with the logical constants <code>TRUE</code>, <code>FALSE</code>, the connectives <code>NOT</code>, <code>AND</code>, <code>OR</code>, <code>XOR</code>, <code>=></code>, <code><=></code>, and the first-order quantifiers <code>EXISTS</code> and <code>FORALL</code>, all with the standard many-sorted logic semantics.</p>
<p>The binary connectives have infix syntax and type <img class="formulaInl" alt="$(\mathrm{BOOLEAN},\mathrm{BOOLEAN}) \to \mathrm{BOOLEAN}$" src="form_64.png"/>. The symbols <code>=</code> and <code>/=</code>, which are also infix, are instead polymorphic, having type <img class="formulaInl" alt="$(T,T) \to \mathrm{BOOLEAN}$" src="form_65.png"/> for every predefined or user-defined value type <img class="formulaInl" alt="$T$" src="form_3.png"/>. They are interpreted respectively as the identity relation and its complement.</p>
<p>The <img class="formulaInl" alt="$\mathrm{DISTINCT}$" src="form_66.png"/> symbol is both overloaded and polymorphic. It has type <img class="formulaInl" alt="$(T,...,T) \to \mathrm{BOOLEAN}$" src="form_67.png"/> for every tuple <img class="formulaInl" alt="$(T,...,T)$" src="form_68.png"/> of length <img class="formulaInl" alt="$n > 0$" src="form_12.png"/> where <img class="formulaInl" alt="$T$" src="form_3.png"/> is a predefined or user-defined value type. For each <img class="formulaInl" alt="$n > 0$" src="form_12.png"/>, it is interpreteted as the relation that holds exactly for tuples of pairwise distinct elements.</p>
<p>The syntax for quantifiers is similar to that of the lambda binder.</p>
<p>Here is an example of a formula built just of these logical symbols and variables:</p>
<pre class="fragment">A, B: TYPE;
quant: BOOLEAN = FORALL (x,y: A, i,j,k: B): i = j AND i /= k
=> EXISTS (z: A): x /= z OR z /= y;
</pre><p>Binding and scoping of quantified variables follows the same rules as in let expressions. In particular, a quantifier will shadow in its scope any constant and function symbols with the same name as one of the variables it quantifies:</p>
<pre class="fragment">A: TYPE;
i,j: INT;
% The first occurrence of i and of j in f are constant symbols,
% the others are variables.
f: BOOLEAN = i = j AND FORALL (i,j: A): i = j OR i /= j;
</pre><p>Optionally, it is also possible to specify <em>instantiation patterns</em> for quantified variables. The general syntax for a quantified formula <img class="formulaInl" alt="$\psi$" src="form_69.png"/> with patterns is</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ Q\:(x_1:T_1, \ldots, x_k:T_k):\; p_1: \ldots\; p_n:\; \varphi \]" src="form_70.png"/>
</p>
<p>where <img class="formulaInl" alt="$n \geq 0$" src="form_71.png"/>, <img class="formulaInl" alt="$Q$" src="form_72.png"/> is either <img class="formulaInl" alt="$\mathrm{FORALL}$" src="form_73.png"/> or <img class="formulaInl" alt="$\mathrm{EXISTS}$" src="form_74.png"/>, <img class="formulaInl" alt="$\varphi$" src="form_75.png"/> is a term of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/>, and each of the <img class="formulaInl" alt="$p_i$" src="form_76.png"/>'s, a <em>pattern for the quantifier</em> <img class="formulaInl" alt="$Q\:(x_1:T_1, \ldots, x_k:T_k)$" src="form_77.png"/>, has the form </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathrm{PATTERN}\; (t_1, \ldots, t_m) \]" src="form_78.png"/>
</p>
<p> where <img class="formulaInl" alt="$m > 0$" src="form_50.png"/> and <img class="formulaInl" alt="$t_1, \ldots, t_m$" src="form_79.png"/> are arbitrary binder-free terms (no lets, no quantifiers). Those terms can contain (free) variables, typically, but not exclusively, drawn from <img class="formulaInl" alt="$x_1, \ldots, x_k$" src="form_80.png"/>. (Additional variables can occur if <img class="formulaInl" alt="$\psi$" src="form_69.png"/> occurs in a bigger formula binding those variables.)</p>
<pre class="fragment">A: TYPE;
b, c: A;
p, q: A -> BOOLEAN;
r: (A, A) -> BOOLEAN;
ASSERT FORALL (x0, x1, x2: A):
PATTERN (r(x0, x1), r(x1, x2)):
(r(x0, x1) AND r(x1, x2)) => r(x0, x2) ;
ASSERT FORALL (x: A):
PATTERN (r(x, b)):
PATTERN (r(x, c)):
p(x) => q(x) ;
ASSERT EXISTS (y: A):
FORALL (x: A):
PATTERN (r(x, y), p(y)):
r(x, y) => q(x) ;
</pre><p>Patterns have no logical meaning: adding them to a formula does not change its semantics. Their purpose is purely operational, as explained in Section <a class="el" href="user_doc.html#user_doc_pres_lang_patterns">Instantiation Patterns</a>.</p>
<p>In addition to these constructs, <a class="el" href="namespaceCVC3.html">CVC3</a> also has a general mixfix conditional operator of the form </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathrm{IF}\ b\ \mathrm{THEN}\ t\ \mathrm{ELSIF}\ b_1\ \mathrm{THEN}\ t_1\ \ldots\ \mathrm{ELSIF}\ b_n\ \mathrm{THEN}\ t_n\ \mathrm{ELSE}\ t_{n+1}\ \mathrm{ENDIF} \]" src="form_81.png"/>
</p>
<p> with <img class="formulaInl" alt="$n \geq 0$" src="form_71.png"/> where <img class="formulaInl" alt="$b, b_1, \ldots, b_n$" src="form_82.png"/> are terms of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> and <img class="formulaInl" alt="$t, t_1, \ldots, t_n, t_{n+1}$" src="form_83.png"/> are terms of the same value type <img class="formulaInl" alt="$T$" src="form_3.png"/>:</p>
<pre class="fragment">% Conditional term
x,y,z,w:REAL;
t: REAL =
IF x > 0 THEN y
ELSIF x >= 1 THEN z
ELSIF x > 2 THEN w
ELSE 2/3 ENDIF;</pre><h3><a class="anchor" id="user_doc_pres_lang_expr_unint"></a>
User-defined Functions and Types</h3>
<p>The theory of user-defined functions is in effect a family of theories of equality parametrized by the atomic types and the free symbols a user can define during a run of <a class="el" href="namespaceCVC3.html">CVC3</a>.</p>
<p>The theory's function symbols consist of all <em>and only</em> the user-defined free symbols.</p>
<h3><a class="anchor" id="user_doc_pres_lang_expr_arith"></a>
Arithmetic</h3>
<p>The real arithmetic theory has predefined symbols for the usual arithmetic constants and operators over the type <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/>, each with the expected type: all numerals <code>0</code>, <code>1</code>, ..., as well as <code>-</code> (both unary and binary), <code>+</code>, <code>*</code>, <code>/</code>, <code><</code>, <code>></code>, <code><=</code>, <code>>=</code>. Rational values can be expressed in fractional form: e.g., 1/2, 3/4, etc.</p>
<p>The size of numerals used in the representation of natural and rational numbers is unbounded (or more accurately, bounded only by the amount of available memory).</p>
<h3><a class="anchor" id="user_doc_pres_lang_expr_bit"></a>
Bit vectors</h3>
<p>The bit vector theory has a large number of predefined function symbols denoting various bit vector operators. We describe the operators and their semantics informally below, often omitting a specification of their type, which should be easy to infer.</p>
<p>The operators' names are overloaded in the obvious way. For instance, the same name is used for each <img class="formulaInl" alt="$m,n > 0$" src="form_84.png"/> for the operator that takes a bit vector of size <img class="formulaInl" alt="$m$" src="form_85.png"/> and one of size <img class="formulaInl" alt="$n$" src="form_86.png"/> and returns their concatenation.</p>
<p>For each size <img class="formulaInl" alt="$n$" src="form_86.png"/>, there are <img class="formulaInl" alt="$2^n$" src="form_87.png"/> elements in the type <img class="formulaInl" alt="$\mathrm{BITVECTOR}(n)$" src="form_11.png"/>. These elements can be named using constant symbols or <em>bit vector constants</em>. Each element in the domain is named by two different constant symbols: once in binary and once in hexadecimal format. Binary constant symbols start with the characters <code>0bin</code> and continue with the representation of the vector in the usual binary format (as an <img class="formulaInl" alt="$n$" src="form_86.png"/>-string over the characters 0,1). Hexadecimal constant symbols start with the characters <code>0hex</code> and continue with the representation of the vector in usual hexadecimal format (as an <img class="formulaInl" alt="$n$" src="form_86.png"/>-string over the characters 0,...,9,a,...,f).</p>
<pre class="fragment">Binary constant Corresponding hexadecimal constant
-----------------------------------------------------------
0bin0000111101010000 0hex0f50
</pre><p>In the binary representation, the rightmost bit is the least significant bit (LSB) of the vector and the leftmost bit is the most significant bit (MSB). The index of the LSB in the bit vector is 0 and the index of the MSB is n-1 for an n-bit constant. This convention extends to all bit vector expressions in the natural way.</p>
<p>Bit vector operators are categorized into word-level, bitwise, arithmetic, and comparison operators.</p>
<pre class="fragment">WORD-LEVEL OPERATORS:
Description Symbol Example
====================================================================
Concatenation _ @ _ 0bin01@0bin0 (= 0bin010)
Extraction _ [i:j] 0bin0011[3:1] (= 0bin001)
Left shift _ << k 0bin0011 << 3 (= 0bin0011000)
Right shift _ >> k 0bin1000 >> 3 (= 0bin0001)
Sign extension SX(_,k) SX(0bin100, 5) (= 0bin11100)
Zero extension BVZEROEXTEND(_,k) BVZEROEXTEND(0bin1,3) (= 0bin0001)
Repeat BVREPEAT(_,k) BVREPEAT(0bin10,3) (= 0bin101010)
Rotate left BVROTL(_,k) BVROTL(0bin101,1) (= 0bin011)
Rotate right BVROTR(_,k) BVROTR(0bin101,1) (= 0bin110)
</pre><p>For each <img class="formulaInl" alt="$m,n > 0$" src="form_84.png"/> there is</p>
<ul>
<li>one infix concatenation operator, taking an <img class="formulaInl" alt="$m$" src="form_85.png"/>-bit vector <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v_2$" src="form_89.png"/> and returning the <img class="formulaInl" alt="$(m+n)$" src="form_90.png"/>-bit concatenation of <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>;</li>
<li>one postfix extraction operator <img class="formulaInl" alt="$[i:j]$" src="form_91.png"/> for each <img class="formulaInl" alt="$i, j$" src="form_92.png"/> with <img class="formulaInl" alt="$n > i >= j >= 0$" src="form_93.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$(i-j+1)$" src="form_95.png"/>-bit subvector of <img class="formulaInl" alt="$v$" src="form_94.png"/> at positions <img class="formulaInl" alt="$i$" src="form_96.png"/> through <img class="formulaInl" alt="$j$" src="form_97.png"/> (inclusive);</li>
<li>one postfix left shift operator <img class="formulaInl" alt="$<< k$" src="form_98.png"/> for each <img class="formulaInl" alt="$k >= 0$" src="form_99.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$(n+k)$" src="form_100.png"/>-bit concatenation of <img class="formulaInl" alt="$v$" src="form_94.png"/> with the <img class="formulaInl" alt="$k$" src="form_58.png"/>-bit zero vector;</li>
<li>one postfix right shift operator <img class="formulaInl" alt="$>> k$" src="form_101.png"/> for each <img class="formulaInl" alt="$k >= 0$" src="form_99.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit concatenation of the <img class="formulaInl" alt="$k$" src="form_58.png"/>-bit zero bit vector with <img class="formulaInl" alt="$v[n-1:k]$" src="form_102.png"/>;</li>
<li>one mixfix sign extension operator <img class="formulaInl" alt="$\mathrm{SX}(\_, k)$" src="form_103.png"/> for each <img class="formulaInl" alt="$k >= n$" src="form_104.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$k$" src="form_58.png"/>-bit concatenation of <img class="formulaInl" alt="$k-n$" src="form_105.png"/> copies of the MSB of <img class="formulaInl" alt="$v$" src="form_94.png"/> and <img class="formulaInl" alt="$v$" src="form_94.png"/>.</li>
<li>one mixfix zero extension operator <img class="formulaInl" alt="$\mathrm{BVZEROEXTEND}(\_, k)$" src="form_106.png"/> for each <img class="formulaInl" alt="$k >= 1$" src="form_107.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$n+k$" src="form_108.png"/>-bit concatenation of <img class="formulaInl" alt="$k$" src="form_58.png"/> zeroes and <img class="formulaInl" alt="$v$" src="form_94.png"/>.</li>
<li>one mixfix repeat operator <img class="formulaInl" alt="$\mathrm{BVREPEAT}(\_, k)$" src="form_109.png"/> for each <img class="formulaInl" alt="$k >= 1$" src="form_107.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$n*k$" src="form_110.png"/>-bit concatenation of <img class="formulaInl" alt="$k$" src="form_58.png"/> copies of <img class="formulaInl" alt="$v$" src="form_94.png"/>.</li>
<li>one mixfix rotate left operator <img class="formulaInl" alt="$\mathrm{BVROTL}(\_, k)$" src="form_111.png"/> for each <img class="formulaInl" alt="$k >= 0$" src="form_99.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$(n)$" src="form_112.png"/>-bit vector obtained by rotating the bits of <img class="formulaInl" alt="$v$" src="form_94.png"/> left <img class="formulaInl" alt="$k$" src="form_58.png"/> times, where a single rotation means removing the MSB and concatenating it as the new LSB.</li>
<li>one mixfix rotate right operator <img class="formulaInl" alt="$\mathrm{BVROTR}(\_, k)$" src="form_113.png"/> for each <img class="formulaInl" alt="$k >= 0$" src="form_99.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$(n)$" src="form_112.png"/>-bit vector obtained by rotating the bits of <img class="formulaInl" alt="$v$" src="form_94.png"/> right <img class="formulaInl" alt="$k$" src="form_58.png"/> times, where a single rotation means removing the LSB and concatenating it as the new MSB.</li>
</ul>
<pre class="fragment">BITWISE OPERATORS:
Description Symbol
==============================
Bitwise AND _ & _
Bitwise OR _ | _
Bitwise NOT ~ _
Bitwise XOR BVXOR(_,_)
Bitwise NAND BVNAND(_,_)
Bitwise NOR BVNOR(_,_)
Bitwise XNOR BVXNOR(_,_)
Bitwise Compare BVCOMP(_,_)
</pre><p>For each <img class="formulaInl" alt="$n > 0$" src="form_12.png"/> there are operators with the names and syntax above, performing the usual bitwise Boolean operations on <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit arguments. All produce <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit results except for <img class="formulaInl" alt="$\mathrm{BVCOMP}$" src="form_114.png"/> which always produces a 1-bit result: <img class="formulaInl" alt="$\mathrm{0bin1}$" src="form_115.png"/> if its two arguments are equal and <img class="formulaInl" alt="$\mathrm{0bin0}$" src="form_116.png"/> otherwise.</p>
<pre class="fragment">ARITHMETIC OPERATORS:
Description Symbol
========================================
Bit vector addition BVPLUS(k,_,_,...)
Bit vector multiplication BVMULT(k,_,_)
Bit vector negation BVUMINUS(_)
Bit vector subtraction BVSUB(k,_,_)
Bit vector left shift BVSHL(_,_)
Bit vector arith shift right BVASHR(_,_)
Bit vector logic shift right BVLSHR(_,_)
Bit vector unsigned divide BVUDIV(_,_)
Bit vector signed divide BVSDIV(_,_)
Bit vector unsigned remainder BVUREM(_,_)
Bit vector signed remainder BVSREM(_,_)
Bit vector signed modulus BVSMOD(_,_)
</pre><p>For each <img class="formulaInl" alt="$n > 0$" src="form_12.png"/> and <img class="formulaInl" alt="$k > 0$" src="form_117.png"/> there is</p>
<ul>
<li>one addition operator <img class="formulaInl" alt="$\mathrm{BVPLUS}(k,\_, \_, \ldots)$" src="form_118.png"/>, taking two or more bit vectors of arbitrary size, and returning the <img class="formulaInl" alt="$(k)$" src="form_119.png"/> least significant bits of their sum.</li>
<li>one multiplication operator <img class="formulaInl" alt="$\mathrm{BVMULT}(k,\_, \_)$" src="form_120.png"/>, taking two bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$k$" src="form_58.png"/> least significant bits of their product.</li>
<li>one prefix negation operator <img class="formulaInl" alt="$\mathrm{BVUMINUS}(\_)$" src="form_121.png"/>, taking an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v$" src="form_94.png"/> and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$\mathrm{BVPLUS}(n,\verb|~|v,\mathrm{0bin1})$" src="form_122.png"/>.</li>
<li>one subtraction operator <img class="formulaInl" alt="$\mathrm{BVSUB}(k,\_, \_)$" src="form_123.png"/>, taking two bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$k$" src="form_58.png"/>-bit vector <img class="formulaInl" alt="$\mathrm{BVPLUS}(k,v_1,\mathrm{BVUMINUS}(v'))$" src="form_124.png"/> where <img class="formulaInl" alt="$v'$" src="form_125.png"/> is <img class="formulaInl" alt="$v_2$" src="form_89.png"/> if the size of <img class="formulaInl" alt="$v_2$" src="form_89.png"/> is greater than or equal to <img class="formulaInl" alt="$k$" src="form_58.png"/>, and <img class="formulaInl" alt="$v_2$" src="form_89.png"/> extended to size <img class="formulaInl" alt="$k$" src="form_58.png"/> by concatenating zeroes in the most significant bits otherwise.</li>
<li>one left shift operator <img class="formulaInl" alt="$\mathrm{BVSHL}(\_, \_)$" src="form_126.png"/>, taking two <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector obtained by creating a vector of zeroes whose length is the value of <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, concatenating this vector onto the least significant bits of <img class="formulaInl" alt="$v_1$" src="form_88.png"/>, and then taking the least significant <img class="formulaInl" alt="$n$" src="form_86.png"/> bits of the result.</li>
<li>one arithmetic shift right operator <img class="formulaInl" alt="$\mathrm{BVASHR}(\_, \_)$" src="form_127.png"/>, taking two <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector obtained by creating a vector whose length is the value of <img class="formulaInl" alt="$v_2$" src="form_89.png"/> and each of whose bits has the same value as the MSB of <img class="formulaInl" alt="$v_1$" src="form_88.png"/>, concatenating this vector onto the most significant bits of <img class="formulaInl" alt="$v_1$" src="form_88.png"/>, and then taking the most significant <img class="formulaInl" alt="$n$" src="form_86.png"/> bits of the result.</li>
<li>one logical shift right operator <img class="formulaInl" alt="$\mathrm{BVLSHR}(\_, \_)$" src="form_128.png"/>, taking two <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector obtained by creating a vector of zeroes whose length is the value of <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, concatenating this vector onto the most significant bits of <img class="formulaInl" alt="$v_1$" src="form_88.png"/>, and then taking the most significant <img class="formulaInl" alt="$n$" src="form_86.png"/> bits of the result.</li>
<li>one unsigned integer division operator <img class="formulaInl" alt="$\mathrm{BVUDIV}(\_, \_)$" src="form_129.png"/>, taking two <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vectors <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and returning the <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector that is the largest integer value that can be multiplied by the integer value of <img class="formulaInl" alt="$v_2$" src="form_89.png"/> to obtain an integer less than or equal to the integer value of <img class="formulaInl" alt="$v_1$" src="form_88.png"/>.</li>
<li>one signed integer division operator <img class="formulaInl" alt="$\mathrm{BVSDIV}(\_, \_)$" src="form_130.png"/>.</li>
<li>one unsigned integer remainder operator <img class="formulaInl" alt="$\mathrm{BVUREM}(\_, \_)$" src="form_131.png"/>.</li>
<li>one signed integer remainder operator <img class="formulaInl" alt="$\mathrm{BVSREM}(\_, \_)$" src="form_132.png"/> (sign follows dividend).</li>
<li>one signed integer modulus operator <img class="formulaInl" alt="$\mathrm{BVSMOD}(\_, \_)$" src="form_133.png"/> (sign follows divisor).</li>
</ul>
<p>For precise definitions of the last four operators, we refer the reader to the equivalent operators defined in the SMT-LIB QF_BV logic (<a class="el" href="user_doc.html#user_doc_smtlib_lang">SMT-LIB Input Language</a>).</p>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> does not have dedicated operators for multiplexers. However, specific multiplexers can be easily defined with the aid of conditional terms.</p>
<pre class="fragment">% Example of 2-to-1 multiplexer
mp: (BITVECTOR(1), BITVECTOR(1), BITVECTOR(1)) -> BITVECTOR(1) =
LAMBDA (s,x,y : BITVECTOR(1)): IF s = 0bin0 THEN x ELSE y ENDIF;
</pre><p>In addition to equality and disequality, <a class="el" href="namespaceCVC3.html">CVC3</a> provides the following comparison operators.</p>
<pre class="fragment">COMPARISON OPERATORS:
Description Symbol
===================================
Less than BVLT(_,_)
Less than or equal to BVLE(_,_)
Greater than BVGT(_,_)
Greater than equal to BVGE(_,_)
Signed less than BVSLT(_,_)
Signed less than or equal to BVSLE(_,_)
Signed greater than BVSGT(_,_)
Signed greater than equal to BVSGE(_,_)
</pre><p>For each <img class="formulaInl" alt="$m, n > 0$" src="form_134.png"/> there is</p>
<ul>
<li>one prefix "less than" operator <img class="formulaInl" alt="$\mathrm{BVLT}(\_, \_)$" src="form_135.png"/>, taking an <img class="formulaInl" alt="$m$" src="form_85.png"/>-bit vector <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and having the value <img class="formulaInl" alt="$\mathrm{TRUE}$" src="form_136.png"/> iff the zero-extension of <img class="formulaInl" alt="$v_1$" src="form_88.png"/> to <img class="formulaInl" alt="$k$" src="form_58.png"/> bits is less than the zero-extension of <img class="formulaInl" alt="$v_2$" src="form_89.png"/> to <img class="formulaInl" alt="$k$" src="form_58.png"/> bits, where <img class="formulaInl" alt="$k$" src="form_58.png"/> is the maximum of <img class="formulaInl" alt="$m$" src="form_85.png"/> and <img class="formulaInl" alt="$n$" src="form_86.png"/>.</li>
<li>one prefix "less than or equal to" operator <img class="formulaInl" alt="$\mathrm{BVLE}(\_, \_)$" src="form_137.png"/>, taking an <img class="formulaInl" alt="$m$" src="form_85.png"/>-bit vector <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and having the value <img class="formulaInl" alt="$\mathrm{TRUE}$" src="form_136.png"/> iff the zero-extension of <img class="formulaInl" alt="$v_1$" src="form_88.png"/> to <img class="formulaInl" alt="$k$" src="form_58.png"/> bits is less than or equal to the zero-extension of <img class="formulaInl" alt="$v_2$" src="form_89.png"/> to <img class="formulaInl" alt="$k$" src="form_58.png"/> bits, where <img class="formulaInl" alt="$k$" src="form_58.png"/> is the maximum of <img class="formulaInl" alt="$m$" src="form_85.png"/> and <img class="formulaInl" alt="$n$" src="form_86.png"/>.</li>
<li>one prefix "greater than" operator <img class="formulaInl" alt="$\mathrm{BVGT}(\_, \_)$" src="form_138.png"/>, taking an <img class="formulaInl" alt="$m$" src="form_85.png"/>-bit vector <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and having the same value as <img class="formulaInl" alt="$\mathrm{BVLT}(v_2, v_1)$" src="form_139.png"/>.</li>
<li>one prefix "greater than or equal to" operator <img class="formulaInl" alt="$\mathrm{BVGE}(\_, \_)$" src="form_140.png"/>, taking an <img class="formulaInl" alt="$m$" src="form_85.png"/>-bit vector <img class="formulaInl" alt="$v_1$" src="form_88.png"/> and an <img class="formulaInl" alt="$n$" src="form_86.png"/>-bit vector <img class="formulaInl" alt="$v_2$" src="form_89.png"/>, and having the same value as <img class="formulaInl" alt="$\mathrm{BVLE}(v_2, v_1)$" src="form_141.png"/>.</li>
</ul>
<p>The signed operators are similar except that the values being compared are considered to be signed bit vector representations (in 2's complement) of integers.</p>
<p>Following are some example <a class="el" href="namespaceCVC3.html">CVC3</a> input formulas involving bit vector expressions</p>
<p>Example 1 illustrates the use of arithmetic, word-level and bitwise NOT operations:</p>
<pre class="fragment">x : BITVECTOR(5);
y : BITVECTOR(4);
yy : BITVECTOR(3);
QUERY
BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;
</pre><p>Example 2 illustrates the use of arithmetic, word-level and multiplexer terms:</p>
<pre class="fragment">bv : BITVECTOR(10);
a : BOOLEAN;
QUERY
0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
AND
0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ;
</pre><p>Example 3 illustrates the use of bitwise operations:</p>
<pre class="fragment">x, y, z, t, q : BITVECTOR(1024);
ASSERT x = ~x;
ASSERT x&y&t&z&q = x;
ASSERT x|y = t;
ASSERT BVXOR(x,~x) = t;
QUERY FALSE;
</pre><p>Example 4 illustrates the use of predicates and all the arithmetic operations:</p>
<pre class="fragment">x, y : BITVECTOR(4);
ASSERT x = 0hex5;
ASSERT y = 0bin0101;
QUERY
BVMULT(8,x,y)=BVMULT(8,y,x)
AND
NOT(BVLT(x,y))
AND
BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
AND
x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1)) ;
</pre><p>Example 5 illustrates the use of shift functions</p>
<pre class="fragment">x, y : BITVECTOR(8);
z, t : BITVECTOR(12);
ASSERT x = 0hexff;
ASSERT z = 0hexff0;
QUERY z = x << 4;
QUERY (z >> 4)[7:0] = x;
</pre><h3><a class="anchor" id="user_doc_pres_lang_expr_arr"></a>
Arrays</h3>
<p>The theory of arrays is a parametric theory of (total) unary functions. It comes equipped with polymorphic selection and update operators, respectively </p>
<center> <img class="formulaInl" alt="$\_[\_]$" src="form_142.png"/> and <img class="formulaInl" alt="$\_\ \mathrm{WITH}\ [\_]\ := \_$" src="form_143.png"/> </center><p> with the usual semantics. For each <em>index</em> type <img class="formulaInl" alt="$T_1$" src="form_22.png"/> and <em>element</em> type <img class="formulaInl" alt="$T_2$" src="form_23.png"/>, the first operator maps an array from <img class="formulaInl" alt="$T_1$" src="form_22.png"/> to <img class="formulaInl" alt="$T_2$" src="form_23.png"/> and an index into it (i.e., a value of type <img class="formulaInl" alt="$T_1$" src="form_22.png"/>) to the element of type <img class="formulaInl" alt="$T_2$" src="form_23.png"/> "stored" into the array at that index. The second maps an array <img class="formulaInl" alt="$a$" src="form_144.png"/> from <img class="formulaInl" alt="$T_1$" src="form_22.png"/> to <img class="formulaInl" alt="$T_2$" src="form_23.png"/>, an index <img class="formulaInl" alt="$i$" src="form_96.png"/>, and a <img class="formulaInl" alt="$T_2$" src="form_23.png"/>-element <img class="formulaInl" alt="$e$" src="form_145.png"/> to the array that stores <img class="formulaInl" alt="$e$" src="form_145.png"/> at index <img class="formulaInl" alt="$i$" src="form_96.png"/> and is otherwise identical to <img class="formulaInl" alt="$a$" src="form_144.png"/>.</p>
<p>Since arrays are just maps, equality between them is <em>extensional</em>: for two arrays of the same type to be different they have to store differ elements in at least one place.</p>
<p>Sequential updates can be chained with the syntax <img class="formulaInl" alt="$\_\ \mathrm{WITH}\ [\_]\ := \_, \ldots, [\_]\ := \_$" src="form_146.png"/>.</p>
<pre class="fragment">A: TYPE = ARRAY INT OF REAL;
a: A;
i: INT = 4;
% selection:
elem: REAL = a[i];
% update
a1: A = a WITH [10] := 1/2;
% sequential update
% (syntactic sugar for (a WITH [10] := 2/3) WITH [42] := 3/2)
a2: A = a WITH [10] := 2/3, [42] := 3/2;
</pre><h3><a class="anchor" id="user_doc_pres_lang_expr_dat"></a>
Datatypes</h3>
<p>The theory of datatypes is in fact a <em>family</em> of theories parametrized by a datatype declaration specifying constructors and selectors for a particular datatype.</p>
<p>No built-in operators other than equality and disequality are provided for this family in the presentation language. Each datatype declaration, however, generates constructor, selector and tester operators as described in Section <a class="el" href="user_doc.html#user_doc_pres_lang_data_types">Inductive Data Types</a>.</p>
<h3><a class="anchor" id="user_doc_pres_lang_expr_rec_tup"></a>
Tuples and Records</h3>
<p>Although they are currently implemented separately in <a class="el" href="namespaceCVC3.html">CVC3</a>, semantically both records and tuples can be seen as special instances of datatypes. In fact, a record of type <img class="formulaInl" alt="$[\# l_0:T_0, \ldots, l_n:T_n \#]$" src="form_147.png"/> could be equivalently modeled as, say, the datatype </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \begin{array}{l} \mathrm{DATATYPE} \\ \ \ \mathrm{Record} = \mathit{rec}(l_0:T_0, \ldots, l_n:T_n) \\ \mathrm{END}; \end{array} \]" src="form_148.png"/>
</p>
<p>Tuples could be seen in turn as special cases of records where the field names are the numbers from 0 to the length of the tuple minus 1. Currently, however, tuples and records have their own syntax for constructor and selector operators.</p>
<p>Records of type <img class="formulaInl" alt="$[\# l_0:T_0, \ldots, l_n:T_n \#]$" src="form_147.png"/> have the associated built-in constructor <img class="formulaInl" alt="$(\#\ l_0 := \_, \ldots, l_n := \_\ \#)$" src="form_149.png"/> whose arguments must be terms of type <img class="formulaInl" alt="$T_0, \ldots, T_n$" src="form_150.png"/>, respectively.</p>
<p>Tuples of type <img class="formulaInl" alt="$[\ T_0, \ldots, T_n\ ]$" src="form_151.png"/> have the associated built-in constructor <img class="formulaInl" alt="$(\ \_, \ldots, \_\ )$" src="form_152.png"/> whose arguments must be terms of type <img class="formulaInl" alt="$T_0, \ldots, T_n$" src="form_150.png"/>, respectively.</p>
<p>The selector operators on records and tuples follows a dot notation syntax.</p>
<pre class="fragment">% Record construction and field selection
Item: TYPE = [# key: INT, weight: REAL #];
x: Item = (# key := 23, weight := 43/10 #);
k: INT = x.key;
v: REAL = x.weight;
% Tuple construction and projection
y: [REAL,INT,REAL] = ( 4/5, 9, 11/9 );
first_elem: REAL = y.0;
third_elem: REAL = y.2;
</pre><p>Differently from datatypes, records and tuples are also provided with built-in update operators similar in syntax and semantics to the update operator for arrays. More precisely, for each record type <img class="formulaInl" alt="$[\#\ l_0:T_0, \ldots, l_n:T_n\ \#]$" src="form_153.png"/> and each <img class="formulaInl" alt="$i=0, \ldots, n$" src="form_154.png"/>, <a class="el" href="namespaceCVC3.html">CVC3</a> provides the operator </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \_\ \mathrm{WITH}\ .l_i\ := \_ \]" src="form_155.png"/>
</p>
<p> The operator maps a record <img class="formulaInl" alt="$r$" src="form_156.png"/> of that type and a value <img class="formulaInl" alt="$v$" src="form_94.png"/> of type <img class="formulaInl" alt="$T_i$" src="form_46.png"/> to the record that stores <img class="formulaInl" alt="$v$" src="form_94.png"/> in field <img class="formulaInl" alt="$l_i$" src="form_157.png"/> and is otherwise identical to <img class="formulaInl" alt="$r$" src="form_156.png"/>. Analogously, for each tuple type <img class="formulaInl" alt="$[T_0, \ldots, T_n]$" src="form_158.png"/> and each <img class="formulaInl" alt="$i=0, \ldots, n$" src="form_154.png"/>, <a class="el" href="namespaceCVC3.html">CVC3</a> provides the operator </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \_\ \mathrm{WITH}\ .i\ := \_ \]" src="form_159.png"/>
</p>
<pre class="fragment">% Record updates
Item: TYPE = [# key: INT, weight: REAL #];
x: Item = (# key := 23, weight := 43/10 #);
x1: Item = x WITH .weight := 48;
% Tuple updates
Tup: TYPE = [REAL,INT,REAL];
y: Tup = ( 4/5, 9, 11/9 );
y1: Tup = y WITH .1 := 3;
</pre><p>Updates to a nested component can be combined in a single WITH operator:</p>
<pre class="fragment">Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #];
State: TYPE = [# pc: INT, cache: Cache #];
s0: State;
s1: State = s0 WITH .cache[10].data := 2/3;</pre><p>Note that, differently from updates on arrays, tuple and record updates are just additional syntactic sugar. For instance, the record <code>x1</code> and tuple <code>y1</code> defined above could have been equivalently defined as follows:</p>
<pre class="fragment">% Record updates
Item: TYPE = [# key: INT, weight: REAL #];
x: Item = (# key := 23, weight := 43/10 #);
x1: Item = (# key := x.key, weight := 48 #);
% Tuple updates
Tup: TYPE = [REAL,INT,REAL];
y: Tup = ( 4/5, 9, 11/9 );
y1: Tup = ( y.0, 3, y.1 );
</pre><h2><a class="anchor" id="user_doc_pres_lang_commands"></a>
Commands</h2>
<p>In addition to declarations of types and constants, the <a class="el" href="namespaceCVC3.html">CVC3</a> input language contains the following commands:</p>
<ul>
<li><code>ASSERT</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Add the formula <img class="formulaInl" alt="$F$" src="form_160.png"/> to the current logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>.</li>
<li><code>QUERY</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Check if the formula <img class="formulaInl" alt="$F$" src="form_160.png"/> is valid in the current logical context: <img class="formulaInl" alt="$\Gamma\models_T F$" src="form_161.png"/>.</li>
<li><code>CHECKSAT</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Check if the formula is satisfiable in the current logical context: <img class="formulaInl" alt="$\Gamma\cup\{F\} \not\models_T \mathit{false}$" src="form_162.png"/>.</li>
<li><code>WHERE</code> – Print all the assumptions in the current logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>.</li>
<li><code>COUNTEREXAMPLE</code> – After an invalid QUERY or satisfiable CHECKSAT, print the context that is a witness for invalidity/satisfiability.</li>
<li><code>COUNTERMODEL</code> – After an invalid QUERY or satisfiable CHECKSAT, print a model that makes the formula invalid/satisfiable. The model is in terms of concrete values for each free symbol.</li>
<li><code>CONTINUE</code> – Search for a counter-example different from the current one (after an invalid QUERY or satisfiable CHECKSAT).</li>
<li><code>RESTART</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Restart an invalid QUERY or satisfiable CHECKSAT with the additional assumption <img class="formulaInl" alt="$F$" src="form_160.png"/>.</li>
</ul>
<ul>
<li><code>PUSH</code> – Save (checkpoint) the current state of the system.</li>
<li><code>POP</code> – Restore the system to the state it was in right before the last call to <code>PUSH</code></li>
<li><code>POPTO</code> <img class="formulaInl" alt="$n$" src="form_86.png"/>– Restore the system to the state it was in right before the most recent call to <code>PUSH</code> made from stack level <img class="formulaInl" alt="$n$" src="form_86.png"/>. Note that the current stack level is printed as part of the output of the <code>WHERE</code> command.</li>
</ul>
<ul>
<li><code>TRANSFORM</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Simplify <img class="formulaInl" alt="$F$" src="form_160.png"/> and print the result.</li>
<li><code>PRINT</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> – Parse and print back the expression <img class="formulaInl" alt="$F$" src="form_160.png"/>.</li>
<li><code>OPTION</code> <em>option</em> <em>value</em> – Set the command-line option flag <em>option</em> to <em>value</em>. Note that <em>option</em> is given as a string enclosed in double-quotes and <em>value</em> as an integer.</li>
</ul>
<p>The remaining commands take a single argument, given as a string enclosed in double-quotes.</p>
<ul>
<li><code>TRACE</code> <em>flag</em> – Turn on tracing for the debug flag <em>flag</em>.</li>
<li><code>UNTRACE</code> <em>flag</em> – Turn off tracing for the debug flag <em>flag</em>.</li>
</ul>
<ul>
<li><code>ECHO</code> <em>string</em> – Print <em>string</em></li>
<li><code>INCLUDE</code> <em>filename</em> – Read commands from the file <em>filename</em>.</li>
</ul>
<p>Here, we explain some of the above commands in more detail.</p>
<h3><a class="anchor" id="user_doc_pres_lang_commands_query"></a>
QUERY</h3>
<p>The command <code>QUERY</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> invokes the core functionality of <a class="el" href="namespaceCVC3.html">CVC3</a> to check the validity of the formula <img class="formulaInl" alt="$F$" src="form_160.png"/> with respect to the assertions made thus far ( <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>). <img class="formulaInl" alt="$F$" src="form_160.png"/> should be a formula as described in <a class="el" href="user_doc.html#user_doc_pres_lang_expr">Terms and Formulas</a>.</p>
<p>There are three possible answers.</p>
<ul>
<li>When the answer is "Valid", this means that <img class="formulaInl" alt="$\Gamma \models_T F$" src="form_163.png"/>. After a valid query, the logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> is exactly as it was before the query.</li>
<li>When the answer is "Invalid", this means that <img class="formulaInl" alt="$\Gamma \not\models_T F$" src="form_164.png"/>. In other words, there is a model of <img class="formulaInl" alt="$T$" src="form_3.png"/> satisfying <img class="formulaInl" alt="$\Gamma \cup \{\neg F\}$" src="form_165.png"/>. After an invalid query, the logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> is augmented with new literals <img class="formulaInl" alt="$\Delta$" src="form_7.png"/> such that <img class="formulaInl" alt="$\Gamma\cup\Delta$" src="form_166.png"/> is consistent in the theory <img class="formulaInl" alt="$T$" src="form_3.png"/>, but <img class="formulaInl" alt="$\Gamma\cup\Delta\models_T \neg F$" src="form_167.png"/>. In fact, in this case <img class="formulaInl" alt="$\Gamma\cup\Delta$" src="form_166.png"/> <em>propositionally</em> satisfies <img class="formulaInl" alt="$\neg f$" src="form_168.png"/>. We call the new context <img class="formulaInl" alt="$\Gamma\cup\Delta$" src="form_166.png"/> a <em>counterexample</em> for <img class="formulaInl" alt="$F$" src="form_160.png"/>.</li>
<li>An answer of "Unknown" is very similar to an answer of "Invalid" in that additional literals are added to the context which propositionally falsify the query formula <img class="formulaInl" alt="$F$" src="form_160.png"/>. The difference is that because <a class="el" href="namespaceCVC3.html">CVC3</a> is incomplete for some theories, it cannot guarantee in this case that <img class="formulaInl" alt="$\Gamma\cup\Delta$" src="form_166.png"/> is actually consistent in <img class="formulaInl" alt="$T$" src="form_3.png"/>. The only sources of incompleteness in <a class="el" href="namespaceCVC3.html">CVC3</a> are non-linear arithmetic and quantifiers.</li>
</ul>
<p>Counterexamples can be printed out using <code>WHERE</code> or <code>COUNTEREXAMPLE</code> commands. <code>WHERE</code> always prints out all of <img class="formulaInl" alt="$\Gamma\cup C$" src="form_169.png"/>. <code>COUNTEREXAMPLE</code> may sometimes be more selective, printing a subset of those formulas from the context which are sufficient for a counterexample.</p>
<p>Since the QUERY command may modify the current context, if you need to check several formulas in a row in the same context, it is a good idea to surround every QUERY command by PUSH and POP in order to preserve the context:</p>
<pre class="fragment">PUSH;
QUERY <formula>;
POP;
</pre><h3><a class="anchor" id="user_doc_pres_lang_commands_checksat"></a>
CHECKSAT</h3>
<p>The command <code>CHECKSAT</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> behaves identically to <code>QUERY</code> <img class="formulaInl" alt="$\neg F$" src="form_170.png"/>.</p>
<h3><a class="anchor" id="user_doc_pres_lang_commands_restart"></a>
RESTART</h3>
<p>The command <code>RESTART</code> <img class="formulaInl" alt="$F$" src="form_160.png"/> can only be invoked after an invalid query. For example:</p>
<pre class="fragment">QUERY <formula>;
Invalid.
RESTART <formula2>;
</pre><p>The behavior of the above command will be identical to the following:</p>
<pre class="fragment">PUSH;
QUERY <formula>;
POP;
ASSERT <formula2>;
QUERY <formula>;
</pre><p>The advantage of using the <code>RESTART</code> command is that it may be much more efficient than the above command sequence. This is because when the <code>RESTART</code> command is used, <a class="el" href="namespaceCVC3.html">CVC3</a> will re-use what it has learned rather than starting over from scratch.</p>
<h2><a class="anchor" id="user_doc_pres_lang_patterns"></a>
Instantiation Patterns</h2>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> processes each universally quantified formula in the current context by generating <em>instances</em> of the formula obtained by replacing its universal variables with ground terms. Patterns restrict the choice of ground terms for the quantified variables, with the goal of controlling the potential explosion of ground instances. In essence, adding patterns to a formula is a way for the user to tell <a class="el" href="namespaceCVC3.html">CVC3</a> to focus only on certain instances which, in the user's opinion, will be most helpful during a proof.</p>
<p>In more detail, patterns have the following effect on formulas that are found in the logical context or get later added to it while <a class="el" href="namespaceCVC3.html">CVC3</a> is trying to prove the validity of some formula <img class="formulaInl" alt="$\varphi$" src="form_75.png"/>.</p>
<p>If a formula in the current context starts with an existential quantifier, <a class="el" href="namespaceCVC3.html">CVC3</a> Skolemizes it, that is, replaces it in the context by the formula obtained by substituting the existentially quantified variables by fresh constants and dropping the quantifier. Any patterns for the existential quantifier are simply ignored.</p>
<p>If a formula starts with a universal quantifier <img class="formulaInl" alt="$\mathrm{FORALL}\; (x_1:T_1, \ldots, x_n:T_n)$" src="form_171.png"/>, <a class="el" href="namespaceCVC3.html">CVC3</a> adds to the context a number of instances of the formula—with the goal of using them to prove the query <img class="formulaInl" alt="$\varphi$" src="form_75.png"/> valid. An instance is obtained by replacing each <img class="formulaInl" alt="$x_i$" src="form_172.png"/> with a ground term of the same type occurring in one of the formulas in the context, and dropping the universal quantifier. If <img class="formulaInl" alt="$x_i$" src="form_172.png"/> occurs in a pattern <img class="formulaInl" alt="$\mathrm{PATTERN}\; (t_1, \ldots, t_m)$" src="form_173.png"/> for the quantifier, it will be instantiated only with terms obtained by simultaneously matching all the terms in the pattern against ground terms in the current context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/>.</p>
<p>Specifically, the matching process produces one or more substitutions <img class="formulaInl" alt="$\sigma$" src="form_174.png"/> for the variables in <img class="formulaInl" alt="$(t_1, \ldots, t_m)$" src="form_175.png"/> which satisfy the following invariant: for each <img class="formulaInl" alt="$i = 1, \ldots, m$" src="form_176.png"/>, <img class="formulaInl" alt="$\sigma(t_i)$" src="form_177.png"/> is a ground term and there is a ground term <img class="formulaInl" alt="$s_i$" src="form_178.png"/> in <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> such that <img class="formulaInl" alt="$\Gamma \models_T \sigma(t_i) = s_i$" src="form_179.png"/>. The variables of <img class="formulaInl" alt="$(x_1:T_1, \ldots, x_n:T_n)$" src="form_180.png"/> that occur in the pattern are instantiated only with those substitutions (while any remaining variables are instantiated arbitrarily).</p>
<p>The Skolemized version or the added instances of a context formula may themselves start with a quantifier. The same instantiation process is applied to them too, recursively.</p>
<p>Note that the matching mechanism is not limited to syntactic matching but is modulo the equations asserted in the context. Because of decidability and/or efficiency limitations, the matching process is not exhaustive. <a class="el" href="namespaceCVC3.html">CVC3</a> will typically miss some substitutions that satisfy the invariant above. As a consequence, it might fail to prove the validity of the query formula <img class="formulaInl" alt="$\varphi$" src="form_75.png"/>, which makes <a class="el" href="namespaceCVC3.html">CVC3</a> incomplete for contexts containing quantified formulas. It should be noted though that exhaustive matching, which can be achieved simply by not specifying any patterns, does not yield completeness anyway since the instantiation of universal variables is still restricted to just the ground terms in the context (whereas in general additional ground terms might be needed).</p>
<h2><a class="anchor" id="user_doc_pres_lang_subtypes"></a>
Subtypes</h2>
<p><a class="el" href="namespaceCVC3.html">CVC3</a>'s language includes the definition of <em>subtypes</em> of value types by means of predicate subtyping.</p>
<p>A subtype <img class="formulaInl" alt="$T_p$" src="form_181.png"/> of a (sub)type <img class="formulaInl" alt="$T$" src="form_3.png"/> is defined as a subset of <img class="formulaInl" alt="$T$" src="form_3.png"/> that satisfies an associated predicate <img class="formulaInl" alt="$p$" src="form_182.png"/>. More precisely, if <img class="formulaInl" alt="$p$" src="form_182.png"/> is a term of type <img class="formulaInl" alt="$T \to \mathrm{BOOLEAN}$" src="form_183.png"/>, then for every model of <img class="formulaInl" alt="$p$" src="form_182.png"/> (among the models of <a class="el" href="namespaceCVC3.html">CVC3</a>'s built-in theories), <img class="formulaInl" alt="$T_P$" src="form_184.png"/> is the <em>extension</em> of <img class="formulaInl" alt="$p$" src="form_182.png"/>, that is, the set of all and only the elements of <img class="formulaInl" alt="$T$" src="form_3.png"/> that satisfy the predicate <img class="formulaInl" alt="$p$" src="form_182.png"/>.</p>
<p>Subtypes like <img class="formulaInl" alt="$T_p$" src="form_181.png"/> above can be defined by the user with a declaration of the form:</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p) \]" src="form_185.png"/>
</p>
<p>where <img class="formulaInl" alt="$p$" src="form_182.png"/> is either just a (previously declared) predicate symbol of type <img class="formulaInl" alt="$T \to \mathrm{BOOLEAN}$" src="form_183.png"/> or a lambda abstraction of the form <img class="formulaInl" alt="$\lambda x:T.\; \varphi$" src="form_186.png"/> where <img class="formulaInl" alt="$\varphi$" src="form_75.png"/> is any <a class="el" href="namespaceCVC3.html">CVC3</a> formula whose set of free variables contains at most <img class="formulaInl" alt="$x$" src="form_187.png"/>.</p>
<p>Here are some examples of subtype declarations:</p>
<pre class="fragment">Animal: TYPE;
fish : Animal;
is_fish: Animal -> BOOLEAN;
ASSERT is_fish(fish);
% Fish is a subtype of Animal:
Fish: TYPE = SUBTYPE(is_fish);
shark : Fish;
is_shark: Fish -> BOOLEAN;
ASSERT is_shark(shark);
% Shark is a subtype of Fish:
Shark: TYPE = SUBTYPE(is_shark);
% Subtypes of REAL
AllReals: TYPE = SUBTYPE(LAMBDA (x:REAL): TRUE);
NonNegReal: TYPE = SUBTYPE(LAMBDA (x:REAL): x >= 0);
% Subtypes of INT
DivisibleBy3: TYPE = SUBTYPE(LAMBDA (x:INT): EXISTS (y:INT): x = 3 * y);</pre><p><a class="el" href="namespaceCVC3.html">CVC3</a> provides integers as a built-in subtype <img class="formulaInl" alt="$INT$" src="form_188.png"/> of <img class="formulaInl" alt="$REAL$" src="form_189.png"/>. <img class="formulaInl" alt="$INT$" src="form_188.png"/> is a subtype and not a base type in order to allow mixed real/integer terms without having to use coercion functions such as <img class="formulaInl" alt="$\mathrm{int\_to\_real}:\mathrm{INT} \to \mathrm{REAL}$" src="form_190.png"/> <img class="formulaInl" alt="$\mathrm{real\_to\_int}:\mathrm{REAL} \to \mathrm{INT}$" src="form_191.png"/> between terms of the two types. It is <em>built-in</em> because it is not definable by means of a first-order predicate.</p>
<p>Note that, with the syntax introduced so far, it seems that it may be possible to define empty subtypes, that is, subtypes with no values at all. For example:</p>
<pre class="fragment">NoReals: TYPE = SUBTYPE(LAMBDA (x:REAL): FALSE);
</pre><p>However, any attempt to do this results in an error. This is because <a class="el" href="namespaceCVC3.html">CVC3</a>'s logic assumes types are not empty. In fact, each time a subtype <img class="formulaInl" alt="$S$" src="form_192.png"/> is declared <a class="el" href="namespaceCVC3.html">CVC3</a> tries to prove that the subtype is non-empty; more precisely, that it is non-empty in every model of the current context. This is done simply by attempting to prove the validity of a formula of the form <img class="formulaInl" alt="$\exists\, x:T.\; p(x)$" src="form_193.png"/> where <img class="formulaInl" alt="$T$" src="form_3.png"/> is the value type of which <img class="formulaInl" alt="$S$" src="form_192.png"/> is a subtype, and <img class="formulaInl" alt="$p$" src="form_182.png"/> is the predicate defining <img class="formulaInl" alt="$S$" src="form_192.png"/>. If <a class="el" href="namespaceCVC3.html">CVC3</a> succeeds, the declaration is accepted. If it fails, <a class="el" href="namespaceCVC3.html">CVC3</a> will issue a type exception and reject the declaration.</p>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> might fail to prove the non-emptyness of a subtype either because the type is indeed empty in some models or because of <a class="el" href="namespaceCVC3.html">CVC3</a>'s incompleteness over quantified formulas. Consider the following examples:</p>
<pre class="fragment">Animal: TYPE;
is_fish: Animal -> BOOLEAN;
% Fish is a subtype of Animal:
Fish: TYPE = SUBTYPE(is_fish);
Interval_0_1: TYPE = SUBTYPE(LAMBDA (x:REAL): 0 < x AND x < 1);
% Subtypes of [REAL, REAL]
StraightLine: TYPE = SUBTYPE(LAMBDA (x:[REAL,REAL]): 3*x.0 + 2*x.1 + 6 = 0);
% Constant ARRAY subtype
ConstArray: TYPE = SUBTYPE(LAMBDA (a: ARRAY INT OF REAL):
EXISTS (x:REAL): FORALL (i:INT): a[i] = x);
</pre><p>Each of these subtype declarations is rejected. For instance, the declaration of <code>Fish</code> is rejected because there are models of <a class="el" href="namespaceCVC3.html">CVC3</a>'s background theory in which <code>is_fish</code> has an empty extension. To fix that it is enough to introduce a free constant of type <code>Animal</code> and assert that it is a <code>Fish</code> as we did above.</p>
<p>In the case of <code>Interval_0_1</code> and <code>Straightline</code>, however, the type is indeed non-empty in every model, but <a class="el" href="namespaceCVC3.html">CVC3</a> is unable to prove it. In such cases, the user can help <a class="el" href="namespaceCVC3.html">CVC3</a> by explicitly providing a witness value for the subtype. This is done with this alternative syntax for subtype declarations:</p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ \mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p,t) \]" src="form_194.png"/>
</p>
<p>where <img class="formulaInl" alt="$p$" src="form_182.png"/> is again a unary predicate and <img class="formulaInl" alt="$t$" src="form_55.png"/> is a term (denoting an element) that satisfies <img class="formulaInl" alt="$p$" src="form_182.png"/>.</p>
<p>The following subtype declarations with witnesses are accepted by <a class="el" href="namespaceCVC3.html">CVC3</a>.</p>
<pre class="fragment">% Subtypes of REAL with witness
Interval_0_1: TYPE = SUBTYPE(LAMBDA (x:REAL): 0 < x AND x < 1, 1/2);
StraightLine: TYPE = SUBTYPE(LAMBDA (x:[REAL,REAL]): 3*x.0 + 2*x.1 + 6 = 0, (0, -3));
</pre><p>We observe that the declaration of <code>ConstArray</code> in the first example is rightly rejected under the empty context because the subtype can be empty in some models. However, even under contexts that exclude this possibility <a class="el" href="namespaceCVC3.html">CVC3</a> is still unable to to prove the subtype's non-emptyness. Again, a declaration with witness helps in this case. Example:</p>
<pre class="fragment">zero_array: ARRAY INT OF REAL;
ASSERT FORALL (i:INT): zero_array[i] = 0;
% At this point the context includes the constant array zero_array
% and the declaration below is accepted.
ConstArray: TYPE = SUBTYPE(LAMBDA (a: ARRAY INT OF REAL):
EXISTS (x:REAL): FORALL (i:INT): a[i] = x, zero_array);
</pre><p>Adding witnesses to declarations to overcome <a class="el" href="namespaceCVC3.html">CVC3</a>'s incompleteness is an adequate, practical solution in most cases.</p>
<p>For additional convenience (when defining array types, for example) <a class="el" href="namespaceCVC3.html">CVC3</a> has a special syntax for specifying subtypes that are finite ranges of <img class="formulaInl" alt="$INT$" src="form_188.png"/>. This is however just syntactic sugar.</p>
<pre class="fragment">% subrange type
FiniteRangeArray: TYPE = ARRAY [-10..10] OF REAL;
% equivalent but less readable formulations
FiniteRange: TYPE = SUBTYPE(LAMBDA (x:INT): -10 <= x AND x <= 10);
FiniteRangeArray2: TYPE = ARRAY FiniteRange OF REAL;
FiniteRangeArray3: TYPE = ARRAY SUBTYPE(LAMBDA (x:INT): -10 <= x AND x <= 10) OF REAL;
</pre><h3><a class="anchor" id="user_doc_pres_lang_subtyping"></a>
Subtype Checking</h3>
<p>The subtype relation between a subtype and its immediate supertype is transitive. This implies that every subtype is a subtype of some value type, and so every term can be given a unique value type. This is important because as far as type checking is concerned, subtypes are ignored by <a class="el" href="namespaceCVC3.html">CVC3</a>. By default, static type checking is enforced only at the level of maximal supertypes, and subtypes play a role only during validity checking.</p>
<p>In essence, for every ground term of the form <img class="formulaInl" alt="$f(t_1, \ldots, t_n)$" src="form_195.png"/> with <img class="formulaInl" alt="$i \geq 0$" src="form_196.png"/> in the logical context, whenever <img class="formulaInl" alt="$f$" src="form_43.png"/> has type <img class="formulaInl" alt="$(S_1, \ldots, S_n) \to S$" src="form_197.png"/> where <img class="formulaInl" alt="$S$" src="form_192.png"/> is a subtype defined by a predicate <img class="formulaInl" alt="$p$" src="form_182.png"/>, <a class="el" href="namespaceCVC3.html">CVC3</a> adds to the context the assertion <img class="formulaInl" alt="$p(f(t_1, \ldots, t_n))$" src="form_198.png"/> constraining <img class="formulaInl" alt="$f(t_1, \ldots, t_n)$" src="form_195.png"/> to be a value in <img class="formulaInl" alt="$S$" src="form_192.png"/>.</p>
<p>This leads to correct answers by <a class="el" href="namespaceCVC3.html">CVC3</a>, provided that all ground terms are <em>well-subtyped</em> in the logical context of the query; that is, if for all terms like <img class="formulaInl" alt="$f(t_1, \ldots, t_n)$" src="form_195.png"/> above the logical context entails that <img class="formulaInl" alt="$t_i$" src="form_45.png"/> is a value of <img class="formulaInl" alt="$S_i$" src="form_199.png"/>. When that is not the case, <a class="el" href="namespaceCVC3.html">CVC3</a> may return spurious countermodels to a query, that is, countermodels that do not respect the subtyping constraints.</p>
<p>For example, after the following declarations:</p>
<pre class="fragment">Pos: TYPE = SUBTYPE(LAMBDA (x: REAL): x > 0, 1);
Neg: TYPE = SUBTYPE(LAMBDA (x: REAL): x < 0, -1);
a: Pos;
b: REAL;
f: Pos -> Neg = LAMBDA (x:Pos): -x;
</pre><p><a class="el" href="namespaceCVC3.html">CVC3</a> will reply "Valid", as it should, to the command:</p>
<pre class="fragment">QUERY f(a) < 0;
</pre><p>However it will reply "Invalid" to the command:</p>
<pre class="fragment">QUERY f(b) < 0;
</pre><p>or to:</p>
<pre class="fragment">QUERY f(-4) < 0;
</pre><p>for that matter, instead of complaining in either case that the query is not well-subtyped. (The query is ill-subtyped in the first case because there are models of the empty context in which the constant <code>b</code> is a non-positive rational; in the second case because in all models of the context the term <code>-4</code> is non-positive.)</p>
<p>In contrast, the command sequence</p>
<pre class="fragment">ASSERT b > 2*a + 3;
QUERY f(b) < 0;
</pre><p>say, produces the correct expected answer because in this case <code>b</code> is indeed positive in every model of the logical context.</p>
<p>Semantically, <a class="el" href="namespaceCVC3.html">CVC3</a>'s behavior is justified as follows. Consider, just for simplicity (the general case is analogous), a function symbol <img class="formulaInl" alt="$f$" src="form_43.png"/> of type <img class="formulaInl" alt="$S_1 \to T_2$" src="form_200.png"/> where <img class="formulaInl" alt="$S_1$" src="form_201.png"/> is a subtype of some value type <img class="formulaInl" alt="$T_1$" src="form_22.png"/>. Instead of interpreting <img class="formulaInl" alt="$S_1$" src="form_201.png"/> as <em>partial</em> function that is total over <img class="formulaInl" alt="$S_1$" src="form_201.png"/> and <em>undefined</em> outside <img class="formulaInl" alt="$S_1$" src="form_201.png"/>, <a class="el" href="namespaceCVC3.html">CVC3</a>'s interprets it as a <em>total</em> function from <img class="formulaInl" alt="$T_1$" src="form_22.png"/> to <img class="formulaInl" alt="$T_2$" src="form_23.png"/> whose behavior outside <img class="formulaInl" alt="$S_1$" src="form_201.png"/> is specified in an arbitrary, but fixed, way. The specification of the behavior outside <img class="formulaInl" alt="$S_1$" src="form_201.png"/> is internal to <a class="el" href="namespaceCVC3.html">CVC3</a> and can, from case to case, go from being completely empty, which means that <a class="el" href="namespaceCVC3.html">CVC3</a> will allow any possible way to extend <img class="formulaInl" alt="$f$" src="form_43.png"/> from <img class="formulaInl" alt="$S_1$" src="form_201.png"/> to <img class="formulaInl" alt="$T_1$" src="form_22.png"/>, to strong enough to allow only one way to extend <img class="formulaInl" alt="$f$" src="form_43.png"/>. The choice depends just on internal implementation considerations, with the understanding that the user is not really interested in <img class="formulaInl" alt="$f$" src="form_43.png"/>'s behavior outside <img class="formulaInl" alt="$S_1$" src="form_201.png"/> anyway.</p>
<p>A simple example of this approach is given by the arithmetic division operation <code>/</code>. Mathematically division is a partial function from <img class="formulaInl" alt="$\mathrm{REAL} \times \mathrm{REAL}$" src="form_202.png"/> to <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/> undefined over pairs in <img class="formulaInl" alt="$\mathrm{REAL} \times \{0\}$" src="form_203.png"/>. <a class="el" href="namespaceCVC3.html">CVC3</a> views <code>/</code> as a total function from <img class="formulaInl" alt="$\mathrm{REAL} \times \mathrm{REAL}$" src="form_202.png"/> to <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/> that maps pairs in <img class="formulaInl" alt="$\mathrm{REAL} \times \{0\}$" src="form_203.png"/> to <img class="formulaInl" alt="$0$" src="form_204.png"/> and is defined as usual otherwise. In other words, <a class="el" href="namespaceCVC3.html">CVC3</a> extends the theory of rational numbers with the axiom <img class="formulaInl" alt="$\forall\; x:\mathrm{REAL}.\; x/0 = 0$" src="form_205.png"/>. Under this view, queries like</p>
<pre class="fragment">x: REAL;
QUERY x/0 = 0 ;
QUERY 3/x = 3/x ;
</pre><p>are perfectly legitimate. Indeed the first formula is valid because in each model of the empty context, <code>x/0</code> is interpreted as zero and <code>=</code> is interpreted as the identity relation. The second formula is valid, more generally, because for each interpretation of <code>x</code> the two arguments of <code>=</code> will evaluate to the same rational number. <a class="el" href="namespaceCVC3.html">CVC3</a> will answer accordingly in both cases.</p>
<p>While this behavior is logically correct, it may be counter-intuitive to users, especially in applications that intend to give <a class="el" href="namespaceCVC3.html">CVC3</a> only well-subtyped formulas. For these applications it is more useful to the user to get a type error from <a class="el" href="namespaceCVC3.html">CVC3</a> as soon as it receives an ill-subtyped assertion or query, such as for instance the two queries above. This feature is provided in <a class="el" href="namespaceCVC3.html">CVC3</a> by using the command-line option <code>+tcc</code>. The mechanism for checking well-subtypedness is described below.</p>
<h3><a class="anchor" id="user_doc_pres_lang_tccs"></a>
Type Correctness Conditions</h3>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> uses an algorithm based on Type Correctness Conditions, TCCs for short, to determine if a term or formula is well-subtyped. This of course requires first an adequate notion of well-subtypedness. To introduce that notion, let us start with the following definition where <img class="formulaInl" alt="$T$" src="form_3.png"/> is the union of <a class="el" href="namespaceCVC3.html">CVC3</a>'s background theories.</p>
<p>Let us say that a (well-typed) term <img class="formulaInl" alt="$t$" src="form_55.png"/> containing no proper subterms of type <img class="formulaInl" alt="$\mathrm{BOOLEAN}$" src="form_13.png"/> is <em>well-subtyped in a model <img class="formulaInl" alt="$M$" src="form_206.png"/></em> of <img class="formulaInl" alt="$T$" src="form_3.png"/> (assigning an interpretation to all the free symbols and free variables of <img class="formulaInl" alt="$t$" src="form_55.png"/>) if</p>
<ul>
<li><img class="formulaInl" alt="$t$" src="form_55.png"/> is a constant or a variable, or</li>
<li>it is of the form <img class="formulaInl" alt="$f(t_1, \ldots, t_n)$" src="form_195.png"/> where <img class="formulaInl" alt="$f$" src="form_43.png"/> has type <img class="formulaInl" alt="$(S_1, \ldots, S_n) \to S$" src="form_197.png"/> and each <img class="formulaInl" alt="$t_i$" src="form_45.png"/> is well-subtyped in <img class="formulaInl" alt="$M$" src="form_206.png"/> and interpreted as a value of <img class="formulaInl" alt="$S_i$" src="form_199.png"/>.</li>
</ul>
<p>Note that this inductive definition includes the case in which the term is an atomic formula. Then we can say that an atomic formula is well-subtyped in a logical context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> if it is well-subtyped in every model of <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> and <img class="formulaInl" alt="$T$" src="form_3.png"/>.</p>
<p>While this seems like a sensible definition of well-subtypedness for atomic formulas, it is not obvious how to extend it properly to non-atomic formulas. For example, defining a non-atomic formula to be well-subtyped in a model if all of its atoms are well-subtyped is too stringent. Perfectly reasonable formulas like </p>
<p class="formulaDsp">
<img class="formulaDsp" alt="\[ y > 0 \;\Rightarrow\; x/y = z \]" src="form_207.png"/>
</p>
<p> with <img class="formulaInl" alt="$x$" src="form_187.png"/>, <img class="formulaInl" alt="$y$" src="form_208.png"/>, and <img class="formulaInl" alt="$z$" src="form_209.png"/> free constants (or free variables) of type <img class="formulaInl" alt="$\mathrm{REAL}$" src="form_10.png"/>, say, would not be well-subtyped in the empty context because there are models of <img class="formulaInl" alt="$T$" src="form_3.png"/> in which the atom <img class="formulaInl" alt="$x/y = z$" src="form_210.png"/> is not well-subtyped (namely, those that interpret <img class="formulaInl" alt="$y$" src="form_208.png"/> as zero).</p>
<p>A better definition can be given by treating logical connectives <em>non-strictly</em> with respect to ill-subtypedness. More formally, but considering for simplicity only formulas built with atoms, negation and disjunction connectives, and existential quantifiers (the missing cases are analogous), we define a non-atomic formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> to be well-subtyped in a model <img class="formulaInl" alt="$M$" src="form_206.png"/> of <img class="formulaInl" alt="$T$" src="form_3.png"/> if one of the following holds:</p>
<ul>
<li><img class="formulaInl" alt="$\phi$" src="form_0.png"/> has the form <img class="formulaInl" alt="$\lnot \phi_1$" src="form_211.png"/> and <img class="formulaInl" alt="$\phi_1$" src="form_212.png"/> is well-subtyped in <img class="formulaInl" alt="$M$" src="form_206.png"/>;</li>
<li><img class="formulaInl" alt="$\phi$" src="form_0.png"/> has the form <img class="formulaInl" alt="$\phi_1 \lor \phi_2$" src="form_213.png"/> and (i) both <img class="formulaInl" alt="$\phi_1$" src="form_212.png"/> and <img class="formulaInl" alt="$\phi_2$" src="form_214.png"/> are well-subtyped in <img class="formulaInl" alt="$M$" src="form_206.png"/> or (ii) <img class="formulaInl" alt="$\phi_1$" src="form_212.png"/> holds and is well-subtyped in <img class="formulaInl" alt="$M$" src="form_206.png"/> or (iii) <img class="formulaInl" alt="$\phi_2$" src="form_214.png"/> holds and is well-subtyped in <img class="formulaInl" alt="$M$" src="form_206.png"/>;</li>
<li><img class="formulaInl" alt="$\phi$" src="form_0.png"/> has the form <img class="formulaInl" alt="$\exists\:x.\; \phi_1$" src="form_215.png"/> and (i) <img class="formulaInl" alt="$\phi_1$" src="form_212.png"/> holds and is well-subtyped in some model <img class="formulaInl" alt="$M'$" src="form_216.png"/> that differs from <img class="formulaInl" alt="$M$" src="form_206.png"/> at most in the interpretation of <img class="formulaInl" alt="$x$" src="form_187.png"/> or (ii) <img class="formulaInl" alt="$\phi_1$" src="form_212.png"/> is well-subtyped in every such model <img class="formulaInl" alt="$M'$" src="form_216.png"/>.</li>
</ul>
<p>In essence, this definition is saying that for well-subtypedness in a model it is irrelevant if a formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> has an ill-subtyped subformula, as long as the truth value of <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is independent from the truth value of that subformula.</p>
<p>Now we can say in general that a <a class="el" href="namespaceCVC3.html">CVC3</a> formula is <em>well-subtyped in a context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/></em> if it is well-subtyped in every model of <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> and <img class="formulaInl" alt="$T$" src="form_3.png"/>.</p>
<p>According to this definition, the previous formula <img class="formulaInl" alt="$y > 0 \;\Rightarrow\; x/y = z$" src="form_217.png"/>, which is equivalent to <img class="formulaInl" alt="$\lnot(y > 0) \;\lor\; x/y = z$" src="form_218.png"/>, is well-subtyped in the empty context. In fact, in all the models of <img class="formulaInl" alt="$T$" src="form_3.png"/> that interpret <img class="formulaInl" alt="$y$" src="form_208.png"/> as zero, the subformula <img class="formulaInl" alt="$\lnot(y > 0)$" src="form_219.png"/> is true and well-subtyped; in all the others, both <img class="formulaInl" alt="$\lnot(y > 0)$" src="form_219.png"/> and <img class="formulaInl" alt="$x/y = z$" src="form_210.png"/> are well-subtyped.</p>
<p>This notion of well-subtypedness has a number of properties that make it fairly robust. One is that it is invariant with respect to equivalence in a context: for every context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> and formulas <img class="formulaInl" alt="$\phi, \phi'$" src="form_220.png"/> such that <img class="formulaInl" alt="$\Gamma \models_T \phi \Leftrightarrow \phi'$" src="form_221.png"/>, the first formula is well-subtyped in <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> if and only if the second is.</p>
<p>Perhaps the most important property, however, is that the definition can be effectively reflected into <a class="el" href="namespaceCVC3.html">CVC3</a>'s logic itself: there is a procedure that for any <a class="el" href="namespaceCVC3.html">CVC3</a> formula <img class="formulaInl" alt="$\phi$" src="form_0.png"/> can compute a well-subtyped formula <img class="formulaInl" alt="$\Delta_\phi$" src="form_222.png"/>, a <em>type correctness condition</em> for <img class="formulaInl" alt="$\phi$" src="form_0.png"/>, such that <img class="formulaInl" alt="$\phi$" src="form_0.png"/> is well-subtyped in a context <img class="formulaInl" alt="$\Gamma$" src="form_1.png"/> if and only if <img class="formulaInl" alt="$\Gamma \models_T \Delta_\phi$" src="form_223.png"/>. This has the nice consequence that the very inference engine of <a class="el" href="namespaceCVC3.html">CVC3</a> can be used to check the well-subtypedness of <a class="el" href="namespaceCVC3.html">CVC3</a> formulas.</p>
<p>When called with the TCC option on (by using the command-line option <code>+tcc</code>), <a class="el" href="namespaceCVC3.html">CVC3</a> behaves as follows. Whenever it receives an ASSERT or QUERY command, the system computes the TCC of the asserted formula or query and checks its validity in the current context (for ASSERTs, before the formula is added to the logical context). If it is able to prove the TCC valid, it just adds the asserted formula to the context or checks the validity of the query formula. If it is unable to prove the TCC valid, it raises an ill-subtypedness exception and aborts.</p>
<p>It is worth pointing out that, since <a class="el" href="namespaceCVC3.html">CVC3</a> checks the validity of an asserted formula in the current logical context at the time of the assertion, the order in which formulas are asserted makes a difference. For instance, attempting to enter the following sequence of commands:</p>
<pre class="fragment">f: [0..100] -> INT;
x: [5..10];
y: REAL;
ASSERT f(y + 3/2) < 15;
ASSERT y + 1/2 = x;
</pre><p>results in a TCC failure for the first assertion because the context right before it does not entail that the term <code>y + 3/2</code> is in the range <code>0..100</code>. In contrast, the sequence</p>
<pre class="fragment">f: [0..100] -> INT;
x: [5..10];
y: REAL;
ASSERT y + 1/2 = x;
ASSERT f(y + 3/2) < 15;
</pre><p>is accepted because each of the formulas above is well-subtyped at the time of its assertion. Note that the assertion of both formulas together in the empty context with</p>
<pre class="fragment">ASSERT f(y + 3/2) < 15 AND y + 1/2 = x
</pre><p>or with</p>
<pre class="fragment">ASSERT y + 1/2 = x AND f(y + 3/2) < 15
</pre><p>is also accepted because the conjunction of the two formulas is well-subtyped in the empty context.</p>
<h1><a class="anchor" id="user_doc_smtlib_lang"></a>
SMT-LIB Input Language</h1>
<p><a class="el" href="namespaceCVC3.html">CVC3</a> is able to read and execute queries in the SMT-LIB format.</p>
<p>Specifically, when called with the option <code>-lang smt</code> it accepts as input an SMT-LIB <em>benchmark</em> belonging to one of the SMT-LIB <em>sublogics</em>. For a well-formed input benchmark, <a class="el" href="namespaceCVC3.html">CVC3</a> returns the string "sat", "unsat" or "unknown", depending on whether it can prove the benchmark satisfiable, unsatisfiable, or neither.</p>
<p>At the time of this writing <a class="el" href="namespaceCVC3.html">CVC3</a> supported all SMT-LIB sublogics.</p>
<p>We refer the reader to the <a href="http://www.smt-lib.org">SMT-LIB website</a> for information on SMT-LIB, its formats, its logics, and its on-line library of benchmarks. </p>
</div></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
