mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-11 13:44:30 -07:00
parent 18ea547cea cb31a294c8
commit a054b099c1
13 changed files with 39 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitattributes vendored Normal file
View file

@ -0,0 +1 @@
src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf

21
src/math/realclosure/realclosure.cpp
View file

@ -660,8 +660,7 @@ namespace realclosure {
return; // interval was already saved.
to_restore.push_back(v);
inc_ref(v);
void * mem = allocator().allocate(sizeof(mpbqi));
v->m_old_interval = new (mem) mpbqi();
v->m_old_interval = new (allocator()) mpbqi();
set_interval(*(v->m_old_interval), v->m_interval);
}
void save_interval(value * v) {
@ -1237,8 +1236,7 @@ namespace realclosure {
}
sign_condition * mk_sign_condition(unsigned qidx, int sign, sign_condition * prev_sc) {
void * mem = allocator().allocate(sizeof(sign_condition));
return new (mem) sign_condition(qidx, sign, prev_sc);
return new (allocator()) sign_condition(qidx, sign, prev_sc);
}
/**
@ -1246,7 +1244,7 @@ namespace realclosure {
This method does not set the interval. It remains (-oo, oo)
*/
rational_function_value * mk_rational_function_value_core(extension * ext, unsigned num_sz, value * const * num, unsigned den_sz, value * const * den) {
rational_function_value * r = alloc(rational_function_value, ext);
rational_function_value * r = new (allocator()) rational_function_value(ext);
inc_ref(ext);
set_p(r->num(), num_sz, num);
if (ext->is_algebraic()) {
@ -1283,7 +1281,7 @@ namespace realclosure {
*/
void mk_infinitesimal(symbol const & n, symbol const & pp_n, numeral & r) {
unsigned idx = next_infinitesimal_idx();
infinitesimal * eps = alloc(infinitesimal, idx, n, pp_n);
infinitesimal * eps = new (allocator()) infinitesimal(idx, n, pp_n);
m_extensions[extension::INFINITESIMAL].push_back(eps);
set_lower(eps->interval(), mpbq(0));
@ -1335,7 +1333,7 @@ namespace realclosure {
void mk_transcendental(symbol const & n, symbol const & pp_n, mk_interval & proc, numeral & r) {
unsigned idx = next_transcendental_idx();
transcendental * t = alloc(transcendental, idx, n, pp_n, proc);
transcendental * t = new (allocator()) transcendental(idx, n, pp_n, proc);
m_extensions[extension::TRANSCENDENTAL].push_back(t);
while (contains_zero(t->interval())) {
@ -1798,8 +1796,7 @@ namespace realclosure {
M and scs will be empty after this operation.
*/
sign_det * mk_sign_det(mpz_matrix & M_s, scoped_polynomial_seq const & prs, int_buffer const & taqrs, scoped_polynomial_seq const & qs, scoped_sign_conditions & scs) {
void * mem = allocator().allocate(sizeof(sign_det));
sign_det * r = new (mem) sign_det();
sign_det * r = new (allocator()) sign_det();
r->M_s.swap(M_s);
set_array_p(r->m_prs, prs);
r->m_taqrs.set(allocator(), taqrs.size(), taqrs.c_ptr());
@ -1814,8 +1811,7 @@ namespace realclosure {
*/
algebraic * mk_algebraic(unsigned p_sz, value * const * p, mpbqi const & interval, mpbqi const & iso_interval, sign_det * sd, unsigned sc_idx) {
unsigned idx = next_algebraic_idx();
void * mem = allocator().allocate(sizeof(algebraic));
algebraic * r = new (mem) algebraic(idx);
algebraic * r = new (allocator()) algebraic(idx);
m_extensions[extension::ALGEBRAIC].push_back(r);
set_p(r->m_p, p_sz, p);
@ -2561,8 +2557,7 @@ namespace realclosure {
}
rational_value * mk_rational() {
void * mem = allocator().allocate(sizeof(rational_value));
return new (mem) rational_value();
return new (allocator()) rational_value();
}
/**

6
src/muz_qe/dl_instruction.cpp
View file

@ -452,7 +452,7 @@ namespace datalog {
class instr_filter_identical : public instruction {
typedef vector<unsigned> column_vector;
typedef unsigned_vector column_vector;
reg_idx m_reg;
column_vector m_cols;
public:
@ -651,7 +651,7 @@ namespace datalog {
class instr_project_rename : public instruction {
typedef vector<unsigned> column_vector;
typedef unsigned_vector column_vector;
bool m_projection;
reg_idx m_src;
column_vector m_cols;
@ -831,7 +831,7 @@ namespace datalog {
class instr_filter_by_negation : public instruction {
typedef vector<unsigned> column_vector;
typedef unsigned_vector column_vector;
reg_idx m_tgt;
reg_idx m_neg_rel;
column_vector m_cols1;

5
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -583,11 +583,12 @@ namespace datalog {
}
rule_set * res = alloc(rule_set, m_context);
if (!transform_rules(source, *res)) {
if (transform_rules(source, *res)) {
res->inherit_predicates(source);
} else {
dealloc(res);
res = 0;
}
res->inherit_predicates(source);
return res;
}

14
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -667,7 +667,7 @@ namespace datalog {
return et->get_data().m_value;
}
void mk_rule_inliner::add_rule(rule* r, unsigned i) {
void mk_rule_inliner::add_rule(rule_set const& source, rule* r, unsigned i) {
svector<bool>& can_remove = m_head_visitor.can_remove();
svector<bool>& can_expand = m_head_visitor.can_expand();
app* head = r->get_head();
@ -676,7 +676,7 @@ namespace datalog {
m_head_index.insert(head);
m_pinned.push_back(r);
if (m_context.get_rules().is_output_predicate(headd) ||
if (source.is_output_predicate(headd) ||
m_preds_with_facts.contains(headd)) {
can_remove.set(i, false);
TRACE("dl", output_predicate(m_context, head, tout << "cannot remove: " << i << " "); tout << "\n";);
@ -692,7 +692,7 @@ namespace datalog {
tl_sz == 1
&& r->get_positive_tail_size() == 1
&& !m_preds_with_facts.contains(r->get_decl(0))
&& !m_context.get_rules().is_output_predicate(r->get_decl(0));
&& !source.is_output_predicate(r->get_decl(0));
can_expand.set(i, can_exp);
}
@ -709,7 +709,7 @@ namespace datalog {
#define PRT(_x_) ((_x_)?"T":"F")
bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
bool done_something = false;
unsigned sz = rules->get_num_rules();
@ -731,7 +731,7 @@ namespace datalog {
svector<bool>& can_expand = m_head_visitor.can_expand();
for (unsigned i = 0; i < sz; ++i) {
add_rule(acc[i].get(), i);
add_rule(source, acc[i].get(), i);
}
// initialize substitution.
@ -808,7 +808,7 @@ namespace datalog {
TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
del_rule(r, i);
add_rule(rl_res.get(), i);
add_rule(source, rl_res.get(), i);
r = rl_res;
@ -875,7 +875,7 @@ namespace datalog {
TRACE("dl", res->display(tout << "after eager inlining\n"););
}
if (m_context.get_params().inline_linear() && inline_linear(res)) {
if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
something_done = true;
}

4
src/muz_qe/dl_mk_rule_inliner.h
View file

@ -172,9 +172,9 @@ namespace datalog {
/**
Inline predicates that are known to not be join-points.
*/
bool inline_linear(scoped_ptr<rule_set>& rules);
bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
void add_rule(rule* r, unsigned i);
void add_rule(rule_set const& rule_set, rule* r, unsigned i);
void del_rule(rule* r, unsigned i);
public:

6
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -429,7 +429,7 @@ namespace datalog {
m_modified = true;
}
void mk_similarity_compressor::process_class(rule_vector::iterator first,
void mk_similarity_compressor::process_class(rule_set const& source, rule_vector::iterator first,
rule_vector::iterator after_last) {
SASSERT(first!=after_last);
//remove duplicates
@ -487,7 +487,7 @@ namespace datalog {
//TODO: compress also rules with pairs (or tuples) of equal constants
#if 1
if (const_cnt>0) {
if (const_cnt>0 && !source.is_output_predicate((*first)->get_decl())) {
unsigned rule_cnt = static_cast<unsigned>(after_last-first);
if (rule_cnt>m_threshold_count) {
merge_class(first, after_last);
@ -521,7 +521,7 @@ namespace datalog {
rule_vector::iterator prev = it;
++it;
if (it==end || rough_compare(*prev, *it)!=0) {
process_class(cl_begin, it);
process_class(source, cl_begin, it);
cl_begin = it;
}
}

2
src/muz_qe/dl_mk_similarity_compressor.h
View file

@ -63,7 +63,7 @@ namespace datalog {
ast_ref_vector m_pinned;
void merge_class(rule_vector::iterator first, rule_vector::iterator after_last);
void process_class(rule_vector::iterator first, rule_vector::iterator after_last);
void process_class(rule_set const& source, rule_vector::iterator first, rule_vector::iterator after_last);
void reset();
public:

10
src/muz_qe/dl_rule_set.cpp
View file

@ -332,15 +332,12 @@ namespace datalog {
void rule_set::inherit_predicates(rule_set const& other) {
m_refs.append(other.m_refs);
SASSERT(m_refs.size() < 1000);
set_union(m_output_preds, other.m_output_preds);
{
obj_map<func_decl, func_decl*>::iterator it = other.m_orig2pred.begin();
obj_map<func_decl, func_decl*>::iterator end = other.m_orig2pred.end();
for (; it != end; ++it) {
m_orig2pred.insert(it->m_key, it->m_value);
m_refs.push_back(it->m_key);
m_refs.push_back(it->m_value);
}
}
{
@ -348,8 +345,6 @@ namespace datalog {
obj_map<func_decl, func_decl*>::iterator end = other.m_pred2orig.end();
for (; it != end; ++it) {
m_pred2orig.insert(it->m_key, it->m_value);
m_refs.push_back(it->m_key);
m_refs.push_back(it->m_value);
}
}
}
@ -515,6 +510,11 @@ namespace datalog {
void rule_set::display(std::ostream & out) const {
out << "; rule count: " << get_num_rules() << "\n";
out << "; predicate count: " << m_head2rules.size() << "\n";
func_decl_set::iterator pit = m_output_preds.begin();
func_decl_set::iterator pend = m_output_preds.end();
for (; pit != pend; ++pit) {
out << "; output: " << (*pit)->get_name() << '\n';
}
decl2rules::iterator it = m_head2rules.begin();
decl2rules::iterator end = m_head2rules.end();
for (; it != end; ++it) {

2
src/muz_qe/rel_context.cpp
View file

@ -254,6 +254,8 @@ namespace datalog {
m_context.transform_rules(alloc(mk_magic_sets, m_context, query_pred));
}
query_pred = m_context.get_rules().get_pred(query_pred);
lbool res = saturate();
if (res != l_undef) {

2
src/test/rcf.cpp
View file

@ -137,7 +137,6 @@ static void tst_lin_indep(unsigned m, unsigned n, int _A[], unsigned ex_sz, unsi
r.resize(A.n());
scoped_mpz_matrix B(mm);
mm.linear_independent_rows(A, r.c_ptr(), B);
SASSERT(r.size() == ex_sz);
for (unsigned i = 0; i < ex_sz; i++) {
SASSERT(r[i] == ex_r[i]);
}
@ -164,7 +163,6 @@ void tst_rcf() {
enable_trace("rcf_clean");
enable_trace("rcf_clean_bug");
tst_denominators();
return;
tst1();
tst2();
{ int A[] = {0, 1, 1, 1, 0, 1, 1, 1, -1}; int c[] = {10, 4, -4}; int b[] = {-2, 4, 6}; tst_solve(3, A, b, c, true); }

2
src/util/array.h
View file

@ -122,7 +122,7 @@ public:
if (m_data) {
if (CallDestructors)
destroy_elements();
a.deallocate(size(), raw_ptr());
a.deallocate(space(size()), raw_ptr());
m_data = 0;
}
}

5
src/util/small_object_allocator.h
View file

@ -21,6 +21,7 @@ Revision History:
#define _SMALL_OBJECT_ALLOCATOR_H_
#include"machine.h"
#include"debug.h"
class small_object_allocator {
static const unsigned CHUNK_SIZE = (8192 - sizeof(void*)*2);
@ -52,8 +53,8 @@ public:
inline void * operator new(size_t s, small_object_allocator & r) { return r.allocate(s); }
inline void * operator new[](size_t s, small_object_allocator & r) { return r.allocate(s); }
inline void operator delete(void * p, size_t s, small_object_allocator & r) { r.deallocate(s,p); }
inline void operator delete[](void * p, size_t s, small_object_allocator & r) { r.deallocate(s,p); }
inline void operator delete(void * p, small_object_allocator & r) { UNREACHABLE(); }
inline void operator delete[](void * p, small_object_allocator & r) { UNREACHABLE(); }
#endif /* _SMALL_OBJECT_ALLOCATOR_H_ */