| Age | Commit message (Collapse) | Author |
|---|
|
Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.
Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
This PR makes sure that option handlers have access to both the canonical option name and the option name that was actually used. It also updates the options README and gets rid of the base_handlers.h of which only a fraction was used.
|
|
This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.
|
|
This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).
|
|
This PR does some general cleanup in the mkoptions.py script: removal of obsolete code and some fixes to the comments.
|
|
This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.
|
|
This PR removes the next two heavily specialized template functions. Both Options::assign() and Options::assignBool() are only used within options.cpp now and there is thus no reason to keep them in the public interface. Furthermore, we can just make them properly named functions instead of template functions.
|
|
This PR gets rid of the templated Options::ref() method (and all its specializations for every option).
|
|
This PR replaces the templated Options::setDefault() methods by new non-templated free functions options::{module}::setDefault{option}().
These methods should be used instead of the common if (!set by user) { set option value } pattern.
|
|
This PR follows a suggestions of @ajreynol to use public references instead of getter functions to access the individual option modules.
|
|
This PR moves the option names out of the option struct (which will be removed) to free constexpr string constants.
|
|
|
|
This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.
|
|
This PR replaces the confusing co-existence of long and smt_name for options by long and a list of alias.
|
|
This PR splits the OptionsHolder class into separate holder classes for every options module and makes them directly accessible via appropriate Options::<module>() methods. We forward declare these new holder classes and thereby retain that we only need to recompile when we change an option module that is explicitly included.
All (generated) methods that previously accessed the old holder object are changed to instead use the new holder objects.
This PR does the bare minimum to do this change, further PRs will eventually get rid of all template specializations that currently surround our options class.
|
|
This PR further simplifies the option declaration by removing the header attribute from module options.
Instead of specifying it manually, it is now automatically generated from the filename of the toml file. The header files and the toml files use matching names already, so this PR simply removes another mechanism that is not used anyway.
This PR also does a minor cleanup of the Options class in the mkoptions.py script.
|
|
This PR removes the possibility of declaring options read_only.
It's only effect is making an attempts to disallow changing the respective option from within our internal code (by not providing a setter method). However, a "read-only" option can still be set via the setOption() methods that is also used by the API, and by SMT-LIB's set-option.
|
|
This PR simplifies the generated code for Options::getOption() and Options::setOption(). It now uses less string streams, less temporary vectors and the new options[...] syntax (instead of options::...().
|
|
This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.
|
|
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular
- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()
The removed methods are only used in few places with are changed to using Options::current().X() instead.
In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
|
|
This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This PR does another round of refactoring of the resource manager and related code.
- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager
Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.
|
|
|
|
|
|
The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
|
|
Signed-off-by: Everett Maus <evmaus@google.com>
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
getName() returns the long option name if it exists and an empty string otherwise.
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
TODO: cvc4autoconfig.h
|
|
Not adding the argument description for non-{bool,void} options is now an error.
Further, adds missing argument descriptions.
|
|
|
|
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.
The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.
This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
|
