From 28266786f3ce96556d982071ba89b5a7a05de07c Mon Sep 17 00:00:00 2001 From: "U-REDMOND\\kenmcmil" Date: Wed, 27 Mar 2013 12:17:52 -0700 Subject: [PATCH] porting to windows --- scripts/mk_util.py | 2 + src/api/dotnet/Properties/AssemblyInfo.cs | 78 +++++++++++------------ src/cmd_context/cmd_context.cpp | 2 - src/interp/iz3base.cpp | 1 + src/interp/iz3base.h | 2 +- src/interp/iz3mgr.h | 13 +++- src/interp/iz3translate_direct.cpp | 4 +- 7 files changed, 56 insertions(+), 46 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index c2a168b70..8116da3f5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -909,6 +909,7 @@ class ExeComponent(Component): for dep in deps: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) + out.write(' ' + FOCI2LIB) out.write(' $(LINK_EXTRA_FLAGS)\n') out.write('%s: %s\n\n' % (self.name, exefile)) @@ -1012,6 +1013,7 @@ class DLLComponent(Component): if not dep in self.reexports: c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) + out.write(' ' + FOCI2LIB) out.write(' $(SLINK_EXTRA_FLAGS)') if IS_WINDOWS: out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs index 1ac6cb520..517349177 100644 --- a/src/api/dotnet/Properties/AssemblyInfo.cs +++ b/src/api/dotnet/Properties/AssemblyInfo.cs @@ -1,39 +1,39 @@ -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 © Microsoft Corporation 2006")] -[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.3.2.0")] -[assembly: AssemblyFileVersion("4.3.2.0")] - +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 © Microsoft Corporation 2006")] +[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.3.2.0")] +[assembly: AssemblyFileVersion("4.3.2.0")] + diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index f53c9850a..20539266b 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -39,8 +39,6 @@ Notes: #include"for_each_expr.h" #include"scoped_timer.h" #include"interpolant_cmds.h" -//FIXME Does this break modularity? -// #include"smt_solver.h" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index e39dc9513..5350a8fb3 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -243,6 +243,7 @@ bool iz3base::is_sat(ast f){ Z3_pop(ctx,1); return res != Z3_L_FALSE; #endif + return false; } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index da0a3ce4a..c8d4b3c9e 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -145,7 +145,7 @@ class iz3base : public iz3mgr, public scopes { ast simplify_and(std::vector &conjuncts); ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map &memo, int depth); ast simplify_with_lit(ast n, ast lit); - void find_children(const stl_ext::hash_set &cnsts_set, + void find_children(const hash_set &cnsts_set, const ast &tree, std::vector &cnsts, std::vector &parents, diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 3317b9d7d..e948e9ceb 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -114,7 +114,7 @@ class ast_r : public ast_i { }; // to make ast_r hashable -namespace stl_ext { +namespace hash_space { template <> class hash { public: @@ -124,12 +124,21 @@ namespace stl_ext { }; } +// to make ast_r hashable in windows +#ifdef WIN32 +template <> inline +size_t stdext::hash_value(const ast_r& s) +{ + return s.raw()->get_id(); +} +#endif + // to make ast_r usable in ordered collections namespace std { template <> class less { public: - size_t operator()(const ast_r &s, const ast_r &t) const { + bool operator()(const ast_r &s, const ast_r &t) const { return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); } }; diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index d4656d3a8..da05c6642 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -81,8 +81,8 @@ namespace std { class less { public: bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const { - size_t ixproof = (size_t) x.proof; - size_t iyproof = (size_t) y.proof; + size_t ixproof = (size_t) x.proof.raw(); + size_t iyproof = (size_t) y.proof.raw(); if(ixproof < iyproof) return true; if(ixproof > iyproof) return false; return x.pivot < y.pivot;