mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-03-11 00:45:09 -07:00
commit 695ce643f5
16 changed files with 103 additions and 58 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/model/func_interp.cpp
View file

@ -276,8 +276,8 @@ expr * func_interp::get_interp() const {
return r;
}
func_interp * func_interp::translate(ast_translation & translator) const {
func_interp * new_fi = alloc(func_interp, m_manager, m_arity);
func_interp * func_interp::translate(ast_translation & translator) const {
func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
ptr_vector<func_entry>::const_iterator it = m_entries.begin();
ptr_vector<func_entry>::const_iterator end = m_entries.end();

1
src/model/model.cpp
View file

@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) {
void model::register_decl(func_decl * d, func_interp * fi) {
SASSERT(d->get_arity() > 0);
SASSERT(&fi->m() == &m_manager);
decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
if (entry->get_data().m_value == 0) {
// new entry

6
src/sat/sat_solver.h
View file

@ -89,7 +89,7 @@ namespace sat {
clause_vector m_learned;
unsigned m_num_frozen;
vector<watch_list> m_watches;
svector<lbool> m_assignment;
char_vector m_assignment;
svector<justification> m_justification;
svector<char> m_decision;
svector<char> m_mark;
@ -200,8 +200,8 @@ namespace sat {
bool is_external(bool_var v) const { return m_external[v] != 0; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
lbool value(literal l) const { return m_assignment[l.index()]; }
lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; }
void assign(literal l, justification j) {

22
src/smt/params/dyn_ack_params.cpp
View file

@ -17,16 +17,14 @@ Revision History:
--*/
#include"dyn_ack_params.h"
#include"smt_params_helper.hpp"
#if 0
void dyn_ack_params::register_params(ini_params & p) {
p.register_int_param("dack", 0, 2, reinterpret_cast<int&>(m_dack),
"0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution.");
p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities");
p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded");
p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict");
p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict).");
p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay);
}
#endif
void dyn_ack_params::updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_dack = static_cast<dyn_ack_strategy>(p.dack());
m_dack_eq = p.dack_eq();
m_dack_factor = p.dack_factor();
m_dack_threshold = p.dack_threshold();
m_dack_gc = p.dack_gc();
m_dack_gc_inv_decay = p.dack_gc_inv_decay();
}

6
src/smt/params/dyn_ack_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef _DYN_ACK_PARAMS_H_
#define _DYN_ACK_PARAMS_H_
#include"params.h"
enum dyn_ack_strategy {
DACK_DISABLED,
DACK_ROOT, // congruence is the root of the conflict
@ -34,15 +36,17 @@ struct dyn_ack_params {
double m_dack_gc_inv_decay;
public:
dyn_ack_params():
dyn_ack_params(params_ref const & p = params_ref()) :
m_dack(DACK_ROOT),
m_dack_eq(false),
m_dack_factor(0.1),
m_dack_threshold(10),
m_dack_gc(2000),
m_dack_gc_inv_decay(0.8) {
updt_params(p);
}
void updt_params(params_ref const & _p);
};

1
src/smt/params/smt_params.cpp
View file

@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
void smt_params::updt_params(params_ref const & p) {
preprocessor_params::updt_params(p);
dyn_ack_params::updt_params(p);
qi_params::updt_params(p);
theory_arith_params::updt_params(p);
theory_bv_params::updt_params(p);

8
src/smt/params/smt_params_helper.pyg
View file

@ -45,5 +45,11 @@ def_module_params(module_name='smt',
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory')
('array.extensional', BOOL, True, 'extensional array theory'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
))

10
src/util/bit_vector.cpp
View file

@ -25,13 +25,11 @@ Revision History:
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
void bit_vector::expand_to(unsigned new_capacity) {
unsigned * new_data = alloc_svect(unsigned, new_capacity);
memset(new_data, 0, new_capacity * sizeof(unsigned));
if (m_capacity > 0) {
memcpy(new_data, m_data, m_capacity * sizeof(unsigned));
dealloc_svect(m_data);
if (m_data) {
m_data = (unsigned*)memory::reallocate(m_data, new_capacity * sizeof(unsigned));
} else {
m_data = alloc_svect(unsigned, new_capacity);
}
m_data = new_data;
m_capacity = new_capacity;
}

4
src/util/bit_vector.h
View file

@ -87,9 +87,7 @@ public:
}
~bit_vector() {
if (m_data) {
dealloc_svect(m_data);
}
dealloc_svect(m_data);
}
void reset() {

42
src/util/memory_manager.cpp
View file

@ -252,6 +252,24 @@ void * memory::allocate(size_t s) {
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
void* memory::reallocate(void *p, size_t s) {
size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
size_t sz = *sz_p;
void *real_p = reinterpret_cast<void*>(sz_p);
s = s + sizeof(size_t); // we allocate an extra field!
g_memory_thread_alloc_size += s - sz;
if (g_memory_thread_alloc_size > SYNCH_THRESHOLD) {
synchronize_counters(true);
}
void *r = realloc(real_p, s);
if (r == 0)
throw_out_of_memory();
*(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
#else
// ==================================
// ==================================
@ -292,5 +310,29 @@ void * memory::allocate(size_t s) {
*(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
void* memory::reallocate(void *p, size_t s) {
size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
size_t sz = *sz_p;
void * real_p = reinterpret_cast<void*>(sz_p);
s = s + sizeof(size_t); // we allocate an extra field!
bool out_of_mem = false;
#pragma omp critical (z3_memory_manager)
{
g_memory_alloc_size += s - sz;
if (g_memory_alloc_size > g_memory_max_used_size)
g_memory_max_used_size = g_memory_alloc_size;
if (g_memory_max_size != 0 && g_memory_alloc_size > g_memory_max_size)
out_of_mem = true;
}
if (out_of_mem)
throw_out_of_memory();
void *r = realloc(real_p, s);
if (r == 0)
throw_out_of_memory();
*(static_cast<size_t*>(r)) = s;
return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
}
#endif

9
src/util/memory_manager.h
View file

@ -34,7 +34,7 @@ Revision History:
# define GCC_RET_NON_NULL
# endif
# define ALLOC_ATTR __attribute__((malloc)) GCC_RET_NON_NULL
#elif defined(_WINDOWS) && (VisualStudioVersion >= 13)
#elif defined(_WINDOWS)
# define ALLOC_ATTR __declspec(restrict)
#else
# define ALLOC_ATTR
@ -57,10 +57,11 @@ public:
static void display_max_usage(std::ostream& os);
static void display_i_max_usage(std::ostream& os);
static void deallocate(void* p);
static void* allocate(size_t s) ALLOC_ATTR;
static ALLOC_ATTR void* allocate(size_t s);
static ALLOC_ATTR void* reallocate(void *p, size_t s);
#if _DEBUG
static void deallocate(char const* file, int line, void* p);
static void* allocate(char const* file, int line, char const* obj, size_t s) ALLOC_ATTR;
static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s);
#endif
static unsigned long long get_allocation_size();
static unsigned long long get_max_used_memory();
@ -95,7 +96,7 @@ void dealloc(T * ptr) {
#endif
template<typename T>
T * alloc_vect(unsigned sz) ALLOC_ATTR;
ALLOC_ATTR T * alloc_vect(unsigned sz);
template<typename T>
T * alloc_vect(unsigned sz) {

12
src/util/vector.h
View file

@ -71,18 +71,12 @@ class vector {
SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;
SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
SZ size = reinterpret_cast<SZ *>(m_data)[SIZE_IDX];
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
throw default_exception("Overflow encountered when expanding vector");
}
SZ * mem = reinterpret_cast<SZ*>(memory::allocate(new_capacity_T));
*mem = new_capacity;
mem ++;
*mem = size;
mem++;
memcpy(mem, m_data, size * sizeof(T));
free_memory();
m_data = reinterpret_cast<T *>(mem);
SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
*mem = new_capacity;
m_data = reinterpret_cast<T *>(mem + 2);
}
}