mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
nikolajbjorner 2015-02-27 11:09:05 -08:00
commit 3bf22964dd
8 changed files with 20 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

18
scripts/mk_util.py
View file

@ -1695,7 +1695,7 @@ def mk_config():
'OBJ_EXT=.obj\n' 'OBJ_EXT=.obj\n'
'LIB_EXT=.lib\n' 'LIB_EXT=.lib\n'
'AR=lib\n' 'AR=lib\n'
'AR_FLAGS=/nologo\n' 'AR_FLAGS=/nologo /LTCG\n'
'AR_OUTFLAG=/OUT:\n' 'AR_OUTFLAG=/OUT:\n'
'EXE_EXT=.exe\n' 'EXE_EXT=.exe\n'
'LINK=cl\n' 'LINK=cl\n'
@ -1709,36 +1709,36 @@ def mk_config():
extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
if DEBUG_MODE: if DEBUG_MODE:
config.write( config.write(
'LINK_FLAGS=/nologo /MDd\n' 'LINK_FLAGS=/nologo /MDd /LTCG\n'
'SLINK_FLAGS=/nologo /LDd\n') 'SLINK_FLAGS=/nologo /LDd /LTCG\n')
if not VS_X64: if not VS_X64:
config.write( 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( config.write(
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' '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') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else: else:
config.write( 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( config.write(
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' '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') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else: else:
# Windows Release mode # Windows Release mode
config.write( config.write(
'LINK_FLAGS=/nologo /MD\n' 'LINK_FLAGS=/nologo /MD /LTCG\n'
'SLINK_FLAGS=/nologo /LD\n') 'SLINK_FLAGS=/nologo /LD /LTCG\n')
if TRACE: if TRACE:
extra_opt = '%s /D _TRACE' % extra_opt extra_opt = '%s /D _TRACE' % extra_opt
if not VS_X64: if not VS_X64:
config.write( 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( config.write(
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' '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') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else: else:
config.write( 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( config.write(
'LINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' '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') 'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')

5
src/muz/base/dl_rule.cpp
View file

@ -884,14 +884,15 @@ namespace datalog {
struct uninterpreted_function_finder_proc { struct uninterpreted_function_finder_proc {
ast_manager& m; ast_manager& m;
datatype_util m_dt; datatype_util m_dt;
dl_decl_util m_dl;
bool m_found; bool m_found;
func_decl* m_func; func_decl* m_func;
uninterpreted_function_finder_proc(ast_manager& m): 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()(var * n) { }
void operator()(quantifier * n) { } void operator()(quantifier * n) { }
void operator()(app * 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_found = true;
m_func = n->get_decl(); m_func = n->get_decl();
} }

2
src/muz/rel/dl_mk_explanations.cpp
View file

@ -828,7 +828,7 @@ namespace datalog {
SASSERT(&expl_singleton->get_plugin()==m_er_plugin); SASSERT(&expl_singleton->get_plugin()==m_er_plugin);
m_e_fact_relation = static_cast<explanation_relation *>(expl_singleton); m_e_fact_relation = static_cast<explanation_relation *>(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 it = predicates.begin();
decl_set::iterator end = predicates.end(); decl_set::iterator end = predicates.end();
for (; it!=end; ++it) { for (; it!=end; ++it) {

1
src/muz/rel/dl_relation_manager.cpp
View file

@ -734,6 +734,7 @@ namespace datalog {
relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src, relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta) { 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); relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta);
if(!res && &tgt.get_plugin()!=&src.get_plugin()) { if(!res && &tgt.get_plugin()!=&src.get_plugin()) {
res = src.get_plugin().mk_union_fn(tgt, src, delta); res = src.get_plugin().mk_union_fn(tgt, src, delta);

2
src/muz/rel/karr_relation.h
View file

@ -45,7 +45,7 @@ namespace datalog {
{} {}
virtual bool can_handle_signature(const relation_signature & sig) { 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"); } static symbol get_name() { return symbol("karr_relation"); }

2
src/smt/asserted_formulas.cpp
View file

@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager); proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager); expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager); proof_ref_vector new_prs2(m_manager);
unsigned i = m_asserted_qhead; unsigned i = 0;
unsigned sz = m_asserted_formulas.size(); unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) { for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i); expr * n = m_asserted_formulas.get(i);

4
src/smt/smt_kernel.cpp
View file

@ -236,8 +236,8 @@ namespace smt {
params_ref ps = m_imp->params(); params_ref ps = m_imp->params();
#pragma omp critical (smt_kernel) #pragma omp critical (smt_kernel)
{ {
dealloc(m_imp); m_imp->~imp();
m_imp = alloc(imp, _m, fps, ps); m_imp = new (m_imp) imp(_m, fps, ps);
} }
} }

4
src/smt/smt_quantifier.cpp
View file

@ -361,8 +361,8 @@ namespace smt {
context & ctx = m_imp->m_context; context & ctx = m_imp->m_context;
smt_params & p = m_imp->m_params; smt_params & p = m_imp->m_params;
quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh(); quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
dealloc(m_imp); m_imp->~imp();
m_imp = alloc(imp, *this, ctx, p, plugin); m_imp = new (m_imp) imp(*this, ctx, p, plugin);
plugin->set_manager(*this); plugin->set_manager(*this);
} }
} }