From acf4ad0ab670d1714e5a82aee7b4ac2c84ecd74a Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 27 Feb 2014 17:23:19 -0800 Subject: [PATCH] use new hashtable implementation in windows --- src/api/api_interp.cpp | 4 -- src/duality/duality.h | 2 - src/duality/duality_solver.cpp | 2 +- src/duality/duality_wrapper.h | 16 -------- src/interp/iz3base.cpp | 2 - src/interp/iz3checker.cpp | 2 - src/interp/iz3foci.cpp | 2 - src/interp/iz3hash.h | 3 ++ src/interp/iz3interp.cpp | 2 - src/interp/iz3mgr.cpp | 2 - src/interp/iz3mgr.h | 8 ---- src/interp/iz3pp.cpp | 4 -- src/interp/iz3proof_itp.cpp | 2 - src/interp/iz3translate.cpp | 2 - src/interp/iz3translate_direct.cpp | 65 ------------------------------ 15 files changed, 4 insertions(+), 114 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 98722022c..2c88a1978 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -39,11 +39,8 @@ Revision History: #include"iz3pp.h" #include"iz3checker.h" -#ifndef WIN32 using namespace stl_ext; -#endif -#ifndef WIN32 // WARNING: don't make a hash_map with this if the range type // has a destructor: you'll get an address dependency!!! namespace stl_ext { @@ -55,7 +52,6 @@ namespace stl_ext { } }; } -#endif typedef interpolation_options_struct *Z3_interpolation_options; diff --git a/src/duality/duality.h b/src/duality/duality.h index e1d058f10..479c90a29 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -25,9 +25,7 @@ Revision History: #include // make hash_map and hash_set available -#ifndef WIN32 using namespace stl_ext; -#endif namespace Duality { diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 1c2f2c927..6079e17d9 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1955,7 +1955,7 @@ namespace Duality { } if(update_count == 0){ if(was_sat) - throw Incompleteness(); + throw "Help!"; reporter->Message("backtracked without learning"); } } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 2b0045023..90f1799a6 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1401,14 +1401,6 @@ namespace hash_space { }; } -// to make Duality::ast hashable in windows -#ifdef WIN32 -template <> inline -size_t stdext::hash_value(const Duality::ast& s) -{ - return s.raw()->get_id(); -} -#endif // to make Duality::ast usable in ordered collections namespace std { @@ -1445,14 +1437,6 @@ namespace hash_space { }; } -// to make Duality::func_decl hashable in windows -#ifdef WIN32 -template <> inline -size_t stdext::hash_value(const Duality::func_decl& s) -{ - return s.raw()->get_id(); -} -#endif // to make Duality::func_decl usable in ordered collections namespace std { diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 26146bfa3..054c8a811 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -34,9 +34,7 @@ Revision History: #include "../smt/smt_solver.h" -#ifndef WIN32 using namespace stl_ext; -#endif iz3base::range &iz3base::ast_range(ast t){ diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index d423ba48f..02acaa5c1 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -36,9 +36,7 @@ Revision History: #include -#ifndef WIN32 using namespace stl_ext; -#endif struct iz3checker : iz3base { diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 1d81a1b15..527e73ae4 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -25,9 +25,7 @@ Revision History: #include "foci2.h" #include "iz3foci.h" -#ifndef WIN32 using namespace stl_ext; -#endif class iz3foci_impl : public iz3secondary { diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index c628ef32b..355c03817 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -445,6 +445,9 @@ namespace hash_space { : public hashtable,EqFun> { public: + + typedef Element value_type; + hash_set() : hashtable,EqFun>(7) {} }; diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 73eaab841..667d962d0 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -43,9 +43,7 @@ Revision History: -#ifndef WIN32 using namespace stl_ext; -#endif diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 35dc67bcd..0259f1b52 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -38,9 +38,7 @@ Revision History: #include "params.h" -#ifndef WIN32 using namespace stl_ext; -#endif std::ostream &operator <<(std::ostream &s, const iz3mgr::ast &a){ diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index e974a199b..4ef594cee 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -126,14 +126,6 @@ namespace hash_space { }; } -// 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 { diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index 31b375c0f..d530a3bc6 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -36,11 +36,8 @@ Revision History: #include"expr_abstract.h" -#ifndef WIN32 using namespace stl_ext; -#endif -#ifndef WIN32 // We promise not to use this for hash_map with range destructor namespace stl_ext { template <> @@ -51,7 +48,6 @@ namespace stl_ext { } }; } -#endif // TBD: algebraic data-types declarations will not be printed. diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 1eb4fcc84..6a150ad38 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -26,9 +26,7 @@ Revision History: #include "iz3proof_itp.h" -#ifndef WIN32 using namespace stl_ext; -#endif // #define INVARIANT_CHECKING diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 9eac5f040..7e0fa65d6 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -39,9 +39,7 @@ Revision History: #include //using std::vector; -#ifndef WIN32 using namespace stl_ext; -#endif diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index a85c9a1c5..a42c7034d 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -42,11 +42,7 @@ Revision History: #include //using std::vector; -#ifndef WIN32 using namespace stl_ext; -#endif - -#ifndef WIN32 /* This can introduce an address dependency if the range type of hash_map has a destructor. Since the code in this file is not used and only here for @@ -62,9 +58,6 @@ namespace stl_ext { }; } -#endif - - static int lemma_count = 0; #if 0 static int nll_lemma_count = 0; @@ -96,38 +89,12 @@ namespace hash_space { }; } -#ifdef WIN32 - -template <> inline -size_t stdext::hash_value(const Z3_resolvent& p) -{ - std::hash h; - return h(p); -} - - -namespace std { - template <> - class less { - public: - bool operator()(const Z3_resolvent &x, const Z3_resolvent &y) const { - 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; - } - }; -} - -#else bool operator==(const Z3_resolvent &x, const Z3_resolvent &y) { return x.proof == y.proof && x.pivot == y.pivot; } -#endif typedef std::vector ResolventAppSet; @@ -151,36 +118,6 @@ namespace hash_space { }; } -#ifdef WIN32 - -template <> inline -size_t stdext::hash_value(const non_local_lits& p) -{ - std::hash h; - return h(p); -} - -namespace std { - template <> - class less { - public: - bool operator()(const non_local_lits &x, const non_local_lits &y) const { - ResolventAppSet::const_iterator itx = x.proofs.begin(); - ResolventAppSet::const_iterator ity = y.proofs.begin(); - while(true){ - if(ity == y.proofs.end()) return false; - if(itx == x.proofs.end()) return true; - size_t xi = (size_t) *itx; - size_t yi = (size_t) *ity; - if(xi < yi) return true; - if(xi > yi) return false; - ++itx; ++ity; - } - } - }; -} - -#else bool operator==(const non_local_lits &x, const non_local_lits &y) { ResolventAppSet::const_iterator itx = x.proofs.begin(); @@ -194,8 +131,6 @@ bool operator==(const non_local_lits &x, const non_local_lits &y) { } -#endif - /* This translator goes directly from Z3 proofs to interpolatable proofs without an intermediate representation as an iz3proof. */