BitwuzlaSharp 0.1.2
See the version list below for details.
dotnet add package BitwuzlaSharp --version 0.1.2
NuGet\Install-Package BitwuzlaSharp -Version 0.1.2
<PackageReference Include="BitwuzlaSharp" Version="0.1.2" />
<PackageVersion Include="BitwuzlaSharp" Version="0.1.2" />
<PackageReference Include="BitwuzlaSharp" />
paket add BitwuzlaSharp --version 0.1.2
#r "nuget: BitwuzlaSharp, 0.1.2"
#:package BitwuzlaSharp@0.1.2
#addin nuget:?package=BitwuzlaSharp&version=0.1.2
#tool nuget:?package=BitwuzlaSharp&version=0.1.2
BitwuzlaSharp
.NET bindings for the Bitwuzla SMT solver — a solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions and their combinations.
The package bundles the native Bitwuzla library for win-x64 and linux-x64, so no separate native install is required.
Install
dotnet add package BitwuzlaSharp
Quick start
using Bitwuzla;
using var tm = new TermManager();
using var options = new Options();
options.Set(BitwuzlaOption.ProduceModels, true);
using var solver = new Solver(tm, options);
Sort bv8 = tm.MkBitVectorSort(8);
Term a = tm.MkConst(bv8, "a");
Term sum = tm.MkTerm(BitwuzlaKind.BvAdd, a, tm.MkBitVectorValue(bv8, 7UL));
// a + 7 == 10
solver.Assert(tm.MkTerm(BitwuzlaKind.Equal, sum, tm.MkBitVectorValue(bv8, 10UL)));
if (solver.CheckSat() == BitwuzlaResult.Sat)
{
Term value = solver.GetValue(a);
Console.WriteLine(value.GetValueString(10)); // 3
}
API shape
All public types live in the Bitwuzla namespace.
TermManager— createsSortandTermvalues; owns their lifetime.Options— solver configuration (BitwuzlaOption).Solver— the solver:Assert,Push/Pop,CheckSat,GetValue, unsat cores, etc.Sort/Term— lightweight handles valid until the owningTermManageris disposed.- A complete low-level P/Invoke surface lives in
Bitwuzla.Native.NativeMethodsfor anything the object model doesn't yet wrap.
Sort and Term are released in bulk when their TermManager is disposed, so dispose the
TermManager (and Solver/Options) when done — typically via using.
Building the native library
The native Bitwuzla library is built in CI from the pinned extern/bitwuzla submodule
(Bitwuzla 0.9.1): cross-platform on Linux, and on Windows via MSYS2/mingw-w64. The resulting
bitwuzla.dll / libbitwuzla.so (plus required runtime dependencies) are packed into
runtimes/<rid>/native/ of the NuGet package.
License
MIT. Bundled native components (Bitwuzla, GMP, MPFR) retain their own licenses; see LICENSE.
| Product | Versions Compatible and additional computed target framework versions. |
|---|---|
| .NET | net5.0 was computed. net5.0-windows was computed. net6.0 was computed. net6.0-android was computed. net6.0-ios was computed. net6.0-maccatalyst was computed. net6.0-macos was computed. net6.0-tvos was computed. net6.0-windows was computed. net7.0 was computed. net7.0-android was computed. net7.0-ios was computed. net7.0-maccatalyst was computed. net7.0-macos was computed. net7.0-tvos was computed. net7.0-windows was computed. net8.0 was computed. net8.0-android was computed. net8.0-browser was computed. net8.0-ios was computed. net8.0-maccatalyst was computed. net8.0-macos was computed. net8.0-tvos was computed. net8.0-windows was computed. net9.0 was computed. net9.0-android was computed. net9.0-browser was computed. net9.0-ios was computed. net9.0-maccatalyst was computed. net9.0-macos was computed. net9.0-tvos was computed. net9.0-windows was computed. net10.0 was computed. net10.0-android was computed. net10.0-browser was computed. net10.0-ios was computed. net10.0-maccatalyst was computed. net10.0-macos was computed. net10.0-tvos was computed. net10.0-windows was computed. |
| .NET Core | netcoreapp2.0 was computed. netcoreapp2.1 was computed. netcoreapp2.2 was computed. netcoreapp3.0 was computed. netcoreapp3.1 was computed. |
| .NET Standard | netstandard2.0 is compatible. netstandard2.1 was computed. |
| .NET Framework | net461 was computed. net462 was computed. net463 was computed. net47 was computed. net471 was computed. net472 was computed. net48 was computed. net481 was computed. |
| MonoAndroid | monoandroid was computed. |
| MonoMac | monomac was computed. |
| MonoTouch | monotouch was computed. |
| Tizen | tizen40 was computed. tizen60 was computed. |
| Xamarin.iOS | xamarinios was computed. |
| Xamarin.Mac | xamarinmac was computed. |
| Xamarin.TVOS | xamarintvos was computed. |
| Xamarin.WatchOS | xamarinwatchos was computed. |
-
.NETStandard 2.0
- No dependencies.
NuGet packages
This package is not used by any NuGet packages.
GitHub repositories
This package is not used by any popular GitHub repositories.