Skip to content

Commit

Permalink
Added a new tool for Minisat-compatible SAT solvers.
Browse files Browse the repository at this point in the history
  • Loading branch information
nafur committed Oct 9, 2019
1 parent 6fba4ac commit 8788001
Show file tree
Hide file tree
Showing 3 changed files with 40 additions and 0 deletions.
35 changes: 35 additions & 0 deletions src/benchmax/tools/Minisat.h
Original file line number Diff line number Diff line change
@@ -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";
}
};

}
3 changes: 3 additions & 0 deletions src/benchmax/tools/Tools.cpp
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
#include "Tools.h"

#include "MathSAT.h"
#include "Minisat.h"
#include "Minisatp.h"
#include "SMTRAT.h"
#include "SMTRAT_OPB.h"
Expand Down Expand Up @@ -38,6 +39,7 @@ Tools loadTools() {
Tools tools;
createTools<Tool>(settings_tools().tools_generic, tools);
createTools<MathSAT>(settings_tools().tools_mathsat, tools);
createTools<Minisat>(settings_tools().tools_minisat, tools);
createTools<Minisatp>(settings_tools().tools_minisatp, tools);
createTools<SMTRAT>(settings_tools().tools_smtrat, tools);
createTools<SMTRAT_OPB>(settings_tools().tools_smtrat_opb, tools);
Expand Down Expand Up @@ -69,6 +71,7 @@ void registerToolSettings(SettingsParser* parser) {
("statistics,s", po::bool_switch(&s.collect_statistics), "run tools with statistics")
("tool", po::value<std::vector<std::filesystem::path>>(&s.tools_generic), "a generic tool")
("mathsat", po::value<std::vector<std::filesystem::path>>(&s.tools_mathsat), "MathSAT with SMT-LIB interface")
("minisat", po::value<std::vector<std::filesystem::path>>(&s.tools_minisat), "Minisat with DIMACS interface")
("minisatp", po::value<std::vector<std::filesystem::path>>(&s.tools_minisatp), "Minisatp with OPB interface")
("smtrat,S", po::value<std::vector<std::filesystem::path>>(&s.tools_smtrat), "SMT-RAT with SMT-LIB interface")
("smtrat-opb,O", po::value<std::vector<std::filesystem::path>>(&s.tools_smtrat_opb), "SMT-RAT with OPB interface")
Expand Down
2 changes: 2 additions & 0 deletions src/benchmax/tools/Tools.h
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ struct ToolSettings {
std::vector<std::filesystem::path> tools_generic;
/// MathSAT with SMT-LIB interface.
std::vector<std::filesystem::path> tools_mathsat;
/// Minisat with DIMACS interface.
std::vector<std::filesystem::path> tools_minisat;
/// Minisatp with OPB interface.
std::vector<std::filesystem::path> tools_minisatp;
/// SMT-RAT with SMT-LIB interface.
Expand Down

0 comments on commit 8788001

Please sign in to comment.