summaryrefslogtreecommitdiff
path: root/NEWS
AgeCommit message (Collapse)Author
2016-06-09Dummy commit.Clark Barrett
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-03Merge branch '1.4.x'Morgan Deters
Conflicts: NEWS
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks ↵Morgan Deters
Christoph Sticksel for reporting).
2014-10-03More array constants and parsing: better error messages, extend to CVC ↵Morgan Deters
presentation language.
2014-10-03Note array const support in NEWSMorgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-13New versioning for development version.Morgan Deters
2014-07-02Minor.Morgan Deters
2014-07-01reword NEWSMorgan Deters
2014-06-30Update NEWSKshitij Bansal
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-19Documentation clean-ups.Morgan Deters
2014-06-19Versioning preparation.Morgan Deters
2014-06-10Some news about API changes.Morgan Deters
2014-01-08Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS config/cvc4.m4
2014-01-08Switch license default back to BSD, and add --best and --enable-gpl options.Morgan Deters
2013-12-24Merge branch '1.3.x'Morgan Deters
Conflicts: NEWS
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-17Merge branch '1.3.x'Morgan Deters
Conflicts: COPYING NEWS
2013-12-17some config changes: new --bsd option, readline gives warning, default build ↵Morgan Deters
is now production.
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-10Update NEWS.Morgan Deters
2013-12-06Initializing 1.3.x branch.Morgan Deters
2013-12-05Fix NEWS.Morgan Deters
2013-12-05NEWS reorganization.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-03change string newsTianyi Liang
2013-12-02Update NEWS file.Morgan Deters
2013-11-27Some versioning in advance of the 1.3 release.Morgan Deters
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-09-11Theory of strings.Tianyi Liang
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
2013-05-29Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵Morgan Deters
unknown key.
2013-05-20Don't allow get-model & co after a user push/popMorgan Deters
This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this.
2013-05-08Prerelease versioning for 1.2.xMorgan Deters
2013-05-08Cutting release 1.2.1.2Morgan Deters
2013-04-03Pre-release versioningMorgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-03updated NEWS to include inequality solverLiana Hadarean
2013-04-01Merging some cleanup work:Morgan Deters
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-02-20Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.Morgan Deters
2013-02-04Printing commands as they're executed now requires verbosity 3+Morgan Deters
2013-01-28Updated NEWS for recent changes.Morgan Deters
2013-01-23add user patterns to the Smt1 parser; update NEWS fileMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback