mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
4992 commits 49 branches 53 tags 182 MiB
Commit graph

4992 commits

This branch
This branch
All branches
Author SHA1 Message Date
Andreas Froehlich
ad8cac7d88 uct forget and minisat restarts added 2015-01-12 17:19:13 +00:00
Christoph M. Wintersteiger
13307a1d51 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:19:12 +00:00
Christoph M. Wintersteiger
7451e5cae0 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:19:11 +00:00
Andreas Froehlich
442827e523 Current version for relocating. 2015-01-12 17:18:52 +00:00
Christoph M. Wintersteiger
664fa82c6c removed tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:18:51 +00:00
Andreas Froehlich
140d28b6b3 plenty of new stuff 2015-01-12 17:18:50 +00:00
Andreas Froehlich
dfe2d945e9 some extensions/modifications. versions added. 2015-01-12 17:18:36 +00:00
Andreas Froehlich
c982f87025 sls tactic default 2015-01-12 17:18:19 +00:00
Christoph M. Wintersteiger
6818e850e9 Disabled BV-SLS as default tactic in anticipation for integration 
with the unstable branch.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:34 +00:00
Christoph M. Wintersteiger
387f036f93 BV-SLS optimization 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:32 +00:00
Christoph M. Wintersteiger
aa0980b83b merge fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:31 +00:00
Christoph M. Wintersteiger
6b9c5dbfc0 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:13 +00:00
Christoph M. Wintersteiger
54cd1ea5e6 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:12 +00:00
Christoph M. Wintersteiger
60753bf46b compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:11 +00:00
Christoph M. Wintersteiger
fc0cdcfd29 compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:10 +00:00
Christoph M. Wintersteiger
a02c59c1bc removed unused file 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:09 +00:00
Christoph M. Wintersteiger
e34b5edf27 BVSLS comments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:15:09 +00:00
Andreas Froehlich
b3924d85ed Cleaned up final SLS version. Enjoy! 2015-01-12 17:15:08 +00:00
Andreas Froehlich
c4fb21cca1 Moved parameters to the right file. Almost clean. 2015-01-12 17:15:07 +00:00
Andreas Froehlich
b5a9e0a1f5 Backup before I touch early pruning ... 2015-01-12 17:15:06 +00:00
Andreas Froehlich
39ea6234a4 Fixed bug with VNS repick. 2015-01-12 17:15:04 +00:00
Andreas Froehlich
8a30a2caa9 Almost cleaned up version. 2015-01-12 17:15:04 +00:00
Andreas Froehlich
42702c8d8a Current version before integration ... 2015-01-12 17:14:46 +00:00
Christoph M. Wintersteiger
f88b034b8b bvsls bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:21 +00:00
Christoph M. Wintersteiger
239849957a bvsls refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:20 +00:00
Christoph M. Wintersteiger
c541694f40 bvsls refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:20 +00:00
Christoph M. Wintersteiger
4e8c0c1418 compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:19 +00:00
Christoph M. Wintersteiger
ff7af2680d compilation fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:17 +00:00
Christoph M. Wintersteiger
beef8198a4 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:16 +00:00
Christoph M. Wintersteiger
cf1a600fb9 bugfix 2015-01-12 17:14:15 +00:00
Christoph M. Wintersteiger
e9482a1447 disabled old code 2015-01-12 17:14:13 +00:00
Christoph M. Wintersteiger
dfd2566e25 removed dependency of bvsls on goal_refs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:14:13 +00:00
Andreas Froehlich
1e55b3bfb5 uct forget and minisat restarts added 2015-01-12 17:14:12 +00:00
Christoph M. Wintersteiger
a6227d5446 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:59 +00:00
Christoph M. Wintersteiger
b1eeb9adf4 SLS refactoring 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:59 +00:00
Andreas Froehlich
aa6f8a4b8a Current version for relocating. 2015-01-12 17:13:42 +00:00
Christoph M. Wintersteiger
e33e637ad8 removed tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:13:12 +00:00
Andreas Froehlich
e310ab5cd7 plenty of new stuff 2015-01-12 17:13:12 +00:00
Andreas Froehlich
b002697e03 some extensions/modifications. versions added. 2015-01-12 17:13:11 +00:00
Andreas Froehlich
40014d019c sls tactic default 2015-01-12 17:13:10 +00:00
Christoph M. Wintersteiger
66abc1c65e Removed unnecessary file 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 17:03:27 +00:00
Christoph M. Wintersteiger
d4ecc3c1be Disabled BV-SLS as default tactic in anticipation for integration 
with the unstable branch.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-12 15:59:20 +00:00
Christoph M. Wintersteiger
d39bd9d6b4 Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls 2015-01-12 15:12:28 +00:00
Christoph M. Wintersteiger
766d585922 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 
Resolved  a bunch of Java documentation conflicts

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/api/java/AST.java
	src/api/java/ASTMap.java
	src/api/java/ASTVector.java
	src/api/java/AlgebraicNum.java
	src/api/java/BoolExpr.java
	src/api/java/Context.java
	src/api/java/Expr.java
	src/api/java/Fixedpoint.java
	src/api/java/Global.java
	src/api/java/InterpolationContext.java
	src/api/java/Model.java
	src/api/java/Solver.java
 2015-01-11 18:39:17 +00:00
Christoph M. Wintersteiger
6c971b1301 Beginnings of a Python API for FPA 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-11 18:29:40 +00:00
Christoph M. Wintersteiger
e0bc704106 FPA API bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-11 18:29:12 +00:00
Christoph M. Wintersteiger
4bd8e0f497 FPA API cosmetics 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-11 18:28:07 +00:00
Christoph M. Wintersteiger
ee0ec7fe3a FPA API: numerals, .NET and Java 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-10 17:28:07 +00:00
Nikolaj Bjorner
bd879c1016 improve logging diagnostics and tracing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-09 15:43:16 -08:00
Christoph M. Wintersteiger
3391c9c44c typo fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-09 11:53:24 +00:00