From: Morgan Deters Date: Tue, 30 Apr 2013 17:59:52 +0000 (-0400) Subject: update versioning X-Git-Tag: cvc5-1.0.0~7287^2~134^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=843cfdae175f8ef6fc3c7a3e3a5fa4e7f37863e1;p=cvc5.git update versioning --- diff --git a/INSTALL b/INSTALL index 57620bd72..cbf8c8a86 100644 --- a/INSTALL +++ b/INSTALL @@ -1,4 +1,4 @@ -CVC4 release version 1.1. +CVC4 release version 1.2. *** Quick-start instructions diff --git a/NEWS b/NEWS index 8c93b1478..17a934729 100644 --- a/NEWS +++ b/NEWS @@ -3,7 +3,15 @@ This file contains a summary of important user-visible changes. Changes since 1.1 ================= -* nothing notable yet +* Real arithmetic now has three simplex solvers for exact precision linear + arithmetic: the classical dual solver and two new solvers based on + techniques for minimizing the sum of infeasibilities. GLPK can now be used + as a heuristic backup to the exact precision solvers. GLPK must be enabled + at configure time. See --help for more information on enabling these solvers. +* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2 +* support for theory "alternates": new ability to prototype new decision + procedures that are selectable at runtime +* various bugfixes Changes since 1.0 ================= diff --git a/README b/README index bda916610..ddb8c856e 100644 --- a/README +++ b/README @@ -1,4 +1,4 @@ -This is CVC4 release version 1.1. For build and installation notes, +This is CVC4 release version 1.2. For build and installation notes, please see the INSTALL file included with this distribution. This first official release of CVC4 is the result of more than three diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 43d87487a..b45602d87 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,4 +1,4 @@ -Release Notes for CVC4 1.1, April 2013 +Release Notes for CVC4 1.2, May 2013 ** Getting started @@ -17,7 +17,7 @@ this, you can use the --lang option. The CVC family of systems relies on Type Correctness Conditions (TCCs) when mixing two types that have a compatible base type. TCCs, and the checking of -such, are not supported by CVC4 1.1. This is an issue when mixing integers and +such, are not supported by CVC4 1.2. This is an issue when mixing integers and reals. A function defined only on integers can be applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain. It is up to the user to ensure that the REAL expression must be an integer. If the REAL expression is not @@ -118,7 +118,7 @@ heap. ** Proof support -CVC4 1.1 has limited support for proofs, and they are disabled by default. +CVC4 1.2 has limited support for proofs, and they are disabled by default. (Run the configure script with --enable-proof to enable proofs). Proofs are exported in LFSC format and are limited to the propositional backbone of the discovered proof (theory lemmas are stated without proof in this @@ -126,7 +126,7 @@ release). ** Nonlinear arithmetic -CVC4 1.1 has a state-of-the-art linear arithmetic solver. However, there +CVC4 1.2 has a state-of-the-art linear arithmetic solver. However, there is extremely limited support for nonlinear arithmetic in this release. ** Portfolio solving diff --git a/library_versions b/library_versions index 1cf417e36..f88f8e40b 100644 --- a/library_versions +++ b/library_versions @@ -50,3 +50,4 @@ 1\.1 libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.1\.1-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 +1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0