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 <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