- Joined
- Jun 27, 2006
- Messages
- 23,048
- Thread Author
- #1
Bart De Smet is one of the highly talented software engineers on Erik Meijer's team and the chief architect of the LINQ to Anything dream. You should watch his Link Removed on this topic.As you learned on Channel 9 Live's PDC10 conversation with Link Removed, Link Removed (the fastest in the world, in fact). Z3 is one of several advanced software engineering technologies coming out of Link Removed.
A while ago, Link Removed library and I've 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 Link Removed.
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:
var theorem = from t in ctx.NewTheorem() where t.X1 - t.X2 >= 1 where t.X1 - t.X2
A while ago, Link Removed library and I've 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 Link Removed.
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.
var theorem = from t in ctx.NewTheorem() where t.X1 - t.X2 >= 1 where t.X1 - t.X2
