diff options
| -rwxr-xr-x | .travis/klee.sh | 2 | ||||
| -rw-r--r-- | Makefile.config.in | 2 | ||||
| -rw-r--r-- | MetaSMT.mk | 2 | ||||
| -rw-r--r-- | autoconf/configure.ac | 42 | ||||
| -rwxr-xr-x | configure | 56 | ||||
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 24 |
6 files changed, 64 insertions, 64 deletions
diff --git a/.travis/klee.sh b/.travis/klee.sh index bb57f281..98dbbc0d 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -66,7 +66,7 @@ for solver in ${SOLVER_LIST}; do ;; metaSMT) echo "metaSMT" - KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-solver=${METASMT_DEFAULT}" + KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-backend=${METASMT_DEFAULT}" ;; *) echo "Unknown solver ${solver}" diff --git a/Makefile.config.in b/Makefile.config.in index d6eada4e..1b0b7ba8 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -35,7 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@ ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ -METASMT_DEFAULT_SOLVER := @METASMT_DEFAULT_SOLVER@ +METASMT_DEFAULT_BACKEND := @METASMT_DEFAULT_BACKEND@ ENABLE_Z3 := @ENABLE_Z3@ Z3_CFLAGS := @Z3_CFLAGS@ diff --git a/MetaSMT.mk b/MetaSMT.mk index 8733d9ec..817fa663 100644 --- a/MetaSMT.mk +++ b/MetaSMT.mk @@ -4,7 +4,7 @@ ifeq ($(ENABLE_METASMT),1) include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile LD.Flags += $(metaSMT_LDFLAGS) - CXX.Flags += -DMETASMT_DEFAULT_SOLVER_$(METASMT_DEFAULT_SOLVER) + CXX.Flags += -DMETASMT_DEFAULT_BACKEND_IS_$(METASMT_DEFAULT_BACKEND) CXX.Flags += $(metaSMT_CXXFLAGS) CXX.Flags += $(metaSMT_INCLUDES) CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 00143171..a08e190e 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -776,41 +776,41 @@ AC_SUBST(ENABLE_METASMT) dnl ************************************************************************** -dnl User option to specify the default solver of metaSMT +dnl User option to specify the default backend of metaSMT dnl ************************************************************************** -AC_ARG_WITH(metasmt-default-solver, - AS_HELP_STRING([--with-metasmt-default-solver], - [Default solver of metaSMT (btor|stp|z3, stp if unspecified)]),,) +AC_ARG_WITH(metasmt-default-backend, + AS_HELP_STRING([--with-metasmt-default-backend], + [Default backend of metaSMT (btor|stp|z3, stp if unspecified)]),,) -if test "X$with_metasmt_default_solver" != X ; then +if test "X$with_metasmt_default_backend" != X ; then if test "X$ENABLE_METASMT" != X1 ; then - AC_MSG_ERROR([--with-metasmt-default-solver requires metaSMT to be enabled]) + AC_MSG_ERROR([--with-metasmt-default-backend requires metaSMT to be enabled]) fi - if test "$with_metasmt_default_solver" == "btor" ; then - METASMT_DEFAULT_SOLVER=BTOR - AC_MSG_NOTICE([metaSMT uses Boolector as default solver]) + if test "$with_metasmt_default_backend" == "btor" ; then + METASMT_DEFAULT_BACKEND=BTOR + AC_MSG_NOTICE([metaSMT uses Boolector as default backend]) fi - if test "$with_metasmt_default_solver" == "z3" ; then - METASMT_DEFAULT_SOLVER=Z3 - AC_MSG_NOTICE([metaSMT uses Z3 as default solver]) + if test "$with_metasmt_default_backend" == "z3" ; then + METASMT_DEFAULT_BACKEND=Z3 + AC_MSG_NOTICE([metaSMT uses Z3 as default backend]) fi - if test "$with_metasmt_default_solver" == "stp" ; then - METASMT_DEFAULT_SOLVER=STP - AC_MSG_NOTICE([metaSMT uses STP as default solver]) + if test "$with_metasmt_default_backend" == "stp" ; then + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([metaSMT uses STP as default backend]) fi - if test "X$METASMT_DEFAULT_SOLVER" == X ; then - METASMT_DEFAULT_SOLVER=STP - AC_MSG_NOTICE([$with_metasmt_default_solver unsupported, metaSMT uses STP as default solver]) + if test "X$METASMT_DEFAULT_BACKEND" == X ; then + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([$with_metasmt_default_backend unsupported, metaSMT uses STP as default backend]) fi else if test "X$ENABLE_METASMT" == X1 ; then - METASMT_DEFAULT_SOLVER=STP - AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default solver]) + METASMT_DEFAULT_BACKEND=STP + AC_MSG_NOTICE([No solver specified, metaSMT uses STP as default backend]) fi fi -AC_SUBST(METASMT_DEFAULT_SOLVER) +AC_SUBST(METASMT_DEFAULT_BACKEND) dnl ************************************************************************** diff --git a/configure b/configure index 3c71aff4..7f1839c0 100755 --- a/configure +++ b/configure @@ -624,7 +624,7 @@ ac_includes_default="\ ac_subst_vars='LTLIBOBJS LIBOBJS -METASMT_DEFAULT_SOLVER +METASMT_DEFAULT_BACKEND ENABLE_METASMT METASMT_ROOT Z3_LDFLAGS @@ -740,7 +740,7 @@ with_tcmalloc with_stp with_z3 with_metasmt -with_metasmt_default_solver +with_metasmt_default_backend ' ac_precious_vars='build_alias host_alias @@ -1395,8 +1395,8 @@ Optional Packages: --with-stp Location of STP installation directory --with-z3 Location of Z3 installation directory --with-metasmt Location of metaSMT installation directory - --with-metasmt-default-solver - Default solver of metaSMT (btor|stp|z3, stp if + --with-metasmt-default-backend + Default backend of metaSMT (btor|stp|z3, stp if unspecified) Some influential environment variables: @@ -5398,41 +5398,41 @@ fi -# Check whether --with-metasmt-default-solver was given. -if test "${with_metasmt_default_solver+set}" = set; then : - withval=$with_metasmt_default_solver; +# Check whether --with-metasmt-default-backend was given. +if test "${with_metasmt_default_backend+set}" = set; then : + withval=$with_metasmt_default_backend; fi -if test "X$with_metasmt_default_solver" != X ; then +if test "X$with_metasmt_default_backend" != X ; then if test "X$ENABLE_METASMT" != X1 ; then - as_fn_error $? "--with-metasmt-default-solver requires metaSMT to be enabled" "$LINENO" 5 + as_fn_error $? "--with-metasmt-default-backend requires metaSMT to be enabled" "$LINENO" 5 fi - if test "$with_metasmt_default_solver" == "btor" ; then - METASMT_DEFAULT_SOLVER=BTOR - { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default solver" >&5 -$as_echo "$as_me: metaSMT uses Boolector as default solver" >&6;} + if test "$with_metasmt_default_backend" == "btor" ; then + METASMT_DEFAULT_BACKEND=BTOR + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Boolector as default backend" >&5 +$as_echo "$as_me: metaSMT uses Boolector as default backend" >&6;} fi - if test "$with_metasmt_default_solver" == "z3" ; then - METASMT_DEFAULT_SOLVER=Z3 - { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default solver" >&5 -$as_echo "$as_me: metaSMT uses Z3 as default solver" >&6;} + if test "$with_metasmt_default_backend" == "z3" ; then + METASMT_DEFAULT_BACKEND=Z3 + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses Z3 as default backend" >&5 +$as_echo "$as_me: metaSMT uses Z3 as default backend" >&6;} fi - if test "$with_metasmt_default_solver" == "stp" ; then - METASMT_DEFAULT_SOLVER=STP - { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default solver" >&5 -$as_echo "$as_me: metaSMT uses STP as default solver" >&6;} + if test "$with_metasmt_default_backend" == "stp" ; then + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: metaSMT uses STP as default backend" >&6;} fi - if test "X$METASMT_DEFAULT_SOLVER" == X ; then - METASMT_DEFAULT_SOLVER=STP - { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_solver unsupported, metaSMT uses STP as default solver" >&5 -$as_echo "$as_me: $with_metasmt_default_solver unsupported, metaSMT uses STP as default solver" >&6;} + if test "X$METASMT_DEFAULT_BACKEND" == X ; then + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: $with_metasmt_default_backend unsupported, metaSMT uses STP as default backend" >&6;} fi else if test "X$ENABLE_METASMT" == X1 ; then - METASMT_DEFAULT_SOLVER=STP - { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default solver" >&5 -$as_echo "$as_me: No solver specified, metaSMT uses STP as default solver" >&6;} + METASMT_DEFAULT_BACKEND=STP + { $as_echo "$as_me:${as_lineno-$LINENO}: No solver specified, metaSMT uses STP as default backend" >&5 +$as_echo "$as_me: No solver specified, metaSMT uses STP as default backend" >&6;} fi fi diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 7bff3437..20c190a5 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -84,30 +84,30 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( #ifdef ENABLE_METASMT -#ifdef METASMT_DEFAULT_SOLVER_BTOR -#define DEFAULT_METASMT_BACKEND_STR "(default = btor)." -#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_BOOLECTOR -#elif METASMT_DEFAULT_SOLVER_Z3 -#define DEFAULT_METASMT_BACKEND_STR "(default = z3)." -#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_Z3 +#ifdef METASMT_DEFAULT_BACKEND_IS_BTOR +#define METASMT_DEFAULT_BACKEND_STR "(default = btor)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_BOOLECTOR +#elif METASMT_DEFAULT_BACKEND_IS_Z3 +#define METASMT_DEFAULT_BACKEND_STR "(default = z3)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3 #else -#define DEFAULT_METASMT_BACKEND_STR "(default = stp)." -#define DEFAULT_METASMT_BACKEND METASMT_BACKEND_STP +#define METASMT_DEFAULT_BACKEND_STR "(default = stp)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP #endif llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend( "metasmt-backend", - llvm::cl::desc("Specify the MetaSMT solver backend type " DEFAULT_METASMT_BACKEND_STR), + llvm::cl::desc("Specify the MetaSMT solver backend type " METASMT_DEFAULT_BACKEND_STR), llvm::cl::values( 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(DEFAULT_METASMT_BACKEND)); + llvm::cl::init(METASMT_DEFAULT_BACKEND)); -#undef DEFAULT_METASMT_BACKEND -#undef DEFAULT_METASMT_BACKEND_STR +#undef METASMT_DEFAULT_BACKEND +#undef METASMT_DEFAULT_BACKEND_STR #endif /* ENABLE_METASMT */ |