mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity
10364 commits 49 branches 53 tags 182 MiB
Commit graph

10364 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Doug Woos
8196173e29 Introduce and use labels_vec 2017-01-30 15:50:34 -08:00
Doug Woos
3791810920 add const & 2017-01-30 15:09:57 -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
Murphy Berzish
ebcfa966c7 data structure refactor in theory_str 2017-01-30 16:07:32 -05: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
Murphy Berzish
fa1ec0b80f smtlib25 draft standard in theory_str 2017-01-27 16:49:40 -05:00
Murphy Berzish
a879b24011 add str.prefixof, str.suffixof in theory_str 2017-01-27 16:26:30 -05:00
Doug Woos
a9d61d48ae Add basic Sine Qua Non filtering 2017-01-27 11:22:39 -08:00
Doug Woos
5796e15088 Thread labels through tactic system 2017-01-27 11:07:13 -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
Murphy Berzish
09ac5645e4 parameterize theory-aware activity of overlap 2017-01-22 23:21:20 -05: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
Murphy Berzish
50e2273dbd substr bugfix 2017-01-20 17:39:32 -05: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