mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-01-19 19:31:24 -08:00
parent e23509797a 43d083bafb
commit 1bfd09e16b
17 changed files with 621 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/dotnet/Program.cs
View file

@ -818,6 +818,7 @@ namespace test_mapi
BigIntCheck(ctx, ctx.MkReal("234234333/2"));
#if !FRAMEWORK_LT_4
string bn = "1234567890987654321";
if (ctx.MkInt(bn).BigInteger.ToString() != bn)
@ -828,6 +829,7 @@ namespace test_mapi
if (ctx.MkBV(bn, 32).BigInteger.ToString() == bn)
throw new TestFailedException();
#endif
// Error handling test.
try
@ -1094,8 +1096,10 @@ namespace test_mapi
static void BigIntCheck(Context ctx, RatNum r)
{
#if !FRAMEWORK_LT_4
Console.WriteLine("Num: " + r.BigIntNumerator);
Console.WriteLine("Den: " + r.BigIntDenominator);
#endif
}
/// <summary>

6
scripts/mk_util.py
View file

@ -2442,7 +2442,7 @@ def mk_config():
CXXFLAGS = '%s -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer' % CXXFLAGS
if is_CXX_clangpp():
CXXFLAGS = '%s -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value' % CXXFLAGS
sysname = os.uname()[0]
sysname, _, _, _, machine = os.uname()
if sysname == 'Darwin':
SO_EXT = '.dylib'
SLIBFLAGS = '-dynamiclib'
@ -2493,7 +2493,9 @@ def mk_config():
# and to make it create an import library.
SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS
LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
CXXFLAGS = '%s -fpic' % CXXFLAGS
config.write('PREFIX=%s\n' % PREFIX)
config.write('CC=%s\n' % CC)
config.write('CXX=%s\n' % CXX)

4
scripts/mk_win_dist.py
View file

@ -241,8 +241,8 @@ def mk_zip(x64):
# Create a zip file for each platform
def mk_zips():
mk_zip_core(False)
mk_zip_core(True)
mk_zip(False)
mk_zip(True)
VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'),

6
src/api/dotnet/dotnet35/Example/App.config Normal file
View file

@ -0,0 +1,6 @@
<?xml version="1.0" encoding="utf-8" ?>
<configuration>
<startup>
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5.2" />
</startup>
</configuration>

78
src/api/dotnet/dotnet35/Example/Example.csproj Normal file
View file

@ -0,0 +1,78 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="14.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProjectGuid>{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}</ProjectGuid>
<OutputType>Exe</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Example</RootNamespace>
<AssemblyName>Example</AssemblyName>
<TargetFrameworkVersion>v4.5.2</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<AutoGenerateBindingRedirects>true</AutoGenerateBindingRedirects>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<PlatformTarget>AnyCPU</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>bin\Debug\</OutputPath>
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<PlatformTarget>AnyCPU</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE;FRAMEWORK_LT_4</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
<DebugSymbols>true</DebugSymbols>
<OutputPath>bin\x64\Debug\</OutputPath>
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>x64</PlatformTarget>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<Prefer32Bit>true</Prefer32Bit>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
<OutputPath>bin\x64\Release\</OutputPath>
<DefineConstants>TRACE;FRAMEWORK_LT_4</DefineConstants>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<Prefer32Bit>true</Prefer32Bit>
</PropertyGroup>
<ItemGroup>
<Compile Include="..\..\..\..\..\examples\dotnet\Program.cs">
<Link>Program.cs</Link>
</Compile>
<Compile Include="Properties\AssemblyInfo.cs" />
</ItemGroup>
<ItemGroup>
<None Include="App.config" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Microsoft.Z3.NET35.csproj">
<Project>{ec3db697-b734-42f7-9468-5b62821eeb5a}</Project>
<Name>Microsoft.Z3.NET35</Name>
</ProjectReference>
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
<Target Name="BeforeBuild">
</Target>
<Target Name="AfterBuild">
</Target>
-->
</Project>

36
src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs Normal file
View file

@ -0,0 +1,36 @@
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
// General Information about an assembly is controlled through the following
// set of attributes. Change these attribute values to modify the information
// associated with an assembly.
[assembly: AssemblyTitle("Example")]
[assembly: AssemblyDescription("")]
[assembly: AssemblyConfiguration("")]
[assembly: AssemblyCompany("")]
[assembly: AssemblyProduct("Example")]
[assembly: AssemblyCopyright("Copyright © 2017")]
[assembly: AssemblyTrademark("")]
[assembly: AssemblyCulture("")]
// Setting ComVisible to false makes the types in this assembly not visible
// to COM components. If you need to access a type in this assembly from
// COM, set the ComVisible attribute to true on that type.
[assembly: ComVisible(false)]
// The following GUID is for the ID of the typelib if this project is exposed to COM
[assembly: Guid("2a8e577b-7b6d-4ca9-832a-ca2eec314812")]
// Version information for an assembly consists of the following four values:
//
// Major Version
// Minor Version
// Build Number
// Revision
//
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("1.0.*")]
[assembly: AssemblyVersion("1.0.0.0")]
[assembly: AssemblyFileVersion("1.0.0.0")]

347
src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj Normal file
View file

@ -0,0 +1,347 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{EC3DB697-B734-42F7-9468-5B62821EEB5A}</ProjectGuid>
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Z3</RootNamespace>
<AssemblyName>Microsoft.Z3</AssemblyName>
<TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile>
</TargetFrameworkProfile>
<CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>Debug\</OutputPath>
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>Debug\Microsoft.Z3.XML</DocumentationFile>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
<CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
<CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
<CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
<CodeContractsInferRequires>True</CodeContractsInferRequires>
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
<CodeContractsDisjunctiveRequires>True</CodeContractsDisjunctiveRequires>
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
<CodeContractsCustomRewriterAssembly />
<CodeContractsCustomRewriterClass />
<CodeContractsLibPaths />
<CodeContractsExtraRewriteOptions />
<CodeContractsExtraAnalysisOptions />
<CodeContractsBaseLineFile />
<CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>Release\</OutputPath>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>Release\Microsoft.Z3.xml</DocumentationFile>
<PlatformTarget>x86</PlatformTarget>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
</PropertyGroup>
<PropertyGroup>
<AssemblyOriginatorKeyFile>
</AssemblyOriginatorKeyFile>
</PropertyGroup>
<PropertyGroup>
<DelaySign>false</DelaySign>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
<DebugSymbols>true</DebugSymbols>
<OutputPath>bin\x64\Debug\</OutputPath>
<DefineConstants>TRACE;DEBUG;FRAMEWORK_LT_4</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>Debug\Microsoft.Z3.XML</DocumentationFile>
<DebugType>full</DebugType>
<PlatformTarget>x64</PlatformTarget>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
<OutputPath>bin\x64\Release\</OutputPath>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>Release\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
</PropertyGroup>
<ItemGroup>
<Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<HintPath>packages\Code.Contract.1.0.0\lib\net35\Microsoft.Contracts.dll</HintPath>
<Private>True</Private>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
</ItemGroup>
<ItemGroup>
<Compile Include="..\AlgebraicNum.cs">
<Link>AlgebraicNum.cs</Link>
</Compile>
<Compile Include="..\ApplyResult.cs">
<Link>ApplyResult.cs</Link>
</Compile>
<Compile Include="..\ArithExpr.cs">
<Link>ArithExpr.cs</Link>
</Compile>
<Compile Include="..\ArithSort.cs">
<Link>ArithSort.cs</Link>
</Compile>
<Compile Include="..\ArrayExpr.cs">
<Link>ArrayExpr.cs</Link>
</Compile>
<Compile Include="..\ArraySort.cs">
<Link>ArraySort.cs</Link>
</Compile>
<Compile Include="..\AST.cs">
<Link>AST.cs</Link>
</Compile>
<Compile Include="..\ASTMap.cs">
<Link>ASTMap.cs</Link>
</Compile>
<Compile Include="..\ASTVector.cs">
<Link>ASTVector.cs</Link>
</Compile>
<Compile Include="..\BitVecExpr.cs">
<Link>BitVecExpr.cs</Link>
</Compile>
<Compile Include="..\BitVecNum.cs">
<Link>BitVecNum.cs</Link>
</Compile>
<Compile Include="..\BitVecSort.cs">
<Link>BitVecSort.cs</Link>
</Compile>
<Compile Include="..\BoolExpr.cs">
<Link>BoolExpr.cs</Link>
</Compile>
<Compile Include="..\BoolSort.cs">
<Link>BoolSort.cs</Link>
</Compile>
<Compile Include="..\Constructor.cs">
<Link>Constructor.cs</Link>
</Compile>
<Compile Include="..\ConstructorList.cs">
<Link>ConstructorList.cs</Link>
</Compile>
<Compile Include="..\Context.cs">
<Link>Context.cs</Link>
</Compile>
<Compile Include="..\DatatypeExpr.cs">
<Link>DatatypeExpr.cs</Link>
</Compile>
<Compile Include="..\DatatypeSort.cs">
<Link>DatatypeSort.cs</Link>
</Compile>
<Compile Include="..\Deprecated.cs">
<Link>Deprecated.cs</Link>
</Compile>
<Compile Include="..\Enumerations.cs">
<Link>Enumerations.cs</Link>
</Compile>
<Compile Include="..\EnumSort.cs">
<Link>EnumSort.cs</Link>
</Compile>
<Compile Include="..\Expr.cs">
<Link>Expr.cs</Link>
</Compile>
<Compile Include="..\FiniteDomainExpr.cs">
<Link>FiniteDomainExpr.cs</Link>
</Compile>
<Compile Include="..\FiniteDomainNum.cs">
<Link>FiniteDomainNum.cs</Link>
</Compile>
<Compile Include="..\FiniteDomainSort.cs">
<Link>FiniteDomainSort.cs</Link>
</Compile>
<Compile Include="..\Fixedpoint.cs">
<Link>Fixedpoint.cs</Link>
</Compile>
<Compile Include="..\FPExpr.cs">
<Link>FPExpr.cs</Link>
</Compile>
<Compile Include="..\FPNum.cs">
<Link>FPNum.cs</Link>
</Compile>
<Compile Include="..\FPRMExpr.cs">
<Link>FPRMExpr.cs</Link>
</Compile>
<Compile Include="..\FPRMNum.cs">
<Link>FPRMNum.cs</Link>
</Compile>
<Compile Include="..\FPRMSort.cs">
<Link>FPRMSort.cs</Link>
</Compile>
<Compile Include="..\FPSort.cs">
<Link>FPSort.cs</Link>
</Compile>
<Compile Include="..\FuncDecl.cs">
<Link>FuncDecl.cs</Link>
</Compile>
<Compile Include="..\FuncInterp.cs">
<Link>FuncInterp.cs</Link>
</Compile>
<Compile Include="..\Global.cs">
<Link>Global.cs</Link>
</Compile>
<Compile Include="..\Goal.cs">
<Link>Goal.cs</Link>
</Compile>
<Compile Include="..\IDecRefQueue.cs">
<Link>IDecRefQueue.cs</Link>
</Compile>
<Compile Include="..\InterpolationContext.cs">
<Link>InterpolationContext.cs</Link>
</Compile>
<Compile Include="..\IntExpr.cs">
<Link>IntExpr.cs</Link>
</Compile>
<Compile Include="..\IntNum.cs">
<Link>IntNum.cs</Link>
</Compile>
<Compile Include="..\IntSort.cs">
<Link>IntSort.cs</Link>
</Compile>
<Compile Include="..\IntSymbol.cs">
<Link>IntSymbol.cs</Link>
</Compile>
<Compile Include="..\ListSort.cs">
<Link>ListSort.cs</Link>
</Compile>
<Compile Include="..\Log.cs">
<Link>Log.cs</Link>
</Compile>
<Compile Include="..\Model.cs">
<Link>Model.cs</Link>
</Compile>
<Compile Include="..\Native.cs">
<Link>Native.cs</Link>
</Compile>
<Compile Include="..\Optimize.cs">
<Link>Optimize.cs</Link>
</Compile>
<Compile Include="..\ParamDescrs.cs">
<Link>ParamDescrs.cs</Link>
</Compile>
<Compile Include="..\Params.cs">
<Link>Params.cs</Link>
</Compile>
<Compile Include="..\Pattern.cs">
<Link>Pattern.cs</Link>
</Compile>
<Compile Include="..\Probe.cs">
<Link>Probe.cs</Link>
</Compile>
<Compile Include="..\Quantifier.cs">
<Link>Quantifier.cs</Link>
</Compile>
<Compile Include="..\RatNum.cs">
<Link>RatNum.cs</Link>
</Compile>
<Compile Include="..\RealExpr.cs">
<Link>RealExpr.cs</Link>
</Compile>
<Compile Include="..\RealSort.cs">
<Link>RealSort.cs</Link>
</Compile>
<Compile Include="..\ReExpr.cs">
<Link>ReExpr.cs</Link>
</Compile>
<Compile Include="..\RelationSort.cs">
<Link>RelationSort.cs</Link>
</Compile>
<Compile Include="..\ReSort.cs">
<Link>ReSort.cs</Link>
</Compile>
<Compile Include="..\SeqExpr.cs">
<Link>SeqExpr.cs</Link>
</Compile>
<Compile Include="..\SeqSort.cs">
<Link>SeqSort.cs</Link>
</Compile>
<Compile Include="..\SetSort.cs">
<Link>SetSort.cs</Link>
</Compile>
<Compile Include="..\Solver.cs">
<Link>Solver.cs</Link>
</Compile>
<Compile Include="..\Sort.cs">
<Link>Sort.cs</Link>
</Compile>
<Compile Include="..\Statistics.cs">
<Link>Statistics.cs</Link>
</Compile>
<Compile Include="..\Status.cs">
<Link>Status.cs</Link>
</Compile>
<Compile Include="..\StringSymbol.cs">
<Link>StringSymbol.cs</Link>
</Compile>
<Compile Include="..\Symbol.cs">
<Link>Symbol.cs</Link>
</Compile>
<Compile Include="..\Tactic.cs">
<Link>Tactic.cs</Link>
</Compile>
<Compile Include="..\TupleSort.cs">
<Link>TupleSort.cs</Link>
</Compile>
<Compile Include="..\UninterpretedSort.cs">
<Link>UninterpretedSort.cs</Link>
</Compile>
<Compile Include="..\Version.cs">
<Link>Version.cs</Link>
</Compile>
<Compile Include="..\Z3Exception.cs">
<Link>Z3Exception.cs</Link>
</Compile>
<Compile Include="..\Z3Object.cs">
<Link>Z3Object.cs</Link>
</Compile>
<Compile Include="Properties\AssemblyInfo.cs" />
</ItemGroup>
<ItemGroup>
<WCFMetadata Include="Service References\" />
</ItemGroup>
<ItemGroup>
<None Include="packages.config" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
</Project>

48
src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln Normal file
View file

@ -0,0 +1,48 @@

Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 14
VisualStudioVersion = 14.0.25420.1
MinimumVisualStudioVersion = 10.0.40219.1
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Microsoft.Z3.NET35", "Microsoft.Z3.NET35.csproj", "{EC3DB697-B734-42F7-9468-5B62821EEB5A}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Example", "Example\Example.csproj", "{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU
Debug|x64 = Debug|x64
Debug|x86 = Debug|x86
Release|Any CPU = Release|Any CPU
Release|x64 = Release|x64
Release|x86 = Release|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|Any CPU.Build.0 = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.ActiveCfg = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x64.Build.0 = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.ActiveCfg = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Debug|x86.Build.0 = Debug|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.ActiveCfg = Release|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|Any CPU.Build.0 = Release|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.ActiveCfg = Release|x64
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x64.Build.0 = Release|x64
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.ActiveCfg = Release|Any CPU
{EC3DB697-B734-42F7-9468-5B62821EEB5A}.Release|x86.Build.0 = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|Any CPU.Build.0 = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x64.Build.0 = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.ActiveCfg = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Debug|x86.Build.0 = Debug|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.ActiveCfg = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|Any CPU.Build.0 = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.ActiveCfg = Release|x64
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x64.Build.0 = Release|x64
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.ActiveCfg = Release|Any CPU
{2A8E577B-7B6D-4CA9-832A-CA2EEC314812}.Release|x86.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
EndGlobal

38
src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs Normal file
View file

@ -0,0 +1,38 @@
using System;
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
using System.Security.Permissions;
// General Information about an assembly is controlled through the following
// set of attributes. Change these attribute values to modify the information
// associated with an assembly.
[assembly: AssemblyTitle("Z3 .NET Interface")]
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
[assembly: AssemblyConfiguration("")]
[assembly: AssemblyCompany("Microsoft Corporation")]
[assembly: AssemblyProduct("Z3")]
[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
[assembly: AssemblyTrademark("")]
[assembly: AssemblyCulture("")]
// Setting ComVisible to false makes the types in this assembly not visible
// to COM components. If you need to access a type in this assembly from
// COM, set the ComVisible attribute to true on that type.
[assembly: ComVisible(false)]
// The following GUID is for the ID of the typelib if this project is exposed to COM
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
// Version information for an assembly consists of the following four values:
//
// Major Version
// Minor Version
// Build Number
// Revision
//
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")]
[assembly: AssemblyVersion("4.5.1.6031")]
[assembly: AssemblyFileVersion("4.5.1.6031")]

38
src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in Normal file
View file

@ -0,0 +1,38 @@
using System;
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
using System.Security.Permissions;
// General Information about an assembly is controlled through the following
// set of attributes. Change these attribute values to modify the information
// associated with an assembly.
[assembly: AssemblyTitle("Z3 .NET Interface")]
[assembly: AssemblyDescription(".NET Interface to the Z3 Theorem Prover")]
[assembly: AssemblyConfiguration("")]
[assembly: AssemblyCompany("Microsoft Corporation")]
[assembly: AssemblyProduct("Z3")]
[assembly: AssemblyCopyright("Copyright (C) 2006-2015 Microsoft Corporation")]
[assembly: AssemblyTrademark("")]
[assembly: AssemblyCulture("")]
// Setting ComVisible to false makes the types in this assembly not visible
// to COM components. If you need to access a type in this assembly from
// COM, set the ComVisible attribute to true on that type.
[assembly: ComVisible(false)]
// The following GUID is for the ID of the typelib if this project is exposed to COM
[assembly: Guid("4853ed71-2078-40f4-8117-bc46646bce0e")]
// Version information for an assembly consists of the following four values:
//
// Major Version
// Minor Version
// Build Number
// Revision
//
// You can specify all the values or you can default the Build and Revision Numbers
// by using the '*' as shown below:
// [assembly: AssemblyVersion("4.2.0.0")]
[assembly: AssemblyVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]
[assembly: AssemblyFileVersion("@VER_MAJOR@.@VER_MINOR@.@VER_BUILD@.@VER_REVISION@")]

3
src/api/dotnet/Readme.NET35 → src/api/dotnet/dotnet35/Readme.NET35
View file

@ -6,4 +6,5 @@ In the project properties of Microsoft.Z3.csproj:
- Under 'Application': Change Target framework to .NET Framework 3.5
- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
- Remove the reference to System.Numerics
- Install the NuGet Package "Microsoft Code Contracts for Net3.5"
- Install the NuGet Package "Microsoft Code Contracts for Net3.5":
In the Package Manager Console enter Install-Package Code.Contract

4
src/api/dotnet/dotnet35/packages.config Normal file
View file

@ -0,0 +1,4 @@
<?xml version="1.0" encoding="utf-8"?>
<packages>
<package id="Code.Contract" version="1.0.0" targetFramework="net35" />
</packages>

15
src/opt/maxsmt.cpp
View file

@ -55,15 +55,18 @@ namespace opt {
void maxsmt_solver_base::commit_assignment() {
expr_ref tmp(m);
rational k(0);
rational k(0), cost(0);
for (unsigned i = 0; i < m_soft.size(); ++i) {
if (get_assignment(i)) {
k += m_weights[i];
}
else {
cost += m_weights[i];
}
}
pb_util pb(m);
tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
TRACE("opt", tout << tmp << "\n";);
TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";);
s().assert_expr(tmp);
}
@ -140,7 +143,9 @@ namespace opt {
m_wth = s.ensure_wmax_theory();
}
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
//m_wth->reset_local();
if (m_wth) {
m_wth->reset_local();
}
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
@ -226,7 +231,9 @@ namespace opt {
m_msolver = 0;
symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";);
TRACE("opt", tout << "maxsmt\n";
s().display(tout); tout << "\n";
);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
}

7
src/opt/opt_solver.cpp
View file

@ -327,12 +327,7 @@ namespace opt {
SASSERT(idx < get_num_assertions());
return m_context.get_formulas()[idx];
}
std::ostream& opt_solver::display(std::ostream & out) const {
m_context.display(out);
return out;
}
smt::theory_var opt_solver::add_objective(app* term) {
smt::theory_var v = get_optimizer().add_objective(term);
m_objective_vars.push_back(v);

1
src/opt/opt_solver.h
View file

@ -104,7 +104,6 @@ namespace opt {
virtual void set_progress_callback(progress_callback * callback);
virtual unsigned get_num_assertions() const;
virtual expr * get_assertion(unsigned idx) const;
virtual std::ostream& display(std::ostream & out) const;
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);

1
src/opt/wmax.cpp
View file

@ -64,6 +64,7 @@ namespace opt {
bool was_sat = false;
expr_ref_vector asms(m);
vector<expr_ref_vector> cores;
obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
for (; it != end; ++it) {
expr* c = assert_weighted(wth(), it->m_key, it->m_value);

1
src/smt/smt_context.cpp
View file

@ -1795,6 +1795,7 @@ namespace smt {
void context::set_conflict(b_justification js, literal not_l) {
if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
m_conflict = js;
m_not_l = not_l;
}