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

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-20 17:57:34 +01:00
parent c377fec7a4 e915d0f67d
commit f8145c8b9f
10 changed files with 88 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -558,6 +558,7 @@ namespace datalog {
m_rule_properties.check_quantifier_free();
m_rule_properties.check_uninterpreted_free();
m_rule_properties.check_nested_free();
m_rule_properties.check_infinite_sorts();
break;
case PDR_ENGINE:
m_rule_properties.collect(r);

27
src/muz/base/rule_properties.cpp
View file

@ -26,7 +26,7 @@ Notes:
using namespace datalog;
rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p):
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {}
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_bv(m), m_generate_proof(false) {}
rule_properties::~rule_properties() {}
@ -48,6 +48,12 @@ void rule_properties::collect(rule_set const& rules) {
if (m_generate_proof && !r->get_proof()) {
rm.mk_rule_asserted_proof(*r);
}
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
m_inf_sort.push_back(m_rule);
}
}
}
}
@ -85,6 +91,16 @@ void rule_properties::check_uninterpreted_free() {
}
}
void rule_properties::check_infinite_sorts() {
if (!m_inf_sort.empty()) {
std::stringstream stm;
rule* r = m_inf_sort.back();
stm << "Rule contains infinite sorts in rule ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_nested_free() {
if (!m_interp_pred.empty()) {
std::stringstream stm;
@ -92,7 +108,6 @@ void rule_properties::check_nested_free() {
stm << "Rule contains nested predicates ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
@ -158,7 +173,8 @@ void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
}
}
void rule_properties::operator()(var* n) { }
void rule_properties::operator()(var* n) {
}
void rule_properties::operator()(quantifier* n) {
m_quantifiers.insert(n, m_rule);
@ -177,6 +193,10 @@ void rule_properties::operator()(app* n) {
m_uninterp_funs.insert(n->get_decl(), m_rule);
}
}
else {
std::cout << mk_pp(n, m) << "\n";
}
}
void rule_properties::reset() {
@ -184,5 +204,6 @@ void rule_properties::reset() {
m_uninterp_funs.reset();
m_interp_pred.reset();
m_negative_rules.reset();
m_inf_sort.reset();
}

4
src/muz/base/rule_properties.h
View file

@ -23,6 +23,7 @@ Notes:
#include"ast.h"
#include"datatype_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"dl_rule.h"
namespace datalog {
@ -33,12 +34,14 @@ namespace datalog {
i_expr_pred& m_is_predicate;
datatype_util m_dt;
dl_decl_util m_dl;
bv_util m_bv;
bool m_generate_proof;
rule* m_rule;
obj_map<quantifier, rule*> m_quantifiers;
obj_map<func_decl, rule*> m_uninterp_funs;
ptr_vector<rule> m_interp_pred;
ptr_vector<rule> m_negative_rules;
ptr_vector<rule> m_inf_sort;
void insert(ptr_vector<rule>& rules, rule* r);
public:
@ -51,6 +54,7 @@ namespace datalog {
void check_existential_tail();
void check_for_negated_predicates();
void check_nested_free();
void check_infinite_sorts();
void operator()(var* n);
void operator()(quantifier* n);
void operator()(app* n);

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

@ -654,7 +654,7 @@ namespace datalog {
family_id expl_kind = m_er_plugin->get_kind();
family_id expl_sieve_kind = sieve_plugin.get_relation_kind(sig, expl_sieve, expl_kind);
product_relation_plugin::rel_spec product_spec;
rel_spec product_spec;
product_spec.push_back(inner_sieve_kind);
product_spec.push_back(expl_sieve_kind);

69
src/muz/rel/dl_product_relation.cpp
View file

@ -77,6 +77,7 @@ namespace datalog {
}
family_id product_relation_plugin::get_relation_kind(const relation_signature & sig, const rel_spec & spec) {
SASSERT(spec.well_formed());
return m_spec_store.get_relation_kind(sig, spec);
}
@ -132,14 +133,11 @@ namespace datalog {
ptr_vector<const product_relation>::const_iterator rend = rels.end();
for(; rit!=rend; ++rit) {
specs.push_back((*rit)->m_spec);
SASSERT(specs.back().well_formed());
std::sort(specs.back().begin(), specs.back().end());
}
vector<rel_spec>::iterator sit = specs.begin();
vector<rel_spec>::iterator send = specs.end();
for(; sit!=send; ++sit) {
rel_spec & s = *sit;
std::sort(s.begin(), s.end());
}
vector<rel_spec>::iterator sit = specs.begin(), send = specs.end();
res.reset();
for(;;) {
@ -160,7 +158,7 @@ namespace datalog {
sit = specs.begin();
for(; sit!=send; ++sit) {
rel_spec & s = *sit;
if(!s.empty() && s.back()==next) {
while (!s.empty() && s.back()==next) {
s.pop_back();
}
}
@ -191,6 +189,7 @@ namespace datalog {
}
rel_spec spec;
m_spec_store.get_relation_spec(s, kind, spec);
SASSERT(spec.well_formed());
relation_vector inner_rels;
unsigned rel_cnt = spec.size();
for(unsigned i=0; i<rel_cnt; i++) {
@ -540,6 +539,7 @@ namespace datalog {
class product_relation_plugin::aligned_union_fn : public relation_union_fn {
relation_manager & m_rmgr;
product_relation_plugin& m_plugin;
bool m_is_widen;
//m_union[i][j] is union between i-th and j-th relation.
@ -556,6 +556,7 @@ namespace datalog {
else {
u = rmgr.mk_union_fn(r1, r2, delta);
}
TRACE("dl_verbose", tout << r1.get_plugin().get_name() << " " << r2.get_plugin().get_name() << " " << (u?"found":"not found") << "\n";);
m_unions.back().push_back(u);
}
@ -574,7 +575,7 @@ namespace datalog {
}
bool can_do_inner_union(unsigned tgt_idx, unsigned src_idx) {
return m_unions[tgt_idx][src_idx]!=0;
return m_unions[tgt_idx][src_idx] != 0;
}
void do_inner_union(unsigned tgt_idx, unsigned src_idx, relation_base& tgt,
@ -601,7 +602,8 @@ namespace datalog {
void do_intersection(relation_base& tgt, relation_base& src) {
scoped_ptr<relation_intersection_filter_fn> intersect_fun =
m_rmgr.mk_filter_by_intersection_fn(tgt, src);
if(!intersect_fun) {
if (!intersect_fun) {
TRACE("dl", tgt.display(tout << "tgt\n"); src.display(tout << "src\n"););
warning_msg("intersection does not exist");
return;
}
@ -613,9 +615,13 @@ namespace datalog {
(*union_fun)(tgt, src);
}
public:
aligned_union_fn(product_relation const& tgt, product_relation const& src, product_relation const* delta,
bool is_widen) :
aligned_union_fn(
product_relation const& tgt,
product_relation const& src,
product_relation const* delta,
bool is_widen) :
m_rmgr(tgt.get_manager()),
m_plugin(tgt.get_plugin()),
m_is_widen(is_widen) {
SASSERT(vectors_equal(tgt.m_spec, src.m_spec));
SASSERT(!delta || vectors_equal(tgt.m_spec, delta->m_spec));
@ -631,6 +637,9 @@ namespace datalog {
virtual void operator()(relation_base& _tgt, const relation_base& _src, relation_base* _delta) {
TRACE("dl", _tgt.display(tout << "dst:\n"); _src.display(tout << "src:\n"););
SASSERT(m_plugin.check_kind(_tgt));
SASSERT(m_plugin.check_kind(_src));
SASSERT(!_delta || m_plugin.check_kind(*_delta));
product_relation& tgt = get(_tgt);
product_relation const& src = get(_src);
product_relation* delta = get(_delta);
@ -652,7 +661,7 @@ namespace datalog {
if (i == j) {
continue; //this is the basic union which we will perform later
}
if (can_do_inner_union(i, j)) {
if (can_do_inner_union(i, j) && can_do_inner_union(j, i)) {
TRACE("dl", itgt.display(tout << "tgt:\n"); src[j].display(tout << "src:\n"););
// union[i][j]
scoped_rel<relation_base> one_side_union = itgt.clone();
@ -740,7 +749,7 @@ namespace datalog {
virtual void operator()(relation_base& _tgt, const relation_base& _src, relation_base* _delta) {
TRACE("dl", _tgt.display(tout << "dst:\n"); _src.display(tout << "src:\n"););
TRACE("dl_verbose", _tgt.display(tout << "dst:\n"); _src.display(tout << "src:\n"););
product_relation& tgt = get(_tgt);
product_relation const& src0 = get(_src);
product_relation* delta = _delta ? get(_delta) : 0;
@ -775,6 +784,7 @@ namespace datalog {
m_inner_union_fun(inner_union_fun) {}
virtual void operator()(relation_base& tgt, const relation_base& _src, relation_base* delta) {
TRACE("dl", tgt.display(tout); _src.display(tout); );
product_relation const& src = get(_src);
(*m_inner_union_fun)(tgt, src[m_single_rel_idx], delta);
}
@ -788,7 +798,8 @@ namespace datalog {
}
return alloc(unaligned_union_fn, get(tgt), get(src), get(delta), is_widen);
}
if(check_kind(src)) {
if (check_kind(src)) {
TRACE("dl", tgt.display(tout << "different kinds"); src.display(tout););
const product_relation & p_src = get(src);
unsigned single_idx;
if(p_src.try_get_single_non_transparent(single_idx)) {
@ -799,7 +810,7 @@ namespace datalog {
else {
inner = get_manager().mk_union_fn(tgt, p_src[single_idx], delta);
}
if(inner) {
if (inner) {
return alloc(single_non_transparent_src_union_fn, single_idx, inner);
}
}
@ -975,10 +986,20 @@ namespace datalog {
func_decl* p = 0;
const relation_signature & sig = get_signature();
family_id new_kind = get_plugin().get_relation_kind(sig, spec);
if(new_kind == get_kind()) {
if (new_kind == get_kind()) {
return;
}
TRACE("dl", {
ast_manager& m = get_ast_manager_from_rel_manager(get_manager());
sig.output(m, tout); tout << "\n";
for (unsigned i = 0; i < spec.size(); ++i) {
tout << spec[i] << " ";
}
tout << "\n";
}
);
unsigned old_sz = size();
unsigned new_sz = spec.size();
unsigned old_remain = old_sz;
@ -1001,10 +1022,10 @@ namespace datalog {
if(old_sz == 0 && m_default_empty) {
//The relation didn't contain any inner relations but it was empty,
//so we make the newly added relations empty as well.
irel = get_manager().mk_empty_relation(sig, new_kind);
irel = get_manager().mk_empty_relation(sig, ikind);
}
else {
irel = get_manager().mk_full_relation(sig, p, new_kind);
irel = get_manager().mk_full_relation(sig, p, ikind);
}
}
new_rels.push_back(irel);
@ -1013,10 +1034,8 @@ namespace datalog {
m_relations = new_rels;
set_kind(new_kind);
DEBUG_CODE(
ensure_correct_kind();
SASSERT(get_kind() == new_kind);
);
m_spec = spec;
SASSERT(get_kind() == new_kind);
}
bool product_relation::try_get_single_non_transparent(unsigned & idx) const {
@ -1104,7 +1123,11 @@ namespace datalog {
}
void product_relation::display(std::ostream & out) const {
out<<"Product of the following relations:\n";
if (m_relations.empty()) {
out << "{}\n";
return;
}
out << "Product of the following relations:\n";
for (unsigned i = 0; i < m_relations.size(); ++i) {
m_relations[i]->display(out);
}

8
src/muz/rel/dl_product_relation.h
View file

@ -27,10 +27,12 @@ namespace datalog {
class product_relation;
struct rel_spec : public svector<family_id> {
bool well_formed() const { return true; }
};
class product_relation_plugin : public relation_plugin {
friend class product_relation;
public:
typedef svector<family_id> rel_spec;
private:
class join_fn;
class transform_fn;
@ -120,8 +122,6 @@ namespace datalog {
typedef product_relation_plugin::rel_spec rel_spec;
/**
If m_relations is empty, value of this determines whether the relation is empty or full.
*/

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

@ -350,6 +350,7 @@ namespace datalog {
//If there is no plugin to handle the signature, we just create an empty product relation and
//stuff will be added to it by later operations.
TRACE("dl", s.output(get_context().get_manager(), tout << "empty product relation"); tout << "\n";);
return product_relation_plugin::get_plugin(*this).mk_empty(s);
}
@ -756,7 +757,6 @@ namespace datalog {
relation_union_fn * relation_manager::mk_union_fn(const relation_base & tgt, const relation_base & src,
const relation_base * delta) {
TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << "\n";);
relation_union_fn * res = tgt.get_plugin().mk_union_fn(tgt, src, delta);
if(!res && &tgt.get_plugin()!=&src.get_plugin()) {
res = src.get_plugin().mk_union_fn(tgt, src, delta);
@ -764,6 +764,7 @@ namespace datalog {
if(!res && delta && &tgt.get_plugin()!=&delta->get_plugin() && &src.get_plugin()!=&delta->get_plugin()) {
res = delta->get_plugin().mk_union_fn(tgt, src, delta);
}
// TRACE("dl", tout << src.get_plugin().get_name() << " " << tgt.get_plugin().get_name() << " " << (res?"created":"not created") << "\n";);
return res;
}

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

@ -486,7 +486,7 @@ namespace datalog {
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
break;
default: {
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
rel_spec rel_kinds; // kinds of plugins that are not table plugins
family_id rel_kind; // the aggregate kind of non-table plugins
for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);

2
src/qe/qe_sat_tactic.cpp
View file

@ -399,7 +399,7 @@ namespace qe {
expr_ref qt(unsigned i, expr* ctx, model_ref& model) {
model_ref model1;
while (true) {
IF_VERBOSE(1, verbose_stream() << "qt " << i << "\n";);
IF_VERBOSE(1, verbose_stream() << "(qt " << i << ")\n";);
TRACE("qe",
tout << i << " " << mk_pp(ctx, m) << "\n";
display(tout););

4
src/util/map.h
View file

@ -108,6 +108,10 @@ public:
m_table.insert(key_data(k, v));
}
bool insert_if_not_there_core(key const & k, value const & v, entry *& et) {
return m_table.insert_if_not_there_core(key_data(k,v), et);
}
key_data const & insert_if_not_there(key const & k, value const & v) {
return m_table.insert_if_not_there(key_data(k, v));
}