cvc4-1.3
NEWS
Go to the documentation of this file.
1 This file contains a summary of important user-visible changes.
2 
3 Changes since 1.2
4 =================
5 
6 New features:
7 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
8  previously missing
9 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
10 * Support in linear logics for /, div, and mod by constants (with the
11  --rewrite-divk command line option).
12 * Parsing support for TPTP's TFF and TFA formats.
13 * A new theory of strings: word (dis-)equations, length constraints,
14  regular expressions.
15 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
16  resolved.
17 * New :command-verbosity SMT option to silence success and error messages
18  on a per-command basis, and API changes to Command infrastructure to
19  support this.
20 
21 Behavioral changes:
22 * It is no longer permitted to request model or proof generation if there's
23  been an intervening push/pop.
24 * User-defined symbols (define-funs) are no longer reported in the output
25  of get-model commands.
26 * Exit codes are now more standard for UNIX command-line tools. Exit code
27  zero means no error---but the result could be sat, unsat, or unknown---and
28  nonzero means error.
29 
30 API changes:
31 * Expr::substitute() now capable of substituting operators (e.g.,
32  function symbols under an APPLY_UF)
33 * Numerous improvements to the Java language bindings
34 
35 Changes since 1.1
36 =================
37 
38 * Real arithmetic now has three simplex solvers for exact precision linear
39  arithmetic: the classical dual solver and two new solvers based on
40  techniques for minimizing the sum of infeasibilities. GLPK can now be used
41  as a heuristic backup to the exact precision solvers. GLPK must be enabled
42  at configure time. See --help for more information on enabling these solvers.
43 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
44 * support for theory "alternates": new ability to prototype new decision
45  procedures that are selectable at runtime
46 * various bugfixes
47 
48 Changes since 1.0
49 =================
50 
51 * bit-vector solver now has a specialized decision procedure for unsigned bit-
52  vector inequalities
53 * numerous important bug fixes, performance improvements, and usability
54  improvements
55 * support for multiline input in interactive mode
56 * Win32-building support via mingw
57 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
58 * user patterns for quantifier instantiation are now supported in the
59  SMT-LIBv1.2 parser
60 * --finite-model-find was incomplete when using --incremental, now fixed
61 * the E-matching procedure is slightly improved
62 * Boolean terms are now supported in datatypes
63 * tuple and record support have been added to the compatibility library
64 * driver verbosity change: for printing all commands as they're executed, you
65  now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
66  allows tracing the solver's activities (with -v and -vv) without having too
67  much output.
68 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
69  use -q. Previously, this would silence all output (including "sat" or
70  "unsat") as well. Now, single -q silences messages and warnings, and
71  double -qq silences all output (except on exception or signal).
72 
73 -- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500
This file contains a summary of important user visible changes Changes which were previously missing *New bv2nat int2bv operators for bitvector integer inter compatibility *Support in linear logics for
Definition: NEWS:4
void * Expr
struct CVC4::options::help__option_t help
This file contains a summary of important user visible changes Changes to_real
Definition: NEWS:4
distribution is under the terms of the modified BSD license certain builds of CVC4 link against GPLed and therefore the use of these builds is restricted in non open source projects See below for a discussion of CLN and and how to ensure you have a build that doesn t link against GPLed libraries THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS AS IS AND ANY EXPRESS OR IMPLIED BUT NOT LIMITED THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY OR CONSEQUENTIAL WHETHER IN STRICT OR EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE Morgan Deters< mdeters @cs.nyu.edu > excluded from the above copyright See src sat minisat Its Niklas Niklas Sorensson free of to any person obtaining a copy of this software and associated documentation to deal in the Software without including without limitation the rights to and or sell copies of the and to permit persons to whom the Software is furnished to do subject to the following conditions
Definition: COPYING:32
This file contains a summary of important user visible changes Changes to_int
Definition: NEWS:4
This file contains a summary of important user visible changes Changes since
Definition: NEWS:4
struct CVC4::options::in__option_t in
either version of the or(at your option) any later version.This program is distributed in the hope that it will be useful
struct CVC4::options::verbosity__option_t verbosity
distribution is under the terms of the modified BSD license certain builds of CVC4 link against GPLed and therefore the use of these builds is restricted in non open source projects See below for a discussion of CLN and and how to ensure you have a build that doesn t link against GPLed libraries THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS AS IS AND ANY EXPRESS OR IMPLIED BUT NOT LIMITED THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY OR CONSEQUENTIAL WHETHER IN STRICT OR EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE Morgan Deters< mdeters @cs.nyu.edu > Dec
Definition: COPYING:22
The core authors and designers of CVC4 are
Definition: AUTHORS:3
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
distribution is under the terms of the modified BSD license certain builds of CVC4 link against GPLed and therefore the use of these builds is restricted in non open source projects See below for a discussion of CLN and and how to ensure you have a build that doesn t link against GPLed libraries THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS AS IS AND ANY EXPRESS OR IMPLIED BUT NOT LIMITED THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY OR CONSEQUENTIAL WHETHER IN STRICT OR EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE Morgan Deters< mdeters @cs.nyu.edu > excluded from the above copyright See src sat minisat Its Niklas Niklas Sorensson free of to any person obtaining a copy of this software and associated documentation to deal in the Software without including without limitation the rights to use
Definition: COPYING:32
uninterpreted function application
Definition: kind.h:97
The core authors and designers of CVC4 New York University Clark New York University Francois Paris Sud University Christopher New York University Morgan New York University Liana New York University Dejan New York University Tim New York University Tianyi The University of Iowa Andrew The University of Iowa Cesare The University of Iowa CVC4 is the fourth in the CVC series of tools(CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version.Information about authors of previous CVC tools is included with their distributions.CVC4 contains MiniSAT code by Niklas Een and Niklas Sorensson The CVC4 parser incorporates some code from ANTLR3
struct CVC4::options::interactive__option_t interactive
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory(or a combination of such theories).It is the fourth in the Cooperating Validity Checker family of tools(CVC
distribution is under the terms of the modified BSD license certain builds of CVC4 link against GPLed and therefore the use of these builds is restricted in non open source projects See below for a discussion of CLN and GLPK
Definition: COPYING:5
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online at
Definition: README:39
distribution is under the terms of the modified BSD license certain builds of CVC4 link against GPLed and therefore the use of these builds is restricted in non open source projects See below for a discussion of CLN and and how to ensure you have a build that doesn t link against GPLed libraries THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS AS IS AND ANY EXPRESS OR IMPLIED BUT NOT LIMITED THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY OR CONSEQUENTIAL WHETHER IN STRICT OR EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE Morgan Deters< mdeters @cs.nyu.edu > Thu
Definition: COPYING:22
This file contains a summary of important user visible changes Changes which were previously missing *New bv2nat int2bv operators for bitvector integer inter compatibility *Support in linear logics div
Definition: NEWS:4
This file contains a summary of important user visible changes Changes is_int
Definition: NEWS:4