summaryrefslogtreecommitdiff
path: root/src/main
AgeCommit message (Collapse)Author
2013-04-26FCSimplex branch mergeTim King
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
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-26Make --incremental the default when running interactivelyMorgan Deters
2013-03-25finish removal of separateOutputKshitij Bansal
2013-03-23Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.Morgan Deters
2013-03-20Better reporting of detached git state in --version and --show-configMorgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-02-20Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.Morgan Deters
2013-02-16Fix version identification for new git repository.Morgan Deters
2013-02-15Merge branch '1.0.x'Kshitij Bansal
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-15make incremental+portfolio experimentalKshitij Bansal
2013-02-04Merge branch '1.0.x'Morgan Deters
2013-02-04driver::totalTime statistic is now reported correctly on crashes, tooMorgan Deters
2013-02-04Printing commands as they're executed now requires verbosity 3+Morgan Deters
2013-01-31Merge branch '1.0.x'Morgan Deters
2013-01-30correct output language bug with --dump-toMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2012-12-07Fix to portfolio buildsMorgan Deters
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)
2012-12-06Fix to portfolio buildsMorgan Deters
2012-11-29reliable benchmark corresponding to bug468Kshitij Bansal
2012-11-28fix a potential race (have failed to reproduce)Kshitij Bansal
2012-11-28treat all get commands like getValue (send only to lastWinner)Kshitij Bansal
2012-11-27fix 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-27more mac fixesMorgan Deters
2012-11-27fix for some Mac buildsMorgan Deters
2012-11-19Run lastWinner thread for all commands. Earlier behavior was to runKshitij Bansal
lastWinner only for (get-model) command, using thread0 otherwise.
2012-11-15some fixes for --threads=1Kshitij Bansal
2012-11-14Quantifiers enabled with portfolio, closing bug 423.Kshitij Bansal
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
just in general, and some documentation adjustments.
2012-10-19Fix problem with incremental with portfolio. Fixes bug 420.Kshitij Bansal
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
closes bug 419, fix typo, fix warning (this commit was certified error- and warning-free by the test-and-commit script.)
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-09* make Model class private (as discussed at meeting today)Morgan Deters
* fix minor issue with s-expr parsing in CVC and SMT grammars * other minor things (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-06* more complete support for --dump assertions:{pre,post}-PREPROCESSING-PASSMorgan Deters
* more minor cleanup/doc (this commit was certified error- and warning-free by the test-and-commit script.)
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-10-03--wait-to-join / --no-wait-to-join optionKshitij Bansal
workaround option till we fix bug 409. for now, I have kept --wait-to-join to be default (old behavior). We could technically make --no-wait-to-join the default when using non-incremental mode, but still possible for problems at exit I think (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
declare-const declare-funs declare-preds define simplify * don't output --help on bad options, just invite user to try --help * Datatypes from SMT2 parser now name the tester is-cons (e.g.) * unknown results produce models, --check-model doesn't fail hard for incorrect unknown models. removed the assert that kept arithmetic from producing models if it saw nonlinear (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-01"Fix" (disable) portfolio when using quantifiersKshitij Bansal
Other changes: * fix compile error in smt_engine in debug builds * add getLogicInfo in smt_engine * remove "empty-channel" and "disable-lemma-sharing" debug tags (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-28Some fixes to portfolioKshitij Bansal
* respect output lang * fix export variable for BOUND_VARIABLE * support export of SUBRANGE_TYPE * statistic for lastWinner, other minor stat changes * fix running of multiple threads on checsat/query * changes of Assert -> assert which became private * fix some destruction time order issues * fix Pickler with AssertionException going private Fixed by not fixing: * portfolio+datatypes does not work - added ExportUnsupportedException to more places, switches to sequential (still TODO / decide : not switch silently, but print error) > note: this exception now needs to be (and is) defined in expr.h Known issues: * problems in portfolio+quantifiers - at least some problems appear to be because of static variables (will be later "fixed" like the datatypes) (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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback