EDN Admin
Well-known member
http://channel9.msdn.com/Tags/bart+de+smet Bart De Smet is one of the highly talented software engineers on http://channel9.msdn.com/tags/erik+meijer Erik Meijer s team and the chief architect of the LINQ to Anything dream. You should watch his http://videoaz.microsoftpdc.com/vod/pdc10_pre_event/ShowContent_VOD/FT10_BartDeSmet_PDC_WMV_High_1280x720_2500k.wmv excellent PDC10 session on this topic.As you learned on Channel 9 Lives PDC10 conversation with http://videoaz.microsoftpdc.com/vod/pdc10_pre_event/ShowContent_VOD/Channel9/CH9_Day2_EngResearch_p1_PDC_WMV_High_480p_1500k.wmv Wolfram Schulte and Erik Meijer , http://research.microsoft.com/en-us/um/redmond/projects/z3/ Z3 is a theorem prover (the fastest in the world, in fact). Z3 is one of several advanced software engineering technologies coming out of http://research.microsoft.com/rise MSRs RiSE team . A while ago, http://community.bartdesmet.net/blogs/bart/archive/2009/04/19/linq-to-z3-theorem-solving-on-steroids-part-0.aspx Bart implemented a LINQ to Z3 library and Ive wanted to dig into this with him for some time. Recently, I got the chance to do just that and it makes for an excellent episode of http://channel9.msdn.com/shows/going+deep Going Deep .
Bart writes in his initial post on the LINQ to Z3 project: With LINQ to Z3 my goal is to abstract away from the low-level Z3 APIs and provide nice syntax with rich static typing support on top of it. The basic idea is the following: Define the “shape” of a theorem, e.g. what symbolic names (and their types) to use;Express constraints over those symbolic names using LINQ syntax (more specifically the where keyword);Ask the resulting object for a solution, resulting in an instance of the “shape” type specified at the start. An example of LINQ to Z3: <pre class="brush: text var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}", solution.X1, solution.X2, solution.X3, solution.X4, solution.X5);[/code] How does LINQ to Z3 work, exactly? Why did Bart do this? What is Z3 useful for? How does it work? Here, we get answers to all of these questions with lots of meaty whiteboarding and demo at the end of the conversation. As usual, there is a lot of information presented here and in a way that is readily understandable by non-experts - this is one of Barts excellent traits: clearly explaining complex subjects so you dont have to be as smart as Bart to fully understand. I left Barts office with better understanding of LINQ, Z3 and LINQ to Z3 (also Solver Foundation and Barts definition of monad....). Thank you, Bart! By the way, this is espisode 201 of Going Deep. http://channel9.msdn.com/Shows/Going+Deep/Erik-Meijer-and-Bart-De-Smet-LINQ-to-Anything Bart and LINQ were the focus for the 100th episode . Its nice to have this 100 episode cycle (LINQ to Anything is LINQ to Everything in this revolution). Thanks to all who have made this series truly interesting! Heres to 200 more.
Tune in. Learn. Enjoy. Code. <img src="http://m.webtrends.com/dcs1wotjh10000w0irc493s0e_6x1g/njs.gif?dcssip=channel9.msdn.com&dcsuri=http://channel9.msdn.com/Feeds/RSS&WT.dl=0&WT.entryid=Entry:RSSView:5b5621190a814f61b1829e300187a260
View the full article
Bart writes in his initial post on the LINQ to Z3 project: With LINQ to Z3 my goal is to abstract away from the low-level Z3 APIs and provide nice syntax with rich static typing support on top of it. The basic idea is the following: Define the “shape” of a theorem, e.g. what symbolic names (and their types) to use;Express constraints over those symbolic names using LINQ syntax (more specifically the where keyword);Ask the resulting object for a solution, resulting in an instance of the “shape” type specified at the start. An example of LINQ to Z3: <pre class="brush: text var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}", solution.X1, solution.X2, solution.X3, solution.X4, solution.X5);[/code] How does LINQ to Z3 work, exactly? Why did Bart do this? What is Z3 useful for? How does it work? Here, we get answers to all of these questions with lots of meaty whiteboarding and demo at the end of the conversation. As usual, there is a lot of information presented here and in a way that is readily understandable by non-experts - this is one of Barts excellent traits: clearly explaining complex subjects so you dont have to be as smart as Bart to fully understand. I left Barts office with better understanding of LINQ, Z3 and LINQ to Z3 (also Solver Foundation and Barts definition of monad....). Thank you, Bart! By the way, this is espisode 201 of Going Deep. http://channel9.msdn.com/Shows/Going+Deep/Erik-Meijer-and-Bart-De-Smet-LINQ-to-Anything Bart and LINQ were the focus for the 100th episode . Its nice to have this 100 episode cycle (LINQ to Anything is LINQ to Everything in this revolution). Thanks to all who have made this series truly interesting! Heres to 200 more.
Tune in. Learn. Enjoy. Code. <img src="http://m.webtrends.com/dcs1wotjh10000w0irc493s0e_6x1g/njs.gif?dcssip=channel9.msdn.com&dcsuri=http://channel9.msdn.com/Feeds/RSS&WT.dl=0&WT.entryid=Entry:RSSView:5b5621190a814f61b1829e300187a260
View the full article