mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
2016 commits 23 branches 48 tags 157 MiB
Commit graph

2016 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
9a53fe43e6 Removed unnecessary #includes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 15:31:12 +00:00
Christoph M. Wintersteiger
ae792f1891 avoid spurious warning message 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:47:32 +00:00
Christoph M. Wintersteiger
a603f76b6c BV-SLS build fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:47:17 +00:00
Christoph M. Wintersteiger
e20dc9f9a4 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:35:25 +00:00
Christoph M. Wintersteiger
71e5f03b44 build fix 2015-01-21 13:04:05 +00:00
Christoph M. Wintersteiger
83023c7211 build fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 13:02:18 +00:00
Christoph M. Wintersteiger
237577acc8 Bumping version to 4.4 
Added to release notes

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:59:54 +00:00
Christoph M. Wintersteiger
0746ede537 BV SLS: Final adjustments 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:59:25 +00:00
Christoph M. Wintersteiger
074ff311c0 BV-SLS final integration. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:19:31 +00:00
Christoph M. Wintersteiger
61ba7f5e09 Merge branch 'bvsls' of https://git01.codeplex.com/z3 into unstable 
Conflicts:
	src/tactic/portfolio/default_tactic.cpp

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-20 15:15:31 +00:00
Christoph M. Wintersteiger
d20c7bc9ee Added is_qfaufbv_probe and is_qfauflia_probe. 
Potential performance disruption for some users:
Changed default_tactic to call the respective tactics,
where previously they would have run the default 'smt'
tactic.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:19:43 +00:00
Christoph M. Wintersteiger
a8d8e3e9e5 formatting 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-19 18:16:51 +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
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
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
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
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
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