diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-15 09:12:07 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-15 09:12:07 -0700 |
commit | e6ccc68bc7b77de584777693aafc0c091bff7f41 (patch) | |
tree | b7e7b133524287aba7fda1cdda195df039f46e70 | |
parent | 552710a4111dbeef6bec6eb74bd4d8a6286797f2 (diff) | |
parent | 4a3bde6335f676a28f4aa5f872c213e0ec8bbaa7 (diff) |
Merge branch 'master' into fixGetUnsatAssumptDumpfixGetUnsatAssumptDump
-rw-r--r-- | config/cvc4.m4 | 15 | ||||
-rw-r--r-- | configure.ac | 22 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 1 |
3 files changed, 5 insertions, 33 deletions
diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 1b0e88098..c6d19a3ea 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -49,7 +49,7 @@ handle_option() { ;; -*|*=*) ;; - production|production-*|debug|debug-*|competition|competition-*) + production|production-*|debug|debug-*|competition|competition-*|testing|testing-*) # regexp `\?' not supported on Mac OS X ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'` ac_cvc4_build_profile_set=yes @@ -103,18 +103,7 @@ handle_option() { unset ac_cvc4_rewritten_args for ac_option do - if test "$ac_option" = personal; then - if test -e personal.conf; then - handle_option --enable-personal-make-rules - while read arg; do - handle_option "$arg" - done < personal.conf - else - AC_MSG_ERROR([personal build profile selected, but cannot find personal.conf]) - fi - else - handle_option "$ac_option" - fi + handle_option "$ac_option" done eval set x $ac_cvc4_rewritten_args shift diff --git a/configure.ac b/configure.ac index f802fa1c0..3eca4da99 100644 --- a/configure.ac +++ b/configure.ac @@ -112,7 +112,7 @@ fi AC_MSG_CHECKING([for requested build profile]) AC_ARG_WITH([build], [AS_HELP_STRING([--with-build=profile], - [for profile in {production,debug,competition,personal}])]) + [for profile in {production,debug,competition,testing}])]) if test -z "${with_build+set}"; then with_build=production @@ -532,7 +532,7 @@ case "$with_build" in if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi ;; - default) # moderately optimized, assertions, tracing, dumping + testing) # moderately optimized, assertions, tracing, dumping CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }" CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }" CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }" @@ -579,8 +579,8 @@ if test -z "${OPTLEVEL+set}"; then OPTLEVEL=3; fi AM_CONDITIONAL([CVC4_BUILD_PROFILE_PRODUCTION], [test "$with_build" = production]) AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEBUG], [test "$with_build" = debug]) -AM_CONDITIONAL([CVC4_BUILD_PROFILE_DEFAULT], [test "$with_build" = default]) AM_CONDITIONAL([CVC4_BUILD_PROFILE_COMPETITION], [test "$with_build" = competition]) +AM_CONDITIONAL([CVC4_BUILD_PROFILE_TESTING], [test "$with_build" = testing]) # permit a static binary AC_MSG_CHECKING([whether to build a static binary]) @@ -1012,22 +1012,6 @@ if test "$target_vendor" = apple; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-D_GLIBCXX_VISIBILITY_DEFAULT=\"__attribute__((__visibility__(\\\"default\\\")))\"" fi -# Tell top-level Makefile to include $(top_srcdir)/personal.mk -AC_ARG_ENABLE([personal-make-rules], - [AS_HELP_STRING([--enable-personal-make-rules], - [include top-level personal.mk (if it exists)])]) -if test "$enable_personal_make_rules" = yes; then - # This allows us to include a personal.mk makefile from every - # generated makefile. Named zz_* in order to make sure this - # comes last, so it gets other definitions (in particular top_srcdir). - zz_cvc4_use_personal_make_rules='yes - -all:; -include $(top_srcdir)/personal.mk -$(top_srcdir)/personal.mk:; @touch "$@"' - AC_SUBST([zz_cvc4_use_personal_make_rules]) -fi - # Doxygen configuration AC_ARG_ENABLE([internals-documentation], [AS_HELP_STRING([--enable-internals-documentation], diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 90928c0bc..8cb530a62 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -73,7 +73,6 @@ private: //fixed finite set range std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range; std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range; - void hasFreeVar( Node f, Node n ); void process( Node q, Node n, bool pol, std::map< Node, unsigned >& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, |