Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
2017-07-05 | Update unit test, news. | ajreynol | |
2017-06-30 | Updated NEWS, README, RELEASE-NOTES. | Clark Barrett | |
2016-06-09 | Dummy commit. | Clark Barrett | |
2014-10-23 | Parsing 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-03 | Merge branch '1.4.x' | Morgan Deters | |
Conflicts: NEWS | |||
2014-10-03 | Fix output of integer-valued real constants in SMT-LIB models (thanks ↵ | Morgan Deters | |
Christoph Sticksel for reporting). | |||
2014-10-03 | More array constants and parsing: better error messages, extend to CVC ↵ | Morgan Deters | |
presentation language. | |||
2014-10-03 | Note array const support in NEWS | Morgan Deters | |
2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters | |
2014-07-13 | New versioning for development version. | Morgan Deters | |
2014-07-02 | Minor. | Morgan Deters | |
2014-07-01 | reword NEWS | Morgan Deters | |
2014-06-30 | Update NEWS | Kshitij Bansal | |
2014-06-21 | Some minor cleanup and documentation. | Morgan Deters | |
2014-06-19 | Documentation clean-ups. | Morgan Deters | |
2014-06-19 | Versioning preparation. | Morgan Deters | |
2014-06-10 | Some news about API changes. | Morgan Deters | |
2014-01-08 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS config/cvc4.m4 | |||
2014-01-08 | Switch license default back to BSD, and add --best and --enable-gpl options. | Morgan Deters | |
2013-12-24 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: NEWS | |||
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters | |
2013-12-17 | Merge branch '1.3.x' | Morgan Deters | |
Conflicts: COPYING NEWS | |||
2013-12-17 | some config changes: new --bsd option, readline gives warning, default build ↵ | Morgan Deters | |
is now production. | |||
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-12-10 | Update NEWS. | Morgan Deters | |
2013-12-06 | Initializing 1.3.x branch. | Morgan Deters | |
2013-12-05 | Fix NEWS. | Morgan Deters | |
2013-12-05 | NEWS reorganization. | Morgan Deters | |
2013-12-04 | Don't put define-funs in model output; bug 411 testcase no longer relevant. | Morgan Deters | |
2013-12-03 | change string news | Tianyi Liang | |
2013-12-02 | Update NEWS file. | Morgan Deters | |
2013-11-27 | Some versioning in advance of the 1.3 release. | Morgan Deters | |
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-09-11 | Theory of strings. | Tianyi Liang | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-09-09 | Support per-command verbosity settings. | Morgan Deters | |
2013-07-11 | Support 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-24 | Support 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-29 | Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵ | Morgan Deters | |
unknown key. | |||
2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan 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-08 | Prerelease versioning for 1.2.x | Morgan Deters | |
2013-05-08 | Cutting release 1.2.1.2 | Morgan Deters | |
2013-04-03 | Pre-release versioning | Morgan Deters | |
2013-04-03 | Some 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-03 | updated NEWS to include inequality solver | Liana Hadarean | |
2013-04-01 | Merging 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-22 | Support for Boolean term conversion in datatypes. | Morgan Deters | |
2013-03-20 | Interactive mode support for multiline input | Morgan Deters | |
2013-02-20 | Single -q quiets messages/warnings. Double -qq silences sat/unsat output too. | Morgan Deters | |