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

3902 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a47f3df703 fix bug in unsat core extraction in sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-18 23:43:51 -07:00
Nikolaj Bjorner
9e3e52f4f6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-18 18:38:35 -07:00
Ken McMillan
da76a51ce6 merging with unstable 2014-08-18 17:14:49 -07:00
Ken McMillan
70a1155d71 fixed duality bug and added some code for returning bounded status (not yet used) 2014-08-18 17:13:16 -07:00
Nikolaj Bjorner
1c56d6ee95 align lengths of weights and soft constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-18 01:17:26 -07:00
Nikolaj Bjorner
ddbff6f77b revamp configuration parameter names for fixedpoint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-18 01:03:11 -07:00
Nikolaj Bjorner
d4ec48219f Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-08-17 21:22:29 -07:00
Nikolaj Bjorner
60054ce469 fix cache bug in PDR reported by Phillip Ruemmer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-17 21:20:56 -07:00
Nikolaj Bjorner
f748a03ac7 opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-16 22:31:54 -07:00
Nikolaj Bjorner
33f74b9c9f sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 22:49:21 -07:00
Nikolaj Bjorner
ddb9e6e8d4 fix flipper 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 18:30:06 -07:00
Nikolaj Bjorner
be1cceba34 fix scope and mus with user-scopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 11:29:08 -07:00
Nikolaj Bjorner
ee1a1b1135 refactor sat/sls interface. Remove wpm2 and bvsls dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 10:40:44 -07:00
Christoph M. Wintersteiger
37ed4b04d0 Bugfix: param_refs didn't make it through to smt::solver (smt_params) in some cases. 
Thanks to user xor88 for pointing us in the right direction!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-14 12:18:00 +01:00
Christoph M. Wintersteiger
0cf1f9c210 .NET API context refcounting; changed int to long to be on the safe side on 64-bit platforms. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-14 12:15:58 +01:00
Nikolaj Bjorner
a02cab2194 wsls code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-13 16:58:02 -07:00
Christoph M. Wintersteiger
606eeb658e bugfix for solver parameters that did not get passed on (codeplex discussion 560796). 
Thanks to user xor88 for reporting this issue.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-13 23:05:45 +01:00
Nikolaj Bjorner
999db1e280 sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-13 01:22:45 -07:00
Nikolaj Bjorner
cafb31ff94 sls updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 22:14:57 -07:00
Nikolaj Bjorner
1412c183d4 finish sls code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 21:42:33 -07:00
Nikolaj Bjorner
311183e19a local updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 19:26:06 -07:00
Nikolaj Bjorner
276bef1c20 local updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 19:25:39 -07:00
Nikolaj Bjorner
180b0d4ec9 add sls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-12 19:24:31 -07:00
mattpark
5a45711f22 Dealt with some concurrency issues due to concurrent GC. 2014-08-12 10:16:00 +01:00
Nikolaj Bjorner
470b5c11b9 mus logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-11 08:06:29 -07:00
Nikolaj Bjorner
1652c16163 add missing code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-10 22:13:55 -07:00
Nikolaj Bjorner
39d90f914d NA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-10 21:27:07 -07:00
Nikolaj Bjorner
e832bdd257 fix bug in blocked clause elimination that was enabled for external variables, fix other bugs in maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-10 21:23:05 -07:00
Nikolaj Bjorner
47ac5c0633 fix doc bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-09 11:41:04 +09:00
Christoph M. Wintersteiger
0df0174d62 .NET API: Enabled .xml documentation generation by default. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-08 15:24:08 +01:00
Nikolaj Bjorner
3d995648ee partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-07 20:39:20 +09:00
Ken McMillan
e17af8a5de doc fix for interpolation bindings for python 2014-08-06 15:34:58 -07:00
Ken McMillan
6880945435 added simple interpolation bindings for python 2014-08-06 15:30:24 -07:00
Ken McMillan
5a107095c9 removing python changes for interp 2014-08-06 11:32:51 -07:00
Ken McMillan
b933a4da85 merged python interp changes 2014-08-06 11:26:44 -07:00
Ken McMillan
31d4e6aa00 merging with unstable 2014-08-06 11:17:44 -07:00
Ken McMillan
ab13987884 working on python interp 2014-08-06 11:16:24 -07:00
Ken McMillan
c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Ken McMillan
7bf87e76ea fix for tree interpolation 2014-08-05 11:11:43 -07:00
Christoph M. Wintersteiger
4610acca0f FPA: reduced number of temporary variables. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-04 17:10:56 +01:00
Christoph M. Wintersteiger
8b40d4a735 FPA theory bug fixes. 
Also removed unnecessary intermediate variables.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-04 17:00:04 +01:00
Nikolaj Bjorner
317e76a11b mss and mss-mus-maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-03 20:23:10 -07:00
Nikolaj Bjorner
d429e72e92 v2 of dual maxres engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-03 18:50:21 -07:00
Nikolaj Bjorner
622d8b5cd1 moving to maxres consolidation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-03 00:18:09 -07:00
Nikolaj Bjorner
6a4c08c7cb moving to maxres consolidation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-03 00:17:55 -07:00
Nikolaj Bjorner
a41b1d34ce moving dual solver to maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-03 00:08:57 -07:00
Nikolaj Bjorner
5e026b7897 mss and maxres tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-02 23:34:43 -07:00
Nikolaj Bjorner
9681dc12b1 tuning auxiliary literals and clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-02 14:25:04 -07:00
Nikolaj Bjorner
8814ba0629 testing maxres with sat core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-02 12:27:57 -07:00
Nikolaj Bjorner
b928734348 perf improvements, mus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-01 16:11:52 -07:00