summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2013-08-13--segv-nospin is now default.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-24Fixes for building with mingw win64.Morgan Deters
2013-07-24Don't allow --stats if not a statistics-enabled buildMorgan Deters
2013-07-23Some fixes for (get-info :all-options)Morgan Deters
2013-07-23fix for win32 option parsing via mingw32Morgan Deters
2013-07-23(get-info :all-options) to get option values; also command-line option ↵Morgan Deters
suggestions
2013-06-06IDL example theory (to be used with --use-theory=idl).Dejan Jovanović
2013-05-17A couple of fixes to the get-option command for compliance with SMT-LIB.Morgan Deters
Thanks to David Cok for reporting this issue.
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan 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-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-19Fix an options-processing bug on some platforms (e.g., MacOS).Morgan Deters
2012-11-30renaming --smtlib to --smtlib-strict; removing --smtlib2 optionMorgan Deters
2012-11-30Adding smtname level options for tlimit, rlimit, etc. Fix to the internal ↵Tim King
documentation in base_options.
2012-10-26build options sources into distribution tarballs (in the same way that antlr ↵Morgan Deters
grammars are pre-generated for tarballs). this speeds up user builds by not requiring them to run the mkoptions script (unless they change an options meta-file). i've tested this, but let me know if there are any problems you encounter.
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
just in general, and some documentation adjustments.
2012-10-22one more incorrect #line fixedMorgan Deters
2012-10-14fix #line number warnings (sorry!)Morgan 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-10Abstract values for SMT-LIB.Morgan Deters
Also fix bug 421 relating to incrementality and models. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09usability: remove --no-interactive from --smtlib optionMorgan Deters
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-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
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-29draft RELEASE-NOTES file, and minor release stuffMorgan Deters
2012-09-28some fixes to build systemMorgan 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-27finally, a portable solutionMorgan Deters
2012-09-27fix for non-MacMorgan Deters
2012-09-27speed up mkoptions script (esp. on Macs)Morgan Deters
2012-09-27better progress indicator for mkoptionsMorgan Deters
2012-09-25fix some Mac issuesMorgan Deters
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-21SMT-LIBv2 compliance updates:Morgan Deters
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (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-20some bugfixes that come as a result of debugging some CASCADE/C stuff..Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-17speed up option-file generation on Mac OS by an order of magnitudeMorgan Deters
2012-09-15minor interface improvements, compliance fixesMorgan 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-12Adding model assertions after SAT responses.Morgan Deters
To enable, use --check-models. Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not. This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too. By default, --check-models is quiet (no output unless it detects a problem). That allows regression runs to pass unless there are problems: make regress CVC4_REGRESSION_ARGS=--check-models To see it work, use -v in addition to --check-models. There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state. --check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models. This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting). Also: * TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants) * The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2) * The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)
2012-09-08Add [*] footnotes to --help output indicating for many options --FOO that ↵Morgan Deters
there are --no-FOO variants.
2012-09-06allow SmtEngine::setOption() for trace and debug tagsMorgan Deters
2012-09-06add --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)Morgan Deters
2012-08-29* Numerous documentation fixes (fix doxygen warnings, add missing ↵Morgan Deters
documentation, etc.). * Remove sat_module.cpp, which was no longer used (was previously refactored?)
2012-08-29To the build system:Morgan Deters
* Fix "make distclean." This should fix the "local regressions fail" that caused documentation, debian, and "distcheck" nightly build targets to fail. * "make clean" now removes some options stuff that previously required a "make distclean." * Cosmetic and portability adjustments.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback