diff --git a/CMakeLists.txt b/CMakeLists.txt index 715679957..a3ed2a312 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,18 +234,22 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") endif() + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") # Does OSX really not need any special flags? message(STATUS "Platform: Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") message(STATUS "Platform: OpenBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (CYGWIN) message(STATUS "Platform: Cygwin") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (WIN32) message(STATUS "Platform: Windows") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 24f22d8ee..d2e3d6b4c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2443,26 +2443,26 @@ def mk_config(): SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': - CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'FreeBSD': - CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS OS_DEFINES = '-D_FREEBSD_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'OpenBSD': - CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS OS_DEFINES = '-D_OPENBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 38d432f33..a1efed19e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -35,7 +35,7 @@ Revision History: parameter::~parameter() { if (m_kind == PARAM_RATIONAL) { - m_rational.~rational(); + reinterpret_cast(m_rational)->~rational(); } } @@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) { return *this; } if (m_kind == PARAM_RATIONAL) { - m_rational.~rational(); + reinterpret_cast(m_rational)->~rational(); } m_kind = other.m_kind; switch(other.m_kind) { case PARAM_INT: m_int = other.get_int(); break; case PARAM_AST: m_ast = other.get_ast(); break; - case PARAM_SYMBOL: m_symbol = other.get_symbol(); break; - case PARAM_RATIONAL: new (&m_rational) rational(other.get_rational()); break; + case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break; + case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break; case PARAM_DOUBLE: m_dval = other.m_dval; break; case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break; default: diff --git a/src/ast/ast.h b/src/ast/ast.h index 64122a7dc..3a3f08df2 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -100,12 +100,12 @@ private: // It is not possible to use tag pointers, since symbols are already tagged. union { - int m_int; // for PARAM_INT - ast* m_ast; // for PARAM_AST - symbol m_symbol; // for PARAM_SYMBOL - rational m_rational; // for PARAM_RATIONAL - double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) - unsigned m_ext_id; // for PARAM_EXTERNAL + int m_int; // for PARAM_INT + ast* m_ast; // for PARAM_AST + char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL + char m_rational[sizeof(rational)]; // for PARAM_RATIONAL + double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) + unsigned m_ext_id; // for PARAM_EXTERNAL }; public: @@ -114,10 +114,12 @@ public: explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {} - explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {} - explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(r) {} + explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } + explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(s) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); + } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -154,8 +156,8 @@ public: int get_int() const { SASSERT(is_int()); return m_int; } ast * get_ast() const { SASSERT(is_ast()); return m_ast; } - symbol const & get_symbol() const { SASSERT(is_symbol()); return m_symbol; } - rational const & get_rational() const { SASSERT(is_rational()); return m_rational; } + symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast(m_symbol)); } + rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast(m_rational)); } double get_double() const { SASSERT(is_double()); return m_dval; } unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 9753adc5b..cbbb9a6bc 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -16,31 +16,31 @@ Author: Revision History: --*/ -#include "smt/asserted_formulas.h" +#include "util/warning.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" +#include "ast/for_each_expr.h" +#include "ast/well_sorted.h" #include "ast/simplifier/arith_simplifier_plugin.h" #include "ast/simplifier/array_simplifier_plugin.h" #include "ast/simplifier/datatype_simplifier_plugin.h" #include "ast/simplifier/fpa_simplifier_plugin.h" #include "ast/simplifier/seq_simplifier_plugin.h" #include "ast/simplifier/bv_simplifier_plugin.h" -#include "ast/for_each_expr.h" -#include "ast/well_sorted.h" -#include "ast/normal_forms/pull_quant.h" #include "ast/simplifier/pull_ite_tree.h" #include "ast/simplifier/push_app_ite.h" -#include "smt/elim_term_ite.h" -#include "ast/pattern/pattern_inference.h" -#include "ast/normal_forms/nnf.h" #include "ast/simplifier/bv_elim.h" #include "ast/simplifier/inj_axiom.h" -#include "ast/rewriter/der.h" #include "ast/simplifier/elim_bounds.h" -#include "util/warning.h" #include "ast/simplifier/bit2int.h" +#include "ast/normal_forms/pull_quant.h" +#include "ast/normal_forms/nnf.h" +#include "ast/pattern/pattern_inference.h" +#include "ast/rewriter/der.h" #include "ast/rewriter/distribute_forall.h" #include "ast/macros/quasi_macros.h" +#include "smt/asserted_formulas.h" +#include "smt/elim_term_ite.h" asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m(m), @@ -138,6 +138,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { m_bsimp->set_eliminate_and(flag); } + void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { if (inconsistent()) return; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 392802d5d..a37668c7b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -53,7 +53,8 @@ namespace smt { // warning_msg("ignoring MODEL_COMPACT=true because it cannot be used with MBQI=true"); // m_params.m_model_compact = false; // } - TRACE("setup", tout << "configuring logical context, logic: " << m_logic << "\n";); + TRACE("setup", tout << "configuring logical context, logic: " << m_logic << " " << cm << "\n";); + m_already_configured = true; switch (cm) { @@ -202,6 +203,9 @@ namespace smt { void setup::setup_QF_UF() { m_params.m_relevancy_lvl = 0; m_params.m_nnf_cnf = false; + m_params.m_restart_strategy = RS_LUBY; + m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; + m_params.m_random_initial_activity = IA_RANDOM; } void setup::setup_QF_BVRE() { @@ -210,13 +214,9 @@ namespace smt { m_context.register_plugin(alloc(theory_seq, m_manager)); } - void setup::setup_QF_UF(static_features const & st) { + void setup::setup_QF_UF(static_features const & st) { check_no_arithmetic(st, "QF_UF"); - m_params.m_relevancy_lvl = 0; - m_params.m_nnf_cnf = false; - m_params.m_restart_strategy = RS_LUBY; - m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; - m_params.m_random_initial_activity = IA_RANDOM; + setup_QF_UF(); TRACE("setup", tout << "st.m_num_theories: " << st.m_num_theories << "\n"; tout << "st.m_num_uninterpreted_functions: " << st.m_num_uninterpreted_functions << "\n";); @@ -548,6 +548,7 @@ namespace smt { } void setup::setup_QF_BV() { + TRACE("setup", tout << "qf-bv\n";); m_params.m_relevancy_lvl = 0; m_params.m_arith_reflect = false; m_params.m_bv_cc = false; @@ -877,7 +878,7 @@ namespace smt { void setup::setup_unknown() { static_features st(m_manager); st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas()); - + TRACE("setup", tout << "setup_unknown\n";); setup_arith(); setup_arrays(); setup_bv(); @@ -916,7 +917,7 @@ namespace smt { tout << "has fpa: " << st.m_has_fpa << "\n"; tout << "has arrays: " << st.m_has_arrays << "\n";); - if (st.num_non_uf_theories() == 0) { + if (st.num_non_uf_theories() == 0) { setup_QF_UF(st); return; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index bde9e0e98..0ad9e5f19 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -93,7 +93,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic == "QF_FD") + else if (logic == "QF_FD" || logic == "SAT") return mk_solver2tactic(mk_fd_solver(m, p)); //else if (logic=="QF_UFNRA") // return mk_qfufnra_tactic(m, p); @@ -102,7 +102,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const } static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { - if (logic == "QF_FD") + if (logic == "QF_FD" || logic == "SAT") return mk_fd_solver(m, p); return 0; } diff --git a/src/util/optional.h b/src/util/optional.h index 6a00cf841..22757f3bd 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -23,35 +23,32 @@ Revision History: template class optional { - union { - T m_obj; - char m_dummy; - }; - bool m_initialized; + char m_obj[sizeof(T)]; + char m_initialized; void construct(const T & val) { - m_initialized = true; - new (&m_obj) T(val); + m_initialized = 1; + new (reinterpret_cast(m_obj)) T(val); } void destroy() { - if (m_initialized) { - m_obj.~T(); + if (m_initialized == 1) { + reinterpret_cast(m_obj)->~T(); } - m_initialized = false; + m_initialized = 0; } public: optional(): - m_initialized(false) {} + m_initialized(0) {} explicit optional(const T & val) { construct(val); } optional(const optional & val): - m_initialized(false) { - if (val.m_initialized) { + m_initialized(0) { + if (val.m_initialized == 1) { construct(*val); } } @@ -62,13 +59,13 @@ public: static optional const & undef() { static optional u; return u; } - bool initialized() const { return m_initialized; } - operator bool() const { return m_initialized; } - bool operator!() const { return !m_initialized; } + bool initialized() const { return m_initialized == 1; } + operator bool() const { return m_initialized == 1; } + bool operator!() const { return m_initialized == 0; } T * get() const { - if (m_initialized) { - return &m_obj; + if (m_initialized == 1) { + return reinterpret_cast(m_obj); } else { return 0; @@ -76,29 +73,29 @@ public: } void set_invalid() { - if (m_initialized) { + if (m_initialized == 1) { destroy(); } } T * operator->() { - SASSERT(m_initialized); - return &m_obj; + SASSERT(m_initialized==1); + return reinterpret_cast(m_obj); } T const * operator->() const { - SASSERT(m_initialized); - return &m_obj; + SASSERT(m_initialized==1); + return reinterpret_cast(m_obj); } const T & operator*() const { - SASSERT(m_initialized); - return m_obj; + SASSERT(m_initialized==1); + return *reinterpret_cast(m_obj); } T & operator*() { - SASSERT(m_initialized); - return m_obj; + SASSERT(m_initialized==1); + return *reinterpret_cast(m_obj); } optional & operator=(const T & val) {