mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP)

Browse source
This commit is contained in:
Ken McMillan 2014-09-30 11:25:47 -07:00
parent 4c71e9479d
commit 4763532501
4 changed files with 36 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.h
View file

@ -54,7 +54,11 @@ Revision History:
// the case that each context only references a few expressions.
// Using a map instead of a vector for the literals can compress space
// consumption.
#ifdef SPARSE_MAP
#define USE_BOOL_VAR_VECTOR 0
#else
#define USE_BOOL_VAR_VECTOR 1
#endif
namespace smt {
@ -69,6 +73,7 @@ namespace smt {
std::string last_failure_as_string() const;
void set_progress_callback(progress_callback *callback);
protected:
ast_manager & m_manager;
smt_params & m_fparams;
@ -106,7 +111,7 @@ namespace smt {
// -----------------------------------
enode * m_true_enode;
enode * m_false_enode;
ptr_vector<enode> m_app2enode; // app -> enode
app2enode_t m_app2enode; // app -> enode
ptr_vector<enode> m_enodes;
plugin_manager<theory> m_theories; // mapping from theory_id -> theory
ptr_vector<theory> m_theory_set; // set of theories for fast traversal

6
src/smt/smt_enode.cpp
View file

@ -24,7 +24,7 @@ namespace smt {
/**
\brief Initialize an enode in the given memory position.
*/
enode * enode::init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner,
enode * enode::init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
@ -60,7 +60,7 @@ namespace smt {
return n;
}
enode * enode::mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner,
enode * enode::mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent) {
SASSERT(m.is_bool(owner) || !merge_tf);
@ -69,7 +69,7 @@ namespace smt {
return init(m, mem, app2enode, owner, generation, suppress_args, merge_tf, iscope_lvl, cgc_enabled, update_children_parent);
}
enode * enode::mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner) {
enode * enode::mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner) {
unsigned sz = get_enode_size(owner->get_num_args());
void * mem = alloc_svect(char, sz);
return init(m, mem, app2enode, owner, 0, false, false, 0, true, false);

29
src/smt/smt_enode.h
View file

@ -38,6 +38,29 @@ namespace smt {
}
};
/** \ brief Use sparse maps in SMT solver.
Define this to use hash maps rather than vectors over ast
nodes. This is useful in the case there are many solvers, each
referencing few nodes from a large ast manager. There is some
unknown performance penalty for this. */
// #define SPARSE_MAP
#ifndef SPARSE_MAP
typedef ptr_vector<enode> app2enode_t; // app -> enode
#else
class app2enode_t : public u_map<enode *> {
public:
void setx(unsigned x, enode *val, enode *def){
if(val == 0)
erase(x);
else
insert(x,val);
}
};
#endif
class tmp_enode;
/**
@ -115,7 +138,7 @@ namespace smt {
friend class tmp_enode;
static enode * init(ast_manager & m, void * mem, ptr_vector<enode> const & app2enode, app * owner,
static enode * init(ast_manager & m, void * mem, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
public:
@ -124,11 +147,11 @@ namespace smt {
return sizeof(enode) + num_args * sizeof(enode*);
}
static enode * mk(ast_manager & m, region & r, ptr_vector<enode> const & app2enode, app * owner,
static enode * mk(ast_manager & m, region & r, app2enode_t const & app2enode, app * owner,
unsigned generation, bool suppress_args, bool merge_tf, unsigned iscope_lvl,
bool cgc_enabled, bool update_children_parent);
static enode * mk_dummy(ast_manager & m, ptr_vector<enode> const & app2enode, app * owner);
static enode * mk_dummy(ast_manager & m, app2enode_t const & app2enode, app * owner);
static void del_dummy(enode * n) { dealloc_svect(reinterpret_cast<char*>(n)); }

2
src/util/map.h
View file

@ -131,7 +131,7 @@ public:
value const& get(key const& k, value const& default_value) const {
entry* e = find_core(k);
if (e) {
return e->m_value;
return e->get_data().m_value;
}
else {
return default_value;