From 5db84575f6d1d57094283d9b473020e720735e4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Mar 2016 22:27:47 -0800 Subject: [PATCH 1/7] fix regression in o7.smt2 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 307dbfda4..6495b11ec 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -896,7 +896,7 @@ namespace opt { } mk_atomic(terms); SASSERT(obj.m_id == id); - obj.m_term = to_app(orig_term); + obj.m_term = orig_term?to_app(orig_term):0; obj.m_terms.reset(); obj.m_terms.append(terms); obj.m_weights.reset(); @@ -940,6 +940,9 @@ namespace opt { bool context::verify_model(unsigned index, model* md, rational const& _v) { rational r; app_ref term = m_objectives[index].m_term; + if (!term) { + return true; + } rational v = m_objectives[index].m_adjust_value(_v); expr_ref val(m); model_ref mdl = md; From 71fff8ffa2fa80a34d2b3bf3f705ef0852310b04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Mar 2016 00:42:50 -0800 Subject: [PATCH 2/7] fix boundary case according to analysis #477, e.g., size = 252, PTR_ALIGNMENT=2, slot_id = 64 = NUM_SLOTS Signed-off-by: Nikolaj Bjorner --- src/util/small_object_allocator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/small_object_allocator.cpp b/src/util/small_object_allocator.cpp index edc3885cd..6ad1af112 100644 --- a/src/util/small_object_allocator.cpp +++ b/src/util/small_object_allocator.cpp @@ -77,7 +77,7 @@ void small_object_allocator::deallocate(size_t size, void * p) { SASSERT(m_alloc_size >= size); SASSERT(p); m_alloc_size -= size; - if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { + if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { memory::deallocate(p); return; } @@ -96,7 +96,7 @@ void * small_object_allocator::allocate(size_t size) { return memory::allocate(size); #endif m_alloc_size += size; - if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) + if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) return memory::allocate(size); #ifdef Z3DEBUG size_t osize = size; From 236875c3abc9877b80afa077eba21e4ef3b94a57 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 16:14:18 +0000 Subject: [PATCH 3/7] [CMake] Fix incorrect variable name. --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0e95cb65a..2af3d7a82 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -105,7 +105,7 @@ else() message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default") message(STATUS "The available build types are: ${available_build_types}") set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String - "Options are ${build_types}" + "Options are ${available_build_types}" FORCE) # Provide drop down menu options in cmake-gui set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types}) From e12875ddb56bd6771c87027a2bb5e41b2d5135fa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 11:28:43 +0000 Subject: [PATCH 4/7] [CMake] Mirror the additional NDEBUG define for non debug builds recently added by 03a8ef27958e369a312c55a93fc8518a9f4a6805 . This relates to #463 Also leave a note regarding ``compiler_flags_override.cmake`` its value is a bit dubious now that the compiler flags are almost the CMake defaults. --- .../cmake/cmake/compiler_flags_override.cmake | 22 ++++++++++++------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/contrib/cmake/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake index d951805de..c6005396b 100644 --- a/contrib/cmake/cmake/compiler_flags_override.cmake +++ b/contrib/cmake/cmake/compiler_flags_override.cmake @@ -1,6 +1,6 @@ # This file overrides the default compiler flags for CMake's built-in # configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here. -# The main purpose is to make sure ``-DNDEBUG`` is never set by default. +# The main purpose is to have very fine grained control of the compiler flags. if (CMAKE_C_COMPILER_ID) set(_lang C) elseif(CMAKE_CXX_COMPILER_ID) @@ -9,19 +9,25 @@ else() message(FATAL_ERROR "Unknown language") endif() +# TODO: The value of doing this is debatable. The flags set here are pretty +# much the CMake defaults now (they didn't use to be) and makes extra work for +# us when supporting different compilers. Perhaps we should move the remaining +# code that sets non-default flags out into the CMakeLists.txt files and remove +# any overrides here? if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU")) - # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed + # Taken from Modules/Compiler/GNU.cmake set(CMAKE_${_lang}_FLAGS_INIT "") set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") + set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG") + set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3 -DNDEBUG") + set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG") # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") + # FIXME: Perhaps we should be using /MD instead? set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1") + set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1 /D NDEBUG") + set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2 /D NDEBUG") + set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1 /D NDEBUG") # Override linker flags (see Windows-MSVC.cmake for CMake's defaults) # The stack size comes from the Python build system. set(_msvc_stack_size "8388608") From c7a7cc74fafc56a2b1a4aed5bbd70df12906a371 Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Wed, 9 Mar 2016 14:06:39 +0100 Subject: [PATCH 5/7] Fix bug in ufbv tactic that enabled ackermannization even if unsat core or proof generation are requested --- src/tactic/smtlogics/qfbv_tactic.cpp | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index cd446852e..7cc875fba 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -35,9 +35,9 @@ Notes: tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { params_ref solve_eq_p; - // conservative guassian elimination. - solve_eq_p.set_uint("solve_eqs_max_occs", 2); - + // conservative guassian elimination. + solve_eq_p.set_uint("solve_eqs_max_occs", 2); + params_ref simp2_p = p; simp2_p.set_bool("som", true); simp2_p.set_bool("pull_cheap_ite", true); @@ -61,13 +61,13 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { using_params(mk_simplify_tactic(m), simp2_p), // // Z3 can solve a couple of extra benchmarks by using hoist_mul - // but the timeout in SMT-COMP is too small. + // but the timeout in SMT-COMP is too small. // Moreover, it impacted negatively some easy benchmarks. // We should decide later, if we keep it or not. // using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m), - mk_ackermannize_bv_tactic(m,p) + if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) ); } @@ -80,14 +80,14 @@ static tactic * main_p(tactic* t) { } -tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { +tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) { params_ref local_ctx_p = p; local_ctx_p.set_bool("local_ctx", true); params_ref solver_p; solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. - + params_ref no_flat_p; no_flat_p.set_bool("flat", false); @@ -98,7 +98,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti params_ref big_aig_p; big_aig_p.set_bool("aig_per_assertion", false); - + tactic* preamble_st = mk_qfbv_preamble(m, p); tactic * st = main_p(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function @@ -119,10 +119,10 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti big_aig_p))))), sat), smt)))); - + st->updt_params(p); return st; - + } @@ -131,9 +131,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * new_sat = cond(mk_produce_proofs_probe(), and_then(mk_simplify_tactic(m), mk_smt_tactic()), mk_sat_tactic(m)); - + return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic()); } - - From ad4ddff99a504ea5d4b8b79b8c153c0be9991779 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 13:07:14 +0000 Subject: [PATCH 6/7] [CMake] If OpenMP support is not found make sure we set ``USE_OPENMP`` to ``OFF`` to make it clear in ccmake/cmake-gui that the support is disabled. Previously it would be left as ``ON`` even if support wasn't actually enabled. --- CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2af3d7a82..3cc29780d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -239,6 +239,7 @@ if (OPENMP_FOUND) else() list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_") message(STATUS "Not using OpenMP") + set(USE_OPENMP OFF CACHE BOOL "Use OpenMP" FORCE) endif() ################################################################################ From 8b53628d67bf48b6d4d9b9339495101e9fca10e8 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 9 Mar 2016 17:01:06 +0000 Subject: [PATCH 7/7] remove a few unused decls --- src/muz/pdr/pdr_sym_mux.h | 3 --- src/opt/opt_context.h | 2 -- src/smt/asserted_formulas.h | 1 - 3 files changed, 6 deletions(-) diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h index 78025f26b..13bdb71ec 100644 --- a/src/muz/pdr/pdr_sym_mux.h +++ b/src/muz/pdr/pdr_sym_mux.h @@ -93,7 +93,6 @@ private: std::string get_suffix(unsigned i); void ensure_tuple_size(func_decl * prim, unsigned sz); - expr_ref isolate_o_idx(expr* e, unsigned idx) const; public: sym_mux(ast_manager & m); @@ -241,8 +240,6 @@ public: func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); } func_decl * const * end_prim_preds() const { return m_prim_preds.end(); } - void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const; - std::string pp_model(const model_core & mdl) const; }; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 5ddd3be99..482b5d3b4 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -226,8 +226,6 @@ namespace opt { virtual bool verify_model(unsigned id, model* mdl, rational const& v); private: - void validate_feasibility(maxsmt& ms); - lbool execute(objective const& obj, bool committed, bool scoped); lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max); lbool execute_maxsat(symbol const& s, bool committed, bool scoped); diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 8478311dc..f4658f101 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -106,7 +106,6 @@ public: void assert_expr(expr * e, proof * in_pr); void assert_expr(expr * e); void reset(); - void set_cancel_flag(bool f); void push_scope(); void pop_scope(unsigned num_scopes); bool inconsistent() const { return m_inconsistent; }