Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

mk_util.py, fix tabs/spaces mix, remove trailing whitespace, remove unused modules #74

Closed
wants to merge 6 commits into from
Closed

mk_util.py, fix tabs/spaces mix, remove trailing whitespace, remove unused modules #74

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8c9afa4
Bumped version number to 4.4.1 in unstable.
wintersteiger Apr 29, 2015
c0dc08e
Added configuration checks for floating-point build flags.
wintersteiger Apr 30, 2015
57af3a4
FPA min/max refactoring and fixes.
wintersteiger May 4, 2015
7dcdecf
fix mixed tab/spaces indent
cao May 5, 2015
f458423
remove trailing whitespace
cao May 5, 2015
0249235
remove unused modules
cao May 5, 2015
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion scripts/mk_project.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

# Z3 Project definition
def init_project_def():
set_version(4, 4, 0, 0)
set_version(4, 4, 1, 0)
add_lib('util', [])
add_lib('polynomial', ['util'], 'math/polynomial')
add_lib('sat', ['util'])
Expand Down
66 changes: 45 additions & 21 deletions scripts/mk_util.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
############################################
import sys
import os
import glob
import re
import getopt
import shutil
Expand All @@ -17,7 +16,6 @@
import distutils.sysconfig
import compileall
import subprocess
import string

def getenv(name, default):
try:
Expand Down Expand Up @@ -86,6 +84,9 @@ def getenv(name, default):
GPROF=False
GIT_HASH=False

FPMATH="Default"
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"

def check_output(cmd):
return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n')

Expand Down Expand Up @@ -237,6 +238,27 @@ def test_openmp(cc):
else:
return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0

def test_fpmath(cc):
global FPMATH_FLAGS
if is_verbose():
print("Testing floating point support...")
t = TempFile('tstsse.cpp')
t.add('int main() { return 42; }\n')
t.commit()
if exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpmath=sse -msse -msse2']) == 0:
FPMATH_FLAGS="-mfpmath=sse -msse -msse2"
return "SSE2-GCC"
elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-msse -msse2']) == 0:
FPMATH_FLAGS="-msse -msse2"
return "SSE2-CLANG"
elif exec_compiler_cmd([cc, CPPFLAGS, 'tstsse.cpp', LDFLAGS, '-mfpu=vfp -mfloat-abi=hard']) == 0:
FPMATH_FLAGS="-mfpu=vfp -mfloat-abi=hard"
return "ARM-VFP"
else:
FPMATH_FLAGS=""
return "UNKNOWN"


def find_jni_h(path):
for root, dirs, files in os.walk(path):
for f in files:
Expand Down Expand Up @@ -388,7 +410,7 @@ def find_ml_lib():
print ('Finding OCAML_LIB...')
t = TempFile('output')
null = open(os.devnull, 'wb')
try:
try:
subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
t.commit()
except:
Expand Down Expand Up @@ -529,7 +551,7 @@ def display_help(exit_code):
print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
print(" -j, --java generate Java bindings.")
print(" --ml generate OCaml bindings.")
print(" --staticlib build Z3 static library.")
print(" --staticlib build Z3 static library.")
if not IS_WINDOWS:
print(" -g, --gmp use GMP.")
print(" --gprof enable gprof")
Expand Down Expand Up @@ -1391,7 +1413,7 @@ def mk_ml_meta(self, ml_meta_in, ml_meta_out, major, minor, build, revision):
fout.close()
if VERBOSE:
print("Updated '%s'" % ml_meta_out)


def mk_makefile(self, out):
if is_ml_enabled():
Expand Down Expand Up @@ -1435,16 +1457,16 @@ def mk_makefile(self, out):
archives = archives + ' ' + os.path.join(sub_dir,m) + '.cma'
mls = mls + ' ' + os.path.join(sub_dir, m) + '.ml'

out.write('%s: %s %s\n' %
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(sub_dir, 'z3native_stubs.c'),
out.write('%s: %s %s\n' %
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
os.path.join(sub_dir, 'z3native_stubs.c'),
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
out.write('\t$(CC) $(CXXFLAGS_OCAML) -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')))

out.write('%s: %s %s %s$(SO_EXT)' % (
os.path.join(sub_dir, "z3ml.cmxa"),
cmis,
os.path.join(sub_dir, "z3ml.cmxa"),
cmis,
archives,
get_component(Z3_DLL_COMPONENT).dll_name))
out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)')))
Expand Down Expand Up @@ -1483,7 +1505,7 @@ def mk_makefile(self, out):
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
out.write('\n\n')


def main_component(self):
return is_ml_enabled()

Expand Down Expand Up @@ -1607,7 +1629,7 @@ def mk_makefile(self, out):
if ML_ENABLED:
out.write('ml_example.byte: api/ml/z3ml.cmxa ')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
out.write('\t%s ' % OCAMLC)
if DEBUG_MODE:
Expand All @@ -1618,7 +1640,7 @@ def mk_makefile(self, out):
out.write('\n')
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa ml_example.byte')
for mlfile in get_ml_files(self.ex_dir):
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
out.write('\n')
out.write('\t%s ' % OCAMLOPT)
if DEBUG_MODE:
Expand Down Expand Up @@ -1779,15 +1801,15 @@ def mk_config():
if is_verbose():
print('64-bit: %s' % is64())
print('OpenMP: %s' % HAS_OMP)
if is_java_enabled():
if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
if is_ml_enabled():
print('OCaml Compiler: %s' % OCAMLC)
print('OCaml Native: %s' % OCAMLOPT)
print('OCaml Library: %s' % OCAML_LIB)
else:
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS
OS_DEFINES = ""
ARITH = "internal"
check_ar()
Expand Down Expand Up @@ -1816,9 +1838,11 @@ def mk_config():
if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
FPMATH = test_fpmath(CXX)
CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)
HAS_OMP = test_openmp(CXX)
if HAS_OMP:
CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS
CXXFLAGS = '%s -fopenmp' % CXXFLAGS
LDFLAGS = '%s -fopenmp' % LDFLAGS
SLIBEXTRAFLAGS = '%s -fopenmp' % SLIBEXTRAFLAGS
else:
Expand Down Expand Up @@ -1871,7 +1895,6 @@ def mk_config():
CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS
if TRACE or DEBUG_MODE:
CPPFLAGS = '%s -D_TRACE' % CPPFLAGS
CXXFLAGS = '%s -msse -msse2' % CXXFLAGS
config.write('PREFIX=%s\n' % PREFIX)
config.write('CC=%s\n' % CC)
config.write('CXX=%s\n' % CXX)
Expand Down Expand Up @@ -1902,9 +1925,10 @@ def mk_config():
print('OpenMP: %s' % HAS_OMP)
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
print('FP math: %s' % FPMATH)
if GPROF:
print('gprof: enabled')
print('Python version: %s' % distutils.sysconfig.get_python_version())
print('Python version: %s' % distutils.sysconfig.get_python_version())
if is_java_enabled():
print('JNI Bindings: %s' % JNI_HOME)
print('Java Compiler: %s' % JAVAC)
Expand Down Expand Up @@ -2793,7 +2817,7 @@ def mk_z3consts_ml(api_files):
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
Expand Down Expand Up @@ -2871,7 +2895,7 @@ def mk_z3consts_ml(api_files):
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
Expand Down
84 changes: 29 additions & 55 deletions src/ast/fpa/fpa2bv_converter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1041,80 +1041,54 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
split_fp(x, x_sgn, x_exp, x_sig);
split_fp(y, y_sgn, y_exp, y_sig);

expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m);
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
mk_is_zero(x, x_is_zero);
mk_is_zero(y, y_is_zero);
m_simp.mk_and(x_is_zero, y_is_zero, c1_and);
mk_is_nan(x, x_is_nan);
m_simp.mk_or(x_is_nan, c1_and, c1);

m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
mk_is_nan(x, x_is_nan);
mk_is_nan(y, y_is_nan);
c2 = y_is_nan;

expr_ref c3(m);
mk_float_lt(f, num, args, c3);
mk_pzero(f, pzero);

expr_ref r_sgn(m), r_sig(m), r_exp(m);
expr_ref lt(m);
mk_float_lt(f, num, args, lt);

expr_ref c3xy(m), c2c3(m);
m_simp.mk_ite(c3, x_sgn, y_sgn, c3xy);
m_simp.mk_ite(c2, x_sgn, c3xy, c2c3);
m_simp.mk_ite(c1, y_sgn, c2c3, r_sgn);

expr_ref c3xy_sig(m), c2c3_sig(m);
m_simp.mk_ite(c3, x_sig, y_sig, c3xy_sig);
m_simp.mk_ite(c2, x_sig, c3xy_sig, c2c3_sig);
m_simp.mk_ite(c1, y_sig, c2c3_sig, r_sig);
result = y;
mk_ite(lt, x, result, result);
mk_ite(both_zero, pzero, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);

expr_ref c3xy_exp(m), c2c3_exp(m);
m_simp.mk_ite(c3, x_exp, y_exp, c3xy_exp);
m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp);
m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp);

mk_fp(r_sgn, r_exp, r_sig, result);
SASSERT(is_well_sorted(m, result));
}

void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);

expr * x = args[0], * y = args[1];

expr * x_sgn, * x_sig, * x_exp;
expr * y_sgn, * y_sig, * y_exp;
expr * x = args[0], *y = args[1];

expr * x_sgn, *x_sig, *x_exp;
expr * y_sgn, *y_sig, *y_exp;
split_fp(x, x_sgn, x_exp, x_sig);
split_fp(y, y_sgn, y_exp, y_sig);

expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m);
mk_is_zero(y, y_is_zero);
expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m);
mk_is_zero(x, x_is_zero);
m_simp.mk_and(y_is_zero, x_is_zero, c1_and);
mk_is_nan(x, x_is_nan);
m_simp.mk_or(x_is_nan, c1_and, c1);

mk_is_zero(y, y_is_zero);
m_simp.mk_and(x_is_zero, y_is_zero, both_zero);
mk_is_nan(x, x_is_nan);
mk_is_nan(y, y_is_nan);
c2 = y_is_nan;

expr_ref c3(m);
mk_float_gt(f, num, args, c3);

expr_ref r_sgn(m), r_sig(m), r_exp(m);

expr_ref c3xy_sgn(m), c2c3_sgn(m);
m_simp.mk_ite(c3, x_sgn, y_sgn, c3xy_sgn);
m_simp.mk_ite(c2, x_sgn, c3xy_sgn, c2c3_sgn);
m_simp.mk_ite(c1, y_sgn, c2c3_sgn, r_sgn);
mk_pzero(f, pzero);

expr_ref c3xy_sig(m), c2c3_sig(m);
m_simp.mk_ite(c3, x_sig, y_sig, c3xy_sig);
m_simp.mk_ite(c2, x_sig, c3xy_sig, c2c3_sig);
m_simp.mk_ite(c1, y_sig, c2c3_sig, r_sig);
expr_ref gt(m);
mk_float_gt(f, num, args, gt);

expr_ref c3xy_exp(m), c2c3_exp(m);
m_simp.mk_ite(c3, x_exp, y_exp, c3xy_exp);
m_simp.mk_ite(c2, x_exp, c3xy_exp, c2c3_exp);
m_simp.mk_ite(c1, y_exp, c2c3_exp, r_exp);
result = y;
mk_ite(gt, x, result, result);
mk_ite(both_zero, pzero, result, result);
mk_ite(y_is_nan, x, result, result);
mk_ite(x_is_nan, y, result, result);

mk_fp(r_sgn, r_exp, r_sig, result);
SASSERT(is_well_sorted(m, result));
}

void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
Expand Down
40 changes: 26 additions & 14 deletions src/ast/rewriter/fpa_rewriter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -411,14 +411,20 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
result = arg1;
return BR_DONE;
}
// expand as using ite's
result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = m_util.mk_pzero(m().get_sort(arg1));
return BR_DONE;
}

result = m().mk_ite(mk_eq_nan(arg1),
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1,
arg2)));
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m_util.mk_lt(arg1, arg2),
arg1,
arg2))));
return BR_REWRITE_FULL;
}

Expand All @@ -431,14 +437,20 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
result = arg1;
return BR_DONE;
}
// expand as using ite's
result = m().mk_ite(m().mk_or(mk_eq_nan(arg1), m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2))),
if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) {
result = m_util.mk_pzero(m().get_sort(arg1));
return BR_DONE;
}

result = m().mk_ite(mk_eq_nan(arg1),
arg2,
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1,
arg2)));
m().mk_ite(mk_eq_nan(arg2),
arg1,
m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)),
m_util.mk_pzero(m().get_sort(arg1)),
m().mk_ite(m_util.mk_gt(arg1, arg2),
arg1,
arg2))));
return BR_REWRITE_FULL;
}

Expand Down