mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
3494 commits 49 branches 53 tags 182 MiB
Commit graph

3494 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6aa0086969 adding wpm2 algorithm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-20 16:46:23 -08:00
Nikolaj Bjorner
0deb951873 different strategies for weighted 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-20 12:04:17 +01:00
Ken McMillan
48e10a9e2d dealing with incompleteness issues in duality 2013-12-19 11:05:56 -08:00
Nikolaj Bjorner
26237a3727 debug benchmarks, theory_pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-19 07:40:18 +02:00
Nikolaj Bjorner
0d6220f383 revert is_all_int bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 21:53:04 +02:00
Nikolaj Bjorner
cff0e0fc6c debug min_max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 09:18:06 +02:00
Nikolaj Bjorner
392b419367 debug min_max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 09:14:10 +02:00
Nikolaj Bjorner
eb1b578bfb fixing optimizaiton bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 08:43:07 +02:00
Nikolaj Bjorner
22166d0760 remove print 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 05:59:16 +02:00
Nikolaj Bjorner
72130ac7b9 fix lower bound update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 05:49:43 +02:00
Christoph M. Wintersteiger
8fb36bd41d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-17 13:53:28 +00:00
Christoph M. Wintersteiger
0b3e50d6e6 Added #include <algorithm> because VS2013 needs that for std::max/std::min 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-17 13:53:10 +00:00
Nikolaj Bjorner
02f74f1028 trying Cezary's example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-17 05:03:20 +02:00
Nikolaj Bjorner
56b9c4c8a2 fix bugs reported by phan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-17 04:20:24 +02:00
Ken McMillan
a318b0f104 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-16 12:45:52 -08:00
Ken McMillan
3588d4a1ca fixing templates for broken windows hash functions 2013-12-16 12:41:43 -08:00
Nikolaj Bjorner
1bcf5b8b5f remove auxiliary variables from weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 11:42:28 +02:00
Nikolaj Bjorner
1ca44ed316 handle proof-wrapper justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 11:25:50 +02:00
Nikolaj Bjorner
e38729a1c6 redo marking mechanism as marked literals can disappear from lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 07:50:24 +02:00
Nikolaj Bjorner
b1caadee49 disabling skip steps to avoid bogus behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 05:24:05 +02:00
Nikolaj Bjorner
15b64261dd fix wmaxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-16 04:55:56 +02:00
Ken McMillan
1e8c04be8e fixing templates for broken windows hash functions 2013-12-15 17:31:46 -08:00
Ken McMillan
852f53d6a6 fixed memory error 2013-12-15 17:24:51 -08:00
Ken McMillan
ebc8a43fe3 removing address dependencies 2013-12-15 15:49:06 -08:00
Nikolaj Bjorner
909408d6ef fix is_all_int bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 10:58:23 +02:00
Nikolaj Bjorner
ddd0bf875d fix bugs in optimization for integers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 08:46:24 +02:00
Nikolaj Bjorner
b764c7bbee fixes to bugs exposed by regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 05:25:47 +02:00
Nikolaj Bjorner
fe5c42c90f fixes to bugs exposed by regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 05:23:47 +02:00
Nikolaj Bjorner
50f18a77af disable 'optimization' that led to wrong model' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 02:40:52 +02:00
Ken McMillan
eee2d7af94 porting to linux 2013-12-14 12:47:02 -08:00
Nikolaj Bjorner
ac893e907f fixes to maxsmt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 16:06:03 +02:00
Nikolaj Bjorner
5f72325e99 working on maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 10:00:21 +02:00
Nikolaj Bjorner
04824d86df fixes to model generation of weighted maxsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:37:42 +02:00
Nikolaj Bjorner
5225ea18b7 fix lower/upper bound updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-14 09:04:48 +02:00
Ken McMillan
3764064e98 fixed some address dependencies 2013-12-13 18:41:35 -08:00
Nikolaj Bjorner
8c85ee6b7c fixing lex optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-13 23:36:42 +01:00
Ken McMillan
bb61f17989 trying to figure out address dependency 2013-12-13 13:45:40 -08:00
Ken McMillan
ac9a7748e8 trying to fix address depedency in duality_solver.cpp 2013-12-13 13:14:04 -08:00
Ken McMillan
0449598530 fussing more with qe in duality 2013-12-13 12:41:51 -08:00
Ken McMillan
a410e7f716 fussing with qe in duality 2013-12-13 12:21:54 -08:00
Ken McMillan
bfa6c99676 still trying to get stl to work 2013-12-12 18:38:09 -08:00
Ken McMillan
cf3ede92ad fix for broken windows stl 2013-12-12 18:35:43 -08:00
Ken McMillan
2cc8132191 still simplifying quantified interpolants in duality 2013-12-12 18:25:24 -08:00
Nikolaj Bjorner
df5c2adc4e debug opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 15:39:38 -06:00
Nikolaj Bjorner
f41d23bc0f debugging model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-12 12:18:34 -06:00
Nikolaj Bjorner
56562a725d fixing bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-11 19:24:20 -06:00
Nikolaj Bjorner
eacb48268c fixing bugs exposed by msf unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-11 19:02:36 -06:00
Ken McMillan
ea8eb74744 simplifying quantified interpolants in duality 2013-12-11 16:25:59 -08:00
Anh-Dung Phan
a737639790 Skip lower bound assertions for unbounded objectives 2013-12-11 12:56:48 -08:00
Anh-Dung Phan
1c0442ea31 Workaround for theory vars without unassigned atoms 2013-12-11 11:49:40 -08:00