SmtCommandLine.h

// Command-line processing utilities related to SMT solvers
#ifndef ROSE_BinaryAnalysis_SmtCommandLine_H
#define ROSE_BinaryAnalysis_SmtCommandLine_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS
 
#include <Sawyer/CommandLine.h>
 
#include <iostream>
#include <string>
 
namespace Rose {
namespace BinaryAnalysis {
 
bool listSmtSolverNames(std::ostream&);
 
std::string validateSmtSolverName(const std::string &name);
 
std::string bestSmtSolverName();
 
void checkSmtCommandLineArg(const std::string &arg, const std::string &listSwitch, std::ostream &errorStream = std::cerr);
 
std::string smtSolverDocumentationString(const std::string &dfltSolver);
 
class SmtSolverValidator: public Sawyer::CommandLine::SwitchAction {
protected:
    SmtSolverValidator() {}
public:
    typedef Sawyer::SharedPointer<SmtSolverValidator> Ptr;
    static Ptr instance() { return Ptr(new SmtSolverValidator); }
protected:
    void operator()(const Sawyer::CommandLine::ParserResult&);
};
 
} // namespace
} // namespace
 
#endif
#endif