diff --git a/README b/README deleted file mode 100644 index 22fc58c7a..000000000 --- a/README +++ /dev/null @@ -1,53 +0,0 @@ -Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under the MIT license. -Z3 can be built using Visual Studio Command Prompt and make/g++. - -1) Building Z3 on Windows using Visual Studio Command Prompt - -32-bit builds, start with: - - python scripts/mk_make.py - -or instead, for a 64-bit build: - - python scripts/mk_make.py -x - -then: - - cd build - nmake - -2) Building Z3 using make/g++ and Python -Execute: - - python scripts/mk_make.py - cd build - make - sudo make install - -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) - - python scripts/mk_make.py --prefix=/home/leo - cd build - make - 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 - -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 - cd build - make - - -To clean Z3 you can delete the build directory and run the mk_make.py script again. diff --git a/README.md b/README.md new file mode 100644 index 000000000..7d2fc5a24 --- /dev/null +++ b/README.md @@ -0,0 +1,161 @@ +# Z3 + +Z3 is a theorem prover from Microsoft Research. It is licensed +under the [MIT license](LICENSE.txt). + +Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides +[bindings for several programming languages][3]. + +See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. + +[1]: #building-z3-on-windows-using-visual-studio-command-prompt +[2]: #building-z3-using-make-and-gccclang +[3]: #z3-bindings + +## Building Z3 on Windows using Visual Studio Command Prompt + +32-bit builds, start with: + +```bash +python scripts/mk_make.py +``` + +or instead, for a 64-bit build: + +```bash +python scripts/mk_make.py -x +``` + +then: + +```bash +cd build +nmake +``` + +## Building Z3 using make and GCC/Clang + +Execute: + +```bash +python scripts/mk_make.py +cd build +make +sudo make install +``` + +Note by default ``gcc`` is used as the C++ compiler if it is available. If you +would prefer to use Clang change the ``mk_make.py`` line to + +```bash +CXX=clang++ CC=clang python scripts/mk_make.py +``` + +Note that Clang < 3.7 does not support OpenMP. + +By default, it will install z3 executable at ``PREFIX/bin``, libraries at +``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` +installation prefix if inferred by the ``mk_make.py`` script. It is usually +``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use +the ``--prefix=`` command line option to change the install prefix. For example: + +```bash +python scripts/mk_make.py --prefix=/home/leo +cd build +make +make install +``` + +Note the above will typically disable the installation of the Python bindings +because the Python ``site-packages`` directory (e.g. +``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and +installing outside of the install prefix is dangerous and misleading. + +To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the +install prefix as the default. The ``DESTDIR`` variable is prepended to the +install locations during ``make install`` and ``make uninstall`` and is intended +to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html). +Therefore it must always contain a trailing slash. + +For example: + +```bash +python scripts/mk_make.py +cd build +make +make install DESTDIR=/home/leo/ +``` + +In this example, the Z3 Python bindings will be stored at +``/home/leo/lib/pythonX.Y/site-packages`` +(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux +distributions) where X.Y corresponds to the python version in your system. + +To uninstall Z3, use + +```bash +sudo make uninstall +``` + +To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. + +## Z3 bindings + +Z3 has bindings for various programming languages. + +### ``.NET`` + +These bindings are enabled by default on Windows and are enabled on other +platforms if [mono](http://www.mono-project.com/) is detected. On these +platforms the location of the C# compiler and gac utility need to be known. You +can set these as follows if they aren't detected automatically. For example: + +```bash +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +``` + +To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. + +Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC`` +to ``/usr/bin/dmcs``. + +Note that when ``make install`` is executed on non-windows platforms the GAC +utility is used to install ``Microsoft.Z3.dll`` into the +[GAC](http://www.mono-project.com/docs/advanced/assemblies-and-the-gac/) as the +``Microsoft.Z3.Sharp`` package. During install a +[pkg-config](http://www.freedesktop.org/wiki/Software/pkg-config/) file +(``Microsoft.Z3.Sharp.pc``) is also installed which allows the +[MonoDevelop](http://www.monodevelop.com/) IDE to find the bindings. Running +``make uninstall`` will remove the dll from the GAC and the pkg-config file. + +See [``examples/dotnet``](examples/dotnet) for examples. + +### ``C`` + +These are always enabled. + +See [``examples/c``](examples/c) for examples. + +### ``C++`` + +These are always enabled. + +See [``examples/c++``](examples/c++) for examples. + +### ``Java`` + +Use the ``--java`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/java``](examples/java) for examples. + +### ``OCaml`` + +Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/ml``](examples/ml) for examples. + +### ``Python`` + +These bindings are always enabled. + +See [``examples/python``](examples/python) for examples. diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6a070fe93..ed5df106b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -79,7 +79,7 @@ TRACE = False DOTNET_ENABLED=False JAVA_ENABLED=False ML_ENABLED=False -PYTHON_INSTALL_ENABLED=True +PYTHON_INSTALL_ENABLED=False STATIC_LIB=False VER_MAJOR=None VER_MINOR=None @@ -612,6 +612,7 @@ def display_help(exit_code): print(" --dotnet generate .NET bindings.") print(" --java generate Java bindings.") print(" --ml generate OCaml bindings.") + print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") @@ -642,14 +643,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 + global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, 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=']) + 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python']) except: print("ERROR: Invalid command line option") display_help(1) @@ -708,6 +709,8 @@ def parse_options(): ML_ENABLED = True elif opt in ('', '--noomp'): USE_OMP = False + elif opt in ('--python'): + PYTHON_INSTALL_ENABLED = True else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -1339,6 +1342,9 @@ class PythonInstallComponent(Component): self.in_prefix_install = True self.libz3Component = libz3Component + if not PYTHON_INSTALL_ENABLED: + return + if IS_WINDOWS: # Installing under Windows doesn't make sense as the install prefix is used # but that doesn't make sense under Windows @@ -1357,7 +1363,15 @@ class PythonInstallComponent(Component): else: # Use path inside the prefix (should be the normal case on Linux) # CMW: Also normal on *BSD? - assert PYTHON_PACKAGE_DIR.startswith(PREFIX) + if not PYTHON_PACKAGE_DIR.startswith(PREFIX): + raise MKException(('The python package directory ({}) must live ' + + 'under the install prefix ({}) to install the python bindings.' + + 'Use --pypkgdir and --prefix to set the python package directory ' + + 'and install prefix respectively. Note that the python package ' + + 'directory does not need to exist and will be created if ' + + 'necessary during install.').format( + PYTHON_PACKAGE_DIR, + PREFIX)) self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) self.in_prefix_install = True @@ -1365,7 +1379,7 @@ class PythonInstallComponent(Component): assert not os.path.isabs(self.pythonPkgDir) def final_info(self): - if not PYTHON_PACKAGE_DIR.startswith(PREFIX): + if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED: print("Warning: The detected Python package directory (%s) is not " "in the installation prefix (%s). This can lead to a broken " "Python API installation. Use --pypkgdir= to change the " diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index bca0bdd1b..ccf18a024 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -789,6 +789,8 @@ sig val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr + val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) + -> expr -> expr -> expr -> expr -> expr val compare : expr -> expr -> int end = struct type expr = Expr of AST.ast @@ -797,6 +799,12 @@ end = struct let gnc e = match e with Expr(a) -> (z3obj_gnc a) let gno e = match e with Expr(a) -> (z3obj_gno a) + let inc_elist (es : expr list) = + List.iter (fun e -> match e with Expr(o) -> o.inc_ref (gnc e) o.m_n_obj) es + + let dec_elist (es : expr list) = + List.iter (fun e -> match e with Expr(o) -> o.dec_ref (gnc e) o.m_n_obj) es + let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> let e = z3_native_object_of_ast_ptr ctx no in if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then @@ -850,6 +858,9 @@ end = struct let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) + let apply4 ctx f t1 t2 t3 t4 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3) (gno t4)) + let simplify ( x : expr ) ( p : Params.params option ) = match p with | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x)) | Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp)) @@ -871,19 +882,30 @@ end = struct if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then raise (Z3native.Exception "Number of arguments does not match") else - expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) + (inc_elist args; + let r = expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) in + dec_elist args; + r) let substitute ( x : expr ) from to_ = if (List.length from) <> (List.length to_) then raise (Z3native.Exception "Argument sizes do not match") else - expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) + (inc_elist from; + inc_elist to_; + let r = expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) in + dec_elist from; + dec_elist to_; + r) let substitute_one ( x : expr ) from to_ = substitute ( x : expr ) [ from ] [ to_ ] let substitute_vars ( x : expr ) to_ = - expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_)) + (inc_elist to_; + let r = expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_)) in + dec_elist to_; + r) let translate ( x : expr ) to_ctx = if (Expr.gc x) == to_ctx then @@ -1257,22 +1279,21 @@ struct let mk_union ( ctx : context ) ( args : expr list ) = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) - - + let mk_intersection ( ctx : context ) ( args : expr list ) = expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args)) let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = - expr_of_ptr ctx (Z3native.mk_set_difference (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + apply2 ctx Z3native.mk_set_difference arg1 arg2 let mk_complement ( ctx : context ) ( arg : expr ) = - expr_of_ptr ctx (Z3native.mk_set_complement (context_gno ctx) (Expr.gno arg)) + apply1 ctx Z3native.mk_set_complement arg let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = - expr_of_ptr ctx (Z3native.mk_set_member (context_gno ctx) (Expr.gno elem) (Expr.gno set)) + apply2 ctx Z3native.mk_set_member elem set let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = - expr_of_ptr ctx (Z3native.mk_set_subset (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + apply2 ctx Z3native.mk_set_subset arg1 arg2 end @@ -1612,10 +1633,10 @@ struct mk_const ctx (Symbol.mk_string ctx name) let mk_mod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + apply2 ctx Z3native.mk_mod t1 t2 let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + apply2 ctx Z3native.mk_rem t1 t2 let mk_numeral_s ( ctx : context ) ( v : string ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx))) @@ -1624,7 +1645,7 @@ struct expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) let mk_int2real ( ctx : context ) ( t : expr ) = - (Expr.expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_int2real t let mk_int2bv ( ctx : context ) ( n : int ) ( t : expr ) = (Expr.expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (Expr.gno t))) @@ -1636,10 +1657,10 @@ struct Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) let get_numerator ( x : expr ) = - expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x)) + apply1 (Expr.gc x) Z3native.get_numerator x let get_denominator ( x : expr ) = - expr_of_ptr (Expr.gc x) (Z3native.get_denominator (Expr.gnc x) (Expr.gno x)) + apply1 (Expr.gc x) Z3native.get_denominator x let get_ratio ( x : expr ) = if (is_rat_numeral x) then @@ -1671,10 +1692,10 @@ struct expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) let mk_is_integer ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_is_int t let mk_real2int ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_real2int t module AlgebraicNumber = struct @@ -1703,26 +1724,19 @@ struct let f x = (Expr.gno x) in (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (List.length t) (Array.of_list (List.map f t)))) - let mk_unary_minus ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (Expr.gno t))) + let mk_unary_minus ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_unary_minus t - let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_div t1 t2 - let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_power t1 t2 - let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_lt t1 t2 - let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_le t1 t2 - let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_gt t1 t2 - let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ge t1 t2 end @@ -1793,100 +1807,63 @@ struct Expr.mk_const ctx name (mk_sort ctx size) let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) = mk_const ctx (Symbol.mk_string ctx name) size - let mk_not ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnot (context_gno ctx) (Expr.gno t)) - let mk_redand ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvredand (context_gno ctx) (Expr.gno t)) - let mk_redor ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvredor (context_gno ctx) (Expr.gno t)) - let mk_and ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_or ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_nand ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_nor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_xnor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_neg ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (Expr.gno t)) - let mk_add ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_sub ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_mul ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_udiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_sdiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_urem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_srem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_smod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ult ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_slt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_ule ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sle ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_uge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_ugt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sgt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + let mk_not ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvnot t + let mk_redand ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredand t + let mk_redor ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredor t + let mk_and ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvand t1 t2 + let mk_or ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvor t1 t2 + let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxor t1 t2 + let mk_nand ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnand t1 t2 + let mk_nor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnor t1 t2 + let mk_xnor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxnor t1 t2 + let mk_neg ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg t + let mk_add ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd t1 t2 + let mk_sub ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub t1 t2 + let mk_mul ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul t1 t2 + let mk_udiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvudiv t1 t2 + let mk_sdiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv t1 t2 + let mk_urem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvurem t1 t2 + let mk_srem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsrem t1 t2 + let mk_smod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsmod t1 t2 + let mk_ult ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvult t1 t2 + let mk_slt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvslt t1 t2 + let mk_ule ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvule t1 t2 + let mk_sle ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsle t1 t2 + let mk_uge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvuge t1 t2 + let mk_sge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsge t1 t2 + let mk_ugt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvugt t1 t2 + let mk_sgt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsgt t1 t2 + let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_concat t1 t2 let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (Expr.gno t)) - let mk_sign_ext ( ctx : context ) ( i : int ) ( t : expr ) = + let mk_sign_ext ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (Expr.gno t)) let mk_zero_ext ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (Expr.gno t)) let mk_repeat ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (Expr.gno t)) - let mk_shl ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_lshr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ashr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_rotate_left ( ctx : context ) ( i : int ) ( t : expr ) = + let mk_shl ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvshl t1 t2 + let mk_lshr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvlshr t1 t2 + let mk_ashr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvashr t1 t2 + let mk_rotate_left ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (Expr.gno t)) let mk_rotate_right ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (Expr.gno t)) - let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_left t1 t2 + let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_right t1 t2 let mk_bv2int ( ctx : context ) ( t : expr ) ( signed : bool ) = expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (Expr.gno t) signed) let mk_add_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_add_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sub_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_add_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd_no_underflow t1 t2 + let mk_sub_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub_no_overflow t1 t2 let mk_sub_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_sdiv_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_neg_no_overflow ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (Expr.gno t))) + let mk_sdiv_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv_no_overflow t1 t2 + let mk_neg_no_overflow ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg_no_overflow t let mk_mul_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_mul_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_mul_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul_no_underflow t1 t2 let mk_numeral ( ctx : context ) ( v : string ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx size))) end @@ -1949,7 +1926,7 @@ struct (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative)) let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) = - (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand))) + apply3 ctx Z3native.mk_fpa_fp sign exponent significand let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s))) let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) = @@ -1997,54 +1974,30 @@ struct let mk_const_s ( ctx : context ) ( name : string ) ( s : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) s - let mk_abs ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_abs (context_gno ctx) (Expr.gno t)) - let mk_neg ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_neg (context_gno ctx) (Expr.gno t)) - let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_add (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_sub (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_mul (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_div (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_fma (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2) (Expr.gno t3)) - let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_sqrt (context_gno ctx) (Expr.gno rm) (Expr.gno t)) - let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_round_to_integral ( ctx : context ) ( rm : expr ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_round_to_integral (context_gno ctx) (Expr.gno rm) (Expr.gno t)) - let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_min (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_max (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_leq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_geq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_eq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_is_normal ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_normal (context_gno ctx) (Expr.gno t)) - let mk_is_subnormal ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_subnormal (context_gno ctx) (Expr.gno t)) - let mk_is_zero ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_zero (context_gno ctx) (Expr.gno t)) - let mk_is_infinite ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_infinite (context_gno ctx) (Expr.gno t)) - let mk_is_nan ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_nan (context_gno ctx) (Expr.gno t)) - let mk_is_negative ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t)) - let mk_is_positive ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t)) + let mk_abs ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_abs t + let mk_neg ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_neg t + let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_add rm t1 t2 + let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_sub rm t1 t2 + let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_mul rm t1 t2 + let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_div rm t1 t2 + let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = apply4 ctx Z3native.mk_fpa_fma rm t1 t2 t3 + let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_sqrt rm t + let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_rem t1 t2 + let mk_round_to_integral ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_round_to_integral rm t + let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_min t1 t2 + let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_max t1 t2 + let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_leq t1 t2 + let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_lt t1 t2 + let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_geq t1 t2 + let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_gt t1 t2 + let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_eq t1 t2 + let mk_is_normal ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_normal t + let mk_is_subnormal ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_subnormal t + let mk_is_zero ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_zero t + let mk_is_infinite ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_infinite t + let mk_is_nan ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_nan t + let mk_is_negative ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_negative t + let mk_is_positive ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_positive t let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s)) let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) = @@ -2059,8 +2012,7 @@ struct expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size) let mk_to_sbv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_fpa_to_sbv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size) - let mk_to_real ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t)) + let mk_to_real ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_to_real t let get_ebits ( ctx : context ) ( s : Sort.sort ) = (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s)) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index afdca7464..b8ec74d18 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3572,15 +3572,19 @@ def Concat(*args): if __debug__: _z3_assert(sz >= 2, "At least two arguments expected.") - ctx = args[0].ctx - - if is_seq(args[0]): - if __debug__: - _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") - v = (Ast * sz)() - for i in range(sz): + ctx = None + for a in args: + if is_expr(a): + ctx = a.ctx + break + if is_seq(args[0]) or isinstance(args[0], str): + args = [_coerce_seq(s, ctx) for s in args] + if __debug__: + _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") + v = (Ast * sz)() + for i in range(sz): v[i] = args[i].as_ast() - return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) + return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) if is_re(args[0]): if __debug__: @@ -9066,7 +9070,12 @@ class SeqRef(ExprRef): def __add__(self, other): return Concat(self, other) + def __radd__(self, other): + return Concat(other, self) + def __getitem__(self, i): + if _is_int(i): + i = IntVal(i, self.ctx) return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) def is_string(self): diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b3648f38d..20bf183e0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1705,6 +1705,7 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); + TRACE("pdr", tout << tr << "\n";); smt::kernel solver(m, get_fparams()); solver.assert_expr(tr); lbool res = solver.check(); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 982aa963f..311a62a38 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -354,6 +354,7 @@ namespace smt { */ template interval theory_arith::evaluate_as_interval(expr * n) { + expr* arg; TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); if (has_var(n)) { TRACE("nl_evaluate", tout << "n has a variable associated with it\n";); @@ -385,6 +386,9 @@ namespace smt { TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); return r; } + else if (m_util.is_to_real(n, arg)) { + return evaluate_as_interval(arg); + } else { rational val; if (m_util.is_numeral(n, val)) { @@ -1660,7 +1664,7 @@ namespace smt { 3) (new non-int coeffs) This only happens in an optional step in the conversion. Now, for int rows, I only apply this optional step only if non-int coeffs are not created. */ - if (is_mixed_real_integer(r)) + if (!get_manager().int_real_coercions() && is_mixed_real_integer(r)) return true; // giving up... see comment above TRACE("cross_nested", tout << "cheking problematic row...\n";); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index cef8d5fc7..e4f698914 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1176,31 +1176,37 @@ namespace smt { unsigned idx = entry.second; if (m_wpos[v] == idx) - find_wpos(v); - + find_wpos(v); literal_vector & bits = m_bits[v]; literal bit = bits[idx]; - lbool val = ctx.get_assignment(bit); + lbool val = ctx.get_assignment(bit); + if (val == l_undef) { + continue; + } theory_var v2 = next(v); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";); + literal antecedent = bit; + + if (val == l_false) { + antecedent.neg(); + } while (v2 != v) { literal_vector & bits2 = m_bits[v2]; literal bit2 = bits2[idx]; SASSERT(bit != ~bit2); lbool val2 = ctx.get_assignment(bit2); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); + if (val != val2) { - literal antecedent = bit; literal consequent = bit2; if (val == l_false) { - antecedent.neg(); consequent.neg(); } - SASSERT(ctx.get_assignment(antecedent) == l_true); assign_bit(consequent, v, v2, idx, antecedent, false); if (ctx.inconsistent()) { TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";); + m_prop_queue.reset(); return; } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4bc867717..f06afce71 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -551,6 +551,9 @@ bool theory_seq::is_solved() { IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";); return false; } + if (!m_nqs.empty()) { + return false; + } for (unsigned i = 0; i < m_automata.size(); ++i) { if (!m_automata[i]) { IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";); @@ -967,10 +970,10 @@ bool theory_seq::solve_ne(unsigned idx) { } } + bool updated = false; dependency* new_deps = n.dep(); vector new_ls, new_rs; literal_vector new_lits(n.lits()); - bool updated = false; for (unsigned i = 0; i < n.ls().size(); ++i) { expr_ref_vector& ls = m_ls; expr_ref_vector& rs = m_rs; @@ -986,8 +989,7 @@ bool theory_seq::solve_ne(unsigned idx) { return true; } else if (!change) { -// std::cout << n.ls(i) << " " << ls << "\n"; -// std::cout << n.rs(i) << " " << rs << "\n"; + TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";); continue; } else { @@ -1015,7 +1017,7 @@ bool theory_seq::solve_ne(unsigned idx) { expr* nr = rhs[j].get(); if (m_util.is_seq(nl) || m_util.is_re(nl)) { ls.reset(); - rs.reset(); + rs.reset(); SASSERT(!m_util.str.is_concat(nl)); SASSERT(!m_util.str.is_concat(nr)); ls.push_back(nl); rs.push_back(nr); @@ -1041,6 +1043,16 @@ bool theory_seq::solve_ne(unsigned idx) { new_deps = m_dm.mk_join(deps, new_deps); } } + if (!updated && num_undef_lits == 0) { + return false; + } + if (!updated) { + for (unsigned j = 0; j < n.ls().size(); ++j) { + new_ls.push_back(n.ls(j)); + new_rs.push_back(n.rs(j)); + } + } + if (num_undef_lits == 1 && new_ls.empty()) { literal_vector lits; literal undef_lit = null_literal; @@ -1064,7 +1076,7 @@ bool theory_seq::solve_ne(unsigned idx) { propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); return true; } - else if (updated) { + if (updated) { if (num_undef_lits == 0 && new_ls.empty()) { TRACE("seq", tout << "conflict\n";); set_conflict(new_deps, new_lits);