diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a3eed360c..fbec2cf06 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1695,7 +1695,7 @@ def mk_config(): 'OBJ_EXT=.obj\n' 'LIB_EXT=.lib\n' 'AR=lib\n' - 'AR_FLAGS=/nologo\n' + 'AR_FLAGS=/nologo /LTCG\n' 'AR_OUTFLAG=/OUT:\n' 'EXE_EXT=.exe\n' 'LINK=cl\n' @@ -1709,36 +1709,36 @@ def mk_config(): extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) if DEBUG_MODE: config.write( - 'LINK_FLAGS=/nologo /MDd\n' - 'SLINK_FLAGS=/nologo /LDd\n') + 'LINK_FLAGS=/nologo /MDd /LTCG\n' + 'SLINK_FLAGS=/nologo /LDd /LTCG\n') if not VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( - 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) + 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: # Windows Release mode config.write( - 'LINK_FLAGS=/nologo /MD\n' - 'SLINK_FLAGS=/nologo /LD\n') + 'LINK_FLAGS=/nologo /MD /LTCG\n' + 'SLINK_FLAGS=/nologo /LD /LTCG\n') if TRACE: extra_opt = '%s /D _TRACE' % extra_opt if not VS_X64: config.write( - 'CXXFLAGS=/nologo /c /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/nologo /c /GL /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') else: config.write( - 'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt) + 'CXXFLAGS=/c /GL /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt) config.write( 'LINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 017bac724..1849903c5 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -884,14 +884,15 @@ namespace datalog { struct uninterpreted_function_finder_proc { ast_manager& m; datatype_util m_dt; + dl_decl_util m_dl; bool m_found; func_decl* m_func; uninterpreted_function_finder_proc(ast_manager& m): - m(m), m_dt(m), m_found(false), m_func(0) {} + m(m), m_dt(m), m_dl(m), m_found(false), m_func(0) {} void operator()(var * n) { } void operator()(quantifier * n) { } void operator()(app * n) { - if (is_uninterp(n)) { + if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) { m_found = true; m_func = n->get_decl(); } diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 60a10190a..7344f187c 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -828,7 +828,7 @@ namespace datalog { SASSERT(&expl_singleton->get_plugin()==m_er_plugin); m_e_fact_relation = static_cast(expl_singleton); } - func_decl_set const& predicates = m_context.get_predicates(); + func_decl_set predicates(m_context.get_predicates()); decl_set::iterator it = predicates.begin(); decl_set::iterator end = predicates.end(); for (; it!=end; ++it) { diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 9421b26df..7fcca9ce2 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -734,6 +734,7 @@ namespace datalog { relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, const relation_base * delta) { + TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << "\n";); relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta); if(!res && &tgt.get_plugin()!=&src.get_plugin()) { res = src.get_plugin().mk_union_fn(tgt, src, delta); diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h index 00a92748a..72448f026 100644 --- a/src/muz/rel/karr_relation.h +++ b/src/muz/rel/karr_relation.h @@ -45,7 +45,7 @@ namespace datalog { {} virtual bool can_handle_signature(const relation_signature & sig) { - return true; + return get_manager().get_context().karr(); } static symbol get_name() { return symbol("karr_relation"); } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 1acfcdf57..faf5ce0ef 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() { proof_ref_vector new_prs1(m_manager); expr_ref_vector new_exprs2(m_manager); proof_ref_vector new_prs2(m_manager); - unsigned i = m_asserted_qhead; + unsigned i = 0; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index d78b82cc6..a4e97380b 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -236,8 +236,8 @@ namespace smt { params_ref ps = m_imp->params(); #pragma omp critical (smt_kernel) { - dealloc(m_imp); - m_imp = alloc(imp, _m, fps, ps); + m_imp->~imp(); + m_imp = new (m_imp) imp(_m, fps, ps); } } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index b76fb6c74..f824cb3f1 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -361,8 +361,8 @@ namespace smt { context & ctx = m_imp->m_context; smt_params & p = m_imp->m_params; quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh(); - dealloc(m_imp); - m_imp = alloc(imp, *this, ctx, p, plugin); + m_imp->~imp(); + m_imp = new (m_imp) imp(*this, ctx, p, plugin); plugin->set_manager(*this); } }