diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index a02a9b40f..f003dd12c 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -82,6 +82,7 @@ JAVA_ENABLED=False
ML_ENABLED=False
PYTHON_INSTALL_ENABLED=False
STATIC_LIB=False
+STATIC_BIN=False
VER_MAJOR=None
VER_MINOR=None
VER_BUILD=None
@@ -532,6 +533,9 @@ def get_version():
def build_static_lib():
return STATIC_LIB
+def build_static_bin():
+ return STATIC_BIN
+
def is_cr_lf(fname):
# Check whether text files use cr/lf
f = open(fname, 'r')
@@ -616,6 +620,7 @@ def display_help(exit_code):
print(" --ml generate OCaml bindings.")
print(" --python generate Python bindings.")
print(" --staticlib build Z3 static library.")
+ print(" --staticbin build a statically linked Z3 binary.")
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
@@ -646,14 +651,14 @@ def display_help(exit_code):
# Parse configuration option for mk_make script
def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
- global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED
+ global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
try:
options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
- 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python'])
+ 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
except:
print("ERROR: Invalid command line option")
display_help(1)
@@ -688,6 +693,8 @@ def parse_options():
DOTNET_ENABLED = True
elif opt in ('--staticlib'):
STATIC_LIB = True
+ elif opt in ('--staticbin'):
+ STATIC_BIN = True
elif opt in ('--optimize'):
SLOW_OPTIMIZE = True
elif not IS_WINDOWS and opt in ('-p', '--prefix'):
@@ -2189,14 +2196,19 @@ def mk_config():
extra_opt = ' -D_NO_OMP_'
if GIT_HASH:
extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
+ if STATIC_BIN:
+ static_opt = '/MT'
+ else:
+ static_opt = '/MD'
if DEBUG_MODE:
+ static_opt = static_opt + 'd'
config.write(
'AR_FLAGS=/nologo\n'
- 'LINK_FLAGS=/nologo /MDd\n'
- 'SLINK_FLAGS=/nologo /LDd\n')
+ 'LINK_FLAGS=/nologo %s\n'
+ 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
if VS_X64:
config.write(
- 'CXXFLAGS=/c /Zi /nologo /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 /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_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')
@@ -2205,7 +2217,7 @@ def mk_config():
exit(1)
else:
config.write(
- 'CXXFLAGS=/c /Zi /nologo /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 /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_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')
@@ -2214,15 +2226,14 @@ def mk_config():
LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
GL = ' /GL' if SLOW_OPTIMIZE else ''
config.write(
- 'AR_FLAGS=/nologo%s\n'
- 'LINK_FLAGS=/nologo /MD\n'
- 'SLINK_FLAGS=/nologo /LD\n'
- % LTCG)
+ 'AR_FLAGS=/nologo %s\n'
+ 'LINK_FLAGS=/nologo %s\n'
+ 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt))
if TRACE:
extra_opt = '%s /D _TRACE ' % extra_opt
if VS_X64:
config.write(
- 'CXXFLAGS=/c%s /Zi /nologo /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' % (GL, extra_opt))
+ 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt))
config.write(
'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG))
@@ -2231,7 +2242,7 @@ def mk_config():
exit(1)
else:
config.write(
- 'CXXFLAGS=/nologo /c%s /Zi /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' % (GL, extra_opt))
+ 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
config.write(
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG))
@@ -2340,7 +2351,9 @@ def mk_config():
LDFLAGS = '%s -m32' % LDFLAGS
SLIBFLAGS = '%s -m32' % SLIBFLAGS
if DEBUG_MODE:
- CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS
+ CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
+ else:
+ CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
if TRACE or DEBUG_MODE:
CPPFLAGS = '%s -D_TRACE' % CPPFLAGS
config.write('PREFIX=%s\n' % PREFIX)
@@ -2356,7 +2369,10 @@ def mk_config():
config.write('AR_OUTFLAG=\n')
config.write('EXE_EXT=\n')
config.write('LINK=%s\n' % CXX)
- config.write('LINK_FLAGS=\n')
+ if STATIC_BIN:
+ config.write('LINK_FLAGS=-static\n')
+ else:
+ config.write('LINK_FLAGS=\n')
config.write('LINK_OUT_FLAG=-o \n')
config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
config.write('SO_EXT=%s\n' % SO_EXT)
@@ -3457,7 +3473,7 @@ def mk_vs_proj_cl_compile(f, name, components, debug):
if debug:
f.write(' WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n')
else:
- f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n')
+ f.write(' WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n')
if VS_PAR:
f.write(' false\n')
f.write(' true\n')
diff --git a/scripts/update_api.py b/scripts/update_api.py
index fc0f1c939..badd960cc 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }
log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
log_h.write('void _Z3_append_log(char const * msg);\n')
##
-exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
+exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
##
core_py.write('# Automatically generated file\n')
core_py.write('import sys, os\n')
@@ -1068,7 +1068,7 @@ def def_API(name, result, params):
if is_obj(result):
exe_c.write(" in.store_result(result);\n")
if name == 'Z3_mk_context' or name == 'Z3_mk_context_rc':
- exe_c.write(" Z3_set_error_handler(result, Z3_replacer_error_handler);")
+ exe_c.write(" Z3_set_error_handler(result, Z3_replayer_error_handler);")
log_c.write('}\n')
exe_c.write('}\n')
mk_log_macro(log_h, name, params)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 3a4276dfd..088cd0d4d 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -8524,11 +8524,11 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
>>> v = FPVal(-2.25, FPSort(8, 24))
>>> v
-1.125*(2**1)
- >>> v = FPVal(-0.0, FPSort(8, 24))
+ >>> FPVal(-0.0, FPSort(8, 24))
-0.0
- >>> v = FPVal(0.0, FPSort(8, 24))
+ >>> FPVal(0.0, FPSort(8, 24))
+0.0
- >>> v = FPVal(+0.0, FPSort(8, 24))
+ >>> FPVal(+0.0, FPSort(8, 24))
+0.0
"""
ctx = _get_ctx(ctx)
@@ -8911,7 +8911,7 @@ def fpNEQ(a, b, ctx=None):
>>> fpNEQ(x, y)
Not(fpEQ(x, y))
>>> (x != y).sexpr()
- '(not (fp.eq x y))'
+ '(distinct x y)'
"""
return Not(fpEQ(a, b, ctx))
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 55a1b93d9..5c7a819da 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -62,7 +62,7 @@ DEFINE_TYPE(Z3_rcf_num);
- \c Z3_constructor: type constructor for a (recursive) datatype.
- \c Z3_constructor_list: list of constructors for a (recursive) datatype.
- \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc.
- - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
+ - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters.
- \c Z3_model: model for the constraints asserted into the logical context.
- \c Z3_func_interp: interpretation of a function in a model.
- \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point.
@@ -1129,7 +1129,7 @@ typedef enum {
Z3_OP_SEQ_EXTRACT,
Z3_OP_SEQ_REPLACE,
Z3_OP_SEQ_AT,
- Z3_OP_SEQ_LENGTH,
+ Z3_OP_SEQ_LENGTH,
Z3_OP_SEQ_INDEX,
Z3_OP_SEQ_TO_RE,
Z3_OP_SEQ_IN_RE,
@@ -1457,7 +1457,7 @@ extern "C" {
/*@{*/
/**
- \deprecated
+ \deprecated
\brief Create a context using the given configuration.
After a context is created, the configuration cannot be changed,
@@ -1474,6 +1474,11 @@ extern "C" {
Z3_solver, Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context.
+ Further remarks:
+ - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
+ - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
+ Z3 will return the same pointer twice.
+
\sa Z3_del_context
def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),))
@@ -1492,11 +1497,13 @@ extern "C" {
anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD.
- Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are
- Z3_ast's.
+ Remarks:
- After a context is created, the configuration cannot be changed.
- All main interaction with Z3 happens in the context of a \c Z3_context.
+ - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
+ - After a context is created, the configuration cannot be changed.
+ - All main interaction with Z3 happens in the context of a \c Z3_context.
+ - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
+ Z3 will return the same pointer twice.
def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),))
*/
@@ -3185,11 +3192,11 @@ extern "C" {
def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST)))
*/
- Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
+ Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s);
/**
\brief Retrieve the string constant stored in \c s.
-
+
\pre Z3_is_string(c, s)
def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST)))
@@ -3285,7 +3292,7 @@ extern "C" {
def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
-
+
/**
\brief Create a regular expression that accepts the sequence \c seq.
@@ -4429,8 +4436,8 @@ extern "C" {
Provides an interface to the AST simplifier used by Z3.
It returns an AST object which is equal to the argument.
- The returned AST is simplified using algebraic simplificaiton rules,
- such as constant propagation (propagating true/false over logical connectives).
+ The returned AST is simplified using algebraic simplificaiton rules,
+ such as constant propagation (propagating true/false over logical connectives).
def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
*/
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 40bb7efe8..0d90e1c5a 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
- tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
+ tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
}
@@ -113,9 +113,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a
result = m.mk_true();
for (unsigned i = 0; i < num; i++) {
for (unsigned j = i+1; j < num; j++) {
- expr_ref eq(m);
+ expr_ref eq(m), neq(m);
mk_eq(args[i], args[j], eq);
- m_simp.mk_and(result, m.mk_not(eq), result);
+ neq = m.mk_not(eq);
+ m_simp.mk_and(result, neq, result);
}
}
}
@@ -422,10 +423,11 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
if (log2(sbits + 2) < ebits + 2)
{
// cap the delta
- expr_ref cap(m), cap_le_delta(m);
+ expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m);
cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2);
cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta));
- m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta);
+ exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta);
+ m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta);
exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta);
dbg_decouple("fpa2bv_add_exp_cap", cap);
}
@@ -465,7 +467,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
expr_ref eq_sgn(m);
m_simp.mk_eq(c_sgn, d_sgn, eq_sgn);
- // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
+ dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; );
// two extra bits for catching the overflow.
@@ -478,11 +480,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
dbg_decouple("fpa2bv_add_c_sig", c_sig);
dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig);
- expr_ref sum(m);
- m_simp.mk_ite(eq_sgn,
- m_bv_util.mk_bv_add(c_sig, shifted_d_sig),
- m_bv_util.mk_bv_sub(c_sig, shifted_d_sig),
- sum);
+ expr_ref sum(m), c_plus_d(m), c_minus_d(m);
+ c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig);
+ c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig);
+ m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum);
SASSERT(is_well_sorted(m, sum));
@@ -594,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
c6 = y_is_zero;
v6 = x;
- // Actual addition.
+ //// Actual addition.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
@@ -949,8 +950,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount);
expr_ref shift_cond(m);
shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4));
- m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig);
- m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp);
+ expr_ref res_sig_shifted(m), res_exp_shifted(m);
+ res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount);
+ res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount));
+ m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
+ m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8);
@@ -1374,8 +1378,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
// (x is 0) || (y is 0) -> z
m_simp.mk_or(x_is_zero, y_is_zero, c7);
- expr_ref ite_c(m);
- m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c);
+ expr_ref ite_c(m), rm_is_not_to_neg(m);
+ rm_is_not_to_neg = m.mk_not(rm_is_to_neg);
+ m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c);
mk_ite(ite_c, pzero, z, v7);
// else comes the fused multiplication.
@@ -1512,11 +1517,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
- expr_ref sum(m);
- m_simp.mk_ite(eq_sgn,
- m_bv_util.mk_bv_add(e_sig, shifted_f_sig),
- m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
- sum);
+ expr_ref sum(m), e_plus_f(m), e_minus_f(m);
+ e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
+ e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
+ m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
SASSERT(is_well_sorted(m, sum));
@@ -1664,10 +1668,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd);
dbg_decouple("fpa2bv_sqrt_real_exp", real_exp);
- expr_ref sig_prime(m);
- m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1),
- m_bv_util.mk_concat(zero1, a_sig),
- sig_prime);
+ expr_ref sig_prime(m), a_z(m), z_a(m);
+ a_z = m_bv_util.mk_concat(a_sig, zero1);
+ z_a = m_bv_util.mk_concat(zero1, a_sig);
+ m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime);
SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1);
dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime);
@@ -1696,21 +1700,22 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(S) == sbits + 5);
SASSERT(m_bv_util.get_bv_size(T) == sbits + 6);
- expr_ref t_lt_0(m);
- m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0);
+ expr_ref t_lt_0(m), T_lsds5(m);
+ T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T);
+ m_simp.mk_eq(T_lsds5, one1, t_lt_0);
expr * or_args[2] = { Q, S };
-
- m_simp.mk_ite(t_lt_0, Q,
- m_bv_util.mk_bv_or(2, or_args),
- Q);
- m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1),
- m_bv_util.mk_extract(sbits+4, 0, T),
- R);
+ expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m);
+ Q_or_S = m_bv_util.mk_bv_or(2, or_args);
+ m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q);
+ R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1);
+ T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T);
+ m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R);
}
- expr_ref is_exact(m);
- m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact);
+ expr_ref is_exact(m), zero_sbits5(m);
+ zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5);
+ m_simp.mk_eq(R, zero_sbits5, is_exact);
dbg_decouple("fpa2bv_sqrt_is_exact", is_exact);
expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m);
@@ -1719,10 +1724,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_sqrt_last", last);
dbg_decouple("fpa2bv_sqrt_rest", rest);
rest_ext = m_bv_util.mk_zero_extend(1, rest);
- expr_ref sticky(m);
- m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last),
- m_bv_util.mk_numeral(1, sbits+4),
- sticky);
+ expr_ref sticky(m), last_ext(m), one_sbits4(m);
+ last_ext = m_bv_util.mk_zero_extend(sbits + 3, last);
+ one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4);
+ m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky);
expr * or_args[2] = { rest_ext, sticky };
res_sig = m_bv_util.mk_bv_or(2, or_args);
@@ -1813,8 +1818,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
mk_one(f, one_1, none);
mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone);
- m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1);
- m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2);
+ expr_ref pow_2_sbitsm1(m), m1(m);
+ pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits);
+ m1 = m_bv_util.mk_numeral(-1, ebits);
+ m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1);
+ m_simp.mk_eq(a_exp, m1, t2);
m_simp.mk_and(t1, t2, tie);
dbg_decouple("fpa2bv_r2i_c42_tie", tie);
@@ -1896,14 +1904,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
SASSERT(is_well_sorted(m, tie2_c));
SASSERT(is_well_sorted(m, v51));
- expr_ref c521(m), v52(m);
- m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521);
- m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521);
+ expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m);
+ rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1));
+ sgn_eq_zero = m.mk_eq(res_sgn, zero_1);
+ m_simp.mk_not(rem_eq_0, c521);
+ m_simp.mk_and(c521, sgn_eq_zero, c521);
m_simp.mk_ite(c521, div_p1, div, v52);
- expr_ref c531(m), v53(m);
- m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531);
- m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531);
+ expr_ref c531(m), v53(m), sgn_eq_one(m);
+ sgn_eq_one = m.mk_eq(res_sgn, one_1);
+ m_simp.mk_not(rem_eq_0, c531);
+ m_simp.mk_and(c531, sgn_eq_one, c531);
m_simp.mk_ite(c531, div_p1, div, v53);
expr_ref c51(m), c52(m), c53(m);
@@ -3377,9 +3388,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
zero_s = m_bv_util.mk_numeral(0, sbits);
m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero);
- expr_ref lz_d(m);
+ expr_ref lz_d(m), norm_or_zero(m);
mk_leading_zeros(denormal_sig, ebits, lz_d);
- m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz);
+ norm_or_zero = m.mk_or(is_normal, is_sig_zero);
+ m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz);
dbg_decouple("fpa2bv_unpack_lz", lz);
expr_ref shift(m);
@@ -3770,8 +3782,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos);
- expr_ref sgn_is_zero(m);
- m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero);
+ expr_ref sgn_is_zero(m), zero1(m);
+ zero1 = m_bv_util.mk_numeral(0, 1);
+ m_simp.mk_eq(sgn, zero1, sgn_is_zero);
dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero);
expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m);
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 65d99d2c8..8dc3dc019 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -26,19 +26,6 @@ Notes:
#include"bv_decl_plugin.h"
#include"basic_simplifier_plugin.h"
-struct func_decl_triple {
- func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; }
- func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp)
- {
- f_sgn = sgn;
- f_sig = sig;
- f_exp = exp;
- }
- func_decl * f_sgn;
- func_decl * f_sig;
- func_decl * f_exp;
- };
-
class fpa2bv_converter {
protected:
ast_manager & m;
diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp
index 45a87087c..188a73e95 100644
--- a/src/ast/fpa/fpa2bv_rewriter.cpp
+++ b/src/ast/fpa/fpa2bv_rewriter.cpp
@@ -66,7 +66,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
m_conv.mk_rm_const(f, result);
return BR_DONE;
- }
+ }
if (m().is_eq(f)) {
SASSERT(num == 2);
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index 7bfc60be4..a130c445b 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -25,8 +25,8 @@ Notes:
#include"fpa2bv_converter.h"
struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
- ast_manager & m_manager;
- expr_ref_vector m_out;
+ ast_manager & m_manager;
+ expr_ref_vector m_out;
fpa2bv_converter & m_conv;
sort_ref_vector m_bindings;
@@ -37,7 +37,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p);
- ~fpa2bv_rewriter_cfg() {
+ ~fpa2bv_rewriter_cfg() {
}
void cleanup_buffers() {
@@ -55,12 +55,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
-
bool pre_visit(expr * t);
- bool reduce_quantifier(quantifier * old_q,
- expr * new_body,
- expr * const * new_patterns,
+ bool reduce_quantifier(quantifier * old_q,
+ expr * new_body,
+ expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr);
@@ -73,7 +72,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
struct fpa2bv_rewriter : public rewriter_tpl {
fpa2bv_rewriter_cfg m_cfg;
fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
- rewriter_tpl(m, m.proofs_enabled(), m_cfg),
+ rewriter_tpl(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 550171ab5..d45a4b092 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -61,7 +61,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_ADD: st = mk_add_core(num_args, args, result); break;
case OP_MUL: st = mk_mul_core(num_args, args, result); break;
case OP_SUB: st = mk_sub(num_args, args, result); break;
- case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
+ case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
@@ -294,7 +294,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) {
for (unsigned i = 0; i < sz; i++) {
expr * arg = args[i];
expr * arg0, *arg1;
- if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
+ if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() &&
((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) {
if (is_eq || !k.is_even()) {
new_args.push_back(arg0);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 1c156d83e..7feed9fb1 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -151,6 +151,7 @@ public:
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm);
+ SASSERT(sz == m_asms.size());
if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@@ -300,6 +301,7 @@ private:
lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
if (sz == 0) {
+ m_asms.shrink(0);
return l_true;
}
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
@@ -331,6 +333,7 @@ private:
sat::literal lit;
for (unsigned i = 0; i < sz; ++i) {
if (dep2asm.find(asms[i], lit)) {
+ SASSERT(lit.var() <= m_solver.num_vars());
m_asms.push_back(lit);
if (i != j && !m_weights.empty()) {
m_weights[j] = m_weights[i];
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index cfedb66d7..28597c6ec 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -91,11 +91,10 @@ class fpa2bv_tactic : public tactic {
// that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
// has a value to propagate.
expr * sgn, *sig, *exp;
- expr_ref top_exp(m);
m_conv.split_fp(new_curr, sgn, exp, sig);
- m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1));
- m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)));
- m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)));
+ result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
+ result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))));
+ result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))));
}
}
}
@@ -155,7 +154,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
- std::swap(d, m_imp);
+ std::swap(d, m_imp);
dealloc(d);
}