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

1450 commits

Author SHA1 Message Date
Nikolaj Bjorner ef3dd32364 some cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:21:53 -08:00
Nikolaj Bjorner 7d311ac2ef use netstandard 2.0 per recommendations 
seems that now the recommended starting point is 2.0 and not lower.
 2021-12-25 13:44:49 -08:00
Nikolaj Bjorner ecf41972b1 increase minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 14:41:52 -08:00
Nikolaj Bjorner dc09d3c5ea fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 14:41:52 -08:00
Nikolaj Bjorner df8f9d7dcb Update release.yml for Azure Pipelines 2021-12-23 12:43:00 -08:00
Nikolaj Bjorner bd2a53c475 Update release.yml for Azure Pipelines 2021-12-23 11:48:08 -08:00
Nikolaj Bjorner 5d4420a763 Update release.yml for Azure Pipelines 2021-12-23 11:46:47 -08:00
Nikolaj Bjorner a00d68fe5a update release scripts and notes in master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 11:43:38 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Nikolaj Bjorner db62038845 Update nightly.yaml 
see if this gets us past the upload to GitHub issue
 2021-12-16 14:20:40 -08:00
Nikolaj Bjorner 4641a20f4f #5700 - Add download x86 as part of release NuGet 
x86 is part of nightly NuGet but was not added to the release pipeline.
 2021-12-16 13:50:31 -08:00
Nikolaj Bjorner 4587575649 if you read this commit message you probably are a programmer who has no life 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 20:25:47 -08:00
Nikolaj Bjorner 43a827c931 Update release.yml for Azure Pipelines 2021-11-18 16:05:22 -08:00
Nikolaj Bjorner 71d5d2486c Update release.yml for Azure Pipelines 2021-11-18 15:01:43 -08:00
Nikolaj Bjorner 72f28f06e4 Update release.yml for Azure Pipelines 2021-11-18 14:05:13 -08:00
Nikolaj Bjorner b95ba89dbe update release pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 13:09:13 -08:00
Nikolaj Bjorner feadfbfba4 enable publish 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 12:00:44 -08:00
Nikolaj Bjorner 5194aa186a nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-17 09:36:50 -08:00
Nikolaj Bjorner 1752055aa6 update nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:49:16 -08:00
Nikolaj Bjorner c826b64e35 prepare release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:41:51 -08:00
Weng Shiwei 723b755ca7
Fix the command of install_name_tool -id. (#5622) 
* Fix the command of `install_name_tool -id`.

* Fix: don't call `ml_example.byte`.
 2021-10-27 11:10:45 +02:00
Weng Shiwei 066076557f
Add post-install testing for ocaml binding. (#5617) 
* Add path flags for cc loader (linux).

* Fix os linking and loading problem (maybe on #4840).

* Add post-install test of OCaml binding on ubuntu.

* Minor.

* Tentative CI for macos.
 2021-10-25 11:21:02 +02:00
Weng Shiwei cd8d8bbb63
Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616) 
* Fix runtime search path for shared-lib and add '-static' to static-lib.

* Revert the change on `META.in`.
 2021-10-21 18:27:54 -04:00
Nuno Lopes 9b5ec6d004 logging cleanup 
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
 2021-08-29 12:24:19 +01:00
Nuno Lopes 1f4a7c5101 logging: don't call the returned function twice (one for log, one for return) 
Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice
it turns out simplify is not idempotent, so calling it twice can result in different results
thus breaking the log.
 2021-08-29 11:06:19 +01:00
Nikolaj Bjorner 9c7d9f06ed #5497 2021-08-22 17:22:37 -07:00
Karlheinz Friedberger 764e033bf4
Specify and document value for environment variable for loading native library in Java bindings (#5477) 
* limit range of environment variable for loading the native library in Java to "true".

This change specifies the range of values that are allowed to set the environment
variable "z3.skipLibraryLoad".
Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value.
Other values, such as "false", "0", "1", "foo", an empty or a missing value are
evaluated to "false" and cause the default loading of the native library.

* adding documentation about environment variable for (not) loading the native library in Java.

This is a follow-up commit for #4667 to provide a publicly visible documentation.
 2021-08-13 14:54:02 -07:00
Nikolaj Bjorner 6dfaaa43cd jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:38:56 -07:00
Nikolaj Bjorner 3f6a7748fa jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:38:16 -07:00
Nikolaj Bjorner ce23798cd0 coverage.yml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 22:36:14 -07:00
Nikolaj Bjorner 211a6c8752 rename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:32:20 -07:00
Nikolaj Bjorner d0686671c5 Merge branch 'master' of https://github.com/z3prover/z3 2021-07-29 11:31:45 -07:00
Nikolaj Bjorner db5252a81b add dummy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-29 11:31:39 -07:00
0152la 72d3074a44
Add Ubuntu CMake Coverage CI step (#5442) 
Adds an extra step to CI jobs which executes the Z3 test suite with
coverage enabled, and additionally executed coverage-enhancing tests
added to z3test.
 2021-07-29 11:29:49 -07:00
Nikolaj Bjorner a3010c8875 version inc, bvsort->bitvecsort 2021-07-13 17:14:47 +02:00
Nikolaj Bjorner 3a402ca2c1 Update release.yml for Azure Pipelines 2021-07-13 15:25:23 +02:00
Nikolaj Bjorner 75a5de99ca Update release.yml for Azure Pipelines 2021-07-13 15:24:19 +02:00
Nikolaj Bjorner 4c53655be7 add z3doc build to release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 23:26:48 +02:00
Nikolaj Bjorner 10ad5bae21 increment version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 06:17:58 +02:00
Nikolaj Bjorner bc2e6ce037 Update release.yml for Azure Pipelines 2021-07-10 22:42:02 +02:00
Nikolaj Bjorner 34885562e0 try without #!/bin/env python #5397 2021-07-10 15:20:56 +02:00
Iain Scott d61d5081a2
Delete unused NuGet release script. (#5351) 2021-06-16 10:48:51 -05:00
Nikolaj Bjorner 39af2a188d centos -> glibc 2021-06-04 15:54:19 -07:00
Nikolaj Bjorner 84b86ac8d2 updated ref to esrp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-04 15:13:34 -07:00
Nuno Lopes 2f9be23d90 attempt to fix MSVC build 2021-06-04 19:49:59 +01:00
Nikolaj Bjorner 88ec0f9fdd undo cxx hoist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-04 11:39:46 -07:00
Nikolaj Bjorner 3655c399f5 hoist c++ flags 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-04 11:33:56 -07:00
Nikolaj Bjorner 654e53e762 auxiliary build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-04 11:15:13 -07:00
Nikolaj Bjorner 7ce88ec032 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-06-04 11:02:00 -07:00
Nikolaj Bjorner dea7c92730 updated nightly 2021-06-04 10:54:32 -07:00
Iain Scott 48beb814f5
Use more generic linux-x64 for NuGet rid instead of specific ubuntu, debian, etc. (#5310) 2021-05-28 13:53:52 -07:00
Nikolaj Bjorner 8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Iain Scott c18f012c83
Remove x64 suffix from NuGet package names. (#5292) 2021-05-21 13:51:02 -07:00
Matt Thornton ce1a48486e
Fix NuGet package name and glibc rid. (#5290) 2021-05-21 08:41:29 -07:00
Nikolaj Bjorner a59dcfdeab update python tag 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-20 15:23:39 -07:00
Matt Thornton 9cc1549dbe
Use osx-x64 for mac rid rather than macos. (#5288) 2021-05-20 15:19:31 -07:00
Nikolaj Bjorner a166aca48e na 2021-04-08 15:48:07 -07:00
Nikolaj Bjorner 9ef7cf1e81 test old connection 2021-04-08 12:14:29 -07:00
Nikolaj Bjorner 887b62efe6 another patch 2021-04-07 18:20:45 -07:00
Nikolaj Bjorner 6e1ac19c44 new name 2021-04-07 17:43:32 -07:00
Nikolaj Bjorner 90995b63c3 fix nightly 2021-04-07 15:43:39 -07:00
Nikolaj Bjorner eb13ad14e5 python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 16:26:44 -07:00
Nikolaj Bjorner ab0735fde2 separate component for asserted_formulas to break dependency cycles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 15:51:38 -07:00
Nikolaj Bjorner 25343232ca add dependency 2021-03-17 15:36:02 -07:00
Nikolaj Bjorner ddbcd08d46 move asserted_formulas to solver scope 2021-03-17 15:02:16 -07:00
Andrew V. Jones d0515dca50
Circular seq axioms node (#5104) 
* Dealing with ambiguity when calling 'find_file' #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Correcting ambiguity when calling 'find_file' if the file is in the current src dir #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

* Ensuring consistency when obtaining the original include #5089

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
 2021-03-16 06:58:54 -07:00
Nikolaj Bjorner d03fdf5fed more descriptive naming convention 2021-03-15 15:48:33 -07:00
Nikolaj Bjorner 4b3fecc35e remove dependency on ast from params 2021-03-15 15:40:41 -07:00
Nikolaj Bjorner 1cb0dbae51 missing dependency for python build 2021-03-14 20:45:30 -07:00
Nikolaj Bjorner 8412ecbdbf fixes to new solver, add mode for using nlsat solver eagerly from nla_core 2021-03-14 13:57:04 -07:00
Nikolaj Bjorner bef6f1a729 fix build 2021-03-02 13:51:58 -08:00
Nuno Lopes d396d46bd1 let's test if all the buildbots are happy with C++17 
it's stil a bit too early for C++20
 2021-02-18 18:13:10 +00:00
Nikolaj Bjorner 85f0084e9c set options and change VS for nightly 2021-02-12 13:41:30 -08:00
Nikolaj Bjorner 80d297dca2 Try to move using windows latest instead of VS2017 2021-02-12 12:45:21 -08:00
Nikolaj Bjorner d0c96abe30 log classificaiton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 14:44:05 -08:00
Nikolaj Bjorner 1d12b72bbc log classificaiton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 14:43:05 -08:00
Nikolaj Bjorner 98eae28fca try to update setup.py to libc naming 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:52:05 -08:00
Nikolaj Bjorner b6294ab235 is glibc the new centos? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:17:33 -08:00
Nikolaj Bjorner c03bd5e1c8 is glibc the new centos? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:17:04 -08:00
Nikolaj Bjorner 5d46ac0aca is glibc the new centos? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 11:14:39 -08:00
Nikolaj Bjorner b7d1d03b08 try revert to u18 for centos zip 2021-02-11 10:36:48 -08:00
Nikolaj Bjorner 2301fce65e it helps to spell 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 09:44:03 -08:00
Nikolaj Bjorner 9883a0b983 downgrade to Ubuntu 18 for ocaml doc build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-02-11 09:43:22 -08:00
Nikolaj Bjorner 9cdb875ba2 remove use of deprecated linux_distribution 2021-02-11 09:40:23 -08:00
Don Syme 504b6559ab
[WIP] Suggestion: build .NET package for both x86 and x64 and rename (#5021) 
* build package for x86

* build package for x86

* build package for x86

Co-authored-by: Don Syme <donsyme@fastmail.com>
 2021-02-11 09:29:32 -08:00
Nikolaj Bjorner 16448104eb add new model event handler for incremental optimization 2021-02-05 17:11:04 -08:00
Nikolaj Bjorner c623e2db28 typo 2021-02-01 09:14:26 -08:00
Nikolaj Bjorner 60cc9d8182 set unicode by default 2021-01-31 11:32:33 -08:00
Nikolaj Bjorner 39bfdbd8c0 make the right diretory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 05:01:16 -08:00
Nikolaj Bjorner c99b805c14 mld 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 18:37:38 -08:00
Nikolaj Bjorner 87cd3487e5 missing pattern dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:44:47 -08:00
Nikolaj Bjorner 34c34b68ee one more nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 16:40:59 -08:00
Nikolaj Bjorner 41a4d102f4 try ocamlfind in the loop 
Thanks to @c-cube
 2021-01-29 13:37:16 -08:00
Nikolaj Bjorner b11203e2d2 try local env 2021-01-29 08:41:14 -08:00
Nikolaj Bjorner 1d7cabaf9a typo 2021-01-29 08:15:40 -08:00
Nikolaj Bjorner a2d344c401 use build path 2021-01-29 07:32:04 -08:00
Nikolaj Bjorner 1f71aeded9 ocamldoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:47:10 -08:00
Nikolaj Bjorner 5c9b205dfc run mk_api_doc in the same environment as make where opan config env is used 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-29 06:25:24 -08:00
Nikolaj Bjorner 8a229bf684 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 22:39:02 -08:00
Nikolaj Bjorner c271a42a2e change zip command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 21:01:08 -08:00