mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
3483 commits 24 branches 48 tags 158 MiB
Commit graph

670 commits

Author SHA1 Message Date
Nuno Lopes
1dc17db56a Fix concat() in c++ api 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-05-15 09:01:56 +01:00
Nikolaj Bjorner
ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Nikolaj Bjorner
4a9d97bd02 add concat to z3++, codeplex request 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-08 21:29:48 -07:00
Nikolaj Bjorner
901d8a9f5b change exception test to take into account new coercion operation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-08 00:38:26 -07:00
Nikolaj Bjorner
ad39811dc0 allow coercion from Boolean to Int/Real, fixes #78 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-07 21:36:37 -07:00
Nikolaj Bjorner
dc52ebd312 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-07 21:33:51 -07:00
Nikolaj Bjorner
45eda4bee7 allow coercion from Boolean to Int/Real, fixes #78 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-07 21:33:36 -07:00
Nikolaj Bjorner
99861ffc32 allow coercion from Boolean to Integers and reals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-05-07 21:32:02 -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
8c3fc574d1 comments fix 2015-04-24 15:37:45 +01:00
Christoph M. Wintersteiger
7e6ab736c0 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-04-17 16:10:13 +01:00
Christoph M. Wintersteiger
f1a1267d4c Added missing notes on fpToIEEEBV in Python. 2015-04-17 16:08:53 +01:00
Ken McMillan
af444beb2e re-indenting interp and duality 2015-04-15 12:22:50 -07:00
Christoph M. Wintersteiger
e1303e1eab Python API: Fixed expression types for floating point conversion functions. 
Partially fixes #39
 2015-04-15 12:07:53 +01: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
2f4c923216 Bugfix; InterpolationContext deleted Z3_config objects (inconsistent with non-Interpolation mk_context). 
Fixes #25
 2015-04-08 13:09:27 +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
1d9c9bcf7a Made the InterpolationContext public. 
Fixes #20
 2015-03-31 19:51:42 +02:00
Nikolaj Bjorner
39892aae10 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:46:17 -07:00
Nikolaj Bjorner
3c5897eea0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2015-03-25 11:25:12 -07:00
Nikolaj Bjorner
2aa91eee70 cache datatype util in context to avoid performance bug, codeplex issue 195 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-03-25 11:24:47 -07:00
Christoph M. Wintersteiger
a792790882 Fixed performance problems with enumeration sorts (Codeplex #190). 2015-03-25 18:08:56 +00: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
3ca3c948cf add bit-vector extract shortcuts to C++ API 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-27 11:08:49 -08:00
Nuno Lopes
a106b4125a move definition of Z3_API to the right file 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:57:40 +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
nikolajbjorner
aa40316268 rewrite terminology for policheck 
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
 2015-02-19 19:09:12 -08:00
Nikolaj Bjorner
8141dadc89 break on small cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-02-08 10:22:06 +01: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
4bed5183f8 Made DRQ objects public in Java and .NET APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 21:58:43 -06: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
3b78509d0a Improved memory use of the .NET API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-30 20:45:16 -06:00
unknown
f020b7c7b8 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-28 17:54:26 -08:00
Christoph M. Wintersteiger
b92bdaeebe ML API readme fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:51:47 +00:00
Christoph M. Wintersteiger
2f3ea1f39d removed legacy ML API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 18:48: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
9cb50c9f28 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 17:33:26 +00:00
Christoph M. Wintersteiger
5f527fa562 documentation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-24 15:54:32 +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
145e025959 FPA API naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 18:14:49 +00:00
Christoph M. Wintersteiger
89bfbd38c8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 17:11:57 +00:00
Christoph M. Wintersteiger
06051989be FPA API: Naming consistency 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 17:11:12 +00:00
Christoph M. Wintersteiger
3bf3de17e9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 17:04:18 +00:00
Christoph M. Wintersteiger
3d91510565 FPA API: naming consistency fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-23 17:03:56 +00:00
Christoph M. Wintersteiger
724e04174e Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng 2015-01-23 15:32:01 +00:00
Christoph M. Wintersteiger
8cd69acaca build fix 2015-01-23 11:34:08 +00:00