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

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 11:15:34 -07:00
parent 8dac9b7b94
commit b66360d0b5
5 changed files with 84 additions and 107 deletions

1
src/math/simplex/model_based_opt.cpp
View file

@ -1088,6 +1088,7 @@ namespace opt {
if (D.is_zero()) {
throw default_exception("modulo 0 is not defined");
}
if (D.is_neg()) D = abs(D);
TRACE("opt1", display(tout << "lcm: " << D << " x: v" << x << " tableau\n"););
rational val_x = m_var2value[x];
rational u = mod(val_x, D);

138
src/muz/rel/dl_base.cpp
View file

@ -39,21 +39,19 @@ namespace datalog {
}
void dealloc_ptr_vector_content(ptr_vector<relation_base> & v) {
ptr_vector<relation_base>::iterator it = v.begin();
ptr_vector<relation_base>::iterator end = v.end();
for(; it!=end; ++it) {
(*it)->deallocate();
for (auto& r : v) {
r->deallocate();
}
}
void get_renaming_args(const unsigned_vector & map, const relation_signature & orig_sig,
expr_ref_vector & renaming_arg) {
expr_ref_vector & renaming_arg) {
ast_manager & m = renaming_arg.get_manager();
unsigned sz = map.size();
unsigned ofs = sz-1;
renaming_arg.resize(sz, static_cast<expr *>(nullptr));
for(unsigned i=0; i<sz; i++) {
if(map[i]!=UINT_MAX) {
for (unsigned i = 0; i < sz; i++) {
if (map[i] != UINT_MAX) {
renaming_arg.set(ofs-i, m.mk_var(map[i], orig_sig[i]));
}
}
@ -74,13 +72,13 @@ namespace datalog {
#endif
void relation_signature::output(ast_manager & m, std::ostream & out) const {
unsigned sz=size();
out<<"(";
for(unsigned i=0; i<sz; i++) {
if(i) { out<<","; }
unsigned sz = size();
out << "(";
for (unsigned i = 0; i < sz; i++) {
if (i != 0) out << ",";
out << mk_pp((*this)[i], m);
}
out<<")";
out << ")";
}
@ -90,8 +88,8 @@ namespace datalog {
ast_manager & m = get_plugin().get_ast_manager();
app_ref bottom_ref(m.mk_false(), m);
scoped_ptr<relation_mutator_fn> reset_fn = get_manager().mk_filter_interpreted_fn(*this, bottom_ref);
if(!reset_fn) {
NOT_IMPLEMENTED_YET();
if (!reset_fn) {
throw default_exception("filter function does not exist");
}
(*reset_fn)(*this);
}
@ -106,16 +104,16 @@ namespace datalog {
unsigned s2sz=s2.size();
unsigned s1first_func=s1sz-s1.functional_columns();
unsigned s2first_func=s2sz-s2.functional_columns();
for(unsigned i=0; i<s1first_func; i++) {
for (unsigned i=0; i<s1first_func; i++) {
result.push_back(s1[i]);
}
for(unsigned i=0; i<s2first_func; i++) {
for (unsigned i=0; i<s2first_func; i++) {
result.push_back(s2[i]);
}
for(unsigned i=s1first_func; i<s1sz; i++) {
for (unsigned i=s1first_func; i<s1sz; i++) {
result.push_back(s1[i]);
}
for(unsigned i=s2first_func; i<s2sz; i++) {
for (unsigned i=s2first_func; i<s2sz; i++) {
result.push_back(s2[i]);
}
result.set_functional_columns(s1.functional_columns()+s2.functional_columns());
@ -127,13 +125,13 @@ namespace datalog {
unsigned func_cnt = src.functional_columns();
if(removed_cols==nullptr) {
if (removed_cols==nullptr) {
result.set_functional_columns(func_cnt);
return;
}
unsigned first_src_fun = src.first_functional();
if(removed_cols[0]<first_src_fun) {
if (removed_cols[0]<first_src_fun) {
//if we remove at least one non-functional column, all the columns in the result are non-functional
result.set_functional_columns(0);
}
@ -150,8 +148,8 @@ namespace datalog {
unsigned remaining_fun = src.functional_columns();
unsigned first_src_fun = src.first_functional();
for(int i=col_cnt-1; i>=0; i--) {
if(removed_cols[i]<first_src_fun) {
for (int i=col_cnt-1; i>=0; i--) {
if (removed_cols[i]<first_src_fun) {
break;
}
remaining_fun--;
@ -168,7 +166,7 @@ namespace datalog {
//after the join the column order is
//(non-functional of s1)(non-functional of s2)(functional of s1)(functional of s2)
if(s1.functional_columns()==0 && s2.functional_columns()==0) {
if (s1.functional_columns()==0 && s2.functional_columns()==0) {
from_project(aux, removed_col_cnt, removed_cols, result);
SASSERT(result.functional_columns()==0);
return;
@ -187,27 +185,27 @@ namespace datalog {
union_find_default_ctx uf_ctx;
union_find<> uf(uf_ctx); //the numbers in uf correspond to column indexes after the join
for(unsigned i=0; i<join_sig_sz; i++) {
for (unsigned i=0; i<join_sig_sz; i++) {
VERIFY(uf.mk_var() == i);
}
for(unsigned i=0; i<joined_col_cnt; i++) {
for (unsigned i=0; i<joined_col_cnt; i++) {
unsigned idx1 = (s1_first_func>cols1[i]) ? cols1[i] : (first_func_ofs+cols1[i]-s1_first_func);
unsigned idx2 = (s2_first_func>cols2[i]) ? (second_ofs+cols2[i]) : (second_func_ofs+cols2[i]-s2_first_func);
uf.merge(idx1, idx2);
}
for(unsigned i=0; i<first_func_ofs; i++) { //we only count the non-functional columns
for (unsigned i=0; i<first_func_ofs; i++) { //we only count the non-functional columns
remaining_in_equivalence_class[uf.find(i)]++;
}
for(unsigned i=0; i<removed_col_cnt; i++) {
for (unsigned i=0; i<removed_col_cnt; i++) {
unsigned rc = removed_cols[i];
if(rc>=first_func_ofs) {
if (rc>=first_func_ofs) {
//removing functional columns won't make us merge rows
continue;
}
unsigned eq_class_idx = uf.find(rc);
if(remaining_in_equivalence_class[eq_class_idx]>1) {
if (remaining_in_equivalence_class[eq_class_idx]>1) {
remaining_in_equivalence_class[eq_class_idx]--;
}
else {
@ -216,7 +214,7 @@ namespace datalog {
}
}
if(merging_rows_can_happen) {
if (merging_rows_can_happen) {
//this one marks all columns as non-functional
from_project(aux, removed_col_cnt, removed_cols, result);
SASSERT(result.functional_columns()==0);
@ -227,9 +225,6 @@ namespace datalog {
}
}
// -----------------------------------
//
// table_base
@ -239,17 +234,17 @@ namespace datalog {
//here we give generic implementation of table operations using iterators
bool table_base::empty() const {
return begin()==end();
return begin() == end();
}
void table_base::remove_facts(unsigned fact_cnt, const table_fact * facts) {
for(unsigned i=0; i<fact_cnt; i++) {
for (unsigned i = 0; i < fact_cnt; i++) {
remove_fact(facts[i]);
}
}
void table_base::remove_facts(unsigned fact_cnt, const table_element * facts) {
for(unsigned i=0; i<fact_cnt; i++) {
for (unsigned i = 0; i < fact_cnt; i++) {
remove_fact(facts + i*get_signature().size());
}
}
@ -257,25 +252,19 @@ namespace datalog {
void table_base::reset() {
vector<table_fact> to_remove;
table_base::iterator it = begin();
table_base::iterator iend = end();
table_fact row;
for(; it!=iend; ++it) {
it->get_fact(row);
for (auto& k : *this) {
k.get_fact(row);
to_remove.push_back(row);
}
remove_facts(to_remove.size(), to_remove.c_ptr());
}
bool table_base::contains_fact(const table_fact & f) const {
iterator it = begin();
iterator iend = end();
table_fact row;
for(; it!=iend; ++it) {
it->get_fact(row);
if(vectors_equal(row, f)) {
for (auto const& k : *this) {
k.get_fact(row);
if (vectors_equal(row, f)) {
return true;
}
}
@ -283,27 +272,25 @@ namespace datalog {
}
bool table_base::fetch_fact(table_fact & f) const {
if(get_signature().functional_columns()==0) {
if (get_signature().functional_columns() == 0) {
return contains_fact(f);
}
else {
unsigned sig_sz = get_signature().size();
unsigned non_func_cnt = sig_sz-get_signature().functional_columns();
table_base::iterator it = begin();
table_base::iterator iend = end();
table_fact row;
for(; it!=iend; ++it) {
it->get_fact(row);
for (auto& k : *this) {
k.get_fact(row);
bool differs = false;
for(unsigned i=0; i<non_func_cnt; i++) {
if(row[i]!=f[i]) {
for (unsigned i=0; i<non_func_cnt; i++) {
if (row[i]!=f[i]) {
differs = true;
}
}
if(differs) {
if (differs) {
continue;
}
for(unsigned i=non_func_cnt; i<sig_sz; i++) {
for (unsigned i=non_func_cnt; i<sig_sz; i++) {
f[i]=row[i];
}
return true;
@ -313,15 +300,15 @@ namespace datalog {
}
bool table_base::suggest_fact(table_fact & f) {
if(get_signature().functional_columns()==0) {
if(contains_fact(f)) {
if (get_signature().functional_columns()==0) {
if (contains_fact(f)) {
return false;
}
add_new_fact(f);
return true;
}
else {
if(fetch_fact(f)) {
if (fetch_fact(f)) {
return false;
}
add_new_fact(f);
@ -330,7 +317,7 @@ namespace datalog {
}
void table_base::ensure_fact(const table_fact & f) {
if(get_signature().functional_columns()==0) {
if (get_signature().functional_columns() == 0) {
add_fact(f);
}
else {
@ -341,14 +328,9 @@ namespace datalog {
table_base * table_base::clone() const {
table_base * res = get_plugin().mk_empty(get_signature());
iterator it = begin();
iterator iend = end();
table_fact row;
for(; it!=iend; ++it) {
it->get_fact(row);
for (auto& k : *this) {
k.get_fact(row);
res->add_new_fact(row);
}
return res;
@ -394,9 +376,9 @@ namespace datalog {
warning_msg("%s", buffer.str().c_str());
}
for(table_element i = 0; i < upper_bound; i++) {
for (table_element i = 0; i < upper_bound; i++) {
fact[0] = i;
if(empty_table || !contains_fact(fact)) {
if (empty_table || !contains_fact(fact)) {
res->add_fact(fact);
}
}
@ -407,12 +389,9 @@ namespace datalog {
out << "table with signature ";
print_container(get_signature(), out);
out << ":\n";
iterator it = begin();
iterator iend = end();
for(; it!=iend; ++it) {
const row_interface & r = *it;
r.display(out);
for (auto& k : *this) {
k.display(out);
}
out << "\n";
@ -448,8 +427,8 @@ namespace datalog {
void table_base::row_interface::get_fact(table_fact & result) const {
result.reset();
unsigned n=size();
for(unsigned i=0; i<n; i++) {
unsigned n = size();
for (unsigned i = 0; i < n; i++) {
result.push_back((*this)[i]);
}
}
@ -470,10 +449,7 @@ namespace datalog {
dl_decl_util util(m);
bool_rewriter brw(m);
table_fact fact;
iterator it = begin();
iterator iend = end();
for(; it != iend; ++it) {
const row_interface & r = *it;
for (row_interface const& r : *this) {
r.get_fact(fact);
conjs.reset();
for (unsigned i = 0; i < fact.size(); ++i) {

38
src/muz/rel/dl_base.h
View file

@ -96,12 +96,12 @@ namespace datalog {
public:
bool operator==(const signature & o) const {
unsigned n=signature_base_base::size();
if(n!=o.size()) {
if (n!=o.size()) {
return false;
}
return memcmp(this->c_ptr(), o.c_ptr(), n*sizeof(sort))==0;
/*for(unsigned i=0; i<n; i++) {
if((*this)[i]!=o[i]) {
/*for (unsigned i=0; i<n; i++) {
if ((*this)[i]!=o[i]) {
return false;
}
}
@ -117,15 +117,15 @@ namespace datalog {
result.reset();
unsigned s1sz=s1.size();
for(unsigned i=0; i<s1sz; i++) {
for (unsigned i=0; i<s1sz; i++) {
result.push_back(s1[i]);
}
unsigned s2sz=s2.size();
for(unsigned i=0; i<s2sz; i++) {
for (unsigned i=0; i<s2sz; i++) {
result.push_back(s2[i]);
}
#if Z3DEBUG
for(unsigned i=0; i<col_cnt; i++) {
for (unsigned i=0; i<col_cnt; i++) {
SASSERT(cols1[i]<s1sz);
SASSERT(cols2[i]<s2sz);
}
@ -171,7 +171,7 @@ namespace datalog {
const unsigned * permutation, signature & result) {
result.reset();
unsigned n = src.size();
for(unsigned i=0; i<n; i++) {
for (unsigned i=0; i<n; i++) {
result.push_back(src[permutation[i]]);
}
}
@ -591,8 +591,8 @@ namespace datalog {
unsigned neg_sig_size = neg_t.get_signature().size();
m_overlap = false;
m_bound.resize(neg_sig_size, false);
for(unsigned i=0; i<joined_col_cnt; i++) {
if(m_bound[negated_cols[i]]) {
for (unsigned i=0; i<joined_col_cnt; i++) {
if (m_bound[negated_cols[i]]) {
m_overlap = true;
}
m_bound[negated_cols[i]]=true;
@ -611,14 +611,14 @@ namespace datalog {
void make_neg_bindings(T & tgt_neg, const U & src) const {
SASSERT(m_all_neg_bound);
SASSERT(!m_overlap);
for(unsigned i=0; i<m_joined_col_cnt; i++) {
for (unsigned i=0; i<m_joined_col_cnt; i++) {
tgt_neg[m_cols2[i]]=src[m_cols1[i]];
}
}
template<typename T, typename U>
bool bindings_match(const T & tgt_neg, const U & src) const {
for(unsigned i=0; i<m_joined_col_cnt; i++) {
if(tgt_neg[m_cols2[i]]!=src[m_cols1[i]]) {
for (unsigned i=0; i<m_joined_col_cnt; i++) {
if (tgt_neg[m_cols2[i]]!=src[m_cols1[i]]) {
return false;
}
}
@ -661,10 +661,10 @@ namespace datalog {
base_object * operator()(const base_object & o) override {
const base_object * res = &o;
scoped_rel<base_object> res_scoped;
if(m_renamers_initialized) {
if (m_renamers_initialized) {
typename renamer_vector::iterator rit = m_renamers.begin();
typename renamer_vector::iterator rend = m_renamers.end();
for(; rit!=rend; ++rit) {
for (; rit!=rend; ++rit) {
res_scoped = (**rit)(*res);
res = res_scoped.get();
}
@ -683,7 +683,7 @@ namespace datalog {
}
m_renamers_initialized = true;
}
if(res_scoped) {
if (res_scoped) {
SASSERT(res==res_scoped.get());
//we don't want to delete the last one since we'll be returning it
return res_scoped.release();
@ -989,7 +989,7 @@ namespace datalog {
#if Z3DEBUG
unsigned first_src_fun = src.size()-src.functional_columns();
bool in_func = permutation_cycle[0]>=first_src_fun;
for(unsigned i=1;i<cycle_len;i++) {
for (unsigned i=1;i<cycle_len;i++) {
SASSERT(in_func == (permutation_cycle[i]>=first_src_fun));
}
#endif
@ -1007,7 +1007,7 @@ namespace datalog {
#if Z3DEBUG
unsigned sz = src.size();
unsigned first_src_fun = sz-src.functional_columns();
for(unsigned i=first_src_fun;i<sz;i++) {
for (unsigned i=first_src_fun;i<sz;i++) {
SASSERT(permutation[i]>=first_src_fun);
}
#endif
@ -1107,7 +1107,7 @@ namespace datalog {
void dec_ref() {
SASSERT(m_ref_cnt>0);
m_ref_cnt--;
if(m_ref_cnt==0) {
if (m_ref_cnt==0) {
dealloc(this);
}
}
@ -1137,7 +1137,7 @@ namespace datalog {
void dec_ref() {
SASSERT(m_ref_cnt>0);
m_ref_cnt--;
if(m_ref_cnt==0) {
if (m_ref_cnt==0) {
dealloc(this);
}
}

2
src/muz/rel/dl_table.cpp
View file

@ -251,7 +251,7 @@ namespace datalog {
}
shift += num_bits;
if (shift >= 32) {
throw default_exception("bit-vector table is specialized to small domains that are powers of two");
throw default_exception("bit-vector table is specialized to small domains that are powers of two");
}
}
m_bv.reserve(1 << shift);

12
src/muz/spacer/spacer_context.cpp
View file

@ -2924,12 +2924,12 @@ expr_ref context::get_ground_sat_answer() const {
<< "Sat answer unavailable when result is false\n";);
return expr_ref(m);
}
// convert a ground refutation into a linear counterexample
// only works for linear CHC systems
expr_ref_vector cex(m);
proof_ref pf = get_ground_refutation();
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned>> positions;
@ -2946,18 +2946,18 @@ expr_ref context::get_ground_sat_answer() const {
} else {
pf.reset();
break;
}
}
premises.reset();
conclusion.reset();
positions.reset();
substs.reset();
}
}
SASSERT(!pf || !m.is_hyper_resolve(pf));
if (pf) {
cex.push_back(m.get_fact(pf));
}
TRACE ("spacer", tout << "ground cex\n" << cex << "\n";);
return mk_and(cex);