mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity
10366 commits 24 branches 48 tags 158 MiB
Commit graph

289 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
0e4e72b1bc Added new params.Add functions to the .NET and Java APIs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-14 13:22:12 +01:00
Nikolaj Bjorner
b050ac7c7c using properties 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-13 19:11:20 -07:00
Nikolaj Bjorner
bae201b37d Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-10-13 18:59:37 -07:00
Nikolaj Bjorner
e46114819b revamp API for acessing values of objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-13 18:59:13 -07:00
Nikolaj Bjorner
a0cdeb2cfe add useful API for parameter setting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-13 14:20:53 -07:00
Christoph M. Wintersteiger
3e7c95db6b Interpolation API bugfixes 
Added Interpolation to the Java API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 12:34:17 +01:00
Christoph M. Wintersteiger
9b8406c717 Resolved interpolation API issues. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-10 11:41:21 +01:00
Christoph M. Wintersteiger
1c1351a064 Interpolation .NET API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-09 18:11:42 +01:00
Christoph M. Wintersteiger
503ad78bf3 Interpolation API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-09 18:08:07 +01:00
Christoph M. Wintersteiger
b03a9d3f0a Interpolation API: infrastructure fixes and .NET API 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-08 21:01:27 +01:00
Nikolaj Bjorner
a3a008bdde update Deprecated API to avoid memory leak and crash when there is a core, ensure invariant in new code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 19:54:04 -07:00
Nikolaj Bjorner
f3d2535b46 another unit test for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-03 16:58:46 -07:00
Nikolaj Bjorner
2bf0b5f33f include selected deprecated facilities for easier experimentation with consequence finding over .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-03 13:05:54 -07:00
Nikolaj Bjorner
08dcd51594 fix bugs in incremental operation of sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-27 12:04:54 -07:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Nikolaj Bjorner
31f16d7aa4 add push/pop to optimization context for convenience 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-01 14:58:58 -07:00
Christoph M. Wintersteiger
0cf1f9c210 .NET API context refcounting; changed int to long to be on the safe side on 64-bit platforms. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-08-14 12:15:58 +01:00
mattpark
5a45711f22 Dealt with some concurrency issues due to concurrent GC. 2014-08-12 10:16:00 +01:00
Nikolaj Bjorner
47ac5c0633 fix doc bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-09 11:41:04 +09:00
Ken McMillan
c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Christoph M. Wintersteiger
c508b66cf7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Conflicts:
	src/ast/float_decl_plugin.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-07-31 17:37:43 +01:00
Nikolaj Bjorner
19050d1c4c merge Fixedpoint.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 12:20:48 -07:00
Nikolaj Bjorner
44751c0ef8 Add missing .NET API functions for parsing rules into fixedpoint object 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-23 15:27:24 -07:00
Christoph M. Wintersteiger
129e2f5e23 FPA API fixes and examples 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-11 17:55:31 +01: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
Christoph M. Wintersteiger
0279a1042d FPA API documentation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-23 18:39:36 +01:00
Christoph M. Wintersteiger
3e5a702073 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2014-04-23 14:50:51 +01: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
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
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
776f1dc631 Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt 2014-03-28 08:52:37 -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
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
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
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
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
2d3f6ca71d add pb constraints to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-13 17:15:41 -08:00
Ken McMillan
3a0947b3ba merged with unstable 2013-10-18 17:26:41 -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
Christoph M. Wintersteiger
b9aa721365 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-26 18:17:46 +01:00