3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

make proto-model evaluation use model_evaluator instead of legacy evaluator

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-05 10:27:19 -08:00
commit 640308b546
11 changed files with 138 additions and 114 deletions

View file

@ -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(' <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
else:
f.write(' <PreprocessorDefinitions>WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
f.write(' <PreprocessorDefinitions>WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
if VS_PAR:
f.write(' <MinimalRebuild>false</MinimalRebuild>\n')
f.write(' <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')

View file

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

View file

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

View file

@ -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)))
*/

View file

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

View file

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

View file

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

View file

@ -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> {
fpa2bv_rewriter_cfg m_cfg;
fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p):
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
rewriter_tpl<fpa2bv_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, c, p) {
}
};

View file

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

View file

@ -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];

View file

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