3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Commit graph

279 commits

Author SHA1 Message Date
Nikolaj Bjorner
9c4409a8fe set timout to max
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-05-09 11:48:28 -07:00
Christoph M. Wintersteiger
c3b7c738f8 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt
Conflicts:
	scripts/mk_project.py
	src/duality/duality.h
	src/duality/duality_solver.cpp
	src/duality/duality_wrapper.h
	src/interp/iz3hash.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-25 22:18:41 +01:00
Christoph M. Wintersteiger
fceaf97c95 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2014-04-25 22:11:34 +01:00
Nikolaj Bjorner
4d2d334999 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-04-23 14:44:03 +02:00
Nikolaj Bjorner
7d16ed9fdc fix exception class in python API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-23 14:13:01 +02:00
Nikolaj Bjorner
55863b4bb5 fix build problems, fix scoping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-23 14:05:59 +02:00
Nikolaj Bjorner
23a74b3c26 fix assertions reported by Christoph
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-23 08:07:37 +02:00
Nikolaj Bjorner
d118f07e37 fix maximize name in C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-22 14:48:05 +02:00
Andreas Froehlich
5ab65d52a6 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls
Conflicts:
	src/tactic/sls/sls_engine.cpp
	src/tactic/sls/sls_engine.h
	src/tactic/sls/sls_evaluator.h
	src/tactic/sls/sls_tracker.h
2014-04-21 17:05:19 +01:00
Nikolaj Bjorner
e3b346df6f working on bcd2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-18 08:04:18 -07:00
Christoph M. Wintersteiger
64bfbb657c .NET API documentation XML build fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-09 11:39:05 +01:00
Christoph M. Wintersteiger
a3b89a8af3 .NET API documentation fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-09 11:24:42 +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
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
a833c9ac41 Fixed bug (codeplex issue 102)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-02 17:56:55 +01:00
Nikolaj Bjorner
1db7e0a149 fix compiler warnings reported by Robert White
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-04-02 15:54:28 +02:00
Nikolaj Bjorner
cc577a431a C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-28 09:39:14 -07:00
Nikolaj Bjorner
13e454ad63 adding C++ API for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-28 09:29:21 -07:00
Nikolaj Bjorner
776f1dc631 Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt 2014-03-28 08:52:37 -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
Christoph M. Wintersteiger
3ab1766588 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into opt 2014-03-27 13:13:10 +00:00
Ken McMillan
732035bf63 merge interp/duality changes with unstable 2014-03-26 14:48:04 -07:00
Nikolaj Bjorner
330120e406 update documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-03-24 03:37:02 -07:00
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
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
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