mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt

Browse source
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-15 09:51:21 -08:00
commit 5edb651f61
5 changed files with 97 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/ast/ast_translation.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/format.h"
#include "ast/ast_translation.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
ast_translation::~ast_translation() {
reset_cache();
@ -47,7 +48,12 @@ void ast_translation::reset_cache() {
void ast_translation::cache(ast * s, ast * t) {
SASSERT(!m_cache.contains(s));
if (s->get_ref_count() > 1) {
if (m_insert_count > (1 << 17)) {
reset_cache();
m_insert_count = 0;
}
m_cache.insert(s, t);
++m_insert_count;
m_from_manager.inc_ref(s);
m_to_manager.inc_ref(t);
}
@ -76,9 +82,15 @@ void ast_translation::push_frame(ast * n) {
bool ast_translation::visit(ast * n) {
ast * r;
if (n->get_ref_count() > 1 && m_cache.find(n, r)) {
m_result_stack.push_back(r);
return true;
if (n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
m_result_stack.push_back(r);
++m_hit_count;
return true;
}
else {
++m_miss_count;
}
}
push_frame(n);
return false;
@ -187,20 +199,32 @@ ast * ast_translation::process(ast const * _n) {
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
++m_num_process;
if (m_num_process > (1 << 16)) {
reset_cache();
m_num_process = 0;
}
if (!visit(const_cast<ast*>(_n))) {
while (!m_frame_stack.empty()) {
loop:
++m_loop_count;
frame & fr = m_frame_stack.back();
ast * n = fr.m_n;
ast * r;
TRACE("ast_translation", tout << mk_ll_pp(n, m_from_manager, false) << "\n";);
if (fr.m_idx == 0 && n->get_ref_count() > 1 && m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
continue;
if (fr.m_idx == 0 && n->get_ref_count() > 1) {
if (m_cache.find(n, r)) {
SASSERT(m_result_stack.size() == fr.m_rpos);
m_result_stack.push_back(r);
m_extra_children_stack.shrink(fr.m_cpos);
m_frame_stack.pop_back();
TRACE("ast_translation", tout << "hit\n";);
m_hit_count++;
continue;
}
else {
m_miss_count++;
}
}
switch (n->get_kind()) {
case AST_VAR: {

16
src/ast/ast_translation.h
View file

@ -37,6 +37,11 @@ class ast_translation {
ptr_vector<ast> m_extra_children_stack; // for sort and func_decl, since they have nested AST in their parameters
ptr_vector<ast> m_result_stack;
obj_map<ast, ast*> m_cache;
unsigned m_loop_count;
unsigned m_hit_count;
unsigned m_miss_count;
unsigned m_insert_count;
unsigned m_num_process;
void cache(ast * s, ast * t);
void collect_decl_extra_children(decl * d);
@ -50,6 +55,11 @@ class ast_translation {
public:
ast_translation(ast_manager & from, ast_manager & to, bool copy_plugins = true) : m_from_manager(from), m_to_manager(to) {
m_loop_count = 0;
m_hit_count = 0;
m_miss_count = 0;
m_insert_count = 0;
m_num_process = 0;
if (&from != &to) {
if (copy_plugins)
m_to_manager.copy_families_plugins(m_from_manager);
@ -73,6 +83,12 @@ public:
void reset_cache();
void cleanup();
unsigned loop_count() const { return m_loop_count; }
unsigned hit_count() const { return m_hit_count; }
unsigned miss_count() const { return m_miss_count; }
unsigned insert_count() const { return m_insert_count; }
unsigned long long get_num_collision() const { return m_cache.get_num_collision(); }
};
// Translation with non-persistent cache.

18
src/sat/sat_config.cpp
View file

@ -87,24 +87,18 @@ namespace sat {
else
throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
if (p.lookahead_cube_cutoff() == symbol("depth")) {
if (p.lookahead_cube_cutoff() == symbol("depth"))
m_lookahead_cube_cutoff = depth_cutoff;
}
else if (p.lookahead_cube_cutoff() == symbol("freevars")) {
else if (p.lookahead_cube_cutoff() == symbol("freevars"))
m_lookahead_cube_cutoff = freevars_cutoff;
}
else if (p.lookahead_cube_cutoff() == symbol("psat")) {
else if (p.lookahead_cube_cutoff() == symbol("psat"))
m_lookahead_cube_cutoff = psat_cutoff;
}
else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) {
else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars"))
m_lookahead_cube_cutoff = adaptive_freevars_cutoff;
}
else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) {
else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat"))
m_lookahead_cube_cutoff = adaptive_psat_cutoff;
}
else {
else
throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'");
}
m_lookahead_cube_fraction = p.lookahead_cube_fraction();
m_lookahead_cube_depth = p.lookahead_cube_depth();
m_lookahead_cube_freevars = p.lookahead_cube_freevars();

38
src/util/hashtable.h
View file

@ -24,11 +24,12 @@ Revision History:
#include<limits.h>
#include "util/memory_manager.h"
#include "util/hash.h"
#include "util/vector.h"
#define DEFAULT_HASHTABLE_INITIAL_CAPACITY 8
#define SMALL_TABLE_CAPACITY 64
// #define HASHTABLE_STATISTICS
// #define HASHTABLE_STATISTICS
#ifdef HASHTABLE_STATISTICS
#define HS_CODE(CODE) { CODE }
@ -375,8 +376,7 @@ public:
} ((void) 0)
void insert(data && e) {
if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
if (((m_size + m_num_deleted) << 2) > (m_capacity * 3)) {
expand_table();
}
unsigned hash = get_hash(e);
@ -488,7 +488,9 @@ public:
else if (curr->is_free()) { \
return 0; \
} \
HS_CODE(const_cast<core_hashtable*>(this)->m_st_collision++;); \
else { \
HS_CODE(const_cast<core_hashtable*>(this)->m_st_collision++;); \
} \
} ((void) 0)
entry * find_core(data const & e) const {
@ -655,7 +657,33 @@ public:
unsigned long long get_num_collision() const { return 0; }
#endif
#define COLL_LOOP_BODY() { \
if (curr->is_used()) { \
if (curr->get_hash() == hash && equals(curr->get_data(), e)) return; \
collisions.push_back(curr->get_data()); \
continue; \
} \
else if (curr->is_free()) { \
continue; \
} \
collisions.push_back(curr->get_data()); \
} ((void) 0);
void get_collisions(data const& e, vector<data>& collisions) {
unsigned hash = get_hash(e);
unsigned mask = m_capacity - 1;
unsigned idx = hash & mask;
entry * begin = m_table + idx;
entry * end = m_table + m_capacity;
entry * curr = begin;
for (; curr != end; ++curr) {
COLL_LOOP_BODY();
}
for (curr = m_table; curr != begin; ++curr) {
COLL_LOOP_BODY();
}
}
};
template<typename T, typename HashProc, typename EqProc>

8
src/util/obj_hashtable.h
View file

@ -204,6 +204,14 @@ public:
unsigned long long get_num_collision() const { return m_table.get_num_collision(); }
void get_collisions(Key * k, vector<Key*>& collisions) {
vector<key_data> cs;
m_table.get_collisions(key_data(k), cs);
for (key_data const& kd : cs) {
collisions.push_back(kd.m_key);
}
}
void swap(obj_map & other) {
m_table.swap(other.m_table);
}