mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity
6858 commits 24 branches 48 tags 158 MiB
Commit graph

167 commits

Author SHA1 Message Date
Nikolaj Bjorner
d7dcd022b9 seq, API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 18:49:21 -08:00
Nikolaj Bjorner
c1ebf6b4fc seq + API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-04 18:01:48 -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
Christoph M. Wintersteiger
383d06b225 Bugfix for Expr.isInt in .NET, Java, ML. 
Fixes #370
 2015-12-10 15:13:55 +00:00
Christoph M. Wintersteiger
00271e5531 C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes. 2015-12-03 17:33:25 +00: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
Christoph M. Wintersteiger
9e756fb6db Warning fix for Comparable<T> in Java API 2015-12-02 14:42:36 +00:00
Christoph M. Wintersteiger
e8d37dba9c Added comments for quantifier constructors. Fixes #319. 2015-11-16 21:58:17 +01:00
Nikolaj Bjorner
4685a5f8ba add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 16:42:13 -08:00
Nikolaj Bjorner
13b19eb351 add translate facility to Java/C# APIs, request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:10:21 -08:00
Christoph M. Wintersteiger
715050da0b Java API comments fix. 2015-11-04 13:34:50 +00:00
Christoph M. Wintersteiger
cab42d2c66 Clarified documentation of par-or tactic. 
Relates to #269.
 2015-10-28 18:50:22 +00:00
Paul Phillips
64a5247813 Changed references to help-tactics to help-tactic. 2015-10-25 11:45:46 -07:00
Christoph M. Wintersteiger
ef80645a71 Java API context deletion concurrency fix. 
Relates to #205 #245
 2015-10-14 22:13:43 +01:00
Christoph M. Wintersteiger
a71a333722 Minor Java API fix. 2015-10-14 21:33:30 +01:00
Christoph M. Wintersteiger
2d3c12716a Bugfix for Java memory leaks. 
Relates to #205 #245
 2015-10-14 21:19:59 +01:00
Christoph M. Wintersteiger
58d3329190 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-14 13:59:20 +01:00
Christoph M. Wintersteiger
24532474a0 Bugfix for concurrent Context creation in Java and .NET. 
Relates to #205 #245
 2015-10-14 13:58:51 +01:00
Christoph M. Wintersteiger
b66f34f0d2 Removed unnecessary debug output. 2015-10-14 12:53:18 +01:00
Christoph M. Wintersteiger
bae3a76c8a Removed unnecessary debug output. 2015-10-14 12:52:16 +01:00
Christoph M. Wintersteiger
e312b47be6 Bugfix for object finalization in Java API. 
Relates to #205 and #245
 2015-10-14 12:43:09 +01:00
Christoph M. Wintersteiger
6263252bf5 Bugfix for concurrent garbage collection in Java API. 
Relates to #205 and #245
 2015-10-14 12:42:27 +01:00
Nikolaj Bjorner
eb5af100bd adding optimize bindings for ML, adding get_reason_unknown to optimize, mentioned in pull request issue #188, second edition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-09 17:49:20 +02: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
Nikolaj Bjorner
318ee3a86d fix issue #176 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-28 22:31:41 -03:00
Nikolaj Bjorner
7d5c144dfe add java Optimize context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-16 18:00:45 -07:00
Nikolaj Bjorner
92f731e51c add java Optimize context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-16 18:00:26 -07:00
Christoph M. Wintersteiger
1bad614646 Fixed .equals for AST, FuncDecl, and Sort, and AST.compareTo in Java 
Fixes #143
 2015-07-14 13:09:00 -07:00
Christoph M. Wintersteiger
5f755a5bd8 Adjusted return types of set functions to ArrayExprs in Java and .NET 
Fixes #137
 2015-07-14 13:07:16 -07:00
Nikolaj Bjorner
ade9b2830a various partial fixes for issue #143 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-10 08:16:57 -07:00
Nikolaj Bjorner
e81dc5a0a0 fixes issue #143 and memory leak on theory plugin setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-26 09:03:56 +02:00
Christoph M. Wintersteiger
004bf1471f Added conversion function for Goal to Expr conversion in .NET, Java, ML 2015-06-10 13:17:34 +01:00
Christoph M. Wintersteiger
98f2de3216 Added Z3_fpa_get_numeral_significand_uint64 to .NET, Java, and ML APIs. 2015-06-09 12:57:19 +01:00
Christoph M. Wintersteiger
624cc8a874 Bugfixes for FPA API. Thanks to Christian Dernehl for reporting these. 2015-06-09 11:53:43 +01:00
Nikolaj Bjorner
e483efd3f4 fixes to Euclidean solver, fixes #100 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:21:20 -07:00
Nikolaj Bjorner
cb00555635 local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-05-27 09:18:52 -07:00
Christoph M. Wintersteiger
91352369a9 Added conversion functions to ASTVectors in .NET and Java. 
Fixes #108
 2015-05-26 11:20:19 +01:00
Christoph M. Wintersteiger
d8f6d84217 Updates for the .NET, Java, and ML APIs for recently changed fixedpoint and interpolation functionality. 
Fixes #103
 2015-05-23 16:53:47 +01:00
Nikolaj Bjorner
279ef05713 expose BoolExpr[] for ASTVector and merge common functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-22 08:57:05 -07:00
Nikolaj Bjorner
b4f72c8145 Revert "Change ASTVector to Expr[] in interpolation result" 2015-05-22 08:24:45 -07:00
Marcus Völker
a229416a2b Change ASTVector to Expr[] in interpolation result 2015-05-22 15:55:09 +02:00
Christoph M. Wintersteiger
1702a55018 Introduced return value classes for interpolation functions. 
Fixes #82.
 2015-05-15 13:50:55 +01: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
2948e47240 Java API doc fix 2015-04-13 17:43:29 +01:00
Nikolaj Bjorner
3ba2e712b2 merge with unstable branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-12 15:54:52 -07:00
Christoph M. Wintersteiger
b7bb53406f Turned Z3Exception into a RuntimeException such that throws declarations are not needed anymore. Thanks to codeplex user steimann for this suggestion. 2015-04-08 13:16:32 +01:00
Christoph M. Wintersteiger
b47851d7da Made GetInterpolant and ComputeInterpolant public in Java and .NET. 
Fixes Codeplex discussion #616450
 2015-04-02 16:51:30 +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
1c77ad00c3 Added accessors to enumeration sorts. Thanks to codeplex user steimann for suggesting this. 
(http://z3.codeplex.com/workitem/195)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-03-24 21:42:05 +00:00
nikolajbjorner
aa40316268 rewrite terminology for policheck 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-19 19:09:12 -08:00