Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-12-22 | Fix to interactive mode determination. | Morgan Deters | |
2013-12-22 | Fix option specification. | Morgan Deters | |
2013-12-17 | some config changes: new --bsd option, readline gives warning, default build ↵ | Morgan Deters | |
is now production. | |||
2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
2013-11-29 | Fix portfolio compile error. | Morgan Deters | |
2013-11-27 | Incremental is now on by default when using from API, off for command-line ↵ | Morgan Deters | |
driver except in interactive mode. | |||
2013-11-12 | Minor portfolio fixes for some platforms. | 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-12 | fix bug 534: portfolio define-fun duplicate model | Kshitij Bansal | |
2013-09-09 | Fix portfolio on bug411.smt2. (get-model command should only go to last winner) | Morgan Deters | |
2013-08-13 | --segv-nospin is now default. | Morgan Deters | |
2013-07-24 | some portfolio driver cleanup | Morgan Deters | |
2013-07-13 | Fix language bindings and portfolio builds. | 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-28 | Fix portfolio builds after yesterday's commits. | Morgan Deters | |
2013-06-27 | Remove output.h from public space, to avoid clashes with symbols defined in ↵ | Morgan Deters | |
users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. | |||
2013-05-17 | Add support for --dump-models option, in preparation for casc. | Andrew Reynolds | |
2013-05-17 | Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵ | Morgan Deters | |
in some places Thanks to David Cok for reporting these issues. | |||
2013-04-26 | FCSimplex branch merge | Tim King | |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters | |
2013-04-01 | update copyrights | Morgan Deters | |
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-26 | Make --incremental the default when running interactively | Morgan Deters | |
2013-03-25 | finish removal of separateOutput | Kshitij Bansal | |
2013-03-23 | Fix bug in portfolio executor output; fixes nightly portfolio-checking runs. | Morgan Deters | |
2013-03-20 | Better reporting of detached git state in --version and --show-config | Morgan Deters | |
2013-03-20 | Interactive mode support for multiline input | Morgan Deters | |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-02-20 | Single -q quiets messages/warnings. Double -qq silences sat/unsat output too. | Morgan Deters | |
2013-02-16 | Fix version identification for new git repository. | Morgan Deters | |
2013-02-15 | Merge branch '1.0.x' | Kshitij Bansal | |
2013-02-15 | prvs commit: lower warning to notice | Kshitij Bansal | |
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu> | |||
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-04 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-04 | driver::totalTime statistic is now reported correctly on crashes, too | Morgan Deters | |
2013-02-04 | Printing commands as they're executed now requires verbosity 3+ | Morgan Deters | |
2013-01-31 | Merge branch '1.0.x' | Morgan Deters | |
2013-01-30 | correct output language bug with --dump-to | Morgan Deters | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters | |
2012-12-07 | Fix to portfolio builds | Morgan Deters | |
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e) | |||
2012-12-06 | Fix to portfolio builds | Morgan Deters | |
2012-11-29 | reliable benchmark corresponding to bug468 | Kshitij Bansal | |
2012-11-28 | fix a potential race (have failed to reproduce) | Kshitij Bansal | |
2012-11-28 | treat all get commands like getValue (send only to lastWinner) | Kshitij Bansal | |
2012-11-27 | fix in CommandSequence invoke : maintain success/failure. Fixes bug 465. | Kshitij Bansal | |
(this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-27 | more mac fixes | Morgan Deters | |
2012-11-27 | fix for some Mac builds | Morgan Deters | |