mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity
4398 commits 23 branches 48 tags 157 MiB
Commit graph

568 commits

Author SHA1 Message Date
Nikolaj Bjorner 9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Christoph M. Wintersteiger fc05eb65bd Fixed regular expressions in build scripts to expect cross-platform newlines. 2015-11-17 13:55:16 +00:00
Nikolaj Bjorner 6e1c246454 avoid exception in Ratul's environment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-16 23:06:04 -08:00
Christoph M. Wintersteiger 706a037bf4 Python 3.x string decoding fix 2015-11-16 15:16:50 +01:00
Nikolaj Bjorner bea68cd194 remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 17:05:15 -08:00
Christoph M. Wintersteiger 05eb78ccac fix for string decoding in build scripts 2015-11-14 15:42:49 +00:00
Christoph M. Wintersteiger 639dfc4b30 fix for string decoding in build scripts 2015-11-14 15:06:55 +00:00
Christoph M. Wintersteiger 27dcd8c5b6 Fix for python decoding of command line output strings 
Fixes #302
 2015-11-13 17:15:04 +00:00
Christoph M. Wintersteiger 2f216ee5c1 Fixed PREFIX for OSX installation. Fixes #124. 2015-11-03 15:35:43 +00:00
Christoph M. Wintersteiger 28ba92b298 Python 3.x issues 2015-10-30 06:31:16 -07:00
Christoph M. Wintersteiger 64fa2db3ff Python 3.x issues 2015-10-29 17:47:07 +00:00
Christoph M. Wintersteiger 7287478370 Fixed Python 3.x issue with commandline output from subprocess.Popen 2015-10-29 15:54:28 +00:00
Christoph M. Wintersteiger 5cb4b1d188 Fix for example build rules. 2015-10-29 13:06:48 +00:00
Christoph M. Wintersteiger b47e9d74e9 Refactored example build rules to avoid compiler warnings. 2015-10-29 13:03:02 +00:00
Christoph M. Wintersteiger eb28ee8999 Python 3.x issues 2015-10-28 22:40:07 +00:00
Christoph M. Wintersteiger 498bafcc4b Merge branch 'ocamlfind_stublibs' of https://github.com/zkincaid/z3 into zkincaid-172 2015-10-19 17:05:55 +01:00
Christoph M. Wintersteiger eb0cdc42d1 Merge branch 'pypy-fix' of https://github.com/zardus/z3 into zardus-76 
# Conflicts:
#	scripts/mk_util.py
 2015-10-19 16:51:43 +01:00
Christoph M. Wintersteiger aa1692370d Merge branch 'fix-mk_util_py' of https://github.com/cao/z3 into cao-tabs 
# Conflicts:
#	scripts/mk_util.py
 2015-10-19 15:35:14 +01:00
Christoph M. Wintersteiger b1fcdadd55 Merge branch 'buildsystem_cleanup' of https://github.com/daniel-j-h/z3 into daniel-j-h-buildsystem_cleanup 2015-10-19 15:18:13 +01:00
Christoph M. Wintersteiger 3c89312d1e Merge pull request #55 from zshipko/master 
support openbsd
 2015-10-19 14:15:56 +01:00
Christoph M. Wintersteiger 115187ee2b Bumped version number to 4.4.2. 2015-10-05 16:04:03 +01:00
Zachary Kincaid 9e34872e8f For ocamlfind install, set rpath to package directory if stublibs does not exist 2015-10-04 10:10:53 -04:00
Christoph M. Wintersteiger d8524ae4dd Fixed indentation 2015-10-03 16:24:06 +01:00
Christoph M. Wintersteiger 08a3ab92f3 Added --noomp to mk_make 2015-10-02 12:38:56 +01:00
Zachary Kincaid eca2488ab4 If ocamlfind is installed, add destdir/stublibs to rpath 2015-07-26 19:59:17 -04:00
Nikolaj Bjorner 9dd704bc4b remove double underscores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-09 18:05:45 -07:00
Nikolaj Bjorner a9a5a69b73 remove double underscores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-09 13:31:22 -07:00
Nikolaj Bjorner 4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Henning Guenther c7e96d897a Replace cone-of-influence filter with generalized dataflow-engine 
Signed-off-by: Henning Guenther <t-hennig@microsoft.com>
 2015-06-29 10:50:51 +01:00
Nuno Lopes e441db5bc4 build system: fix typo in OS_DEFINES for linux 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-23 13:59:36 +01:00
Nuno Lopes 4346966f00 Run link-time optimization on windows only when configured with --optimize 
This should probably be revisited for VS 2015

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-22 14:48:50 +01:00
Nikolaj Bjorner 6f0d76a62e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-21 09:39:32 -07:00
Nikolaj Bjorner 949c21ca08 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 02:23:56 -07:00
Nikolaj Bjorner fe7c577d99 isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 01:54:52 -07:00
Nikolaj Bjorner 1657cdd8b4 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 12:47:19 -07:00
Nikolaj Bjorner d469a16bb8 add more Copyright notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:59:21 -07:00
Nikolaj Bjorner b08ccc7816 added missing Copyright forms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-10 11:54:02 -07:00
zach shipko 9cc4fc919d Merge branch 'master' of https://github.com/Z3Prover/z3 2015-05-30 18:36:26 -07:00
Christoph M. Wintersteiger 85419ca503 Added branch into QF_NRA from QF_FP problems containing to_real terms. 2015-05-29 14:21:27 +01:00
Christoph M. Wintersteiger d8d0b21e42 Bugfix for dll/so name resolution in Java. 
Fixes #111
 2015-05-29 12:55:17 +01:00
Nuno Lopes 8ff7735a20 python 3 fixes 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-19 13:47:43 +01:00
Nuno Lopes ef32aaaf12 don't use -fPIC on cygwin 64 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-18 16:37:20 +01:00
Nikolaj Bjorner e8811748d3 fix regressions in nl/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-16 19:08:37 +01:00
Nuno Lopes 7ae68f003a dont use /LTCG on windows debug builds 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-15 19:20:57 +01:00
Nikolaj Bjorner ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Nuno Lopes ce749240d7 more fixes for python 3 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-12 18:43:51 +01:00
Christoph M. Wintersteiger 043f441a4c Python 3.x compatibility. 
Fixes problems reported in comments to 1abeb825a3
 2015-05-12 10:29:37 +01:00
Nikolaj Bjorner 839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-09 19:40:34 -07:00
Yan 8b9bf9ea90 Fix mk_util.py so that it explicitly closes files (instead of relying on reference counting, which doesn't exist in pypy) 2015-05-05 11:38:04 -07:00
Kevin Borgolte 024923526b remove unused modules 2015-05-05 11:31:32 -07:00
Kevin Borgolte f458423868 remove trailing whitespace 2015-05-05 11:29:48 -07:00
Kevin Borgolte 7dcdecfa09 fix mixed tab/spaces indent 2015-05-05 11:29:26 -07:00
Nikolaj Bjorner 9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Christoph M. Wintersteiger c0dc08ee9c Added configuration checks for floating-point build flags. 2015-04-30 17:17:44 +01:00
Christoph M. Wintersteiger 8c9afa423b Bumped version number to 4.4.1 in unstable. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-04-29 17:22:24 +01:00
Christoph M. Wintersteiger 78cc1e0703 Remove temporary files created during configuration tests. 2015-04-29 15:15:57 +01:00
Christoph M. Wintersteiger 1abeb825a3 Fixed python 3.x problems. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-04-28 14:58:58 +01:00
zach shipko f034ed54ab support openbsd 2015-04-23 11:28:17 -07:00
Nikolaj Bjorner 3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Daniel J. Hofmann ce9036c300 Minor python-related style fixes 2015-04-09 21:24:15 +02:00
Christoph M. Wintersteiger 03020b9f96 Build system bugfixes. 
Partially fixes #27
 2015-04-08 12:09:14 +01:00
Christoph M. Wintersteiger ba066ff899 Bugfix for build scripts. 
Partially fixes #27
 2015-04-08 11:54:25 +01:00
Christoph M. Wintersteiger 0e8d314a2a Fixed Java API installation targets. Fixes #28 2015-04-08 11:02:56 +01:00
Christoph M. Wintersteiger 0ad97022a1 Added (un)install targets for the Java API 2015-04-07 13:48:34 +01:00
Nikolaj Bjorner 52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Christoph M. Wintersteiger 0f03cd2ae0 Enabled test for OpenMP in Windows (for old and express versions of visual studio). 
Fixes #8
 2015-03-29 15:49:03 +01:00
Nikolaj Bjorner 4bfe20647b remove tab in mk_util.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-03-27 02:43:21 -07:00
Christoph M. Wintersteiger 8d11c431b7 Bugfix for the OCaml bindings on Windows 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 17:44:53 +00:00
Christoph M. Wintersteiger ec4a07318e Bugfix for the Java API on Windows 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 15:19:15 +00:00
Christoph M. Wintersteiger 1f8119f601 Bugfix for the Java API. Thanks to codeplex user susmitj for reporting this problem! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-04 15:14:07 +00:00
Christoph M. Wintersteiger 400e203bce Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-02 17:31:42 +00:00
Christoph M. Wintersteiger 71f2d358ef Bugfix in windows dist scripts 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-02 17:30:41 +00:00
Nuno Lopes dd2c179663 Fix warnings during compilation with MSVC due to /LTCG 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-03-02 15:05:38 +00:00
Nuno Lopes 8d303a09b5 Compile Z3 with link-time optimizations on Windows, yielding a 2-3% speedup 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-25 13:10:29 +00:00
Nuno Lopes 1e30fd2c65 Hide non-exported symbols when compiling with gcc/clang. 
I get a 17% reduction in the size of libz3.so on linux 32 bits, plus a 0.5-1% speedup when using the API.

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:38:46 +00:00
Nuno Lopes 5676fbbc9e compiler love: make a few symbols static and avoid unneeded relocations 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:13:51 +00:00
Christoph M. Wintersteiger 5c7d0380d3 Fixes in the OCaml FPA API and example 2015-01-24 18:29:52 +00:00
Christoph M. Wintersteiger 1c9051016a Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 
Conflicts:
	scripts/mk_util.py
 2015-01-24 18:29:03 +00:00
Christoph M. Wintersteiger 65ccc9a8ea added FPA ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 19:36:47 +00:00
Christoph M. Wintersteiger ffd10675f4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 11:07:48 +00:00
Christoph M. Wintersteiger d56d63e3e8 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
 2015-01-21 14:25:31 +00:00
Christoph M. Wintersteiger 052baaabe4 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 14:22:35 +00:00
Christoph M. Wintersteiger d0a7246f00 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-21 13:51:00 +00:00
Christoph M. Wintersteiger 5e6ea4e570 added --x86 build flag 2015-01-20 19:03:49 +00:00
Christoph M. Wintersteiger 237577acc8 Bumping version to 4.4 
Added to release notes

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:59:54 +00:00
Christoph M. Wintersteiger a8d8e3e9e5 formatting 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:16:51 +00:00
Christoph M. Wintersteiger ed0fa93245 Minor adjustments after rebase 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:35:19 +00:00
Christoph M. Wintersteiger c9fa77cc70 ML API: fixed Python 3.4 issues in the build scripts 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:17:59 +00:00
Christoph M. Wintersteiger e754aa1c11 Minor adjustments after rebasing ml-ng onto unstable. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:17:58 +00:00
Christoph M. Wintersteiger bb31014417 ML API: build fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:17:14 +00:00
Christoph M. Wintersteiger 5c67b59685 ML API: Windows build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:17:12 +00:00
Christoph M. Wintersteiger 05f42b0073 ML API: build fixes? 2015-01-19 17:17:11 +00:00
Christoph M. Wintersteiger 93a20d9074 ML API: build fixes 2015-01-19 17:17:10 +00:00
Christoph M. Wintersteiger ea9fc43544 ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:48 +00:00
Christoph M. Wintersteiger d47f143591 ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:47 +00:00
Christoph M. Wintersteiger 198c6ef930 ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:45 +00:00
Christoph M. Wintersteiger 4c28085022 ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:45 +00:00
Christoph M. Wintersteiger ceabafa01c ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:44 +00:00
Christoph M. Wintersteiger 2ee4409962 ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:43 +00:00
Christoph M. Wintersteiger 40c6be0baa ML API: build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 17:16:42 +00:00