From 4ca14e808d788ef9570dda1188645783c6a11e70 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 15 Jun 2021 15:44:52 -0700 Subject: pow2: adding a kind, inference rules, and some implementations in the pow2 solver (#6736) This PR is the sequel of #6676 . It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations. --- src/CMakeLists.txt | 1 + src/api/cpp/cvc5_kind.h | 16 ++++++++ src/theory/arith/kinds | 2 + src/theory/arith/nl/pow2_solver.cpp | 73 +++++++++++++++++++++++++++++++++++++ src/theory/inference_id.cpp | 4 ++ src/theory/inference_id.h | 5 +++ 6 files changed, 101 insertions(+) create mode 100644 src/theory/arith/nl/pow2_solver.cpp 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& 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& children) const` + */ + POW2, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, 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" typerule ARCCOSECANT "SimpleTypeRule" typerule ARCSECANT "SimpleTypeRule" typerule ARCCOTANGENT "SimpleTypeRule" +typerule POW2 "SimpleTypeRule" typerule SQRT "SimpleTypeRule" 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& assertions, + const std::vector& false_asserts, + const std::vector& 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, -- cgit v1.2.3 From c299e8661f24d3a6acb736e9e5df1b1920488ac3 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Tue, 15 Jun 2021 16:20:20 -0700 Subject: [Optimization] Use Result in OptimizationResult (#6740) OptimizationResult now contains: - cvc5::Result - optimal value for objective - whether the objective is unbounded This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API. Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)... --- src/omt/bitvector_optimizer.cpp | 128 +++++++++++------------- src/omt/integer_optimizer.cpp | 13 ++- src/smt/optimization_solver.cpp | 91 +++++++++-------- src/smt/optimization_solver.h | 121 +++++++++++----------- test/unit/theory/theory_bv_opt_white.cpp | 20 ++-- test/unit/theory/theory_int_opt_white.cpp | 16 +-- test/unit/theory/theory_opt_multigoal_white.cpp | 49 ++++----- 7 files changed, 214 insertions(+), 224 deletions(-) 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(); - } - 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(); + 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(); - } - 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(); + 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/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 OptimizationSolver::getValues() { - Assert(d_objectives.size() == d_results.size()); return d_results; } -void OptimizationSolver::setObjectiveCombination( - ObjectiveCombination combination) -{ - d_objectiveCombination = combination; -} - std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -106,13 +98,12 @@ std::unique_ptr 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 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 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 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 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 d_results; - - /** The current objective combination method **/ - ObjectiveCombination d_objectiveCombination; }; } // namespace smt 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(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(); 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(); 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(), @@ -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(), 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(), @@ -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(), @@ -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(), 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 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 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 std::set> 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 results = optSolver.getValues(); std::pair res = { results[0].getValue().getConst().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().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().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 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(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); } -- cgit v1.2.3 From 6ae5647e754925a5c963d2b92c7255d7e0de6b03 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 16 Jun 2021 10:46:01 +0200 Subject: Properly consider aliases in option handlers (#6683) 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. --- src/options/CMakeLists.txt | 1 - src/options/README | 127 ----------------------- src/options/README.md | 211 +++++++++++++++++++++++++++++++++++++++ src/options/base_handlers.h | 87 ---------------- src/options/mkoptions.py | 51 +++++----- src/options/options_handler.cpp | 117 +++++++++++++++------- src/options/options_handler.h | 144 +++++++++++++++++--------- src/options/options_template.cpp | 91 ++++++++--------- src/options/prop_options.toml | 8 +- 9 files changed, 468 insertions(+), 369 deletions(-) delete mode 100644 src/options/README create mode 100644 src/options/README.md delete mode 100644 src/options/base_handlers.h 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::() - 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- alternative option - false: omit --no- 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- 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 -#include -#include - -#include "options/option_exception.h" - -namespace cvc5 { -namespace options { - -template