Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2013-02-04 | Printing commands as they're executed now requires verbosity 3+ | Morgan Deters | |
2013-01-28 | Updated NEWS for recent changes. | Morgan Deters | |
2013-01-23 | add user patterns to the Smt1 parser; update NEWS file | Morgan Deters | |
2012-12-06 | * tuple and record support in compatibility library | Morgan Deters | |
(this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-12-01 | Cutting release 1.0.1.0 | Morgan Deters | |
2012-10-06 | * Clean up some options documentation | Morgan Deters | |
* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2009-11-03 | commit of project structure including autotools support | Morgan Deters | |