mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix #3826

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 14:39:54 -07:00
parent 6d6881c87a
commit 35f184a6b9
11 changed files with 108 additions and 114 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/model/model_core.cpp
View file

@ -47,7 +47,12 @@ bool model_core::eval(func_decl* f, expr_ref & r) const {
}
void model_core::register_decl(func_decl * d, expr * v) {
SASSERT(d->get_arity() == 0);
if (d->get_arity() > 0) {
func_interp* fi = alloc(func_interp, m, d->get_arity());
fi->set_else(v);
register_decl(d, fi);
return;
}
TRACE("model", tout << "register " << d->get_name() << "\n";
if (v) tout << mk_pp(v, m) << "\n";
);

3
src/muz/base/dl_engine_base.h
View file

@ -96,8 +96,9 @@ namespace datalog {
throw default_exception(std::string("certificates are not supported for ") + m_name);
}
virtual model_ref get_model() {
return model_ref(alloc(model, m));
return model_ref();
}
virtual void get_rules_along_trace (rule_ref_vector& rules) {
throw default_exception(std::string("get_rules_along_trace is not supported for ") + m_name);
}

1
src/muz/base/dl_rule.cpp
View file

@ -1019,7 +1019,6 @@ namespace datalog {
void rule::display(context & ctx, std::ostream & out) const {
ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n";
//out << mk_pp(m_head, m);
output_predicate(ctx, m_head, out);
if (m_tail_size == 0) {
out << ".\n";

65
src/muz/base/dl_rule_set.cpp
View file

@ -188,12 +188,10 @@ namespace datalog {
unsigned curr_index = init_len;
rule_dependencies reversed(*this, true);
iterator pit = begin();
iterator pend = end();
for (; pit!=pend; ++pit) {
func_decl * pred = pit->m_key;
for (auto& kv : *this) {
func_decl * pred = kv.m_key;
unsigned deg = in_degree(pred);
if (deg==0) {
if (deg == 0) {
res.push_back(pred);
}
else {
@ -201,13 +199,10 @@ namespace datalog {
}
}
while (curr_index<res.size()) { //res.size() can change in the loop iteration
while (curr_index < res.size()) { //res.size() can change in the loop iteration
func_decl * curr = res[curr_index];
const item_set & children = reversed.get_deps(curr);
item_set::iterator cit = children.begin();
item_set::iterator cend = children.end();
for (; cit!=cend; ++cit) {
func_decl * child = *cit;
for (func_decl * child : children) {
deg_map::obj_map_entry * e = degs.find_core(child);
SASSERT(e);
unsigned & child_deg = e->get_data().m_value;
@ -227,20 +222,14 @@ namespace datalog {
return true;
}
void rule_dependencies::display(std::ostream & out ) const
{
iterator pit = begin();
iterator pend = end();
for (; pit != pend; ++pit) {
func_decl * pred = pit->m_key;
const item_set & deps = *pit->m_value;
item_set::iterator dit=deps.begin();
item_set::iterator dend=deps.end();
if (dit == dend) {
out<<pred->get_name()<<" - <none>\n";
void rule_dependencies::display(std::ostream & out ) const {
for (auto const& kv : *this) {
func_decl * pred = kv.m_key;
const item_set & deps = *kv.m_value;
if (deps.empty()) {
out << pred->get_name()<<" - <none>\n";
}
for (; dit != dend; ++dit) {
func_decl * dep = *dit;
for (func_decl* dep : deps) {
out << pred->get_name() << " -> " << dep->get_name() << "\n";
}
}
@ -473,9 +462,8 @@ namespace datalog {
bool change = true;
while (change) {
change = false;
func_decl_set::iterator it = non_founded.begin(), end = non_founded.end();
for (; it != end; ++it) {
rule_vector const& rv = get_predicate_rules(*it);
for (func_decl * f : non_founded) {
rule_vector const& rv = get_predicate_rules(f);
bool found = false;
for (unsigned i = 0; !found && i < rv.size(); ++i) {
rule const& r = *rv[i];
@ -484,8 +472,8 @@ namespace datalog {
is_founded = founded.contains(r.get_decl(j));
}
if (is_founded) {
founded.insert(*it);
non_founded.remove(*it);
founded.insert(f);
non_founded.remove(f);
change = true;
found = true;
}
@ -497,19 +485,12 @@ 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';
for (func_decl * f : m_output_preds) {
out << "; output: " << f->get_name() << '\n';
}
decl2rules::iterator it = m_head2rules.begin();
decl2rules::iterator end = m_head2rules.end();
for (; it != end; ++it) {
ptr_vector<rule> * rules = it->m_value;
ptr_vector<rule>::iterator it2 = rules->begin();
ptr_vector<rule>::iterator end2 = rules->end();
for (; it2 != end2; ++it2) {
rule * r = *it2;
for (auto const& kv : m_head2rules) {
ptr_vector<rule> * rules = kv.m_value;
for (rule* r : *rules) {
if (!r->passes_output_thresholds(m_context)) {
continue;
}
@ -722,8 +703,8 @@ namespace datalog {
void rule_stratifier::display(std::ostream& out) const {
m_deps.display(out << "dependencies\n");
out << "strata\n";
for (unsigned i = 0; i < m_strats.size(); ++i) {
for (auto * item : *m_strats[i]) {
for (auto * s : m_strats) {
for (auto * item : *s) {
out << item->get_name() << " ";
}
out << "\n";

88
src/muz/base/dl_util.h
View file

@ -88,7 +88,7 @@ namespace datalog {
for (unsigned i = 0; i < n; i++) {
expr * arg = src->get_arg(i);
if (!is_var(arg)) {
tgt[i]=arg;
tgt[i] = arg;
}
}
}
@ -168,12 +168,12 @@ namespace datalog {
}
bool empty() const {
return size()==0;
return size() == 0;
}
void get(unsigned i, unsigned & index1, unsigned & index2) const {
index1=m_args1[i];
index2=m_args2[i];
index1 = m_args1[i];
index2 = m_args2[i];
}
void reset() {
@ -192,11 +192,11 @@ namespace datalog {
*/
template<typename T>
void fill_into_second(const app * f1, T & tgt) const {
unsigned n=size();
for(unsigned i=0; i<n; i++) {
unsigned n = size();
for (unsigned i = 0; i < n; i++) {
unsigned f1_index, tgt_index;
get(i, f1_index, tgt_index);
tgt[tgt_index]=f1->get_arg(f1_index);
tgt[tgt_index] = f1->get_arg(f1_index);
}
}
@ -216,19 +216,19 @@ namespace datalog {
//TODO: optimize number of checks when variable occurs multiple times
unsigned a1num = expr_cont_get_size(a1);
unsigned a2num = expr_cont_get_size(a2);
for(unsigned i1=0; i1<a1num; i1++) {
expr * e1=expr_cont_get(a1,i1);
if(!is_var(e1)) {
for (unsigned i1 = 0; i1<a1num; i1++) {
expr * e1 = expr_cont_get(a1,i1);
if (!is_var(e1)) {
continue;
}
var* v1=to_var(e1);
for(unsigned i2=0; i2<a2num; i2++) {
expr * e2=expr_cont_get(a2,i2);
if(!is_var(e2)) {
var* v1 = to_var(e1);
for (unsigned i2 = 0; i2<a2num; i2++) {
expr * e2 = expr_cont_get(a2,i2);
if (!is_var(e2)) {
continue;
}
var* v2=to_var(e2);
if(v1->get_idx()==v2->get_idx()) {
var* v2 = to_var(e2);
if (v1->get_idx() == v2->get_idx()) {
add_pair(i1, i2);
}
}
@ -244,14 +244,14 @@ namespace datalog {
template<class T>
void project_out_vector_columns(T & container, unsigned removed_col_cnt, const unsigned * removed_cols) {
if(removed_col_cnt==0) {
if (removed_col_cnt==0) {
return;
}
unsigned n = container.size();
unsigned ofs = 1;
unsigned r_i = 1;
for(unsigned i=removed_cols[0]+1; i<n; i++) {
if(r_i!=removed_col_cnt && removed_cols[r_i]==i) {
for (unsigned i=removed_cols[0]+1; i<n; i++) {
if (r_i!=removed_col_cnt && removed_cols[r_i]==i) {
r_i++;
ofs++;
continue;
@ -271,14 +271,14 @@ namespace datalog {
template<class T, class M>
void project_out_vector_columns(ref_vector<T,M> & container, unsigned removed_col_cnt,
const unsigned * removed_cols) {
if(removed_col_cnt==0) {
if (removed_col_cnt==0) {
return;
}
unsigned n = container.size();
unsigned ofs = 1;
unsigned r_i = 1;
for(unsigned i=removed_cols[0]+1; i<n; i++) {
if(r_i!=removed_col_cnt && removed_cols[r_i]==i) {
for (unsigned i=removed_cols[0]+1; i<n; i++) {
if (r_i!=removed_col_cnt && removed_cols[r_i]==i) {
r_i++;
ofs++;
continue;
@ -319,11 +319,11 @@ namespace datalog {
template<class T>
void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) {
if(cycle_len<2) {
if (cycle_len<2) {
return;
}
typename T::data aux = container[permutation_cycle[0]];
for(unsigned i=1; i<cycle_len; i++) {
for (unsigned i=1; i<cycle_len; i++) {
container[permutation_cycle[i-1]]=container[permutation_cycle[i]];
}
container[permutation_cycle[cycle_len-1]]=aux;
@ -331,11 +331,11 @@ namespace datalog {
template<class T, class M>
void permutate_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
if(cycle_len<2) {
if (cycle_len<2) {
return;
}
T * aux = container.get(permutation_cycle[0]);
for(unsigned i=1; i<cycle_len; i++) {
for (unsigned i=1; i<cycle_len; i++) {
container.set(permutation_cycle[i-1], container.get(permutation_cycle[i]));
}
container.set(permutation_cycle[cycle_len-1], aux);
@ -385,14 +385,14 @@ namespace datalog {
template<class T, class U>
bool vectors_equal(const T & c1, const U & c2) {
if(c1.size()!=c2.size()) {
if (c1.size()!=c2.size()) {
return false;
}
typename T::data * it1 = c1.c_ptr();
typename T::data * end1 = c1.c_ptr()+c1.size();
typename U::data * it2 = c2.c_ptr();
for(; it1!=end1; ++it1, ++it2) {
if(*it1!=*it2) {
for (; it1!=end1; ++it1, ++it2) {
if (*it1!=*it2) {
return false;
}
}
@ -436,7 +436,7 @@ namespace datalog {
void dealloc_ptr_vector_content(ptr_vector<T> & v) {
typename ptr_vector<T>::iterator it = v.begin();
typename ptr_vector<T>::iterator end = v.end();
for(; it!=end; ++it) {
for (; it!=end; ++it) {
dealloc(*it);
}
}
@ -448,7 +448,7 @@ namespace datalog {
void push_into_vector(VectType & vector, const U & src) {
typename U::iterator it = src.begin();
typename U::iterator end = src.end();
for(; it!=end; ++it) {
for (; it!=end; ++it) {
vector.push_back(*it);
}
}
@ -457,7 +457,7 @@ namespace datalog {
void push_into_vector(VectType & vector, const ref_vector<U,M> & src) {
U * const * it = src.begin();
U * const * end = src.end();
for(; it!=end; ++it) {
for (; it!=end; ++it) {
vector.push_back(*it);
}
}
@ -466,7 +466,7 @@ namespace datalog {
void insert_into_set(SetType & tgt, const U & src) {
typename U::const_iterator it = src.begin();
typename U::const_iterator end = src.end();
for(; it!=end; ++it) {
for (; it!=end; ++it) {
tgt.insert(*it);
}
}
@ -480,8 +480,8 @@ namespace datalog {
template<class T>
bool remove_from_vector(T & v, const typename T::data & el) {
unsigned sz = v.size();
for(unsigned i=0; i<sz; i++) {
if(v[i]==el) {
for (unsigned i=0; i<sz; i++) {
if (v[i]==el) {
std::swap(v[i], v.back());
v.pop_back();
return true;
@ -515,28 +515,28 @@ namespace datalog {
template<class T, class U>
void sort_two_arrays(unsigned len, T* keys, U* vals) {
if(len<2) {
if (len<2) {
return;
}
if(len==2) {
if(keys[0]>keys[1]) {
if (len==2) {
if (keys[0]>keys[1]) {
std::swap(keys[0], keys[1]);
std::swap(vals[0], vals[1]);
}
return;
}
unsigned_vector numbers;
for(unsigned i=0; i<len; i++) {
for (unsigned i=0; i<len; i++) {
numbers.push_back(i);
}
aux__index_comparator<T> cmp(keys);
std::sort(numbers.begin(), numbers.end(), cmp);
for(unsigned i=0; i<len; i++) {
for (unsigned i=0; i<len; i++) {
unsigned prev_i = i;
for(;;) {
for (;;) {
unsigned src_i = numbers[prev_i];
numbers[prev_i]=prev_i;
if(src_i==i) {
if (src_i==i) {
break;
}
std::swap(keys[prev_i], keys[src_i]);
@ -565,8 +565,8 @@ namespace datalog {
template<class Container>
void add_sequence_without_set(unsigned start, unsigned count, const Container & complement, unsigned_vector & v) {
unsigned after_last = start+count;
for(unsigned i=start; i<after_last; i++) {
if(!complement.contains(i)) {
for (unsigned i=start; i<after_last; i++) {
if (!complement.contains(i)) {
v.push_back(i);
}
}

19
src/muz/fp/horn_tactic.cpp
View file

@ -283,13 +283,8 @@ class horn_tactic : public tactic {
g->reset();
if (produce_models) {
model_ref md = m_ctx.get_model();
model_converter_ref mc2 = model2model_converter(&*md);
if (mc) {
mc = concat(mc.get(), mc2.get());
}
else {
mc = mc2;
}
model_converter_ref mc2 = model2model_converter(md.get());
mc = concat(mc.get(), mc2.get());
}
break;
}
@ -314,14 +309,12 @@ class horn_tactic : public tactic {
}
void simplify(expr* q,
goal_ref const& g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc) {
goal_ref const& g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc) {
expr_ref fml(m);
func_decl* query_pred = to_app(q)->get_decl();
m_ctx.set_output_predicate(query_pred);
m_ctx.get_rules(); // flush adding rules.

8
src/muz/rel/dl_relation_manager.cpp
View file

@ -115,6 +115,14 @@ namespace datalog {
e->get_data().m_value = rel;
}
decl_set relation_manager::collect_predicates() const {
decl_set res;
for (auto const& kv : m_relations) {
res.insert(kv.m_key);
}
return res;
}
void relation_manager::collect_non_empty_predicates(decl_set & res) const {
for (auto const& kv : m_relations) {
if (!kv.m_value->fast_empty()) {

3
src/muz/rel/dl_relation_manager.h
View file

@ -115,7 +115,7 @@ namespace datalog {
m_next_relation_fid(0) {}
virtual ~relation_manager();
void reset();
void reset_relations();
@ -155,6 +155,7 @@ namespace datalog {
}
}
decl_set collect_predicates() const;
void collect_non_empty_predicates(decl_set & res) const;
void restrict_predicates(const decl_set & preds);

23
src/muz/rel/rel_context.cpp
View file

@ -257,16 +257,6 @@ namespace datalog {
is_approx = true;
}
rel.to_formula(e);
#if 0
// Alternative format:
// List the signature of the relation as
// part of the answer.
expr_ref_vector args(m);
for (unsigned j = 0; j < q->get_arity(); ++j) {
args.push_back(m.mk_var(j, q->get_domain(j)));
}
e = m.mk_implies(m.mk_app(q, args.size(), args.c_ptr()), e);
#endif
ans.push_back(e);
}
SASSERT(!m_last_result_relation);
@ -294,6 +284,19 @@ namespace datalog {
return res;
}
model_ref rel_context::get_model() {
model_ref md = alloc(model, m);
auto& rm = get_rmanager();
func_decl_set decls = rm.collect_predicates();
expr_ref fml(m);
for (func_decl* p : decls) {
rm.get_relation(p).to_formula(fml);
md->register_decl(p, fml);
}
(*m_context.get_model_converter())(md);
return md;
}
void rel_context::transform_rules() {
rule_transformer transf(m_context);
transf.register_plugin(alloc(mk_coi_filter, m_context));

2
src/muz/rel/rel_context.h
View file

@ -91,6 +91,8 @@ namespace datalog {
void transform_rules() override;
model_ref get_model() override;
bool try_get_size(func_decl* pred, unsigned& rel_size) const override;
/**
\brief query result if it contains fact.

3
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -104,13 +104,14 @@ namespace datalog {
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
for (auto const& kv : engine) {
if (!kv.m_value.is_reachable()) {
mc0->add(kv.m_key, m.mk_false());
unreachable.insert(kv.m_key);
}
}
for (func_decl* f : unreachable) {
mc0->add(f, m.mk_false());
}
m_context.add_model_converter(mc0);
TRACE("dl", m_context.get_model_converter()->display(tout););
}
CTRACE("dl", res, res->display(tout););
return res.detach();