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

pccheck output file

parent a2abfa5a
......@@ -39,7 +39,7 @@ const std::string prg_help =
struct config_t
{
std::string input_file{};
std::string output_file{};
std::string encoding_file{};
bool encode_only{false};
unsigned verbosity{3}; // 0 means no output
bool no_up_backbones{false};
......@@ -77,14 +77,13 @@ dump_config(const config_t &conf, unsigned level)
{
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.TLog(level) << "\tinput_file: " << conf.input_file << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.DumpVerbosity("\t", level);
SUBool::PCCheckGoalOptions::kGoalAnnotation.DumpValue(
"\t", level, "goal", conf.goal);
SUBool::logs.TLog(level)
<< "\tencode_only: " << SUBool::bool_to_string(conf.encode_only)
<< std::endl;
SUBool::logs.DumpValue("\t", level, "encoding_file", conf.encoding_file);
SUBool::logs.DumpValue("\t", level, "no_up_backbones", conf.no_up_backbones);
SUBool::kLitImplSystemAnnotation.DumpValue(
"\t", level, "impl_system", conf.impl_system);
......@@ -147,13 +146,19 @@ parse_arguments(int argc, char *argv[])
config_t conf;
SUBool::PrgOptions opts(true);
opts.SetHelpDesc(prg_help);
opts.InputOutput(&conf.input_file, &conf.output_file);
opts.SinglePositional({&conf.input_file, "input"});
auto goal_opts = opts.MakeOptionsGroup<SUBool::PCCheckGoalOptions>();
if (!opts.Parse(argc, argv))
{
return {};
}
conf.goal = goal_opts->Goal();
if (goal_opts->EncodeFile())
{
conf.encode_only = true;
conf.encoding_file = *(goal_opts->EncodeFile());
}
conf.enc_conf.use_backmap = goal_opts->Dump();
return conf;
#if 0
try
......@@ -455,11 +460,11 @@ encode(const config_t &conf, const SUBool::CompHypothesis &hyp,
}
}
enc->BuildEncoding(cnf, cl2lit, impl_system, scc_graph);
SUBool::OutputStream os(conf.output_file);
SUBool::OutputStream os(conf.encoding_file);
if (!os)
{
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
<< "[encode] Failed to open file '" << conf.output_file
<< "[encode] Failed to open file '" << conf.encoding_file
<< "' for writing" << std::endl;
return 2;
}
......
......@@ -300,6 +300,12 @@ SUBool::PCCheckGoalOptions::PCCheckGoalOptions()
kGoalAnnotation, "goal,g", "What should be checked", kDefaultGoal)
{
Add(mGoalOption);
AddOptions() //
("encode,e", po::value(&mEncodeFile),
"Do not check, just write the encoding to the given file.") //
("dump,d", po::bool_switch(&mDump),
"Dump the names of variables into the output file (given with -e "
"option).");
}
bool
......
......@@ -237,7 +237,9 @@ namespace SUBool
private:
EnumOption<GOAL> mGoalOption;
GOAL mGoal;
GOAL mGoal{kDefaultGoal};
bool mDump{false};
boost::optional<std::string> mEncodeFile{};
public:
PCCheckGoalOptions();
......@@ -245,6 +247,8 @@ namespace SUBool
virtual bool GetValues() override;
GOAL Goal() const;
bool Dump() const;
const boost::optional<std::string> &EncodeFile() const;
};
} // namespace SUBool
......@@ -381,4 +385,16 @@ SUBool::PCCheckGoalOptions::Goal() const
return mGoal;
}
inline bool
SUBool::PCCheckGoalOptions::Dump() const
{
return mDump;
}
inline const boost::optional<std::string> &
SUBool::PCCheckGoalOptions::EncodeFile() const
{
return mEncodeFile;
}
#endif
......@@ -2,7 +2,7 @@
TODO: Allow only input file, output file should be passed with -e option
General Options
Goal
-u, --uc Aim for unit refutation completeness instead
of propagation completeness.
......
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