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-16 13:55:00 -07:00
parent de5f1ebe9f 51d3db8105
commit 7e4c9a7f75
7 changed files with 22 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -2755,7 +2755,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
app const * cls = to_app(f1);
unsigned num_args = cls->get_num_args();
#ifdef Z3DEBUG
vector<bool> found;
svector<bool> found;
#endif
for (unsigned i = 0; i < num_args; i++) {
expr * lit = cls->get_arg(i);

21
src/muz_qe/dl_compiler.cpp
View file

@ -803,17 +803,15 @@ namespace datalog {
context& m_context;
item_set & m_removed;
svector<T> m_stack;
ast_mark m_stack_content;
ast_mark m_visited;
void traverse(T v) {
SASSERT(!m_stack_content.is_marked(v));
if(m_visited.is_marked(v) || m_removed.contains(v)) {
SASSERT(!m_visited.is_marked(v));
if (m_removed.contains(v)) {
return;
}
m_stack.push_back(v);
m_stack_content.mark(v, true);
m_visited.mark(v, true);
const item_set & deps = m_deps.get_deps(v);
@ -821,33 +819,34 @@ namespace datalog {
item_set::iterator end = deps.end();
for(; it!=end; ++it) {
T d = *it;
if(m_stack_content.is_marked(d)) {
if (m_visited.is_marked(d)) {
//TODO: find the best vertex to remove in the cycle
remove_from_stack();
break;
continue;
}
traverse(d);
}
SASSERT(m_stack.back()==v);
m_stack.pop_back();
m_stack_content.mark(v, false);
m_visited.mark(v, false);
}
void remove_from_stack() {
for (unsigned i = 0; i < m_stack.size(); ++i) {
func_decl* p = m_stack[i];
rule_vector const& rules = m_rules.get_predicate_rules(p);
unsigned stratum = m_rules.get_predicate_strat(p);
if (m_context.has_facts(p)) {
m_removed.insert(p);
return;
}
rule_vector const& rules = m_rules.get_predicate_rules(p);
unsigned stratum = m_rules.get_predicate_strat(p);
for (unsigned j = 0; j < rules.size(); ++j) {
rule const& r = *rules[j];
bool ok = true;
for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
ok &= m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
ok = m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
}
if (ok) {
m_removed.insert(p);
@ -858,8 +857,8 @@ namespace datalog {
// nothing was found.
m_removed.insert(m_stack.back());
}
public:
cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed)
: m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }

13
src/muz_qe/dl_sparse_table.cpp
View file

@ -1022,19 +1022,16 @@ namespace datalog {
class sparse_table_plugin::rename_fn : public convenient_table_rename_fn {
const unsigned m_cycle_len;
const unsigned m_col_cnt;
unsigned_vector m_out_of_cycle;
public:
rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle)
: convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle),
m_cycle_len(permutation_cycle_len), m_col_cnt(orig_sig.size()) {
: convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) {
SASSERT(permutation_cycle_len>=2);
idx_set cycle_cols;
for (unsigned i=0; i<m_cycle_len; i++) {
for (unsigned i=0; i < permutation_cycle_len; ++i) {
cycle_cols.insert(permutation_cycle[i]);
}
for (unsigned i=0; i<m_col_cnt; i++) {
for (unsigned i=0; i < orig_sig.size(); ++i) {
if (!cycle_cols.contains(i)) {
m_out_of_cycle.push_back(i);
}
@ -1045,10 +1042,10 @@ namespace datalog {
const sparse_table::column_layout & src_layout,
const sparse_table::column_layout & tgt_layout) {
for (unsigned i=1; i<m_cycle_len; i++) {
for (unsigned i=1; i < m_cycle.size(); ++i) {
tgt_layout.set(tgt, m_cycle[i-1], src_layout.get(src, m_cycle[i]));
}
tgt_layout.set(tgt, m_cycle[m_cycle_len-1], src_layout.get(src, m_cycle[0]));
tgt_layout.set(tgt, m_cycle[m_cycle.size()-1], src_layout.get(src, m_cycle[0]));
unsigned_vector::const_iterator it = m_out_of_cycle.begin();
unsigned_vector::const_iterator end = m_out_of_cycle.end();

3
src/muz_qe/pdr_prop_solver.cpp
View file

@ -145,7 +145,8 @@ namespace pdr {
rational two(2);
for (unsigned j = 0; j < bv_size; ++j) {
parameter p(j);
expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
//expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c));
if ((r % two).is_zero()) {
e = m.mk_not(e);
}

6
src/util/bit_vector.cpp
View file

@ -208,8 +208,8 @@ void bit_vector::display(std::ostream & out) const {
void fr_bit_vector::reset() {
unsigned sz = size();
vector<unsigned>::const_iterator it = m_one_idxs.begin();
vector<unsigned>::const_iterator end = m_one_idxs.end();
unsigned_vector::const_iterator it = m_one_idxs.begin();
unsigned_vector::const_iterator end = m_one_idxs.end();
for (; it != end; ++it) {
unsigned idx = *it;
if (idx < sz)
@ -217,5 +217,3 @@ void fr_bit_vector::reset() {
}
m_one_idxs.reset();
}

2
src/util/bit_vector.h
View file

@ -204,7 +204,7 @@ inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {
This class should be used if the reset is frequently called.
*/
class fr_bit_vector : private bit_vector {
svector<unsigned> m_one_idxs;
unsigned_vector m_one_idxs;
public:
void reset();

2
src/util/mpff.h
View file

@ -107,7 +107,7 @@ class mpff_manager {
unsigned m_precision; //!< Number of words in the significand. Must be an even number.
unsigned m_precision_bits; //!< Number of bits in the significand. Must be 32*m_precision.
vector<unsigned> m_significands; //!< Array containing all significands.
unsigned_vector m_significands; //!< Array containing all significands.
unsigned m_capacity; //!< Number of significands that can be stored in m_significands.
bool m_to_plus_inf; //!< If True, then round to plus infinity, otherwise to minus infinity
id_gen m_id_gen;