1/*! 2 3\page user_doc The CVC3 User's Manual 4 5<!--<b>Note:</b> This user manual is still under construction. Some newer features of CVC3 are not yet documented here. Please let us know if you have a question 6that is not answered here.--> 7 8<strong>Contents</strong> 9 10<ul> 11<li>\ref user_doc_what_is_cvc3</li> 12<li>\ref user_doc_command_line</li> 13<li>\ref user_doc_pres_lang 14 <ul> 15 <li>\ref user_doc_pres_lang_types</li> 16 <ul> 17 <li>\ref user_doc_pres_lang_real_type</li> 18 <li>\ref user_doc_pres_lang_bitvec_types</li> 19 <li>\ref user_doc_pres_lang_unint_types</li> 20 <li>\ref user_doc_pres_lang_bool_type</li> 21 <li>\ref user_doc_pres_lang_fun_types</li> 22 <li>\ref user_doc_pres_lang_array_types</li> 23 <li>\ref user_doc_pres_lang_tuple_types</li> 24 <li>\ref user_doc_pres_lang_record_types</li> 25 <li>\ref user_doc_pres_lang_data_types</li> 26 <li>\ref user_doc_pres_lang_typing</li> 27 </ul> 28 <li>\ref user_doc_pres_lang_expr 29 <ul> 30 <li>\ref user_doc_pres_lang_expr_logic</li> 31 <li>\ref user_doc_pres_lang_expr_unint</li> 32 <li>\ref user_doc_pres_lang_expr_arith</li> 33 <li>\ref user_doc_pres_lang_expr_bit</li> 34 <li>\ref user_doc_pres_lang_expr_arr</li> 35 <li>\ref user_doc_pres_lang_expr_dat</li> 36 <li>\ref user_doc_pres_lang_expr_rec_tup</li> 37 </ul> 38 </li> 39 <li>\ref user_doc_pres_lang_commands</li> 40 <ul> 41 <li>\ref user_doc_pres_lang_commands_query</li> 42 <li>\ref user_doc_pres_lang_commands_checksat</li> 43 <li>\ref user_doc_pres_lang_commands_restart</li> 44 </ul> 45 <li>\ref user_doc_pres_lang_patterns</li> 46 <li>\ref user_doc_pres_lang_subtypes 47 <ul> 48 <li>\ref user_doc_pres_lang_subtyping</li> 49 <li>\ref user_doc_pres_lang_tccs</li> 50 </ul> 51 </li> 52 </ul> 53</li> 54<li>\ref user_doc_smtlib_lang</li> 55</ul> 56 57\section user_doc_what_is_cvc3 What is CVC3? 58 59CVC3 is an automated <em>validity checker</em> for a many-sorted (i.e., typed) 60first-order logic with <em>built-in theories</em>, 61including some support for quantifiers, 62partial functions, and predicate subtypes. 63The current built-in theories are the theories of: 64<ul> 65<li> 66equality over <em>free</em> (aka <em>uninterpreted</em>) function and predicate symbols, 67</li> 68<li> 69real and integer linear arithmetic 70(with some support for non-linear arithmetic), 71</li> 72<li> 73bit vectors, 74</li> 75<li> 76arrays, 77</li> 78<li> 79tuples, 80</li> 81<li> 82records, 83</li> 84<li> 85user-defined inductive datatypes. 86</li> 87</ul> 88 89CVC3 checks whether a given formula \f$\phi\f$ is valid in 90the built-in theories under a given set \f$\Gamma\f$ of assumptions. 91More precisely, it checks whether 92\f[\Gamma\models_T \phi\f] 93that is, 94whether \f$\phi\f$ is a logical consequence of the union \f$T\f$ of 95the built-in theories and the set of formulas \f$\Gamma\f$. 96 97Roughly speaking, 98when \f$\phi\f$ is <em>universal</em> and all the formulas in \f$\Gamma\f$ 99are <em>existential</em> 100(i.e., when \f$\phi\f$ and \f$\Gamma\f$ contain at most universal, 101respectively existential, quantifiers), 102CVC3 is in fact a decision procedure: 103it is always guaranteed (well, modulo bugs and memory limits) to return a correct "valid" or 104"invalid" answer. 105In all other cases, CVC3 is sound but incomplete: 106it will never say that an invalid formula is valid 107but it may either never return or give up and return "unknown" 108in some cases when \f$\Gamma \models_T \phi\f$. 109 110 111When CVC3 returns "valid" it can return a formal proof of the validity 112of \f$\phi\f$ under the <em>logical context</em> \f$\Gamma\f$, 113together with the subset \f$\Gamma'\f$ of \f$\Gamma\f$ used 114in the proof, such that \f$\Gamma'\models_T \phi\f$. 115 116When CVC3 returns "invalid" it can return, in the current terminology, 117both a <em>counter-example</em> to \f$\phi\f$'s validity under \f$\Gamma\f$ 118and a <em>counter-model</em>. 119Both a counter-example and a counter-models are a set \f$\Delta\f$ of 120additional formulas consistent with \f$\Gamma\f$ in \f$T\f$, 121but entailing the negation of \f$\phi\f$. 122In formulas: 123<center> 124\f$\Gamma \cup \Delta \not\models_T \mathit{false}\f$ 125and 126\f$\Gamma \cup \Delta \models_T \lnot \phi\f$. 127</center> 128 129The difference is that a counter-model is given as a set of equations 130providing a concrete assignment of values for the free symbols in 131\f$\Gamma\f$ and \f$\phi\f$ 132(see \ref user_doc_pres_lang_commands_query for more details). 133 134CVC3 can be used in two modes: as a library 135or as a command-line executable (implemented as a command-line interface to 136the library). 137Interfaces to the library are available in C/C++, Java and .NET. 138This manual mainly describes the command-line interface on a unix-type platform. 139 140 141\section user_doc_command_line Running CVC3 from a Command Line 142 143Assuming you have properly installed CVC3 on your machine 144(check the \ref INSTALL section for that), 145you will have an executable file called <tt>cvc3</tt>. 146It reads the input (a sequence 147of commands) from the standard input and prints the results on the standard 148output. Errors and some other messages (e.g. debugging traces) are 149printed on the standard error. 150 151Typically, the input to <tt>cvc3</tt> is saved in a file and 152redirected to the executable, or given on a command line: 153 154\verbatim 155# Reading from standard input: 156 cvc3 < input-file.cvc 157# Reading directly from file: 158 cvc3 input-file.cvc 159\endverbatim 160 161Notice that, for efficiency, CVC3 uses input buffers, and the 162input is not always processed immediately after each command. 163Therefore, if you want to type the commands interactively and receive 164immediate feedback, use the <tt>+interactive</tt> option (can be 165shortened to <tt>+int</tt>): 166 167\verbatim 168 cvc3 +int 169\endverbatim 170 171Run <tt>cvc3 -h</tt> for more information on the available options. 172 173The command line front-end of CVC3 supports two input languages. 174<ul> 175<li> 176CVC3's own <em>presentation language</em> 177whose syntax was initially inspired by the PVS and SAL systems 178and is almost identical to the input language of CVC and CVC Lite, the 179predecessors of CVC3; 180</li> 181<li> 182the standard language promoted by the 183<a href="http://www.SMT-LIB.org">SMT-LIB initiative</a> for SMT-LIB benchmarks. 184</li> 185</ul> 186 187We describe the input languages next, concentrating mostly on the first. 188 189 190\section user_doc_pres_lang Presentation Input Language 191 192The input language consists of a sequence of symbol declarations and commands, 193each followed by a semicolon (<tt>;</tt>). 194 195Any text after the first occurrence of a percent character 196and to the end of the current line is a comment: 197 198\verbatim 199%%% This is a CVC3 comment 200\endverbatim 201 202 203\subsection user_doc_pres_lang_types Type system 204 205CVC3's type system includes a set of built-in types which can be expanded 206with additional user-defined types. 207 208The type system consists of 209<em>value</em> types, <em>non-value</em> types and <em>subtypes</em> of value types, 210all of which are interpreted as sets. 211For convenience, 212we will sometimes identify below the interpretation of a type with the type itself. 213 214 215 216Value types consist of <em>atomic</em> types and <em>structured</em> types. 217The atomic types are 218\f$\mathrm{REAL}\f$, 219\f$\mathrm{BITVECTOR}(n)\f$ for all \f$n > 0\f$, 220as well as 221user-defined atomic types (also called <em>uninterpreted</em> types). 222The structured types are 223<em>array</em>, 224<em>tuple</em>, and 225<em>record</em> types, 226as well as 227ML-style user-defined (inductive) <em>datatypes</em>. 228 229Non-value types consist of the type \f$\mathrm{BOOLEAN}\f$ and 230<em>function</em> types. Subtypes include the built-in subtype 231\f$\mathrm{INT}\f$ of \f$\mathrm{REAL}\f$ and are covered in the \ref 232user_doc_pres_lang_subtypes section below. 233 234 235\subsubsection user_doc_pres_lang_real_type REAL Type 236 237The \f$\mathrm{REAL}\f$ type is interpreted as the set of rational numbers. 238The name \f$\mathrm{REAL}\f$ is justified by the fact that a CVC3 formula is valid in 239the theory of rational numbers iff it is valid in the theory of real numbers. 240 241 242\subsubsection user_doc_pres_lang_bitvec_types Bit Vector Types 243 244For every positive numeral <i>n</i>, the type \f$\mathrm{BITVECTOR}(n)\f$ is interpreted 245as the set of all bit vectors of size <i>n</i>. 246 247 248\subsubsection user_doc_pres_lang_unint_types User-defined Atomic Types 249 250User-defined atomic types are each interpreted as a set of unspecified cardinality 251but disjoint from any other type. 252They are created by declarations like the following: 253 254\verbatim 255% User declarations of atomic types: 256 257MyBrandNewType: TYPE; 258 259Apples, Oranges: TYPE; 260\endverbatim 261 262 263\subsubsection user_doc_pres_lang_bool_type BOOLEAN Type 264 265The \f$\mathrm{BOOLEAN}\f$ type is, perhaps confusingly, the type of CVC3 formulas, 266not the two-element set of Boolean values. 267The fact that \f$\mathrm{BOOLEAN}\f$ is not a value type 268in practice means that it is not possible 269for function symbols in CVC3 to have a arguments of type \f$\mathrm{BOOLEAN}\f$. 270The reason is that 271CVC3 follows the two-tiered structure of classical first-order logic 272that distinguishes between formulas and terms, 273and allows terms to occur in formulas but not vice versa. 274(An exception is the IF-THEN-ELSE construct, see later.) 275The only difference is that, syntactically, formulas in CVC3 are terms of 276type \f$\mathrm{BOOLEAN}\f$. 277A function symbol <tt>f</tt> then <em>can</em> have \f$\mathrm{BOOLEAN}\f$ as 278its return type. 279But that is just CVC3's way, 280inherited from the previous systems of the CVC family, 281to say that <tt>f</tt> is a predicate symbol. 282 283<!-- 284CT: next line slightly reworded: 285--> 286CVC3 does have a type that behaves like a Boolean Value type, 287that is, a value type with only two elements 288and with the usual Boolean operations defined on it: 289it is <tt>BITVECTOR(1)</tt>. 290 291 292\subsubsection user_doc_pres_lang_fun_types Function Types 293 294All structured types are actually <em>families</em> of types. 295Function (\f$\to\f$) types are created by the mixfix type constructors 296 297\f[ 298\begin{array}{l} 299\_ \to \_ 300\\[1ex] 301(\ \_\ ,\ \_\ ) \to \_ 302\\[1ex] 303(\ \_\ ,\ \_\ ,\ \_\ ) \to \_ 304\\[1ex] 305\ldots 306\end{array} 307\f] 308 309whose arguments can be instantiated by any value (sub)type, 310with the addition that the last argument can also be \f$\mathrm{BOOLEAN}\f$. 311 312\verbatim 313% Function type declarations 314 315UnaryFunType: TYPE = INT -> REAL; 316BinaryFunType: TYPE = (REAL, REAL) -> ARRAY REAL OF REAL; 317TernaryFunType: TYPE = (REAL, BITVECTOR(4), INT) -> BOOLEAN; 318\endverbatim 319 320A function type of the form \f$(T_1, \ldots, T_n) \to T\f$ with \f$n > 0\f$ is interpreted 321as the set of all total functions 322from the Cartesian product \f$T_1 \times \cdots \times T_n\f$ to \f$T\f$ 323when \f$T\f$ is not \f$\mathrm{BOOLEAN}\f$. 324Otherwise, 325it is interpreted as the set of all relations over \f$T_1 \times \cdots \times T_n\f$ 326 327The example above also shows how to introduce <em>type names</em>. 328A name like <tt>UnaryFunType</tt> above is just an abbreviation 329for the type \f$\mathrm{INT} \to \mathrm{REAL}\f$ and can be used interchangeably with it. 330 331<br> 332In general, any type defined by a type expression <tt>E</tt> can be given a name 333with the declaration: 334 335\verbatim 336name : TYPE = E; 337\endverbatim 338 339 340\subsubsection user_doc_pres_lang_array_types Array Types 341 342Array types are created by the mixfix type constructors 343\f$\mathrm{ARRAY}\ \_\ \mathrm{OF}\ \_\f$ 344whose arguments can be instantiated by any value type. 345 346\verbatim 347T1 : TYPE; 348 349% Array types: 350 351ArrayType1: TYPE = ARRAY T1 OF REAL; 352ArrayType2: TYPE = ARRAY INT OF (ARRAY INT OF REAL); 353ArrayType3: TYPE = ARRAY [INT, INT] OF INT; 354\endverbatim 355 356An array type of the form \f$\mathrm{ARRAY}\ T_1\ \mathrm{OF}\ T_2\f$ is interpreted 357as the set of all total maps from \f$T_1\f$ to \f$T_2\f$. 358The main conceptual difference with the type \f$T_1 \to T_2\f$ is that 359arrays, contrary to functions, are first-class objects of the language: 360they can be arguments or results of functions. 361Moreover, array types come equipped with an update operation. 362 363 364\subsubsection user_doc_pres_lang_tuple_types Tuple Types 365 366Tuple types are created by the mixfix type constructors 367 368\f[ 369\begin{array}{l} 370[\ \_\ ] 371\\[1ex] 372[\ \_\ ,\ \_\ ] 373\\[1ex] 374[\ \_\ ,\ \_\ \ ,\ \_\ ] 375\\[1ex] 376\ldots 377\end{array} 378\f] 379 380whose arguments can be instantiated by any value type. 381 382\verbatim 383% Tuple declaration 384 385TupleType: TYPE = [ REAL, ArrayType1, [INT, INT] ]; 386 387\endverbatim 388 389A tuple type of the form \f$[T_1, \ldots, T_n]\f$ is interpreted 390as the Cartesian product \f$T_1 \times \cdots \times T_n\f$. 391Note that while the types \f$(T_1, \ldots, T_n) \to T\f$ and 392\f$[T_1 \times \cdots \times T_n] \to T\f$ are semantically equivalent, 393they are operationally different in CVC3. 394The first is the type of functions that take <em>n</em> arguments, 395while the second is the type of functions of <em>1</em> argument of type n-tuple. 396 397 398\subsubsection user_doc_pres_lang_record_types Record Types 399 400Similar to, but more general than tuple types, 401record types are created by type constructors of the form 402 403\f[ 404[\#\ l_1: \_\ ,\ \ldots\ ,\ l_n: \_\ \#] 405\f] 406 407where \f$n > 0\f$, 408\f$l_1,\ldots, l_n\f$ are field labels, 409and 410the arguments can be instantiated with any value types. 411 412\verbatim 413% Record declaration 414 415RecordType: TYPE = [# number: INT, value: REAL, info: TupleType #]; 416\endverbatim 417 418The order of the fields in a record type is meaningful. 419In other words, permuting the field names gives a different type. 420Note that records are 421<!-- 422CT: removed 423(at the moment) 424--> 425non-recursive. 426For instance, 427it is not possible to declare a record type called <tt>Person</tt> 428containing a field of type <tt>Person</tt>. 429Recursive types are provided in CVC3 as ML-style datatypes. 430 431 432\subsubsection user_doc_pres_lang_data_types Inductive Data Types 433 434Inductive datatypes are created by declarations of the form 435 436\f[ 437\begin{array}{l} 438\mathrm{DATATYPE} \\ 439\ \ \mathit{type\_name}_1 = C_{1,1} \mid C_{1,2} \mid \cdots \mid C_{1,m_1}, \\ 440\ \ \mathit{type\_name}_2 = C_{2,1} \mid C_{2,2} \mid \cdots \mid C_{2,m_2}, \\ 441\ \ \vdots \\ 442\ \ \mathit{type\_name}_n = C_{n,1} \mid C_{n,2} \mid \cdots \mid C_{n,m_n} \\ 443\mathrm{END}; 444\end{array} 445\f] 446 447Each of the \f$C_{ij}\f$ is either a constant symbol 448or an expression of the form 449 450\f[ 451\mathit{cons}(\ \mathit{sel}_1: T_1,\ \ldots,\ \mathit{sel}_k: T_k\ ) 452\f] 453 454where \f$T_1, \ldots, T_k\f$ are any value types or type names for value types, 455including any \f$\mathit{type\_name}_i\f$. 456Such declarations introduce for the datatype: 457- <em>constructor</em> symbols \f$cons\f$ of type 458 \f$(T_1, \ldots, T_k) \to \mathit{type\_name}_i\f$, 459- <em>selector</em> symbols \f$\mathit{sel}_j\f$ of type 460 \f$\mathit{type\_name}_i \to T_j\f$, 461 and 462- <em>tester</em> symbols \f$\mathit{is\_cons}\f$ of type 463 \f$\mathit{type\_name}_i \to \mathrm{BOOLEAN}\f$. 464 465Here are some examples of datatype declarations: 466 467\verbatim 468% simple enumeration type 469% implicitly defined are the testers: is_red, is_yellow and is_blue 470% (similarly for the other datatypes) 471 472DATATYPE 473 PrimaryColor = red | yellow | blue 474END; 475 476 477% infinite set of pairwise distinct values ...v(-1), v(0), v(1), ... 478 479DATATYPE 480 Id = v (id: INT) 481END; 482 483 484% ML-style integer lists 485 486DATATYPE 487 IntList = nil | cons (head: INT, tail: IntList) 488END; 489 490 491% ASTs 492 493DATATYPE 494 Term = var (index: INT) 495 | apply (arg_1: Term, arg_2: Term) 496 | lambda (arg: INT, body: Term) 497END; 498 499 500% Trees 501 502DATATYPE 503 Tree = tree (value: REAL, children: TreeList), 504 TreeList = nil_tl 505 | cons_tl (first_t1: Tree, rest_t1: TreeList) 506END; 507\endverbatim 508 509Constructor, selector and tester symbols defined for a datatype have global scope. 510So, for instance, it is not possible for two different datatypes to use 511the same name for a constructor. 512 513A datatype is interpreted as a term algebra constructed by the constructor symbols 514over some sets of generators. 515For example, the datatype <tt>IntList</tt> is interpreted as the set of 516all terms constructed with <tt>nil</tt> and <tt>cons</tt> over the integers. 517 518Because of this semantics, CVC3 allows only <em>inductive</em> datatypes, that is, datatypes 519whose values are essentially (labeled, ordered) finite trees. 520Infinite structures such as streams or 521even finite but cyclic ones such as circular lists are then excluded. 522For instance, 523none of the following declarations define inductive datatypes, 524and are rejected by CVC3: 525 526\verbatim 527DATATYPE 528 IntStream = s (first:INT, rest: IntStream) 529END; 530 531DATATYPE 532 RationalTree = node1 (first_child1: RationalTree) 533 | node2 (first_child2: RationalTree, second_child2:RationalTree) 534END; 535 536DATATYPE 537 T1 = c1 (s1: T2), 538 T2 = c2 (s2: T1) 539END; 540\endverbatim 541 542In concrete, 543a declaration of \f$n \geq 1\f$ datatypes \f$T_1, \ldots, T_n\f$ will be rejected 544if for any one of the types \f$T_1, \ldots, T_n\f$, it is impossible to build a 545finite term of that type using only the constructors of \f$T_1, \ldots, T_n\f$ and 546free constants of type other than \f$T_1, \ldots, T_n\f$. 547 548 549Datatypes are the only types for which 550the user also chooses names for the built-in operations defined on the type for: 551- constructing a value (with the constructors), 552- extracting components from a value (with the selectors), 553or 554- checking if a value was constructed with a certain constructor or not 555(with the testers). 556 557For all the other types, 558CVC3 provides predefined names 559for the built-in operations on the type. 560 561 562\subsubsection user_doc_pres_lang_typing Type Checking 563 564In essence, 565CVC3 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 566(the typing rules for formulas are analogous): 567 568- each variable has one associated (non-function) type, 569- each constant symbol has one associated (non-function) type, 570- each function symbol has one or more associated function types, 571- the type of a term consisting just of a variable or a constant symbol is 572 the type associated to that variable or constant symbol, 573- the term obtained by applying 574 a function symbol \f$f\f$ to the terms \f$t_1, \ldots, t_n\f$ is \f$T\f$ 575 if \f$f\f$ has type \f$(T_1, \ldots, T_n) \to T\f$ and 576 each \f$t_i\f$ has type \f$T_i\f$. 577 578Attempting to enter an ill-typed term will result in an error. 579 580The main difference with standard many-sorted logic is that some built-in symbols 581are parametrically polymorphic. 582For instance the function symbol for extracting the element of any array 583has type \f$(\mathit{ARRAY}\ T_1\ \mathit{OF}\ T_2,\; T_1) \to T_2\f$ 584for all types \f$T_1, T_2\f$ not containing function or predicate types. 585 586 587\subsection user_doc_pres_lang_expr Terms and Formulas 588 589In addition to type expressions, CVC3 has expressions 590for terms and formulas (i.e., terms of type \f$\mathrm{BOOLEAN}\f$). 591By and large, these are standard first-order terms 592built out of (typed) variables, 593predefined theory-specific operators, 594free (i.e., user-defined) function symbols, 595and quantifiers. 596Extensions include an if-then-else operator, 597lambda abstractions, and local symbol declarations, 598as illustrated below. 599Note that these extensions still keep CVC3's language first-order. 600In particular, lambda abstractions are restricted to take and return 601only terms of a value type. 602Similarly, quantifiers can only quantify variables of a value type. 603 604Free function symbols include <em>constant</em> symbols and 605<em>predicate</em> symbols, 606respectively nullary function symbols and 607function symbols with a \f$\mathrm{BOOLEAN}\f$ return type. 608Free symbols are introduced with global declarations of the form 609\f$f_1, \ldots, f_m: T;\f$ 610where \f$m > 0\f$, 611\f$f_i\f$ are the names of the symbols and \f$T\f$ is their type: 612 613\verbatim 614% integer constants 615 616a, b, c: INT; 617 618% real constants 619 620x,y,z: REAL; 621 622% unary function 623 624f1: REAL -> REAL; 625 626% binary function 627 628f2: (REAL, INT) -> REAL; 629 630% unary function with a tuple argument 631 632f3: [INT, REAL] -> BOOLEAN; 633 634% binary predicate 635 636p: (INT, REAL) -> BOOLEAN; 637 638% Propositional "variables" 639 640P,Q; BOOLEAN; 641\endverbatim 642 643Like type declarations, 644such free symbol declarations have global scope and must be unique. 645In other words, it is not possible to globally declare a symbol more than once. 646This entails among other things that free symbols cannot be overloaded 647with different types. 648 649As with types, a new free symbol can be defined as the name of a term 650of the corresponding type. 651With constant symbols this is done with a declaration of the form \f$f:T = t;\f$ : 652 653\verbatim 654c: INT; 655 656i: INT = 5 + 3*c; 657 658j: REAL = 3/4; 659 660t: [REAL, INT] = (2/3, -4); 661 662r: [# key: INT, value: REAL #] = (# key := 4, value := (c + 1)/2 #); 663 664f: BOOLEAN = FORALL (x:INT): x <= 0 OR x > c ; 665\endverbatim 666 667A restriction on constants of type \f$\mathit{BOOLEAN}\f$ is that 668their value can only be a <em>closed</em> formula, 669that is, a formula with no free variables. 670 671A term and its name can be used interchangeably in later expressions. 672Named terms are often useful for shared subterms 673(terms used several times in different places) 674since their use can make the input exponentially more concise. 675Named terms are processed very efficiently by CVC3. 676It is much more efficient to associate a 677complex term with a name directly rather than 678to declare a constant and later assert that it is equal to the same term. 679This point will be explained in more detail later in 680section \ref user_doc_pres_lang_commands. 681 682 683More generally, 684in CVC3 one can associate a term to function symbols of any arity. 685For non-constant function symbols 686this is done with a declaration of the form 687\f[ 688f:(T_1, \ldots, T_n) \to T = \mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t\;; 689\f] 690where \f$t\f$ is any term of type \f$T\f$ 691with free variables in \f$\{x_1, \ldots, x_n\}\f$. 692The lambda binder has the usual semantics and conforms to the usual lexical scoping rules: 693within the term \f$t\f$ the declaration of the symbols \f$x_1, \ldots, x_n\f$ 694as local variables of respective type \f$T_1, \ldots, T_n\f$ hides 695any previous, global declaration of those symbols. 696 697As a general shorthand, 698when \f$k\f$ consecutive types \f$T_i, \ldots, T_{i+k-1}\f$ 699in the lambda expression \f$\mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t\f$ are identical, 700the syntax \f$\mathrm{LAMBDA}(x_1:T_1, \ldots, x_i,\ldots, x_{i+k-1}:T_i,\ldots, x:T_n): t\f$ 701is also allowed. 702 703 704\verbatim 705% Global declaration of x as a unary function symbol 706 707x: REAL -> REAL; 708 709 710% Local declarations of x as a constant symbol 711 712f: REAL -> REAL = LAMBDA (x: REAL): 2*x + 3; 713 714p: (INT, INT) -> BOOLEAN = LAMBDA (x,i: INT): i*x - 1 > 0; 715 716g: (REAL, INT) -> [REAL, INT] = LAMBDA (x: REAL, i:INT): (x + 1, i - 3); 717\endverbatim 718 719 720 721Constant and function symbols can also be declared <em>locally</em> anywhere within a term 722by means of a <em>let</em> binder. 723This is done with a declaration of the form 724\f[ 725\begin{array}{rl} 726\mathrm{LET} & f_1 = t_1, \\ 727 & \vdots \\ 728 & f_n = t_m \\ 729\mathrm{IN} & t ; 730\end{array} 731\f] 732for constant symbols, and of the form 733\f[ 734\begin{array}{rlcl} 735\mathrm{LET} 736 & f_1 & = &\mathrm{LAMBDA}(x^1_1:T^1_1, \ldots, x^{n_1}_1:T^{n_1}_1):\; t_1, 737 \\ 738 & & \vdots & 739 \\ 740 & f_m & = & \mathrm{LAMBDA}(x^1_m:T^1_m, \ldots, x^{n_m}_m:T^{n_m}_m):\; t_m 741 \\ 742 \mathrm{IN} & t ; 743\end{array} 744\f] 745for non-constant symbols. 746Let binders can be nested arbitrarily 747and follow the usual lexical scoping rules. 748 749\verbatim 750t: REAL = 751 LET g = LAMBDA(x:INT): x + 1, 752 x1 = 42, 753 x2 = 2*x1 + 7/2 754 IN 755 (LET x3 = g(x1) IN x3 + x2) / x1; 756\endverbatim 757 758Note that the same symbol <tt>=</tt> is used, unambiguously, 759in the syntax of global declarations, 760let declarations, 761and as a predicate symbol. 762 763In addition to user-defined symbols, 764CVC3 terms can use a number of predefined symbols: 765the logical symbols 766as well as <em>theory</em> symbols, 767function symbols belonging to one of the built-in theories. 768They are described next, with the theory symbols grouped by theory. 769 770 771\subsubsection user_doc_pres_lang_expr_logic Logical Symbols 772 773The logical symbols in CVC3's language include 774the equality and disequality predicate symbols, 775respectively written as <tt>=</tt> and <tt>/=</tt>, 776the multiarity disequality symbol <tt>DISTINCT</tt>, 777together with the logical constants <tt>TRUE</tt>, <tt>FALSE</tt>, 778the connectives <tt>NOT</tt>, <tt>AND</tt>, <tt>OR</tt>, 779<tt>XOR</tt>, <tt>=></tt>, <tt><=></tt>, 780and the first-order quantifiers <tt>EXISTS</tt> and <tt>FORALL</tt>, 781all with the standard many-sorted logic semantics. 782 783The binary connectives have infix syntax and type 784\f$(\mathrm{BOOLEAN},\mathrm{BOOLEAN}) \to \mathrm{BOOLEAN}\f$. 785The symbols <tt>=</tt> and <tt>/=</tt>, which are also infix, are instead polymorphic, 786having type \f$(T,T) \to \mathrm{BOOLEAN}\f$ 787for every predefined or user-defined value type \f$T\f$. 788They are interpreted respectively as the identity relation and its complement. 789 790The \f$\mathrm{DISTINCT}\f$ symbol is both overloaded and polymorphic. 791It has type \f$(T,...,T) \to \mathrm{BOOLEAN}\f$ 792for every tuple \f$(T,...,T)\f$ of length \f$n > 0\f$ 793where \f$T\f$ is a predefined or user-defined value type. 794For each \f$n > 0\f$, 795it is interpreteted as the relation that holds exactly 796for tuples of pairwise distinct elements. 797 798The syntax for quantifiers is similar to that of the lambda binder. 799 800Here is an example of a formula built just of these logical symbols and variables: 801 802\verbatim 803A, B: TYPE; 804 805quant: BOOLEAN = FORALL (x,y: A, i,j,k: B): i = j AND i /= k 806 => EXISTS (z: A): x /= z OR z /= y; 807\endverbatim 808 809 810Binding and scoping of quantified variables follows the same rules as 811in let expressions. 812In particular, a quantifier will shadow in its scope any constant and function symbols 813with the same name as one of the variables it quantifies: 814 815\verbatim 816A: TYPE; 817i,j: INT; 818 819% The first occurrence of i and of j in f are constant symbols, 820% the others are variables. 821 822f: BOOLEAN = i = j AND FORALL (i,j: A): i = j OR i /= j; 823\endverbatim 824 825Optionally, it is also possible to specify 826<em>instantiation patterns</em> for quantified variables. 827The general syntax for a quantified formula \f$\psi\f$ with patterns is 828 829\f[ 830 Q\:(x_1:T_1, \ldots, x_k:T_k):\; 831 p_1: \ldots\; p_n:\; 832 \varphi 833\f] 834 835where 836\f$n \geq 0\f$, 837\f$Q\f$ is either \f$\mathrm{FORALL}\f$ or \f$\mathrm{EXISTS}\f$, 838\f$\varphi\f$ is a term of type \f$\mathrm{BOOLEAN}\f$, 839and 840each of the \f$p_i\f$'s, 841a <em>pattern for the quantifier</em> \f$Q\:(x_1:T_1, \ldots, x_k:T_k)\f$, 842has the form 843\f[ 844 \mathrm{PATTERN}\; (t_1, \ldots, t_m) 845\f] 846where 847\f$m > 0\f$ 848and 849\f$t_1, \ldots, t_m\f$ are arbitrary binder-free terms (no lets, no quantifiers). 850Those terms can contain (free) variables, 851typically, but not exclusively, drawn from \f$x_1, \ldots, x_k\f$. 852(Additional variables can occur 853if \f$\psi\f$ occurs in a bigger formula binding those variables.) 854 855\verbatim 856A: TYPE; 857b, c: A; 858p, q: A -> BOOLEAN; 859r: (A, A) -> BOOLEAN; 860 861ASSERT FORALL (x0, x1, x2: A): 862 PATTERN (r(x0, x1), r(x1, x2)): 863 (r(x0, x1) AND r(x1, x2)) => r(x0, x2) ; 864 865ASSERT FORALL (x: A): 866 PATTERN (r(x, b)): 867 PATTERN (r(x, c)): 868 p(x) => q(x) ; 869 870ASSERT EXISTS (y: A): 871 FORALL (x: A): 872 PATTERN (r(x, y), p(y)): 873 r(x, y) => q(x) ; 874\endverbatim 875 876Patterns have no logical meaning: adding them to a formula does not change its semantics. 877Their purpose is purely operational, 878as explained in Section \ref user_doc_pres_lang_patterns. 879 880 881In addition to these constructs, 882CVC3 also has a general mixfix conditional operator of the form 883\f[ 884\mathrm{IF}\ b\ 885\mathrm{THEN}\ t\ 886\mathrm{ELSIF}\ b_1\ 887\mathrm{THEN}\ t_1\ 888\ldots\ 889\mathrm{ELSIF}\ b_n\ 890\mathrm{THEN}\ t_n\ 891\mathrm{ELSE}\ t_{n+1}\ 892\mathrm{ENDIF} 893\f] 894with \f$n \geq 0\f$ 895where \f$b, b_1, \ldots, b_n\f$ are terms of type \f$\mathrm{BOOLEAN}\f$ 896and 897\f$t, t_1, \ldots, t_n, t_{n+1}\f$ are terms of the same value type \f$T\f$: 898 899\verbatim 900% Conditional term 901x,y,z,w:REAL; 902t: REAL = 903 IF x > 0 THEN y 904 ELSIF x >= 1 THEN z 905 ELSIF x > 2 THEN w 906 ELSE 2/3 ENDIF; 907 908\endverbatim 909 910\subsubsection user_doc_pres_lang_expr_unint User-defined Functions and Types 911 912The theory of user-defined functions is in effect a family of theories 913of equality parametrized by the atomic types and the free symbols a user 914can define during a run of CVC3. 915<!-- 916[CB: I think this is confusing--this is true for all theories] 917For each run, the theory's types consist of all the user-defined types 918as well as all the predefined types from the other built-in theories. 919--> 920The theory's function symbols consist of all <em>and only</em> the user-defined free symbols. 921 922<!-- 923[CB: No longer true] 924Note that this theory is stronger than the theory of equality over 925the user-defined free symbols, because it also imposes cardinality constraints on 926all of its value types. 927Specifically, 928the \f$\mathrm{REAL}\f$ type and each user-defined atomic types are infinite; 929each bit vector type is finite; 930each array type is finite if both its index and element types are finite, and infinite otherwise; 931each inductive datatype (and similarly for tuple and record types) is finite or infinite 932depending on whether it defines a finite or an infinite term algebra. 933--> 934 935\subsubsection user_doc_pres_lang_expr_arith Arithmetic 936 937The real arithmetic theory has predefined symbols for the usual arithmetic 938constants and operators 939over the type \f$\mathrm{REAL}\f$, each with the expected type: 940all numerals <tt>0</tt>, <tt>1</tt>, ..., 941as well as <tt>-</tt> 942(both unary and binary), <tt>+</tt>, <tt>*</tt>, <tt>/</tt>, <tt><</tt>, 943<tt>></tt>, <tt><=</tt>, <tt>>=</tt>. 944Rational values can be expressed in fractional form: e.g., 1/2, 3/4, etc. 945 946The 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). 947 948 949\subsubsection user_doc_pres_lang_expr_bit Bit vectors 950 951The bit vector theory has a large number of predefined function symbols 952denoting various bit vector operators. 953We describe the operators and their semantics informally below, 954often omitting a specification of their type, which should be easy to infer. 955 956The operators' names are overloaded in the obvious way. 957For instance, the same name is used for each \f$m,n > 0\f$ 958for the operator that takes a bit vector of size \f$m\f$ and one of size \f$n\f$ and 959returns their concatenation. 960 961For each size \f$n\f$, 962there are \f$2^n\f$ elements in the type \f$\mathrm{BITVECTOR}(n)\f$. These 963elements can be named using constant symbols 964or <em>bit vector constants</em>. Each element in the domain is named by two 965different constant symbols: once in binary and once in hexadecimal format. 966Binary constant symbols start with the characters <tt>0bin</tt> 967and continue with the representation of the vector in the usual binary format 968(as an \f$n\f$-string over the characters 0,1). 969Hexadecimal constant symbols start with the characters <tt>0hex</tt> 970and continue with the representation of the vector in usual hexadecimal format 971(as an \f$n\f$-string over the characters 0,...,9,a,...,f). 972 973\verbatim 974Binary constant Corresponding hexadecimal constant 975----------------------------------------------------------- 9760bin0000111101010000 0hex0f50 977\endverbatim 978 979In the binary representation, 980the rightmost bit is the least significant bit (LSB) of the vector and 981the leftmost bit is the most significant bit (MSB). 982The index of the LSB in the bit vector is 0 and 983the index of the MSB is n-1 for an n-bit constant. 984This convention extends to all bit vector expressions in the natural way. 985 986Bit vector operators are categorized into 987word-level, bitwise, arithmetic, and comparison operators. 988 989\verbatim 990WORD-LEVEL OPERATORS: 991 992Description Symbol Example 993==================================================================== 994Concatenation _ @ _ 0bin01@0bin0 (= 0bin010) 995Extraction _ [i:j] 0bin0011[3:1] (= 0bin001) 996Left shift _ << k 0bin0011 << 3 (= 0bin0011000) 997Right shift _ >> k 0bin1000 >> 3 (= 0bin0001) 998Sign extension SX(_,k) SX(0bin100, 5) (= 0bin11100) 999Zero extension BVZEROEXTEND(_,k) BVZEROEXTEND(0bin1,3) (= 0bin0001) 1000Repeat BVREPEAT(_,k) BVREPEAT(0bin10,3) (= 0bin101010) 1001Rotate left BVROTL(_,k) BVROTL(0bin101,1) (= 0bin011) 1002Rotate right BVROTR(_,k) BVROTR(0bin101,1) (= 0bin110) 1003\endverbatim 1004 1005 1006For each \f$m,n > 0\f$ there is 1007- 1008one infix concatenation operator, 1009taking an \f$m\f$-bit vector \f$v_1\f$ and an \f$n\f$-bit vector \f$v_2\f$ and 1010returning the \f$(m+n)\f$-bit concatenation of \f$v_1\f$ and \f$v_2\f$; 1011- 1012one postfix extraction operator \f$[i:j]\f$ for each \f$i, j\f$ with \f$n > i >= j >= 0\f$, 1013taking an \f$n\f$-bit vector \f$v\f$ and 1014returning the \f$(i-j+1)\f$-bit subvector of \f$v\f$ at positions \f$i\f$ 1015through \f$j\f$ (inclusive); 1016- 1017one postfix left shift operator \f$<< k\f$ for each \f$k >= 0\f$, 1018taking an \f$n\f$-bit vector \f$v\f$ and 1019returning the \f$(n+k)\f$-bit concatenation of \f$v\f$ with the \f$k\f$-bit zero vector; 1020- 1021one postfix right shift operator \f$>> k\f$ for each \f$k >= 0\f$, 1022taking an \f$n\f$-bit vector \f$v\f$ and 1023returning the \f$n\f$-bit concatenation of the \f$k\f$-bit zero bit vector with \f$v[n-1:k]\f$; 1024- 1025one mixfix sign extension operator \f$\mathrm{SX}(\_, k)\f$ for each \f$k >= n\f$, 1026taking an \f$n\f$-bit vector \f$v\f$ and 1027returning the \f$k\f$-bit concatenation of \f$k-n\f$ copies of the MSB of \f$v\f$ 1028and \f$v\f$. 1029- 1030one mixfix zero extension operator \f$\mathrm{BVZEROEXTEND}(\_, k)\f$ for each \f$k >= 1\f$, 1031taking an \f$n\f$-bit vector \f$v\f$ and 1032returning the \f$n+k\f$-bit concatenation of \f$k\f$ zeroes and \f$v\f$. 1033- 1034one mixfix repeat operator \f$\mathrm{BVREPEAT}(\_, k)\f$ for each \f$k >= 1\f$, 1035taking an \f$n\f$-bit vector \f$v\f$ and 1036returning the \f$n*k\f$-bit concatenation of \f$k\f$ copies of \f$v\f$. 1037- 1038one mixfix rotate left operator \f$\mathrm{BVROTL}(\_, k)\f$ for each \f$k >= 0\f$, 1039taking an \f$n\f$-bit vector \f$v\f$ and 1040returning the \f$(n)\f$-bit vector obtained by rotating the bits of \f$v\f$ 1041left \f$k\f$ times, where a single rotation means removing the MSB and 1042concatenating it as the new LSB. 1043- 1044one mixfix rotate right operator \f$\mathrm{BVROTR}(\_, k)\f$ for each \f$k >= 0\f$, 1045taking an \f$n\f$-bit vector \f$v\f$ and 1046returning the \f$(n)\f$-bit vector obtained by rotating the bits of \f$v\f$ 1047right \f$k\f$ times, where a single rotation means removing the LSB and 1048concatenating it as the new MSB. 1049 1050\verbatim 1051BITWISE OPERATORS: 1052 1053Description Symbol 1054============================== 1055Bitwise AND _ & _ 1056Bitwise OR _ | _ 1057Bitwise NOT ~ _ 1058Bitwise XOR BVXOR(_,_) 1059Bitwise NAND BVNAND(_,_) 1060Bitwise NOR BVNOR(_,_) 1061Bitwise XNOR BVXNOR(_,_) 1062Bitwise Compare BVCOMP(_,_) 1063\endverbatim 1064 1065For each \f$n > 0\f$ there are operators with the names and syntax above, 1066performing the usual bitwise Boolean operations on \f$n\f$-bit arguments. All 1067produce \f$n\f$-bit results except for \f$\mathrm{BVCOMP}\f$ which always 1068produces a 1-bit result: \f$\mathrm{0bin1}\f$ if its two arguments are equal 1069and \f$\mathrm{0bin0}\f$ otherwise. 1070 1071\verbatim 1072ARITHMETIC OPERATORS: 1073 1074Description Symbol 1075======================================== 1076Bit vector addition BVPLUS(k,_,_,...) 1077Bit vector multiplication BVMULT(k,_,_) 1078Bit vector negation BVUMINUS(_) 1079Bit vector subtraction BVSUB(k,_,_) 1080Bit vector left shift BVSHL(_,_) 1081Bit vector arith shift right BVASHR(_,_) 1082Bit vector logic shift right BVLSHR(_,_) 1083Bit vector unsigned divide BVUDIV(_,_) 1084Bit vector signed divide BVSDIV(_,_) 1085Bit vector unsigned remainder BVUREM(_,_) 1086Bit vector signed remainder BVSREM(_,_) 1087Bit vector signed modulus BVSMOD(_,_) 1088\endverbatim 1089 1090 1091For each \f$n > 0\f$ and \f$k > 0\f$ there is 1092- 1093one addition operator \f$\mathrm{BVPLUS}(k,\_, \_, \ldots)\f$, 1094taking two or more bit vectors of arbitrary size, and returning the \f$(k)\f$ 1095least significant bits of their sum. 1096- 1097one multiplication operator \f$\mathrm{BVMULT}(k,\_, \_)\f$, 1098taking two bit vectors \f$v_1\f$ and \f$v_2\f$, and 1099returning the \f$k\f$ least significant bits of their product. 1100- 1101one prefix negation operator \f$\mathrm{BVUMINUS}(\_)\f$, 1102taking an \f$n\f$-bit vector \f$v\f$ and 1103returning the \f$n\f$-bit vector \f$\mathrm{BVPLUS}(n,\verb|~|v,\mathrm{0bin1})\f$. 1104- 1105one subtraction operator \f$\mathrm{BVSUB}(k,\_, \_)\f$, 1106taking two bit vectors \f$v_1\f$ and \f$v_2\f$, and 1107returning the \f$k\f$-bit vector 1108\f$\mathrm{BVPLUS}(k,v_1,\mathrm{BVUMINUS}(v'))\f$ where \f$v'\f$ is \f$v_2\f$ 1109if the size of \f$v_2\f$ is greater than or equal to \f$k\f$, and \f$v_2\f$ 1110extended to size \f$k\f$ by concatenating zeroes in the most significant bits otherwise. 1111- 1112one left shift operator \f$\mathrm{BVSHL}(\_, \_)\f$, 1113taking two \f$n\f$-bit vectors \f$v_1\f$ and \f$v_2\f$, and 1114returning the \f$n\f$-bit vector obtained by creating a vector of zeroes whose 1115length is the value of \f$v_2\f$, concatenating this vector onto the least 1116significant bits of \f$v_1\f$, and then taking the least significant \f$n\f$ 1117bits of the result. 1118- 1119one arithmetic shift right operator \f$\mathrm{BVASHR}(\_, \_)\f$, 1120taking two \f$n\f$-bit vectors \f$v_1\f$ and \f$v_2\f$, and 1121returning the \f$n\f$-bit vector obtained by creating a vector whose 1122length is the value of \f$v_2\f$ and each of whose bits has the same value as 1123the MSB of \f$v_1\f$, concatenating this vector onto the most 1124significant bits of \f$v_1\f$, and then taking the most significant \f$n\f$ 1125bits of the result. 1126- 1127one logical shift right operator \f$\mathrm{BVLSHR}(\_, \_)\f$, 1128taking two \f$n\f$-bit vectors \f$v_1\f$ and \f$v_2\f$, and 1129returning the \f$n\f$-bit vector obtained by creating a vector of zeroes whose 1130length is the value of \f$v_2\f$, concatenating this vector onto the most 1131significant bits of \f$v_1\f$, and then taking the most significant \f$n\f$ 1132bits of the result. 1133- 1134one unsigned integer division operator \f$\mathrm{BVUDIV}(\_, \_)\f$, 1135taking two \f$n\f$-bit vectors \f$v_1\f$ and \f$v_2\f$, and 1136returning the \f$n\f$-bit vector that is the largest integer value that can be 1137multiplied by the integer value of \f$v_2\f$ to obtain an integer less than or 1138equal to the integer value of \f$v_1\f$. 1139- 1140one signed integer division operator \f$\mathrm{BVSDIV}(\_, \_)\f$. 1141- 1142one unsigned integer remainder operator \f$\mathrm{BVUREM}(\_, \_)\f$. 1143- 1144one signed integer remainder operator \f$\mathrm{BVSREM}(\_, \_)\f$ (sign 1145follows dividend). 1146- 1147one signed integer modulus operator \f$\mathrm{BVSMOD}(\_, \_)\f$ (sign follows 1148divisor). 1149 1150For precise definitions of the last four operators, we refer the reader to the 1151equivalent operators defined in the SMT-LIB QF_BV logic (\ref user_doc_smtlib_lang). 1152 1153CVC3 does not have dedicated operators for multiplexers. 1154However, specific multiplexers can be easily defined with the aid of conditional terms. 1155 1156\verbatim 1157% Example of 2-to-1 multiplexer 1158 1159mp: (BITVECTOR(1), BITVECTOR(1), BITVECTOR(1)) -> BITVECTOR(1) = 1160 LAMBDA (s,x,y : BITVECTOR(1)): IF s = 0bin0 THEN x ELSE y ENDIF; 1161\endverbatim 1162 1163 1164In addition to equality and disequality, CVC3 provides the following comparison operators. 1165 1166\verbatim 1167COMPARISON OPERATORS: 1168 1169Description Symbol 1170=================================== 1171Less than BVLT(_,_) 1172Less than or equal to BVLE(_,_) 1173Greater than BVGT(_,_) 1174Greater than equal to BVGE(_,_) 1175Signed less than BVSLT(_,_) 1176Signed less than or equal to BVSLE(_,_) 1177Signed greater than BVSGT(_,_) 1178Signed greater than equal to BVSGE(_,_) 1179\endverbatim 1180 1181For each \f$m, n > 0\f$ there is 1182- 1183one prefix "less than" operator \f$\mathrm{BVLT}(\_, \_)\f$, 1184taking an \f$m\f$-bit vector \f$v_1\f$ and an \f$n\f$-bit vector \f$v_2\f$, and 1185having the value \f$\mathrm{TRUE}\f$ iff the zero-extension of \f$v_1\f$ to \f$k\f$ 1186bits is less than the zero-extension of \f$v_2\f$ to \f$k\f$ bits, where 1187\f$k\f$ is the maximum of \f$m\f$ and \f$n\f$. 1188- 1189one prefix "less than or equal to" operator \f$\mathrm{BVLE}(\_, \_)\f$, 1190taking an \f$m\f$-bit vector \f$v_1\f$ and an \f$n\f$-bit vector \f$v_2\f$, and 1191having the value \f$\mathrm{TRUE}\f$ iff the zero-extension of \f$v_1\f$ to \f$k\f$ 1192bits is less than or equal to the zero-extension of \f$v_2\f$ to \f$k\f$ bits, where 1193\f$k\f$ is the maximum of \f$m\f$ and \f$n\f$. 1194- 1195one prefix "greater than" operator \f$\mathrm{BVGT}(\_, \_)\f$, 1196taking an \f$m\f$-bit vector \f$v_1\f$ and an \f$n\f$-bit vector \f$v_2\f$, and 1197having the same value as \f$\mathrm{BVLT}(v_2, v_1)\f$. 1198- 1199one prefix "greater than or equal to" operator \f$\mathrm{BVGE}(\_, \_)\f$, 1200taking an \f$m\f$-bit vector \f$v_1\f$ and an \f$n\f$-bit vector \f$v_2\f$, and 1201having the same value as \f$\mathrm{BVLE}(v_2, v_1)\f$. 1202 1203The signed operators are similar except that the values being compared are 1204considered to be signed bit vector representations (in 2's complement) of integers. 1205 1206Following are some example CVC3 input formulas involving bit vector expressions 1207 1208Example 1 illustrates the use of arithmetic, word-level and bitwise NOT operations: 1209 1210\verbatim 1211x : BITVECTOR(5); 1212y : BITVECTOR(4); 1213yy : BITVECTOR(3); 1214 1215QUERY 1216 BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ; 1217\endverbatim 1218 1219Example 2 illustrates the use of arithmetic, word-level and multiplexer terms: 1220 1221\verbatim 1222bv : BITVECTOR(10); 1223a : BOOLEAN; 1224 1225QUERY 1226 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] 1227 AND 1228 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ; 1229\endverbatim 1230 1231Example 3 illustrates the use of bitwise operations: 1232 1233\verbatim 1234x, y, z, t, q : BITVECTOR(1024); 1235 1236ASSERT x = ~x; 1237ASSERT x&y&t&z&q = x; 1238ASSERT x|y = t; 1239ASSERT BVXOR(x,~x) = t; 1240QUERY FALSE; 1241\endverbatim 1242 1243Example 4 illustrates the use of predicates and all the arithmetic operations: 1244 1245\verbatim 1246x, y : BITVECTOR(4); 1247 1248ASSERT x = 0hex5; 1249ASSERT y = 0bin0101; 1250 1251QUERY 1252 BVMULT(8,x,y)=BVMULT(8,y,x) 1253 AND 1254 NOT(BVLT(x,y)) 1255 AND 1256 BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x))) 1257 AND 1258 x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1)) ; 1259\endverbatim 1260 1261Example 5 illustrates the use of shift functions 1262 1263\verbatim 1264x, y : BITVECTOR(8); 1265z, t : BITVECTOR(12); 1266 1267ASSERT x = 0hexff; 1268ASSERT z = 0hexff0; 1269QUERY z = x << 4; 1270QUERY (z >> 4)[7:0] = x; 1271\endverbatim 1272 1273 1274\subsubsection user_doc_pres_lang_expr_arr Arrays 1275 1276The theory of arrays is a parametric theory of (total) unary functions. 1277It comes equipped with polymorphic selection and update operators, 1278respectively 1279<center> 1280\f$\_[\_]\f$ and \f$\_\ \mathrm{WITH}\ [\_]\ := \_\f$ 1281</center> 1282with the usual semantics. 1283For each <em>index</em> type \f$T_1\f$ and <em>element</em> type \f$T_2\f$, 1284the first operator maps an array from \f$T_1\f$ to \f$T_2\f$ 1285and an index into it (i.e., a value of type \f$T_1\f$) 1286to the element of type \f$T_2\f$ "stored" into the array at that index. 1287The second maps an array \f$a\f$ from \f$T_1\f$ to \f$T_2\f$, 1288an index \f$i\f$, 1289and a \f$T_2\f$-element \f$e\f$ to the array 1290that stores \f$e\f$ at index \f$i\f$ and is otherwise identical to \f$a\f$. 1291 1292Since arrays are just maps, equality between them is <em>extensional</em>: 1293for two arrays of the same type to be different 1294they have to store differ elements in at least one place. 1295 1296Sequential updates can be chained with the syntax 1297\f$\_\ \mathrm{WITH}\ [\_]\ := \_, \ldots, [\_]\ := \_\f$. 1298 1299\verbatim 1300A: TYPE = ARRAY INT OF REAL; 1301a: A; 1302i: INT = 4; 1303 1304% selection: 1305 1306 1307elem: REAL = a[i]; 1308 1309% update 1310 1311a1: A = a WITH [10] := 1/2; 1312 1313% sequential update 1314% (syntactic sugar for (a WITH [10] := 2/3) WITH [42] := 3/2) 1315 1316a2: A = a WITH [10] := 2/3, [42] := 3/2; 1317\endverbatim 1318 1319<!-- 1320We decided not to mention array initialization. 1321This will remain for now an undocumented feature of the theory. 1322--> 1323 1324 1325\subsubsection user_doc_pres_lang_expr_dat Datatypes 1326 1327The theory of datatypes is in fact a <em>family</em> of theories 1328parametrized by a datatype declaration specifying 1329constructors and selectors for a particular datatype. 1330 1331No built-in operators other than equality and disequality are provided for this family 1332in the presentation language. 1333Each datatype declaration, however, generates constructor, selector and tester operators 1334as described in Section \ref user_doc_pres_lang_data_types. 1335 1336 1337\subsubsection user_doc_pres_lang_expr_rec_tup Tuples and Records 1338 1339Although they are currently implemented separately in CVC3, 1340semantically both records and tuples can be seen as special instances of datatypes. 1341In fact, a record of type \f$[\# l_0:T_0, \ldots, l_n:T_n \#]\f$ 1342could be equivalently modeled as, say, the datatype 1343\f[ 1344\begin{array}{l} 1345\mathrm{DATATYPE} \\ 1346\ \ \mathrm{Record} = \mathit{rec}(l_0:T_0, \ldots, l_n:T_n) \\ 1347\mathrm{END}; 1348\end{array} 1349\f] 1350 1351Tuples could be seen in turn as special cases of records 1352where the field names are the numbers from 0 to the length of the tuple minus 1. 1353Currently, however, 1354tuples and records have their own syntax for constructor and selector operators. 1355 1356Records of type \f$[\# l_0:T_0, \ldots, l_n:T_n \#]\f$ have the associated 1357built-in constructor 1358\f$(\#\ l_0 := \_, \ldots, l_n := \_\ \#)\f$ whose arguments 1359must be terms of type \f$T_0, \ldots, T_n\f$, respectively. 1360 1361Tuples of type \f$[\ T_0, \ldots, T_n\ ]\f$ have the associated 1362built-in constructor 1363\f$(\ \_, \ldots, \_\ )\f$ whose arguments 1364must be terms of type \f$T_0, \ldots, T_n\f$, respectively. 1365 1366The selector operators on records and tuples follows a dot notation syntax. 1367 1368\verbatim 1369% Record construction and field selection 1370 1371Item: TYPE = [# key: INT, weight: REAL #]; 1372 1373x: Item = (# key := 23, weight := 43/10 #); 1374k: INT = x.key; 1375v: REAL = x.weight; 1376 1377% Tuple construction and projection 1378 1379y: [REAL,INT,REAL] = ( 4/5, 9, 11/9 ); 1380first_elem: REAL = y.0; 1381third_elem: REAL = y.2; 1382\endverbatim 1383 1384Differently from datatypes, 1385records and tuples are also provided with built-in update operators 1386similar in syntax and semantics to the update operator for arrays. 1387More precisely, 1388for each record type \f$[\#\ l_0:T_0, \ldots, l_n:T_n\ \#]\f$ 1389and each \f$i=0, \ldots, n\f$, 1390CVC3 provides the operator 1391\f[ 1392 \_\ \mathrm{WITH}\ .l_i\ := \_ 1393\f] 1394The operator maps a record \f$r\f$ of that type 1395and a value \f$v\f$ of type \f$T_i\f$ to the record 1396that stores \f$v\f$ in field \f$l_i\f$ and is otherwise identical to \f$r\f$. 1397Analogously, 1398for each tuple type \f$[T_0, \ldots, T_n]\f$ 1399and each \f$i=0, \ldots, n\f$, 1400CVC3 provides the operator 1401\f[ 1402 \_\ \mathrm{WITH}\ .i\ := \_ 1403\f] 1404 1405\verbatim 1406% Record updates 1407 1408Item: TYPE = [# key: INT, weight: REAL #]; 1409 1410x: Item = (# key := 23, weight := 43/10 #); 1411 1412x1: Item = x WITH .weight := 48; 1413 1414% Tuple updates 1415 1416Tup: TYPE = [REAL,INT,REAL]; 1417y: Tup = ( 4/5, 9, 11/9 ); 1418y1: Tup = y WITH .1 := 3; 1419\endverbatim 1420 1421Updates to a nested component can be combined in a single WITH operator: 1422 1423\verbatim 1424Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #]; 1425State: TYPE = [# pc: INT, cache: Cache #]; 1426 1427s0: State; 1428s1: State = s0 WITH .cache[10].data := 2/3; 1429 1430\endverbatim 1431 1432Note that, differently from updates on arrays, 1433tuple and record updates are just additional syntactic sugar. 1434For instance, 1435the record <tt>x1</tt> and tuple <tt>y1</tt> defined above could 1436have been equivalently defined as follows: 1437 1438\verbatim 1439% Record updates 1440 1441Item: TYPE = [# key: INT, weight: REAL #]; 1442 1443x: Item = (# key := 23, weight := 43/10 #); 1444 1445x1: Item = (# key := x.key, weight := 48 #); 1446 1447% Tuple updates 1448 1449Tup: TYPE = [REAL,INT,REAL]; 1450y: Tup = ( 4/5, 9, 11/9 ); 1451y1: Tup = ( y.0, 3, y.1 ); 1452\endverbatim 1453 1454 1455 1456 1457 1458 1459\subsection user_doc_pres_lang_commands Commands 1460 1461In addition to declarations of types and constants, the CVC3 input 1462language contains the following commands: 1463 1464- <tt>ASSERT</tt> \f$F\f$ -- Add the formula \f$F\f$ to the current logical context \f$\Gamma\f$. 1465- <tt>QUERY</tt> \f$F\f$ -- Check if the formula \f$F\f$ is valid in the current 1466 logical context: \f$\Gamma\models_T F\f$. 1467- <tt>CHECKSAT</tt> \f$F\f$ -- Check if the formula is satisfiable in the current 1468 logical context: \f$\Gamma\cup\{F\} \not\models_T \mathit{false}\f$. 1469- <tt>WHERE</tt> -- Print all the assumptions in the current logical context \f$\Gamma\f$. 1470- <tt>COUNTEREXAMPLE</tt> -- After an invalid QUERY or satisfiable CHECKSAT, 1471 print the context that is a witness for invalidity/satisfiability. 1472- <tt>COUNTERMODEL</tt> -- After an invalid QUERY or satisfiable CHECKSAT, 1473 print a model that makes the formula invalid/satisfiable. The model is in 1474 terms of concrete values for each free symbol. 1475- <tt>CONTINUE</tt> -- Search for a counter-example different from the current 1476 one (after an invalid QUERY or satisfiable CHECKSAT). 1477- <tt>RESTART</tt> \f$F\f$ -- Restart an invalid QUERY or satisfiable CHECKSAT 1478 with the additional assumption \f$F\f$. 1479 1480- <tt>PUSH</tt> -- Save (checkpoint) the current state of the system. 1481- <tt>POP</tt> -- Restore the system to the state it was in right before the 1482 last call to <tt>PUSH</tt> 1483- <tt>POPTO</tt> \f$n\f$-- Restore the system to the state it was in right 1484 before the most recent call to <tt>PUSH</tt> made from stack level \f$n\f$. 1485 Note that the current stack level is printed as part of the output of the <tt>WHERE</tt> command. 1486 1487- <tt>TRANSFORM</tt> \f$F\f$ -- Simplify \f$F\f$ and print the result. 1488- <tt>PRINT</tt> \f$F\f$ -- Parse and print back the expression \f$F\f$. 1489- <tt>OPTION</tt> <I>option</I> <I>value</I> -- Set the command-line option 1490 flag <I>option</I> to <I>value</I>. Note that <I>option</I> is given as a 1491 string enclosed in double-quotes and <I>value</I> as an integer. 1492 1493<!-- 1494[CB: Don't advertise these for now--the functionality needs to be reviewed] 1495 1496- <tt>DUMP_PROOF</tt> -- dump the proof of the last (successful) QUERY 1497- <tt>DUMP_ASSUMPTIONS</tt> -- dump the assumptions used in the proof 1498 of the last (successful) QUERY 1499- <tt>DUMP_TCC</tt> -- dump the TCC for the last formula in ASSERT or QUERY 1500- <tt>DUMP_TCC_ASSUMPTIONS</tt> -- dump assumptions used in the proofs of the 1501 TCC for the last ASSERT or QUERY 1502- <tt>DUMP_TCC_PROOF</tt> -- dump the proof of the TCC for the last ASSERT 1503 or QUERY 1504- <tt>DUMP_CLOSURE</tt> -- convert the last (successful) QUERY into an 1505 implication (assumptions => query) and print this formula 1506- <tt>DUMP_CLOSURE_PROOF</tt> -- dump the proof of the closure of the last 1507 (successful) QUERY 1508--> 1509 1510The remaining commands take a single argument, given as a string enclosed in 1511double-quotes. 1512 1513- <tt>TRACE</tt> <I>flag</I> -- Turn on tracing for the debug flag <I>flag</I>. 1514- <tt>UNTRACE</tt> <I>flag</I> -- Turn off tracing for the debug flag <I>flag</I>. 1515 1516- <tt>ECHO</tt> <I>string</I> -- Print <I>string</I> 1517- <tt>INCLUDE</tt> <I>filename</I> -- Read commands from the file <I>filename</I>. 1518 1519Here, we explain some of the above commands in more detail. 1520 1521\subsubsection user_doc_pres_lang_commands_query QUERY 1522 1523The command <tt>QUERY</tt> \f$F\f$ invokes the core 1524functionality of CVC3 to check the validity of the formula \f$F\f$ with respect 1525to the assertions made thus far (\f$\Gamma\f$). \f$F\f$ should be a formula as 1526described in \ref user_doc_pres_lang_expr. 1527 1528There are three possible answers. 1529- When the answer is "Valid", this means that \f$\Gamma \models_T F\f$. After 1530a valid query, the logical context \f$\Gamma\f$ is exactly as it was before the query. 1531- When the answer is "Invalid", this means that \f$\Gamma \not\models_T F\f$. 1532In other words, there is a model of \f$T\f$ satisfying \f$\Gamma \cup \{\neg F\}\f$. After an 1533invalid query, the logical context \f$\Gamma\f$ is augmented with new literals 1534\f$\Delta\f$ such that \f$\Gamma\cup\Delta\f$ is consistent in the theory \f$T\f$, but 1535\f$\Gamma\cup\Delta\models_T \neg F\f$. In fact, in this case \f$\Gamma\cup\Delta\f$ 1536<em>propositionally</em> satisfies \f$\neg f\f$. We call the new context 1537\f$\Gamma\cup\Delta\f$ a <em>counterexample</em> for \f$F\f$. 1538- An answer of "Unknown" is very similar to an answer of "Invalid" in that 1539additional literals are added to the context which propositionally falsify the 1540query formula \f$F\f$. The difference is that because CVC3 is incomplete for 1541some theories, it cannot guarantee in this case that \f$\Gamma\cup\Delta\f$ is 1542actually consistent in \f$T\f$. The only sources of incompleteness in CVC3 are 1543non-linear arithmetic and quantifiers. 1544 1545Counterexamples can be printed out using <tt>WHERE</tt> or 1546<tt>COUNTEREXAMPLE</tt> commands. <tt>WHERE</tt> always prints out all of 1547\f$\Gamma\cup C\f$. <tt>COUNTEREXAMPLE</tt> may sometimes be more 1548selective, printing a subset of those formulas from the context which 1549are sufficient for a counterexample. 1550 1551Since the QUERY command may modify the current context, if you need to check 1552several formulas in a row in the same context, it is a good idea to 1553surround every QUERY command by PUSH and POP in order to preserve the 1554context: 1555 1556\verbatim 1557PUSH; 1558QUERY <formula>; 1559POP; 1560\endverbatim 1561 1562\subsubsection user_doc_pres_lang_commands_checksat CHECKSAT 1563 1564The command <tt>CHECKSAT</tt> \f$F\f$ behaves identically to <tt>QUERY</tt> 1565\f$\neg F\f$. 1566 1567\subsubsection user_doc_pres_lang_commands_restart RESTART 1568 1569The command <tt>RESTART</tt> \f$F\f$ can only be invoked after an invalid 1570query. For example: 1571 1572\verbatim 1573QUERY <formula>; 1574Invalid. 1575RESTART <formula2>; 1576\endverbatim 1577 1578The behavior of the above command will be identical to the following: 1579 1580\verbatim 1581PUSH; 1582QUERY <formula>; 1583POP; 1584ASSERT <formula2>; 1585QUERY <formula>; 1586\endverbatim 1587 1588The advantage of using the <tt>RESTART</tt> command is that it may be much more 1589efficient than the above command sequence. This is because when the 1590<tt>RESTART</tt> command is used, CVC3 will re-use what it has learned rather 1591than starting over from scratch. 1592 1593<!-- 1594[CB: Remove for now] 1595\verbatim 1596DUMP_PROOF 1597DUMP_ASSUMPTIONS 1598\endverbatim 1599 1600Print out a proof of the latest QUERY (if it was successfully proven), 1601and the assumptions (formulas) from the current logical context used 1602in the proof. 1603 1604Note, that <tt>DUMP_PROOF</tt> uses free proof variables for the 1605proofs of assumptions without defining them, and therefore, is not 1606necessarily the best way to check the proofs. See DUMP_CLOSURE_PROOF. 1607 1608\verbatim 1609DUMP_CLOSURE 1610DUMP_CLOSURE_PROOF 1611\endverbatim 1612 1613If the last QUERY successfully proved a formula \f$\phi\f$ using only 1614a subset \f$\Gamma'\subseteq\Gamma\f$ of the current logical context, 1615then <tt>DUMP_CLOSURE</tt> prints a formula 1616\f[\bigwedge\Gamma'\Rightarrow\phi,\f] which is now valid by itself, 1617independent of the logical context, and <tt>DUMP_CLOSURE_PROOF</tt> 1618prints out a proof of that formula. 1619 1620This eliminates the problem of undefined proof variables from 1621<tt>DUMP_PROOF</tt>. In addition, the proofs of all the relevant TCCs 1622are incorporated into the proof of the closure using a 3-valued 1623implication introduction rule. See the next section on 1624\ref user_doc_pres_lang_tccs for details. 1625--> 1626 1627\subsection user_doc_pres_lang_patterns Instantiation Patterns 1628 1629CVC3 processes each universally quantified formula in the current context 1630by generating <em>instances</em> of 1631the formula obtained by replacing its universal variables with ground terms. 1632Patterns restrict the choice of ground terms for the quantified variables, 1633with the goal of controlling the potential explosion of ground instances. 1634In essence, adding patterns to a formula is a way for the user to tell CVC3 1635to focus only on certain instances which, in the user's opinion, will be most 1636helpful during a proof. 1637 1638In more detail, 1639patterns have the following effect on formulas that are found in the logical context 1640or get later added to it 1641while CVC3 is trying to prove the validity of some formula \f$\varphi\f$. 1642 1643If a formula in the current context starts with an existential quantifier, 1644CVC3 Skolemizes it, that is, replaces it in the context 1645by the formula obtained by substituting the existentially quantified variables 1646by fresh constants and dropping the quantifier. 1647Any patterns for the existential quantifier are simply ignored. 1648 1649If a formula starts with a universal quantifier \f$\mathrm{FORALL}\; (x_1:T_1, \ldots, x_n:T_n)\f$, 1650CVC3 adds to the context a number of instances 1651of the formula---with the goal of using them to prove the query \f$\varphi\f$ valid. 1652An instance is obtained by replacing each \f$x_i\f$ with 1653a ground term of the same type occurring in one of the formulas in the context, 1654and dropping the universal quantifier. 1655If \f$x_i\f$ occurs in a pattern \f$\mathrm{PATTERN}\; (t_1, \ldots, t_m)\f$ 1656for the quantifier, 1657it will be instantiated only with terms obtained by simultaneously matching 1658all the terms in the pattern against ground terms in the current context \f$\Gamma\f$. 1659 1660Specifically, the matching process produces one or more substitutions \f$\sigma\f$ 1661for the variables in \f$(t_1, \ldots, t_m)\f$ 1662which satisfy the following invariant: 1663for each \f$i = 1, \ldots, m\f$, 1664\f$\sigma(t_i)\f$ is a ground term 1665and 1666there is a ground term \f$s_i\f$ in \f$\Gamma\f$ such that 1667\f$\Gamma \models_T \sigma(t_i) = s_i\f$. 1668The variables of \f$(x_1:T_1, \ldots, x_n:T_n)\f$ that occur in the pattern 1669are instantiated only with those substitutions (while any remaining variables are instantiated arbitrarily). 1670 1671The Skolemized version or the added instances of a context formula may 1672themselves start with a quantifier. 1673The same instantiation process is applied to them too, recursively. 1674 1675Note that the matching mechanism is not limited to syntactic matching but is modulo 1676the equations asserted in the context. 1677Because of decidability and/or efficiency limitations, 1678the matching process is not exhaustive. 1679CVC3 will typically miss some substitutions that satisfy the invariant above. 1680As a consequence, it might fail to prove the validity of the query formula \f$\varphi\f$, which makes CVC3 incomplete for contexts containing quantified formulas. 1681It 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). 1682 1683 1684 1685\subsection user_doc_pres_lang_subtypes Subtypes 1686 1687CVC3's language includes the definition of <em>subtypes</em> of 1688value types by means of predicate subtyping. 1689 1690A subtype \f$T_p\f$ of a (sub)type \f$T\f$ is defined as 1691a subset of \f$T\f$ that satisfies an associated predicate \f$p\f$. 1692More precisely, 1693if \f$p\f$ is a term of type \f$T \to \mathrm{BOOLEAN}\f$, 1694then for every model of \f$p\f$ (among the models of CVC3's built-in theories), 1695\f$T_P\f$ is the <em>extension</em> of \f$p\f$, 1696that is, 1697the set of all and only the elements of \f$T\f$ that 1698satisfy the predicate \f$p\f$. 1699 1700 1701Subtypes like \f$T_p\f$ above can be defined by the user with a declaration of the form: 1702 1703\f[ 1704\mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p) 1705\f] 1706 1707where \f$p\f$ is 1708either just a (previously declared) predicate symbol of type \f$T \to \mathrm{BOOLEAN}\f$ 1709or a lambda abstraction of the form \f$\lambda x:T.\; \varphi\f$ 1710where \f$\varphi\f$ is any CVC3 formula 1711whose set of free variables contains at most \f$x\f$. 1712 1713Here are some examples of subtype declarations: 1714 1715\verbatim 1716Animal: TYPE; 1717 1718fish : Animal; 1719 1720is_fish: Animal -> BOOLEAN; 1721 1722ASSERT is_fish(fish); 1723 1724% Fish is a subtype of Animal: 1725 1726Fish: TYPE = SUBTYPE(is_fish); 1727 1728shark : Fish; 1729 1730is_shark: Fish -> BOOLEAN; 1731 1732ASSERT is_shark(shark); 1733 1734% Shark is a subtype of Fish: 1735 1736Shark: TYPE = SUBTYPE(is_shark); 1737 1738 1739% Subtypes of REAL 1740 1741AllReals: TYPE = SUBTYPE(LAMBDA (x:REAL): TRUE); 1742 1743NonNegReal: TYPE = SUBTYPE(LAMBDA (x:REAL): x >= 0); 1744 1745% Subtypes of INT 1746 1747DivisibleBy3: TYPE = SUBTYPE(LAMBDA (x:INT): EXISTS (y:INT): x = 3 * y); 1748 1749\endverbatim 1750 1751CVC3 provides integers as a built-in subtype \f$INT\f$ of \f$REAL\f$. 1752\f$INT\f$ is a subtype and not a base type 1753in order to allow mixed real/integer terms 1754without having to use coercion functions 1755such as 1756\f$\mathrm{int\_to\_real}:\mathrm{INT} \to \mathrm{REAL}\f$ 1757\f$\mathrm{real\_to\_int}:\mathrm{REAL} \to \mathrm{INT}\f$ 1758between terms of the two types. 1759It is <em>built-in</em> 1760because it is not definable by means of a first-order predicate. 1761 1762 1763Note that, with the syntax introduced so far, it seems that it may be possible 1764to define empty subtypes, that is, subtypes with no values at all. For example: 1765 1766\verbatim 1767NoReals: TYPE = SUBTYPE(LAMBDA (x:REAL): FALSE); 1768\endverbatim 1769 1770However, any attempt to do this results in an error. This is because CVC3's 1771logic assumes types are not empty. In fact, 1772each time a subtype \f$S\f$ is declared 1773CVC3 tries to prove that the subtype is non-empty; 1774more precisely, that it is non-empty in every model of the current context. 1775This is done simply by attempting to prove the validity of a formula of the form 1776\f$\exists\, x:T.\; p(x)\f$ where \f$T\f$ is the value type of which \f$S\f$ is a subtype, 1777and \f$p\f$ is the predicate defining \f$S\f$. 1778If CVC3 succeeds, the declaration is accepted. 1779If it fails, 1780CVC3 will issue a type exception and reject the declaration. 1781 1782CVC3 might fail to prove the non-emptyness of a subtype 1783either because the type is indeed empty in some models 1784or because of CVC3's incompleteness over quantified formulas. 1785Consider the following examples: 1786 1787\verbatim 1788Animal: TYPE; 1789 1790is_fish: Animal -> BOOLEAN; 1791 1792% Fish is a subtype of Animal: 1793 1794Fish: TYPE = SUBTYPE(is_fish); 1795 1796Interval_0_1: TYPE = SUBTYPE(LAMBDA (x:REAL): 0 < x AND x < 1); 1797 1798% Subtypes of [REAL, REAL] 1799 1800StraightLine: TYPE = SUBTYPE(LAMBDA (x:[REAL,REAL]): 3*x.0 + 2*x.1 + 6 = 0); 1801 1802 1803% Constant ARRAY subtype 1804 1805ConstArray: TYPE = SUBTYPE(LAMBDA (a: ARRAY INT OF REAL): 1806 EXISTS (x:REAL): FORALL (i:INT): a[i] = x); 1807\endverbatim 1808 1809Each of these subtype declarations is rejected. For instance, 1810the declaration of <tt>Fish</tt> is rejected 1811because there are models of CVC3's background theory 1812in which <tt>is_fish</tt> has an empty extension. 1813To fix that it is enough to introduce a free constant of type <tt>Animal</tt> 1814and assert that it is a <tt>Fish</tt> as we did above. 1815 1816In the case of <tt>Interval_0_1</tt> and <tt>Straightline</tt>, however, 1817the type is indeed non-empty in every model, 1818but CVC3 is unable to prove it. 1819In such cases, 1820the user can help CVC3 by explicitly providing a witness value for the subtype. 1821This is done with this alternative syntax for subtype declarations: 1822 1823\f[ 1824\mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p,t) 1825\f] 1826 1827where \f$p\f$ is again a unary predicate and 1828\f$t\f$ is a term (denoting an element) that satisfies \f$p\f$. 1829 1830The following subtype declarations with witnesses are accepted by CVC3. 1831 1832\verbatim 1833% Subtypes of REAL with witness 1834 1835Interval_0_1: TYPE = SUBTYPE(LAMBDA (x:REAL): 0 < x AND x < 1, 1/2); 1836 1837StraightLine: TYPE = SUBTYPE(LAMBDA (x:[REAL,REAL]): 3*x.0 + 2*x.1 + 6 = 0, (0, -3)); 1838\endverbatim 1839 1840 1841We observe that 1842the declaration of <tt>ConstArray</tt> in the first example is rightly rejected 1843under the empty context because the subtype can be empty in some models. 1844However, even under contexts that exclude this possibility CVC3 is still unable to 1845to prove the subtype's non-emptyness. 1846Again, a declaration with witness helps in this case. 1847Example: 1848 1849\verbatim 1850zero_array: ARRAY INT OF REAL; 1851 1852ASSERT FORALL (i:INT): zero_array[i] = 0; 1853 1854% At this point the context includes the constant array zero_array 1855% and the declaration below is accepted. 1856 1857ConstArray: TYPE = SUBTYPE(LAMBDA (a: ARRAY INT OF REAL): 1858 EXISTS (x:REAL): FORALL (i:INT): a[i] = x, zero_array); 1859\endverbatim 1860 1861 1862Adding witnesses to declarations to overcome CVC3's incompleteness 1863is an adequate, practical solution in most cases. 1864 1865<!-- 1866[CB: This works now!] 1867It should be clear though that it is only a partial solution. 1868For example, 1869the, admittedly contrived, declaration of the non-empty subtype below 1870by means of a non-linear arithmetic predicate is still rejected by CVC3: 1871 1872\verbatim 1873NonNegReal2: TYPE = SUBTYPE(LAMBDA (x: REAL): EXISTS (y:REAL): x = y*y, 4); 1874\endverbatim 1875 1876In this case the user must find alternative witnesses 1877(0 or 1 will do in the example above) 1878or alternative ways to model the problem at hand 1879that do not make use of the <tt>NonNegReal2</tt> subtype. 1880--> 1881 1882For additional convenience (when defining array types, for example) 1883CVC3 has a special syntax for specifying subtypes that are finite ranges of \f$INT\f$. 1884This is however just syntactic sugar. 1885 1886\verbatim 1887% subrange type 1888 1889FiniteRangeArray: TYPE = ARRAY [-10..10] OF REAL; 1890 1891 1892% equivalent but less readable formulations 1893 1894FiniteRange: TYPE = SUBTYPE(LAMBDA (x:INT): -10 <= x AND x <= 10); 1895 1896FiniteRangeArray2: TYPE = ARRAY FiniteRange OF REAL; 1897 1898FiniteRangeArray3: TYPE = ARRAY SUBTYPE(LAMBDA (x:INT): -10 <= x AND x <= 10) OF REAL; 1899\endverbatim 1900 1901 1902\subsubsection user_doc_pres_lang_subtyping Subtype Checking 1903 1904The subtype relation between a subtype and its immediate supertype is transitive. 1905This implies that every subtype is a subtype of some value type, 1906and so every term can be given a unique value type. 1907This is important because as far as type checking is concerned, 1908subtypes are ignored by CVC3. 1909By default, static type checking is enforced only at the level of maximal supertypes, 1910and subtypes play a role only during validity checking. 1911 1912In essence, 1913for every ground term of the form 1914\f$f(t_1, \ldots, t_n)\f$ with \f$i \geq 0\f$ in the logical context, 1915whenever \f$f\f$ has type \f$(S_1, \ldots, S_n) \to S\f$ 1916where \f$S\f$ is a subtype defined by a predicate \f$p\f$, 1917CVC3 adds to the context the assertion \f$p(f(t_1, \ldots, t_n))\f$ 1918constraining \f$f(t_1, \ldots, t_n)\f$ to be a value in \f$S\f$. 1919 1920<!--With quantifier-free contexts and queries,--> 1921This leads to correct answers by CVC3, 1922provided that all ground terms are 1923<em>well-subtyped</em> 1924in the logical context of the query; 1925that is, if for all terms like \f$f(t_1, \ldots, t_n)\f$ above 1926the logical context entails that \f$t_i\f$ is a value of \f$S_i\f$. 1927When that is not the case, CVC3 may return spurious countermodels to a query, 1928that is, countermodels that do not respect the subtyping constraints. 1929 1930For example, after the following declarations: 1931 1932\verbatim 1933Pos: TYPE = SUBTYPE(LAMBDA (x: REAL): x > 0, 1); 1934Neg: TYPE = SUBTYPE(LAMBDA (x: REAL): x < 0, -1); 1935 1936a: Pos; 1937b: REAL; 1938 1939f: Pos -> Neg = LAMBDA (x:Pos): -x; 1940\endverbatim 1941 1942CVC3 will reply "Valid", as it should, to the command: 1943 1944\verbatim 1945QUERY f(a) < 0; 1946\endverbatim 1947 1948However it will reply "Invalid" to the command: 1949 1950\verbatim 1951QUERY f(b) < 0; 1952\endverbatim 1953 1954or to: 1955 1956\verbatim 1957QUERY f(-4) < 0; 1958\endverbatim 1959 1960for that matter, 1961instead of complaining in either case that the query is not well-subtyped. 1962(The query is ill-subtyped in the first case 1963because there are models of the empty context in which 1964the constant <tt>b</tt> is a non-positive rational; 1965in the second case 1966because in all models of the context the term <tt>-4</tt> is non-positive.) 1967 1968In contrast, the command sequence 1969 1970\verbatim 1971ASSERT b > 2*a + 3; 1972QUERY f(b) < 0; 1973\endverbatim 1974 1975say, produces the correct expected answer 1976because in this case <tt>b</tt> is indeed positive in every model of the logical context. 1977 1978Semantically, CVC3's behavior is justified as follows. 1979Consider, just for simplicity (the general case is analogous), 1980a function symbol \f$f\f$ of type \f$S_1 \to T_2\f$ 1981where \f$S_1\f$ is a subtype of some value type \f$T_1\f$. 1982Instead of interpreting \f$S_1\f$ as <em>partial</em> function 1983that is total over \f$S_1\f$ and <em>undefined</em> outside \f$S_1\f$, 1984CVC3's interprets it as a <em>total</em> function from \f$T_1\f$ to \f$T_2\f$ 1985whose behavior outside \f$S_1\f$ is specified in an arbitrary, but fixed, way. 1986The specification of the behavior outside \f$S_1\f$ is internal to CVC3 1987and can, from case to case, go from being completely empty, 1988which means that 1989CVC3 will allow any possible way to extend \f$f\f$ from \f$S_1\f$ to \f$T_1\f$, 1990to strong enough to allow only one way to extend \f$f\f$. 1991The choice depends just on internal implementation considerations, 1992with the understanding that 1993the user is not really interested in \f$f\f$'s behavior outside \f$S_1\f$ anyway. 1994 1995A simple example of this approach is given 1996by the arithmetic division operation <tt>/</tt>. 1997Mathematically division is a partial function 1998from \f$\mathrm{REAL} \times \mathrm{REAL}\f$ to \f$\mathrm{REAL}\f$ 1999undefined over pairs in \f$\mathrm{REAL} \times \{0\}\f$. 2000CVC3 views <tt>/</tt> as a total function 2001from \f$\mathrm{REAL} \times \mathrm{REAL}\f$ to \f$\mathrm{REAL}\f$ 2002that maps pairs in \f$\mathrm{REAL} \times \{0\}\f$ to \f$0\f$ 2003and is defined as usual otherwise. 2004In other words, 2005CVC3 extends the theory of rational numbers 2006with the axiom \f$\forall\; x:\mathrm{REAL}.\; x/0 = 0\f$. 2007Under this view, queries like 2008 2009\verbatim 2010x: REAL; 2011 2012QUERY x/0 = 0 ; 2013QUERY 3/x = 3/x ; 2014\endverbatim 2015 2016are perfectly legitimate. Indeed the first formula is valid 2017because in each model of the empty context, 2018<tt>x/0</tt> is interpreted as zero and 2019<tt>=</tt> is interpreted as the identity relation. 2020The second formula is valid, more generally, because 2021for each interpretation of <tt>x</tt> the two arguments of <tt>=</tt> 2022will evaluate to the same rational number. 2023CVC3 will answer accordingly in both cases. 2024 2025While this behavior is logically correct, 2026it may be counter-intuitive to users, 2027especially in applications that intend to give CVC3 only well-subtyped formulas. 2028For these applications 2029it is more useful to the user to get a type error from CVC3 2030as soon as it receives an ill-subtyped assertion or query, 2031such as for instance the two queries above. 2032This feature is provided in CVC3 by using the command-line option 2033<tt>+tcc</tt>. The mechanism for checking well-subtypedness is described below. 2034 2035 2036\subsubsection user_doc_pres_lang_tccs Type Correctness Conditions 2037 2038CVC3 uses an algorithm based on Type Correctness Conditions, TCCs for short, 2039to determine if a term or formula is well-subtyped. 2040This of course requires first an adequate notion of well-subtypedness. 2041To introduce that notion, 2042let us start with the following definition 2043where \f$T\f$ is the union of CVC3's background theories. 2044 2045Let us say that 2046a (well-typed) term \f$t\f$ containing no proper subterms of type \f$\mathrm{BOOLEAN}\f$ is 2047<em>well-subtyped in a model \f$M\f$</em> of \f$T\f$ 2048(assigning an interpretation to all the free symbols and free variables of \f$t\f$) 2049if 2050 2051- \f$t\f$ is a constant or a variable, or 2052- it is of the form \f$f(t_1, \ldots, t_n)\f$ 2053where 2054\f$f\f$ has type \f$(S_1, \ldots, S_n) \to S\f$ and 2055each \f$t_i\f$ is well-subtyped in \f$M\f$ and interpreted as a value of \f$S_i\f$. 2056 2057Note that this inductive definition includes the case in which the term is 2058an atomic formula. 2059Then we can say that 2060an atomic formula is well-subtyped in a logical context \f$\Gamma\f$ 2061if it is well-subtyped in every model of \f$\Gamma\f$ and \f$T\f$. 2062 2063While this seems like a sensible definition of well-subtypedness for atomic formulas, 2064it is not obvious how to extend it properly to non-atomic formulas. 2065For example, defining a non-atomic formula to be well-subtyped in a model 2066if all of its atoms are well-subtyped is too stringent. 2067Perfectly reasonable formulas like 2068\f[ 2069y > 0 \;\Rightarrow\; x/y = z 2070\f] 2071with \f$x\f$, \f$y\f$, and \f$z\f$ free constants (or free variables) 2072of type \f$\mathrm{REAL}\f$, say, 2073would not be well-subtyped in the empty context 2074because there are models of \f$T\f$ in which the atom \f$x/y = z\f$ is not well-subtyped 2075(namely, those that interpret \f$y\f$ as zero). 2076 2077A better definition can be given 2078by treating logical connectives <em>non-strictly</em> with respect to ill-subtypedness. 2079More formally, 2080but considering for simplicity only formulas 2081built with atoms, negation and disjunction connectives, and existential quantifiers 2082(the missing cases are analogous), 2083we define a non-atomic formula \f$\phi\f$ to be well-subtyped 2084in a model \f$M\f$ of \f$T\f$ if one of the following holds: 2085 2086- \f$\phi\f$ has the form \f$\lnot \phi_1\f$ and 2087 \f$\phi_1\f$ is well-subtyped in \f$M\f$; 2088- \f$\phi\f$ has the form \f$\phi_1 \lor \phi_2\f$ and 2089 (i) both \f$\phi_1\f$ and \f$\phi_2\f$ are well-subtyped in \f$M\f$ or 2090 (ii) \f$\phi_1\f$ holds and is well-subtyped in \f$M\f$ or 2091 (iii) \f$\phi_2\f$ holds and is well-subtyped in \f$M\f$; 2092- \f$\phi\f$ has the form \f$\exists\:x.\; \phi_1\f$ and 2093 (i) \f$\phi_1\f$ holds and is well-subtyped in some model \f$M'\f$ 2094 that differs from \f$M\f$ at most in the interpretation of \f$x\f$ or 2095 (ii) \f$\phi_1\f$ is well-subtyped in every such model \f$M'\f$. 2096 2097In essence, this definition is saying that for well-subtypedness in a model 2098it is irrelevant if a formula \f$\phi\f$ has an ill-subtyped subformula, 2099as long as the truth value of \f$\phi\f$ is independent 2100from the truth value of that subformula. 2101 2102Now we can say in general that 2103a CVC3 formula is <em>well-subtyped in a context \f$\Gamma\f$</em> 2104if it is well-subtyped in every model of \f$\Gamma\f$ and \f$T\f$. 2105 2106According to this definition, the previous formula \f$y > 0 \;\Rightarrow\; x/y = z\f$, 2107which is equivalent to \f$\lnot(y > 0) \;\lor\; x/y = z\f$, 2108is well-subtyped in the empty context. 2109In fact, in all the models of \f$T\f$ that interpret \f$y\f$ as zero, 2110the subformula \f$\lnot(y > 0)\f$ is true and well-subtyped; 2111in all the others, both \f$\lnot(y > 0)\f$ and \f$x/y = z\f$ are well-subtyped. 2112 2113 2114This notion of well-subtypedness has a number of properties 2115that make it fairly robust. 2116One is that it is invariant with respect to equivalence in a context: 2117for every context \f$\Gamma\f$ and formulas \f$\phi, \phi'\f$ 2118such that \f$\Gamma \models_T \phi \Leftrightarrow \phi'\f$, 2119the first formula is well-subtyped in \f$\Gamma\f$ if and only if the second is. 2120 2121Perhaps the most important property, however, is that 2122the definition can be effectively reflected into CVC3's logic itself: 2123there is a procedure that 2124for any CVC3 formula \f$\phi\f$ can compute 2125a well-subtyped formula \f$\Delta_\phi\f$, 2126a <em>type correctness condition</em> for \f$\phi\f$, 2127such that 2128\f$\phi\f$ is well-subtyped in a context \f$\Gamma\f$ 2129if and only if 2130\f$\Gamma \models_T \Delta_\phi\f$. 2131This has the nice consequence that 2132the very inference engine of CVC3 can be used to check 2133the well-subtypedness of CVC3 formulas. 2134 2135When called with the TCC option on (by using the command-line option <tt>+tcc</tt>), CVC3 behaves as follows. 2136Whenever it receives an ASSERT or QUERY command, 2137the system computes the TCC of the asserted formula or query 2138and checks its validity in the current context (for ASSERTs, 2139before the formula is added to the logical context). 2140If it is able to prove the TCC valid, 2141it just adds the asserted formula to the context 2142or checks the validity of the query formula. 2143If it is unable to prove the TCC valid, 2144it raises an ill-subtypedness exception and aborts. 2145 2146<!-- 2147The command <tt>DUMP_TCC</tt> prints out the TCC for the formula 2148in the most recent ASSERT or QUERY, 2149and <tt>DUMP_TCC_PROOF</tt> produces the corresponding proof 2150(assuming TCC has been proven successfully). 2151--> 2152 2153It is worth pointing out that, 2154since CVC3 checks the validity of an asserted formula 2155in the current logical context at the time of the assertion, 2156the order in which formulas are asserted makes a difference. 2157For instance, 2158attempting to enter the following sequence of commands: 2159 2160\verbatim 2161f: [0..100] -> INT; 2162x: [5..10]; 2163y: REAL; 2164 2165ASSERT f(y + 3/2) < 15; 2166ASSERT y + 1/2 = x; 2167\endverbatim 2168 2169results in a TCC failure for the first assertion 2170because the context right before it does not 2171entail that the term <tt>y + 3/2</tt> is in the range <tt>0..100</tt>. 2172In contrast, the sequence 2173 2174\verbatim 2175f: [0..100] -> INT; 2176x: [5..10]; 2177y: REAL; 2178 2179ASSERT y + 1/2 = x; 2180ASSERT f(y + 3/2) < 15; 2181\endverbatim 2182 2183is accepted 2184because each of the formulas above is well-subtyped at the time of its assertion. 2185Note that 2186the assertion of both formulas together in the empty context with 2187 2188\verbatim 2189ASSERT f(y + 3/2) < 15 AND y + 1/2 = x 2190\endverbatim 2191 2192or with 2193 2194\verbatim 2195ASSERT y + 1/2 = x AND f(y + 3/2) < 15 2196\endverbatim 2197 2198is also accepted because the conjunction of the two formulas 2199is well-subtyped in the empty context. 2200 2201 2202\section user_doc_smtlib_lang SMT-LIB Input Language 2203 2204CVC3 is able to read and execute queries in the SMT-LIB format. 2205 2206Specifically, when called with the option <tt>-lang smt</tt> 2207it accepts as input an SMT-LIB <em>benchmark</em> 2208belonging to one of the SMT-LIB <em>sublogics</em>. 2209For a well-formed input benchmark, 2210CVC3 returns the string "sat", "unsat" or "unknown", 2211depending on whether it can prove the benchmark satisfiable, unsatisfiable, or neither. 2212 2213At the time of this writing CVC3 supported all SMT-LIB sublogics. 2214 2215We refer the reader to the 2216<a href="http://www.smt-lib.org">SMT-LIB website</a> 2217for information on SMT-LIB, its formats, its logics, and its on-line library of benchmarks. 2218 2219 2220*/ 2221 2222 2223