diff --git a/src/benchmax/tools/Minisat.h b/src/benchmax/tools/Minisat.h new file mode 100644 index 000000000..4f238aac5 --- /dev/null +++ b/src/benchmax/tools/Minisat.h @@ -0,0 +1,35 @@ +/** + * @file smtratSolverTool.h + * @author: Sebastian Junges + * + * + */ + +#pragma once + +#include "Tool.h" + +namespace benchmax { + +/** + * Tool wrapper for a Minisat solver. + */ +class Minisat: public Tool { +public: + /// Create tool. + Minisat(const fs::path& binary, const std::string& arguments): Tool("Minisat", binary, arguments) {} + + /// Only handles .opb files. + virtual bool canHandle(const fs::path& path) const override { + return is_extension(path, ".cnf") || is_extension(path, ".dimacs"); + } + + /// Parse results from stdout. + virtual void additionalResults(const fs::path&, BenchmarkResult& result) const override { + if (result.exitCode == 10) result.answer = "sat"; + else if (result.exitCode == 20) result.answer = "unsat"; + else result.answer = "unknown"; + } +}; + +} diff --git a/src/benchmax/tools/Tools.cpp b/src/benchmax/tools/Tools.cpp index f76649455..a5f2d0ac7 100644 --- a/src/benchmax/tools/Tools.cpp +++ b/src/benchmax/tools/Tools.cpp @@ -1,6 +1,7 @@ #include "Tools.h" #include "MathSAT.h" +#include "Minisat.h" #include "Minisatp.h" #include "SMTRAT.h" #include "SMTRAT_OPB.h" @@ -38,6 +39,7 @@ Tools loadTools() { Tools tools; createTools(settings_tools().tools_generic, tools); createTools(settings_tools().tools_mathsat, tools); + createTools(settings_tools().tools_minisat, tools); createTools(settings_tools().tools_minisatp, tools); createTools(settings_tools().tools_smtrat, tools); createTools(settings_tools().tools_smtrat_opb, tools); @@ -69,6 +71,7 @@ void registerToolSettings(SettingsParser* parser) { ("statistics,s", po::bool_switch(&s.collect_statistics), "run tools with statistics") ("tool", po::value>(&s.tools_generic), "a generic tool") ("mathsat", po::value>(&s.tools_mathsat), "MathSAT with SMT-LIB interface") + ("minisat", po::value>(&s.tools_minisat), "Minisat with DIMACS interface") ("minisatp", po::value>(&s.tools_minisatp), "Minisatp with OPB interface") ("smtrat,S", po::value>(&s.tools_smtrat), "SMT-RAT with SMT-LIB interface") ("smtrat-opb,O", po::value>(&s.tools_smtrat_opb), "SMT-RAT with OPB interface") diff --git a/src/benchmax/tools/Tools.h b/src/benchmax/tools/Tools.h index ccbe4ba90..ac92ccf05 100644 --- a/src/benchmax/tools/Tools.h +++ b/src/benchmax/tools/Tools.h @@ -35,6 +35,8 @@ struct ToolSettings { std::vector tools_generic; /// MathSAT with SMT-LIB interface. std::vector tools_mathsat; + /// Minisat with DIMACS interface. + std::vector tools_minisat; /// Minisatp with OPB interface. std::vector tools_minisatp; /// SMT-RAT with SMT-LIB interface.