3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Commit graph

1765 commits

Author SHA1 Message Date
Mikolas Janota
2141a075ba Refactoring ackermannization functionality. 2016-01-28 18:24:54 +00:00
Mikolas Janota
e7477e2f6a Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:51 +00:00
Mikolas Janota
094d357b07 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 12:10:36 +00:00
Dan Liew
250c8d028d Fix bug when configuring when building OCaml bindings is enabled
when using Python2.

The output from ``check_output()`` has ``unicode`` type under
Python 2 but type ``str`` under Python 3. This type ended up being
used inside the ``MakeRuleCmd`` class which asserts that it receives
paths of type ``str``. To fix the problem under Python 2 the asserts
have been made weaker by also allowing the paths to be of type
``unicode``.
2016-01-12 19:38:43 +00:00
Dan Liew
cb106d71cf Teach the OCaml bindings install rule to respect the DESTDIR makefile
variable. Previously it would try to install into the system (e.g.
``/usr/lib/ocaml``) regardless of the value of DESTDIR.

Unfortunately it looks like packagers who use DESTDIR to do staged
installs will need to have their packages patch their user's OCaml
``ld.conf`` file manually at package install time (not ``make install``
time) with the extra path to the Z3 Ocaml package directory. We could
use the ``touch`` command to create an empty ``ld.conf`` before running
``ocamlfind install`` but that adds the wrong path to ``ld.conf``
because it contains DESTDIR.
2016-01-11 21:13:25 +00:00
Dan Liew
f038291293 Don't silently fail if ocamlfind cannot be found when building the Ocaml
bindings is enabled. That is really unhelpful behaviour. Instead emit a
warning. I would prefer an error message but apparently being able to
build but not install the OCaml bindings is desirable.

Whilst I'm here also print information about ocamlfind where it should
have been mentioned.
2016-01-11 19:36:02 +00:00
Mikolas Janota
b26e4b1516 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-11 18:27:47 +00:00
Dan Liew
49a2ed01c8 Improve error message emitting during configure when the Python
bindings are enabled and the set python package directory does
not live under the install prefix. This is the other part required
to fix issue #404.
2016-01-08 21:21:54 +00:00
Dan Liew
e9ea687bb9 Disable the Python bindings by default which partially fixes issue #404.
To enable the Python bindings use the newly added ``--python`` option.
2016-01-08 21:21:54 +00:00
Mikolas Janota
743a59254e Merge remote-tracking branch 'upstream/master' into lackr 2016-01-07 16:39:43 +00:00
Christoph M. Wintersteiger
3e000d7525 build fix for libz3.vcxproj 2016-01-05 14:40:31 +00:00
Christoph M. Wintersteiger
8b47a84598 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 11:34:35 +00:00
Christoph M. Wintersteiger
4915f2da04 Added facilities for generating a libz3.vcxproj next to z3.vcxproj for simplified DLL build in VS. 2016-01-04 21:53:24 +00:00
Christoph M. Wintersteiger
25af97fb8b tabs 2016-01-04 21:04:07 +00:00
Nikolaj Bjorner
0c03a87c82 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-03 14:08:29 -08:00
Christoph M. Wintersteiger
758c9cd7a0 Build fix for install dependencies 2016-01-01 17:02:31 +00:00
Christoph M. Wintersteiger
d6330e157d Refactored Python API installation build. 2016-01-01 16:42:01 +00:00
Nikolaj Bjorner
f414869456 add symbolic automaton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-23 19:46:10 -08:00
Nikolaj Bjorner
7a9bd72e2e merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-22 17:48:47 -08:00
Nikolaj Bjorner
ea876715e3 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-22 10:46:50 -08:00
Nikolaj Bjorner
9c6271dded add debugging facilities for github issues #384 #367
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-22 10:43:18 -08:00
Tony Tiger
e98ee6ec06 Fixing building under OS X
Previous method is_osx_hack didn't exist, possibly wasn't cleaned up. This
change has been tested and Z3 compiles successfully within a 2.7 virtualenv
running on OS X 10.10.5.
2015-12-22 13:00:55 +00:00
Christoph M. Wintersteiger
a30fe1e2ec Followup to previous build fix. Relates to #357 and #361 2015-12-22 00:52:37 +01:00
Christoph M. Wintersteiger
ea218da2c4 Bugfix in build scripts.
Additional fix for #357, relates to #361.
2015-12-22 00:37:27 +01:00
Christoph M. Wintersteiger
06deb07a49 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-17 12:47:34 +00:00
Christoph M. Wintersteiger
0fe1e3248f .NET build fix 2015-12-17 12:47:24 +00:00
Christoph M. Wintersteiger
1cc2385fd2 typo 2015-12-17 12:33:45 +00:00
Mikolas Janota
c6e66ebc3a Adding ackr component. 2015-12-15 18:43:36 +00:00
Christoph M. Wintersteiger
90b1b07af4 build fixes 2015-12-15 15:03:53 +00:00
Christoph M. Wintersteiger
22a77721ef Updated build options for .NET API 2015-12-15 14:20:31 +00:00
Christoph M. Wintersteiger
f4e3989766 .NET API build fixes 2015-12-15 13:09:02 +00:00
Christoph M. Wintersteiger
942b6ba5ec Updated .NET build. 2015-12-15 12:24:59 +00:00
Christoph M. Wintersteiger
fc5b9156cf Merge pull request #363 from delcypher/dotnet_configure_assembly_info
Refactor ``mk_all_assembly_infos()`` to use the ``configure_file()`` and misc fixes for dotnet bindings
2015-12-15 11:35:14 +00:00
Dan Liew
439d8d8afe Fix issue on non-windows systems when emitting the build rule
for the ".NET" bindings example.

Previously there was a hack that would to path separator replacement
( '/' -> '\' ) which breaks paths under non-windows platforms. The hack
has been made slightly better by doing ( '/' -> os.path.sep). This
preserves the existing behaviour under Windows and unbreaks the build
on non-windows platforms.

I'm not entirely sure why the path replacement needs to be done in
the first place. I thought Windows was supposed to support using
'/' as a path separator (as well as '/'). Maybe ``csc.exe`` doesn't
support these kind of paths?
2015-12-15 08:56:47 +00:00
Dan Liew
44393b37de Emit dependency of phony target `examples on _ex_dotnet_example`
when building of the ".NET" bindings is enabled.
2015-12-15 08:46:47 +00:00
Christoph M. Wintersteiger
edb1f4d896 ML API build fix 2015-12-14 14:55:38 +00:00
Christoph M. Wintersteiger
134b93b43e ML API build fixes for Windows. 2015-12-14 14:41:19 +00:00
Dan Liew
d3d10490ea Fix bug in `Makefile` generation when emitting the command to build
the ".NET" bindings when in debug mode.

``;`` is a shell command separator so it needs to be quoted when
emitting ``/define:DEBUG;TRACE``.
2015-12-14 09:56:03 +00:00
Dan Liew
81c98cf3ee Refactor `mk_all_assembly_infos() to use the configure_file()`
function. The old implementation was buggy under Python 3.5 and
unsafe (not using with statements on calls to ``open()``).
2015-12-14 09:51:45 +00:00
Christoph M. Wintersteiger
5a357097c0 ML API Windows build fixes 2015-12-12 20:01:52 +00:00
Christoph M. Wintersteiger
d456400f93 Merge branch 'new_ocaml_install' of https://github.com/wintersteiger/z3 into new_ocaml_install 2015-12-12 19:34:02 +00:00
Christoph M. Wintersteiger
d5f79c1f17 build fix for ML API 2015-12-12 19:30:25 +00:00
Dan Liew
140b3de3aa Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 19:30:24 +00:00
Christoph M. Wintersteiger
325d516825 ocaml build fix 2015-12-12 19:30:22 +00:00
Christoph M. Wintersteiger
02f7ae4a4d updated ocaml build and installation 2015-12-12 19:30:22 +00:00
Dan Liew
948df47027 Make warnings that are emitted when installing Python bindings outside
the install prefix on OSX less aggressive by not stating that this might
lead to a broken install (even though it might!).

Also emit a similar warning during the configuration step.

This partially addresses #361
2015-12-12 09:34:50 +00:00
Christoph M. Wintersteiger
f164f17190 ocaml build fix 2015-12-11 20:01:55 +00:00
Christoph M. Wintersteiger
50f17e403c updated ocaml build and installation 2015-12-11 19:56:23 +00:00
Nikolaj Bjorner
8949790c16 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 07:37:51 -08:00
Nikolaj Bjorner
820fb10ef8 create .so impages for OpenBSD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 07:37:40 -08:00