From 64868646eed7384c38db41aff5002215b92c1601 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Fri, 4 Oct 2013 18:32:55 +0100 Subject: MetaSMT builder, solver and command-line options. --- lib/Basic/CmdLineOptions.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'lib/Basic') diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index ac0474fb..1201ac29 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,5 +73,17 @@ llvm::cl::list queryLoggingOptions( llvm::cl::CommaSeparated ); + +llvm::cl::opt +UseMetaSMT("use-metasmt", + llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."), + llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"), + clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), + clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), + clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), + clEnumValEnd), + llvm::cl::init(METASMT_BACKEND_NONE)); + + } -- cgit 1.4.1