diff --git a/.gitignore b/.gitignore index 3d6e631f1..a935d9dba 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,8 @@ *~ *.pyc +*.pyo +# Ignore callgrind files +callgrind.out.* # .hpp files are automatically generated *.hpp .z3-trace diff --git a/README b/README index e002a3ac5..ad136e5f6 100644 --- a/README +++ b/README @@ -17,22 +17,24 @@ Execute: make sudo make install -It will install z3 executable at /usr/bin, libraries at /usr/lib, and include files at /usr/include. -You can change the installation p +By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, +where PREFIX is the installation prefix used for installing Python in your system. +It is usually /usr for most Linux distros, and /usr/local for FreeBSD. +Use the following commands to install in a different prefix (e.g., /home/leo) -Use the following commands to install in a different prefix (e.g., /home/leo), and the Z3 python -bindings in a different python package directory. - - python scripts/mk_make.py --prefix=/home/leo --pydir=/home/leo/python + python scripts/mk_make.py --prefix=/home/leo cd build make - sudo make install + make install + +In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages, +where X.Y corresponds to the python version in your system. To uninstall Z3, use sudo make uninstall -3) Building Z3 using clang and clang++ on Linux/OSX +4) Building Z3 using clang and clang++ on Linux/OSX Remark: clang does not support OpenMP yet. CXX=clang++ CC=clang python scripts/mk_make.py diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 694a6d635..104828a45 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -51,6 +51,8 @@ Version 4.3.2 - Fixed timers on Linux and FreeBSD. +- Fixed crash reported at http://z3.codeplex.com/workitem/11. + Version 4.3.1 ============= diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 268a6d27b..e4f860a95 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -68,7 +68,7 @@ VER_MAJOR=None VER_MINOR=None VER_BUILD=None VER_REVISION=None -PREFIX='/usr' +PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0] GMP=False VS_PAR=False VS_PAR_NUM=8 @@ -357,7 +357,6 @@ def display_help(exit_code): print(" -s, --silent do not print verbose messages.") if not IS_WINDOWS: print(" -p , --prefix= installation prefix (default: %s)." % PREFIX) - print(" -y , --pydir= installation prefix for Z3 python bindings (default: %s)." % PYTHON_PACKAGE_DIR) else: print(" --parallel=num use cl option /MP with 'num' parallel processes") print(" -b , --build= subdirectory where Z3 will be built (default: build).") @@ -393,9 +392,9 @@ def parse_options(): global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR try: options, remainder = getopt.gnu_getopt(sys.argv[1:], - 'b:dsxhmcvtnp:gjy:', + 'b:dsxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', - 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'pydir=', 'parallel=']) + 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=']) except: print("ERROR: Invalid command line option") display_help(1) @@ -429,12 +428,13 @@ def parse_options(): STATIC_LIB = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): PREFIX = arg + PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages') + mk_dir(PYTHON_PACKAGE_DIR) + if sys.version >= "3": + mk_dir(os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')) elif IS_WINDOWS and opt == '--parallel': VS_PAR = True VS_PAR_NUM = int(arg) - elif opt in ('-y', '--pydir'): - PYTHON_PACKAGE_DIR = arg - mk_dir(PYTHON_PACKAGE_DIR) elif opt in ('-g', '--gmp'): GMP = True elif opt in ('-j', '--java'): @@ -1402,6 +1402,7 @@ def mk_config(): print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) + print('Python version: %s' % distutils.sysconfig.get_python_version()) if is_java_enabled(): print('Java Home: %s' % JAVA_HOME) print('Java Compiler: %s' % JAVAC) @@ -1414,15 +1415,30 @@ def mk_install(out): out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib')) for c in get_components(): c.mk_install(out) - out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR) + out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR) + if sys.version >= "3": + out.write('\t@cp %s*.pyc %s\n' % (os.path.join('__pycache__', 'z3'), + os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))) + else: + out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR) out.write('\t@echo Z3 was successfully installed.\n') + if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): + if os.uname()[0] == 'Darwin': + LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH" + else: + LD_LIBRARY_PATH = "LD_LIBRARY_PATH" + out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' % + (os.path.join(PREFIX, 'lib'), LD_LIBRARY_PATH)) + out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) out.write('\n') def mk_uninstall(out): out.write('uninstall:\n') for c in get_components(): c.mk_uninstall(out) + out.write('\t@rm -f %s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3')) out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3')) + out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3')) out.write('\t@echo Z3 was successfully uninstalled.\n') out.write('\n') @@ -1441,6 +1457,8 @@ def mk_makefile(): if c.main_component(): out.write(' %s' % c.name) out.write('\n\t@echo Z3 was successfully built.\n') + out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR) + out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be also executed if \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR) if not IS_WINDOWS: out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n") out.write('\t@echo " sudo make install"\n') @@ -1920,19 +1938,35 @@ def mk_def_files(): if c.require_def_file(): mk_def_file(c) -def cp_z3pyc_to_build(): +def cp_z3py_to_build(): mk_dir(BUILD_DIR) + # Erase existing .pyc files + for root, dirs, files in os.walk(Z3PY_SRC_DIR): + for f in files: + if f.endswith('.pyc'): + rmf(os.path.join(root, f)) + # Compile Z3Py files if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1: raise MKException("failed to compile Z3Py sources") + # Copy sources to build + for py in filter(lambda f: f.endswith('.py'), os.listdir(Z3PY_SRC_DIR)): + shutil.copyfile(os.path.join(Z3PY_SRC_DIR, py), os.path.join(BUILD_DIR, py)) + if is_verbose(): + print("Copied '%s'" % py) + # Python 2.x support for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)): - try: - os.remove(os.path.join(BUILD_DIR, pyc)) - except: - pass shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc)) - os.remove(os.path.join(Z3PY_SRC_DIR, pyc)) if is_verbose(): print("Generated '%s'" % pyc) + # Python 3.x support + src_pycache = os.path.join(Z3PY_SRC_DIR, '__pycache__') + if os.path.exists(src_pycache): + for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)): + target_pycache = os.path.join(BUILD_DIR, '__pycache__') + mk_dir(target_pycache) + shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc)) + if is_verbose(): + print("Generated '%s'" % pyc) def mk_bindings(api_files): if not ONLY_MAKEFILES: @@ -1949,7 +1983,7 @@ def mk_bindings(api_files): check_java() mk_z3consts_java(api_files) _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK - cp_z3pyc_to_build() + cp_z3py_to_build() # Extract enumeration types from API files, and add python definitions. def mk_z3consts_py(api_files): diff --git a/src/api/api_context.h b/src/api/api_context.h index edb79b2d5..896011615 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -54,7 +54,7 @@ namespace api { datalog::dl_decl_util m_datalog_util; // Support for old solver API - smt_params m_fparams; + smt_params m_fparams; smt::kernel * m_solver; // General purpose solver for backward compatibility // ------------------------------- diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9b1d5f1f0..c138bcd62 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -44,6 +44,7 @@ from z3core import * from z3types import * from z3consts import * from z3printer import * +from fractions import Fraction import sys import io @@ -2523,6 +2524,15 @@ class RatNumRef(ArithRef): """ return Z3_get_numeral_string(self.ctx_ref(), self.as_ast()) + def as_fraction(self): + """Return a Z3 rational as a Python Fraction object. + + >>> v = RealVal("1/5") + >>> v.as_fraction() + Fraction(1, 5) + """ + return Fraction(self.numerator_as_long(), self.denominator_as_long()) + class AlgebraicNumRef(ArithRef): """Algebraic irrational values.""" diff --git a/src/api/python/z3num.py b/src/api/python/z3num.py index 581536e44..75cabbb27 100644 --- a/src/api/python/z3num.py +++ b/src/api/python/z3num.py @@ -8,6 +8,7 @@ from z3 import * from z3core import * from z3printer import * +from fractions import Fraction def _to_numeral(num, ctx=None): if isinstance(num, Numeral): @@ -170,6 +171,14 @@ class Numeral: assert(self.is_integer()) return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast())) + def as_fraction(self): + """ Return a numeral (that is a rational) as a Python Fraction. + >>> Numeral("1/5").as_fraction() + Fraction(1, 5) + """ + assert(self.is_rational()) + return Fraction(self.numerator().as_long(), self.denominator().as_long()) + def approx(self, precision=10): """Return a numeral that approximates the numeral `self`. The result `r` is such that |r - self| <= 1/10^precision diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index f2dccf065..752bad072 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -206,6 +206,21 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E)); m_e = m->mk_const(e_decl); m->inc_ref(m_e); + + func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); + m_0_pw_0_int = m->mk_const(z_pw_z_int); + m->inc_ref(m_0_pw_0_int); + + func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); + m_0_pw_0_real = m->mk_const(z_pw_z_real); + m->inc_ref(m_0_pw_0_real); + + MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); + MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); + MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); + MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i); + MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r); + MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r); } arith_decl_plugin::arith_decl_plugin(): @@ -253,7 +268,15 @@ arith_decl_plugin::arith_decl_plugin(): m_acosh_decl(0), m_atanh_decl(0), m_pi(0), - m_e(0) { + m_e(0), + m_0_pw_0_int(0), + m_0_pw_0_real(0), + m_neg_root_decl(0), + m_div_0_decl(0), + m_idiv_0_decl(0), + m_mod_0_decl(0), + m_u_asin_decl(0), + m_u_acos_decl(0) { } arith_decl_plugin::~arith_decl_plugin() { @@ -303,6 +326,14 @@ void arith_decl_plugin::finalize() { DEC_REF(m_atanh_decl); DEC_REF(m_pi); DEC_REF(m_e); + DEC_REF(m_0_pw_0_int); + DEC_REF(m_0_pw_0_real); + DEC_REF(m_neg_root_decl); + DEC_REF(m_div_0_decl); + DEC_REF(m_idiv_0_decl); + DEC_REF(m_mod_0_decl); + DEC_REF(m_u_asin_decl); + DEC_REF(m_u_acos_decl); m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr()); m_manager->dec_array_ref(m_small_reals.size(), m_small_reals.c_ptr()); } @@ -347,6 +378,14 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_ATANH: return m_atanh_decl; case OP_PI: return m_pi->get_decl(); case OP_E: return m_e->get_decl(); + case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl(); + case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl(); + case OP_NEG_ROOT: return m_neg_root_decl; + case OP_DIV_0: return m_div_0_decl; + case OP_IDIV_0: return m_idiv_0_decl; + case OP_MOD_0: return m_mod_0_decl; + case OP_U_ASIN: return m_u_asin_decl; + case OP_U_ACOS: return m_u_acos_decl; default: return 0; } } @@ -426,12 +465,20 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args return true; return false; } + +static bool is_const_op(decl_kind k) { + return + k == OP_PI || + k == OP_E || + k == OP_0_PW_0_INT || + k == OP_0_PW_0_REAL; +} func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); - if (arity == 0 && k != OP_PI && k != OP_E) { + if (arity == 0 && !is_const_op(k)) { m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } @@ -448,7 +495,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters unsigned num_args, expr * const * args, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); - if (num_args == 0 && k != OP_PI && k != OP_E) { + if (num_args == 0 && !is_const_op(k)) { m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index e63e866c3..53ab1881b 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -35,6 +35,7 @@ enum arith_sort_kind { enum arith_op_kind { OP_NUM, // rational & integers OP_IRRATIONAL_ALGEBRAIC_NUM, // irrationals that are roots of polynomials with integer coefficients + // OP_LE, OP_GE, OP_LT, @@ -67,6 +68,15 @@ enum arith_op_kind { // constants OP_PI, OP_E, + // under-specified symbols + OP_0_PW_0_INT, // 0^0 for integers + OP_0_PW_0_REAL, // 0^0 for reals + OP_NEG_ROOT, // x^n when n is even and x is negative + OP_DIV_0, // x/0 + OP_IDIV_0, // x div 0 + OP_MOD_0, // x mod 0 + OP_U_ASIN, // asin(x) for x < -1 or x > 1 + OP_U_ACOS, // acos(x) for x < -1 or x > 1 LAST_ARITH_OP }; @@ -126,7 +136,16 @@ protected: app * m_pi; app * m_e; - + + app * m_0_pw_0_int; + app * m_0_pw_0_real; + func_decl * m_neg_root_decl; + func_decl * m_div_0_decl; + func_decl * m_idiv_0_decl; + func_decl * m_mod_0_decl; + func_decl * m_u_asin_decl; + func_decl * m_u_acos_decl; + ptr_vector m_small_ints; ptr_vector m_small_reals; @@ -182,6 +201,10 @@ public: app * mk_e() const { return m_e; } + app * mk_0_pw_0_int() const { return m_0_pw_0_int; } + + app * mk_0_pw_0_real() const { return m_0_pw_0_real; } + virtual expr * get_some_value(sort * s); virtual void set_cancel(bool f); @@ -339,6 +362,15 @@ public: app * mk_pi() { return plugin().mk_pi(); } app * mk_e() { return plugin().mk_e(); } + app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); } + app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); } + app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); } + app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); } + app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); } + app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); } + app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); } + app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); } + /** \brief Return the equality (= lhs rhs), but it makes sure that if one of the arguments is a numeral, then it will be in the right-hand-side; diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 857cec105..47842ae90 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -113,15 +113,14 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * m_manager->raise_exception("invalid const array definition, invalid domain size"); return 0; } - unsigned num_parameters = s->get_num_parameters(); - - if (num_parameters == 0) { - m_manager->raise_exception("parameter mismatch"); + if (!is_array_sort(s)) { + m_manager->raise_exception("invalid const array definition, parameter is not an array sort"); + return 0; + } + if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) { + m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument"); return 0; } - - // TBD check that range sort corresponds to last parameter. - parameter param(s); func_decl_info info(m_family_id, OP_CONST_ARRAY, 1, ¶m); info.m_private_parameters = true; diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 9dbbeb231..0bb7378f4 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -292,7 +292,14 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c } expr * fv = m().mk_app(f, values.size(), values.c_ptr()); - parameter p(m().get_sort(args[0])); + sort * in_s = get_sort(args[0]); + ptr_vector domain; + unsigned domain_sz = get_array_arity(in_s); + for (unsigned i = 0; i < domain_sz; i++) + domain.push_back(get_array_domain(in_s, i)); + sort_ref out_s(m()); + out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range()); + parameter p(out_s.get()); result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv); return BR_REWRITE2; } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index f8ff27337..44efe0199 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -63,6 +63,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) { m_blast_eq_value = p.blast_eq_value(); m_split_concat_eq = p.split_concat_eq(); m_udiv2mul = p.udiv2mul(); + m_bvnot2arith = p.bvnot2arith(); m_mkbv2num = _p.get_bool("mkbv2num", false); } @@ -1527,6 +1528,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) { } #endif + if (m_bvnot2arith) { + // (bvnot x) --> (bvsub -1 x) + bv_size = get_bv_size(arg); + rational minus_one = (rational::power_of_two(bv_size) - numeral(1)); + result = m_util.mk_bv_sub(m_util.mk_numeral(minus_one, bv_size), arg); + return BR_REWRITE1; + } + return BR_FAILED; } diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index ba5ac5580..a94fd18c1 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -67,6 +67,7 @@ class bv_rewriter : public poly_rewriter { bool m_mkbv2num; bool m_split_concat_eq; bool m_udiv2mul; + bool m_bvnot2arith; bool is_zero_bit(expr * x, unsigned idx); diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg index 780d8e724..d9ee9f7a3 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -7,4 +7,6 @@ def_module_params(module_name='rewriter', ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"), ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"), ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"), - ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"))) + ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"), + ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)") + )) diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 2ff341e07..84b732280 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -429,6 +429,29 @@ namespace datalog { } } + void mk_slice::filter_unique_vars(rule& r) { + // + // Variables that occur in multiple uinterpreted predicates are not sliceable. + // + uint_set used_vars; + for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) { + app* p = r.get_tail(j); + for (unsigned i = 0; i < p->get_num_args(); ++i) { + expr* v = p->get_arg(i); + if (is_var(v)) { + unsigned vi = to_var(v)->get_idx(); + add_var(vi); + if (used_vars.contains(vi)) { + m_var_is_sliceable[vi] = false; + } + else { + used_vars.insert(vi); + } + } + } + } + } + void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) { expr_ref_vector conjs = get_tail_conjs(r); for (unsigned j = 0; j < conjs.size(); ++j) { @@ -475,6 +498,7 @@ namespace datalog { } } } + filter_unique_vars(r); // // Collect the set of variables that are solved. // Collect the occurrence count of the variables per conjunct. @@ -750,51 +774,11 @@ namespace datalog { m_solved_vars.reset(); -#if 0 - uint_set used_vars; - expr_ref b(m); - - TBD: buggy code: for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); - if (is_eq(e, v, b)) { - if (v >= m_solved_vars.size()) { - m_solved_vars.resize(v+1); - } - if (v < sorts.size() && sorts[v]) { - TRACE("dl", tout << "already bound " << mk_pp(e, m) << "\n";); - add_free_vars(used_vars, e); - } - else if (m_solved_vars[v].get()) { - TRACE("dl", tout << "already solved " << mk_pp(e, m) << "\n";); - add_free_vars(used_vars, e); - add_free_vars(used_vars, m_solved_vars[v].get()); - used_vars.insert(v); - } - else { - TRACE("dl", tout << "new solution " << mk_pp(e, m) << "\n";); - m_solved_vars[v] = b; - } - } - else { - TRACE("dl", tout << "not solved " << mk_pp(e, m) << "\n";); - add_free_vars(used_vars, e); - } + tail.push_back(to_app(e)); } -#endif - for (unsigned i = 0; i < conjs.size(); ++i) { - expr* e = conjs[i].get(); -#if 0 - if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) { - TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";); - // skip conjunct - } -#endif - tail.push_back(to_app(e)); - - } - - + new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0); rm.fix_unbound_vars(new_rule, false); diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h index d798430d5..26a8175f2 100644 --- a/src/muz_qe/dl_mk_slice.h +++ b/src/muz_qe/dl_mk_slice.h @@ -89,6 +89,8 @@ namespace datalog { void update_predicate(app* p, app_ref& q); + void filter_unique_vars(rule& r); + void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars); public: diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index df4a55475..6949c4264 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -971,15 +971,15 @@ namespace fm { } bool is_linear_ineq(expr * t) const { + bool result = false; m.is_not(t, t); expr * lhs, * rhs; - TRACE("is_occ_bug", tout << mk_pp(t, m) << "\n";); if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) { - if (!m_util.is_numeral(rhs)) - return false; - return is_linear_pol(lhs); + result = m_util.is_numeral(rhs) && is_linear_pol(lhs); } - return false; + TRACE("qe_lite", tout << mk_pp(t, m) << " " << (result?"true":"false") << "\n";); + + return result; } bool is_occ(expr * t) { @@ -1049,7 +1049,7 @@ namespace fm { cnstr->m_xs = reinterpret_cast(mem_xs); cnstr->m_as = reinterpret_cast(mem_as); for (unsigned i = 0; i < num_vars; i++) { - TRACE("mk_constraint_bug", tout << "xs[" << i << "]: " << xs[i] << "\n";); + TRACE("qe_lite", tout << "xs[" << i << "]: " << xs[i] << "\n";); cnstr->m_xs[i] = xs[i]; new (cnstr->m_as + i) rational(as[i]); } @@ -1241,7 +1241,7 @@ namespace fm { if (c2->m_dead) continue; if (subsumes(c, *c2)) { - TRACE("fm_subsumption", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";); + TRACE("qe_lite", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";); c2->m_dead = true; continue; } @@ -1284,12 +1284,12 @@ namespace fm { } void updt_params() { - m_fm_real_only = true; + m_fm_real_only = false; m_fm_limit = 5000000; m_fm_cutoff1 = 8; m_fm_cutoff2 = 256; m_fm_extra = 0; - m_fm_occ = false; + m_fm_occ = true; } void set_cancel(bool f) { @@ -1318,7 +1318,7 @@ namespace fm { expr * f = g[i]; if (is_occ(f)) continue; - TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";); + TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";); quick_for_each_expr(proc, visited, f); } } @@ -1447,6 +1447,7 @@ namespace fm { SASSERT(m_uppers.size() == m_is_int.size()); SASSERT(m_forbidden.size() == m_is_int.size()); SASSERT(m_var2pos.size() == m_is_int.size()); + TRACE("qe_lite", tout << mk_pp(t,m) << " |-> " << x << " forbidden: " << forbidden << "\n";); return x; } @@ -1468,7 +1469,7 @@ namespace fm { x = mk_var(t); SASSERT(m_expr2var.contains(t)); SASSERT(m_var2expr.get(x) == t); - TRACE("to_var_bug", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";); + TRACE("qe_lite", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";); return x; } @@ -1488,6 +1489,7 @@ namespace fm { void add_constraint(expr * f, expr_dependency * dep) { + TRACE("qe_lite", tout << mk_pp(f, m) << "\n";); SASSERT(!m.is_or(f) || m_fm_occ); sbuffer lits; sbuffer xs; @@ -1524,7 +1526,7 @@ namespace fm { neg = !neg; expr * lhs = to_app(l)->get_arg(0); expr * rhs = to_app(l)->get_arg(1); - m_util.is_numeral(rhs, c); + VERIFY (m_util.is_numeral(rhs, c)); if (neg) c.neg(); unsigned num_mons; @@ -1567,7 +1569,7 @@ namespace fm { } } - TRACE("to_var_bug", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";); + TRACE("qe_lite", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";); constraint * new_c = mk_constraint(lits.size(), lits.c_ptr(), @@ -1578,7 +1580,7 @@ namespace fm { strict, dep); - TRACE("to_var_bug", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";); + TRACE("qe_lite", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";); VERIFY(register_constraint(new_c)); } @@ -1591,7 +1593,7 @@ namespace fm { if (is_false(*c)) { del_constraint(c); m_inconsistent = true; - TRACE("add_constraint_bug", tout << "is false "; display(tout, *c); tout << "\n";); + TRACE("qe_lite", tout << "is false "; display(tout, *c); tout << "\n";); return false; } @@ -1614,7 +1616,7 @@ namespace fm { return true; } else { - TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";); + TRACE("qe_lite", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";); m_new_fmls.push_back(to_expr(*c)); del_constraint(c); return false; @@ -1668,7 +1670,7 @@ namespace fm { } // x_cost_lt is not a total order on variables std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int)); - TRACE("fm", + TRACE("qe_lite", svector::iterator it2 = x_cost_vector.begin(); svector::iterator end2 = x_cost_vector.end(); for (; it2 != end2; ++it2) { @@ -1854,7 +1856,7 @@ namespace fm { if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) { // literal is true - TRACE("fm", tout << "resolution " << x << " consequent literal is always true: \n"; + TRACE("qe_lite", tout << "resolution " << x << " consequent literal is always true: \n"; display(tout, l); tout << "\n"; display(tout, u); tout << "\n";); @@ -1898,7 +1900,7 @@ namespace fm { } if (tautology) { - TRACE("fm", tout << "resolution " << x << " tautology: \n"; + TRACE("qe_lite", tout << "resolution " << x << " tautology: \n"; display(tout, l); tout << "\n"; display(tout, u); tout << "\n";); @@ -1908,7 +1910,7 @@ namespace fm { expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep); if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) { - TRACE("fm", tout << "resolution " << x << " inconsistent: \n"; + TRACE("qe_lite", tout << "resolution " << x << " inconsistent: \n"; display(tout, l); tout << "\n"; display(tout, u); tout << "\n";); @@ -1926,7 +1928,7 @@ namespace fm { new_strict, new_dep); - TRACE("fm", tout << "resolution " << x << "\n"; + TRACE("qe_lite", tout << "resolution " << x << "\n"; display(tout, l); tout << "\n"; display(tout, u); @@ -1949,7 +1951,7 @@ namespace fm { if (l.empty() || u.empty()) { // easy case mark_constraints_dead(x); - TRACE("fm", tout << "variable was eliminated (trivial case)\n";); + TRACE("qe_lite", tout << "variable was eliminated (trivial case)\n";); return true; } @@ -1967,7 +1969,7 @@ namespace fm { m_counter += num_lowers * num_uppers; - TRACE("fm_bug", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n"; + TRACE("qe_lite", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n"; display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u);); unsigned num_old_cnstrs = num_uppers + num_lowers; @@ -1977,7 +1979,7 @@ namespace fm { for (unsigned i = 0; i < num_lowers; i++) { for (unsigned j = 0; j < num_uppers; j++) { if (m_inconsistent || num_new_cnstrs > limit) { - TRACE("fm", tout << "too many new constraints: " << num_new_cnstrs << "\n";); + TRACE("qe_lite", tout << "too many new constraints: " << num_new_cnstrs << "\n";); del_constraints(new_constraints.size(), new_constraints.c_ptr()); return false; } @@ -2002,7 +2004,7 @@ namespace fm { backward_subsumption(*c); register_constraint(c); } - TRACE("fm", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";); + TRACE("qe_lite", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";); return true; } @@ -2018,7 +2020,7 @@ namespace fm { if (!c->m_dead) { c->m_dead = true; expr * new_f = to_expr(*c); - TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";); + TRACE("qe_lite", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";); m_new_fmls.push_back(new_f); } } @@ -2049,7 +2051,7 @@ namespace fm { m_new_fmls.push_back(m.mk_false()); } else { - TRACE("fm", display(tout);); + TRACE("qe_lite", display(tout);); subsume(); var_vector candidates; diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index d2292ede9..169e27927 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -99,93 +99,15 @@ Rules (mod t1 t2) --> k2 | same constraints as above */ -struct purify_arith_decls { - ast_manager & m; - func_decl * m_int_0_pw_0_decl; // decl for: int 0^0 - func_decl * m_real_0_pw_0_decl; // decl for: rel 0^0 - func_decl * m_neg_root_decl; // decl for: even root of negative (real) number - func_decl * m_div_0_decl; // decl for: x/0 - func_decl * m_idiv_0_decl; // decl for: div(x, 0) - func_decl * m_mod_0_decl; // decl for: mod(x, 0) - func_decl * m_asin_u_decl; // decl for: asin(x) when x < -1 or x > 1 - func_decl * m_acos_u_decl; // decl for: acos(x) when x < -1 or x > 1 - - void inc_refs() { - m.inc_ref(m_int_0_pw_0_decl); - m.inc_ref(m_real_0_pw_0_decl); - m.inc_ref(m_neg_root_decl); - m.inc_ref(m_div_0_decl); - m.inc_ref(m_idiv_0_decl); - m.inc_ref(m_mod_0_decl); - m.inc_ref(m_asin_u_decl); - m.inc_ref(m_acos_u_decl); - } - - void dec_refs() { - m.dec_ref(m_int_0_pw_0_decl); - m.dec_ref(m_real_0_pw_0_decl); - m.dec_ref(m_neg_root_decl); - m.dec_ref(m_div_0_decl); - m.dec_ref(m_idiv_0_decl); - m.dec_ref(m_mod_0_decl); - m.dec_ref(m_asin_u_decl); - m.dec_ref(m_acos_u_decl); - } - - purify_arith_decls(arith_util & u): - m(u.get_manager()) { - sort * i = u.mk_int(); - sort * r = u.mk_real(); - m_int_0_pw_0_decl = m.mk_const_decl(symbol("0^0-int"), i); - m_real_0_pw_0_decl = m.mk_const_decl(symbol("0^0-real"), r); - sort * rr[2] = { r, r }; - m_neg_root_decl = m.mk_func_decl(symbol("neg-root"), 2, rr, r); - m_div_0_decl = m.mk_func_decl(symbol("/0"), 1, &r, r); - m_idiv_0_decl = m.mk_func_decl(symbol("div0"), 1, &i, i); - m_mod_0_decl = m.mk_func_decl(symbol("mod0"), 1, &i, i); - m_asin_u_decl = m.mk_func_decl(symbol("asin-u"), 1, &r, r); - m_acos_u_decl = m.mk_func_decl(symbol("acos-u"), 1, &r, r); - inc_refs(); - } - - purify_arith_decls(ast_manager & _m, - func_decl * int_0_pw_0, - func_decl * real_0_pw_0, - func_decl * neg_root, - func_decl * div_0, - func_decl * idiv_0, - func_decl * mod_0, - func_decl * asin_u, - func_decl * acos_u - ): - m(_m), - m_int_0_pw_0_decl(int_0_pw_0), - m_real_0_pw_0_decl(real_0_pw_0), - m_neg_root_decl(neg_root), - m_div_0_decl(div_0), - m_idiv_0_decl(idiv_0), - m_mod_0_decl(mod_0), - m_asin_u_decl(asin_u), - m_acos_u_decl(acos_u) { - inc_refs(); - } - - ~purify_arith_decls() { - dec_refs(); - } -}; - struct purify_arith_proc { arith_util & m_util; - purify_arith_decls & m_aux_decls; bool m_produce_proofs; bool m_elim_root_objs; bool m_elim_inverses; bool m_complete; - purify_arith_proc(arith_util & u, purify_arith_decls & d, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete): + purify_arith_proc(arith_util & u, bool produce_proofs, bool elim_root_objs, bool elim_inverses, bool complete): m_util(u), - m_aux_decls(d), m_produce_proofs(produce_proofs), m_elim_root_objs(elim_root_objs), m_elim_inverses(elim_inverses), @@ -247,15 +169,6 @@ struct purify_arith_proc { expr * mk_fresh_int_var() { return mk_fresh_var(true); } - func_decl * div0_decl() { return m_owner.m_aux_decls.m_div_0_decl; } - func_decl * idiv0_decl() { return m_owner.m_aux_decls.m_idiv_0_decl; } - func_decl * mod0_decl() { return m_owner.m_aux_decls.m_mod_0_decl; } - func_decl * int_0_pw_0_decl() { return m_owner.m_aux_decls.m_int_0_pw_0_decl; } - func_decl * real_0_pw_0_decl() { return m_owner.m_aux_decls.m_real_0_pw_0_decl; } - func_decl * neg_root_decl() { return m_owner.m_aux_decls.m_neg_root_decl; } - func_decl * asin_u_decl() { return m_owner.m_aux_decls.m_asin_u_decl; } - func_decl * acos_u_decl() { return m_owner.m_aux_decls.m_acos_u_decl; } - expr * mk_int_zero() { return u().mk_numeral(rational(0), true); } expr * mk_real_zero() { return u().mk_numeral(rational(0), false); } @@ -332,7 +245,7 @@ struct purify_arith_proc { if (complete()) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), - EQ(k, m().mk_app(div0_decl(), x)))); + EQ(k, u().mk_div0(x)))); push_cnstr_pr(result_pr); } } @@ -380,10 +293,10 @@ struct purify_arith_proc { push_cnstr_pr(mod_pr); if (complete()) { - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, m().mk_app(idiv0_decl(), x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x)))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, m().mk_app(mod0_decl(), x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x)))); push_cnstr_pr(mod_pr); } } @@ -445,8 +358,7 @@ struct purify_arith_proc { push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); if (complete()) { - func_decl * z_pw_z = is_int ? int_0_pw_0_decl() : real_0_pw_0_decl(); - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, m().mk_const(z_pw_z)))); + push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); push_cnstr_pr(result_pr); } } @@ -470,7 +382,7 @@ struct purify_arith_proc { push_cnstr_pr(result_pr); if (complete()) { push_cnstr(OR(u().mk_ge(x, zero), - EQ(k, m().mk_app(neg_root_decl(), x, u().mk_numeral(n, false))))); + EQ(k, u().mk_neg_root(x, u().mk_numeral(n, false))))); push_cnstr_pr(result_pr); } } @@ -561,10 +473,10 @@ struct purify_arith_proc { // x < -1 implies k = asin_u(x) // x > 1 implies k = asin_u(x) push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, m().mk_app(asin_u_decl(), x)))); + EQ(k, u().mk_u_asin(x)))); push_cnstr_pr(result_pr); push_cnstr(OR(u().mk_le(x, one), - EQ(k, m().mk_app(asin_u_decl(), x)))); + EQ(k, u().mk_u_asin(x)))); push_cnstr_pr(result_pr); } return BR_DONE; @@ -603,10 +515,10 @@ struct purify_arith_proc { // x < -1 implies k = acos_u(x) // x > 1 implies k = acos_u(x) push_cnstr(OR(u().mk_ge(x, mone), - EQ(k, m().mk_app(acos_u_decl(), x)))); + EQ(k, u().mk_u_acos(x)))); push_cnstr_pr(result_pr); push_cnstr(OR(u().mk_le(x, one), - EQ(k, m().mk_app(acos_u_decl(), x)))); + EQ(k, u().mk_u_acos(x)))); push_cnstr_pr(result_pr); } return BR_DONE; @@ -835,12 +747,10 @@ struct purify_arith_proc { class purify_arith_tactic : public tactic { arith_util m_util; - purify_arith_decls m_aux_decls; params_ref m_params; public: purify_arith_tactic(ast_manager & m, params_ref const & p): m_util(m), - m_aux_decls(m_util), m_params(p) { } @@ -879,7 +789,7 @@ public: bool elim_root_objs = m_params.get_bool("elim_root_objects", true); bool elim_inverses = m_params.get_bool("elim_inverses", true); bool complete = m_params.get_bool("complete", true); - purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete); + purify_arith_proc proc(m_util, produce_proofs, elim_root_objs, elim_inverses, complete); proc(*(g.get()), mc, produce_models); diff --git a/src/util/params.cpp b/src/util/params.cpp index 0ee42868d..4aff0de92 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -933,3 +933,8 @@ void params::set_sym(char const * k, symbol const & v) { SET_SYM_VALUE(); } +#ifdef Z3DEBUG +void pp(params_ref const & p) { + std::cout << p << std::endl; +} +#endif