diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp index 938167207..6e28ffccd 100644 --- a/CASC/Schedules.cpp +++ b/CASC/Schedules.cpp @@ -1568,18 +1568,18 @@ void Schedules::getCascSat2019Schedule(const Property& property, Schedule& quick void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick, Schedule& fallback) { switch (property.getSMTLIBLogic()) { - case SMT_AUFDTLIA: - case SMT_AUFDTLIRA: // Add new logic here even though probably not best schedule - case SMT_AUFDTNIRA: // Add new logic here even though probably not best schedule + case SMTLIBLogic::AUFDTLIA: + case SMTLIBLogic::AUFDTLIRA: // Add new logic here even though probably not best schedule + case SMTLIBLogic::AUFDTNIRA: // Add new logic here even though probably not best schedule quick.push("lrs+1010_5:4_afp=100000:afq=1.2:anc=none:cond=on:fsr=off:ile=on:irw=on:nm=64:nwc=1:stl=30:sac=on:sp=occurrence:urr=on_9"); quick.push("dis+11_5_add=large:afr=on:afp=10000:afq=1.2:anc=none:gs=on:gsem=on:ile=on:irw=on:lma=on:lwlo=on:nm=64:nwc=1:sas=z3:sos=all:sac=on:sp=reverse_arity:urr=on:updr=off_273"); quick.push("dis+1011_2:3_add=large:afr=on:afp=40000:afq=1.0:anc=none:br=off:cond=on:gs=on:gsem=on:ile=on:irw=on:lma=on:lwlo=on:nwc=1:sos=on:sac=on:sp=occurrence:tac=axiom:tar=off:urr=on:updr=off_264"); break; - case SMT_UFDTLIA: - case SMT_UFDTLIRA: // Add new logic here even though probably not best schedule - case SMT_UFDTNIA: - case SMT_UFDTNIRA: // Add new logic here even though probably not best schedule + case SMTLIBLogic::UFDTLIA: + case SMTLIBLogic::UFDTLIRA: // Add new logic here even though probably not best schedule + case SMTLIBLogic::UFDTNIA: + case SMTLIBLogic::UFDTNIRA: // Add new logic here even though probably not best schedule quick.push("dis+1011_2:3_add=large:afr=on:afp=40000:afq=1.0:anc=none:br=off:cond=on:gs=on:gsem=on:ile=on:irw=on:lma=on:lwlo=on:nwc=1:sos=on:sac=on:sp=occurrence:tac=axiom:tar=off:urr=on:updr=off_2"); quick.push("lrs+11_7_add=off:afr=on:afp=40000:afq=1.1:amm=off:anc=none:bsr=on:br=off:fde=unused:gs=on:gsem=on:inw=on:ile=on:irw=on:lma=on:nm=64:nwc=1:stl=30:sos=all:sac=on:urr=on:updr=off:uhcvi=on_5"); quick.push("dis+1004_1_add=off:afr=on:afp=1000:afq=1.1:amm=off:anc=none:bd=off:fde=none:gs=on:gsaa=from_current:gsem=on:ile=on:irw=on:lwlo=on:nm=64:newcnf=on:nwc=1:sas=z3:sp=occurrence:tac=light:tar=off:tha=off:thi=all:urr=on:uhcvi=on_6"); @@ -1588,7 +1588,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs+1011_3:1_ind=struct:newcnf=on:ile=on:irw=on:lma=on:lwlo=on:sac=on:updr=off_10"); break; - case SMT_UFDT: + case SMTLIBLogic::UFDT: quick.push("lrs+11_8:1_av=off:cond=on:fde=none:ile=on:nm=16:nwc=1.3:stl=30:sp=reverse_arity:urr=on:updr=off_135"); quick.push("ott+1003_14_av=off:fsr=off:fde=unused:ile=on:lcm=predicate:nm=0:newcnf=on:nwc=1:sp=occurrence:uhcvi=on_12"); quick.push("lrs+10_3:1_av=off:cond=on:fde=none:ile=on:lma=on:lwlo=on:nm=64:nwc=1:stl=30:sp=reverse_arity:tar=off:uhcvi=on_148"); @@ -1622,7 +1622,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs+10_5:1_av=off:fde=unused:ile=on:lwlo=on:nwc=1.1:stl=90:sp=occurrence:urr=on_343"); break; - case SMT_LIA: + case SMTLIBLogic::LIA: quick.push("dis+1011_8_afp=10000:afq=1.2:amm=sco:anc=none:bce=on:gs=on:gsem=off:ile=on:lma=on:nm=16:newcnf=on:nwc=2.5:sas=z3:sos=all:sac=on:sp=occurrence:updr=off_2"); quick.push("dis+11_3_afr=on:afp=4000:afq=2.0:amm=sco:anc=none:bce=on:cond=on:fsr=off:ile=on:lwlo=on:nm=64:newcnf=on:nwc=1:sas=z3:tha=off:thf=on_2"); quick.push("dis-2_4_add=large:afp=1000:afq=1.0:amm=sco:anc=none:bce=on:gs=on:inw=on:ile=on:lwlo=on:nm=64:newcnf=on:nwc=1:sas=z3:sos=all:sp=reverse_arity:tha=off:thi=all_13"); @@ -1631,7 +1631,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs-11_4:1_afp=4000:afq=2.0:anc=none:br=off:gs=on:lwlo=on:nm=64:nwc=3:stl=30:urr=on_1"); break; - case SMT_UFNIA: + case SMTLIBLogic::UFNIA: quick.push("lrs+11_5:4_av=off:gs=on:gsem=on:irw=on:lma=on:lwlo=on:nm=32:newcnf=on:nwc=1.3:stl=30:sp=reverse_arity:updr=off_63"); quick.push("ott+1010_7_av=off:fsr=off:fde=none:lma=on:nm=2:newcnf=on:nwc=1.3:sos=on:sp=reverse_arity:uhcvi=on_194"); quick.push("dis+1011_8_av=off:bd=off:bsr=on:bce=on:cond=on:fsr=off:fde=unused:ile=on:nm=64:nwc=1.1:sd=10:ss=axioms:st=1.5:sos=all:sp=reverse_arity:tha=off_569"); @@ -1691,13 +1691,13 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs+4_3:1_add=off:afp=1000:afq=2.0:anc=none:gs=on:gsem=on:ile=on:lma=on:nm=2:nwc=5:sas=z3:stl=30:sac=on:sp=occurrence:updr=off_8"); break; - case SMT_ALIA: + case SMTLIBLogic::ALIA: quick.push("lrs+2_4_add=off:afr=on:afp=40000:afq=1.0:amm=off:anc=none:bd=off:bce=on:fde=none:gs=on:gsem=on:lma=on:nm=64:newcnf=on:nwc=1.3:sas=z3:stl=30:tha=off:thi=strong:uwa=one_side_interpreted:urr=on:updr=off:uhcvi=on_3"); quick.push("ott-3_2:3_add=off:afr=on:afp=40000:afq=1.0:bsr=on:cond=fast:fsr=off:fde=none:gs=on:ile=on:lma=on:lwlo=on:nm=2:newcnf=on:nwc=1.2:nicw=on:sas=z3:sos=all:sp=reverse_arity:urr=ec_only:updr=off_44"); quick.push("lrs-1_128_aac=none:add=off:afp=40000:afq=1.0:amm=off:anc=none:fsr=off:inw=on:ile=on:lcm=reverse:lma=on:nm=16:nwc=10:sas=z3:stl=30:sac=on:updr=off_195"); break; - case SMT_UFLIA: + case SMTLIBLogic::UFLIA: quick.push("lrs-11_2:1_add=off:afr=on:afp=10000:afq=2.0:amm=sco:anc=none:inw=on:ile=on:irw=on:lcm=reverse:lma=on:nm=64:nwc=1.5:sas=z3:stl=30:sp=reverse_arity:urr=on_9"); quick.push("lrs-10_3_av=off:bs=unit_only:bsr=on:cond=on:fsr=off:fde=unused:gs=on:inw=on:irw=on:lma=on:nm=64:newcnf=on:nwc=1.2:sas=z3:stl=30:tha=off:urr=ec_only_42"); quick.push("lrs+1011_2:1_afr=on:afp=10000:afq=2.0:amm=off:gsp=on:gs=on:inw=on:ile=on:nm=2:nwc=1:sas=z3:stl=30:tha=off_296"); @@ -1806,12 +1806,12 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs+1011_3:2_add=large:afp=10000:afq=1.4:amm=sco:anc=none:cond=fast:fde=unused:gsp=on:gs=on:ile=on:irw=on:lma=on:nwc=1:stl=30:sac=on:tha=off:updr=off:uhcvi=on_118"); break; - case SMT_UFIDL: + case SMTLIBLogic::UFIDL: quick.push("dis+11_3_add=large:afp=100000:afq=1.4:amm=off:anc=none:fsr=off:gs=on:ile=on:irw=on:lma=on:nm=32:nwc=1:tha=off:updr=off_2"); quick.push("dis+10_3_afr=on:afp=1000:afq=1.0:anc=none:cond=on:fsr=off:gs=on:ile=on:irw=on:lwlo=on:nm=32:nwc=1:sos=all:sp=occurrence:urr=on_3"); break; - case SMT_LRA: + case SMTLIBLogic::LRA: quick.push("dis+1011_2:1_add=off:afp=40000:afq=1.1:amm=sco:anc=none:fsr=off:fde=unused:gsp=on:ile=on:irw=on:nm=64:newcnf=on:nwc=1.1:sas=z3:sos=all:sp=occurrence:updr=off:uhcvi=on_298"); quick.push("dis+4_5_av=off:cond=on:fsr=off:gs=on:gsem=on:ile=on:irw=on:lwlo=on:nm=6:nwc=1:sos=on:sp=reverse_arity:updr=off_5"); quick.push("ott+11_4_av=off:ile=on:lma=on:nm=64:nwc=1:sos=all:sp=occurrence:uwa=interpreted_only:updr=off:uhcvi=on_37"); @@ -1819,15 +1819,15 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("dis+11_2_add=large:afr=on:afp=1000:afq=1.1:anc=none:gs=on:gsaa=full_model:ile=on:irw=on:lma=on:nm=16:nwc=1:sas=z3:sos=on:sac=on:sp=occurrence:thi=strong:uhcvi=on_72"); break; - case SMT_NIA: + case SMTLIBLogic::NIA: quick.push("dis+11_10_add=off:afr=on:afp=100000:afq=1.2:amm=off:anc=none:cond=on:gs=on:gsem=on:inw=on:ile=on:irw=on:lma=on:nm=64:newcnf=on:nwc=10:sas=z3:sac=on:sp=reverse_arity_2"); break; - case SMT_UFLRA: + case SMTLIBLogic::UFLRA: quick.push("dis+11_4_afp=4000:afq=1.4:amm=sco:anc=none:gs=on:ile=on:lma=on:nm=64:nwc=1.7:sas=z3:sac=on:sp=occurrence_2"); break; - case SMT_NRA: + case SMTLIBLogic::NRA: quick.push("dis+1011_4:1_anc=none:cond=fast:fsr=off:gs=on:gsaa=full_model:gsem=off:ile=on:lma=on:lwlo=on:nm=64:nwc=1:sas=z3:sac=on:sp=occurrence_9"); quick.push("dis+11_2_add=large:afp=10000:afq=1.0:amm=sco:anc=none:gs=on:ile=on:lma=on:lwlo=on:nm=64:newcnf=on:nwc=1:sas=z3:sos=all:uwa=all:updr=off_2"); quick.push("dis+11_3_afr=on:afp=40000:afq=2.0:anc=none:fsr=off:gs=on:lma=on:nm=64:newcnf=on:nwc=1:nicw=on:sas=z3:sos=all:sac=on:sp=occurrence:urr=on_2"); @@ -1835,10 +1835,10 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("lrs+1011_3_add=large:afp=1000:afq=1.1:anc=none:cond=on:fsr=off:ile=on:irw=on:lma=on:nm=64:newcnf=on:nwc=1:nicw=on:sas=z3:stl=30:sos=all:sac=on_182"); break; - case SMT_ANIA: // a newcomer ANIA, let's put it next to ALL - case SMT_ALL: // Add ALL here as we don't currently have a schedule for it and this is better than just using fallback - case SMT_AUFLIA: - case SMT_AUFNIA: + case SMTLIBLogic::ANIA: // a newcomer ANIA, let's put it next to ALL + case SMTLIBLogic::ALL: // Add ALL here as we don't currently have a schedule for it and this is better than just using fallback + case SMTLIBLogic::AUFLIA: + case SMTLIBLogic::AUFNIA: quick.push("lrs+1011_1_add=off:afr=on:afp=1000:afq=1.1:amm=off:anc=none:br=off:bce=on:er=filter:gsp=on:gs=on:gsaa=full_model:inw=on:ile=on:nm=32:nwc=1.2:sas=z3:stl=30:uwa=one_side_constant:urr=on_7"); quick.push("dis+11_3_add=off:afp=1000:afq=2.0:amm=off:anc=none:fsr=off:gs=on:gsaa=full_model:inw=on:ile=on:lcm=predicate:lma=on:nm=6:nwc=1:sas=z3:sos=all:sp=occurrence:tha=off:uhcvi=on_13"); quick.push("fmb+10_1_av=off:fde=unused:ile=on:irw=on:lcm=predicate:lma=on:nm=16:nwc=1.7:sos=all:sp=reverse_arity_2"); @@ -1867,7 +1867,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick break; - case SMT_AUFNIRA: + case SMTLIBLogic::AUFNIRA: quick.push("dis+11_2_add=large:afp=1000:afq=1.1:anc=none:fsr=off:fde=none:ile=on:irw=on:lma=on:nm=64:nwc=1:sas=z3:sos=all:sac=on_5"); quick.push("lrs+10_8_afr=on:afp=4000:afq=1.1:amm=sco:anc=none:bsr=on:cond=on:gs=on:gsem=off:irw=on:lma=on:nm=64:newcnf=on:nwc=1:nicw=on:sas=z3:stl=30:sac=on:tha=off:urr=on:updr=off_2"); quick.push("dis+1002_5_add=large:afr=on:afp=4000:afq=1.4:amm=off:anc=none:fsr=off:gs=on:gsem=on:irw=on:lma=on:nm=64:newcnf=on:nwc=1:sos=all:sac=on:sp=occurrence:updr=off_6"); @@ -1890,7 +1890,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("ott+1004_8:1_afp=10000:afq=1.1:amm=sco:anc=none:bd=off:bsr=on:fde=unused:ile=on:nm=2:newcnf=on:nwc=1:nicw=on:sas=z3:sp=reverse_arity:tha=off:updr=off_146"); break; - case SMT_UF: + case SMTLIBLogic::UF: quick.push("lrs+11_5_av=off:cond=on:lma=on:nm=64:newcnf=on:nwc=1:stl=30:updr=off_22"); quick.push("fmb+10_1_av=off:fmbes=contour:fmbsr=1.5:ile=on:updr=off_28"); quick.push("dis+11_50_add=large:afp=10000:afq=1.2:anc=none:fsr=off:gs=on:gsem=off:ile=on:irw=on:nm=64:newcnf=on:nwc=1:sac=on_4"); @@ -1956,7 +1956,7 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("ott+1011_8:1_add=off:afr=on:afp=40000:afq=1.2:amm=off:anc=none:bd=off:fsr=off:ile=on:nm=64:newcnf=on:nwc=1.1:sas=z3:sp=reverse_arity:updr=off_55"); break; - case SMT_AUFLIRA: + case SMTLIBLogic::AUFLIRA: quick.push("lrs+1010_2_anc=none:fsr=off:gs=on:irw=on:newcnf=on:nwc=1:sas=z3:stl=30:sos=on:sp=occurrence:updr=off_4"); quick.push("lrs+1010_4_av=off:bd=off:bs=unit_only:bsr=on:gs=on:inw=on:ile=on:lma=on:newcnf=on:nwc=2.5:stl=30:sp=occurrence:updr=off_6"); quick.push("dis+2_3_add=off:afp=40000:afq=1.1:anc=none:cond=on:gs=on:inw=on:ile=on:lcm=reverse:nm=64:newcnf=on:nwc=1:sas=z3:sp=reverse_arity:tha=off:urr=on:updr=off_43"); @@ -1967,35 +1967,35 @@ void Schedules::getSmtcomp2018Schedule(const Property& property, Schedule& quick quick.push("dis+1011_32_aac=none:add=off:afr=on:afp=40000:afq=1.0:amm=sco:bs=on:bsr=on:br=off:fde=unused:gs=on:gsaa=full_model:ile=on:lcm=predicate:nm=6:newcnf=on:nwc=1.5:sas=z3:sos=all:sac=on:tha=off:thi=all:uwa=one_side_constant:urr=on_1"); break; - case SMT_QF_ABV: - case SMT_QF_ALIA: - case SMT_QF_ANIA: - case SMT_QF_AUFBV: - case SMT_QF_AUFLIA: - case SMT_QF_AUFNIA: - case SMT_QF_AX: - case SMT_QF_BV: - case SMT_QF_IDL: - case SMT_QF_LIA: - case SMT_QF_LIRA: - case SMT_QF_LRA: - case SMT_QF_NIA: - case SMT_QF_NIRA: - case SMT_QF_NRA: - case SMT_QF_RDL: - case SMT_QF_UF: - case SMT_QF_UFBV: - case SMT_QF_UFIDL: - case SMT_QF_UFLIA: - case SMT_QF_UFLRA: - case SMT_QF_UFNIA: - case SMT_QF_UFNRA: + case SMTLIBLogic::QF_ABV: + case SMTLIBLogic::QF_ALIA: + case SMTLIBLogic::QF_ANIA: + case SMTLIBLogic::QF_AUFBV: + case SMTLIBLogic::QF_AUFLIA: + case SMTLIBLogic::QF_AUFNIA: + case SMTLIBLogic::QF_AX: + case SMTLIBLogic::QF_BV: + case SMTLIBLogic::QF_IDL: + case SMTLIBLogic::QF_LIA: + case SMTLIBLogic::QF_LIRA: + case SMTLIBLogic::QF_LRA: + case SMTLIBLogic::QF_NIA: + case SMTLIBLogic::QF_NIRA: + case SMTLIBLogic::QF_NRA: + case SMTLIBLogic::QF_RDL: + case SMTLIBLogic::QF_UF: + case SMTLIBLogic::QF_UFBV: + case SMTLIBLogic::QF_UFIDL: + case SMTLIBLogic::QF_UFLIA: + case SMTLIBLogic::QF_UFLRA: + case SMTLIBLogic::QF_UFNIA: + case SMTLIBLogic::QF_UFNRA: throw UserErrorException("Kein Kinderspiel, Bruder, use Z3 for quantifier-free problems!"); - case SMT_BV: - case SMT_UFBV: + case SMTLIBLogic::BV: + case SMTLIBLogic::UFBV: throw UserErrorException("Sorry, we don't deal with bit-vectors!"); - case SMT_UNDEFINED: + case SMTLIBLogic::UNDEFINED: throw UserErrorException("This version cannot be used with this logic!"); } diff --git a/CMakeLists.txt b/CMakeLists.txt index 7e628cfaa..bebc93810 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -5,7 +5,6 @@ cmake_minimum_required (VERSION 3.14.0) project(Vampire) include(CheckIPOSupported) -include(CheckPIESupported) # require the compiler to use C++17 set(CMAKE_CXX_STANDARD 17) @@ -19,13 +18,15 @@ if(CMAKE_CXX_COMPILER_ID STREQUAL GNU OR CMAKE_CXX_COMPILER_ID MATCHES Clang$) add_compile_options(-fno-threadsafe-statics) # ...or RTTI add_compile_options(-fno-rtti) - # enable standards-compliant standard library with sized operator delete - add_compile_options(-fsized-deallocation) endif() # compile command database set(CMAKE_EXPORT_COMPILE_COMMANDS ON) +# we use threads, make sure we link the thread-support stuff +find_package(Threads REQUIRED) +link_libraries(Threads::Threads) + # variables for binary name, set later set(VAMPIRE_BINARY vampire) set(VAMPIRE_BINARY_BUILD) @@ -805,6 +806,7 @@ if(CMAKE_BUILD_TYPE STREQUAL Debug) add_compile_definitions(VDEBUG=1) elseif(CMAKE_BUILD_TYPE STREQUAL Release) add_compile_definitions(VDEBUG=0) + add_compile_definitions(NDEBUG) endif() # enable for time profiling @@ -838,28 +840,7 @@ if (NOT Z3_FOUND) else () message(STATUS "Found Z3 ${Z3_VERSION_STRING}") include_directories(${Z3_CXX_INCLUDE_DIRS}) - if(NOT BUILD_SHARED_LIBS AND Z3_FOUND AND CMAKE_CXX_COMPILER_ID STREQUAL GNU) - # https://stackoverflow.com/questions/58848694/gcc-whole-archive-recipe-for-static-linking-to-pthread-stopped-working-in-rec - message(STATUS "Adding workaround for gcc static linking against pthread") - link_libraries(${Z3_LIBRARIES} -pthread -Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive) - else() - link_libraries(${Z3_LIBRARIES}) - endif() - - # Z3 needs threads now - if (APPLE) - set(CMAKE_THREAD_LIBS_INIT "-lpthread") - set(CMAKE_HAVE_THREADS_LIBRARY 1) - set(CMAKE_USE_WIN32_THREADS_INIT 0) - set(CMAKE_USE_PTHREADS_INIT 1) - set(THREADS_PREFER_PTHREAD_FLAG ON) - else () - set(CMAKE_THREAD_PREFER_PTHREAD TRUE) - set(THREADS_PREFER_PTHREAD_FLAG TRUE) - find_package(Threads REQUIRED) - link_libraries(Threads::Threads) - endif () - + link_libraries(${Z3_LIBRARIES}) add_library(Z3 SHARED IMPORTED) set_property(TARGET Z3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY}) add_compile_definitions(VZ3=1) @@ -1004,24 +985,6 @@ if(CMAKE_BUILD_TYPE STREQUAL Release AND IPO) set_property(TARGET vampire PROPERTY INTERPROCEDURAL_OPTIMIZATION true) endif() -# do not generate position-independent code: -# 1. it has some overhead -# 2. it's used for ASLR, which isn't a huge concern for us and messes with our backtrace support -check_pie_supported(OUTPUT_VARIABLE PIE_ERROR LANGUAGES CXX) -if(NOT CMAKE_CXX_LINK_PIE_SUPPORTED) - message(STATUS "disabling position-independent code not supported, stack traces may be broken") - message(STATUS "${PIE_ERROR}") -endif() - -# FIXME this guard should not be necessary but is currently because of how we do static linking above -if(BUILD_SHARED_LIBS) - set_property(TARGET vampire PROPERTY POSITION_INDEPENDENT_CODE false) - if(COMPILE_TESTS) - set_property(TARGET vtest PROPERTY POSITION_INDEPENDENT_CODE false) - endif() -endif() - - ################################################################ # subsat (standalone version of the SAT solver used for subsumption and subsumption resolution) ################################################################ diff --git a/Debug/Assertion.cpp b/Debug/Assertion.cpp index d74bfa7c8..ee5dc39c4 100644 --- a/Debug/Assertion.cpp +++ b/Debug/Assertion.cpp @@ -46,7 +46,7 @@ void Assertion::violated(const char* file, int line, const char* cond) << " violated:\n" << cond << "\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----" << std::endl; } abortAfterViolation(); @@ -62,7 +62,7 @@ void Assertion::violatedStrEquality(const char* file, int line, const char* val1 << val1Str << " == \"" << val1 << "\"\n" << val2Str << " == \"" << val2 << "\"\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); diff --git a/Debug/Assertion.hpp b/Debug/Assertion.hpp index 22524dedb..1a3ba3653 100644 --- a/Debug/Assertion.hpp +++ b/Debug/Assertion.hpp @@ -238,7 +238,7 @@ void Debug::Assertion::violated(const char* file, int line, const char* cond, << cond << "\n" << "Value of " << repStr << " is: " << rep << "\n----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); @@ -255,7 +255,7 @@ void Debug::Assertion::violated(const char* file, int line, const char* cond, << "Value of " << repStr << " is: " << rep << "\n" << "Value of " << repStr2 << " is: " << rep2 << "\n----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); @@ -271,7 +271,7 @@ void Debug::Assertion::violatedEquality(const char* file, int line, const char* << val1Str << " == " << val1 << "\n" << val2Str << " == " << val2 << "\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); @@ -287,7 +287,7 @@ void Debug::Assertion::violatedNonequality(const char* file, int line, const cha << val1Str << " == " << val1 << "\n" << val2Str << " == " << val2 << "\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); @@ -319,7 +319,7 @@ void Debug::Assertion::violatedComparison(const char* file, int line, const char << val1Str << " == " << val1 << "\n" << val2Str << " == " << val2 << "\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); @@ -334,7 +334,7 @@ void Debug::Assertion::violatedMethod(const char* file, int line, const T& obj, << file << ", line " << line << " was violated for:\n" << objStr << " == " << obj << "\n" << "----- stack dump -----\n"; - Tracer::printStack(std::cout); + Tracer::printStack(); std::cout << "----- end of stack dump -----\n"; } abortAfterViolation(); diff --git a/Debug/Tracer.cpp b/Debug/Tracer.cpp index d063b45c3..3fe06d980 100644 --- a/Debug/Tracer.cpp +++ b/Debug/Tracer.cpp @@ -17,70 +17,66 @@ * * @since 01/05/2002 Manchester * @since 25/12/2023 Mísečky invoke system binary for backtrace + * @since 25/07/2024 Oxford invoke debugger for general sanity */ -#if __has_include() -#include -#define HAVE_EXECINFO -#endif - +#include #include #include +// for getpid() +// TODO compile guards for this and similar headers +#include + #include "Tracer.hpp" -#include "Lib/System.hpp" #include "Lib/Environment.hpp" +#include "Lib/System.hpp" #include "Shell/Options.hpp" // define in version.cpp.in extern const char* VERSION_STRING; -// if we have a callstack, the maximum number to actually retrieve -const unsigned MAX_CALLS = 1024; +// try and invoke the GNU debugger in batch mode on this process +static bool try_gdb(pid_t pid) { + std::stringstream command; + command + // ask for a traceback in batch mode + << "gdb --batch -ex bt --pid=" + << pid; + std::cout << command.str() << '\n'; + return std::system(command.str().c_str()) == 0; +} + +// try and invoke the LLVM debugger in batch mode on this process +static bool try_lldb(pid_t pid) { + std::stringstream command; + command + // ask for a traceback in batch mode + << "lldb --batch -o bt " + //<< argv0 + << " --attach-pid " + << pid; + std::cout << command.str() << '\n'; + return std::system(command.str().c_str()) == 0; +} /** - * Print the stack. + * Print the stack if --traceback on * @since 24/10/2002 Manchester * @since 12/7/2023 using platform-specific calls to get the stack trace */ -void Debug::Tracer::printStack(std::ostream& str) { - str << "Version : " << VERSION_STRING << "\n"; - -#ifdef HAVE_EXECINFO - void *call_stack[MAX_CALLS]; - int sz = ::backtrace(call_stack, MAX_CALLS); - str << "call stack:"; - for(int i = 0; i < sz; i++) - str << ' ' << call_stack[sz - (i + 1)]; - str << std::endl; - - if (env.options->traceback()) { -// UNIX-like systems, including BSD and Linux but not MacOS -#if defined(__unix__) - str << "invoking addr2line(1) ..." << std::endl; - std::stringstream out; - out << "addr2line -Cfe " << Lib::System::getArgv0(); - for(int i = 0; i < sz; i++) - out << ' ' << call_stack[sz - (i + 1)]; - std::system(out.str().c_str()); -// Apple things -#elif defined(__APPLE__) - str << "invoking atos(1) ..." << std::endl; - std::stringstream out; - out << "atos -o " << Lib::System::getArgv0(); - for(int i = 0; i < sz; i++) - out << ' ' << call_stack[sz - (i + 1)]; - std::system(out.str().c_str()); -#else - // TODO symbol lookup support for other platforms - str << "no symbol lookup support for this platform yet" << std::endl; -#endif +void Debug::Tracer::printStack() { + std::cout << "Version : " << VERSION_STRING << "\n"; + if(env.options->traceback()) { + pid_t pid = getpid(); + // is your favourite debugger not here? add it! + if(!try_gdb(pid) && !try_lldb(pid)) + std::cout << "(neither GDB nor LLDB worked: perhaps you need to install one of them?)\n"; } else - str << "(use '--traceback on' to get a human-readable stack trace)" << std::endl; + std::cout << "(use '--traceback on' to invoke a debugger and get a human-readable stack trace)\n"; -#else - // TODO backtrace support for other platforms - str << "no call stack support for this platform yet" << std::endl; -#endif -} // Tracer::printStack (ostream& str) + // usually causes debuggers to break here + // if not under a debugger, ignored + std::raise(SIGTRAP); +} diff --git a/Debug/Tracer.hpp b/Debug/Tracer.hpp index 013f3df3b..d0e90fbcb 100644 --- a/Debug/Tracer.hpp +++ b/Debug/Tracer.hpp @@ -27,8 +27,8 @@ namespace Debug { namespace Tracer { - // print the current stack - void printStack(std::ostream &out); + // print the current stack to stdout + void printStack(); }; template diff --git a/FMB/FiniteModelBuilder.cpp b/FMB/FiniteModelBuilder.cpp index e25381e9d..62770718a 100644 --- a/FMB/FiniteModelBuilder.cpp +++ b/FMB/FiniteModelBuilder.cpp @@ -40,7 +40,6 @@ #include "Lib/List.hpp" #include "Lib/Stack.hpp" #include "Lib/System.hpp" -#include "Lib/Sort.hpp" #include "Lib/Random.hpp" #include "Lib/DHSet.hpp" #include "Lib/ArrayMap.hpp" @@ -298,11 +297,11 @@ bool FiniteModelBuilder::reset(){ // Compare function symbols by their usage in the problem struct FMBSymmetryFunctionComparator { - static Comparison compare(unsigned f1, unsigned f2) + static bool compare(unsigned f1, unsigned f2) { unsigned c1 = env.signature->getFunction(f1)->usageCnt(); unsigned c2 = env.signature->getFunction(f2)->usageCnt(); - return Int::compare(c2,c1); + return c2 < c1; } }; @@ -764,8 +763,8 @@ void FiniteModelBuilder::init() for(unsigned s=0;s<_sortedSignature->sorts;s++){ Stack sortedConstants = _sortedSignature->sortedConstants[s]; Stack sortedFunctions = _sortedSignature->sortedFunctions[s]; - sort(sortedConstants.begin(),sortedConstants.end()); - sort(sortedFunctions.begin(),sortedFunctions.end()); + sort(sortedConstants.begin(),sortedConstants.end(), FMBSymmetryFunctionComparator::compare); + sort(sortedFunctions.begin(),sortedFunctions.end(), FMBSymmetryFunctionComparator::compare); } } } @@ -2603,7 +2602,7 @@ void FiniteModelBuilder::SmtBasedDSAE::reportZ3OutOfMemory() if(env.statistics) { env.statistics->print(std::cout); } - Debug::Tracer::printStack(std::cout); + Debug::Tracer::printStack(); System::terminateImmediately(1); } diff --git a/Kernel/InferenceStore.cpp b/Kernel/InferenceStore.cpp index f88e2ab51..fc79f1ed4 100644 --- a/Kernel/InferenceStore.cpp +++ b/Kernel/InferenceStore.cpp @@ -21,7 +21,6 @@ #include "Lib/Stack.hpp" #include "Lib/StringUtils.hpp" #include "Lib/ScopedPtr.hpp" -#include "Lib/Sort.hpp" #include "Shell/LaTeX.hpp" #include "Shell/Options.hpp" @@ -184,14 +183,6 @@ std::string getQuantifiedStr(Unit* u, List* nonQuantified=0) return getQuantifiedStr(vars, res, t_map); } -struct UnitNumberComparator -{ - static Comparison compare(Unit* u1, Unit* u2) - { - return Int::compare(u1->number(), u2->number()); - } -}; - struct InferenceStore::ProofPrinter { ProofPrinter(ostream& out, InferenceStore* is) @@ -290,7 +281,10 @@ struct InferenceStore::ProofPrinter void printDelayed() { // Sort - sort(delayed.begin(),delayed.end()); + sort( + delayed.begin(), delayed.end(), + [](Unit *u1, Unit *u2) -> bool { return u1->number() < u2->number(); } + ); // Print for(unsigned i=0;i -#include +#include +#include #include "Allocator.hpp" -#include -#include - -#ifdef __APPLE__ -#include -#endif - #ifndef INDIVIDUAL_ALLOCATIONS Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR; #endif -static size_t ALLOCATED = 0; -// set by main very soon after launch -static size_t LIMIT = std::numeric_limits::max(); - -size_t Lib::getUsedMemory() { return ALLOCATED; } -size_t Lib::getMemoryLimit() { return LIMIT; } -void Lib::setMemoryLimit(size_t limit) { LIMIT = limit; } - -// override global allocators to keep track of allocated memory, doing very little else -// TODO does not support get_new_handler/set_new_handler as we don't use it, but we could -void *operator new(size_t size, std::align_val_t align_val) { - size_t align = static_cast(align_val); - // standard says `size` must be an integer multiple of `align` - ASS_EQ(size % align, 0) - - if(ALLOCATED + size > LIMIT) - throw std::bad_alloc(); - ALLOCATED += size; - { -// aligned_alloc is not supported prior to macOS 10.13 -#if !defined(__APPLE__) || (defined(__APPLE__) && MAC_OS_X_VERSION_MIN_REQUIRED >= 101300) - if(void *ptr = std::aligned_alloc(align, size)) - return ptr; +#if __has_include() +#include +#define HAVE_RLIMIT #endif - // we might be here because `aligned_alloc` is finicky (Apple, looking at you) - // so try again with `malloc` and hope for good alignment - if(void *ptr = std::malloc(size)) - return ptr; +const size_t MIN_MEMORY = 20971520; - } - // no, we're actually out of memory - throw std::bad_alloc(); -} +void Lib::setMemoryLimit(size_t limit) { + // if limit is less than floor, ignore it + if(limit < MIN_MEMORY) + return; -// a version of the above operator-new without alignment information -void *operator new(size_t size) { - if(ALLOCATED + size > LIMIT) - throw std::bad_alloc(); - ALLOCATED += size; - { - if(void *ptr = std::malloc(size)) - return ptr; +#ifdef HAVE_RLIMIT + struct rlimit rlimit; + rlimit.rlim_cur = rlimit.rlim_max = limit; + if (setrlimit(RLIMIT_DATA, &rlimit) != 0) { +#if defined(__APPLE__) && defined(__MACH__) + if (errno != EINVAL) // silence buggy failure on OSX +#endif + std::perror("memory limiting failed"); } - throw std::bad_alloc(); -} - -// normal delete, just decrements `ALLOCATED` and calls free() -void operator delete(void *ptr, size_t size) noexcept { - ASS_GE(ALLOCATED, size) - ALLOCATED -= size; - std::free(ptr); -} -// aligned-and-sized delete -// forwards to the sized delete as we don't use the alignment information -void operator delete(void *ptr, size_t size, std::align_val_t align) noexcept { - operator delete(ptr, size); -} - -// unsized (and unaligned) delete -// called if we don't know the size of the deallocated object somehow, -// occurs very rarely and usually from deep in the bowels of the standard library -// TODO does cause us to slightly over-report allocated memory -void operator delete(void *ptr) noexcept { - std::free(ptr); +#else + // TODO should we warn here? +#endif } diff --git a/Lib/Allocator.hpp b/Lib/Allocator.hpp index 45e262159..4d1e09492 100644 --- a/Lib/Allocator.hpp +++ b/Lib/Allocator.hpp @@ -24,7 +24,6 @@ #include #include "Debug/Assertion.hpp" -#include "Portability.hpp" /* * uncomment the following to use Valgrind more profitably @@ -34,25 +33,18 @@ // #define INDIVIDUAL_ALLOCATIONS namespace Lib { - -// get the amount of memory used by global operator new so far -size_t getUsedMemory(); - -// get the memory limit for global operator new -size_t getMemoryLimit(); -// set the memory limit for global operator new +// attempt to set a memory limit for this process by system call void setMemoryLimit(size_t bytes); - } #ifdef INDIVIDUAL_ALLOCATIONS namespace Lib { inline void *alloc(size_t size, size_t align = alignof(std::max_align_t)) { - return ::operator new(size, (std::max_align_t)align); + return ::operator new(size, (std::align_val_t)align); } inline void free(void *pointer, size_t size, size_t align = alignof(std::max_align_t)) { - ::operator delete(pointer); + ::operator delete(pointer, (std::align_val_t)align); } } // namespace Lib #define USE_GLOBAL_SMALL_OBJECT_ALLOCATOR(C) @@ -215,7 +207,7 @@ class SmallObjectAllocator { if(size <= 8 * sizeof(void *)) return FSA8.free(pointer); - ::operator delete(pointer, size, (std::align_val_t)align); + ::operator delete(pointer, (std::align_val_t)align); } private: diff --git a/Lib/SharedSet.hpp b/Lib/SharedSet.hpp index 1da5338d7..5f7669169 100644 --- a/Lib/SharedSet.hpp +++ b/Lib/SharedSet.hpp @@ -360,7 +360,10 @@ class SharedSet { } } if(!sorted) { - sort(is.begin(), is.end()); + std::sort( + is.begin(), is.end(), + [](const T &l, const T &r) -> bool { return DefaultComparator::compare(l, r) == LESS; } + ); unique = false; //maybe they are unique, we just need to check } if(!unique) { diff --git a/Lib/Sort.hpp b/Lib/Sort.hpp index e15b08577..a582b03e3 100644 --- a/Lib/Sort.hpp +++ b/Lib/Sort.hpp @@ -17,13 +17,11 @@ #ifndef __Sort__ -# define __Sort__ +#define __Sort__ +#include "Comparison.hpp" #include "Debug/Assertion.hpp" -#include "Allocator.hpp" -#include "DArray.hpp" - namespace Lib { /** A type level predicate that tells whether there is a function `Result T::compare(T const&) const;` for some result type Result. o @@ -70,282 +68,6 @@ struct DefaultComparator } }; -template -void sort(C* first, C* afterLast) -{ - //modified sorting code, that was originally in Resolution::Tautology::sort - - C* arr=first; - size_t size=afterLast-first; - if(size<=1) { - //nothing to sort - return; - } - - // array behaves as a stack of calls to quicksort - static DArray ft(32); - - size_t from = 0; - size_t to=size-1; - ft.ensure(to); - - size_t p = 0; // pointer to the next element in ft - for (;;) { - ASS(from= 0); - from = ft[p]; - to = ft[p+1]; - continue; - } - return; - } -} - -/** - * A template class to sort data. The type ToCompare is the - * type of elements to sort. The type Comparator is the class that - * contains a function bool lessThan(ToCompare, ToCompare). - * A typical work with this class is as follows: - * - *
    - *
  1. a comparator c and an element s of the class Sort are created;
    2. - *
  2. elements of the class ToCompare are added one by one;
    3. - *
  3. s.sort() is called
    4. - *
  4. the resulting sorted collection is read.
    5. - *
- * @since 16/07/2003 flight Moscow-London, changed from a - * previous one-type version. - * @since 03/04/2004 Torrevieja, changed to use a comparator instead of - * a static function - */ -template -class Sort -{ - public: - /** - * Initialize the sort element. - * - * @param length the number of elements to sort - * @param comparator object used for comparison - */ - Sort (int length,Comparator& comparator) - : - _size(length), - _length(0), - _comparator(comparator) - { - void* mem = ALLOC_KNOWN(length*sizeof(ToCompare),"Sort<>"); - _elems = array_new(mem, length); - } - - inline ~Sort () - { - array_delete(_elems,_size); - DEALLOC_KNOWN(_elems,_size*sizeof(ToCompare),"Sort<>"); - } - - /** - * Return the length (the number of elements to sort) - */ - inline int length () const { return _length; } - - /** - * Return the nth element, used to retrieve sorted elements - */ - inline ToCompare operator [] (int n) const - { - ASS(n < _length); - return _elems[n]; - } // Sort::operator [] - - /** - * Add an element to sort. - * - * @param elem the element. - */ - inline void add (ToCompare elem) - { - ASS(_length < _size); - - _elems[_length++] = elem; - } // Sort::add - - /** - * Sort elements. - */ - inline void sort () - { - sort (0,_length-1); - } - - /** - * Check membership in the sorted list. Membership is checked using - * == for equality. - * - * @return true if elem is the member of Sort - * @since 17/07/2003 Manchester, changed to the new two-argument Sort class - */ - inline bool member (const ToCompare elem) const { - return member (elem,0,_length-1); - } - - protected: // structure - /** array of elements */ - ToCompare* _elems; - /** capacity */ - int _size; - /** the number of elements */ - int _length; - /** object used to compare elements */ - Comparator& _comparator; - - /** - * Quicksort elements between, and including indexes p and r, was taken - * from the Rivest et al. book - never use this book for practical - * algorithms :) - * @since 16/04/2006 Bellevue, improved: the algorithm sometimes - * compared elements with themselves - * @since 27/06/2008 Manchester, replaced since the old one was showing - * quadratic behaviour - */ - void sort(int p,int r) - { - ASS(r < _length); - - if (p >= r) { - return; - } - int m = (p+r)/2; - int i = p; - int j = r; - ToCompare a = _elems[m]; - while (i < m) { - ToCompare b = _elems[i]; - if (! _comparator.lessThan(a,b)) { // a[i] <= a[m] - i++; - continue; - } - if (m < j) { - _elems[i] = _elems[j]; - _elems[j] = b; - j--; - continue; - } - _elems[m] = b; - _elems[i] = _elems[m-1]; - m--; - j--; - } - while (m < j) { - ToCompare b = _elems[j]; - if (! _comparator.lessThan(b,a)) { // a[m] <= a[j] - j--; - continue; - } - _elems[m] = b; - _elems[j] = _elems[m+1]; - m++; - } - _elems[m] = a; - sort(p,m-1); - sort(m+1,r); - } // sort - - /** - * Check membership in the sorted list between the indexes fst - * and snd. Membership is checked using == for equality. The function - * works correctly only if lessThan is a total order. - * - * @return true if elem is the member of Sort[fst] ... Sort[snd] - * @since 17/07/2003 Manchester, changed to the new two-argument Sort class - */ - bool member (const ToCompare elem, int fst, int lst) const - { - for (;;) { - if (fst > lst) { - return false; - } - - int mid = (fst + lst) / 2; - - if (_elems[mid] == elem) { - return true; - } - - if (_comparator.lessThan(_elems[mid],elem)) { - lst = mid-1; - } - else { // _elems[mid] > c - fst = mid+1; - } - } - } // Sort::member -}; // class Sort - } // namespace Lib #endif diff --git a/Lib/System.cpp b/Lib/System.cpp index 98ad5a95e..dd71d6d8d 100644 --- a/Lib/System.cpp +++ b/Lib/System.cpp @@ -17,10 +17,6 @@ #include -// TODO these should probably be guarded -// for getpid -#include - #ifdef __linux__ #include #endif @@ -37,8 +33,6 @@ namespace Lib { -const char* System::s_argv0 = 0; - const char* signalToString (int sigNum) { switch (sigNum) @@ -108,7 +102,6 @@ void handleSignal (int sigNum) #ifndef _MSC_VER case SIGQUIT: case SIGBUS: - case SIGTRAP: #endif // following is not standards-compliant as it calls functions that are not permitted in signal handlers // but we're dying anyway, so try our best to report something @@ -123,7 +116,7 @@ void handleSignal (int sigNum) if (!Shell::UIHelper::portfolioParent) { if(env.statistics) env.statistics->print(std::cout); - Debug::Tracer::printStack(std::cout); + Debug::Tracer::printStack(); } System::terminateImmediately(VAMP_RESULT_STATUS_OTHER_SIGNAL); } diff --git a/Lib/System.hpp b/Lib/System.hpp index ae5ce876e..199b12e8a 100644 --- a/Lib/System.hpp +++ b/Lib/System.hpp @@ -38,16 +38,6 @@ class System { } static void registerForSIGHUPOnParentDeath(); - - /** - * Register the value of the argv[0] argument of the main function, so that - * it can be later used to determine the executable directory - */ - static void registerArgv0(const char* argv0) { s_argv0 = argv0; } - static const char *getArgv0() { return s_argv0; } - -private: - static const char* s_argv0; }; } diff --git a/Makefile b/Makefile index e79fe013f..50f0ba2c5 100644 --- a/Makefile +++ b/Makefile @@ -23,21 +23,15 @@ # CHECK_LEAKS - test for memory leaks (debugging mode only) # VZ3 - compile with Z3 -COMPILE_ONLY = -fno-pie +COMMON_FLAGS = -DVTIME_PROFILING=0 -OS = $(shell uname) -ifeq ($(OS),Darwin) -LINK_ONLY = -Wl,-no_pie -else -LINK_ONLY = -no-pie -endif +DBG_FLAGS = $(COMMON_FLAGS) -g -DVDEBUG=1 -DCHECK_LEAKS=0 # debugging for spider +REL_FLAGS = $(COMMON_FLAGS) -O3 -DVDEBUG=0 -DNDEBUG # no debugging -DBG_FLAGS = -fsized-deallocation -g -DVTIME_PROFILING=0 -DVDEBUG=1 -DCHECK_LEAKS=0 # debugging for spider -REL_FLAGS = -fsized-deallocation -O3 -DVTIME_PROFILING=0 -DVDEBUG=0 -D NDEBUG # no debugging GCOV_FLAGS = -O0 --coverage #-pedantic -MINISAT_DBG_FLAGS = -D DEBUG -MINISAT_REL_FLAGS = -D NDEBUG +MINISAT_DBG_FLAGS = -DDEBUG +MINISAT_REL_FLAGS = -DNDEBUG MINISAT_FLAGS = $(MINISAT_DBG_FLAGS) #XFLAGS = -g -DVDEBUG=1 -DVTEST=1 -DCHECK_LEAKS=1 # full debugging + testing @@ -86,14 +80,13 @@ XFLAGS = -Wfatal-errors -g -DVDEBUG=1 -DCHECK_LEAKS=0 -DUSE_SYSTEM_ALLOCATION=1 INCLUDES= -I. Z3FLAG= -DVZ3=0 Z3LIB= -ifeq (,$(shell echo $(MAKECMDGOALS) | sed 's/.*z3.*//g')) -INCLUDES= -I. -Iz3/src/api -Iz3/src/api/c++ -ifeq (,$(shell echo $(MAKECMDGOALS) | sed 's/.*static.*//g')) -Z3LIB= -Lz3/build -lz3 -lgomp -pthread -Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive -ldl -else +ifeq (,$(shell echo $(MAKECMDGOALS) | sed 's/.*z3.*//g')) +INCLUDES= -I. -Iz3/src/api -Iz3/src/api/c++ +# ifeq (,$(shell echo $(MAKECMDGOALS) | sed 's/.*static.*//g')) +# Z3LIB= -Lz3/build -lz3 -lgomp -pthread -Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive -ldl +# else Z3LIB= -Lz3/build -lz3 -endif - +# endif Z3FLAG= -DVZ3=1 endif @@ -527,15 +520,15 @@ obj/%X: | obj $(CONF_ID)/%.o : %.cpp | $(CONF_ID) mkdir -p `dirname $@` - $(CXX) $(CXXFLAGS) $(COMPILE_ONLY) -c -o $@ $*.cpp -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -MMD -MF $(CONF_ID)/$*.d + $(CXX) $(CXXFLAGS) -c -o $@ $*.cpp -MMD -MF $(CONF_ID)/$*.d %.o : %.c $(CONF_ID)/%.o : %.c | $(CONF_ID) - $(CC) $(CCFLAGS) $(COMPILE_ONLY) -c -o $@ $*.c -MMD -MF $(CONF_ID)/$*.d + $(CC) $(CCFLAGS) -c -o $@ $*.c -MMD -MF $(CONF_ID)/$*.d %.o : %.cc $(CONF_ID)/%.o : %.cc | $(CONF_ID) - $(CXX) $(CXXFLAGS) $(COMPILE_ONLY) -c -o $@ $*.cc $(MINISAT_FLAGS) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -MMD -MF $(CONF_ID)/$*.d + $(CXX) $(CXXFLAGS) -c -o $@ $*.cc $(MINISAT_FLAGS) -MMD -MF $(CONF_ID)/$*.d ################################################################ # targets for executables @@ -547,7 +540,7 @@ VSAT_OBJ := $(addprefix $(CONF_ID)/, $(VSAT_DEP)) TKV_OBJ := $(addprefix $(CONF_ID)/, $(TKV_DEP)) define COMPILE_CMD -$(CXX) $(CXXFLAGS) $(LINK_ONLY) $(filter -l%, $+) $(filter %.o, $^) -o $@_$(BRANCH)_$(COM_CNT) $(Z3LIB) +$(CXX) $(CXXFLAGS) $(filter -l%, $+) $(filter %.o, $^) -o $@_$(BRANCH)_$(COM_CNT) $(Z3LIB) @#$(CXX) -static $(CXXFLAGS) $(Z3LIB) $(filter %.o, $^) -o $@ @#strip $@ endef @@ -585,7 +578,7 @@ compile_commands: compile_commands/%.o: compile_commands mkdir -p $(dir $@) - echo $(CXX) $(CXXFLAGS) -c $*.cpp -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -MMD -MF $(CONF_ID)/$*.d > $@ + echo $(CXX) $(CXXFLAGS) -c $*.cpp -MMD -MF $(CONF_ID)/$*.d > $@ compile_commands.json: $(foreach x, $(VAMPIRE_DEP), compile_commands/$x) echo '[' > $@ diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp index 47dbc5ec5..c4a44989a 100644 --- a/Parse/SMTLIB2.cpp +++ b/Parse/SMTLIB2.cpp @@ -64,7 +64,7 @@ static const char* TYPECON_POSTFIX = "()"; SMTLIB2::SMTLIB2(UnitList::FIFO formulaBuffer) : _logicSet(false), - _logic(SMT_UNDEFINED), + _logic(SMTLIBLogic::UNDEFINED), _numeralsAreReal(false), _formulas(formulaBuffer), _topLevelExpr(nullptr) @@ -430,66 +430,18 @@ void SMTLIB2::readBenchmark(LExprList* bench) // ---------------------------------------------------------------------- +#define X(N) #N, const char * SMTLIB2::s_smtlibLogicNameStrings[] = { - "ALIA", - "ALL", - "ANIA", - "AUFDTLIA", - "AUFDTLIRA", - "AUFDTNIRA", - "AUFLIA", - "AUFLIRA", - "AUFNIA", - "AUFNIRA", - "BV", - "LIA", - "LRA", - "NIA", - "NRA", - "QF_ABV", - "QF_ALIA", - "QF_ANIA", - "QF_AUFBV", - "QF_AUFLIA", - "QF_AUFNIA", - "QF_AX", - "QF_BV", - "QF_IDL", - "QF_LIA", - "QF_LIRA", - "QF_LRA", - "QF_NIA", - "QF_NIRA", - "QF_NRA", - "QF_RDL", - "QF_UF", - "QF_UFBV", - "QF_UFIDL", - "QF_UFLIA", - "QF_UFLRA", - "QF_UFNIA", - "QF_UFNRA", - "UF", - "UFBV", - "UFDT", - "UFDTLIA", - "UFDTLIRA", - "UFDTNIA", - "UFDTNIRA", - "UFIDL", - "UFLIA", - "UFLRA", - "UFNIA" + SMTLIBLogic_X }; +#undef X SMTLIBLogic SMTLIB2::getLogicFromString(const std::string& str) { static NameArray smtlibLogicNames(s_smtlibLogicNameStrings, sizeof(s_smtlibLogicNameStrings)/sizeof(char*)); - ASS_EQ(smtlibLogicNames.length, SMT_UNDEFINED); - int res = smtlibLogicNames.tryToFind(str.c_str()); if(res==-1) { - return SMT_UNDEFINED; + return SMTLIBLogic::UNDEFINED; } return static_cast(res); } @@ -500,64 +452,64 @@ void SMTLIB2::readLogic(const std::string& logicStr) _logicSet = true; switch (_logic) { - case SMT_ALL: - case SMT_ALIA: - case SMT_ANIA: - case SMT_AUFDTLIA: - case SMT_AUFDTLIRA: - case SMT_AUFDTNIRA: - case SMT_AUFLIA: - case SMT_AUFNIA: - case SMT_AUFLIRA: - case SMT_AUFNIRA: - case SMT_LIA: - case SMT_NIA: - case SMT_QF_ALIA: - case SMT_QF_ANIA: - case SMT_QF_AUFLIA: - case SMT_QF_AUFNIA: - case SMT_QF_AX: - case SMT_QF_IDL: - case SMT_QF_LIA: - case SMT_QF_LIRA: - case SMT_QF_NIA: - case SMT_QF_NIRA: - case SMT_QF_UF: - case SMT_QF_UFIDL: - case SMT_QF_UFLIA: - case SMT_QF_UFNIA: - case SMT_UF: - case SMT_UFDT: - case SMT_UFDTLIA: - case SMT_UFDTLIRA: - case SMT_UFDTNIA: - case SMT_UFDTNIRA: - case SMT_UFIDL: - case SMT_UFLIA: - case SMT_UFNIA: + case SMTLIBLogic::ALL: + case SMTLIBLogic::ALIA: + case SMTLIBLogic::ANIA: + case SMTLIBLogic::AUFDTLIA: + case SMTLIBLogic::AUFDTLIRA: + case SMTLIBLogic::AUFDTNIRA: + case SMTLIBLogic::AUFLIA: + case SMTLIBLogic::AUFNIA: + case SMTLIBLogic::AUFLIRA: + case SMTLIBLogic::AUFNIRA: + case SMTLIBLogic::LIA: + case SMTLIBLogic::NIA: + case SMTLIBLogic::QF_ALIA: + case SMTLIBLogic::QF_ANIA: + case SMTLIBLogic::QF_AUFLIA: + case SMTLIBLogic::QF_AUFNIA: + case SMTLIBLogic::QF_AX: + case SMTLIBLogic::QF_IDL: + case SMTLIBLogic::QF_LIA: + case SMTLIBLogic::QF_LIRA: + case SMTLIBLogic::QF_NIA: + case SMTLIBLogic::QF_NIRA: + case SMTLIBLogic::QF_UF: + case SMTLIBLogic::QF_UFIDL: + case SMTLIBLogic::QF_UFLIA: + case SMTLIBLogic::QF_UFNIA: + case SMTLIBLogic::UF: + case SMTLIBLogic::UFDT: + case SMTLIBLogic::UFDTLIA: + case SMTLIBLogic::UFDTLIRA: + case SMTLIBLogic::UFDTNIA: + case SMTLIBLogic::UFDTNIRA: + case SMTLIBLogic::UFIDL: + case SMTLIBLogic::UFLIA: + case SMTLIBLogic::UFNIA: break; // pure real arithmetic theories treat decimals as Real constants - case SMT_LRA: - case SMT_NRA: - case SMT_QF_LRA: - case SMT_QF_NRA: - case SMT_QF_RDL: - case SMT_QF_UFLRA: - case SMT_QF_UFNRA: - case SMT_UFLRA: + case SMTLIBLogic::LRA: + case SMTLIBLogic::NRA: + case SMTLIBLogic::QF_LRA: + case SMTLIBLogic::QF_NRA: + case SMTLIBLogic::QF_RDL: + case SMTLIBLogic::QF_UFLRA: + case SMTLIBLogic::QF_UFNRA: + case SMTLIBLogic::UFLRA: _numeralsAreReal = true; break; // we don't support bit vectors - case SMT_BV: - case SMT_QF_ABV: - case SMT_QF_AUFBV: - case SMT_QF_BV: - case SMT_QF_UFBV: - case SMT_UFBV: + case SMTLIBLogic::BV: + case SMTLIBLogic::QF_ABV: + case SMTLIBLogic::QF_AUFBV: + case SMTLIBLogic::QF_BV: + case SMTLIBLogic::QF_UFBV: + case SMTLIBLogic::UFBV: USER_ERROR_EXPR("unsupported logic "+logicStr); - default: + case SMTLIBLogic::UNDEFINED: if (env.options->ignoreUnrecognizedLogic()) { break; } else { diff --git a/SAT/MinisatInterfacingNewSimp.cpp b/SAT/MinisatInterfacingNewSimp.cpp index 262057fc0..78d648125 100644 --- a/SAT/MinisatInterfacingNewSimp.cpp +++ b/SAT/MinisatInterfacingNewSimp.cpp @@ -52,7 +52,7 @@ void MinisatInterfacingNewSimp::reportMinisatOutOfMemory() { if(env.statistics) { env.statistics->print(std::cout); } - Debug::Tracer::printStack(std::cout); + Debug::Tracer::printStack(); System::terminateImmediately(1); } diff --git a/Saturation/ProvingHelper.cpp b/Saturation/ProvingHelper.cpp index 0f3073be5..0db320d25 100644 --- a/Saturation/ProvingHelper.cpp +++ b/Saturation/ProvingHelper.cpp @@ -57,9 +57,6 @@ using namespace Shell; catch(const std::bad_alloc &) { env.statistics->terminationReason=Statistics::MEMORY_LIMIT; env.statistics->refutation=0; - size_t limit=Lib::getMemoryLimit(); - //add extra 1 MB to allow proper termination - Lib::setMemoryLimit(limit+1000000); } catch(TimeLimitExceededException&) { env.statistics->terminationReason=Statistics::TIME_LIMIT; @@ -107,9 +104,6 @@ void ProvingHelper::runVampire(Problem& prb, const Options& opt) catch(const std::bad_alloc &) { env.statistics->terminationReason=Statistics::MEMORY_LIMIT; env.statistics->refutation=0; - size_t limit=Lib::getMemoryLimit(); - //add extra 1 MB to allow proper termination - Lib::setMemoryLimit(limit+1000000); } catch(TimeLimitExceededException&) { env.statistics->terminationReason=Statistics::TIME_LIMIT; diff --git a/Shell/Normalisation.cpp b/Shell/Normalisation.cpp index dc3a62a70..5b969badd 100644 --- a/Shell/Normalisation.cpp +++ b/Shell/Normalisation.cpp @@ -60,14 +60,17 @@ UnitList* Normalisation::normalise (UnitList* units) unsigned length = UnitList::length(units); // more than one literal - Sort srt(length,*this); + std::vector srt; UnitList::Iterator us(units); while (us.hasNext()) { Unit* unit = us.next(); normalise(unit); - srt.add(unit); + srt.push_back(unit); } - srt.sort(); + sort( + srt.begin(), srt.end(), + [this](Unit *u1, Unit *u2) -> bool { return lessThan(u1, u2); } + ); UnitList* result = UnitList::empty(); for (int k = length-1;k >= 0;k--) { result = new UnitList(srt[k],result); @@ -96,11 +99,15 @@ void Normalisation::normalise (Unit* unit) } // more than one literal - Sort srt(length,*this); + std::vector srt; for (int i = 0;i < length;i++) { - srt.add(clause[i]); + srt.push_back(clause[i]); } - srt.sort(); + + sort( + srt.begin(), srt.end(), + [this](Literal *l, Literal *k) -> bool { return lessThan(l, k); } + ); for (int i=0;i < length;i++) { clause[i] = srt[i]; } diff --git a/Shell/Options.cpp b/Shell/Options.cpp index 32b7bade0..e4f47e00a 100644 --- a/Shell/Options.cpp +++ b/Shell/Options.cpp @@ -93,7 +93,7 @@ void Options::init() 131072 // 128 GB (current max on the StarExecs) #endif ); - _memoryLimit.description="Memory limit in MB"; + _memoryLimit.description="Attempt to limit memory use (in MB). Limits less than 20MB are ignored to allow Vampire to start. Known not to work on MacOS for mysterious reasons: https://forums.developer.apple.com/forums/thread/702803"; _lookup.insert(&_memoryLimit); #if VAMPIRE_PERF_EXISTS diff --git a/Shell/Property.cpp b/Shell/Property.cpp index 3299783d9..724bd0761 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -89,7 +89,7 @@ Property::Property() _allClausesGround(true), _allNonTheoryClausesGround(true), _allQuantifiersEssentiallyExistential(true), - _smtlibLogic(SMTLIBLogic::SMT_UNDEFINED) + _smtlibLogic(SMTLIBLogic::UNDEFINED) { _interpretationPresence.init(Theory::instance()->numberOfFixedInterpretations(), false); } // Property::Property diff --git a/Shell/SMTLIBLogic.hpp b/Shell/SMTLIBLogic.hpp index 9bbf2d5ce..a4df2e984 100644 --- a/Shell/SMTLIBLogic.hpp +++ b/Shell/SMTLIBLogic.hpp @@ -22,61 +22,66 @@ namespace Shell { * UF - uninterpreted function = first order we know and love * DT - datatypes (term algebras) * - * VERY IMPORTANT if this is changed: must also update SMTLIB2::smtLogicNameStrings - * (which themselves must be in alphabetical order, so this is also alphabetic) + * https://en.wikipedia.org/wiki/X_macro */ -enum SMTLIBLogic { - SMT_ALIA, - SMT_ALL, - SMT_ANIA, - SMT_AUFDTLIA, - SMT_AUFDTLIRA, - SMT_AUFDTNIRA, - SMT_AUFLIA, - SMT_AUFLIRA, - SMT_AUFNIA, - SMT_AUFNIRA, - SMT_BV, - SMT_LIA, - SMT_LRA, - SMT_NIA, - SMT_NRA, - SMT_QF_ABV, - SMT_QF_ALIA, - SMT_QF_ANIA, - SMT_QF_AUFBV, - SMT_QF_AUFLIA, - SMT_QF_AUFNIA, - SMT_QF_AX, - SMT_QF_BV, - SMT_QF_IDL, - SMT_QF_LIA, - SMT_QF_LIRA, - SMT_QF_LRA, - SMT_QF_NIA, - SMT_QF_NIRA, - SMT_QF_NRA, - SMT_QF_RDL, - SMT_QF_UF, - SMT_QF_UFBV, - SMT_QF_UFIDL, - SMT_QF_UFLIA, - SMT_QF_UFLRA, - SMT_QF_UFNIA, - SMT_QF_UFNRA, - SMT_UF, - SMT_UFBV, - SMT_UFDT, - SMT_UFDTLIA, - SMT_UFDTLIRA, - SMT_UFDTNIA, - SMT_UFDTNIRA, - SMT_UFIDL, - SMT_UFLIA, - SMT_UFLRA, - SMT_UFNIA, - SMT_UNDEFINED + +#define SMTLIBLogic_X\ + X(ALIA)\ + X(ALL)\ + X(ANIA)\ + X(AUFDTLIA)\ + X(AUFDTLIRA)\ + X(AUFDTNIRA)\ + X(AUFLIA)\ + X(AUFLIRA)\ + X(AUFNIA)\ + X(AUFNIRA)\ + X(BV)\ + X(LIA)\ + X(LRA)\ + X(NIA)\ + X(NRA)\ + X(QF_ABV)\ + X(QF_ALIA)\ + X(QF_ANIA)\ + X(QF_AUFBV)\ + X(QF_AUFLIA)\ + X(QF_AUFNIA)\ + X(QF_AX)\ + X(QF_BV)\ + X(QF_IDL)\ + X(QF_LIA)\ + X(QF_LIRA)\ + X(QF_LRA)\ + X(QF_NIA)\ + X(QF_NIRA)\ + X(QF_NRA)\ + X(QF_RDL)\ + X(QF_UF)\ + X(QF_UFBV)\ + X(QF_UFIDL)\ + X(QF_UFLIA)\ + X(QF_UFLRA)\ + X(QF_UFNIA)\ + X(QF_UFNRA)\ + X(UF)\ + X(UFBV)\ + X(UFDT)\ + X(UFDTLIA)\ + X(UFDTLIRA)\ + X(UFDTNIA)\ + X(UFDTNIRA)\ + X(UFIDL)\ + X(UFLIA)\ + X(UFLRA)\ + X(UFNIA)\ + X(UNDEFINED) + +#define X(N) N, +enum class SMTLIBLogic { + SMTLIBLogic_X }; +#undef X } diff --git a/Shell/Statistics.cpp b/Shell/Statistics.cpp index 6d9647e66..ebc53761f 100644 --- a/Shell/Statistics.cpp +++ b/Shell/Statistics.cpp @@ -18,7 +18,6 @@ #include "Debug/RuntimeStatistics.hpp" -#include "Lib/Allocator.hpp" #include "Lib/Environment.hpp" #include "Lib/Timer.hpp" #include "SAT/Z3Interfacing.hpp" @@ -246,12 +245,6 @@ void Statistics::print(ostream& out) case Statistics::SATISFIABLE: out << "Satisfiable"; break; - case Statistics::SAT_SATISFIABLE: - out << "SAT Satisfiable"; - break; - case Statistics::SAT_UNSATISFIABLE: - out << "SAT Unsatisfiable"; - break; case Statistics::UNKNOWN: out << "Unknown"; break; @@ -469,13 +462,11 @@ void Statistics::print(ostream& out) } - COND_OUT("Memory used [KB]", Lib::getUsedMemory()/1024); - addCommentSignForSZS(out); out << "Time elapsed: "; Timer::printMSString(out,Timer::elapsedMilliseconds()); out << endl; - + Timer::updateInstructionCount(); unsigned instr = Timer::elapsedMegaInstructions(); if (instr) { @@ -483,7 +474,7 @@ void Statistics::print(ostream& out) out << "Instructions burned: " << instr << " (million)"; out << endl; } - + addCommentSignForSZS(out); out << "------------------------------\n"; diff --git a/Shell/Statistics.hpp b/Shell/Statistics.hpp index 3c7b2306d..1530748f2 100644 --- a/Shell/Statistics.hpp +++ b/Shell/Statistics.hpp @@ -20,11 +20,7 @@ #include #include "Forwards.hpp" - -#include "Lib/ScopedPtr.hpp" - -#include "Lib/Allocator.hpp" -#include "Lib/Option.hpp" +#include "Debug/Assertion.hpp" extern const char *VERSION_STRING; @@ -288,12 +284,8 @@ class Statistics { enum TerminationReason { /** refutation found */ REFUTATION, - /** SAT SATISFIABLE */ - SAT_SATISFIABLE, /** satisfiability detected (saturated set built) */ SATISFIABLE, - /** sat solver Unsatisfiable */ - SAT_UNSATISFIABLE, /** saturation terminated but an incomplete strategy was used */ REFUTATION_NOT_FOUND, /** inappropriate strategy **/ @@ -312,12 +304,8 @@ class Statistics { switch (self) { case REFUTATION: return out << "REFUTATION"; - case SAT_SATISFIABLE: - return out << "SAT_SATISFIABLE"; case SATISFIABLE: return out << "SATISFIABLE"; - case SAT_UNSATISFIABLE: - return out << "SAT_UNSATISFIABLE"; case REFUTATION_NOT_FOUND: return out << "REFUTATION_NOT_FOUND"; case INAPPROPRIATE: diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp index 09d651180..f72021115 100644 --- a/Shell/UIHelper.cpp +++ b/Shell/UIHelper.cpp @@ -106,7 +106,6 @@ void reportSpiderStatus(char status) << (problemName.length() == 0 ? "unknown" : problemName) << " " << Timer::elapsedDeciseconds() << " " << Timer::elapsedMegaInstructions() << " " - << Lib::getUsedMemory()/1048576 << " " << (Lib::env.options ? Lib::env.options->testId() : "unknown") << " " << commitNumber << ':' << z3Version << endl; #endif @@ -562,12 +561,6 @@ void UIHelper::outputResult(ostream& out) ASS(!s_expecting_unsat); - break; - case Statistics::SAT_SATISFIABLE: - outputSatisfiableResult(out); - break; - case Statistics::SAT_UNSATISFIABLE: - out<<"good job\n"; break; case Statistics::INAPPROPRIATE: if(env.options->outputMode() == Options::Output::SMTCOMP){ diff --git a/Shell/UIHelper.hpp b/Shell/UIHelper.hpp index 34d7138f6..7b2ded390 100644 --- a/Shell/UIHelper.hpp +++ b/Shell/UIHelper.hpp @@ -40,7 +40,7 @@ class UIHelper { struct LoadedPiece { std::string _id; UnitList::FIFO _units; - SMTLIBLogic _smtLibLogic = SMT_UNDEFINED; + SMTLIBLogic _smtLibLogic = SMTLIBLogic::UNDEFINED; bool _hasConjecture = false; }; static Stack _loadedPieces; diff --git a/Test/UnitTesting.cpp b/Test/UnitTesting.cpp index cab19075e..5813a2e3f 100644 --- a/Test/UnitTesting.cpp +++ b/Test/UnitTesting.cpp @@ -225,10 +225,6 @@ int main(int argc, const char** argv) using namespace Lib; using namespace std; - // enable tracebacks in failing unit tests by default - System::registerArgv0(argv[0]); - env.options->setTraceback(true); - bool success; auto cmd = std::string(argv[1]); auto args = Stack(argc - 2); diff --git a/UnitTests/tSkipList.cpp b/UnitTests/tSkipList.cpp index c6a1b6a7d..9ee2322d4 100644 --- a/UnitTests/tSkipList.cpp +++ b/UnitTests/tSkipList.cpp @@ -55,7 +55,7 @@ TEST_FUN(skiplist1) sl1.remove(arr[i]); } - sort(darr.begin(), darr.end()); + std::sort(darr.begin(), darr.end()); for(int i=0;i