mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity
19575 commits 22 branches 48 tags 155 MiB
Commit graph

42 commits

Author SHA1 Message Date
Nikolaj Bjorner f7691d34fd fix generic example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-02-21 08:16:01 -08:00
Nikolaj Bjorner 5b385bd2fe fix #6665 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-04-02 10:58:21 -07:00
Nikolaj Bjorner ce09c2ea6d fix build 2023-03-27 09:56:09 -07:00
Nikolaj Bjorner b4ad747e0b fix #6644 2023-03-27 09:00:38 -07:00
Nikolaj Bjorner a24a922688 fix #5915 2022-03-22 16:03:44 -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
Alexander Kreuzer dc5fa89de3
Mixing Integers and Rational in the new Java API #5085 (#5098) 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 05:24:23 -07:00
Addison Crump 3bca1fbcd8
Java type generics (#4832) 
* Generify, needs some testing and review

* Remove unnecessary change

* Whoops, ? capture that type

* Misread the docs, whoops

* More permissible arithmetic operations

* Implement believed Optimize generics

* Missed a few generics

* More permissible expr for arrays in parameters

* More permissible expr for bitvecs in parameters

* More permissible expr for bools in parameters

* More permissible expr for fps in parameters

* More permissible expr for fprms in parameters

* More permissible expr for ints in parameters

* More permissible expr for reals in parameters

* Undo breaking name conflict due to type erasure; see notes

* Whoops, fix typing of ReExpr

* Sort corrections for Re, Seq

* More permissible expr for regular expressions in parameters

* Fix name conflict between sequences and regular expressions; see notes

* Minor typo, big implications!

* Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency

* More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture

* Be less dumb and just type it a little differently

* Update examples, make sure to type Expr and FuncDecl sort returns

* General fixups

* Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction

* Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird
 2020-11-30 10:04:54 -08:00
Richard Bradley 04e0b767c3 Fix sudoku Java example 2019-07-31 23:32:38 +01:00
Bruce Mitchener a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner 648a531950 update java example to bypass bit-rot 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-02 09:50:29 -07:00
Nikolaj Bjorner 3736c0ae8b touch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 08:52:25 -07:00
Nikolaj Bjorner 8ecff9e5ee fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 08:04:10 -07:00
Nikolaj Bjorner e98c808f47 fixing compilation errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 03:18:29 -07:00
Nikolaj Bjorner bb041495e3 fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-02 14:00:37 -07:00
Bruce Mitchener 73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner c18d60a9c5 fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 20:56:36 -08:00
Christoph M. Wintersteiger d8a02bc040 Fixed AST translation functions in .NET and Java APIs. Fixes #1073. 2017-06-14 13:24:54 +01:00
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Christoph M. Wintersteiger e9eb88e1b3 fixed java build issues. Relates to #648. 2016-06-24 15:08:56 +01:00
Christoph M. Wintersteiger cbda38ee80 Added finite domain expressions and numerals to the .NET, Java, and Python APIs. 
Relates to #318
 2015-12-02 17:01:52 +00:00
Nikolaj Bjorner a0894ac7bf add basic example of using optimizaiton context to Java as raised in issue #179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-30 11:32:14 -03:00
Christoph M. Wintersteiger 8862cb4833 Java example: Removed throws declarations for Z3Exception. 2015-04-09 14:52:50 +01:00
Christoph M. Wintersteiger 9b137d54d3 Bugfix and new examples for implicit assumptions in Z3_solver_assert_and_track. Thanks to Amir Ebrahimi for reporting this issue! 
(See http://stackoverflow.com/questions/28558683/modeling-constraints-in-z3-and-unsat-core-cases)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-18 16:25:27 +00:00
Christoph M. Wintersteiger b96551a1a2 .NET/Java/ML: Moved toggle_warning_messages to Global, added en/disable_trace. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 14:17:39 +00:00
Christoph M. Wintersteiger d7a62baef4 Improved memory use of the Java API. Thanks to Joerg Pfaehler for reporting this issue! 
+ formatting

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 21:10:22 -06:00
Christoph M. Wintersteiger 7fe9ad5cb4 Java FPA API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:22:02 +00:00
Christoph M. Wintersteiger 0faf329054 FPA API: bugfixes and examples for .NET and Java 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-03 17:26:58 +00:00
Christoph M. Wintersteiger 2f9b3c42eb Java API cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 19:43:36 +01:00
Christoph M. Wintersteiger cc99e96786 Java API Cleanup 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-24 18:00:36 +01:00
Christoph M. Wintersteiger 5fe58c2f2d Java API: renamed assert_(...) to add(...) 
.NET API: added alias Add(...) for Assert(...)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-26 19:13:48 +00:00
Christoph M. Wintersteiger 91402f2060 C API: fixed mk_context/mk_context_rc exception behaviour 
Adjusted .NET/Java APIs accordingly.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-02-08 18:54:44 +00:00
Christoph M. Wintersteiger 4b18c8f9c4 Java API: syntactic adjustments, getters, setters, 
... convenience parameters, etc.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-17 19:31:02 +00:00
Christoph M. Wintersteiger 4d1d784a1c Java+.Net Examples: refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-12-04 19:32:20 +00:00
Leonardo de Moura 54e452a1af chasing bug in the Java bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 16:58:44 -08:00
Leonardo de Moura 847c5f9691 fixing problems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-12-03 11:55:24 -08:00
Christoph M. Wintersteiger 692593baaa Java API: 32-bit issues and bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 22:31:07 +00:00
Christoph M. Wintersteiger 0c1f2a8281 Java API: Added exception wrappers and build dependencies. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-30 15:39:25 +00:00
Leonardo de Moura 001c8487e9 small change to be able to test java example on linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2012-11-29 09:13:24 -08:00
Christoph M. Wintersteiger bbfd9dd19f Java API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-28 22:20:36 +00:00
Christoph M. Wintersteiger 519d308b86 Java API: bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-28 14:59:39 +00:00
Christoph M. Wintersteiger a9883e972f Java API: Bugfixes and Example. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2012-11-27 23:06:35 +00:00