mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
10864 commits 23 branches 48 tags 157 MiB
Commit graph

10864 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 62ec02e50f extend rewriting features for arrays, #2151 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 12:29:50 -07:00
Lev Nachmanson e59d60fbbe Remove unnecessary null pointer checks 2019-03-22 10:47:11 -07:00
Lev Nachmanson 61ac006cbe Remove unnecessary null pointer checks 2019-03-22 10:32:33 -07:00
Lev Nachmanson 6e5d0b7594 Remove unnecessary null pointer checks 2019-03-22 09:43:34 -07:00
Lev Nachmanson eae4fd6afd fix the build lp.cpp in test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Lev Nachmanson 885d640301 make explicit rational(double)constructor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-19 19:45:33 -07:00
Nikolaj Bjorner 057151c7a8 fix #2188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-18 07:56:25 -07:00
Nikolaj Bjorner 93a4afe5d2 add multi-argument select for C# 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:36:29 -07:00
Nikolaj Bjorner d953bdd2e4 add multi-argument select for C# 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:35:03 -07:00
Nikolaj Bjorner 9bc4914268 add nth remapping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:32:28 -07:00
Nikolaj Bjorner 834cf962a1 expose nth over API, change _getitem_ in python bindings to use nth instead of at, add 'at' operator for the purpose of the previous semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-17 11:23:01 -07:00
Nikolaj Bjorner f534f79a21 include all sorts from declarations, and include sorts from datatypes #2185 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 18:16:09 -07:00
Nikolaj Bjorner 957c3be02f build errors/warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 16:52:18 -07:00
Nikolaj Bjorner 36a2052cca update to TWEAK 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 15:46:48 -07:00
Nikolaj Bjorner 433064dee9 Merge branch 'master' of https://github.com/z3prover/z3 2019-03-16 11:53:02 -07:00
Nikolaj Bjorner 869cb66736 step 1 in aligning version tweaks for #2184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-16 11:52:55 -07:00
Nikolaj Bjorner 8c177c019b
Merge pull request #2183 from ahelwer/master 
Use release commit hash in nuspec
 2019-03-15 15:28:54 -07:00
Andrew Helwer a492eb0209 Fixed missed renamed variable 2019-03-15 15:23:33 -07:00
Andrew Helwer f0aebb1600 Fixed nuget package spec generation code 2019-03-15 15:20:32 -07:00
Nikolaj Bjorner 340f30c41d Merge branch 'master' of https://github.com/z3prover/z3 2019-03-14 18:22:49 -07:00
Nikolaj Bjorner 7b50fca02c display dimacs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 18:22:42 -07:00
Nikolaj Bjorner 1645fcee0a
Merge pull request #2181 from Z3Prover/ahelwer-patch-1 
Remove dependency on TargetPlatform macro
 2019-03-14 15:54:46 -07:00
Andrew Helwer 0a477a0a93
Remove dependency on TargetPlatform macro 
Unnecessary, since dropping support for x86
 2019-03-14 15:46:03 -07:00
Nikolaj Bjorner e19c119496 copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 15:41:52 -07:00
Nikolaj Bjorner 001c120169 x64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 15:35:33 -07:00
Nikolaj Bjorner 038f992ff4 remove platformtarget for dotnetcore spec 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-14 12:48:27 -07:00
Nikolaj Bjorner 90b78eb64a use random_next instead of library random 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-13 19:59:05 -07:00
Nikolaj Bjorner c499bd4116
Merge pull request #2180 from levnach/Prover 
snap variables to bounds when maximizing terms
 2019-03-13 19:09:40 -07:00
Nikolaj Bjorner d642ed5591 adding targets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-13 18:03:18 -07:00
Lev Nachmanson f336039da3 snap variables to bounds when maximizing terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2019-03-13 15:28:50 -07:00
Nikolaj Bjorner 75b1e8fe27 add tracing for 2157 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-12 20:12:17 -07:00
Nikolaj Bjorner 519e83bce4 Merge branch 'master' of https://github.com/z3prover/z3 2019-03-12 19:07:59 -07:00
Nikolaj Bjorner 8f1c5239be updates for #2151 #2152 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-12 13:39:57 -07:00
Nikolaj Bjorner 05663592ee fix #2173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-10 14:42:00 -07:00
Nikolaj Bjorner 376076ea9b Merge branch 'master' of https://github.com/z3prover/z3 2019-03-09 19:31:37 -08:00
Nikolaj Bjorner 5bc0fb47a8 fix #2169 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-09 19:31:30 -08:00
Nuno Lopes 9736c46375 constify is_threaded if MT is disabled 2019-03-08 11:16:10 +00:00
Nuno Lopes cd4b53500c avoid a few str copies + symbol hiding 2019-03-08 10:13:46 +00:00
Nuno Lopes 70ada9919e cmake: fix windows build with long absolute directory names 2019-03-07 11:09:25 +00:00
Nuno Lopes deb2deb4ad fix linking of .so on old build system 2019-03-07 10:04:06 +00:00
Nuno Lopes c0f7afacc4 bump cmake minimum version to 3.4 as it was released 3+ years ago 
some misc compiler flags cleanup
 2019-03-07 09:58:36 +00:00
Nikolaj Bjorner c7bbf2f8de Merge branch 'master' of https://github.com/z3prover/z3 2019-03-07 00:07:54 -08:00
Nikolaj Bjorner 9d2a106838 unused variable warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-07 00:07:48 -08:00
Nikolaj Bjorner f7773fdcc8 rewrite quantifiers in model evaluator #2171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 22:04:31 -08:00
Nikolaj Bjorner 5abc4a6d68 rewrite quantifiers in model evaluator #2171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 22:03:57 -08:00
Nikolaj Bjorner 65f0da9806
Merge pull request #2170 from mtrberzi/issue2092 
z3str3: fix str.indexof with offset (issue #2092)
 2019-03-06 17:36:46 -08:00
Nikolaj Bjorner de7731fd22
Merge pull request #2167 from Egor18/master 
Fix misprint
 2019-03-06 17:36:28 -08:00
Nikolaj Bjorner d6e0f7659d Merge branch 'master' of https://github.com/z3prover/z3 2019-03-06 10:18:36 -08:00
Nikolaj Bjorner 5a02edc8cd add recognizer for distinct 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-06 10:18:29 -08:00
Murphy Berzish e05596e7e5 z3str3: fix str.indexof with offset (issue #2092) 2019-03-06 11:41:56 -05:00