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

5145 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
363af825c0 working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 20:25:36 -08:00
Nikolaj Bjorner
c14c65465a working on stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-26 19:46:42 -08:00
Christoph M. Wintersteiger
0e74362ecb Added support for the final draft of the FPA standard (and fpa2bv conversion). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-01-24 15:36:23 +00:00
Christoph M. Wintersteiger
b2be81fd4d bugfix for OSX build configuration 2014-01-22 13:41:48 +00:00
Nikolaj Bjorner
f68eff3276 move network flow code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-21 09:06:30 -08:00
Christoph M. Wintersteiger
73a1dddc45 Bugfixes for the build on new OSX machines (XCode 5.0 on). 2014-01-21 17:06:13 +00:00
Nikolaj Bjorner
f6fd426c28 moved network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-21 08:46:02 -08:00
Nikolaj Bjorner
26a3d2ca31 add stand-alone simplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-21 08:40:28 -08:00
Nikolaj Bjorner
c6a9dae00a use external stack instead to manage memory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-15 20:26:48 -08:00
Nikolaj Bjorner
ff54b3d92b fix memory leak for scoped_numeral over trail objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-15 17:00:07 -08:00
Nikolaj Bjorner
39dcc653df fix normalization regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 20:20:26 -08:00
Nikolaj Bjorner
d548c51a98 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-13 13:42:15 -08:00
Nikolaj Bjorner
b80302cfb0 generalize guard in conflict resolution to handle non-equality binary predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 13:41:47 -08:00
Nikolaj Bjorner
236b2d2ff3 working on incremtal PB theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 10:12:45 -08:00
Nikolaj Bjorner
da4793de76 fix type checking bug reported by Nate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-09 21:14:30 -08:00
Ken McMillan
f380e31a6b runs the integer/cntrol svcomp examples from the Horn repo 2014-01-09 17:16:10 -08:00
Nikolaj Bjorner
1f7c994e43 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-01-06 16:23:50 -08:00
Nikolaj Bjorner
5adb4a22d1 enable partial results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-06 16:23:37 -08:00
Nikolaj Bjorner
f1710e5618 check parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-06 16:06:47 -08:00
Nikolaj Bjorner
23e811d136 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-05 20:44:56 -08:00
Nikolaj Bjorner
084a6f35eb fix bug reported by Nuno Lopes: inlining is unsound for negated predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 17:37:35 -08:00
Nikolaj Bjorner
3fa0e6f3fb testing decomposition during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 16:05:26 -08:00
Nikolaj Bjorner
8d0d123a4c pareto take 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 01:45:34 -08:00
Nikolaj Bjorner
a307bd67e0 pareto take 3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 01:35:31 -08:00
Nikolaj Bjorner
8883234647 pareto2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-01 22:32:27 -08:00
Nikolaj Bjorner
af27efbf4a pareto0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-01 21:13:25 -08:00
Nikolaj Bjorner
c5b82796ca moving parameters to theory_pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-01 20:00:10 -08:00
Nikolaj Bjorner
81f1f7690d fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-31 15:59:56 -08:00
Nikolaj Bjorner
4027de42f6 add optimized sorting network 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-30 13:06:58 -08:00
Nikolaj Bjorner
5965515385 bugfix to rational and working on adaptive sorting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 20:27:37 -08:00
Nikolaj Bjorner
a554ebb835 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-12-27 17:45:24 -08:00
Nikolaj Bjorner
eb4def108f reinit logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 17:45:14 -08:00
Nikolaj Bjorner
4cd2731b20 working on sn 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 15:08:27 -08:00
Nikolaj Bjorner
8f1a235f00 add app.config 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 14:50:04 -08:00
Anh-Dung Phan
e223e386fe Add binding redirects 2013-12-27 14:38:57 -08:00
Anh-Dung Phan
8accc49386 Add a README for MSF plugin 2013-12-27 11:39:50 -08:00
Anh-Dung Phan
0fabd40e49 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2013-12-27 11:18:25 -08:00
Anh-Dung Phan
5cc4cc8226 Add MSF plugins 2013-12-27 11:18:10 -08:00
Nikolaj Bjorner
32762b54a7 debug looping behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-27 07:50:25 -08:00
Nikolaj Bjorner
58f8181a74 fixes to dotnet interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 17:14:29 -08:00
Nikolaj Bjorner
a0e98ca39b working on pb pre-processing/subsumption 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 10:14:05 -08:00
Nikolaj Bjorner
0641c4f694 working on pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 09:53:33 -08:00
Ken McMillan
11ba2178a9 speeding up interpolation in RPFP_caching 2013-12-24 17:20:12 -08:00
Nikolaj Bjorner
70c4432bb4 working on pb pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 13:22:21 -08:00
Ken McMillan
1b9f1ea6b3 remove assert on failed label compuation in duality 2013-12-23 11:47:24 -08:00
Ken McMillan
673ba137e5 added qe_lite preprocessing pass to duality 2013-12-23 11:17:38 -08:00
Nikolaj Bjorner
0c2ec6951a working on pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 03:25:22 -08:00
Nikolaj Bjorner
24f2fd380c adding pre-processing of BP constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-23 01:33:24 -08:00
Ken McMillan
9e88691c69 optimizing solver performance in duality 2013-12-22 18:33:40 -08:00
Ken McMillan
c98b853917 speeding up Generalize and adding Lazy Propagation 2013-12-21 16:54:35 -08:00