mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
9997 commits 23 branches 48 tags 156 MiB
Commit graph

900 commits

Author SHA1 Message Date
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner a79400a01b fix bugs in scc_tr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:55:42 -07:00
Nikolaj Bjorner 3765bde5e9 updated OSX build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-22 20:19:08 -07:00
Nikolaj Bjorner bfc0b214ab update script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 14:49:36 -07:00
Nikolaj Bjorner 12f147403c update script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 14:13:27 -07:00
Nikolaj Bjorner 5d68a09233 update script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 11:25:38 -07:00
Nikolaj Bjorner 1470dbf517 back to path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 10:57:40 -07:00
Nikolaj Bjorner ba30365e2d updated script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 10:26:09 -07:00
Nikolaj Bjorner 9765a6d0d3 updated script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-21 09:23:01 -07:00
Nikolaj Bjorner ff2924e83b fix mac build error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:19:40 -07:00
Nikolaj Bjorner 6304578111 mac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:08:26 -07:00
Nikolaj Bjorner 16d2c2c506 mac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:06:54 -07:00
Nikolaj Bjorner 116f0e0c70 cd below 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:05:12 -07:00
Nikolaj Bjorner 971f83997c add ls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:02:19 -07:00
Nikolaj Bjorner 76eae5fa5c add mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 16:57:01 -07:00
Nikolaj Bjorner 4529ad933a add vstsmac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 15:19:05 -07:00
Nikolaj Bjorner 931dbd5933 remove python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 13:37:04 -07:00
Nikolaj Bjorner 8c4ea7983f use vc path in 2013 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 12:59:42 -07:00
Nikolaj Bjorner 6ee4efe93a remove python tests from x86 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 12:48:21 -07:00
Nikolaj Bjorner f7dfc39984 add vstsvs2013 outline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 12:20:40 -07:00
Nikolaj Bjorner db7844bef7 adding build definition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 09:33:23 -07:00
Nikolaj Bjorner 0d13a2812e add error checking and command argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 09:26:39 -07:00
Nikolaj Bjorner eb6bbd390a vsts script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 08:33:09 -07:00
Nikolaj Bjorner dc01266354 fixing after clone 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 20:50:24 -07:00
Nikolaj Bjorner d5bd7878b3 fix example test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 20:03:47 -07:00
Nikolaj Bjorner d5811a13eb add test-benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 19:18:05 -07:00
Nikolaj Bjorner b727a3463d update vsts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 18:21:34 -07:00
Nikolaj Bjorner ac2fe879ae update script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 15:55:00 -07:00
Nikolaj Bjorner ba2e28fa0e update build script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 14:55:38 -07:00
Nikolaj Bjorner 7ded2a90e6 remove unreachable from vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 11:55:18 -07:00
Nikolaj Bjorner 7a64c82d99 comment out pull 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 11:15:49 -07:00
Nikolaj Bjorner a873cc41bf update vsts script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 10:43:59 -07:00
Nikolaj Bjorner 8602c52bc9 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 10:41:42 -07:00
Nikolaj Bjorner afb12fe6c3 move script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-18 17:22:58 -07:00
Pierre Pronchery 5f7bd993de Add support for NetBSD 
Originally from David Holland <dholland@NetBSD.org>.
 2018-03-13 21:59:35 +01:00
Nikolaj Bjorner 3d9139f6ef bump revision 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-10 12:07:55 -08:00
Nikolaj Bjorner 0ce2001449 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-10 11:39:22 -08:00
Bruce Mitchener 878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Christoph M. Wintersteiger 0ef33a98c4
Revert "Fix encoding error" 2018-02-13 14:08:55 +00:00
Nikolaj Bjorner ad92bfb1a1 fix python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 20:19:24 -08:00
Virgile ROBLES fddc4e311f
Fix encoding error 
The encode/decode is not needed and fails if any non-ASCII character is returned by g++ or clang++
 2018-01-26 00:30:59 +01:00
Nikolaj Bjorner 1992749e78 to ascii or not to ascii #1447 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-07 18:52:00 -08:00
Christoph M. Wintersteiger 63951b815d Bumped version number. 2017-12-18 18:58:21 +00:00
Ivan Gotovchits 49678065bd fixes compilation flags for OCaml plugins 
The `-linkall` option is needed for a plugin to be standalone,
otherwise it will miss those dependencies that are not used.
 2017-12-13 14:45:06 -05:00
Nikolaj Bjorner b96dacfff2 set version, fix build of test files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 08:42:01 -08:00
Nikolaj Bjorner 161b6a9983 increase minor version, update java/.net apis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 11:51:37 -08:00
Nikolaj Bjorner 89971e2a98 remove smtlib1 dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 10:37:30 -08:00
Nikolaj Bjorner 61d149a724 fix java build problem with bool arrays 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 16:18:18 -08:00
Nikolaj Bjorner 795e0c641a add method to create bit-vectors directly from an array of Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 14:44:59 -08:00
Christoph M. Wintersteiger 7c63a5cc1d Fixed MSYS/MinGW build. Fixes #1335. 2017-11-11 16:38:53 +00:00
Christoph M. Wintersteiger 45975bec65 Improved support for MSYS/MINGW. Fixes #969. 2017-11-11 15:11:54 +00:00
Christoph M. Wintersteiger 19f43713c9 Fixed Windows build of C example. 2017-11-08 21:16:03 +00:00
Christoph M. Wintersteiger 17bcb37cf1 Fixed error handlers in Python API. 2017-11-08 20:09:18 +00:00
Christoph M. Wintersteiger bec6c3f9e2 Fixed C example build. 2017-11-08 18:22:17 +00:00
Christoph M. Wintersteiger a8b52419f5 Fixed C example build. 2017-11-08 18:14:42 +00:00
Christoph M. Wintersteiger bf563bbd5f Fixed default library path order in Python API. 2017-11-08 17:29:40 +00:00
Christoph M. Wintersteiger ef800d7b93 Fixed library path order in Python API. 2017-11-08 17:20:25 +00:00
Christoph M. Wintersteiger d2c5e0e76a Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989. 2017-11-08 16:36:47 +00:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Paul Ehrlich 2a459c5ff6 MSYS offers a MINGW shell as well. (uses different os.uname()) 2017-11-01 12:02:48 +01:00
Christoph M. Wintersteiger e50470f2c4 Added support for MSYS2 2017-10-30 18:24:38 +00:00
Nikolaj Bjorner 60b970b9ba add proofs dependency to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:23:13 -07:00
Nikolaj Bjorner db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Nikolaj Bjorner c1b243a8e3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:24:30 +01:00
Nikolaj Bjorner a625301a41 expose incremental cubing over API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-28 15:05:10 -07:00
Christoph M. Wintersteiger 9a464dded4 Removed -std=c++11 from OCaml stubs build command. Fixes #1263. 2017-09-27 14:22:59 +01:00
Nikolaj Bjorner 597f77cd77 initial sketch for dominator based simplifiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-28 20:03:31 -07:00
Nicolas Braud-Santoni 4cb7f72509 First version of the inj. tactic 2017-08-22 17:10:20 +00:00
Nikolaj Bjorner e1d08e9526 remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 20:41:29 -07:00
Dan Liew a2d7b43554 Update header includes to be relative to src/ directory. 2017-08-17 18:26:53 +01:00
Nuno Lopes 4b00bc636b revert the patch to remove no-strict-aliasing 
VS 2012 doesnt support C++11 unions..
 2017-08-14 23:00:59 +01:00
Nikolaj Bjorner dc4dbdf51e Merge branch 'master' of https://github.com/z3prover/z3 2017-08-14 12:52:41 -07:00
Nikolaj Bjorner 086ea7867e another stab at #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-14 12:52:25 -07:00
Nuno Lopes 2473c69679 Drop no-strict-aliasing and fix 2 places where it was violated 2017-08-14 20:09:49 +01:00
Nikolaj Bjorner 5fdea2cb18 use rfind instead of index to avoid prefix clashes #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 10:19:07 -07:00
Nikolaj Bjorner 8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner 2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger 6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Nikolaj Bjorner 0eb2915e83 Merge pull request #1182 from agurfinkel/spacer-z3 
Spacer
 2017-07-31 17:10:09 -07:00
Nikolaj Bjorner 8fdf3177da add initialization to unused parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:06:29 -07:00
Arie Gurfinkel 5b9bf74787 Spacer engine for HORN logic 
The algorithms implemented in the engine are described in the following papers

Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96

Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
 2017-07-31 17:02:29 -04:00
Nikolaj Bjorner b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Nikolaj Bjorner 45e31b0db3 add dummy initialization to unused variables to avoid compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 10:17:46 -07:00
Nikolaj Bjorner ca67274519 another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 12:59:34 -07:00
Nikolaj Bjorner af47aa0120 updated suspenders for #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 12:32:44 -07:00
Nikolaj Bjorner b902018373 add suspenders for #989 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:56:01 -07:00
Nikolaj Bjorner 2e3a5a2060 attempt at addressing #989 by referencing _lib directly instead of over lib() in function calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:03:18 -07:00
Daniel Perelman d57494395c Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. 2017-07-06 16:59:20 -07:00
Dan Liew d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp. 
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:53 +01:00
Dan Liew 6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp. 
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:46 +01:00
Dan Liew 229fd3dc3e [CMake] Fix dependencies for generating install_tactic.cpp. 
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

With this information CMake will now regenerate `install_tactic.cpp`
correctly.

This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:03:48 +01:00
Nikolaj Bjorner 691788f449 remove stale references to foci 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-19 20:21:08 -07:00
Christoph M. Wintersteiger a258236229 Disabled debug output 2017-05-19 18:51:52 +01:00
Christoph M. Wintersteiger 46791047fa Fixed VS 2017 platform toolset version in .vcxproj 2017-05-12 14:28:55 +01:00
Nikolaj Bjorner a64a73255e make source directory relative to build directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 15:46:24 -07:00
Nikolaj Bjorner 7731163d11 use forward slash on src include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 14:42:43 -07:00
Nikolaj Bjorner 911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Christoph M. Wintersteiger 79dcf03a42 Enabled C++11 in GCC and Clang 2017-05-05 15:01:10 +01:00
Christoph M. Wintersteiger 0ebce66c57 Fixed bug with .NET keyfile path containing spaces. Fixes #1003. 2017-05-05 14:22:40 +01:00