Repository files navigation

.NET 8.0 LINQ bindings for theZ3 theorem prover fromMicrosoft Research.

Based on the proof of concept byBart De Smet which was curated intoZ3.LinqBinding byRicardo Niepel.

A number of examples are included in this solution, which you can runfrom .NET Interactive (requiresVisual Studio Code) orfrom Visual Studio.

Provide a solution where either X is true or Y is true, but not both (using aValueTuple).

using(varctx=newZ3Context()){vartheorem=fromtinctx.NewTheorem<(boolx,booly)>()wheret.x^t.yselectt;varresult=theorem.Solve();Console.WriteLine(result);}

Solve the following system with 3 variables, with linear equalities and inequalities:

$$x_1 - x_2 \ge 1\\x_1 - x_2 \le 3\\x_1 = 2x_3 + x_2$$

using(varctx=newZ3Context()){vartheorem=fromtinctx.NewTheorem<Symbols<int,int,int>>()wheret.X1-t.X2>=1wheret.X1-t.X2<=3wheret.X1==(2*t.X3)+t.X2selectt;varresult=theorem.Solve();Console.WriteLine(result);}

In this example, we have two countries that produce crude oil which we refine into three end-products: gasoline, jet fuel, and lubricant. The crude oil from each country yields different quantities of end-products once the oil is refined:

Given we need to produce the following volume of refined end-product:

What is the most cost efficient purchase strategy of crude oil from Saudi Arabia and Venezuela?

using(varctx=newZ3Context()){vartheorem=fromtinctx.NewTheorem<(doublesa,doublevz)>()where0.3*t.sa+0.4*t.vz>=1900// Gasolenewhere0.4*t.sa+0.2*t.vz>=1500// Jet fuelwhere0.2*t.sa+0.3*t.vz>=500// Lubricantwhere0<=t.sa&&t.sa<=9000// Max # barrels we can purchasewhere0<=t.vz&&t.vz<=6000// Max # barrels we can purchase                  orderby(20.0*t.sa)+(15.0*t.vz)// Optimize for costselectt;varresult=theorem.Solve();Console.WriteLine($"SA:{result.sa} barrels (${result.sa*20}), VZ:{result.vz} barrels (${result.vz*15})");}

In this example, you want to minimize the cost of shipping goods from 2 different warehouses to 4 different customers. Each warehouse has a limited supply and each customer has a certain demand.

Cost of shipping ($ per product):

Number of products shipped:

1. The objective is to minimize the cost (Total Shipping Cost).
2. The variables are the number of products to ship from each warehouse to each customer.
3. The constraints are the number of products ordered and the number of products available in each warehouse.

using(varctx=newZ3Context()){vartheorem=fromtinctx.NewTheorem<(doublew1c1,doublew1c2,doublew1c3,doublew1c4,doublew2c1,doublew2c2,doublew2c3,doublew2c4)>()wheret.w1c1+t.w1c2+t.w1c3+t.w1c4<=60_000// Warehouse 1 Product Availabilitywheret.w2c1+t.w2c2+t.w2c3+t.w2c4<=80_000// Warehouse 2 Product Availabilitywheret.w1c1+t.w2c1==35_000&&(t.w1c1>=0&&t.w2c1>=0)// Customer 1 Orderswheret.w1c2+t.w2c2==22_000&&(t.w1c2>=0&&t.w2c2>=0)// Customer 2 Orderswheret.w1c3+t.w2c3==18_000&&(t.w1c3>=0&&t.w2c3>=0)// Customer 3 Orderswheret.w1c4+t.w2c4==30_000&&(t.w1c4>=0&&t.w2c4>=0)// Customer 4 Orders        orderby(1.00*t.w1c1)+(3.00*t.w1c2)+(0.50*t.w1c3)+(4.00*t.w1c4)+(2.50*t.w2c1)+(5.00*t.w2c2)+(1.50*t.w2c3)+(2.50*t.w2c4)// Optimize for Total Shipping Costselectt;varresult=theorem.Solve();Console.WriteLine($"|                     | Customer 1 | Customer 2  | Customer 3 | Customer 4 |");Console.WriteLine($"|---------------------|------------|-------------|------------|------------|");Console.WriteLine($"| Warehouse 1         |{result.w1c1}      |{result.w1c2}       |{result.w1c3}      |{result.w1c4}          |");Console.WriteLine($"| Warehouse 2         |{result.w2c1}          |{result.w2c2}           |{result.w2c3}      |{result.w2c4}      |");Console.WriteLine();Console.WriteLine(string.Create(CultureInfo.CreateSpecificCulture("en-US"),$"Total Cost:{1.00*result.w1c1+3.00*result.w1c2+0.50*result.w1c3+4.00*result.w1c4+2.50*result.w2c1+5.00*result.w2c2+1.50*result.w2c3+2.50*result.w2c4:C}"));}

You can install theZ3.Linq NuGet Package.

Add the package:

#r "nuget:Z3.Linq"

Then add the following using statements:

usingSystem;usingZ3.Linq;

Then you can copy any of the above samples.

Add theZ3.Linq package.Configure your application totarget x64 platform. This is a requirement asZ3.Linq uses theMicrosoft.Z3 package.

There are a number of ways in which you could contribute to this project:

• Create new examples!
• Improve the documentation.
• Report / fix bugs.
• Suggest any implementation improvements or optimizations.
• Blog about the project!

All PRs are welcome.

2009:Bart De Smet describes a prototype LINQ to Z3 binding in three blog posts:

• LINQ to Z3 - Part 1 – Exploring The Z3 Theorem Prover
• LINQ to Z3 - Part 2 – LINQ to the Unexpected
• LINQ to Z3 - Part 3 – Theorem Solving On Steroids

2010: Bart wasinterviewed on Channel 9 about the LINQ to Z3 concept:

2012: Bart presentedLINQ to Everything at TechEd Europe 2012:

2015: Z3 was open sourced under the MIT license and thesource code was moved to GitHub, where it is actively maintained.

2015:Ricardo Niepel (Microsoft) publishes the sample asZ3.LinqBinding using.NET 4.5 and Z3 binaries4.4.0

2018:Jean-Sylvain Boige (My Intelligence Agency) addsMissionaries And Cannibals sample.

2020:Karel Frajtak addssupport for fractions.

2021:Howard van Rooijen andIan Griffiths (endjin) upgrade the project to.NET 6.0, addedOptimize support via LINQ'sOrderBy,ValueTuple support, demonstrate usingrecord types, and fix nullability issues. They upgraded the solution to useZ3 NuGet package, merged in features fromJean-Sylvain Boige andKarel Frajtak forks, created archives of Bart's original blog posts and talks. They republished the project asZ3.Linq, created a newPolyglot Notebook ofsamples, and published a NuGet packageZ3.Linq.

2023:Whit Waldo upgrades the project to.NET 8.0

This project is sponsored byendjin, a UK based Technology Consultancy which specializes in Data, AI, DevOps & Cloud, and is a.NET Foundation Corporate Sponsor.

We help small teams achieve big things.

We produce two free weekly newsletters:

• Azure Weekly for all things about the Microsoft Azure Platform
• Power BI Weekly for all things Power BI, Microsoft Fabric, and Azure Synapse Analytics

Keep up with everything that's going on at endjin via ourblog, follow us onTwitter,YouTube orLinkedIn.

We have become the maintainers of a number of popular .NET Open Source Projects:

• Reactive Extensions for .NET
• Reaqtor
• Argotic Syndication Framework

And we have over 50 Open Source projects of our own, spread across the following GitHub Orgs:

• endjin
• Corvus
• Menes
• Marain
• AIS.NET

And the DevOps tooling we have created for managing all these projects is available on thePowerShell Gallery.

For more information about our products and services, or for commercial support of this project, pleasecontact us.

This project has adopted a code of conduct adapted from theContributor Covenant to clarify expected behavior in our community. This code of conduct has beenadopted by many other projects. For more information see theCode of Conduct FAQ or contacthello@endjin.com with any additional questions or comments.

TheIP Maturity Model is endjin's IP quality assessment framework, which we've developed over a number of years when doing due diligence assessments of 3rd party systems. We've codified the approach into aconfigurable set of rules, which are committed into theroot of a repo, and aAzure Function HttpTrigger HTTP endpoint which can evaluate the ruleset, and render an svg badge for display in repo'sreadme.md.