summaryrefslogtreecommitdiff
path: root/src/main/driver_unified.cpp
AgeCommit message (Collapse)Author
2014-04-06fix for hiding prompt/header in shell, error-behavior options as in SMTLIBKshitij Bansal
2014-03-19Set dumping options from (set-option..) and API more directly.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-22Fix to interactive mode determination.Morgan Deters
2013-11-29Fix portfolio compile error.Morgan Deters
2013-11-27Incremental is now on by default when using from API, off for command-line ↵Morgan Deters
driver except in interactive mode.
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-08-13--segv-nospin is now default.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-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Make --incremental the default when running interactivelyMorgan Deters
2013-02-16Fix version identification for new git repository.Morgan Deters
2013-02-15prvs commit: lower warning to noticeKshitij Bansal
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
2013-02-15make incremental+portfolio experimentalKshitij Bansal
2013-02-04driver::totalTime statistic is now reported correctly on crashes, tooMorgan Deters
2013-01-30correct output language bug with --dump-toMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09typoKshitij Bansal
2012-10-09bugfix: isQuantified, bugfix: flushKshitij Bansal
2012-10-06* Clean up some options documentationMorgan 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.)
2012-09-29Fix a few segfaults in driver.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-28Public interface review items:Morgan Deters
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
* Change --lang smt to mean SMT-LIBv2 * --lang smt1 now means SMT-LIBv1 * SMT-LIBv2 parser now gives helpful error if input looks like v1 * SMT-LIBv1 parser now gives helpful error if input looks like v2 * CVC presentation language parser now gives helpful error if input looks like either SMT-LIB v1 or v2 * Other associated changes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-26The Tuesday Afternoon Catch-All Commit (TACAC):Morgan Deters
* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds) * New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.). * SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core) (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
Statistics-printing problem, limited to certain benchmarks). Mark some unlabeled header files "cvc4_private.h". Other minor cleanup. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry). The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it). This is part of the ongoing effort to clean up the public interface. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-21better verbosity support (so it's sensible when the library is used via the API)Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-14Fix a few minor issues in options processing, improving usability, ↵Morgan Deters
consistency, error-reporting, and documentation.
2012-09-08Some minor changes after reviewing the portfolio "unified driver" commit.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-08Single driver for both sequential and portfolioKshitij Bansal
A "command executer" layer between parsing commands and invoking them. New implementation of portfolio driver splits only when check-sat or query command is encountered, and then switches back to sequential till the next one. As side effect, restores functionality of interactive mode and push/pops.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback