mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

merging interpolation fix (issue 182)

Browse source
This commit is contained in:
Ken McMillan 2015-03-20 17:46:01 -07:00
commit be709802cd
49 changed files with 256 additions and 123 deletions
Download patch file Download diff file Expand all files Collapse all files

2
RELEASE_NOTES
View file

@ -11,7 +11,7 @@ Version 4.4
- Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one. - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one.
- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, and Codeplex users rsas, clockish, Heizmann. - Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886.
Version 4.3.2 Version 4.3.2

10
examples/c++/example.cpp
View file

@ -975,6 +975,15 @@ void substitute_example() {
std::cout << new_f << std::endl; std::cout << new_f << std::endl;
} }
void extract_example() {
std::cout << "extract example\n";
context c;
expr x(c);
x = c.constant("x", c.bv_sort(32));
expr y = x.extract(21, 10);
std::cout << y << " " << y.hi() << " " << y.lo() << "\n";
}
int main() { int main() {
try { try {
demorgan(); std::cout << "\n"; demorgan(); std::cout << "\n";
@ -1013,6 +1022,7 @@ int main() {
expr_vector_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n";
exists_expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n";
substitute_example(); std::cout << "\n"; substitute_example(); std::cout << "\n";
extract_example(); std::cout << "\n";
std::cout << "done\n"; std::cout << "done\n";
} }
catch (exception & ex) { catch (exception & ex) {

33
scripts/mk_util.py
View file

@ -1376,6 +1376,7 @@ class MLComponent(Component):
sub_dir = os.path.join('api', 'ml') sub_dir = os.path.join('api', 'ml')
mk_dir(os.path.join(BUILD_DIR, sub_dir)) mk_dir(os.path.join(BUILD_DIR, sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir api_src = get_component(API_COMPONENT).to_src_dir
out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it.
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)): for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f))) out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f)) str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
@ -1412,7 +1413,7 @@ class MLComponent(Component):
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'), (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs.c'),
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)')); get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
out.write('\t$(CC) $(CXXFLAGS) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' % out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' %
(OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs'))) (OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs')))
out.write('%s: %s %s %s$(SO_EXT)' % ( out.write('%s: %s %s %s$(SO_EXT)' % (
@ -1695,7 +1696,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'
@ -1713,16 +1714,16 @@ def mk_config():
'SLINK_FLAGS=/nologo /LDd\n') 'SLINK_FLAGS=/nologo /LDd\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 /LTCG /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 /LTCG /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 /LTCG /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 /LTCG /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(
@ -1732,16 +1733,16 @@ def mk_config():
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 /LTCG /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 /LTCG /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 /LTCG /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 /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
# End of Windows VS config.mk # End of Windows VS config.mk
if is_verbose(): if is_verbose():
@ -1782,7 +1783,7 @@ def mk_config():
FOCI2 = False FOCI2 = False
if GIT_HASH: if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
CXXFLAGS = '%s -c' % CXXFLAGS CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
HAS_OMP = test_openmp(CXX) HAS_OMP = test_openmp(CXX)
if HAS_OMP: if HAS_OMP:
CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS
@ -2104,7 +2105,7 @@ def mk_pat_db():
c = get_component(PATTERN_COMPONENT) c = get_component(PATTERN_COMPONENT)
fin = open(os.path.join(c.src_dir, 'database.smt2'), 'r') fin = open(os.path.join(c.src_dir, 'database.smt2'), 'r')
fout = open(os.path.join(c.src_dir, 'database.h'), 'w') fout = open(os.path.join(c.src_dir, 'database.h'), 'w')
fout.write('char const * g_pattern_database =\n') fout.write('static char const g_pattern_database[] =\n')
for line in fin: for line in fin:
fout.write('"%s\\n"\n' % line.strip('\n')) fout.write('"%s\\n"\n' % line.strip('\n'))
fout.write(';\n') fout.write(';\n')

2
scripts/mk_win_dist.py
View file

@ -39,7 +39,7 @@ def mk_dir(d):
os.makedirs(d) os.makedirs(d)
def set_build_dir(path): def set_build_dir(path):
global BUILD_DIR global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR
BUILD_DIR = path BUILD_DIR = path
BUILD_X86_DIR = os.path.join(path, 'x86') BUILD_X86_DIR = os.path.join(path, 'x86')
BUILD_X64_DIR = os.path.join(path, 'x64') BUILD_X64_DIR = os.path.join(path, 'x64')

5
scripts/update_api.py
View file

@ -642,6 +642,7 @@ def mk_java():
java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('#ifdef __cplusplus\n')
java_wrapper.write('extern "C" {\n') java_wrapper.write('extern "C" {\n')
java_wrapper.write('#endif\n\n') java_wrapper.write('#endif\n\n')
java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n')
java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n')
java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n')
java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n')
@ -688,13 +689,13 @@ def mk_java():
java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n') java_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
java_wrapper.write(' // wrappers below.\n') java_wrapper.write(' // wrappers below.\n')
java_wrapper.write('}\n\n') java_wrapper.write('}\n\n')
java_wrapper.write('JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str) java_wrapper.write('DLL_VIS JNIEXPORT void JNICALL Java_%s_Native_setInternalErrorHandler(JNIEnv * jenv, jclass cls, jlong a0)\n' % pkg_str)
java_wrapper.write('{\n') java_wrapper.write('{\n')
java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n') java_wrapper.write(' Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler);\n')
java_wrapper.write('}\n\n') java_wrapper.write('}\n\n')
java_wrapper.write('') java_wrapper.write('')
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name))) java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
i = 0; i = 0;
for param in params: for param in params:
java_wrapper.write(', ') java_wrapper.write(', ')

8
src/api/api_ast.cpp
View file

@ -300,7 +300,7 @@ extern "C" {
Z3_CATCH_RETURN(-1); Z3_CATCH_RETURN(-1);
} }
char const * Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s) { Z3_API char const * Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
Z3_TRY; Z3_TRY;
LOG_Z3_get_symbol_string(c, s); LOG_Z3_get_symbol_string(c, s);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
@ -823,7 +823,7 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
char const * Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a) { Z3_API char const * Z3_ast_to_string(Z3_context c, Z3_ast a) {
Z3_TRY; Z3_TRY;
LOG_Z3_ast_to_string(c, a); LOG_Z3_ast_to_string(c, a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
@ -866,11 +866,11 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
char const * Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s) { Z3_API char const * Z3_sort_to_string(Z3_context c, Z3_sort s) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(s)); return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(s));
} }
char const * Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) { Z3_API char const * Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f)); return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f));
} }

6
src/api/api_context.cpp
View file

@ -548,12 +548,12 @@ extern "C" {
} }
} }
char const * Z3_API Z3_get_error_msg(Z3_error_code err) { Z3_API char const * Z3_get_error_msg(Z3_error_code err) {
LOG_Z3_get_error_msg(err); LOG_Z3_get_error_msg(err);
return _get_error_msg_ex(0, err); return _get_error_msg_ex(0, err);
} }
char const * Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) { Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
LOG_Z3_get_error_msg_ex(c, err); LOG_Z3_get_error_msg_ex(c, err);
return _get_error_msg_ex(c, err); return _get_error_msg_ex(c, err);
} }
@ -577,7 +577,7 @@ extern "C" {
}; };
ast_manager & Z3_API Z3_get_manager(__in Z3_context c) { Z3_API ast_manager& Z3_get_manager(__in Z3_context c) {
return mk_c(c)->m(); return mk_c(c)->m();
} }

12
src/api/api_interp.cpp
View file

@ -293,10 +293,10 @@ extern "C" {
else { else {
model_ref _m; model_ref _m;
m_solver.get()->get_model(_m); m_solver.get()->get_model(_m);
Z3_model_ref *crap = alloc(Z3_model_ref); Z3_model_ref *tmp_val = alloc(Z3_model_ref);
crap->m_model = _m.get(); tmp_val->m_model = _m.get();
mk_c(c)->save_object(crap); mk_c(c)->save_object(tmp_val);
*model = of_model(crap); *model = of_model(tmp_val);
} }
*out_interp = of_ast_vector(v); *out_interp = of_ast_vector(v);
@ -490,8 +490,8 @@ extern "C" {
try { try {
std::string foo(filename); std::string foo(filename);
if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){ if (foo.size() >= 5 && foo.substr(foo.size() - 5) == ".smt2"){
Z3_ast ass = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0); Z3_ast assrts = Z3_parse_smtlib2_file(ctx, filename, 0, 0, 0, 0, 0, 0);
Z3_app app = Z3_to_app(ctx, ass); Z3_app app = Z3_to_app(ctx, assrts);
int nconjs = Z3_get_app_num_args(ctx, app); int nconjs = Z3_get_app_num_args(ctx, app);
assertions.resize(nconjs); assertions.resize(nconjs);
for (int k = 0; k < nconjs; k++) for (int k = 0; k < nconjs; k++)

2
src/api/api_model.cpp
View file

@ -651,7 +651,7 @@ extern "C" {
Z3_CATCH_RETURN(Z3_FALSE); Z3_CATCH_RETURN(Z3_FALSE);
} }
char const * Z3_API Z3_model_to_string(Z3_context c, Z3_model m) { Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) {
Z3_TRY; Z3_TRY;
LOG_Z3_model_to_string(c, m); LOG_Z3_model_to_string(c, m);
RESET_ERROR_CODE(); RESET_ERROR_CODE();

2
src/api/api_quant.cpp
View file

@ -507,7 +507,7 @@ extern "C" {
return (Z3_ast)(p); return (Z3_ast)(p);
} }
char const * Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p) { Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p)); return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
} }

2
src/api/api_solver_old.cpp
View file

@ -297,7 +297,7 @@ extern "C" {
Z3_CATCH; Z3_CATCH;
} }
char const * Z3_API Z3_context_to_string(Z3_context c) { Z3_API char const * Z3_context_to_string(Z3_context c) {
Z3_TRY; Z3_TRY;
LOG_Z3_context_to_string(c); LOG_Z3_context_to_string(c);
RESET_ERROR_CODE(); RESET_ERROR_CODE();

3
src/api/c++/z3++.h
View file

@ -866,6 +866,9 @@ namespace z3 {
friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; } friend expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); } friend expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); return expr(ctx(), r); }
unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
/** /**
\brief Return a simplified version of this expression. \brief Return a simplified version of this expression.

10
src/api/java/Solver.java
View file

@ -176,9 +176,9 @@ public class Solver extends Z3Object
**/ **/
public int getNumAssertions() throws Z3Exception public int getNumAssertions() throws Z3Exception
{ {
ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
getContext().nCtx(), getNativeObject())); getContext().nCtx(), getNativeObject()));
return ass.size(); return assrts.size();
} }
/** /**
@ -188,12 +188,12 @@ public class Solver extends Z3Object
**/ **/
public BoolExpr[] getAssertions() throws Z3Exception public BoolExpr[] getAssertions() throws Z3Exception
{ {
ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
getContext().nCtx(), getNativeObject())); getContext().nCtx(), getNativeObject()));
int n = ass.size(); int n = assrts.size();
BoolExpr[] res = new BoolExpr[n]; BoolExpr[] res = new BoolExpr[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++)
res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject()); res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
return res; return res;
} }

6
src/api/z3_macros.h
View file

@ -35,7 +35,11 @@
#endif #endif
#ifndef Z3_API #ifndef Z3_API
#define Z3_API # ifdef __GNUC__
# define Z3_API __attribute__ ((visibility ("default")))
# else
# define Z3_API
# endif
#endif #endif
#ifndef DEFINE_TYPE #ifndef DEFINE_TYPE

8
src/ast/ast_smt_pp.cpp
View file

@ -34,9 +34,9 @@ Revision History:
// --------------------------------------- // ---------------------------------------
// smt_renaming // smt_renaming
const static char* m_predef_names[] = { static const char m_predef_names[][8] = {
"=", ">=", "<=", "+", "-", "*", ">", "<", "!=", "or", "and", "implies", "not", "iff", "xor", "=", ">=", "<=", "+", "-", "*", ">", "<", "!=", "or", "and", "implies", "not", "iff", "xor",
"true", "false", "forall", "exists", "let", "flet", NULL "true", "false", "forall", "exists", "let", "flet"
}; };
symbol smt_renaming::fix_symbol(symbol s, int k) { symbol smt_renaming::fix_symbol(symbol s, int k) {
@ -120,8 +120,8 @@ bool smt_renaming::all_is_legal(char const* s) {
} }
smt_renaming::smt_renaming() { smt_renaming::smt_renaming() {
for (const char **p = m_predef_names; *p; ++p) { for (unsigned i = 0; i < ARRAYSIZE(m_predef_names); ++i) {
symbol s(*p); symbol s(m_predef_names[i]);
m_translate.insert(s, s); m_translate.insert(s, s);
m_rev_translate.insert(s, s); m_rev_translate.insert(s, s);
} }

2
src/ast/rewriter/poly_rewriter.h
View file

@ -26,8 +26,6 @@ Notes:
template<typename Config> template<typename Config>
class poly_rewriter : public Config { class poly_rewriter : public Config {
public:
static char const * g_ste_blowup_msg;
protected: protected:
typedef typename Config::numeral numeral; typedef typename Config::numeral numeral;
sort * m_curr_sort; sort * m_curr_sort;

5
src/ast/rewriter/poly_rewriter_def.h
View file

@ -22,9 +22,6 @@ Notes:
#include"ast_ll_pp.h" #include"ast_ll_pp.h"
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
template<typename Config>
char const * poly_rewriter<Config>::g_ste_blowup_msg = "sum of monomials blowup";
template<typename Config> template<typename Config>
void poly_rewriter<Config>::updt_params(params_ref const & _p) { void poly_rewriter<Config>::updt_params(params_ref const & _p) {
@ -356,7 +353,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " "; TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " ";
tout << "\n";); tout << "\n";);
if (sum.size() > m_som_blowup) if (sum.size() > m_som_blowup)
throw rewriter_exception(g_ste_blowup_msg); throw rewriter_exception("sum of monomials blowup");
m_args.reset(); m_args.reset();
for (unsigned i = 0; i < num_args; i++) { for (unsigned i = 0; i < num_args; i++) {
expr * const * v = sums[i]; expr * const * v = sums[i];

1
src/cmd_context/cmd_context.cpp
View file

@ -1185,6 +1185,7 @@ void cmd_context::reset(bool finalize) {
restore_assertions(0); restore_assertions(0);
if (m_solver) if (m_solver)
m_solver = 0; m_solver = 0;
m_scopes.reset();
m_pp_env = 0; m_pp_env = 0;
m_dt_eh = 0; m_dt_eh = 0;
if (m_manager) { if (m_manager) {

30
src/cmd_context/context_params.cpp
View file

@ -24,6 +24,16 @@ Notes:
#include"solver.h" #include"solver.h"
context_params::context_params() { context_params::context_params() {
m_unsat_core = false;
m_model = true;
m_model_validate = false;
m_auto_config = true;
m_proof = false;
m_trace = false;
m_debug_ref_count = false;
m_smtlib2_compliant = false;
m_well_sorted_check = false;
m_timeout = UINT_MAX;
updt_params(); updt_params();
} }
@ -98,17 +108,17 @@ void context_params::updt_params() {
} }
void context_params::updt_params(params_ref const & p) { void context_params::updt_params(params_ref const & p) {
m_timeout = p.get_uint("timeout", UINT_MAX); m_timeout = p.get_uint("timeout", m_timeout);
m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true)); m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
m_auto_config = p.get_bool("auto_config", true); m_auto_config = p.get_bool("auto_config", m_auto_config);
m_proof = p.get_bool("proof", false); m_proof = p.get_bool("proof", m_proof);
m_model = p.get_bool("model", true); m_model = p.get_bool("model", m_model);
m_model_validate = p.get_bool("model_validate", false); m_model_validate = p.get_bool("model_validate", m_model_validate);
m_trace = p.get_bool("trace", false); m_trace = p.get_bool("trace", m_trace);
m_trace_file_name = p.get_str("trace_file_name", "z3.log"); m_trace_file_name = p.get_str("trace_file_name", "z3.log");
m_unsat_core = p.get_bool("unsat_core", false); m_unsat_core = p.get_bool("unsat_core", m_unsat_core);
m_debug_ref_count = p.get_bool("debug_ref_count", false); m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count);
m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false); m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
} }
void context_params::collect_param_descrs(param_descrs & d) { void context_params::collect_param_descrs(param_descrs & d) {

14
src/duality/duality_rpfp.cpp
View file

@ -1131,10 +1131,10 @@ namespace Duality {
} }
std::vector<expr> *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() }; std::vector<expr> *cnsts[2] = { &child->getTerms(), &assumptions->getTerms() };
for (unsigned i = 0; i < assumps.size(); i++) { for (unsigned i = 0; i < assumps.size(); i++) {
expr &ass = assumps[i]; expr &as = assumps[i];
expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; expr alit = (as.is_app() && as.decl().get_decl_kind() == Implies) ? as.arg(0) : as;
bool isA = map.find(alit) != map.end(); bool isA = map.find(alit) != map.end();
cnsts[isA ? 0 : 1]->push_back(ass); cnsts[isA ? 0 : 1]->push_back(as);
} }
} }
else else
@ -3221,12 +3221,12 @@ done:
std::vector<expr> assumps, core, conjuncts; std::vector<expr> assumps, core, conjuncts;
AssertEdgeCache(edge,assumps); AssertEdgeCache(edge,assumps);
for(unsigned i = 0; i < edge->Children.size(); i++){ for(unsigned i = 0; i < edge->Children.size(); i++){
expr ass = GetAnnotation(edge->Children[i]); expr as = GetAnnotation(edge->Children[i]);
std::vector<expr> clauses; std::vector<expr> clauses;
if(!ass.is_true()){ if(!as.is_true()){
CollectConjuncts(ass.arg(1),clauses); CollectConjuncts(as.arg(1),clauses);
for(unsigned j = 0; j < clauses.size(); j++) for(unsigned j = 0; j < clauses.size(); j++)
GetAssumptionLits(ass.arg(0) || clauses[j],assumps); GetAssumptionLits(as.arg(0) || clauses[j],assumps);
} }
} }
expr fmla = GetAnnotation(node); expr fmla = GetAnnotation(node);

2
src/interp/iz3scopes.cpp
View file

@ -165,7 +165,7 @@ scopes::range scopes::range_glb(const range &rng1, const range &rng2){
return bar.first->second; return bar.first->second;
//std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo); //std::pair<hash_set<scopes::range_lo>::iterator,bool> bar = rt->unique.insert(foo);
// const range_lo *baz = &*(bar.first); // const range_lo *baz = &*(bar.first);
// return (range_lo *)baz; // exit const hell // return (range_lo *)baz; // coerce const
} }
scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){ scopes::range_lo *scopes::range_lub_lo(range_lo *rng1, range_lo *rng2){

4
src/model/func_interp.cpp
View file

@ -276,8 +276,8 @@ expr * func_interp::get_interp() const {
return r; return r;
} }
func_interp * func_interp::translate(ast_translation & translator) const { func_interp * func_interp::translate(ast_translation & translator) const {
func_interp * new_fi = alloc(func_interp, m_manager, m_arity); func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
ptr_vector<func_entry>::const_iterator it = m_entries.begin(); ptr_vector<func_entry>::const_iterator it = m_entries.begin();
ptr_vector<func_entry>::const_iterator end = m_entries.end(); ptr_vector<func_entry>::const_iterator end = m_entries.end();

1
src/model/model.cpp
View file

@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) {
void model::register_decl(func_decl * d, func_interp * fi) { void model::register_decl(func_decl * d, func_interp * fi) {
SASSERT(d->get_arity() > 0); SASSERT(d->get_arity() > 0);
SASSERT(&fi->m() == &m_manager);
decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0); decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
if (entry->get_data().m_value == 0) { if (entry->get_data().m_value == 0) {
// new entry // new entry

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/sat/sat_clause.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include<memory.h> #include<memory.h>
#include"sat_clause.h" #include"sat_clause.h"
#include"z3_exception.h" #include"z3_exception.h"
#include"trace.h"
namespace sat { namespace sat {
@ -173,6 +174,7 @@ namespace sat {
} }
void clause_allocator::del_clause(clause * cls) { void clause_allocator::del_clause(clause * cls) {
TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
m_id_gen.recycle(cls->id()); m_id_gen.recycle(cls->id());
size_t size = clause::get_obj_size(cls->m_capacity); size_t size = clause::get_obj_size(cls->m_capacity);
#ifdef _AMD64_ #ifdef _AMD64_

5
src/sat/sat_elim_eqs.cpp
View file

@ -128,6 +128,11 @@ namespace sat {
if (j == 0) { if (j == 0) {
// empty clause // empty clause
m_solver.set_conflict(justification()); m_solver.set_conflict(justification());
for (; it != end; ++it) {
*it2 = *it;
it2++;
}
cs.set_end(it2);
return; return;
} }
TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";); TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);

19
src/sat/sat_integrity_checker.cpp
View file

@ -207,6 +207,24 @@ namespace sat {
} }
return true; return true;
} }
bool integrity_checker::check_disjoint_clauses() const {
uint_set ids;
clause_vector::const_iterator it = s.m_clauses.begin();
clause_vector::const_iterator end = s.m_clauses.end();
for (; it != end; ++it) {
ids.insert((*it)->id());
}
it = s.m_learned.begin();
end = s.m_learned.end();
for (; it != end; ++it) {
if (ids.contains((*it)->id())) {
TRACE("sat", tout << "Repeated clause: " << (*it)->id() << "\n";);
return false;
}
}
return true;
}
bool integrity_checker::operator()() const { bool integrity_checker::operator()() const {
if (s.inconsistent()) if (s.inconsistent())
@ -216,6 +234,7 @@ namespace sat {
SASSERT(check_watches()); SASSERT(check_watches());
SASSERT(check_bool_vars()); SASSERT(check_bool_vars());
SASSERT(check_reinit_stack()); SASSERT(check_reinit_stack());
SASSERT(check_disjoint_clauses());
return true; return true;
} }
}; };

1
src/sat/sat_integrity_checker.h
View file

@ -36,6 +36,7 @@ namespace sat {
bool check_bool_vars() const; bool check_bool_vars() const;
bool check_watches() const; bool check_watches() const;
bool check_reinit_stack() const; bool check_reinit_stack() const;
bool check_disjoint_clauses() const;
bool operator()() const; bool operator()() const;
}; };
}; };

1
src/sat/sat_simplifier.cpp
View file

@ -227,6 +227,7 @@ namespace sat {
} }
void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) { void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
TRACE("sat", tout << "cleanup_clauses\n";);
clause_vector::iterator it = cs.begin(); clause_vector::iterator it = cs.begin();
clause_vector::iterator it2 = it; clause_vector::iterator it2 = it;
clause_vector::iterator end = cs.end(); clause_vector::iterator end = cs.end();

5
src/sat/sat_solver.cpp
View file

@ -50,7 +50,10 @@ namespace sat {
} }
solver::~solver() { solver::~solver() {
SASSERT(check_invariant());
TRACE("sat", tout << "Delete clauses\n";);
del_clauses(m_clauses.begin(), m_clauses.end()); del_clauses(m_clauses.begin(), m_clauses.end());
TRACE("sat", tout << "Delete learned\n";);
del_clauses(m_learned.begin(), m_learned.end()); del_clauses(m_learned.begin(), m_learned.end());
} }
@ -1121,6 +1124,7 @@ namespace sat {
\brief GC (the second) half of the clauses in the database. \brief GC (the second) half of the clauses in the database.
*/ */
void solver::gc_half(char const * st_name) { void solver::gc_half(char const * st_name) {
TRACE("sat", tout << "gc\n";);
unsigned sz = m_learned.size(); unsigned sz = m_learned.size();
unsigned new_sz = sz/2; unsigned new_sz = sz/2;
unsigned j = new_sz; unsigned j = new_sz;
@ -1145,6 +1149,7 @@ namespace sat {
\brief Use gc based on dynamic psm. Clauses are initially frozen. \brief Use gc based on dynamic psm. Clauses are initially frozen.
*/ */
void solver::gc_dyn_psm() { void solver::gc_dyn_psm() {
TRACE("sat", tout << "gc\n";);
// To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact // To do gc at scope_lvl() > 0, I will need to use the reinitialization stack, or live with the fact
// that I may miss some propagations for reactivated clauses. // that I may miss some propagations for reactivated clauses.
SASSERT(scope_lvl() == 0); SASSERT(scope_lvl() == 0);

6
src/sat/sat_solver.h
View file

@ -89,7 +89,7 @@ namespace sat {
clause_vector m_learned; clause_vector m_learned;
unsigned m_num_frozen; unsigned m_num_frozen;
vector<watch_list> m_watches; vector<watch_list> m_watches;
svector<lbool> m_assignment; char_vector m_assignment;
svector<justification> m_justification; svector<justification> m_justification;
svector<char> m_decision; svector<char> m_decision;
svector<char> m_mark; svector<char> m_mark;
@ -200,8 +200,8 @@ namespace sat {
bool is_external(bool_var v) const { return m_external[v] != 0; } bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
lbool value(literal l) const { return m_assignment[l.index()]; } lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; } lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; } unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; } unsigned lvl(literal l) const { return m_level[l.var()]; }
void assign(literal l, justification j) { void assign(literal l, justification j) {

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);

2
src/smt/database.h
View file

@ -1,4 +1,4 @@
static char const * g_pattern_database = static char const g_pattern_database[] =
"(benchmark patterns \n" "(benchmark patterns \n"
" :status unknown \n" " :status unknown \n"
" :logic ALL \n" " :logic ALL \n"

22
src/smt/params/dyn_ack_params.cpp
View file

@ -17,16 +17,14 @@ Revision History:
--*/ --*/
#include"dyn_ack_params.h" #include"dyn_ack_params.h"
#include"smt_params_helper.hpp"
#if 0 void dyn_ack_params::updt_params(params_ref const & _p) {
void dyn_ack_params::register_params(ini_params & p) { smt_params_helper p(_p);
p.register_int_param("dack", 0, 2, reinterpret_cast<int&>(m_dack), m_dack = static_cast<dyn_ack_strategy>(p.dack());
"0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); m_dack_eq = p.dack_eq();
p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); m_dack_factor = p.dack_factor();
p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); m_dack_threshold = p.dack_threshold();
p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict"); m_dack_gc = p.dack_gc();
p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); m_dack_gc_inv_decay = p.dack_gc_inv_decay();
p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); }
}
#endif

6
src/smt/params/dyn_ack_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef _DYN_ACK_PARAMS_H_ #ifndef _DYN_ACK_PARAMS_H_
#define _DYN_ACK_PARAMS_H_ #define _DYN_ACK_PARAMS_H_
#include"params.h"
enum dyn_ack_strategy { enum dyn_ack_strategy {
DACK_DISABLED, DACK_DISABLED,
DACK_ROOT, // congruence is the root of the conflict DACK_ROOT, // congruence is the root of the conflict
@ -34,15 +36,17 @@ struct dyn_ack_params {
double m_dack_gc_inv_decay; double m_dack_gc_inv_decay;
public: public:
dyn_ack_params(): dyn_ack_params(params_ref const & p = params_ref()) :
m_dack(DACK_ROOT), m_dack(DACK_ROOT),
m_dack_eq(false), m_dack_eq(false),
m_dack_factor(0.1), m_dack_factor(0.1),
m_dack_threshold(10), m_dack_threshold(10),
m_dack_gc(2000), m_dack_gc(2000),
m_dack_gc_inv_decay(0.8) { m_dack_gc_inv_decay(0.8) {
updt_params(p);
} }
void updt_params(params_ref const & _p);
}; };

1
src/smt/params/smt_params.cpp
View file

@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
void smt_params::updt_params(params_ref const & p) { void smt_params::updt_params(params_ref const & p) {
preprocessor_params::updt_params(p); preprocessor_params::updt_params(p);
dyn_ack_params::updt_params(p);
qi_params::updt_params(p); qi_params::updt_params(p);
theory_arith_params::updt_params(p); theory_arith_params::updt_params(p);
theory_bv_params::updt_params(p); theory_bv_params::updt_params(p);

8
src/smt/params/smt_params_helper.pyg
View file

@ -45,5 +45,11 @@ def_module_params(module_name='smt',
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('array.weak', BOOL, False, 'weak array theory'), ('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory') ('array.extensional', BOOL, True, 'extensional array theory'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
)) ))

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);
} }
} }

6
src/tactic/sls/sls_engine.cpp
View file

@ -555,8 +555,12 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
mc = 0; mc = 0;
} }
lbool sls_engine::operator()() { lbool sls_engine::operator()() {
m_tracker.initialize(m_assertions); m_tracker.initialize(m_assertions);
m_tracker.reset(m_assertions);
if (m_restart_init)
m_tracker.randomize(m_assertions);
lbool res = l_undef; lbool res = l_undef;
do { do {

11
src/util/bit_vector.cpp
View file

@ -25,13 +25,12 @@ Revision History:
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1) #define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
void bit_vector::expand_to(unsigned new_capacity) { void bit_vector::expand_to(unsigned new_capacity) {
unsigned * new_data = alloc_svect(unsigned, new_capacity); if (m_data) {
memset(new_data, 0, new_capacity * sizeof(unsigned)); m_data = (unsigned*)memory::reallocate(m_data, new_capacity * sizeof(unsigned));
if (m_capacity > 0) { } else {
memcpy(new_data, m_data, m_capacity * sizeof(unsigned)); m_data = alloc_svect(unsigned, new_capacity);
dealloc_svect(m_data);
} }
m_data = new_data; memset(m_data + m_capacity, 0, (new_capacity - m_capacity) * sizeof(unsigned));
m_capacity = new_capacity; m_capacity = new_capacity;
} }

4
src/util/bit_vector.h
View file

@ -87,9 +87,7 @@ public:
} }
~bit_vector() { ~bit_vector() {
if (m_data) { dealloc_svect(m_data);
dealloc_svect(m_data);
}
} }
void reset() { void reset() {

46
src/util/memory_manager.cpp
View file

@ -60,7 +60,7 @@ static void throw_out_of_memory() {
} }
#ifdef PROFILE_MEMORY #ifdef PROFILE_MEMORY
unsigned g_synch_counter = 0; static unsigned g_synch_counter = 0;
class mem_usage_report { class mem_usage_report {
public: public:
~mem_usage_report() { ~mem_usage_report() {
@ -173,6 +173,7 @@ void memory::display_i_max_usage(std::ostream & os) {
<< "\n"; << "\n";
} }
#if _DEBUG
void memory::deallocate(char const * file, int line, void * p) { void memory::deallocate(char const * file, int line, void * p) {
deallocate(p); deallocate(p);
TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";);); TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";););
@ -183,6 +184,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
TRACE("memory", tout << "alloc " << std::hex << r << std::dec << " " << file << ":" << line << " " << obj << " " << s << "\n";); TRACE("memory", tout << "alloc " << std::hex << r << std::dec << " " << file << ":" << line << " " << obj << " " << s << "\n";);
return r; return r;
} }
#endif
#if defined(_WINDOWS) || defined(_USE_THREAD_LOCAL) #if defined(_WINDOWS) || defined(_USE_THREAD_LOCAL)
// ================================== // ==================================
@ -250,6 +252,24 @@ void * memory::allocate(size_t s) {
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
} }
void* memory::reallocate(void *p, size_t s) {
size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
size_t sz = *sz_p;
void *real_p = reinterpret_cast<void*>(sz_p);
s = s + sizeof(size_t); // we allocate an extra field!
g_memory_thread_alloc_size += s - sz;
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
synchronize_counters(true);
}
void *r = realloc(real_p, s);
if (r == 0)
throw_out_of_memory();
*(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
#else #else
// ================================== // ==================================
// ================================== // ==================================
@ -290,5 +310,29 @@ void * memory::allocate(size_t s) {
*(static_cast<size_t*>(r)) = s; *(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
} }
void* memory::reallocate(void *p, size_t s) {
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
size_t sz = *sz_p;
void * real_p = reinterpret_cast<void*>(sz_p);
s = s + sizeof(size_t); // we allocate an extra field!
bool out_of_mem = false;
#pragma omp critical (z3_memory_manager)
{
g_memory_alloc_size += s - sz;
if (g_memory_alloc_size > g_memory_max_used_size)
g_memory_max_used_size = g_memory_alloc_size;
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
out_of_mem = true;
}
if (out_of_mem)
throw_out_of_memory();
void *r = realloc(real_p, s);
if (r == 0)
throw_out_of_memory();
*(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
#endif #endif

28
src/util/memory_manager.h
View file

@ -23,6 +23,24 @@ Revision History:
#include<ostream> #include<ostream>
#include"z3_exception.h" #include"z3_exception.h"
#ifndef __has_builtin
# define __has_builtin(x) 0
#endif
#ifdef __GNUC__
# if (__GNUC__ * 100 + __GNUC_MINOR__) >= 409 || __has_builtin(returns_nonnull)
# define GCC_RET_NON_NULL __attribute__((returns_nonnull))
# else
# define GCC_RET_NON_NULL
# endif
# define ALLOC_ATTR __attribute__((malloc)) GCC_RET_NON_NULL
#elif defined(_WINDOWS)
# define ALLOC_ATTR __declspec(restrict)
#else
# define ALLOC_ATTR
#endif
class out_of_memory_error : public z3_error { class out_of_memory_error : public z3_error {
public: public:
out_of_memory_error(); out_of_memory_error();
@ -39,9 +57,12 @@ public:
static void display_max_usage(std::ostream& os); static void display_max_usage(std::ostream& os);
static void display_i_max_usage(std::ostream& os); static void display_i_max_usage(std::ostream& os);
static void deallocate(void* p); static void deallocate(void* p);
static void* allocate(size_t s); static ALLOC_ATTR void* allocate(size_t s);
static ALLOC_ATTR void* reallocate(void *p, size_t s);
#if _DEBUG
static void deallocate(char const* file, int line, void* p); static void deallocate(char const* file, int line, void* p);
static void* allocate(char const* file, int line, char const* obj, size_t s); static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
#endif
static unsigned long long get_allocation_size(); static unsigned long long get_allocation_size();
static unsigned long long get_max_used_memory(); static unsigned long long get_max_used_memory();
// temporary hack to avoid out-of-memory crash in z3.exe // temporary hack to avoid out-of-memory crash in z3.exe
@ -74,6 +95,9 @@ void dealloc(T * ptr) {
#endif #endif
template<typename T>
ALLOC_ATTR T * alloc_vect(unsigned sz);
template<typename T> template<typename T>
T * alloc_vect(unsigned sz) { T * alloc_vect(unsigned sz) {
T * r = static_cast<T*>(memory::allocate(sizeof(T) * sz)); T * r = static_cast<T*>(memory::allocate(sizeof(T) * sz));

4
src/util/util.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include"util.h" #include"util.h"
unsigned g_verbosity_level = 0; static unsigned g_verbosity_level = 0;
void set_verbosity_level(unsigned lvl) { void set_verbosity_level(unsigned lvl) {
g_verbosity_level = lvl; g_verbosity_level = lvl;
@ -40,7 +40,7 @@ std::ostream& verbose_stream() {
} }
void (*g_fatal_error_handler)(int) = 0; static void (*g_fatal_error_handler)(int) = 0;
void fatal_error(int error_code) { void fatal_error(int error_code) {
if (g_fatal_error_handler) { if (g_fatal_error_handler) {

12
src/util/vector.h
View file

@ -71,18 +71,12 @@ class vector {
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2; SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1; SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2; SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
SZ size = reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) { if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector"); throw default_exception("Overflow encountered when expanding vector");
} }
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(new_capacity_T)); SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
*mem = new_capacity; *mem = new_capacity;
mem ++; m_data = reinterpret_cast<T *>(mem + 2);
*mem = size;
mem++;
memcpy(mem, m_data, size * sizeof(T));
free_memory();
m_data = reinterpret_cast<T *>(mem);
} }
} }