diff --git a/CMakeLists.txt b/CMakeLists.txt index 0e95cb65a..3cc29780d 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}) @@ -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() ################################################################################ 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") diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt index d59265c5c..ed3a84edf 100644 --- a/contrib/cmake/src/tactic/core/CMakeLists.txt +++ b/contrib/cmake/src/tactic/core/CMakeLists.txt @@ -18,6 +18,7 @@ z3_add_component(core_tactics split_clause_tactic.cpp symmetry_reduce_tactic.cpp tseitin_cnf_tactic.cpp + collect_occs.cpp COMPONENT_DEPENDENCIES normal_forms tactic 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; } diff --git a/src/tactic/core/collect_occs.cpp b/src/tactic/core/collect_occs.cpp new file mode 100644 index 000000000..69c538db6 --- /dev/null +++ b/src/tactic/core/collect_occs.cpp @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + collect_cccs.cpp + +Abstract: + + Collect variables by occurrences. + +Author: + + Leonardo (leonardo) 2011-10-22 + +Notes: + +--*/ + +#include "ast.h" +#include "goal.h" +#include "hashtable.h" +#include "collect_occs.h" + +bool collect_occs::visit(expr * t) { + if (m_visited.is_marked(t)) { + if (is_uninterp_const(t)) + m_more_than_once.mark(t); + return true; + } + m_visited.mark(t); + if (is_uninterp_const(t)) { + m_vars.push_back(to_app(t)); + return true; + } + if (is_var(t)) + return true; + if (is_app(t) && to_app(t)->get_num_args() == 0) + return true; + m_stack.push_back(frame(t, 0)); + return false; +} + +void collect_occs::process(expr * t) { + SASSERT(m_stack.empty()); + if (visit(t)) + return; + SASSERT(!m_stack.empty()); + unsigned num; + expr * child; + while (!m_stack.empty()) { + start: + frame & fr = m_stack.back(); + expr * t = fr.first; + switch (t->get_kind()) { + case AST_APP: + num = to_app(t)->get_num_args(); + while (fr.second < num) { + child = to_app(t)->get_arg(fr.second); + fr.second++; + if (!visit(child)) + goto start; + } + m_stack.pop_back(); + break; + case AST_QUANTIFIER: + // don't need to visit patterns + child = to_quantifier(t)->get_expr(); + fr.second++; + if (!visit(child)) + goto start; + m_stack.pop_back(); + break; + default: + UNREACHABLE(); + } + } +} + + +void collect_occs::operator()(goal const & g, obj_hashtable & r) { + unsigned sz = g.size(); + for (unsigned i = 0; i < sz; i++) { + expr * t = g.form(i); + process(t); + } + + ptr_vector::const_iterator it = m_vars.begin(); + ptr_vector::const_iterator end = m_vars.end(); + for (; it != end; ++it) { + if (m_more_than_once.is_marked(*it)) + continue; + r.insert(*it); + } + m_visited.reset(); + m_more_than_once.reset(); +} diff --git a/src/tactic/core/collect_occs.h b/src/tactic/core/collect_occs.h new file mode 100644 index 000000000..7b42e44a6 --- /dev/null +++ b/src/tactic/core/collect_occs.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + collect_cccs.h + +Abstract: + + Collect variables by occurrences. + +Author: + + Leonardo (leonardo) 2011-10-22 + +Notes: + +--*/ +#ifndef COLLECT_OCCS_H_ +#define COLLECT_OCCS_H_ + +class collect_occs { + expr_fast_mark1 m_visited; + expr_fast_mark2 m_more_than_once; + typedef std::pair frame; + svector m_stack; + ptr_vector m_vars; + + bool visit(expr * t); + void process(expr * t); + +public: + + void operator()(goal const & g, obj_hashtable & r); + +}; + +#endif diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 538797ddf..156f69388 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -24,6 +24,7 @@ Notes: #include"bv_decl_plugin.h" #include"array_decl_plugin.h" #include"datatype_decl_plugin.h" +#include"collect_occs.h" #include"cooperate.h" #include"ast_smt2_pp.h" #include"ast_ll_pp.h" @@ -32,86 +33,6 @@ class elim_uncnstr_tactic : public tactic { struct imp { // unconstrained vars collector - struct collect { - expr_fast_mark1 m_visited; - expr_fast_mark2 m_more_than_once; - typedef std::pair frame; - svector m_stack; - ptr_vector m_vars; - - bool visit(expr * t) { - if (m_visited.is_marked(t)) { - if (is_uninterp_const(t)) - m_more_than_once.mark(t); - return true; - } - m_visited.mark(t); - if (is_uninterp_const(t)) { - m_vars.push_back(to_app(t)); - return true; - } - if (is_var(t)) - return true; - if (is_app(t) && to_app(t)->get_num_args() == 0) - return true; - m_stack.push_back(frame(t, 0)); - return false; - } - - void process(expr * t) { - SASSERT(m_stack.empty()); - if (visit(t)) - return; - SASSERT(!m_stack.empty()); - unsigned num; - expr * child; - while (!m_stack.empty()) { - start: - frame & fr = m_stack.back(); - expr * t = fr.first; - switch (t->get_kind()) { - case AST_APP: - num = to_app(t)->get_num_args(); - while (fr.second < num) { - child = to_app(t)->get_arg(fr.second); - fr.second++; - if (!visit(child)) - goto start; - } - m_stack.pop_back(); - break; - case AST_QUANTIFIER: - // don't need to visit patterns - child = to_quantifier(t)->get_expr(); - fr.second++; - if (!visit(child)) - goto start; - m_stack.pop_back(); - break; - default: - UNREACHABLE(); - } - } - } - - void operator()(goal const & g, obj_hashtable & r) { - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = g.form(i); - process(t); - } - - ptr_vector::const_iterator it = m_vars.begin(); - ptr_vector::const_iterator end = m_vars.end(); - for (; it != end; ++it) { - if (m_more_than_once.is_marked(*it)) - continue; - r.insert(*it); - } - m_visited.reset(); - m_more_than_once.reset(); - } - }; typedef extension_model_converter mc; @@ -910,7 +831,7 @@ class elim_uncnstr_tactic : public tactic { TRACE("elim_uncnstr_bug", g->display(tout);); tactic_report report("elim-uncnstr-vars", *g); m_vars.reset(); - collect p; + collect_occs p; p(*g, m_vars); if (m_vars.empty()) { result.push_back(g.get()); @@ -977,7 +898,7 @@ class elim_uncnstr_tactic : public tactic { m_rw->reset(); // reset cache m_vars.reset(); { - collect p; + collect_occs p; p(*g, m_vars); } if (m_vars.empty()) 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()); } - -