mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
2549 commits 49 branches 53 tags 182 MiB
Commit graph

2549 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Christoph M. Wintersteiger
3391c9c44c typo fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-09 11:53:24 +00:00
Christoph M. Wintersteiger
46e236487b Eliminated FPRMNum classes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-09 11:53:18 +00:00
Christoph M. Wintersteiger
71912830f1 Formatting, mostly tabs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:54:44 +00:00
Christoph M. Wintersteiger
0381e4317a Formatting, mostly tabs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:54:04 +00:00
Christoph M. Wintersteiger
cad841cff4 to_fp_real marked as NIY for now 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:23:13 +00:00
Christoph M. Wintersteiger
7fe9ad5cb4 Java FPA API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:22:02 +00:00
Christoph M. Wintersteiger
ee2c9095c6 .NET FPA API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:21:29 +00:00
Christoph M. Wintersteiger
bcbce8f190 FPA Java and .NET API updates 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 16:31:09 +00:00
Christoph M. Wintersteiger
33dc6340e1 More renaming mk_value -> mk_numeral 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:23:13 +00:00
Christoph M. Wintersteiger
c0bc2518b0 Renaming for consistency mk_value -> mk_numeral 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:22:44 +00:00
Christoph M. Wintersteiger
c5b220cc12 FPA: Added AST kind descriptions 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:07:59 +00:00
Christoph M. Wintersteiger
c0a027fc80 FPA: Elminated nzero/pzero AST kinds 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:07:47 +00:00
Christoph M. Wintersteiger
0cedd32ea2 More renaming floats -> fpa 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 13:47:26 +00:00