Commit 903a3a37 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

timeouts and cardinality options in pccompile

parent 92078159
......@@ -15,6 +15,7 @@
#include <iostream>
#include "cardinal.h"
#include "cardinal_opt.h"
#include "cnfcompress.h"
#include "logstream.h"
#include "normalform.h"
......@@ -142,7 +143,7 @@ dump_config(const config_t &conf, unsigned level)
"\t", level, "initial_negatives", conf.initial_negatives);
SUBool::logs.TLog(level)
<< "\trandom seed: " << conf.random_seed << std::endl;
SUBool::logs.TLog(level) << "\ttimeout: " << conf.timeout << std::endl;
SUBool::logs.DumpValue("\t", level, "timeout", conf.timeout);
SUBool::logs.TLog(level)
<< "\tcomp_base_config.timeouts.timeout: "
<< conf.comp_base_config.timeouts.timeout << std::endl;
......@@ -182,6 +183,9 @@ parse_arguments(int argc, char *argv[], config_t &conf)
auto pccheck_random_opts =
opts.MakeOptionsGroup<SUBool::PCRandomPCChecksOptions>();
auto minimize_opts = opts.MakeOptionsGroup<SUBool::PCMinimizationOptions>();
auto timeout_opts = opts.MakeOptionsGroup<SUBool::PCTimeoutsOptions>();
auto cardinal_opt_group =
opts.MakeOptionsGroup<SUBool::CardinalOptionsGroup>();
if (!opts.Parse(argc, argv))
{
return 1;
......@@ -209,6 +213,10 @@ parse_arguments(int argc, char *argv[], config_t &conf)
conf.comp_base_config.minimize_method = minimize_opts->MinimizeMethod();
conf.comp_base_config.minimize_steps = minimize_opts->MinimizeSteps();
conf.level_minimize = !minimize_opts->NoLevelMinimize();
conf.timeout = timeout_opts->Timeout();
conf.comp_base_config.timeouts = timeout_opts->EmpTimeouts();
conf.amo_encoding = cardinal_opt_group->AmoEncoding();
conf.exone_encoding = cardinal_opt_group->ExOneEncoding();
return 0;
#if 0
try
......
......@@ -39,7 +39,7 @@ namespace SUBool
static const size_t kLogStep = 1000;
std::atomic<unsigned> mVerbLevel;
std::atomic<unsigned> mFloatPrecision{3};
static const unsigned kDefaultFloatPrecision = 3;
LogStream(std::ostream &out, unsigned verbosity_level)
: mOut(&out), mVerbLevel(verbosity_level)
......@@ -80,12 +80,13 @@ namespace SUBool
template <class T>
void
DumpValue(const std::string &line_prefix, unsigned level,
const std::string &name, const T &value)
const std::string &name, const T &value,
unsigned float_precision = kDefaultFloatPrecision)
{
if (CheckLevel(level))
{
TLog(level) << line_prefix << name << ": "
<< std::setprecision(mFloatPrecision) << value
<< std::setprecision(float_precision) << value
<< std::endl;
}
}
......@@ -100,7 +101,7 @@ namespace SUBool
template <>
inline void
SUBool::LogStream::DumpValue<bool>(const std::string &line_prefix,
unsigned level, const std::string &name, const bool &value)
unsigned level, const std::string &name, const bool &value, unsigned)
{
DumpValue<std::string>(line_prefix, level, name, bool_to_string(value));
}
......
......@@ -239,3 +239,47 @@ SUBool::PCMinimizationOptions::GetValues()
{
return mMinimizeMethodOption.GetValue(mMinimizeMethod);
}
SUBool::PCTimeoutsOptions::PCTimeoutsOptions() : OptionsGroup("Timeouts")
{
AddOptions() //
("timeout,t",
po::value<long double>(&mTimeout)->default_value(-1.0l, "-1.0"),
"Total timeout for the computation in seconds as a fractional "
"number. After this amount of seconds, the process finishes. Value "
"t<=0.0 means that the computation is not bounded by a timeout. The "
"timer uses CLOCK_REALTIME") //
("emp-timeout",
po::value<long double>(&mEmpTimeouts.timeout)
->default_value(-1.0l, "-1.0"),
"Timeout for a single SAT call which looks for an empowering "
"implicate. The timeout is in seconds as a fractional number.") //
("emp-timeout-level-base",
po::value<long double>(&mEmpTimeouts.level_base)
->default_value(-1.0l, "-1.0"),
"This parameter together with emp-timeout-level-factor allows to "
"set the timeout for a single SAT which looks for an empowering "
"implicate depending on the number of levels of unit propagation "
"allowed in the encoding. Denote the value of "
"emp-timeout-level-base as B and the value of "
"emp-timeout-level-factor as F. For a level L which is neither 0 "
"nor maximum (i.e. the number of variables), the timeout is set as "
"B+F*L. If the value is higher than emp-timeout, then the value of "
"emp-timeout is used instead. If the value is not positive, then it "
"is interpreted as infinity. The parameter value is passed as a "
"fractional number specifying the number of seconds.") //
("emp-timeout-level-factor",
po::value<long double>(&mEmpTimeouts.level_factor)
->default_value(0.0l, "0.0"),
"This parameter together with emp-timeout-level-base allows to set "
"the timeout for a single SAT which looks for an empowering "
"implicate depending on the number of levels of unit propagation "
"allowed in the encoding (see the description of "
"emp-timeout-level-base for more details).");
}
bool
SUBool::PCTimeoutsOptions::GetValues()
{
return true;
}
......@@ -338,4 +338,16 @@ SUBool::PCMinimizationOptions::NoLevelMinimize() const
{
return mNoLevelMinimize;
}
inline const SUBool::AbsCheckerSAT::Timeouts &
SUBool::PCTimeoutsOptions::EmpTimeouts() const
{
return mEmpTimeouts;
}
inline long double
SUBool::PCTimeoutsOptions::Timeout() const
{
return mTimeout;
}
#endif
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment