mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
6082 commits 23 branches 48 tags 157 MiB
Commit graph

6082 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9f461dbe7b local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 06:46:01 -08:00
Nikolaj Bjorner
b4dd2f07b2 testing card_extension 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 21:53:26 -08:00
Nikolaj Bjorner
8b7bafbd9f updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 21:23:53 -08:00
Nikolaj Bjorner
1a95c33775 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-01-30 18:42:53 -08:00
Nikolaj Bjorner
685fb5d7c4 preparing for cardinality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 18:42:39 -08:00
Nikolaj Bjorner
1d1949e395 ensure that parallel threads are only invoked when thread count > 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 18:30:06 -08:00
Nikolaj Bjorner
32b5e54c8d working on card extension 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 17:22:06 -08:00
Nikolaj Bjorner
92e2d920fd working on card for sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 14:03:27 -08:00
Nikolaj Bjorner
af0ea13570 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-30 11:30:52 -08:00
Nikolaj Bjorner
76bc4f0b38 refine parsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 11:30:42 -08:00
Christoph M. Wintersteiger
841b5be40b Merge pull request #885 from martin-neuhaeusser/master 
Fix off-by-one bug in array indexing in the OCaml bindings
 2017-01-30 17:58:42 +00:00
Nikolaj Bjorner
a412a554eb merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 09:39:23 -08:00
martin-neuhaeusser
0e966f21ff Fix off-by-one bug in array indexing in the OCaml bindings 
This patch fixes an off-by-one bug that occurred in the construction of output arrays
in the OCaml bindings.
 2017-01-30 17:28:24 +01:00
Nikolaj Bjorner
dadcc6e8ff Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-30 02:09:26 -08:00
Nikolaj Bjorner
37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Nikolaj Bjorner
0123b63f8a experimenting with cardinalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-27 16:12:46 -08:00
Nikolaj Bjorner
b70f1f0319 fix overflow exposed in #880 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-27 09:47:18 -08:00
Nikolaj Bjorner
962979b09c rework sat.mus to use restart count for bounded minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 13:28:40 -08:00
Nikolaj Bjorner
49d7fd4f9c updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 09:27:57 -08:00
Nikolaj Bjorner
c3eb279637 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-26 08:37:54 -08:00
Nikolaj Bjorner
a0a81fc2d7 add format #879 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 08:37:37 -08:00
Nikolaj Bjorner
7386e2f3e9 add warning for scearios of #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:29:30 -08:00
Nikolaj Bjorner
6e6c5935d7 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-25 18:09:37 -08:00
Nikolaj Bjorner
777091e653 fix part 1 of #875 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:09:27 -08:00
Nikolaj Bjorner
4782e19086 fix bug in sat-simplifier decreasing heap values of variables that are not in the heap 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 16:21:51 -08:00
Nikolaj Bjorner
60783e5696 fix regression for z3num 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 13:26:58 -08:00
Nikolaj Bjorner
4ec4abd7e3 fix test for int-value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-23 13:31:43 -08:00
Nikolaj Bjorner
127bae85bd fixing card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-22 15:33:29 -08:00
Christoph M. Wintersteiger
adf8072eaa Added option to limit the distance of unsat core extension through patterns. 2017-01-21 12:28:37 +00:00
Nikolaj Bjorner
904f87feac working on card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-20 21:36:52 -08:00
Nikolaj Bjorner
d68cb5aee7 working on conflict resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-20 07:44:00 -08:00
Nikolaj Bjorner
1bfd09e16b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-19 19:31:24 -08:00
Nikolaj Bjorner
e23509797a access parameters from Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 19:28:20 -08:00
Nikolaj Bjorner
13099b1590 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 17:56:43 -08:00
Nikolaj Bjorner
e17c130422 updated cardinality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 17:55:15 -08:00
Christoph M. Wintersteiger
43d083bafb Windows build fix. 2017-01-19 11:19:29 +00:00
Nikolaj Bjorner
238e85867a working on card 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-18 15:40:39 -08:00
Christoph M. Wintersteiger
b9bfd4ddf5 Merge pull request #854 from angr/fix/fpic-arm 
Add -fpic to armv7/armv8 build
 2017-01-18 21:55:52 +00:00
Christoph M. Wintersteiger
5c1ffe13d1 x64 build fix for .NET 3.5 API 2017-01-18 13:06:28 +00:00
Christoph M. Wintersteiger
81c3a7dabd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-18 12:32:10 +00:00
Christoph M. Wintersteiger
a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Nikolaj Bjorner
e1640fcee9 cardinality reduction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 16:08:33 -08:00
Nikolaj Bjorner
16552d32cb Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 14:19:32 -08:00
Nikolaj Bjorner
0aa912371b Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 14:19:24 -08:00
Nikolaj Bjorner
735998c386 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 13:41:25 -08:00
Nikolaj Bjorner
873d975c77 fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 13:41:15 -08:00
Christoph M. Wintersteiger
6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Christoph M. Wintersteiger
0fae048e3e Windows build fix. 2017-01-17 12:58:32 +00:00
Christoph M. Wintersteiger
625681f82f Updated cmake build 2017-01-16 15:59:16 +00:00
Christoph M. Wintersteiger
e472a8d4cf Enabled filenames in error messages during inclusion of files. 2017-01-16 15:46:58 +00:00