diff --git a/clasp/cli/clasp_cli_options.inl b/clasp/cli/clasp_cli_options.inl index 42328fe..1489b4b 100644 --- a/clasp/cli/clasp_cli_options.inl +++ b/clasp/cli/clasp_cli_options.inl @@ -1,5 +1,5 @@ // -// Copyright (c) 2013-2017 Benjamin Kaufmann +// Copyright (c) 2013-present Benjamin Kaufmann // // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ // @@ -352,7 +352,9 @@ OPTION(restarts, "!,r", ARG(arg("")), "Configure restart policy\n" \ " D,,: Restart based on moving LBD average over last conflicts\n" \ " Mavg(,LBD)* > avg(LBD)\n" \ " use conflict level average if > 0 and avg(LBD) > \n"\ - " no|0 : Disable restarts", FUN(arg) { return ITE(arg.off(), (SELF.disable(),true), arg>>SELF.sched);}, GET(SELF.sched)) + " no|0 : Disable restarts", FUN(arg) { RestartParams::Dynamic dyn = {0}; char s; \ + return ITE(arg.off(), (SELF.disable(),true), ITE(arg.peek() == 'd' || arg.peek() == 'D', (arg>>s>>dyn && dyn.base && (SELF.setDynamic(dyn),true)), arg>>SELF.rsSched));},\ + GET_FUN(str) { ITE(SELF.disabled(), str<"), DEFINE_ENUM_MAPPING(RestartParams::SeqUpdate, \ MAP("no",RestartParams::seq_continue), MAP("repeat", RestartParams::seq_repeat), MAP("disable", RestartParams::seq_disable))),\ "Update restart seq. on model {no|repeat|disable}",\ @@ -365,16 +367,19 @@ OPTION(counter_restarts, "" , ARG(arg("")), "Use counter implication rest FUN(arg) { uint32 n = 0; uint32 m = SELF.counterBump; \ return (arg.off() || (arg >> n >> opt(m) && n > 0)) && SET_OR_FILL(SELF.counterRestart, n) && SET_OR_FILL(SELF.counterBump, m); },\ GET_IF(SELF.counterRestart, SELF.counterRestart, SELF.counterBump)) -OPTION(block_restarts , "" , ARG(arg("")), "Use glucose-style blocking restarts\n" \ - " %A: [,][,]\n" \ - " : Window size for moving average (0=disable blocking)\n" \ - " : Block restart if assignment > average * [1.4]\n" \ - " : Disable blocking for the first conflicts [10000]\n", FUN(arg) { \ - uint32 n = 0; double R = 0.0; uint32 x = 0;\ - return (arg.off() || (arg>>n>>opt(R = 1.4)>>opt(x = 10000) && n && R >= 1.0 && R <= 5.0))\ - && SET(SELF.blockWindow, n) && SET(SELF.blockScale, (float)R) && SET_OR_FILL(SELF.blockFirst, x);},\ - GET_IF(SELF.blockWindow, SELF.blockWindow, SELF.blockScale, SELF.blockFirst)) -OPTION(dyn_queue_keep , ",@3", ARG(arg("0..3")->implicit("0")), "Keep dynamic lbd/cfl queue", STORE_LEQ(SELF.dynStrat, 3u), GET(SELF.dynStrat)) +OPTION(block_restarts , "" , ARG_EXT(arg(""), DEFINE_ENUM_MAPPING(MovingAvg::Type, \ + MAP("d", MovingAvg::avg_sma), MAP("e", MovingAvg::avg_ema), MAP("l", MovingAvg::avg_ema_log), \ + MAP("es", MovingAvg::avg_ema_smooth), MAP("ls", MovingAvg::avg_ema_log_smooth))),\ + "Use glucose-style blocking restarts\n" \ + " %A: [,][,][,]\n" \ + " : Window size for moving average (0=disable blocking)\n" \ + " : Block restart if assignment > average * [1.4]\n" \ + " : Disable blocking for the first conflicts [10000]\n" \ + " : Type of moving average [e]\n", \ + FUN(arg) { uint32 n = 0; float R = 1.4; uint32 c = 10000; MovingAvg::Type a = MovingAvg::avg_ema; \ + return ITE(arg.off(), (SELF.block=RestartParams::Block(), true), arg>>n>>opt(R)>>opt(c)>>opt(a) && SET_GEQ(SELF.block.window, n, 1) \ + && R >= 1.0 && R <= 5.0 && SET(SELF.block.fscale, static_cast(R*100.0f)) && SET(SELF.block.first, c) && SET(SELF.block.avg, a)); },\ + GET_FUN(str) { ITE(!SELF.block.window, str<(SELF.block.avg)); }) OPTION(shuffle , "!" , ARG(arg(",")), "Shuffle problem after +(*i) restarts\n", FUN(arg) { uint32 n1 = 0; uint32 n2 = 0;\ return (arg.off() || (arg>>n1>>opt(n2) && n1)) && SET_OR_FILL(SELF.shuffle, n1) && SET_OR_FILL(SELF.shuffleNext, n2);},\ GET_IF(SELF.shuffle, SELF.shuffle, SELF.shuffleNext)) @@ -410,11 +415,11 @@ OPTION(del_grow , "!", NO_ARG, "Configure size-based deletion policy\n" \ " : Set grow schedule () [grow on restart]", FUN(arg){ double f; double g; ScheduleStrategy sc = ScheduleStrategy::def();\ return ITE(arg.off(), (SELF.growSched = ScheduleStrategy::none(), SELF.fGrow = 0.0f, true),\ arg>>f>>opt(g = 3.0)>>opt(sc) && SET_R(SELF.fGrow, (float)f, 1.0f, FLT_MAX) && SET_R(SELF.fMax, (float)g, 0.0f, FLT_MAX)\ - && (sc.defaulted() || !sc.user()) && (SELF.growSched=sc, true));},\ + && (SELF.growSched=sc, true));},\ GET_FUN(str) { if (SELF.fGrow == 0.0f) str<")), "Configure conflict-based deletion policy\n" \ " %A: ,... (see restarts)", FUN(arg){\ - return ITE(arg.off(), (SELF.cflSched=ScheduleStrategy::none()).disabled(), arg>>SELF.cflSched && !SELF.cflSched.user());}, GET(SELF.cflSched)) + return ITE(arg.off(), (SELF.cflSched=ScheduleStrategy::none()).disabled(), arg>>SELF.cflSched);}, GET(SELF.cflSched)) OPTION(del_init , "" , ARG(defaultsTo("3.0")->state(Value::value_defaulted)), "Configure initial deletion limit\n"\ " %A: [,,] ( > 0)\n" \ " : Set initial limit to P=estimated problem size/ [%D]\n" \ @@ -493,7 +498,7 @@ OPTION(global_restarts, ",@1", ARG(arg("")), "Configure global restart policy " : Maximal number of global restarts (0=disable)\n" \ " : Restart schedule [x,100,1.5] ()\n", FUN(arg) {\ return ITE(arg.off(), (SELF.restarts = SolveOptions::GRestarts(), true), arg>>SELF.restarts.maxR>>opt(SELF.restarts.sched = ScheduleStrategy())\ - && SELF.restarts.maxR && !SELF.restarts.sched.user());},\ + && SELF.restarts.maxR);},\ GET_IF(SELF.restarts.maxR, SELF.restarts.maxR, SELF.restarts.sched)) OPTION(distribute, "!,@1", ARG_EXT(defaultsTo("conflict,global,4"), \ DEFINE_ENUM_MAPPING(Distributor::Policy::Types, MAP("all", Distributor::Policy::all), MAP("short", Distributor::Policy::implicit), MAP("conflict", Distributor::Policy::conflict), MAP("loop" , Distributor::Policy::loop))\ diff --git a/clasp/solver_strategies.h b/clasp/solver_strategies.h index fdb0ec3..d6a980a 100644 --- a/clasp/solver_strategies.h +++ b/clasp/solver_strategies.h @@ -1,5 +1,5 @@ // -// Copyright (c) 2006-2017 Benjamin Kaufmann +// Copyright (c) 2006-present Benjamin Kaufmann // // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ // @@ -68,7 +68,7 @@ namespace Clasp { struct ScheduleStrategy { public: //! Supported strategies. - enum Type { Geometric = 0, Arithmetic = 1, Luby = 2, User = 3 }; + enum Type { Geometric = 0, Arithmetic = 1, Luby = 2 }; ScheduleStrategy(Type t = Geometric, uint32 b = 100, double g = 1.5, uint32 o = 0); //! Creates luby's sequence with unit-length unit and optional outer limit. @@ -80,12 +80,11 @@ struct ScheduleStrategy { //! Creates fixed sequence with length base. static ScheduleStrategy fixed(uint32 base) { return ScheduleStrategy(Arithmetic, base, 0, 0); } static ScheduleStrategy none() { return ScheduleStrategy(Geometric, 0); } - static ScheduleStrategy def() { return ScheduleStrategy(User, 0, 0.0); } + static ScheduleStrategy def() { return ScheduleStrategy(Arithmetic, 0); } uint64 current() const; bool disabled() const { return base == 0; } - bool defaulted()const { return base == 0 && type == User; } - bool user() const { return base != 0 && type == User; } - void reset() { idx = 0; } + bool defaulted()const { return base == 0 && type == Arithmetic; } + void reset() { idx = 0; } uint64 next(); void advanceTo(uint32 idx); uint32 base : 30; // base of sequence (n1) @@ -281,26 +280,45 @@ typedef Range Range32; * \see ScheduleStrategy */ struct RestartParams { - RestartParams(); + typedef ScheduleStrategy Schedule; enum SeqUpdate { seq_continue = 0, seq_repeat = 1, seq_disable = 2 }; + struct Dynamic { + uint32 base; + float k; + uint32 lim; + uint32 fast : 3; + uint32 keep : 2; + uint32 slow : 3; + uint32 sWin : 24; + }; + RestartParams(); uint32 prepare(bool withLookback); void disable(); - bool dynamic() const { return sched.user(); } - bool local() const { return cntLocal != 0; } - SeqUpdate update() const { return static_cast(upRestart); } - ScheduleStrategy sched; /**< Restart schedule to use. */ - float blockScale; /**< Scaling factor for blocking restarts. */ - uint32 blockWindow: 16; /**< Size of moving assignment average for blocking restarts (0: disable). */ - uint32 blockFirst : 16; /**< Enable blocking restarts after blockFirst conflicts. */ - CLASP_ALIGN_BITFIELD(uint32) - uint32 counterRestart:15;/**< Apply counter implication bump every counterRestart restarts (0: disable). */ - uint32 counterBump:15; /**< Bump factor for counter implication restarts. */ - uint32 dynStrat :2; /**< Keep lbd/cfl queue on restart/block? */ + bool disabled() const { return base() == 0; } + bool dynamic() const { return rsSched.type == 3u; } + bool local() const { return cntLocal != 0; } + SeqUpdate update() const { return static_cast(upRestart); } + uint32 base() const { return rsSched.base; } + float dynK() const; + uint32 dynLim() const; + void setDynamic(const Dynamic&); + Schedule schedule() const; + Dynamic rsDynamic()const; + Schedule rsSched; + struct Block { + float scale() const { return static_cast(fscale) / 100.0f; } + uint32 window : 23; /**< Size of moving assignment average for blocking restarts (0: disable). */ + uint32 fscale : 9; /**< Scaling factor for blocking restarts. */ + uint32 first : 29; /**< Disable blocking restarts for first conflicts. */ + uint32 avg : 3; /**< Use avg strategy (see MovingAvg::Type) */ + } block; /**< Blocking restarts options. */ + uint32 counterRestart:16; /**< Apply counter implication bump every counterRestart restarts (0: disable). */ + uint32 counterBump :16; /**< Bump factor for counter implication restarts. */ CLASP_ALIGN_BITFIELD(uint32) - uint32 shuffle :14; /**< Shuffle program after shuffle restarts (0: disable). */ - uint32 shuffleNext:14; /**< Re-Shuffle program every shuffleNext restarts (0: disable). */ - uint32 upRestart : 2; /**< How to update restart sequence after a model was found (one of SeqUpdate). */ - uint32 cntLocal : 1; /**< Count conflicts globally or relative to current branch? */ + uint32 shuffle :14; /**< Shuffle program after shuffle restarts (0: disable). */ + uint32 shuffleNext :14; /**< Re-Shuffle program every shuffleNext restarts (0: disable). */ + uint32 upRestart : 2; /**< How to update restart sequence after a model was found (one of SeqUpdate). */ + uint32 cntLocal : 1; /**< Count conflicts globally or relative to current branch? */ }; //! Reduce strategy used during solving. @@ -379,8 +397,8 @@ struct ReduceParams { Range32 sizeInit(const SharedContext& ctx) const; uint32 cflInit(const SharedContext& ctx) const; uint32 getBase(const SharedContext& ctx) const; - float fReduce() const { return strategy.fReduce / 100.0f; } - float fRestart() const { return strategy.fRestart/ 100.0f; } + float fReduce() const { return static_cast(strategy.fReduce) / 100.0f; } + float fRestart() const { return static_cast(strategy.fRestart)/ 100.0f; } static uint32 getLimit(uint32 base, double f, const Range& r); ScheduleStrategy cflSched; /**< Conflict-based deletion schedule. */ ScheduleStrategy growSched; /**< Growth-based deletion schedule. */ diff --git a/clasp/solver_types.h b/clasp/solver_types.h index a5286d6..3e0a9eb 100644 --- a/clasp/solver_types.h +++ b/clasp/solver_types.h @@ -70,19 +70,18 @@ struct SearchLimits { //! Type for implementing Glucose-style dynamic restarts. /*! * \see G. Audemard, L. Simon. "Refining Restarts Strategies for SAT and UNSAT" - * \note In contrast to Glucose's dynamic restarts, this class also implements - * a heuristic for dynamically adjusting the margin ratio K. + * \note In contrast to Glucose's dynamic restarts, this class also implements a heuristic for + * dynamically adjusting the margin ratio K. */ struct DynamicLimit { - enum Type { lbd_limit, level_limit }; - enum QStrat { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 }; - //! Creates new limit with bounded queue of the given window size. - static DynamicLimit* create(uint32 window); - //! Destroys this object and its bounded queue. - void destroy(); + enum Type { lbd_limit, level_limit }; + enum Keep { keep_never = 0, keep_restart = 1, keep_block = 2, keep_always = 3 }; + //! Creates new limit with moving average of the given window size. + DynamicLimit(uint32 window, MovingAvg::Type fast, Keep keep, MovingAvg::Type slow, uint32 slowWin = 0); + //! Resets moving average and adjust limit. - void init(float k, Type type, QStrat strat, uint32 uLimit = 16000); - //! Resets current run - depending on the queue strategy this also clears the bounded queue. + void init(float k, Type type, uint32 uLimit = 16000); + //! Resets current run - depending on the Keep strategy this also clears the moving average. void resetBlock(); //! Resets moving and global average. void reset(); @@ -99,16 +98,8 @@ struct DynamicLimit { uint32 restart(uint32 maxLBD, float k); //! Returns the number of updates since last restart. uint32 runLen() const { return num_; } - //! Returns the maximal size of the bounded queue. - uint32 window() const { return cap_; } //! Returns whether it is time to restart. - bool reached() const { return runLen() >= window() && (sma(adjust.type) * adjust.rk) > global.avg(adjust.type); } - struct { - //! Returns the global lbd or conflict level average. - double avg(Type t) const { return ratio(sum[t], samples); } - uint64 sum[2]; //!< Sum of lbds/conflict levels since last call to resetGlobal(). - uint64 samples;//!< Samples since last call to resetGlobal(). - } global; //!< Global lbd/conflict level data. + bool reached() const { return runLen() >= avg_.win() && (movingAverage() * adjust.rk) > globalAverage(); } struct { //! Returns the average restart length, i.e. number of conflicts between restarts. double avgRestart() const { return ratio(samples, restarts); } @@ -118,20 +109,27 @@ struct DynamicLimit { float rk; //!< LBD/CFL dynamic limit factor (typically < 1.0). Type type; //!< Dynamic limit based on lbd or conflict level. } adjust; //!< Data for dynamically adjusting margin ratio (rk). + + double globalAverage() const { return global_.avg(adjust.type); } + double movingAverage() const { return avg_.get(); } private: - DynamicLimit(uint32 size); DynamicLimit(const DynamicLimit&); DynamicLimit& operator=(const DynamicLimit&); - double sma(Type t) const { return sum_[t] / double(cap_); } - void resetRun(bool keepQ); - uint64 sum_[2]; - uint32 cap_; - uint32 pos_; - uint32 num_; - QStrat qStrat_; -POTASSCO_WARNING_BEGIN_RELAXED - uint32 buffer_[0]; -POTASSCO_WARNING_END_RELAXED + void resetRun(Keep k); + struct Global { + explicit Global(MovingAvg::Type type, uint32 size = 0); + //! Returns the global lbd or conflict level average. + double avg(Type t) const { return (t == lbd_limit ? lbd : cfl).get(); } + void reset() { + lbd.clear(); + cfl.clear(); + } + MovingAvg lbd; //!< Moving average of lbds + MovingAvg cfl; //!< Moving average of conflict levels + } global_; //!< Global lbd/conflict level data. + MovingAvg avg_; //!< (Fast) moving average. + uint32 num_; //!< Number of samples in this run. + Keep keep_; //!< Strategy for keeping fast moving average. }; //! Type for implementing Glucose-style blocking of restarts. @@ -140,22 +138,18 @@ POTASSCO_WARNING_END_RELAXED * \see A. Biere, A. Froehlich "Evaluating CDCL Restart Schemes" */ struct BlockLimit { - explicit BlockLimit(uint32 windowSize, double R = 1.4); + explicit BlockLimit(uint32 windowSize, double R = 1.4, MovingAvg::Type t = MovingAvg::Type::avg_ema); bool push(uint32 nAssign) { - ema = n >= span - ? exponentialMovingAverage(ema, nAssign, alpha) - : cumulativeMovingAverage(ema, nAssign, n); + avg.push(nAssign); return ++n >= next; } //! Returns the exponential moving average scaled by r. - double scaled() const { return ema * r; } - double ema; //!< Current exponential moving average. - double alpha; //!< Smoothing factor: 2/(span+1). - uint64 next; //!< Enable once n >= next. - uint64 inc; //!< Block restart for next inc conflicts. - uint64 n; //!< Number of data points seen so far. - uint32 span; //!< Minimum observation window. - float r; //!< Scale factor for ema. + double scaled() const { return avg.get() * r; } + MovingAvg avg; //!< Moving average. + uint64 next; //!< Enable once n >= next. + uint64 inc; //!< Block restart for next inc conflicts. + uint64 n; //!< Number of data points seen so far. + float r; //!< Scale factor for moving average. }; /////////////////////////////////////////////////////////////////////////////// // Statistics @@ -301,7 +295,7 @@ struct SolverStats : public CoreStats { ~SolverStats(); bool enableExtended(); bool enable(const SolverStats& o) { return !o.extra || enableExtended(); } - void enableLimit(uint32 size); + void acquireLimit(DynamicLimit* limit); void reset(); void accu(const SolverStats& o); void accu(const SolverStats& o, bool enableRhs); diff --git a/clasp/util/misc_types.h b/clasp/util/misc_types.h index 3677873..f76150f 100644 --- a/clasp/util/misc_types.h +++ b/clasp/util/misc_types.h @@ -1,5 +1,5 @@ // -// Copyright (c) 2006-2017 Benjamin Kaufmann +// Copyright (c) 2006-present Benjamin Kaufmann // // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ // @@ -141,16 +141,94 @@ class RNG { /*! * Computes ema = currentEma + ((double(sample) - currentEma)*alpha); */ -template -inline double exponentialMovingAverage(double currentEma, T sample, double alpha) { - return (static_cast(sample) * alpha) + (currentEma * (1.0 - alpha)); +inline double exponentialMovingAverage(double currentEma, double sample, double alpha) { + return currentEma + (alpha * (sample - currentEma)); } -//! Updates the given moving average with the given sample. -template -inline double cumulativeMovingAverage(double currentAvg, T sample, uint64 numSeen) { +//! Updates the given cumulative moving average with the given sample. +inline double cumulativeMovingAverage(double currentAvg, double sample, uint64 numSeen) { return (static_cast(sample) + (currentAvg * numSeen)) / static_cast(numSeen + 1); } +//! Updates the given simple moving average with the given sample. +inline double simpleMovingAverage(double currentAvg, uint32 sample, uint32* buffer, uint32 cap, uint32 pos, bool full) { + assert(pos < cap); + double oldS = static_cast(buffer[pos]); + double newS = static_cast(sample); + buffer[pos] = sample; + return full ? currentAvg + ((newS - oldS) / cap) : cumulativeMovingAverage(currentAvg, newS, pos); +} + +class MovingAvg { +public: + enum Type { avg_sma = 0, avg_ema = 1, avg_ema_log = 2, avg_ema_smooth = 3, avg_ema_log_smooth = 4 }; + + MovingAvg(uint32 window, Type type) + : avg_(0.0), extra_(), pos_(0), win_(window), full_(window == 0), cma_(0), ema_(type != avg_sma) { + assert(window > 0 || type == avg_sma); + if (ema_) { + cma_ = (type < avg_ema_smooth); + extra_.alpha = (type & 1u) != 0 ? 2.0 / (window + 1) : 1.0 / (1u << log2(window)); + } + else if (window) { + extra_.sma = new uint32[window]; + } + else { + extra_.num = 0; + } + } + + ~MovingAvg() { + if (!ema_ && win_) + delete [] extra_.sma; + } + + bool push(uint32 val) { + if (cumulative()) avg_ = cumulativeMovingAverage(avg_, val, extra_.num++); + else if (ema_ == 0) avg_ = simpleMovingAverage(avg_, val, extra_.sma, win_, pos_, valid()); + else if (valid()) avg_ = exponentialMovingAverage(avg_, val, extra_.alpha); + else if (cma_) avg_ = cumulativeMovingAverage(avg_, val, pos_); + else avg_ = exponentialMovingAverage(avg_, val, smoothAlpha(extra_.alpha, pos_)); + if (++pos_ == win_) { pos_ = 0; full_ = 1; } + return valid(); + } + + void clear() { + avg_ = 0.0; + pos_ = 0; + if (cumulative()) + extra_.num = 0; + else + full_ = 0; + } + + double get() const { return avg_; } + bool valid() const { return full_ != 0; } + uint32 win() const { return win_; } + +private: + MovingAvg(const MovingAvg&); + MovingAvg& operator=(const MovingAvg&); + bool cumulative() const { + return !ema_ && !win_; + } + + static double smoothAlpha(double alpha, uint32 pos) { + return pos < 32 ? std::max(alpha, 1.0 / static_cast(uint32(1) << pos)) : alpha; + } + + double avg_; + union Extra { + uint32* sma; // Buffer for SMA + double alpha; // Smoothing factor for EMA + uint64 num; // Number of data points for CMA + } extra_; + uint32 pos_; // + uint32 win_ : 29; // Window size (for SMA/EMA) + uint32 full_: 1; // Enough data points seen? + uint32 cma_ : 1; // Use cumulative moving average for first data points + uint32 ema_ : 1; // Exponential Moving Average? +}; + //! An unary operator function that calls p->destroy(). struct DestroyObject { template void operator()(T* p) const { if (p) p->destroy(); } diff --git a/src/clasp_options.cpp b/src/clasp_options.cpp index 948750a..b7a09fd 100644 --- a/src/clasp_options.cpp +++ b/src/clasp_options.cpp @@ -234,6 +234,9 @@ static std::string& xconvert(std::string& out, X x) { \ #define ARG(a) #define NO_ARG #include +DEFINE_ENUM_MAPPING(DynamicLimit::Keep, \ + MAP("n", DynamicLimit::keep_never), MAP("r", DynamicLimit::keep_restart), MAP("b", DynamicLimit::keep_block), \ + MAP("br", DynamicLimit::keep_always), MAP("rb", DynamicLimit::keep_always)) namespace Cli { DEFINE_ENUM_MAPPING(ConfigKey, \ MAP("auto", config_default), MAP("frumpy", config_frumpy), MAP("jumpy", config_jumpy), \ @@ -245,37 +248,38 @@ DEFINE_ENUM_MAPPING(ConfigKey, \ ///////////////////////////////////////////////////////////////////////////////////////// // Conversion functions for complex clasp types ///////////////////////////////////////////////////////////////////////////////////////// +static int convertRet(int res, const char* in, const char** next) { + if (next) *next = in; + return res; +} + static int xconvert(const char* x, ScheduleStrategy& out, const char** errPos, int e) { using Potassco::xconvert; - if (!x) { return 0; } - const char* next = std::strchr(x, ','); + const char* next = std::strchr(x ? x : "", ','); uint32 base = 0; - int tok = 1; - if (errPos) { *errPos = x; } - if (!next || !xconvert(next+1, base, &next, e) || base == 0) { return 0; } - if (strncasecmp(x, "f,", 2) == 0 || strncasecmp(x, "fixed,", 6) == 0){ + if (!next || !xconvert(next+1, base, &next, e) || base == 0) { return convertRet(0, x, errPos); } + if (strncasecmp(x, "f,", 2) == 0 || strncasecmp(x, "fixed,", 6) == 0) { out = ScheduleStrategy::fixed(base); } else if (strncasecmp(x, "l,", 2) == 0 || strncasecmp(x, "luby,", 5) == 0) { uint32 lim = 0; - if (*next == ',' && !xconvert(next+1, lim, &next, e)) { return 0; } + if (*next == ',' && !xconvert(next+1, lim, &next, e)) { return convertRet(0, next, errPos); } out = ScheduleStrategy::luby(base, lim); } else if (strncmp(x, "+,", 2) == 0 || strncasecmp(x, "add,", 4) == 0) { std::pair arg(0, 0); - if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return 0; } + if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return convertRet(0, next, errPos); } out = ScheduleStrategy::arith(base, arg.first, arg.second); } - else if (strncmp(x, "x,", 2) == 0 || strncmp(x, "*,", 2) == 0 || strncasecmp(x, "d,", 2) == 0) { + else if (strncmp(x, "x,", 2) == 0 || strncmp(x, "*,", 2) == 0) { std::pair arg(0, 0); - if (*next != ',' || !xconvert(next+1, arg, &next, e)) { return 0; } - if (strncasecmp(x, "d", 1) == 0 && arg.first > 0.0) { out = ScheduleStrategy(ScheduleStrategy::User, base, arg.first, arg.second); } - else if (strncasecmp(x, "d", 1) != 0 && arg.first >= 1.0){ out = ScheduleStrategy::geom(base, arg.first, arg.second); } - else { return 0; } + if (*next != ',' || !xconvert(next+1, arg, &next, e) || arg.first < 1.0) { return convertRet(0, next, errPos); } + out = ScheduleStrategy::geom(base, arg.first, arg.second); + } + else { + return convertRet(0, x, errPos); } - else { next = x; tok = 0; } - if (errPos) { *errPos = next; } - return tok; + return convertRet(1, next, errPos); } static std::string& xconvert(std::string& out, const ScheduleStrategy& sched) { using Potassco::xconvert; @@ -295,12 +299,56 @@ static std::string& xconvert(std::string& out, const ScheduleStrategy& sched) { out[t] = 'l'; if (sched.len) { return xconvert(out.append(1, ','), sched.len); } else { return out; } - case ScheduleStrategy::User: - out[t] = 'd'; - return xconvert(out.append(1, ','), std::make_pair((double)sched.grow, sched.len)); default: POTASSCO_ASSERT(false, "xconvert(ScheduleStrategy): unknown type"); } } +static int xconvert(const char* x, RestartParams::Dynamic& out, const char** errPos, int e) { + using Potassco::xconvert; + if (!x || !xconvert(x, out.base, &x, e)) + return convertRet(0, x, errPos); + if (out.base > 0) { + if (*x != ',' || !xconvert(x + 1, out.k, &x, e) || out.k <= 0) + return convertRet(0, x, errPos); + if (*x == ',' && !xconvert(x + 1, out.lim, &x, e)) + return convertRet(0, x, errPos); + MovingAvg::Type fast = MovingAvg::Type::avg_sma; + if (*x == ',' && !xconvert(x + 1, fast, &x, e)) + return convertRet(0, x, errPos); + out.fast = fast; + DynamicLimit::Keep keep = DynamicLimit::keep_never; + const char* next = 0; + if (*x == ',' && fast != MovingAvg::Type::avg_sma && xconvert(x + 1, keep, &next, e)) + x = next; + out.keep = keep; + MovingAvg::Type slow = MovingAvg::Type::avg_sma; + if (*x == ',' && !xconvert(x + 1, slow, &x, e)) + return convertRet(0, x, errPos); + out.slow = slow; + uint32 n = 0; + if (*x == ',' && slow != MovingAvg::Type::avg_sma && !xconvert(x + 1, n, &x, e)) + return convertRet(0, x, errPos); + SET_OR_FILL(out.sWin, n); + } + return convertRet(1, x, errPos); +} +static std::string& xconvert(std::string& out, const RestartParams::Dynamic& in) { + using Potassco::xconvert; + if (!in.base) + return xconvert(out, in.base); + + xconvert(out, std::make_pair(in.base, in.k)); + if (in.lim || in.fast || in.slow) + xconvert(out.append(1, ','), in.lim); + if (in.fast || in.slow) + xconvert(out.append(1, ','), static_cast(in.fast)); + if (in.fast && in.keep) + xconvert(out.append(1, ','), static_cast(in.keep)); + if (in.slow) { + xconvert(out.append(1, ','), static_cast(in.slow)); + if (in.sWin) xconvert(out.append(1, ','), in.sWin); + } + return out; +} static bool setOptLegacy(OptParams& out, uint32 n) { if (n >= 20) { return false; } out.type = n < 4 ? OptParams::type_bb : OptParams::type_usc; @@ -1178,7 +1226,7 @@ const char* validate(const SolverParams& solver, const SolveParams& search) { const ReduceParams& reduce = search.reduce; if (solver.search == SolverParams::no_learning) { if (Heuristic_t::isLookback(solver.heuId)) return "Heuristic requires lookback strategy!"; - if (!search.restart.sched.disabled() && !search.restart.sched.defaulted()) return "'no-lookback': restart options disabled!"; + if (!search.restart.disabled()) return "'no-lookback': restart options disabled!"; if (!reduce.cflSched.disabled() || (!reduce.growSched.disabled() && !reduce.growSched.defaulted()) || search.reduce.fReduce() != 0) return "'no-lookback': deletion options disabled!"; } bool hasSched = !reduce.cflSched.disabled() || !reduce.growSched.disabled() || reduce.maxRange != UINT32_MAX; diff --git a/src/solve_algorithms.cpp b/src/solve_algorithms.cpp index 3b166aa..b21b42a 100644 --- a/src/solve_algorithms.cpp +++ b/src/solve_algorithms.cpp @@ -92,20 +92,14 @@ bool BasicSolve::assume(const LitVec& path) { return solver_->pushRoot(path); } -BasicSolve::State::State(Solver& s, const SolveParams& p) { +BasicSolve::State::State(Solver& s, const SolveParams& p) + : dbGrowNext(p.reduce.growSched.current()), dbRed(p.reduce.cflSched), nRestart(0), nGrow(0) + , dbRedInit(p.reduce.cflInit(*s.sharedContext())), dbPinned(0), rsShuffle(p.restart.shuffle), resetState(false) { Range32 dbLim= p.reduce.sizeInit(*s.sharedContext()); - dbGrowNext = p.reduce.growSched.current(); dbMax = dbLim.lo; dbHigh = dbLim.hi; - dbRed = p.reduce.cflSched; - nRestart = 0; - nGrow = 0; - dbRedInit = p.reduce.cflInit(*s.sharedContext()); - dbPinned = 0; - rsShuffle = p.restart.shuffle; - resetState = false; if (dbLim.lo < s.numLearntConstraints()) { - dbMax = std::min(dbHigh, double(s.numLearntConstraints() + p.reduce.initRange.lo)); + dbMax = std::min(dbHigh, double(s.numLearntConstraints() + p.reduce.initRange.lo)); } if (dbRedInit && dbRed.type != ScheduleStrategy::Luby) { if (dbRedInit < dbRed.base) { @@ -116,13 +110,16 @@ BasicSolve::State::State(Solver& s, const SolveParams& p) { dbRedInit = 0; } if (p.restart.dynamic()) { - s.stats.enableLimit(p.restart.sched.base); - s.stats.limit->reset(); + const RestartParams::Dynamic& dr = p.restart.rsDynamic(); + s.stats.acquireLimit(new DynamicLimit(dr.base, static_cast(dr.fast), + static_cast(dr.keep), + static_cast(dr.slow), dr.sWin)); } - if (p.restart.blockScale > 0.0f && p.restart.blockWindow > 0) { - rsBlock.reset(new BlockLimit(p.restart.blockWindow, p.restart.blockScale)); - rsBlock->inc = std::max(p.restart.sched.base, uint32(50)); - rsBlock->next = std::max(p.restart.blockWindow, p.restart.blockFirst); + if (p.restart.block.fscale > 0 && p.restart.block.window > 0) { + const RestartParams::Block& block = p.restart.block; + rsBlock.reset(new BlockLimit(block.window, block.scale(), static_cast(block.avg))); + rsBlock->inc = std::max(p.restart.base(), uint32(50)); + rsBlock->next = std::max(block.window, block.first); } s.stats.lastRestart = s.stats.analyzed; } @@ -148,7 +145,7 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* } WeightLitVec inDegree; SearchLimits sLimit; - ScheduleStrategy rs = p.restart.sched; + ScheduleStrategy rs = p.restart.schedule(); ScheduleStrategy dbGrow = p.reduce.growSched; Solver::DBInfo db = {0,0,dbPinned}; ValueRep result = value_free; @@ -159,7 +156,7 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* sLimit = SearchLimits(); } else if (p.restart.dynamic() && s.stats.limit) { - if (!nRestart) { s.stats.limit->init((float)p.restart.sched.grow, DynamicLimit::lbd_limit, static_cast(p.restart.dynStrat)); } + if (!nRestart) { s.stats.limit->init(p.restart.dynK(), DynamicLimit::lbd_limit); } sLimit.restart.dynamic = s.stats.limit; sLimit.restart.conflicts = s.stats.limit->adjust.limit - std::min(s.stats.limit->adjust.samples, s.stats.limit->adjust.limit - 1); } @@ -202,7 +199,12 @@ ValueRep BasicSolve::State::solve(Solver& s, const SolveParams& p, SolveLimits* } if (sLimit.restart.dynamic) { n = sLimit.restart.dynamic->runLen(); - sLimit.restart.conflicts = sLimit.restart.dynamic->restart(rs.len ? rs.len : UINT32_MAX, (float)rs.grow); + uint32 limLbd = p.restart.dynLim(); + if (limLbd == 0) + limLbd = UINT32_MAX; + else if (limLbd == UINT32_MAX) + limLbd = 0; + sLimit.restart.conflicts = sLimit.restart.dynamic->restart(limLbd, p.restart.dynK()); } else { sLimit.restart.conflicts = n = rs.next(); diff --git a/src/solver_strategies.cpp b/src/solver_strategies.cpp index eb57bb0..49064af 100644 --- a/src/solver_strategies.cpp +++ b/src/solver_strategies.cpp @@ -97,17 +97,19 @@ ScheduleStrategy::ScheduleStrategy(Type t, uint32 b, double up, uint32 lim) : base(b), type(t), idx(0), len(lim), grow(0.0) { if (t == Geometric) { grow = static_cast(std::max(1.0, up)); } else if (t == Arithmetic) { grow = static_cast(std::max(0.0, up)); } - else if (t == User) { grow = static_cast(std::max(0.0, up)); } else if (t == Luby && lim){ len = std::max(uint32(2), (static_cast(std::pow(2.0, std::ceil(log(double(lim))/log(2.0)))) - 1)*2); } } +static uint64_t saturate(double d) { + return d < static_cast(UINT64_MAX) ? static_cast(d) : UINT64_MAX; +} + uint64 ScheduleStrategy::current() const { - enum { t_add = ScheduleStrategy::Arithmetic, t_luby = ScheduleStrategy::Luby }; - if (base == 0) return UINT64_MAX; - else if (type == t_add) return static_cast(addR(idx, grow) + base); - else if (type == t_luby)return static_cast(lubyR(idx)) * base; - uint64 x = static_cast(growR(idx, grow) * base); - return x + !x; + if (base == 0) return UINT64_MAX; + else if (type == Geometric) return saturate(growR(idx, grow) * base); + else if (type == Arithmetic) return static_cast(addR(idx, grow) + base); + else if (type == Luby) return static_cast(lubyR(idx)) * base; + else return base; } uint64 ScheduleStrategy::next() { if (++idx != len) { return current(); } @@ -138,19 +140,50 @@ void ScheduleStrategy::advanceTo(uint32 n) { // RestartParams ///////////////////////////////////////////////////////////////////////////////////////// RestartParams::RestartParams() - : sched() - , blockScale(1.4f), blockWindow(0), blockFirst(0) + : rsSched() + , block() , counterRestart(0), counterBump(9973) , shuffle(0), shuffleNext(0) , upRestart(0), cntLocal(0) { static_assert(sizeof(RestartParams) == sizeof(ScheduleStrategy) + (3 * sizeof(uint32)) + sizeof(float), "Invalid structure alignment"); } + +ScheduleStrategy RestartParams::schedule() const { + return dynamic() ? ScheduleStrategy::none() : rsSched; +} +RestartParams::Dynamic RestartParams::rsDynamic() const { + Dynamic ret = {0}; + if (!dynamic()) + return ret; + ret.base = base(); + ret.k = dynK(); + ret.lim = dynLim(); + std::memcpy(&ret.base + 3, &rsSched.idx, sizeof(uint32)); + return ret; +} + +float RestartParams::dynK() const { + return rsSched.grow; +} + +uint32 RestartParams::dynLim() const { + return rsSched.len; +} + +void RestartParams::setDynamic(const Dynamic& dyn) { + rsSched.type = 3u; + rsSched.base = dyn.base; + rsSched.grow = dyn.k; + rsSched.len = dyn.lim; + std::memcpy(&rsSched.idx, &dyn.base + 3, sizeof(uint32)); +} + void RestartParams::disable() { std::memset(this, 0, sizeof(RestartParams)); - sched = ScheduleStrategy::none(); + rsSched = ScheduleStrategy::none(); } uint32 RestartParams::prepare(bool withLookback) { - if (!withLookback || sched.disabled()) { + if (!withLookback || disabled()) { disable(); } return 0; diff --git a/src/solver_types.cpp b/src/solver_types.cpp index 10336ed..e83d080 100644 --- a/src/solver_types.cpp +++ b/src/solver_types.cpp @@ -43,59 +43,58 @@ SearchLimits::SearchLimits() { ///////////////////////////////////////////////////////////////////////////////////////// // DynamicLimit ///////////////////////////////////////////////////////////////////////////////////////// -DynamicLimit* DynamicLimit::create(uint32 size) { +DynamicLimit::Global::Global(MovingAvg::Type type, uint32 size) + : lbd(size, type) + , cfl(size, type) { +} + +static uint32 verifySize(uint32 size) { POTASSCO_REQUIRE(size != 0, "size must be > 0"); - void* m = ::operator new(sizeof(DynamicLimit) + (size*sizeof(uint32))); - return new (m)DynamicLimit(size); + return size; } -DynamicLimit::DynamicLimit(uint32 sz) : cap_(sz), pos_(0), num_(0), qStrat_(keep_never) { - std::memset(&global, 0, sizeof(global)); - init(0.7f, lbd_limit, keep_never); + +DynamicLimit::DynamicLimit(uint32 size, MovingAvg::Type fast, Keep keep, MovingAvg::Type slow, uint32 slowSize) + : global_(slow, slowSize || slow == MovingAvg::avg_sma ? slowSize : 200 * verifySize(size)) + , avg_(verifySize(size), fast) + , num_(0) + , keep_(keep) { + init(0.7f, lbd_limit); } -void DynamicLimit::init(float k, Type t, QStrat strat, uint32 uLimit) { - resetRun((strat & keep_restart) != 0); + +void DynamicLimit::init(float k, Type t, uint32 uLimit) { + resetRun(keep_restart); std::memset(&adjust, 0, sizeof(adjust)); adjust.limit = uLimit; adjust.rk = k; adjust.type = t; - qStrat_ = strat; } void DynamicLimit::resetBlock() { - resetRun((qStrat_ & keep_block) != 0); + resetRun(keep_block); } -void DynamicLimit::destroy() { - this->~DynamicLimit(); - ::operator delete(this); -} -void DynamicLimit::resetRun(bool keepQ) { + +void DynamicLimit::resetRun(Keep k) { num_ = 0; - if (!keepQ) - sum_[0] = sum_[1] = pos_ = 0; + if ((keep_ & k) == 0) + avg_.clear(); } void DynamicLimit::reset() { - std::memset(&global, 0, sizeof(global)); - resetRun(false); + global_.reset(); + resetRun(keep_never); } void DynamicLimit::update(uint32 dl, uint32 lbd) { // update global avg ++adjust.samples; - ++global.samples; - global.sum[lbd_limit] += lbd; - global.sum[level_limit] += dl; + global_.cfl.push(dl); + global_.lbd.push(lbd); // update moving avg - sum_[lbd_limit] += lbd; - sum_[level_limit] += dl; - if (++num_ > cap_) { - sum_[lbd_limit] -= (buffer_[pos_] & 127u); - sum_[level_limit] -= (buffer_[pos_] >> 7u); - } - buffer_[pos_++] = ((dl << 7) + lbd); - if (pos_ == cap_) { pos_ = 0; } + ++num_; + uint32 v = adjust.type == lbd_limit ? lbd : dl; + avg_.push(v); } uint32 DynamicLimit::restart(uint32 maxLBD, float k) { ++adjust.restarts; - if (adjust.samples >= adjust.limit) { - Type nt = global.avg(lbd_limit) > maxLBD ? level_limit : lbd_limit; + if (adjust.samples >= adjust.limit && maxLBD) { + Type nt = global_.avg(lbd_limit) > maxLBD ? level_limit : lbd_limit; if (nt == adjust.type) { double rLen = adjust.avgRestart(); bool sx = num_ >= adjust.limit; @@ -106,17 +105,16 @@ uint32 DynamicLimit::restart(uint32 maxLBD, float k) { else if (rLen >= 4000.0) { rk += 0.05f; } else if (rLen >= 1000.0) { uLim += 10000u; } else if (rk > k) { rk -= 0.05f; } - init(rk, nt, qStrat_, uLim); + init(rk, nt, uLim); } - else { init(k, nt, qStrat_); } + else { init(k, nt); } } - else { resetRun((qStrat_ & keep_restart) != 0); } + else { resetRun(keep_restart); } return adjust.limit; } -BlockLimit::BlockLimit(uint32 windowSize, double R) - : ema(0.0), alpha(2.0/(windowSize+1)) +BlockLimit::BlockLimit(uint32 windowSize, double R, MovingAvg::Type at) + : avg(windowSize, at) , next(windowSize), inc(50), n(0) - , span(windowSize) , r(static_cast(R)) {} ///////////////////////////////////////////////////////////////////////////////////////// @@ -186,14 +184,14 @@ SolverStats::SolverStats(const SolverStats& o) : CoreStats(o), limit(0), extra(0 } SolverStats::~SolverStats() { delete extra; - if (limit) limit->destroy(); + delete limit; } bool SolverStats::enableExtended() { return extra != 0 || (extra = new (std::nothrow) ExtendedStats()) != 0; } -void SolverStats::enableLimit(uint32 size) { - if (limit && limit->window() != size) { limit->destroy(); limit = 0; } - if (!limit) { limit = DynamicLimit::create(size); } +void SolverStats::acquireLimit(DynamicLimit* dl) { + delete limit; + limit = dl; } void SolverStats::reset() { CoreStats::reset(); diff --git a/tests/cli_test.cpp b/tests/cli_test.cpp index 53ce512..67837f3 100644 --- a/tests/cli_test.cpp +++ b/tests/cli_test.cpp @@ -108,7 +108,7 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(config.getValue("configuration") == tempName); REQUIRE(config.solve.numModels == 0); REQUIRE(config.solver(0).heuId == Heuristic_t::Berkmin); - REQUIRE(config.search(0).restart.sched == ScheduleStrategy::geom(100, 1.5)); + REQUIRE(config.search(0).restart.schedule() == ScheduleStrategy::geom(100, 1.5)); std::remove(tempName); REQUIRE(config.setValue(config.getKey(ClaspCliConfig::KEY_ROOT, "configuration"), tempName) == -2); } @@ -156,7 +156,7 @@ TEST_CASE("Cli options", "[cli]") { // search option REQUIRE(config.setValue("solver.2.restarts", "+,100,10")); REQUIRE(config.numSearch() == 3); - REQUIRE(config.search(2).restart.sched == ScheduleStrategy::arith(100, 10)); + REQUIRE(config.search(2).restart.schedule() == ScheduleStrategy::arith(100, 10)); REQUIRE(config.numSolver() == 3); REQUIRE(config.setValue("solver.17.heuristic", "unit")); @@ -464,6 +464,72 @@ TEST_CASE("Cli options", "[cli]") { REQUIRE(config.getValue("solve.opt_mode") == "opt,50,20"); } + SECTION("test dynamic restart option") { + REQUIRE(config.getValue("solver.restarts") == "x,100,1.5,0"); + REQUIRE_FALSE(config.setValue("solver.restarts", "D,100")); + REQUIRE_FALSE(config.setValue("solver.restarts", "D,0")); + + REQUIRE(config.setValue("solver.restarts", "D,50,0.8")); + REQUIRE(config.getValue("solver.restarts") == "d,50,0.8"); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,20")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,20"); + REQUIRE(config.search(0).restart.dynamic()); + REQUIRE(config.search(0).restart.dynLim() == 20); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,0,es,r")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,0,es,r"); + REQUIRE(config.search(0).restart.dynamic()); + RestartParams::Dynamic dyn = config.search(0).restart.rsDynamic(); + REQUIRE(dyn.lim == 0); + REQUIRE(dyn.fast == uint32(MovingAvg::Type::avg_ema_smooth)); + REQUIRE(dyn.keep == uint32(DynamicLimit::keep_restart)); + + REQUIRE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234")); + REQUIRE(config.getValue("solver.restarts") == "d,100,0.9,255,ls,br,e,1234"); + REQUIRE(config.search(0).restart.dynamic()); + dyn = config.search(0).restart.rsDynamic(); + REQUIRE(dyn.lim == 255); + REQUIRE(dyn.fast == uint32(MovingAvg::Type::avg_ema_log_smooth)); + REQUIRE(dyn.keep == uint32(DynamicLimit::keep_always)); + REQUIRE(dyn.slow == uint32(MovingAvg::Type::avg_ema)); + REQUIRE(dyn.sWin == 1234); + + REQUIRE_FALSE(config.setValue("solver.restarts", "D,100,0.9,255,ls,rb,e,1234,12")); + + REQUIRE(config.setValue("solver.restarts", "D,50,0.8,0,ls,es,10000")); + REQUIRE(config.getValue("solver.restarts") == "d,50,0.8,0,ls,es,10000"); + dyn = config.search(0).restart.rsDynamic(); + REQUIRE(dyn.lim == 0); + REQUIRE(dyn.fast == uint32(MovingAvg::Type::avg_ema_log_smooth)); + REQUIRE(dyn.keep == uint32(DynamicLimit::keep_never)); + REQUIRE(dyn.slow == uint32(MovingAvg::Type::avg_ema_smooth)); + REQUIRE(dyn.sWin == 10000); + } + + SECTION("test block restart option") { + REQUIRE(config.getValue("solver.block_restarts") == "no"); + REQUIRE_FALSE(config.setValue("solver.block_restarts", "0,1.3")); + + REQUIRE(config.setValue("solver.block_restarts", "5000")); + REQUIRE(config.getValue("solver.block_restarts") == "5000,1.4,10000,e"); + RestartParams::Block b = config.search(0).restart.block; + REQUIRE(b.window == 5000); + REQUIRE(b.first == 10000); + REQUIRE(b.scale() == 1.4f); + REQUIRE(b.avg == uint32(MovingAvg::Type::avg_ema)); + + REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,0.8")); + REQUIRE_FALSE(config.setValue("solver.block_restarts", "5000,5.1")); + + REQUIRE(config.setValue("solver.block_restarts", "10000,1.1,0,d")); + b = config.search(0).restart.block; + REQUIRE(b.window == 10000); + REQUIRE(b.scale() == 1.1f); + REQUIRE(b.first == 0); + REQUIRE(b.avg == uint32(MovingAvg::Type::avg_sma)); + } + SECTION("test get values") { std::string out; REQUIRE(config.getValue(config.getKey(ClaspCliConfig::KEY_TESTER, "configuration"), out) == -1); @@ -547,15 +613,19 @@ TEST_CASE("Cli mt options", "[cli][mt]") { REQUIRE(config.getValue("configuration") == tempName); REQUIRE(config.solve.numModels == 0); REQUIRE(config.solver(0).heuId == Heuristic_t::Berkmin); - REQUIRE(config.search(0).restart.sched == ScheduleStrategy::geom(100, 1.5)); + REQUIRE(config.search(0).restart.schedule() == ScheduleStrategy::geom(100, 1.5)); REQUIRE(config.solve.numSolver() == 4); REQUIRE(config.numSolver() == 4); REQUIRE(config.solver(1).heuId == Heuristic_t::Vsids); REQUIRE(config.solver(2).heuId == Heuristic_t::Vmtf); REQUIRE(config.solver(3).heuId == Heuristic_t::None); - REQUIRE(config.search(1).restart.sched == ScheduleStrategy::luby(128)); - REQUIRE(config.search(2).restart.sched == ScheduleStrategy(ScheduleStrategy::User, 100, 0.7, 0)); - REQUIRE(config.search(3).restart.sched == ScheduleStrategy::fixed(1000)); + REQUIRE(config.search(1).restart.schedule() == ScheduleStrategy::luby(128)); + REQUIRE(config.search(2).restart.schedule() == ScheduleStrategy::none()); + REQUIRE(config.search(2).restart.dynamic()); + REQUIRE(config.search(2).restart.base() == 100); + REQUIRE(config.search(2).restart.dynK() == 0.7f); + REQUIRE(config.search(2).restart.dynLim() == 0); + REQUIRE(config.search(3).restart.schedule() == ScheduleStrategy::fixed(1000)); std::remove(tempName); REQUIRE(config.setValue(config.getKey(ClaspCliConfig::KEY_ROOT, "configuration"), tempName) == -2); } diff --git a/tests/solver_test.cpp b/tests/solver_test.cpp index 5897c20..1bd5458 100644 --- a/tests/solver_test.cpp +++ b/tests/solver_test.cpp @@ -1773,6 +1773,22 @@ TEST_CASE("once", "[.once]") { REQUIRE((r1.idx == r2.idx && r1.len == r2.len)); } } + SECTION("testScheduleOverflow") { + ScheduleStrategy g = ScheduleStrategy::geom(100, 0.0); + REQUIRE(g.grow == 1.0); + REQUIRE(g.current() == 100); + + g = ScheduleStrategy::geom(1, 2.0); + REQUIRE(g.current() == 1); + REQUIRE(g.next() == 2); + REQUIRE(g.next() == 4); + g.advanceTo(12); + REQUIRE(g.current() == 4096); + g.advanceTo(63); + REQUIRE(g.current() == (uint64(1) << 63)); + g.advanceTo(64); + REQUIRE(g.current() == UINT64_MAX); + } } #if CLASP_HAS_THREADS