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

1635 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan
b3bd9db4a5 merge duality debug code 2014-05-09 13:18:28 -07:00
Ken McMillan
ddd3867beb merged interp hack 2014-05-09 13:12:10 -07:00
Ken McMillan
90ca1b95c0 debugging code in duality 2014-05-09 13:10:03 -07:00
Ken McMillan
2a887a7608 interp localization hack 2014-05-09 13:08:39 -07:00
Ken McMillan
a4f3afd70d added fixedpoint.conjecture_file option 2014-05-05 14:29:54 -07:00
Ken McMillan
f4790a183d strarting on conjecture printing in duality 2014-04-24 16:18:20 -07:00
Ken McMillan
2755854c81 trying alternate encoding of distint 2014-04-22 16:42:35 -07:00
Ken McMillan
77f8aa9f6b fix for quantifiers in interpolants 2014-04-22 13:28:11 -07:00
Ken McMillan
60ef669fbc removed distinct predicate hack 2014-04-10 17:54:49 -07:00
Ken McMillan
de81db9a3b fixed several interpolation problems 2014-04-10 17:53:17 -07:00
Ken McMillan
f7d589fc49 changed fixedpoint output format for easier parsing in Boogie 2014-04-10 17:53:00 -07:00
Ken McMillan
58ffffe4d4 hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death 2014-04-06 13:01:20 -07:00
Ken McMillan
2b492f04f6 merging duality and interpolation changes 2014-04-04 15:50:59 -07:00
Ken McMillan
bdc7bfde87 duality quantifier simplification fix 2014-04-04 13:10:18 -07:00
Christoph M. Wintersteiger
dee21c6656 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-04-04 17:57:57 +01:00
Christoph M. Wintersteiger
9c052f589d C API bugfix (Stackoverflow #22864146) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-04 17:57:50 +01:00
Ken McMillan
43644fc2cb g++ pedantry 2014-04-04 01:28:09 +01:00
Ken McMillan
588aeff5c3 merged interpolation and duality changes 2014-04-03 17:11:15 -07:00
Ken McMillan
fc62be37b6 getting rid of DOS line endings 2014-04-03 17:09:11 -07:00
Ken McMillan
9a2fe83697 interpolation fix 2014-04-03 13:20:08 -07:00
Christoph M. Wintersteiger
4444eb361c bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-03 13:11:39 +01:00
Christoph M. Wintersteiger
944dfee008 .NET and Java API Bugfix (Codeplex issue 101) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 19:25:05 +01:00
Christoph M. Wintersteiger
7bb1469d71 removed debugging code. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 19:10:30 +01:00
Christoph M. Wintersteiger
a833c9ac41 Fixed bug (codeplex issue 102) 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-02 17:56:55 +01:00
Ken McMillan
4671c1be41 duality fix 2014-04-01 17:50:48 -07:00
Ken McMillan
278d619521 set text default to auto to try to avoid crlf disasters 2014-04-01 17:20:37 -07:00
Ken McMillan
6c9483c70a interpolation fix and improving duality quantifier handling 2014-04-01 17:10:14 -07:00
Nikolaj Bjorner
6f7c9607ea Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-03-28 08:52:04 -07:00
Nikolaj Bjorner
4c95bb4dd9 add 'distinct' to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-28 08:51:50 -07:00
Ken McMillan
732035bf63 merge interp/duality changes with unstable 2014-03-26 14:48:04 -07:00
Ken McMillan
fcada914d5 duality fix 2014-03-26 14:10:21 -07:00
Ken McMillan
c9fcf7ee96 interpolation fix (add simplify_cong) 2014-03-24 17:21:29 -07:00
Ken McMillan
e3c1cdfe8c interpolation fix 2014-03-24 11:33:09 -07:00
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