porting to windows

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))

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)) {

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;
 }
 
 

src/interp/iz3base.h

@@ -145,7 +145,7 @@ class iz3base : public iz3mgr, public scopes {
   ast simplify_and(std::vector<ast> &conjuncts);
   ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth);
   ast simplify_with_lit(ast n, ast lit);  
-  void find_children(const stl_ext::hash_set<ast> &cnsts_set,
+  void find_children(const hash_set<ast> &cnsts_set,
 		     const ast &tree,
 		     std::vector<ast> &cnsts,
 		     std::vector<int> &parents,

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<ast_r> {
   public:
@@ -124,12 +124,21 @@ namespace stl_ext {
   };
 }
 
+// to make ast_r hashable in windows
+#ifdef WIN32 
+template <> inline
+size_t stdext::hash_value<ast_r >(const ast_r& s)
+{	
+  return s.raw()->get_id();
+}
+#endif
+
 // to make ast_r usable in ordered collections
 namespace std {
   template <>
     class less<ast_r> {
   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();
     }
   };

src/interp/iz3translate_direct.cpp

@@ -81,8 +81,8 @@ namespace std {
   class less<Z3_resolvent > {
   public:
    bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const {
-     size_t ixproof = (size_t) x.proof;
+     size_t ixproof = (size_t) x.proof.raw();
-     size_t iyproof = (size_t) y.proof;
+     size_t iyproof = (size_t) y.proof.raw();
      if(ixproof < iyproof) return true;
      if(ixproof > iyproof) return false;
      return x.pivot < y.pivot;