mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
18665 commits 49 branches 53 tags 182 MiB
Commit graph

1686 commits

Author SHA1 Message Date
Dan Liew
9558dc14fb Refactor `exec_pyg_scripts()` so that it is usable externally 
via a new ``pyg2hpp.py`` script. This will allow other build systems to
take ``pyg`` files and generate the corresponding ``hpp`` files.
 2016-03-04 15:22:00 +00:00
Christoph M. Wintersteiger
c9a5676346 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-04 15:15:16 +00:00
Christoph M. Wintersteiger
cf5910e041 typos 2016-03-04 15:08:03 +00:00
Christoph M. Wintersteiger
b27977ea90 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-02 15:14:12 +00:00
Christoph M. Wintersteiger
4fe4db6657 build fix for static libray on Windows 2016-03-01 17:34:45 +00:00
Nikolaj Bjorner
4cf72e23e6 fix python 3 compat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-27 09:58:45 -08:00
Nikolaj Bjorner
ce8862d415 fix bug in conflict clause generation in seq-branch-variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-26 18:15:45 -08:00
Christoph M. Wintersteiger
0930cfc53f ML API build fixes for cygwin 2016-02-15 15:44:46 +00:00
Christoph M. Wintersteiger
62cae4186b ML API bug fixes 2016-02-15 12:54:05 +00:00
Christoph M. Wintersteiger
18c0a3bfaf removed comments 2016-02-14 19:57:21 +00:00
Christoph M. Wintersteiger
b99fcb9c8a More new OCaml API 2016-02-14 19:56:22 +00:00
Christoph M. Wintersteiger
824169da0a New OCaml API 2016-02-13 22:09:45 +00:00
Nikolaj Bjorner
e484fc365d add outline of bv bounds tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 22:57:47 +00:00
Christoph M. Wintersteiger
c01f0323c3 Merge branch 'lackr' of https://github.com/MikolasJanota/z3 into MikolasJanota-lackr 2016-02-10 14:26:04 +00:00
Christoph M. Wintersteiger
a16f524eae Install target fix for ocamlfind_install on Windows. 
Relates to #409
 2016-02-09 19:58:52 +00:00
Mikolas Janota
b614e7732b Merge remote-tracking branch 'upstream/master' into lackr 2016-02-08 12:54:22 +00:00
Dan Liew
508d2e32c8 Fix a bug in Python build scripts where an extra ending slash in the 
build directory would cause REV_BUILD_DIR to be set incorrectly and
would lead to a broken Makefile being generated.

What would happen before:

```
$ python scripts/mk_make.py --build FOO_1
...
REV_BUILD_DIR='..'
```

```
$ python scripts/mk_make.py --build FOO_1/
...
REV_BUILD_DIR='../..'
```
^^^^^ that's wrong. It should be REV_BUILD_DIR='..'

To fix this the ``reverse_path()`` function has been taught to ignore empty
components in ``p.split(os.sep)``.
 2016-02-05 14:51:15 +00:00
Dan Liew
33f676ef6b Do not hardcode default build directory name. 2016-02-05 14:39:27 +00:00
Dan Liew
6112ea2ec7 Fix typo 2016-02-05 14:38:41 +00:00
mikolas
faa620f673 Further refactoring ackermannization. 2016-02-03 17:31:19 +00:00
mikolas
2679b74543 refactoring 2016-02-03 13:53:52 +00:00
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