mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
1852 commits 23 branches 48 tags 157 MiB
Commit graph

1852 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger d1376343c7 Compilation fix. 
gcc 4.3.2 (on debian 5) did not like the definitions of gcd and abs in class rational, so I moved them outside of the class.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-03-22 16:42:11 +00:00
Ken McMillan fb2caf99e6 duality fix 2014-03-21 10:35:33 -07:00
Christoph M. Wintersteiger 83f88917a8 bugfix for python 2.6 2014-03-20 17:47:41 +00:00
Nikolaj Bjorner 3e0e9c7f3c parse also bit-vector constants with set-info. Reported by David Cok 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 20:30:58 -07:00
Nikolaj Bjorner a9e8045071 fix bug reported by Nuno Lopes when query gets sliced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 20:23:54 -07:00
Nikolaj Bjorner a8fb15ce2c patch bounds normalization bug found by dvitek 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-19 18:02:05 -07:00
Ken McMillan 3e91037a4d duality fixes 2014-03-19 12:37:05 -07:00
Ken McMillan 2417b75d8d duality: added restarts 2014-03-16 15:37:19 -07:00
Ken McMillan 663d110b72 interpolation fix 2014-03-16 12:09:53 -07:00
Ken McMillan 675820ff67 merged changes from linux 2014-03-14 14:51:39 -07:00
Ken McMillan bbab6be280 duality: eager deduction and history-based conjectures 2014-03-14 13:40:31 -07:00
Ken McMillan 180f55bbda adding support for non-extensional arrays in duality 2014-03-11 18:20:42 -07:00
Nikolaj Bjorner 4732e03259 filter fresh constants from models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-07 08:59:27 -08:00
Ken McMillan 83a774ac79 duality fix plus mbqi option 2014-03-04 18:38:08 -08:00
Nikolaj Bjorner 601cb43f78 fix quotation bug reported by Arie Gurfinkel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-04 17:18:49 -08:00
Nikolaj Bjorner b1b349f496 modify offset check to accept linear expressions over numerals. Codeplex issue 81 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:50:29 -08:00
Nikolaj Bjorner 23313e5bdc remove unsound simplification for rem. Codeplex Issue 76 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:24:40 -08:00
Nikolaj Bjorner 4f20216677 fix documnetation to say milli-seconds. Issue 84 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:14:26 -08:00
Nikolaj Bjorner a00a9fbdfd generate error on duplicated data-type accessors. Issue 85 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-02 17:10:48 -08:00
Nikolaj Bjorner e27b7e3038 use size_t for return values from strlen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:09:57 -08:00
Nikolaj Bjorner f2ecd70e65 fix ctx solver simplify, remove horn inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:02:18 -08:00
Ken McMillan 19dbd02e13 interpolation fix 2014-02-28 10:38:35 -08:00
Ken McMillan acf4ad0ab6 use new hashtable implementation in windows 2014-02-27 17:23:19 -08:00
Ken McMillan 08d892bbdb interpolation fixes 2014-02-27 17:21:47 -08:00
Nikolaj Bjorner 891d0d07f8 removig unsound simplification in ctx-solver-simplify tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-27 13:42:40 -08:00
Ken McMillan 4f06b347b3 new hastable implementation for interp/duality 2014-02-25 18:21:06 -08:00
Ken McMillan ee9907a700 two interpolation fixes 2014-02-25 18:19:50 -08:00
Christoph M. Wintersteiger 4c8bbad8d6 FPA probe bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-25 18:16:28 +00:00
Christoph M. Wintersteiger b968eb2b8c FPA probe bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-25 18:13:16 +00:00
Ken McMillan 7fc011dbb8 interpolation fixes 2014-02-24 11:59:02 -08:00
Christoph M. Wintersteiger efd0cdc740 bugfix for FPA 2014-02-24 14:01:51 +00:00
Christoph M. Wintersteiger 4a9f12dd34 bugfix for FPA 2014-02-24 13:57:15 +00:00
Christoph M. Wintersteiger 07d56bdc70 Java API bugfixes for cygwin compilation 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-21 13:44:39 +00:00
Christoph M. Wintersteiger d51d9b18f9 Bugfixes for compilation in Cygwin (WIN32 -> _WINDOWS) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-21 13:00:02 +00:00
Leonardo de Moura e077fc5cb4 fix(api/python): make sure Z3 compiles using Python3 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-20 14:09:55 -08:00
Ken McMillan 75bb495585 merging interpolation and duality changes into unstable 2014-02-19 15:36:16 -08:00
Ken McMillan 65c54b87d0 duality fix 2014-02-19 13:57:27 -08:00
Ken McMillan c9cf658e7c interpolation fix for commutativity 2014-02-19 13:56:55 -08:00
Ken McMillan 76fb66314b interpolation fix for commutativity 2014-02-19 13:56:16 -08:00
Ken McMillan 928d419138 duality fixes 2014-02-17 12:15:11 -08:00
Ken McMillan cb3dc63e68 some interpolation fixes; make duality a bit more persistent in checking interpolant 2014-02-14 15:52:07 -08:00
Ken McMillan 88ff20a0fb fixed multiple interpolation bugs 2014-02-14 15:48:38 -08:00
Christoph M. Wintersteiger e860c65567 bugfix for sign computation in floating-point FMA 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-02-13 19:33:51 +00:00
Ken McMillan f45ad4bdc0 disable silly warnings and add needed header for VS 2014-02-10 12:56:39 -08:00
Ken McMillan ba193a59b1 some interpolation fixes, plus some options to remove features for testing in duality 2014-02-09 16:04:02 -08:00
Ken McMillan 19830bcd33 fix a few warnings 2014-01-28 11:43:00 -08:00
Ken McMillan 466c35100d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-28 11:28:24 -08:00
Christoph M. Wintersteiger f111dd4e61 Fixes for the build on OS X 10.9 2014-01-28 14:00:42 +00: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