Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* This is a feature that Dejan and I want for the upcoming tutorial.
It allows rapid prototyping of new decision procedure implementations
(which we may choose to demonstrate), and a new --use-theory command-line
option to select from different available implementations. It has no
affect on the current set of theories, as no "alternates" are defined.
* Also update the new-theory script, which was broken and incomplete.
|
|
|
|
|
|
|
|
* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed
|
|
|
|
references)
|
|
|
|
|
|
|
|
|
|
|
|
explicit template instantiation rules, -fvisibility=hidden, and the way that
Apple distributes libstdc++.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
don't advertise them in help listing for --enable-language-bindings
|
|
** remove a number of warnings in bindings generation
** give appropriate names for operator-overloading
** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code
* Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
|
|
|
|
1. The source tree was configured.
2. The builds directory was removed.
3. The source tree was re-configured.
Which led to a nasty dangling symlink that caused (3) to abort.
Fixed.
|
|
just in general, and some documentation adjustments.
|
|
* Better errors/warnings when SWIG isn't installed (resolves bug 373)
* Allow compatibility bindings to be built when SWIG isn't available
|
|
|
|
* 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.
|
|
|
|
|
|
* 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.)
|
|
consistency, error-reporting, and documentation.
|
|
College London (via Peter Collingbourne):
cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)
These patches will help the group build Boogie support for CVC4.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
should work now
|
|
|
|
Also some cleanup of option-related exceptions infrastructure.
|
|
1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)
The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:
* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***
Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).
Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).
Benefits of the new options system include:
1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose
I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
|