diff options
-rw-r--r-- | src/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/api/cpp/cvc5_kind.h | 16 | ||||
-rw-r--r-- | src/omt/bitvector_optimizer.cpp | 128 | ||||
-rw-r--r-- | src/omt/integer_optimizer.cpp | 13 | ||||
-rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/options/README | 127 | ||||
-rw-r--r-- | src/options/README.md | 211 | ||||
-rw-r--r-- | src/options/base_handlers.h | 87 | ||||
-rw-r--r-- | src/options/mkoptions.py | 51 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 117 | ||||
-rw-r--r-- | src/options/options_handler.h | 144 | ||||
-rw-r--r-- | src/options/options_template.cpp | 91 | ||||
-rw-r--r-- | src/options/prop_options.toml | 8 | ||||
-rw-r--r-- | src/smt/optimization_solver.cpp | 91 | ||||
-rw-r--r-- | src/smt/optimization_solver.h | 121 | ||||
-rw-r--r-- | src/theory/arith/kinds | 2 | ||||
-rw-r--r-- | src/theory/arith/nl/pow2_solver.cpp | 73 | ||||
-rw-r--r-- | src/theory/inference_id.cpp | 4 | ||||
-rw-r--r-- | src/theory/inference_id.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_opt_white.cpp | 20 | ||||
-rw-r--r-- | test/unit/theory/theory_int_opt_white.cpp | 16 | ||||
-rw-r--r-- | test/unit/theory/theory_opt_multigoal_white.cpp | 49 |
22 files changed, 783 insertions, 593 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index bec3a8345..2419e1e41 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -441,6 +441,7 @@ libcvc5_add_sources( theory/arith/nl/nonlinear_extension.h theory/arith/nl/poly_conversion.cpp theory/arith/nl/poly_conversion.h + theory/arith/nl/pow2_solver.cpp theory/arith/nl/pow2_solver.h theory/arith/nl/stats.cpp theory/arith/nl/stats.h diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2ec190360..2c5d2873e 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` */ IAND, + /** + * Operator for raising 2 to a non-negative integer power + * + * Create with: + * - `Solver::mkOp(Kind kind) const` + * + + * Parameters: + * - 1: Op of kind IAND + * - 2: Integer term + * + * Create with: + * - `Solver::mkTerm(const Op& op, const Term& child) const` + * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` + */ + POW2, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index bce6c9b6d..01cb6da42 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -53,15 +53,13 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -104,39 +102,35 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); } intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - upperBound = value.getConst<BitVector>(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // lowerBound == pivot ==> upperbound = lowerbound + 1 - // and lowerbound <= target < upperbound is UNSAT - // return the upperbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - lowerBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + upperBound = value.getConst<BitVector>(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // lowerBound == pivot ==> upperbound = lowerbound + 1 + // and lowerbound <= target < upperbound is UNSAT + // return the upperbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + lowerBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, @@ -148,15 +142,13 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); - } - + // the last result that is SAT + Result lastSatResult = intermediateSatResult; // value equals to upperBound value = optChecker->getValue(target); @@ -196,39 +188,35 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, nm->mkNode(GTOperator, target, nm->mkConst(pivot)), nm->mkNode(LEOperator, target, nm->mkConst(upperBound)))); intermediateSatResult = optChecker->checkSat(); - if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::SAT) + switch (intermediateSatResult.isSat()) { - value = optChecker->getValue(target); - lowerBound = value.getConst<BitVector>(); - } - else if (intermediateSatResult.isSat() == Result::UNSAT) - { - if (lowerBound == pivot) - { - // upperbound = lowerbound + 1 - // and lowerbound < target <= upperbound is UNSAT - // return the lowerbound + case Result::SAT_UNKNOWN: optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); - } - else - { - upperBound = pivot; - } - } - else - { - optChecker->pop(); - return OptimizationResult(OptimizationResult::UNKNOWN, value); + return OptimizationResult(intermediateSatResult, value); + case Result::SAT: + lastSatResult = intermediateSatResult; + value = optChecker->getValue(target); + lowerBound = value.getConst<BitVector>(); + break; + case Result::UNSAT: + if (lowerBound == pivot) + { + // upperbound = lowerbound + 1 + // and lowerbound < target <= upperbound is UNSAT + // return the lowerbound + optChecker->pop(); + return OptimizationResult(lastSatResult, value); + } + else + { + upperBound = pivot; + } + break; + default: Unreachable(); } optChecker->pop(); } - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } } // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 045268337..379b0cd43 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -33,13 +33,10 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; - if (intermediateSatResult.isUnknown()) + if (intermediateSatResult.isUnknown() + || intermediateSatResult.isSat() == Result::UNSAT) { - return OptimizationResult(OptimizationResult::UNKNOWN, value); - } - if (intermediateSatResult.isSat() == Result::UNSAT) - { - return OptimizationResult(OptimizationResult::UNSAT, value); + return OptimizationResult(intermediateSatResult, value); } // node storing target > old_value (used in optimization loop) Node increment; @@ -56,12 +53,14 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, // then assert optimization_target > current_model_value incrementalOperator = kind::GT; } + Result lastSatResult = intermediateSatResult; // Workhorse of linear search: // This loop will keep incrmenting/decrementing the objective until unsat // When unsat is hit, // the optimized value is the model value just before the unsat call while (intermediateSatResult.isSat() == Result::SAT) { + lastSatResult = intermediateSatResult; value = optChecker->getValue(target); Assert(!value.isNull()); increment = nm->mkNode(incrementalOperator, target, value); @@ -69,7 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, intermediateSatResult = optChecker->checkSat(); } optChecker->pop(); - return OptimizationResult(OptimizationResult::OPTIMAL, value); + return OptimizationResult(lastSatResult, value); } OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 26ced1a24..cc7b621a8 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -17,7 +17,6 @@ check_python_module("toml") libcvc5_add_sources( - base_handlers.h decision_weight.h didyoumean.cpp didyoumean.h diff --git a/src/options/README b/src/options/README deleted file mode 100644 index 868690b85..000000000 --- a/src/options/README +++ /dev/null @@ -1,127 +0,0 @@ -Modules -======= - - Each options module starts with the following required attributes: - - id ... (string) ID of the module (e.g., "ARITH") - name ... (string) name of the module (e.g., "Arithmetic Theory") - header ... (string) name of the options header to generated (e.g., "options/arith_options.h") - - A module defines 0 or more options. - - In general, each attribute/value pair is required to be in one line. - Comments start with # and are not allowed in attribute/value lines. - - -Options -======= - - Options can be defined with the [[option]] tag, the required attributes for - an option are: - - category ... (string) common | expert | regular | undocumented - type ... (string) C++ type of the option value - - Optional attributes are: - - name ... (string) option name that is used to access via - options::<name>() - smt_name ... (string) alternative name to access option via - set-option/get-option commands - short ... (string) short option name consisting of one character - (no '-' prefix required) - long ... (string) long option name (required if short is specified, - no '--' prefix required). - long option names may have a suffix '=XXX' where - 'XXX' can be used to indicate the type of the - option value, e.g., '=MODE', '=LANG', '=N', ... - default ... (string) default value of type 'type' - handler ... (string) handler for parsing option values before setting - option - predicates ... (list) functions that check whether given option value is - valid - includes ... (list) header files required by handler/predicates - alternate ... (bool) true (default): add --no-<long> alternative option - false: omit --no-<long> alternative option - help ... (string) documentation (required if category is not - undocumented) - - Note that if an option defines a long option name with type 'bool', - mkoptions.py automatically generates a --no-<long> option to set the option - to false. - This behaviour can be explicitely disabled for options with attribute - alternate = false. - More information on how to use handler and predicates can be found - at the end of the README. - - - Example: - - [[option]] - name = "outputLanguage" - smt_name = "output-language" - category = "common" - short = "" - long = "output-lang=LANG" - type = "OutputLanguage" - default = "language::output::LANG_AUTO" - handler = "stringToOutputLanguage" - predicates = [] - includes = ["options/language.h"] - help = "force output language (default is \"auto\"; see --output-lang help)" - - -Further information (the old option package) -============================================ - - The options/ package supports a wide range of operations for responding to - an option being set. Roughly the three major concepts are: - - - handler to parse an option before setting its value. - - predicates to reject bad values for the option. - - More details on each class of custom handlers. - - - handler = "" - - Handlers provide support for parsing custom option types. - The signature for a handler call is: - - T custom-option-handler(std::string option, std::string optarg, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-handler as a dispatch into a function on handler with the - signature: - - T OptionsHandler::custom-option-handler(std::string option, - std::string optarg); - - The handlers are run before predicates. - Having multiple handlers is considered bad practice and is unsupported. - Handlers may have arbitrary side effects, but should call no code - inaccessible to liboptions. For side effects that are not required in order - to parse the option, using :predicate is recommended. Memory - management done by a handler needs to either be encapsulated by the type - and the destructor for the type or should *always* be owned by handler. - More elaborate memory management schemes are not currently supported. - - - predicates = [...] - - Predicates provide support for checking whether or not the value of an - option is acceptable. Predicates are run after handlers. - The signature for a predicate call is: - - void custom-predicate(std::string option, T value, - OptionsHandler* handler); - - where T is the type of the option. The suggested implementation is to - implement custom-predicate as a dispatch into a function on handler with - the signature: - - void OptionsHandler::custom-predicate(std::string option, T value); - - The predicates are run after handlers. Multiple - predicates may be defined for the same option, but the order they are run - is not guaranteed. Predicates may have arbitrary side effects, but should - call no code inaccessible to liboptions. diff --git a/src/options/README.md b/src/options/README.md new file mode 100644 index 000000000..df5686abc --- /dev/null +++ b/src/options/README.md @@ -0,0 +1,211 @@ +Specifying Modules +================== + +Every options module, that is a group of options that belong together in some +way, is declared in its own file in `options/{module name}_options.toml`. Each +options module starts with the following required attributes: + +* `id` (string): ID of the module (e.g., `"arith"`) +* `name` (string): name of the module (e.g., `"Arithmetic Theory"`) + +Additional, a module can optionally be defined to be public. A public module +includes `cvc5_public.h` instead of `cvc5_private.h` can thus be included from +"external" code like the parser or the main driver. + +* `public` (bool): make option module public + +A module defines 0 or more options. + +In general, each attribute/value pair is required to be in one line. Comments +start with # and are not allowed in attribute/value lines. + +After parsing, a module is extended to have the following attributes: + +* `id`: lower-case version of the parsed `id` +* `id_cap`: upper-case version of `id` (used for the `Holder{id_cap}` class) +* `filename`: base filename for generated files (`"{id}_options"`) +* `header`: generated header name (`"options/{filename}.h"`) + + +Specifying Options +================== + +Options can be defined within a module file with the `[[option]]` tag, the +required attributes for an option are: + +* `category` (string): one of `common`, `expert`, `regular`, or `undocumented` +* `type` (string): the C++ type of the option value + +Optional attributes are: + +* `name` (string): the option name used to access the option internally + (`d_option.{module.id}.{name}`) +* `long` (string): long option name (without `--` prefix). Long option names may + have a suffix `=XXX` where `XXX` can be used to indicate the type of the + option value, e.g., `=MODE`, `=LANG`, `=N`, ... +* `short` (string): short option name consisting of one character (no `-` prefix + required), can be given if `long` is specified +* `alias` (list): alternative names that can be used instead of `long` +* `default` (string): default value, needs to be a valid C++ expression of type + `type` +* `alternate` (bool, default `true`): if `true`, adds `--no-{long}` alternative + option +* `mode` (list): used to define options whose type shall be an auto-generated + enum, more details below +* `handler` (string): alternate parsing routine for option types not covered by + the default parsers, more details below +* `predicates` (list): custom validation function to check whether an option + value is valid, more details below +* `includes` (list): additional header files required by handler or predicate + functions +* `help` (string): documentation string (required, unless the `category` is + `undocumented`) +* `help_mode` (string): documentation for the mode enum (required if `mode` is + given) + + +Handler functions +----------------- + +Custom handler functions are used to turn the option value from a `std::string` +into the type specified by `type`. Standard handler functions are provided for +basic types (`std::string`, `bool`, integer types and floating point types) as +well as enums specified by `mode`. A custom handler function needs to be member +function of `options::OptionsHandler` with signature `{type} {handler}(const +std::string& option, const std::string& flag, const std::string& optionvalue)`, +or alternatively `void {handler}(const std::string& option, const std::string& +flag)` if the `type` is `void`. The two parameters `option` and `flag` hold the +canonical and the actually used option names, respectively, and they may differ +if an alternative name (from `alias`) was used. While `option` should be used to +identify an option (e.g. by comparing against `*__name`), `flag` should be +usually used in user messages. + + +Predicate functions +------------------- + +Predicate functions are used to check whether an option value is valid after it +has been parsed by a (standard or custom) handler function. Like a handler +function, a predicate function needs to be a member function of +`options::OptionsHandler` with signature `void {predicate}(const std::string& +option, const std::string& flag, {type} value)`. If the check fails, the +predicate should raise an `OptionException`. + + +Mode options +------------ + +An option can be defined to hold one of a given set of values we call modes. +Doing so automatically defines an `enum class` for the set of modes and makes +the option accept one of the values from the enum. The enum class will be called +`{type}` and methods `operator<<` and `stringTo{enum}` are automatically +generated. A mode is defined by specifying `[[option.mode.{NAME}]]` after the +main `[[option]]` section with the following attributes: + +* `name` (string): the string value that corresponds to the enum value +* `help` (string): documentation about this mode + +Example: + + [[option]] + name = "bitblastMode" + category = "regular" + long = "bitblast=MODE" + type = "BitblastMode" + default = "LAZY" + help = "choose bitblasting mode, see --bitblast=help" + help_mode = "Bit-blasting modes." + [[option.mode.LAZY]] + name = "lazy" + help = "Separate boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver." + [[option.mode.EAGER]] + name = "eager" + help = "Bitblast eagerly to bit-vector SAT solver." + +The option can now be set with `--bitblast=lazy`, `(set-option :bitblast +eager)`, or `options::set("bitblast", "eager")`. + + +Generated code +============== + +The entire options setup heavily relies on generating a lot of code from the +information retrieved from the `*_options.toml` files. After code generation, +files related to options live either in `src/options/` (if not changed) or in +`build/src/options/` (if automatically generated). After all code has been +generated, the entire options setup consists of the following components: + +* `options.h`: core `Options` class +* `options_api.h`: utility methods used by the API (`parse()`, `set()`, `get()`, + ...) +* `options_public.h`: utility methods used to access options from outside of + libcvc5 +* `{module}_options.h`: specifics for one single options module + + +`Options` class +--------------- + +The `Options` class is the central entry point for regular usage of options. It +holds a `std::unique_ptr` to an "option holder" for every option module, that +can be accessed using references `{module}` (either as `const&` or `&`). These +holders hold the actual option data for the specific module. + +The holder types are forward declared and can thus only be accessed if one also +includes the appropriate `{module}_options.h`, which contains the proper +declaration for the holder class. + + +Option modules +-------------- + +Every option module declares an "option holder" class, which is a simple struct +that has two members for every option (that is not declared as `type = void`): +the actual option value as `{option.type} {option.name}` and a Boolean flag +`bool {option.name}__setByUser` that indicates whether the option value was +explicitly set by the user. If any of the options of a module is a mode option, +the option module also defines an enum class that corresponds to the mode, +including `operator<<()` and `stringTo{mode type}`. + +For convenience, the option modules also provide methods `void +{module.id}::setDefault{option.name}(Options& opts, {option.type} value)`. Each +such method sets the option value to the given value, if the option was not yet +set by the user, i.e., the `__setByUser` flag is false. Additionally, every +option module exports the `long` option name as `static constexpr const char* +{module.id}::{option.name}__name`. + + +Full Example +============ + + [[option]] + category = "regular" + name = "decisionMode" + long = "decision=MODE" + alias = ["decision-mode"] + type = "DecisionMode" + default = "INTERNAL" + predicates = ["setDecisionModeStopOnly"] + help = "choose decision mode, see --decision=help" + help_mode = "Decision modes." + [[option.mode.INTERNAL]] + name = "internal" + help = "Use the internal decision heuristics of the SAT solver." + [[option.mode.JUSTIFICATION]] + name = "justification" + help = "An ATGP-inspired justification heuristic." + [[option.mode.RELEVANCY]] + name = "justification-stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." + +This defines a new option that is accessible via +`d_options.{module.id}.decisionMode` and stores an automatically generated mode +`DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and +`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +with `--decision-mode=justification`, and similarly from an SMT-LIB input with +`(set-option :decision internal)` and `(set-option :decision-mode +justification)`. The command-line help for this option looks as follows: + + --output-lang=LANG | --output-language=LANG + force output language (default is "auto"; see + --output-lang help) diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h deleted file mode 100644 index 86112a907..000000000 --- a/src/options/base_handlers.h +++ /dev/null @@ -1,87 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add one-line brief description here ]] - * - * [[ Add lengthier description here ]] - * \todo document this file - */ - -#include "cvc5_private.h" - -#ifndef CVC5__BASE_HANDLERS_H -#define CVC5__BASE_HANDLERS_H - -#include <iostream> -#include <string> -#include <sstream> - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template <template <class U> class Cmp> -class comparator { - long d_lbound; - double d_dbound; - bool d_hasLbound; - - public: - comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} - comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} - comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {} - template <class T> - void operator()(std::string option, const T& value) { - if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || - (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { - std::stringstream ss; - ss << option << ": " << value << " is not a legal setting"; - throw OptionException(ss.str()); - } - } -};/* class comparator */ - -struct greater : public comparator<std::greater> { - greater(int i) : comparator<std::greater>(i) {} - greater(long l) : comparator<std::greater>(l) {} - greater(double d) : comparator<std::greater>(d) {} -};/* struct greater */ - -struct greater_equal : public comparator<std::greater_equal> { - greater_equal(int i) : comparator<std::greater_equal>(i) {} - greater_equal(long l) : comparator<std::greater_equal>(l) {} - greater_equal(double d) : comparator<std::greater_equal>(d) {} -};/* struct greater_equal */ - -struct less : public comparator<std::less> { - less(int i) : comparator<std::less>(i) {} - less(long l) : comparator<std::less>(l) {} - less(double d) : comparator<std::less>(d) {} -};/* struct less */ - -struct less_equal : public comparator<std::less_equal> { - less_equal(int i) : comparator<std::less_equal>(i) {} - less_equal(long l) : comparator<std::less_equal>(l) {} - less_equal(double d) : comparator<std::less_equal>(d) {} -};/* struct less_equal */ - -struct not_equal : public comparator<std::not_equal_to> { - not_equal(int i) : comparator<std::not_equal_to>(i) {} - not_equal(long l) : comparator<std::not_equal_to>(l) {} - not_equal(double d) : comparator<std::not_equal_to>(d) {} -};/* struct not_equal_to */ - -} // namespace options -} // namespace cvc5 - -#endif /* CVC5__BASE_HANDLERS_H */ diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 7e1cf68e4..e2fbd4cf1 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -210,6 +210,30 @@ def get_holder_ref_decls(modules): return concat_format(' options::Holder{id_cap}& {id};', modules) +def get_handler(option): + """Render handler call for assignment functions""" + optname = option.long_name if option.long else "" + if option.handler: + if option.type == 'void': + return 'opts.handler().{}("{}", option)'.format(option.handler, optname) + else: + return 'opts.handler().{}("{}", option, optionarg)'.format(option.handler, optname) + elif option.mode: + return 'stringTo{}(optionarg)'.format(option.type) + elif option.type != 'bool': + return 'handleOption<{}>("{}", option, optionarg)'.format(option.type, optname) + return None + + +def get_predicates(option): + """Render predicate calls for assignment functions""" + if not option.predicates: + return [] + optname = option.long_name if option.long else "" + assert option.type != 'void' + return ['opts.handler().{}("{}", option, value);'.format(x, optname) + for x in option.predicates] + class Module(object): """Options module. @@ -713,31 +737,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ sphinxgen.add(module, option) # Generate handler call - handler = None - if option.handler: - if option.type == 'void': - handler = 'opts.handler().{}(option)'.format(option.handler) - else: - handler = \ - 'opts.handler().{}(option, optionarg)'.format(option.handler) - elif option.mode: - handler = 'stringTo{}(optionarg)'.format(option.type) - elif option.type != 'bool': - handler = \ - 'handleOption<{}>(option, optionarg)'.format(option.type) + handler = get_handler(option) # Generate predicate calls - predicates = [] - if option.predicates: - if option.type == 'bool': - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] - else: - assert option.type != 'void' - predicates = \ - ['opts.handler().{}(option, value);'.format(x) \ - for x in option.predicates] + predicates = get_predicates(option) # Generate options_handler and getopt_long cases = [] @@ -813,7 +816,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='key')) elif option.handler: - h = 'handler->{handler}("{smtname}"' + h = 'handler->{handler}("{smtname}", key' if argument_req: h += ', optionarg' h += ');' diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 1ac5ec56d..e109ab44c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -67,10 +67,11 @@ void throwLazyBBUnsupported(options::SatSolverMode m) OptionsHandler::OptionsHandler(Options* options) : d_options(options) { } -unsigned long OptionsHandler::limitHandler(std::string option, - std::string optarg) +uint64_t OptionsHandler::limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg) { - unsigned long ms; + uint64_t ms; std::istringstream convert(optarg); if (!(convert >> ms)) { @@ -80,14 +81,18 @@ unsigned long OptionsHandler::limitHandler(std::string option, return ms; } -void OptionsHandler::setResourceWeight(std::string option, std::string optarg) +void OptionsHandler::setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg) { d_options->base.resourceWeightHolder.emplace_back(optarg); } // theory/quantifiers/options_handlers.h -void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) +void OptionsHandler::checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode) { if (mode == InstWhenMode::PRE_FULL) { @@ -97,7 +102,9 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode) } // theory/bv/options_handlers.h -void OptionsHandler::abcEnabledBuild(std::string option, bool value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_USE_ABC if(value) { @@ -110,7 +117,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, bool value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::abcEnabledBuild(std::string option, std::string value) +void OptionsHandler::abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value) { #ifndef CVC5_USE_ABC if(!value.empty()) { @@ -123,7 +132,9 @@ void OptionsHandler::abcEnabledBuild(std::string option, std::string value) #endif /* CVC5_USE_ABC */ } -void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) +void OptionsHandler::checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m) { if (m == SatSolverMode::CRYPTOMINISAT && !Configuration::isBuiltWithCryptominisat()) @@ -166,7 +177,9 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m) } } -void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) +void OptionsHandler::checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m) { if (m == options::BitblastMode::LAZY) { @@ -185,7 +198,9 @@ void OptionsHandler::checkBitblastMode(std::string option, BitblastMode m) } } -void OptionsHandler::setBitblastAig(std::string option, bool arg) +void OptionsHandler::setBitblastAig(const std::string& option, + const std::string& flag, + bool arg) { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { @@ -211,8 +226,9 @@ szs\n\ + Print instantiations as SZS compliant proof.\n\ "; -InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, - std::string optarg) +InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "default") { return InstFormatMode::DEFAULT; @@ -228,24 +244,30 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(std::string option, } // decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(std::string option, DecisionMode m) +void OptionsHandler::setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m) { d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); } -void OptionsHandler::setProduceAssertions(std::string option, bool value) +void OptionsHandler::setProduceAssertions(const std::string& option, + const std::string& flag, + bool value) { d_options->smt.produceAssertions = value; d_options->smt.interactiveMode = value; } -void OptionsHandler::setStats(const std::string& option, bool value) +void OptionsHandler::setStats(const std::string& option, + const std::string& flag, + bool value) { #ifndef CVC5_STATISTICS_ON if (value) { std::stringstream ss; - ss << "option `" << option + ss << "option `" << flag << "' requires a statistics-enabled build of cvc5; this binary was not " "built with statistics support"; throw OptionException(ss.str()); @@ -282,18 +304,25 @@ void OptionsHandler::setStats(const std::string& option, bool value) } } -void OptionsHandler::threadN(std::string option) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); +void OptionsHandler::threadN(const std::string& option, const std::string& flag) +{ + throw OptionException(flag + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); } // expr/options_handlers.h -void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) { +void OptionsHandler::setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth) +{ if(depth < -1) { throw OptionException("--expr-depth requires a positive argument, or -1."); } } -void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) { +void OptionsHandler::setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag) +{ if(dag < 0) { throw OptionException("--dag-thresh requires a nonnegative argument."); } @@ -312,12 +341,16 @@ static void print_config_cond (const char * str, bool cond = false) { print_config(str, cond ? "yes" : "no"); } -void OptionsHandler::copyright(std::string option) { +void OptionsHandler::copyright(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::copyright() << std::endl; exit(0); } -void OptionsHandler::showConfiguration(std::string option) { +void OptionsHandler::showConfiguration(const std::string& option, + const std::string& flag) +{ std::cout << Configuration::about() << std::endl; print_config ("version", Configuration::getVersionString()); @@ -385,7 +418,8 @@ static void printTags(unsigned ntags, char const* const* tags) std::cout << std::endl; } -void OptionsHandler::showDebugTags(std::string option) +void OptionsHandler::showDebugTags(const std::string& option, + const std::string& flag) { if (!Configuration::isDebugBuild()) { @@ -399,7 +433,8 @@ void OptionsHandler::showDebugTags(std::string option) exit(0); } -void OptionsHandler::showTraceTags(std::string option) +void OptionsHandler::showTraceTags(const std::string& option, + const std::string& flag) { if (!Configuration::isTracingBuild()) { @@ -431,7 +466,9 @@ static std::string suggestTags(char const* const* validTags, return didYouMean.getMatchAsString(inputTag); } -void OptionsHandler::enableTraceTag(std::string option, std::string optarg) +void OptionsHandler::enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(!Configuration::isTracingBuild()) { @@ -453,7 +490,9 @@ void OptionsHandler::enableTraceTag(std::string option, std::string optarg) Trace.on(optarg); } -void OptionsHandler::enableDebugTag(std::string option, std::string optarg) +void OptionsHandler::enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg) { if (!Configuration::isDebugBuild()) { @@ -484,8 +523,9 @@ void OptionsHandler::enableDebugTag(std::string option, std::string optarg) Trace.on(optarg); } -OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, - std::string optarg) +OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -502,8 +542,9 @@ OutputLanguage OptionsHandler::stringToOutputLanguage(std::string option, Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(std::string option, - std::string optarg) +InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; @@ -520,7 +561,9 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option, } /* options/base_options_handlers.h */ -void OptionsHandler::setVerbosity(std::string option, int value) +void OptionsHandler::setVerbosity(const std::string& option, + const std::string& flag, + int value) { if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&cvc5::null_os); @@ -550,14 +593,18 @@ void OptionsHandler::setVerbosity(std::string option, int value) } } -void OptionsHandler::increaseVerbosity(std::string option) { +void OptionsHandler::increaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity += 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } -void OptionsHandler::decreaseVerbosity(std::string option) { +void OptionsHandler::decreaseVerbosity(const std::string& option, + const std::string& flag) +{ d_options->base.verbosity -= 1; - setVerbosity(option, options::verbosity()); + setVerbosity(option, flag, d_options->base.verbosity); } } // namespace options diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 4b9b1c0ae..9aee1df22 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -19,9 +19,9 @@ #define CVC5__OPTIONS__OPTIONS_HANDLER_H #include <ostream> +#include <sstream> #include <string> -#include "options/base_handlers.h" #include "options/bv_options.h" #include "options/decision_options.h" #include "options/language.h" @@ -44,72 +44,122 @@ class OptionsHandler { public: OptionsHandler(Options* options); - void unsignedGreater0(const std::string& option, unsigned value) { - options::greater(0)(option, value); + template <typename T> + void geqZero(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0) + { + std::stringstream ss; + ss << flag << ": " << value << " is not a legal setting, should be " + << value << " >= 0."; + throw OptionException(ss.str()); + } } - - void unsignedLessEqual2(const std::string& option, unsigned value) { - options::less_equal(2)(option, value); - } - - void doubleGreaterOrEqual0(const std::string& option, double value) { - options::greater_equal(0.0)(option, value); - } - - void doubleLessOrEqual1(const std::string& option, double value) { - options::less_equal(1.0)(option, value); + template <typename T> + void betweenZeroAndOne(const std::string& option, + const std::string& flag, + T value) const + { + if (value < 0 || value > 1) + { + std::stringstream ss; + ss << flag << ": " << value + << " is not a legal setting, should be 0 <= " << flag << " <= 1."; + throw OptionException(ss.str()); + } } // theory/quantifiers/options_handlers.h - void checkInstWhenMode(std::string option, InstWhenMode mode); + void checkInstWhenMode(const std::string& option, + const std::string& flag, + InstWhenMode mode); // theory/bv/options_handlers.h - void abcEnabledBuild(std::string option, bool value); - void abcEnabledBuild(std::string option, std::string value); - - template<class T> void checkSatSolverEnabled(std::string option, T m); - - void checkBvSatSolver(std::string option, SatSolverMode m); - void checkBitblastMode(std::string option, BitblastMode m); - - void setBitblastAig(std::string option, bool arg); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + bool value); + void abcEnabledBuild(const std::string& option, + const std::string& flag, + const std::string& value); + + template <class T> + void checkSatSolverEnabled(const std::string& option, + const std::string& flag, + T m); + + void checkBvSatSolver(const std::string& option, + const std::string& flag, + SatSolverMode m); + void checkBitblastMode(const std::string& option, + const std::string& flag, + BitblastMode m); + + void setBitblastAig(const std::string& option, + const std::string& flag, + bool arg); // printer/options_handlers.h - InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); + InstFormatMode stringToInstFormatMode(const std::string& option, + const std::string& flag, + const std::string& optarg); // decision/options_handlers.h - void setDecisionModeStopOnly(std::string option, DecisionMode m); + void setDecisionModeStopOnly(const std::string& option, + const std::string& flag, + DecisionMode m); /** * Throws a ModalException if this option is being set after final * initialization. */ - void setProduceAssertions(std::string option, bool value); + void setProduceAssertions(const std::string& option, + const std::string& flag, + bool value); - void setStats(const std::string& option, bool value); + void setStats(const std::string& option, const std::string& flag, bool value); - unsigned long limitHandler(std::string option, std::string optarg); - void setResourceWeight(std::string option, std::string optarg); + uint64_t limitHandler(const std::string& option, + const std::string& flag, + const std::string& optarg); + void setResourceWeight(const std::string& option, + const std::string& flag, + const std::string& optarg); /* expr/options_handlers.h */ - void setDefaultExprDepthPredicate(std::string option, int depth); - void setDefaultDagThreshPredicate(std::string option, int dag); + void setDefaultExprDepthPredicate(const std::string& option, + const std::string& flag, + int depth); + void setDefaultDagThreshPredicate(const std::string& option, + const std::string& flag, + int dag); /* main/options_handlers.h */ - void copyright(std::string option); - void showConfiguration(std::string option); - void showDebugTags(std::string option); - void showTraceTags(std::string option); - void threadN(std::string option); + void copyright(const std::string& option, const std::string& flag); + void showConfiguration(const std::string& option, const std::string& flag); + void showDebugTags(const std::string& option, const std::string& flag); + void showTraceTags(const std::string& option, const std::string& flag); + void threadN(const std::string& option, const std::string& flag); /* options/base_options_handlers.h */ - void setVerbosity(std::string option, int value); - void increaseVerbosity(std::string option); - void decreaseVerbosity(std::string option); - OutputLanguage stringToOutputLanguage(std::string option, std::string optarg); - InputLanguage stringToInputLanguage(std::string option, std::string optarg); - void enableTraceTag(std::string option, std::string optarg); - void enableDebugTag(std::string option, std::string optarg); + void setVerbosity(const std::string& option, + const std::string& flag, + int value); + void increaseVerbosity(const std::string& option, const std::string& flag); + void decreaseVerbosity(const std::string& option, const std::string& flag); + OutputLanguage stringToOutputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + InputLanguage stringToInputLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableTraceTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + void enableDebugTag(const std::string& option, + const std::string& flag, + const std::string& optarg); private: @@ -121,8 +171,10 @@ public: }; /* class OptionHandler */ -template<class T> -void OptionsHandler::checkSatSolverEnabled(std::string option, T m) +template <class T> +void OptionsHandler::checkSatSolverEnabled(const std::string& option, + const std::string& flag, + T m) { #if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \ && !defined(CVC5_USE_KISSAT) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index e909a5f0a..2c22065c2 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -58,7 +58,6 @@ extern int optreset; ${headers_module}$ #include "base/cvc5config.h" -#include "options/base_handlers.h" ${headers_handler}$ @@ -82,7 +81,9 @@ thread_local Options* Options::s_current = NULL; */ template <class T, bool is_numeric, bool is_integer> struct OptionHandler { - static T handle(std::string option, std::string optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg); };/* struct OptionHandler<> */ /** Variant for integral C++ types */ @@ -99,32 +100,35 @@ struct OptionHandler<T, true, true> { return str.find('-') != std::string::npos; } - static T handle(const std::string& option, const std::string& optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { try { T i; bool success = stringToInt(i, optionarg); if(!success){ - throw OptionException(option + ": failed to parse "+ optionarg + - " as an integer of the appropriate type."); + throw OptionException(flag + ": failed to parse " + optionarg + + " as an integer of the appropriate type."); } // Depending in the platform unsigned numbers with '-' signs may parse. // Reject these by looking for any minus if it is not signed. if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { // unsigned type but user gave negative argument - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(i < std::numeric_limits<T>::min()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << std::numeric_limits<T>::min(); + ss << flag + << " requires an argument >= " << std::numeric_limits<T>::min(); throw OptionException(ss.str()); } else if(i > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -137,7 +141,7 @@ struct OptionHandler<T, true, true> { // } } catch(std::invalid_argument&) { // user gave something other than an integer - throw OptionException(option + " requires an integer argument"); + throw OptionException(flag + " requires an integer argument"); } } };/* struct OptionHandler<T, true, true> */ @@ -145,29 +149,33 @@ struct OptionHandler<T, true, true> { /** Variant for numeric but non-integral C++ types */ template <class T> struct OptionHandler<T, true, false> { - static T handle(std::string option, std::string optionarg) { - std::stringstream in(optionarg); + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { + std::stringstream inss(optionarg); long double r; - in >> r; - if(! in.eof()) { + inss >> r; + if (!inss.eof()) + { // we didn't consume the whole string (junk at end) - throw OptionException(option + " requires a numeric argument"); + throw OptionException(flag + " requires a numeric argument"); } if(! std::numeric_limits<T>::is_signed && r < 0.0) { // unsigned type but user gave negative value - throw OptionException(option + " requires a nonnegative argument"); + throw OptionException(flag + " requires a nonnegative argument"); } else if(r < -std::numeric_limits<T>::max()) { // negative overflow for type std::stringstream ss; - ss << option << " requires an argument >= " - << -std::numeric_limits<T>::max(); + ss << flag + << " requires an argument >= " << -std::numeric_limits<T>::max(); throw OptionException(ss.str()); } else if(r > std::numeric_limits<T>::max()) { // positive overflow for type std::stringstream ss; - ss << option << " requires an argument <= " - << std::numeric_limits<T>::max(); + ss << flag + << " requires an argument <= " << std::numeric_limits<T>::max(); throw OptionException(ss.str()); } @@ -178,7 +186,10 @@ struct OptionHandler<T, true, false> { /** Variant for non-numeric C++ types */ template <class T> struct OptionHandler<T, false, false> { - static T handle(std::string option, std::string optionarg) { + static T handle(const std::string& option, + const std::string& flag, + const std::string& optionarg) + { T::unsupported_handleOption_call___please_write_me; // The above line causes a compiler error if this version of the template // is ever instantiated (meaning that a specialization is missing). So @@ -191,36 +202,26 @@ struct OptionHandler<T, false, false> { /** Handle an option of type T in the default way. */ template <class T> -T handleOption(std::string option, std::string optionarg) { - return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg); +T handleOption(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ + return OptionHandler<T, + std::numeric_limits<T>::is_specialized, + std::numeric_limits<T>::is_integer>::handle(option, + flag, + optionarg); } /** Handle an option of type std::string in the default way. */ template <> -std::string handleOption<std::string>(std::string option, std::string optionarg) { +std::string handleOption<std::string>(const std::string& option, + const std::string& flag, + const std::string& optionarg) +{ return optionarg; } -/** - * Run handler, and any user-given predicates, for option T. - * If a user specifies a :handler or :predicates, it overrides this. - */ -template <class T> -typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) { - // By default, parse the option argument in a way appropriate for its type. - // E.g., for "unsigned int" options, ensure that the provided argument is - // a nonnegative integer that fits in the unsigned int type. - - return handleOption<typename T::type>(option, optionarg); -} - -template <class T> -void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) { - // By default, nothing to do for bool. Users add things with - // :predicate in options files to provide custom checking routines - // that can throw exceptions. -} - Options::Options(OptionsListener* ol) : d_handler(new options::OptionsHandler(this)), // clang-format off diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 26d7a451b..eda5ea963 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -8,7 +8,7 @@ name = "SAT Layer" long = "random-freq=P" type = "double" default = "0.0" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "sets the frequency of random decisions in the sat solver (P=0.0 by default)" [[option]] @@ -24,7 +24,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.95" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "variable activity decay factor for Minisat" [[option]] @@ -32,7 +32,7 @@ name = "SAT Layer" category = "regular" type = "double" default = "0.999" - predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"] + predicates = ["betweenZeroAndOne"] help = "clause activity decay factor for Minisat" [[option]] @@ -49,7 +49,7 @@ name = "SAT Layer" long = "restart-int-inc=F" type = "double" default = "3.0" - predicates = ["doubleGreaterOrEqual0"] + predicates = ["geqZero"] help = "sets the restart interval increase factor for the sat solver (F=3.0 by default)" [[option]] diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index e85ea82ef..a46452004 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), d_objectives(parent->getUserContext()), - d_results(), - d_objectiveCombination(LEXICOGRAPHIC) + d_results() { } -OptimizationResult::ResultType OptimizationSolver::checkOpt() +Result OptimizationSolver::checkOpt(ObjectiveCombination combination) { // if the results of the previous call have different size than the // objectives, then we should clear the pareto optimization context @@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() { d_results.emplace_back(); } - switch (d_objectiveCombination) + switch (combination) { case BOX: return optimizeBox(); break; case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break; @@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target, std::vector<OptimizationResult> OptimizationSolver::getValues() { - Assert(d_objectives.size() == d_results.size()); return d_results; } -void OptimizationSolver::setObjectiveCombination( - ObjectiveCombination combination) -{ - d_objectiveCombination = combination; -} - std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -106,13 +98,12 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( return optChecker; } -OptimizationResult::ResultType OptimizationSolver::optimizeBox() +Result OptimizationSolver::optimizeBox() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); OptimizationResult partialResult; - OptimizationResult::ResultType aggregatedResultType = - OptimizationResult::OPTIMAL; + Result aggregatedResult(Result::Sat::SAT); std::unique_ptr<OMTOptimizer> optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // match the optimization result type, and aggregate the results of // subproblems - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: break; - case OptimizationResult::UNBOUNDED: break; - case OptimizationResult::UNSAT: - if (aggregatedResultType == OptimizationResult::OPTIMAL) + case Result::SAT: break; + case Result::UNSAT: + // the assertions are unsatisfiable + for (size_t j = 0; j < numObj; ++j) { - aggregatedResultType = OptimizationResult::UNSAT; + d_results[j] = partialResult; } - break; - case OptimizationResult::UNKNOWN: - aggregatedResultType = OptimizationResult::UNKNOWN; + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + aggregatedResult = partialResult.getResult(); break; default: Unreachable(); } @@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox() } // kill optChecker after optimization ends d_optChecker.reset(); - return aggregatedResultType; + return aggregatedResult; } -OptimizationResult::ResultType -OptimizationSolver::optimizeLexicographicIterative() +Result OptimizationSolver::optimizeLexicographicIterative() { // resets the optChecker d_optChecker = createOptCheckerWithTimeout(d_parent); - OptimizationResult partialResult; + // partialResult defaults to SAT if no objective is present + // NOTE: the parenthesis around Result(Result::SAT) is required, + // otherwise the compiler will report "parameter declarator cannot be + // qualified". For more details: + // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it + // https://en.wikipedia.org/wiki/Most_vexing_parse + OptimizationResult partialResult((Result(Result::SAT)), TNode()); std::unique_ptr<OMTOptimizer> optimizer; for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { @@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative() d_results[i] = partialResult; // checks the optimization result of the current objective - switch (partialResult.getType()) + switch (partialResult.getResult().isSat()) { - case OptimizationResult::OPTIMAL: + case Result::SAT: // assert target[i] == value[i] and proceed d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode( kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue())); break; - case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED; - case OptimizationResult::UNSAT: return OptimizationResult::UNSAT; - case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::UNSAT: + d_optChecker.reset(); + return partialResult.getResult(); + case Result::SAT_UNKNOWN: + d_optChecker.reset(); + return partialResult.getResult(); default: Unreachable(); } + + // if the result for the current objective is unbounded + // then just stop + if (partialResult.isUnbounded()) break; } // kill optChecker in case pareto misuses it d_optChecker.reset(); - // now all objectives are OPTIMAL, just return OPTIMAL as overall result - return OptimizationResult::OPTIMAL; + // now all objectives are optimal, just return SAT as the overall result + return partialResult.getResult(); } -OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() +Result OptimizationSolver::optimizeParetoNaiveGIA() { // initial call to Pareto optimizer, create the checker if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent); @@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() switch (satResult.isSat()) { - case Result::Sat::UNSAT: return OptimizationResult::UNSAT; - case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN; + case Result::Sat::UNSAT: return satResult; + case Result::Sat::SAT_UNKNOWN: return satResult; case Result::Sat::SAT: { // if satisfied, use d_results to store the initial results @@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } default: Unreachable(); } + Result lastSatResult = satResult; + // a vector storing assertions saying that no objective is worse std::vector<Node> noWorseObj; // a vector storing assertions saying that there is at least one objective @@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() case Result::Sat::SAT_UNKNOWN: // if result is UNKNOWN, abort the current session and return UNKNOWN d_optChecker.reset(); - return OptimizationResult::UNKNOWN; + return satResult; case Result::Sat::SAT: { + lastSatResult = satResult; // if result is SAT, update d_results to the more optimal values for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { d_results[i] = OptimizationResult( - OptimizationResult::OPTIMAL, - d_optChecker->getValue(d_objectives[i].getTarget())); + satResult, d_optChecker->getValue(d_objectives[i].getTarget())); } break; } @@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA() // for the next run. d_optChecker->assertFormula(nm->mkOr(someObjBetter)); - return OptimizationResult::OPTIMAL; + return lastSatResult; } } // namespace smt diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 6d138deb2..d13168780 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -33,63 +33,75 @@ namespace smt { /** * The optimization result of an optimization objective * containing: - * - whether it's optimal or not - * - if so, the optimal value, otherwise the value might be empty node or - * something suboptimal + * - the optimization result: SAT/UNSAT/UNKNOWN + * - the optimal value if SAT and bounded + * (optimal value reached and it's not infinity), + * or an empty node if SAT and unbounded + * (optimal value is +inf for maximum or -inf for minimum), + * otherwise the value might be empty node + * or something suboptimal + * - whether the objective is unbounded */ class OptimizationResult { public: /** - * Enum indicating whether the checkOpt result - * is optimal or not. - **/ - enum ResultType - { - // whether the value is optimal is UNKNOWN - UNKNOWN, - // the original set of assertions has result UNSAT - UNSAT, - // the value is optimal - OPTIMAL, - // the goal is unbounded, - // if objective is maximize, it's +infinity - // if objective is minimize, it's -infinity - UNBOUNDED, - }; - - /** * Constructor * @param type the optimization outcome * @param value the optimized value + * @param unbounded whether the objective is unbounded **/ - OptimizationResult(ResultType type, TNode value) - : d_type(type), d_value(value) + OptimizationResult(Result result, TNode value, bool unbounded = false) + : d_result(result), d_value(value), d_unbounded(unbounded) + { + } + OptimizationResult() + : d_result(Result::Sat::SAT_UNKNOWN, + Result::UnknownExplanation::NO_STATUS), + d_value(), + d_unbounded(false) { } - OptimizationResult() : d_type(UNKNOWN), d_value() {} ~OptimizationResult() = default; /** * Returns an enum indicating whether - * the result is optimal or not. - * @return an enum showing whether the result is optimal, unbounded, - * unsat or unknown. + * the result is SAT or not. + * @return whether the result is SAT, UNSAT or SAT_UNKNOWN **/ - ResultType getType() const { return d_type; } + Result getResult() const { return d_result; } + /** * Returns the optimal value. * @return Node containing the optimal value, - * if getType() is not OPTIMAL, it might return an empty node or a node - * containing non-optimal value + * if result is unbounded, this will be an empty node, + * if getResult() is UNSAT, it will return an empty node, + * if getResult() is SAT_UNKNOWN, it will return something suboptimal + * or an empty node, depending on how the solver runs. **/ Node getValue() const { return d_value; } + /** + * Checks whether the objective is unbouned + * @return whether the objective is unbounded + * if the objective is unbounded (this function returns true), + * then the optimal value is: + * +inf, if it's maximize; + * -inf, if it's minimize + **/ + bool isUnbounded() const { return d_unbounded; } + private: - /** the indicating whether the result is optimal or something else **/ - ResultType d_type; - /** if the result is optimal, this is storing the optimal value **/ + /** indicating whether the result is SAT, UNSAT or UNKNOWN **/ + Result d_result; + /** if the result is bounded, this is storing the value **/ Node d_value; + /** whether the objective is unbounded + * If this is true, then: + * if objective is maximize, it's +infinity; + * if objective is minimize, it's -infinity + **/ + bool d_unbounded; }; /** @@ -199,10 +211,10 @@ class OptimizationSolver /** * Run the optimization loop for the added objective * For multiple objective combination, it defaults to lexicographic, - * and combination could be set by calling - * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO) + * possible combinations: BOX, LEXICOGRAPHIC, PARETO + * @param combination BOX / LEXICOGRAPHIC / PARETO */ - OptimizationResult::ResultType checkOpt(); + Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC); /** * Add an optimization objective. @@ -223,11 +235,6 @@ class OptimizationSolver **/ std::vector<OptimizationResult> getValues(); - /** - * Sets the objective combination - **/ - void setObjectiveCombination(ObjectiveCombination combination); - private: /** * Initialize an SMT subsolver for offline optimization purpose @@ -244,26 +251,26 @@ class OptimizationSolver /** * Optimize multiple goals in Box order - * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED; - * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN; - * UNKNOWN if any of the objective is UNKNOWN. + * @return SAT if all of the objectives are optimal or unbounded; + * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN; + * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeBox(); + Result optimizeBox(); /** * Optimize multiple goals in Lexicographic order, * using iterative implementation - * @return OPTIMAL if all objectives are OPTIMAL and bounded; - * UNBOUNDED if one of the objectives is UNBOUNDED + * @return SAT if the objectives are optimal, + * if one of the objectives is unbounded, + * the optimization will stop at that objective; + * UNSAT if any of the objectives is UNSAT * and optimization will stop at that objective; - * UNSAT if one of the objectives is UNSAT - * and optimization will stop at that objective; - * UNKNOWN if one of the objectives is UNKNOWN + * SAT_UNKNOWN if any of the objectives is UNKNOWN * and optimization will stop at that objective; * If the optimization is stopped at an objective, - * all objectives following that objective will be UNKNOWN. + * all objectives following that objective will be SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeLexicographicIterative(); + Result optimizeLexicographicIterative(); /** * Optimize multiple goals in Pareto order @@ -277,11 +284,12 @@ class OptimizationSolver * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm. * Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009. * - * @return if it finds a new Pareto optimal result it will return OPTIMAL; + * @return if it finds a new Pareto optimal result it will return SAT; * if it exhausts the results in the Pareto front it will return UNSAT; - * if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN. + * if the underlying SMT solver returns SAT_UNKNOWN, + * it will return SAT_UNKNOWN. **/ - OptimizationResult::ResultType optimizeParetoNaiveGIA(); + Result optimizeParetoNaiveGIA(); /** A pointer to the parent SMT engine **/ SmtEngine* d_parent; @@ -294,9 +302,6 @@ class OptimizationSolver /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; - - /** The current objective combination method **/ - ObjectiveCombination d_objectiveCombination; }; } // namespace smt diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 396befb35..0c93db90f 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -26,6 +26,7 @@ operator INTS_MODULUS_TOTAL 2 "integer modulus with interpreted division by 0 (i operator ABS 1 "absolute value" parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" +operator POW2 1 "arithmetic power of 2" operator EXPONENTIAL 1 "exponential" operator SINE 1 "sine" @@ -148,6 +149,7 @@ typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>" typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCSECANT "SimpleTypeRule<RReal, AReal>" typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>" +typerule POW2 "SimpleTypeRule<RInteger, AInteger>" typerule SQRT "SimpleTypeRule<RReal, AReal>" diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp new file mode 100644 index 000000000..534895c7f --- /dev/null +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Makai Mann, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of pow2 solver. + */ + +#include "theory/arith/nl/pow2_solver.h" + +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace arith { +namespace nl { + +Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model) + : d_im(im), d_model(model), d_initRefine(state.getUserContext()) +{ + NodeManager* nm = NodeManager::currentNM(); + d_false = nm->mkConst(false); + d_true = nm->mkConst(true); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_two = nm->mkConst(Rational(2)); +} + +Pow2Solver::~Pow2Solver() {} + +void Pow2Solver::initLastCall(const std::vector<Node>& assertions, + const std::vector<Node>& false_asserts, + const std::vector<Node>& xts) +{ + d_pow2s.clear(); + Trace("pow2-mv") << "POW2 terms : " << std::endl; + for (const Node& a : xts) + { + Kind ak = a.getKind(); + if (ak != POW2) + { + // don't care about other terms + continue; + } + d_pow2s.push_back(a); + } + Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; +} + +void Pow2Solver::checkInitialRefine() {} + +void Pow2Solver::checkFullRefine() {} + +Node Pow2Solver::valueBasedLemma(Node i) { return Node(); } + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fe4ed4c22..778c842a6 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -75,6 +75,10 @@ const char* toString(InferenceId i) return "ARITH_NL_IAND_SUM_REFINE"; case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "ARITH_NL_IAND_BITWISE_REFINE"; + case InferenceId::ARITH_NL_POW2_INIT_REFINE: + return "ARITH_NL_POW2_INIT_REFINE"; + case InferenceId::ARITH_NL_POW2_VALUE_REFINE: + return "ARITH_NL_POW2_VALUE_REFINE"; case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 169992f41..6a87776d6 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -126,6 +126,11 @@ enum class InferenceId ARITH_NL_IAND_SUM_REFINE, // bitwise refinements (IAndSolver::checkFullRefine) ARITH_NL_IAND_BITWISE_REFINE, + //-------------------- nonlinear pow2 solver + // initial refinements (Pow2Solver::checkInitialRefine) + ARITH_NL_POW2_INIT_REFINE, + // value refinements (Pow2Solver::checkFullRefine) + ARITH_NL_POW2_VALUE_REFINE, //-------------------- nonlinear cad solver // conflict / infeasible subset obtained from cad ARITH_NL_CAD_CONFLICT, diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index c23ce79dd..5cd29878e 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, (uint32_t)0x3FFFFFA1)); @@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>(); std::cout << "opt value is: " << val << std::endl; @@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), @@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index cf0434ddc..583f908e7 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), @@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min) // We activate our objective so the subsolver knows to optimize it d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // We expect max_cost == 99 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), @@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); // This should return OPT_UNSAT since 0 > x > 100 is impossible. - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); // We expect our check to have returned UNSAT - ASSERT_EQ(r, OptimizationResult::UNSAT); + ASSERT_EQ(r.isSat(), Result::UNSAT); d_smtEngine->resetAssertions(); } @@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE); - OptimizationResult::ResultType r = d_optslv->checkOpt(); + Result r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 73c6d9e7e..9a091fb3b 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Box optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::BOX); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Box optimization + Result r = optSolver.checkOpt(OptimizationSolver::BOX); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. @@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) (maximize b) */ OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::PARETO); optSolver.addObjective(a, OptimizationObjective::MAXIMIZE); optSolver.addObjective(b, OptimizationObjective::MAXIMIZE); - OptimizationResult::ResultType r; + Result r; // all possible result pairs <a, b> std::set<std::pair<uint32_t, uint32_t>> possibleResults = { {1, 3}, {2, 2}, {3, 1}}; - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); std::pair<uint32_t, uint32_t> res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); res = { results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(), @@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.count(res), 1); possibleResults.erase(res); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::UNSAT); + r = optSolver.checkOpt(OptimizationSolver::PARETO); + ASSERT_EQ(r.isSat(), Result::UNSAT); ASSERT_EQ(possibleResults.size(), 0); } @@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // y <= x d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - // Lexico optimization OptimizationSolver optSolver(d_smtEngine.get()); - optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); - // minimize x optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); @@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) // maximize z optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); - OptimizationResult::ResultType r = optSolver.checkOpt(); + // Lexico optimization + Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + ASSERT_EQ(r.isSat(), Result::SAT); std::vector<OptimizationResult> results = optSolver.getValues(); @@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop) d_smtEngine->pop(); // now we only have one objective: (minimize x) - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 1); ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u)); // resetting the assertions also resets the optimization objectives d_smtEngine->resetAssertions(); - r = optSolver.checkOpt(); - ASSERT_EQ(r, OptimizationResult::OPTIMAL); + r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC); + ASSERT_EQ(r.isSat(), Result::SAT); results = optSolver.getValues(); ASSERT_EQ(results.size(), 0); } |