Christoph M. Wintersteiger
|
a965d65901
|
ML API temp files added to .gitignore
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:41:17 +00:00 |
|
Christoph M. Wintersteiger
|
d5f135c432
|
More new ML API.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:40:52 +00:00 |
|
Christoph M. Wintersteiger
|
8d30fabc0a
|
New native ML API layer.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:40:40 +00:00 |
|
Christoph M. Wintersteiger
|
65ddf2be49
|
More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:40:39 +00:00 |
|
Christoph M. Wintersteiger
|
f5a0520b83
|
More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:40:37 +00:00 |
|
Christoph M. Wintersteiger
|
03a5c88ded
|
More new ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:40:10 +00:00 |
|
Christoph M. Wintersteiger
|
70f0d2f423
|
Beginnings of a new ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:38:52 +00:00 |
|
Christoph M. Wintersteiger
|
5619f6b583
|
FPA Python API bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-19 15:18:12 +00:00 |
|
Nikolaj Bjorner
|
9790784488
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2015-01-18 04:50:20 +05:30 |
|
Nikolaj Bjorner
|
6af9782927
|
set default file format to smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-01-18 04:50:00 +05:30 |
|
Christoph M. Wintersteiger
|
c3247d7598
|
FPA: bugfix for rounding mode bv translation
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-17 16:36:33 +00:00 |
|
Christoph M. Wintersteiger
|
67e04c5dfb
|
Python example: removed function that has no body.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-16 17:40:28 +00:00 |
|
Christoph M. Wintersteiger
|
2b03ec63f6
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2015-01-16 17:35:12 +00:00 |
|
Christoph M. Wintersteiger
|
bb722b24c1
|
Added call to memory::finalize() to ease memory leak debugging
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-16 17:34:01 +00:00 |
|
Christoph M. Wintersteiger
|
88aa349eb7
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2015-01-16 12:30:28 +00:00 |
|
Nikolaj Bjorner
|
b9bbfbdbb7
|
fix interval dependencies bug. Codeplex issue 163
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-01-16 12:05:12 +05:30 |
|
Christoph M. Wintersteiger
|
2f81b6c6b5
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2015-01-15 19:26:03 +00:00 |
|
Christoph M. Wintersteiger
|
5344d6f3c0
|
various bugfixes and extensions for FPA
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-15 19:25:49 +00:00 |
|
Christoph M. Wintersteiger
|
caafee0033
|
Added simplifier plugin for FP
|
2015-01-15 19:18:18 +00:00 |
|
Nikolaj Bjorner
|
ec384d3d31
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2015-01-15 17:23:37 +05:30 |
|
Nikolaj Bjorner
|
dbc9bebd18
|
fix instance test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-01-15 16:47:10 +05:30 |
|
Christoph M. Wintersteiger
|
0e37a1722f
|
BV-SLS Cosmetics
|
2015-01-12 17:44:56 +00:00 |
|
Christoph M. Wintersteiger
|
f1a00da401
|
BV-SLS Cosmetics
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:43:56 +00:00 |
|
Christoph M. Wintersteiger
|
58bf80f113
|
Cosmetics
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:22:13 +00:00 |
|
Christoph M. Wintersteiger
|
916ef815fa
|
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:19:45 +00:00 |
|
Christoph M. Wintersteiger
|
168c3eb363
|
BV-SLS optimization
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:44 +00:00 |
|
Christoph M. Wintersteiger
|
85ff954bc6
|
merge fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:43 +00:00 |
|
Christoph M. Wintersteiger
|
8745872d28
|
compilation fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:42 +00:00 |
|
Christoph M. Wintersteiger
|
0016ba5f3e
|
compilation fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:41 +00:00 |
|
Christoph M. Wintersteiger
|
7105e4d213
|
compilation fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:40 +00:00 |
|
Christoph M. Wintersteiger
|
7a7566f39e
|
compilation fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:39 +00:00 |
|
Christoph M. Wintersteiger
|
bec5938d9c
|
removed unused file
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:39 +00:00 |
|
Christoph M. Wintersteiger
|
992d150b81
|
BVSLS comments
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:38 +00:00 |
|
Andreas Froehlich
|
7d18a17bb3
|
Cleaned up final SLS version. Enjoy!
|
2015-01-12 17:19:37 +00:00 |
|
Andreas Froehlich
|
80c94ef0b6
|
Moved parameters to the right file. Almost clean.
|
2015-01-12 17:19:37 +00:00 |
|
Andreas Froehlich
|
ca1e3c3d9f
|
Backup before I touch early pruning ...
|
2015-01-12 17:19:25 +00:00 |
|
Andreas Froehlich
|
fb18547a5f
|
Fixed bug with VNS repick.
|
2015-01-12 17:19:24 +00:00 |
|
Andreas Froehlich
|
de028e7a30
|
Almost cleaned up version.
|
2015-01-12 17:19:24 +00:00 |
|
Andreas Froehlich
|
c56e55b230
|
Current version before integration ...
|
2015-01-12 17:19:23 +00:00 |
|
Christoph M. Wintersteiger
|
a48bb976e9
|
bvsls bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:22 +00:00 |
|
Christoph M. Wintersteiger
|
e382742a29
|
bvsls refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:22 +00:00 |
|
Christoph M. Wintersteiger
|
ad412d4f08
|
bvsls refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:20 +00:00 |
|
Christoph M. Wintersteiger
|
1b98e6002b
|
compilation fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:19 +00:00 |
|
Christoph M. Wintersteiger
|
b76ffddf49
|
compilation fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:18 +00:00 |
|
Christoph M. Wintersteiger
|
71fdb59747
|
removed dependency of bvsls on goal_refs
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:17 +00:00 |
|
Christoph M. Wintersteiger
|
e9797c3922
|
bugfix
|
2015-01-12 17:19:16 +00:00 |
|
Christoph M. Wintersteiger
|
1834bb5950
|
disabled old code
|
2015-01-12 17:19:15 +00:00 |
|
Christoph M. Wintersteiger
|
1f326d9e72
|
removed dependency of bvsls on goal_refs
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2015-01-12 17:19:14 +00:00 |
|
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 |
|