diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 5b10dadd0..20bb012b1 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -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 } /// diff --git a/scripts/mk_util.py b/scripts/mk_util.py index fd8962bda..807a131c1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 11048650f..66f44426f 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -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'), diff --git a/src/api/dotnet/dotnet35/Example/App.config b/src/api/dotnet/dotnet35/Example/App.config new file mode 100644 index 000000000..88fa4027b --- /dev/null +++ b/src/api/dotnet/dotnet35/Example/App.config @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file diff --git a/src/api/dotnet/dotnet35/Example/Example.csproj b/src/api/dotnet/dotnet35/Example/Example.csproj new file mode 100644 index 000000000..2b096ed40 --- /dev/null +++ b/src/api/dotnet/dotnet35/Example/Example.csproj @@ -0,0 +1,78 @@ + + + + + Debug + AnyCPU + {2A8E577B-7B6D-4CA9-832A-CA2EEC314812} + Exe + Properties + Example + Example + v4.5.2 + 512 + true + + + AnyCPU + true + full + false + bin\Debug\ + TRACE;DEBUG;FRAMEWORK_LT_4 + prompt + 4 + + + AnyCPU + pdbonly + true + bin\Release\ + TRACE;FRAMEWORK_LT_4 + prompt + 4 + + + true + bin\x64\Debug\ + TRACE;DEBUG;FRAMEWORK_LT_4 + full + x64 + prompt + MinimumRecommendedRules.ruleset + true + + + bin\x64\Release\ + TRACE;FRAMEWORK_LT_4 + true + pdbonly + x64 + prompt + MinimumRecommendedRules.ruleset + true + + + + Program.cs + + + + + + + + + {ec3db697-b734-42f7-9468-5b62821eeb5a} + Microsoft.Z3.NET35 + + + + + \ No newline at end of file diff --git a/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..ed0d8454f --- /dev/null +++ b/src/api/dotnet/dotnet35/Example/Properties/AssemblyInfo.cs @@ -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")] diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj new file mode 100644 index 000000000..d278b4f1d --- /dev/null +++ b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.csproj @@ -0,0 +1,347 @@ + + + + Debug + AnyCPU + 8.0.30703 + 2.0 + {EC3DB697-B734-42F7-9468-5B62821EEB5A} + Library + Properties + Microsoft.Z3 + Microsoft.Z3 + v3.5 + 512 + + + 0 + + + true + full + false + Debug\ + TRACE;DEBUG;FRAMEWORK_LT_4 + prompt + 4 + true + Debug\Microsoft.Z3.XML + False + False + True + False + False + True + False + True + True + False + False + False + True + False + False + False + True + False + False + True + True + True + False + False + + + + + + + True + Full + %28none%29 + 2 + + + pdbonly + true + Release\ + FRAMEWORK_LT_4 + prompt + 4 + true + Release\Microsoft.Z3.xml + x86 + + + true + + + + + + + false + + + true + bin\x64\Debug\ + TRACE;DEBUG;FRAMEWORK_LT_4 + true + Debug\Microsoft.Z3.XML + full + x64 + prompt + MinimumRecommendedRules.ruleset + + + bin\x64\Release\ + FRAMEWORK_LT_4 + true + Release\Microsoft.Z3.xml + true + pdbonly + x64 + prompt + MinimumRecommendedRules.ruleset + + + + packages\Code.Contract.1.0.0\lib\net35\Microsoft.Contracts.dll + True + + + + + + + AlgebraicNum.cs + + + ApplyResult.cs + + + ArithExpr.cs + + + ArithSort.cs + + + ArrayExpr.cs + + + ArraySort.cs + + + AST.cs + + + ASTMap.cs + + + ASTVector.cs + + + BitVecExpr.cs + + + BitVecNum.cs + + + BitVecSort.cs + + + BoolExpr.cs + + + BoolSort.cs + + + Constructor.cs + + + ConstructorList.cs + + + Context.cs + + + DatatypeExpr.cs + + + DatatypeSort.cs + + + Deprecated.cs + + + Enumerations.cs + + + EnumSort.cs + + + Expr.cs + + + FiniteDomainExpr.cs + + + FiniteDomainNum.cs + + + FiniteDomainSort.cs + + + Fixedpoint.cs + + + FPExpr.cs + + + FPNum.cs + + + FPRMExpr.cs + + + FPRMNum.cs + + + FPRMSort.cs + + + FPSort.cs + + + FuncDecl.cs + + + FuncInterp.cs + + + Global.cs + + + Goal.cs + + + IDecRefQueue.cs + + + InterpolationContext.cs + + + IntExpr.cs + + + IntNum.cs + + + IntSort.cs + + + IntSymbol.cs + + + ListSort.cs + + + Log.cs + + + Model.cs + + + Native.cs + + + Optimize.cs + + + ParamDescrs.cs + + + Params.cs + + + Pattern.cs + + + Probe.cs + + + Quantifier.cs + + + RatNum.cs + + + RealExpr.cs + + + RealSort.cs + + + ReExpr.cs + + + RelationSort.cs + + + ReSort.cs + + + SeqExpr.cs + + + SeqSort.cs + + + SetSort.cs + + + Solver.cs + + + Sort.cs + + + Statistics.cs + + + Status.cs + + + StringSymbol.cs + + + Symbol.cs + + + Tactic.cs + + + TupleSort.cs + + + UninterpretedSort.cs + + + Version.cs + + + Z3Exception.cs + + + Z3Object.cs + + + + + + + + + + + \ No newline at end of file diff --git a/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln new file mode 100644 index 000000000..b6e252684 --- /dev/null +++ b/src/api/dotnet/dotnet35/Microsoft.Z3.NET35.sln @@ -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 diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..fb4319002 --- /dev/null +++ b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs @@ -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")] diff --git a/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in new file mode 100644 index 000000000..e5a85f16f --- /dev/null +++ b/src/api/dotnet/dotnet35/Properties/AssemblyInfo.cs.in @@ -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@")] diff --git a/src/api/dotnet/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35 similarity index 87% rename from src/api/dotnet/Readme.NET35 rename to src/api/dotnet/dotnet35/Readme.NET35 index 73743fd15..f8c2958ee 100644 --- a/src/api/dotnet/Readme.NET35 +++ b/src/api/dotnet/dotnet35/Readme.NET35 @@ -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 diff --git a/src/api/dotnet/dotnet35/packages.config b/src/api/dotnet/dotnet35/packages.config new file mode 100644 index 000000000..daa06aed7 --- /dev/null +++ b/src/api/dotnet/dotnet35/packages.config @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 97b6a5293..f93291599 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -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); } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 42129be70..351141a3f 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -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); diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index cdaad3cf2..27168e2ca 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -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& mutexes); virtual lbool preferred_sat(expr_ref_vector const& asms, vector& cores); diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 690e2000b..9708bdc8f 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -64,6 +64,7 @@ namespace opt { bool was_sat = false; expr_ref_vector asms(m); vector cores; + obj_map::iterator it = soft.begin(), end = soft.end(); for (; it != end; ++it) { expr* c = assert_weighted(wth(), it->m_key, it->m_value); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ea97d1a64..c7aecca88 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; }