mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
use new hashtable implementation in windows
This commit is contained in:
parent
4f06b347b3
commit
acf4ad0ab6
|
@ -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;
|
||||
|
||||
|
|
|
@ -25,9 +25,7 @@ Revision History:
|
|||
#include <map>
|
||||
|
||||
// make hash_map and hash_set available
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
namespace Duality {
|
||||
|
||||
|
|
|
@ -1955,7 +1955,7 @@ namespace Duality {
|
|||
}
|
||||
if(update_count == 0){
|
||||
if(was_sat)
|
||||
throw Incompleteness();
|
||||
throw "Help!";
|
||||
reporter->Message("backtracked without learning");
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1401,14 +1401,6 @@ namespace hash_space {
|
|||
};
|
||||
}
|
||||
|
||||
// to make Duality::ast hashable in windows
|
||||
#ifdef WIN32
|
||||
template <> inline
|
||||
size_t stdext::hash_value<Duality::ast >(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<Duality::func_decl >(const Duality::func_decl& s)
|
||||
{
|
||||
return s.raw()->get_id();
|
||||
}
|
||||
#endif
|
||||
|
||||
// to make Duality::func_decl usable in ordered collections
|
||||
namespace std {
|
||||
|
|
|
@ -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){
|
||||
|
|
|
@ -36,9 +36,7 @@ Revision History:
|
|||
#include <iterator>
|
||||
|
||||
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
struct iz3checker : iz3base {
|
||||
|
||||
|
|
|
@ -25,9 +25,7 @@ Revision History:
|
|||
#include "foci2.h"
|
||||
#include "iz3foci.h"
|
||||
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
class iz3foci_impl : public iz3secondary {
|
||||
|
||||
|
|
|
@ -445,6 +445,9 @@ namespace hash_space {
|
|||
: public hashtable<Element,Element,HashFun,identity<Element>,EqFun> {
|
||||
|
||||
public:
|
||||
|
||||
typedef Element value_type;
|
||||
|
||||
hash_set()
|
||||
: hashtable<Element,Element,HashFun,identity<Element>,EqFun>(7) {}
|
||||
};
|
||||
|
|
|
@ -43,9 +43,7 @@ Revision History:
|
|||
|
||||
|
||||
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -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){
|
||||
|
|
|
@ -126,14 +126,6 @@ namespace hash_space {
|
|||
};
|
||||
}
|
||||
|
||||
// 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 {
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -26,9 +26,7 @@ Revision History:
|
|||
|
||||
#include "iz3proof_itp.h"
|
||||
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
// #define INVARIANT_CHECKING
|
||||
|
||||
|
|
|
@ -39,9 +39,7 @@ Revision History:
|
|||
#include <set>
|
||||
|
||||
//using std::vector;
|
||||
#ifndef WIN32
|
||||
using namespace stl_ext;
|
||||
#endif
|
||||
|
||||
|
||||
|
||||
|
|
|
@ -42,11 +42,7 @@ Revision History:
|
|||
#include <set>
|
||||
|
||||
//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<Z3_resolvent >(const Z3_resolvent& p)
|
||||
{
|
||||
std::hash<Z3_resolvent> h;
|
||||
return h(p);
|
||||
}
|
||||
|
||||
|
||||
namespace std {
|
||||
template <>
|
||||
class less<Z3_resolvent > {
|
||||
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<Z3_resolvent *> ResolventAppSet;
|
||||
|
||||
|
@ -151,36 +118,6 @@ namespace hash_space {
|
|||
};
|
||||
}
|
||||
|
||||
#ifdef WIN32
|
||||
|
||||
template <> inline
|
||||
size_t stdext::hash_value<non_local_lits >(const non_local_lits& p)
|
||||
{
|
||||
std::hash<non_local_lits> h;
|
||||
return h(p);
|
||||
}
|
||||
|
||||
namespace std {
|
||||
template <>
|
||||
class less<non_local_lits > {
|
||||
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. */
|
||||
|
||||
|
|
Loading…
Reference in a new issue