mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity
16836 commits 29 branches 50 tags 166 MiB
Commit graph

2340 commits

Author SHA1 Message Date
Nikolaj Bjorner
b71580f11c fix APIs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-24 03:11:53 -07:00
Nikolaj Bjorner
ff1543d700 fix APIs, add python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-23 21:28:11 -07:00
Nikolaj Bjorner
1c7d523838 separate out parameter references for API call to fix build problem 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-21 14:23:02 -07:00
Nikolaj Bjorner
88df909a6c merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-20 14:09:18 -07:00
Ken McMillan
acf4ad0ab6 use new hashtable implementation in windows 2014-02-27 17:23:19 -08:00
Christoph M. Wintersteiger
d1d038da35 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2014-02-27 18:06:13 +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
Nikolaj Bjorner
c42ee3bb01 Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt 2014-02-11 15:44:12 -08:00
Christoph M. Wintersteiger
f111dd4e61 Fixes for the build on OS X 10.9 2014-01-28 14:00:42 +00: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
58f8181a74 fixes to dotnet interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-26 17:14:29 -08: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
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
Anh-Dung Phan
caba15d6b3 Remove superfluouse indices to make .NET API thinner 2013-12-10 17:15:51 -08:00
Nikolaj Bjorner
4d6aa1a0f3 add to_string and get_help methods to optimize API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-06 11:34:41 -08:00
Anh-Dung Phan
d38e2b9b78 Expose objective indices to .NET API 2013-12-05 17:30:40 -08:00
Christoph M. Wintersteiger
a533527004 exception message clarity fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-05 12:45:14 +00:00
Nikolaj Bjorner
56c4fa8f6d expose models, working on network flow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-04 17:39:54 -08:00
Christoph M. Wintersteiger
16ebceb9ff Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Conflicts:
	scripts/mk_project.py

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-04 13:50:42 +00:00
Nikolaj Bjorner
e3fe80fd4d add .NET interface and finish C interface for optimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 20:20:24 -08:00
Nikolaj Bjorner
4719aa11bb backfilling API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 17:00:34 -08:00
Nikolaj Bjorner
222d4a8f01 add sketch of C-based API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-03 14:47:59 -08:00
Nikolaj Bjorner
97dfb6d521 moving to rational coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-21 15:55:08 -08:00
Nikolaj Bjorner
61385c8489 a.ctx -> self.ctx, thanks gario 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-20 09:54:37 -08:00
Nikolaj Bjorner
33895d522b fix and enable learning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-19 20:47:16 -08:00
Nikolaj Bjorner
ee0abfbfe9 rename card->pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 21:25:02 -08:00
Nikolaj Bjorner
2b2d0e155c debugged new pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-18 18:03:49 -08:00
Nikolaj Bjorner
34af198816 missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-14 08:51:01 -08:00
Nikolaj Bjorner
2d3f6ca71d add pb constraints to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-13 17:15:41 -08:00
Nikolaj Bjorner
d1937b2032 add PB operators to C-based API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-13 17:09:10 -08:00
Ken McMillan
a785a5a4b8 Merge branch 'unstable' into interp 2013-11-05 12:28:13 -08:00
Ken McMillan
81df4932fb added quantifiers in new interpolation 2013-10-25 18:40:26 -07:00
Ken McMillan
3a0947b3ba merged with unstable 2013-10-18 17:26:41 -07:00
Christoph M. Wintersteiger
5e6a47e2d3 Example fixed (substitute does not include a rewriter call anymore). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-09-26 11:35:08 +01:00
Nikolaj Bjorner
4363c9f44f use safe replace for external substitution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-24 18:47:19 +03:00
Nikolaj Bjorner
c1384095f3 fix default argument identification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-23 21:44:24 +03:00
Nikolaj Bjorner
fd1f4b9191 fix bugs reported by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-23 04:07:08 +03:00
Nikolaj Bjorner
457b22b00e add TPTP example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-06 21:49:00 -07:00
Nikolaj Bjorner
0d56499e2d re-organize muz_qe into separate units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-28 21:20:24 -07:00
Nikolaj Bjorner
5c145dcd4b fix parameter checking on quantifiers (thanks to Esteban Pavese), fix query tracking in rel_context (thanks to Nuno Lopes), fix counter for free variables under quantfiers (thanks to Tomer Weiss) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-22 15:00:52 -07:00
Nikolaj Bjorner
7bbabcdf6d updated documentation for finite domain sizes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-16 14:47:48 -07:00
Nikolaj Bjorner
0fd94a033f change non-null test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-12 09:52:10 -07:00
Nikolaj Bjorner
3b64265c27 remove duplicated definition of is_store and is_select 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-09 09:15:04 -07:00
Christoph M. Wintersteiger
092dfa396a Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-08-07 15:22:06 +01:00
Nikolaj Bjorner
f1d3a13b7f add missing case handlers for internal bit-vector operators that leak during simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-16 11:46:29 +04:00
Nikolaj Bjorner
9a49f5f204 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-07-10 17:21:16 +03:00
Nikolaj Bjorner
784455d1fc detect approximate relations to return unknown, fix product relations, fix symbolic magic set transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-07-10 17:20:44 +03:00
Leonardo de Moura
ccb36f1ae7 Fix issue https://z3.codeplex.com/workitem/54 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-09 08:22:17 -07:00
Christoph M. Wintersteiger
b9aa721365 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-26 18:17:46 +01:00