mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge pull request #1809 from agurfinkel/deep_space

Browse source 
Fix performance regression
This commit is contained in:
Nikolaj Bjorner 2018-09-04 20:35:46 -07:00 committed by GitHub
parent e8a78ec696 f67346d16e
commit 1e11b62bc6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
10 changed files with 702 additions and 84 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,7 +31,7 @@ namespace datalog {
rule_dependencies::rule_dependencies(const rule_dependencies & o, bool reversed):
m_context(o.m_context) {
if (reversed) {
for (auto & kv : o) {
for (auto & kv : o) {
func_decl * pred = kv.m_key;
item_set & orig_items = *kv.get_value();
@ -114,8 +114,8 @@ namespace datalog {
app* a = to_app(e);
d = a->get_decl();
if (m_context.is_predicate(d)) {
// insert d and ensure the invariant
// that every predicate is present as
// insert d and ensure the invariant
// that every predicate is present as
// a key in m_data
s.insert(d);
ensure_key(d);
@ -148,7 +148,7 @@ namespace datalog {
item_set& itms = *kv.get_value();
set_intersection(itms, allowed);
}
for (func_decl* f : to_remove)
for (func_decl* f : to_remove)
remove_m_data_entry(f);
}
@ -253,18 +253,18 @@ namespace datalog {
//
// -----------------------------------
rule_set::rule_set(context & ctx)
: m_context(ctx),
m_rule_manager(ctx.get_rule_manager()),
m_rules(m_rule_manager),
rule_set::rule_set(context & ctx)
: m_context(ctx),
m_rule_manager(ctx.get_rule_manager()),
m_rules(m_rule_manager),
m_deps(ctx),
m_stratifier(nullptr),
m_refs(ctx.get_manager()) {
}
rule_set::rule_set(const rule_set & other)
: m_context(other.m_context),
m_rule_manager(other.m_rule_manager),
rule_set::rule_set(const rule_set & other)
: m_context(other.m_context),
m_rule_manager(other.m_rule_manager),
m_rules(m_rule_manager),
m_deps(other.m_context),
m_stratifier(nullptr),
@ -353,10 +353,27 @@ namespace datalog {
break; \
} \
} \
DEL_VECTOR(*rules);
DEL_VECTOR(m_rules);
}
}
void rule_set::replace_rule(rule * r, rule * other) {
TRACE("dl", r->display(m_context, tout << "replace:"););
func_decl* d = r->get_decl();
rule_vector* rules = m_head2rules.find(d);
#define REPLACE_VECTOR(_v) \
for (unsigned i = (_v).size(); i > 0; ) { \
--i; \
if ((_v)[i] == r) { \
(_v)[i] = other; \
break; \
} \
} \
REPLACE_VECTOR(*rules);
REPLACE_VECTOR(m_rules);
}
void rule_set::ensure_closed() {
if (!is_closed()) {
@ -365,7 +382,7 @@ namespace datalog {
}
bool rule_set::close() {
SASSERT(!is_closed()); //the rule_set is not already closed
SASSERT(!is_closed()); //the rule_set is not already closed
m_deps.populate(*this);
m_stratifier = alloc(rule_stratifier, m_deps);
if (!stratified_negation()) {
@ -426,7 +443,7 @@ namespace datalog {
inherit_predicates(src);
}
const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const {
const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const {
decl2rules::obj_map_entry * e = m_head2rules.find_core(pred);
if (!e) {
return m_empty_rule_vector;
@ -519,7 +536,7 @@ namespace datalog {
out << "\n";
non_empty = false;
}
for (func_decl * first : *strat) {
const func_decl_set & deps = m_deps.get_deps(first);
for (func_decl * dep : deps) {
@ -545,8 +562,8 @@ namespace datalog {
unsigned rule_stratifier::get_predicate_strat(func_decl * pred) const {
unsigned num;
if (!m_pred_strat_nums.find(pred, num)) {
//the number of the predicate is not stored, therefore it did not appear
//in the algorithm and therefore it does not depend on anything and nothing
//the number of the predicate is not stored, therefore it did not appear
//in the algorithm and therefore it does not depend on anything and nothing
//depends on it. So it is safe to assign zero strate to it, although it is
//not strictly true.
num = 0;
@ -641,7 +658,7 @@ namespace datalog {
}
// We put components whose indegree is zero to m_strats and assign its
// We put components whose indegree is zero to m_strats and assign its
// m_components entry to zero.
unsigned comp_cnt = m_components.size();
for (unsigned i = 0; i < comp_cnt; i++) {
@ -680,7 +697,7 @@ namespace datalog {
strats_index++;
}
//we have managed to topologicaly order all the components
SASSERT(std::find_if(m_components.begin(), m_components.end(),
SASSERT(std::find_if(m_components.begin(), m_components.end(),
std::bind1st(std::not_equal_to<item_set*>(), (item_set*)0)) == m_components.end());
//reverse the strats array, so that the only the later components would depend on earlier ones
@ -713,7 +730,7 @@ namespace datalog {
}
out << "\n";
}
}
};

13
src/muz/base/dl_rule_set.h
View file

@ -77,7 +77,7 @@ namespace datalog {
\brief Number of predicates that depend on \c f.
*/
unsigned out_degree(func_decl * f) const;
/**
\brief If the rependency graph is acyclic, put all elements into \c res
ordered so that elements can depend only on elements that are before them.
@ -131,7 +131,7 @@ namespace datalog {
it must exist for the whole lifetime of the \c stratifier object.
*/
rule_stratifier(const rule_dependencies & deps)
: m_deps(deps), m_next_preorder(0)
: m_deps(deps), m_next_preorder(0)
{
process();
}
@ -145,7 +145,7 @@ namespace datalog {
const comp_vector & get_strats() const { return m_strats; }
unsigned get_predicate_strat(func_decl * pred) const;
void display( std::ostream & out ) const;
};
@ -203,6 +203,10 @@ namespace datalog {
\brief Remove rule \c r from the rule set.
*/
void del_rule(rule * r);
/**
\brief Replace a rule \c r with the rule \c other
*/
void replace_rule(rule * r, rule * other);
/**
\brief Add all rules from a different rule_set.
@ -276,8 +280,7 @@ namespace datalog {
inline std::ostream& operator<<(std::ostream& out, rule_set const& r) { r.display(out); return out; }
};
#endif /* DL_RULE_SET_H_ */

1
src/muz/base/fp_params.pyg
View file

@ -177,5 +177,6 @@ def_module_params('fp',
('spacer.dump_threshold', DOUBLE, 5.0, 'Threshold in seconds on dumping benchmarks'),
('spacer.gpdr', BOOL, False, 'Use GPDR solving strategy for non-linear CHC'),
('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'),
('spacer.use_bg_invs', BOOL, False, 'Enable external background invariants'),
))

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

@ -493,7 +493,8 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
m_pob(nullptr), m_ctp(nullptr),
m_lvl(lvl), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(WEAKNESS_MAX),
m_external(false), m_blocked(false) {
m_external(false), m_blocked(false),
m_background(false) {
SASSERT(m_body);
normalize(m_body, m_body);
}
@ -505,7 +506,8 @@ lemma::lemma(pob_ref const &p) :
m_pob(p), m_ctp(nullptr),
m_lvl(p->level()), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(p->weakness()),
m_external(false), m_blocked(false) {
m_external(false), m_blocked(false),
m_background(false) {
SASSERT(m_pob);
m_pob->get_skolems(m_zks);
add_binding(m_pob->get_binding());
@ -519,8 +521,8 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
m_pob(p), m_ctp(nullptr),
m_lvl(p->level()), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(p->weakness()),
m_external(false), m_blocked(false)
{
m_external(false), m_blocked(false),
m_background(false) {
if (m_pob) {
m_pob->get_skolems(m_zks);
add_binding(m_pob->get_binding());
@ -921,10 +923,10 @@ void pred_transformer::simplify_formulas()
{m_frames.simplify_formulas ();}
expr_ref pred_transformer::get_formulas(unsigned level) const
expr_ref pred_transformer::get_formulas(unsigned level, bool bg) const
{
expr_ref_vector res(m);
m_frames.get_frame_geq_lemmas (level, res);
m_frames.get_frame_geq_lemmas (level, res, bg);
return mk_and(res);
}
@ -935,6 +937,7 @@ bool pred_transformer::propagate_to_next_level (unsigned src_level)
/// \brief adds a lemma to the solver and to child solvers
void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
{
SASSERT(!lemma->is_background());
unsigned lvl = lemma->level();
expr* l = lemma->get_expr();
SASSERT(!lemma->is_ground() || is_clause(m, l));
@ -975,8 +978,9 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only)
next_level(lvl), ground_only); }
}
bool pred_transformer::add_lemma (expr *e, unsigned lvl) {
bool pred_transformer::add_lemma (expr *e, unsigned lvl, bool bg) {
lemma_ref lem = alloc(lemma, m, e, lvl);
lem->set_background(bg);
return m_frames.add_lemma(lem.get());
}
@ -1217,15 +1221,18 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
}
void pred_transformer::add_cover(unsigned level, expr* property)
void pred_transformer::add_cover(unsigned level, expr* property, bool bg)
{
SASSERT(!bg || is_infty_level(level));
// replace bound variables by local constants.
expr_ref result(property, m), v(m), c(m);
expr_substitution sub(m);
proof_ref pr(m);
pr = m.mk_asserted(m.mk_true());
for (unsigned i = 0; i < sig_size(); ++i) {
c = m.mk_const(pm.o2n(sig(i), 0));
v = m.mk_var(i, sig(i)->get_range());
sub.insert(v, c);
sub.insert(v, c, pr);
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
@ -1236,13 +1243,38 @@ void pred_transformer::add_cover(unsigned level, expr* property)
expr_ref_vector lemmas(m);
flatten_and(result, lemmas);
for (unsigned i = 0, sz = lemmas.size(); i < sz; ++i) {
add_lemma(lemmas.get(i), level);
add_lemma(lemmas.get(i), level, bg);
}
}
void pred_transformer::propagate_to_infinity (unsigned level)
{m_frames.propagate_to_infinity (level);}
// compute a conjunction of all background facts
void pred_transformer::get_pred_bg_invs(expr_ref_vector& out) {
expr_ref inv(m), tmp1(m), tmp2(m);
ptr_vector<func_decl> preds;
for (auto kv : m_pt_rules) {
expr* tag = kv.m_value->tag();
datalog::rule const &r = kv.m_value->rule();
find_predecessors (r, preds);
for (unsigned i = 0, preds_sz = preds.size(); i < preds_sz; i++) {
func_decl* pre = preds[i];
pred_transformer &pt = ctx.get_pred_transformer(pre);
const lemma_ref_vector &invs = pt.get_bg_invs();
CTRACE("spacer", !invs.empty(),
tout << "add-bg-invariant: " << mk_pp (pre, m) << "\n";);
for (auto inv : invs) {
// tag -> inv1 ... tag -> invn
tmp1 = m.mk_implies(tag, inv->get_expr());
pm.formula_n2o(tmp1, tmp2, i);
out.push_back(tmp2);
TRACE("spacer", tout << tmp2 << "\n";);
}
}
}
}
/// \brief Returns true if the obligation is already blocked by current lemmas
@ -1344,6 +1376,14 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
expr_ref_vector post (m), reach_assumps (m);
post.push_back (n.post ());
flatten_and(post);
// if equality propagation is disabled in arithmetic, expand
// equality literals into two inequalities to increase the space
// for interpolation
if (!ctx.use_eq_prop()) {
expand_literals(m, post);
}
// populate reach_assumps
if (n.level () > 0 && !m_all_init) {
@ -1472,7 +1512,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
expr_ref lemma_expr(m);
lemma_expr = lem->get_expr();
expr_ref_vector conj(m), aux(m);
expr_ref_vector cand(m), aux(m), conj(m);
expr_ref gnd_lemma(m);
@ -1482,8 +1522,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
lemma_expr = gnd_lemma.get();
}
conj.push_back(mk_not(m, lemma_expr));
flatten_and (conj);
cand.push_back(mk_not(m, lemma_expr));
flatten_and (cand);
prop_solver::scoped_level _sl(*m_solver, level);
prop_solver::scoped_subset_core _sc (*m_solver, true);
@ -1494,9 +1534,12 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
if (ctx.use_ctp()) {mdl_ref_ptr = &mdl;}
m_solver->set_core(core);
m_solver->set_model(mdl_ref_ptr);
expr * bg = m_extend_lit.get ();
lbool r = m_solver->check_assumptions (conj, aux, m_transition_clause,
1, &bg, 1);
conj.push_back(m_extend_lit);
if (ctx.use_bg_invs()) get_pred_bg_invs(conj);
lbool r = m_solver->check_assumptions (cand, aux, m_transition_clause,
conj.size(), conj.c_ptr(), 1);
if (r == l_false) {
solver_level = m_solver->uses_level ();
lem->reset_ctp();
@ -1527,6 +1570,7 @@ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state,
m_solver->set_core(&core);
m_solver->set_model (nullptr);
expr_ref_vector aux (m);
if (ctx.use_bg_invs()) get_pred_bg_invs(conj);
conj.push_back (m_extend_lit);
lbool res = m_solver->check_assumptions (state, aux,
m_transition_clause,
@ -1941,14 +1985,27 @@ void pred_transformer::update_solver_with_rfs(prop_solver *solver,
}
/// pred_transformer::frames
bool pred_transformer::frames::add_lemma(lemma *new_lemma)
{
TRACE("spacer", tout << "add-lemma: " << pp_level(new_lemma->level()) << " "
<< m_pt.head()->get_name() << " "
<< mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
if (new_lemma->is_background()) {
SASSERT (is_infty_level(new_lemma->level()));
for (auto &l : m_bg_invs) {
if (l->get_expr() == new_lemma->get_expr()) return false;
}
TRACE("spacer", tout << "add-external-lemma: "
<< pp_level(new_lemma->level()) << " "
<< m_pt.head()->get_name() << " "
<< mk_pp(new_lemma->get_expr(), m_pt.get_ast_manager()) << "\n";);
m_bg_invs.push_back(new_lemma);
return true;
}
unsigned i = 0;
for (auto *old_lemma : m_lemmas) {
if (old_lemma->get_expr() == new_lemma->get_expr()) {
@ -2295,6 +2352,7 @@ void context::updt_params() {
m_use_restarts = m_params.spacer_restarts();
m_restart_initial_threshold = m_params.spacer_restart_initial_threshold();
m_pdr_bfs = m_params.spacer_gpdr_bfs();
m_use_bg_invs = m_params.spacer_use_bg_invs();
if (m_use_gpdr) {
// set options to be compatible with GPDR
@ -2423,36 +2481,38 @@ expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p)
if (m_rels.find(p, pt)) {
return pt->get_cover_delta(p_orig, level);
} else {
IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);
IF_VERBOSE(10, verbose_stream() << "did not find predicate "
<< p->get_name() << "\n";);
return expr_ref(m.mk_true(), m);
}
}
void context::add_cover(int level, func_decl* p, expr* property)
void context::add_cover(int level, func_decl* p, expr* property, bool bg)
{
scoped_proof _pf_(m);
pred_transformer* pt = nullptr;
if (!m_rels.find(p, pt)) {
pt = alloc(pred_transformer, *this, get_manager(), p);
m_rels.insert(p, pt);
IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);
IF_VERBOSE(10, verbose_stream() << "did not find predicate "
<< p->get_name() << "\n";);
}
unsigned lvl = (level == -1)?infty_level():((unsigned)level);
pt->add_cover(lvl, property);
pt->add_cover(lvl, property, bg);
}
void context::add_invariant (func_decl *p, expr *property)
{add_cover (infty_level(), p, property);}
{add_cover (infty_level(), p, property, true);}
expr_ref context::get_reachable(func_decl *p)
{
expr_ref context::get_reachable(func_decl *p) {
pred_transformer* pt = nullptr;
if (!m_rels.find(p, pt))
{ return expr_ref(m.mk_false(), m); }
return pt->get_reachable();
}
bool context::validate()
{
bool context::validate() {
if (!m_validate_result) { return true; }
std::stringstream msg;
@ -2483,7 +2543,7 @@ bool context::validate()
model_ref model;
vector<relation_info> rs;
model_converter_ref mc;
get_level_property(m_inductive_lvl, refs, rs);
get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
inductive_property ex(m, mc, rs);
ex.to_model(model);
var_subst vs(m, false);
@ -2624,13 +2684,13 @@ void context::init_lemma_generalizers()
}
void context::get_level_property(unsigned lvl, expr_ref_vector& res,
vector<relation_info>& rs) const {
vector<relation_info>& rs, bool with_bg) const {
for (auto const& kv : m_rels) {
pred_transformer* r = kv.m_value;
if (r->head() == m_query_pred) {
continue;
}
expr_ref conj = r->get_formulas(lvl);
expr_ref conj = r->get_formulas(lvl, with_bg);
m_pm.formula_n2o(0, false, conj);
res.push_back(conj);
ptr_vector<func_decl> sig(r->head()->get_arity(), r->sig());
@ -2662,7 +2722,7 @@ lbool context::solve(unsigned from_lvl)
IF_VERBOSE(1, {
expr_ref_vector refs(m);
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
model_converter_ref mc;
inductive_property ex(m, mc, rs);
verbose_stream() << ex.to_string();
@ -2844,7 +2904,7 @@ model_ref context::get_model()
model_ref model;
expr_ref_vector refs(m);
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
ex.to_model (model);
return model;
@ -2877,7 +2937,7 @@ expr_ref context::mk_unsat_answer() const
{
expr_ref_vector refs(m);
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
return ex.to_expr();
}

72
src/muz/spacer/spacer_context.h
View file

@ -128,8 +128,9 @@ class lemma {
unsigned m_init_lvl; // level at which lemma was created
unsigned m_bumped:16;
unsigned m_weakness:16;
unsigned m_external:1;
unsigned m_blocked:1;
unsigned m_external:1; // external lemma from another solver
unsigned m_blocked:1; // blocked by CTP
unsigned m_background:1; // background assumed fact
void mk_expr_core();
void mk_cube_core();
@ -163,6 +164,9 @@ public:
void set_external(bool ext){m_external = ext;}
bool external() { return m_external;}
void set_background(bool v) {m_background = v;}
bool is_background() {return m_background;}
bool is_blocked() {return m_blocked;}
void set_blocked(bool v) {m_blocked=v;}
@ -222,6 +226,7 @@ class pred_transformer {
pred_transformer &m_pt; // parent pred_transformer
lemma_ref_vector m_pinned_lemmas; // all created lemmas
lemma_ref_vector m_lemmas; // active lemmas
lemma_ref_vector m_bg_invs; // background (assumed) invariants
unsigned m_size; // num of frames
bool m_sorted; // true if m_lemmas is sorted by m_lt
@ -230,7 +235,8 @@ class pred_transformer {
void sort ();
public:
frames (pred_transformer &pt) : m_pt (pt), m_size(0), m_sorted (true) {}
frames (pred_transformer &pt) : m_pt (pt),
m_size(0), m_sorted (true) {}
~frames() {}
void simplify_formulas ();
@ -245,17 +251,25 @@ class pred_transformer {
}
}
}
void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out) const {
void get_frame_geq_lemmas (unsigned level, expr_ref_vector &out,
bool with_bg = false) const {
for (auto &lemma : m_lemmas) {
if (lemma->level() >= level) {
out.push_back(lemma->get_expr());
}
}
if (with_bg) {
for (auto &lemma : m_bg_invs)
out.push_back(lemma->get_expr());
}
}
unsigned size () const {return m_size;}
unsigned lemma_size () const {return m_lemmas.size ();}
void add_frame () {m_size++;}
const lemma_ref_vector& get_bg_invs() const {return m_bg_invs;}
unsigned size() const {return m_size;}
unsigned lemma_size() const {return m_lemmas.size ();}
unsigned bg_invs_size() const {return m_bg_invs.size();}
void add_frame() {m_size++;}
void inherit_frames (frames &other) {
for (auto &other_lemma : other.m_lemmas) {
lemma_ref new_lemma = alloc(lemma, m_pt.get_ast_manager(),
@ -265,6 +279,7 @@ class pred_transformer {
add_lemma(new_lemma.get());
}
m_sorted = false;
m_bg_invs.append(other.m_bg_invs);
}
bool add_lemma (lemma *new_lemma);
@ -418,6 +433,11 @@ class pred_transformer {
app_ref mk_fresh_rf_tag ();
// get tagged formulae of all of the background invariants for all of the
// predecessors of the current transformer
void get_pred_bg_invs(expr_ref_vector &out);
const lemma_ref_vector &get_bg_invs() const {return m_frames.get_bg_invs();}
public:
pred_transformer(context& ctx, manager& pm, func_decl* head);
~pred_transformer() {}
@ -448,7 +468,7 @@ public:
}
unsigned get_num_levels() const {return m_frames.size ();}
expr_ref get_cover_delta(func_decl* p_orig, int level);
void add_cover(unsigned level, expr* property);
void add_cover(unsigned level, expr* property, bool bg = false);
expr_ref get_reachable();
std::ostream& display(std::ostream& strm) const;
@ -484,7 +504,7 @@ public:
bool propagate_to_next_level(unsigned level);
void propagate_to_infinity(unsigned level);
/// \brief Add a lemma to the current context and all users
bool add_lemma(expr * lemma, unsigned lvl);
bool add_lemma(expr * e, unsigned lvl, bool bg);
bool add_lemma(lemma* lem) {return m_frames.add_lemma(lem);}
expr* get_reach_case_var (unsigned idx) const;
bool has_rfs () const { return !m_reach_facts.empty () ;}
@ -527,7 +547,7 @@ public:
bool check_inductive(unsigned level, expr_ref_vector& state,
unsigned& assumes_level, unsigned weakness = UINT_MAX);
expr_ref get_formulas(unsigned level) const;
expr_ref get_formulas(unsigned level, bool bg = false) const;
void simplify_formulas();
@ -958,6 +978,7 @@ class context {
bool m_simplify_formulas_pre;
bool m_simplify_formulas_post;
bool m_pdr_bfs;
bool m_use_bg_invs;
unsigned m_push_pob_max_depth;
unsigned m_max_level;
unsigned m_restart_initial_threshold;
@ -992,7 +1013,8 @@ class context {
// Generate inductive property
void get_level_property(unsigned lvl, expr_ref_vector& res,
vector<relation_info> & rs) const;
vector<relation_info> & rs,
bool with_bg = false) const;
// Initialization
@ -1027,18 +1049,20 @@ public:
const fp_params &get_params() const { return m_params; }
bool use_native_mbp () {return m_use_native_mbp;}
bool use_ground_pob () {return m_ground_pob;}
bool use_instantiate () {return m_instantiate;}
bool weak_abs() {return m_weak_abs;}
bool use_qlemmas () {return m_use_qlemmas;}
bool use_euf_gen() {return m_use_euf_gen;}
bool simplify_pob() {return m_simplify_pob;}
bool use_ctp() {return m_use_ctp;}
bool use_inc_clause() {return m_use_inc_clause;}
unsigned blast_term_ite_inflation() {return m_blast_term_ite_inflation;}
bool elim_aux() {return m_elim_aux;}
bool reach_dnf() {return m_reach_dnf;}
bool use_eq_prop() const {return m_use_eq_prop;}
bool use_native_mbp() const {return m_use_native_mbp;}
bool use_ground_pob() const {return m_ground_pob;}
bool use_instantiate() const {return m_instantiate;}
bool weak_abs() const {return m_weak_abs;}
bool use_qlemmas() const {return m_use_qlemmas;}
bool use_euf_gen() const {return m_use_euf_gen;}
bool simplify_pob() const {return m_simplify_pob;}
bool use_ctp() const {return m_use_ctp;}
bool use_inc_clause() const {return m_use_inc_clause;}
unsigned blast_term_ite_inflation() const {return m_blast_term_ite_inflation;}
bool elim_aux() const {return m_elim_aux;}
bool reach_dnf() const {return m_reach_dnf;}
bool use_bg_invs() const {return m_use_bg_invs;}
ast_manager& get_ast_manager() const {return m;}
manager& get_manager() {return m_pm;}
@ -1081,7 +1105,7 @@ public:
unsigned get_num_levels(func_decl* p);
expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
void add_cover(int level, func_decl* pred, expr* property);
void add_cover(int level, func_decl* pred, expr* property, bool bg = false);
expr_ref get_reachable (func_decl* p);
void add_invariant (func_decl *pred, expr* property);
model_ref get_model();

1
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -94,6 +94,7 @@ void prop_solver::add_level()
void prop_solver::ensure_level(unsigned lvl)
{
if (is_infty_level(lvl)) return;
while (lvl >= level_cnt()) {
add_level();
}

3
src/muz/spacer/spacer_util.h
View file

@ -48,7 +48,8 @@ namespace spacer {
}
inline bool is_infty_level(unsigned lvl) {
return lvl == infty_level ();
// XXX: level is 16 bits in class pob
return lvl >= 65535;
}
inline unsigned next_level(unsigned lvl) {

1
src/muz/transforms/CMakeLists.txt
View file

@ -25,6 +25,7 @@ z3_add_component(transforms
dl_mk_array_eq_rewrite.cpp
dl_mk_array_instantiation.cpp
dl_mk_elim_term_ite.cpp
dl_mk_synchronize.cpp
COMPONENT_DEPENDENCIES
dataflow
hilbert

376
src/muz/transforms/dl_mk_synchronize.cpp Normal file
View file

@ -0,0 +1,376 @@
/*++
Copyright (c) 2017-2018 Saint-Petersburg State University
Module Name:
dl_mk_synchronize.h
Abstract:
Rule transformer that attempts to merge recursive iterations
relaxing the shape of the inductive invariant.
Author:
Dmitry Mordvinov (dvvrd) 2017-05-24
Lidiia Chernigovskaia (LChernigovskaya) 2017-10-20
Revision History:
--*/
#include "muz/transforms/dl_mk_synchronize.h"
#include <algorithm>
namespace datalog {
typedef mk_synchronize::item_set_vector item_set_vector;
mk_synchronize::mk_synchronize(context& ctx, unsigned priority):
rule_transformer::plugin(priority, false),
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager())
{}
bool mk_synchronize::is_recursive(rule &r, func_decl &decl) const {
func_decl *hdecl = r.get_head()->get_decl();
// AG: shouldn't decl appear in the body?
if (hdecl == &decl) return true;
auto & strata = m_stratifier->get_strats();
unsigned num_of_stratum = m_stratifier->get_predicate_strat(hdecl);
return strata[num_of_stratum]->contains(&decl);
}
bool mk_synchronize::has_recursive_premise(app * app) const {
func_decl* app_decl = app->get_decl();
if (m_deps->get_deps(app_decl).contains(app_decl)) {
return true;
}
rule_stratifier::comp_vector const & strata = m_stratifier->get_strats();
unsigned num_of_stratum = m_stratifier->get_predicate_strat(app_decl);
return strata[num_of_stratum]->size() > 1;
}
item_set_vector mk_synchronize::add_merged_decls(ptr_vector<app> & apps) {
unsigned sz = apps.size();
item_set_vector merged_decls;
merged_decls.resize(sz);
auto & strata = m_stratifier->get_strats();
for (unsigned j = 0; j < sz; ++j) {
unsigned nos;
nos = m_stratifier->get_predicate_strat(apps[j]->get_decl());
merged_decls[j] = strata[nos];
}
return merged_decls;
}
void mk_synchronize::add_new_rel_symbols(unsigned idx,
item_set_vector const & decls,
ptr_vector<func_decl> & decls_buf,
bool & was_added) {
if (idx >= decls.size()) {
string_buffer<> buffer;
ptr_vector<sort> domain;
for (auto &d : decls_buf) {
buffer << d->get_name() << "!!";
domain.append(d->get_arity(), d->get_domain());
}
symbol new_name = symbol(buffer.c_str());
if (!m_cache.contains(new_name)) {
was_added = true;
func_decl* orig = decls_buf[0];
func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name,
symbol::null, domain.size(), domain.c_ptr(), orig);
m_cache.insert(new_name, product_pred);
}
return;
}
// -- compute Cartesian product of decls, and create a new
// -- predicate for each element of the product
for (auto &p : *decls[idx]) {
decls_buf[idx] = p;
add_new_rel_symbols(idx + 1, decls, decls_buf, was_added);
}
}
void mk_synchronize::replace_applications(rule & r, rule_set & rules,
ptr_vector<app> & apps) {
app_ref replacing = product_application(apps);
ptr_vector<app> new_tail;
svector<bool> new_tail_neg;
unsigned n = r.get_tail_size() - apps.size() + 1;
unsigned tail_idx = 0;
new_tail.resize(n);
new_tail_neg.resize(n);
new_tail[0] = replacing;
new_tail_neg[0] = false;
for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
app* tail = r.get_tail(i);
if (!apps.contains(tail)) {
++tail_idx;
new_tail[tail_idx] = tail;
new_tail_neg[tail_idx] = false;
}
}
for (unsigned i = r.get_positive_tail_size(); i < r.get_uninterpreted_tail_size(); ++i) {
++tail_idx;
new_tail[tail_idx] = r.get_tail(i);
new_tail_neg[tail_idx] = true;
}
for (unsigned i = r.get_uninterpreted_tail_size(); i < r.get_tail_size(); ++i) {
++tail_idx;
new_tail[tail_idx] = r.get_tail(i);
new_tail_neg[tail_idx] = false;
}
rule_ref new_rule(rm);
new_rule = rm.mk(r.get_head(), tail_idx + 1,
new_tail.c_ptr(), new_tail_neg.c_ptr(), symbol::null, false);
rules.replace_rule(&r, new_rule.get());
}
rule_ref mk_synchronize::rename_bound_vars_in_rule(rule * r,
unsigned & var_idx) {
// AG: shift all variables in a rule so that lowest var index is var_idx?
// AG: update var_idx in the process?
ptr_vector<sort> sorts;
r->get_vars(m, sorts);
expr_ref_vector revsub(m);
revsub.resize(sorts.size());
for (unsigned i = 0; i < sorts.size(); ++i) {
if (sorts[i]) {
revsub[i] = m.mk_var(var_idx++, sorts[i]);
}
}
rule_ref new_rule(rm);
new_rule = rm.mk(r);
rm.substitute(new_rule, revsub.size(), revsub.c_ptr());
return new_rule;
}
vector<rule_ref_vector> mk_synchronize::rename_bound_vars(item_set_vector const & heads,
rule_set & rules) {
// AG: is every item_set in heads corresponds to rules that are merged?
// AG: why are bound variables renamed in the first place?
// AG: the data structure seems too complex
vector<rule_ref_vector> result;
unsigned var_idx = 0;
for (auto item : heads) {
rule_ref_vector dst_vector(rm);
for (auto *head : *item) {
for (auto *r : rules.get_predicate_rules(head)) {
rule_ref new_rule = rename_bound_vars_in_rule(r, var_idx);
dst_vector.push_back(new_rule.get());
}
}
result.push_back(dst_vector);
}
return result;
}
void mk_synchronize::add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
app_ref_vector & new_tail,
svector<bool> & new_tail_neg,
unsigned & tail_idx) {
unsigned max_sz = 0;
for (auto &rc : recursive_calls)
max_sz= std::max(rc.size(), max_sz);
unsigned n = recursive_calls.size();
ptr_vector<app> merged_recursive_calls;
for (unsigned j = 0; j < max_sz; ++j) {
merged_recursive_calls.reset();
merged_recursive_calls.resize(n);
for (unsigned i = 0; i < n; ++i) {
unsigned sz = recursive_calls[i].size();
merged_recursive_calls[i] =
j < sz ? recursive_calls[i][j] : recursive_calls[i][sz - 1];
}
++tail_idx;
new_tail[tail_idx] = product_application(merged_recursive_calls);
new_tail_neg[tail_idx] = false;
}
}
void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail,
svector<bool> & new_tail_neg,
unsigned & tail_idx) {
for (unsigned i = 0, sz = r.get_positive_tail_size(); i < sz; ++i) {
app* tail = r.get_tail(i);
if (!is_recursive(r, *tail)) {
++tail_idx;
new_tail[tail_idx] = tail;
new_tail_neg[tail_idx] = false;
}
}
for (unsigned i = r.get_positive_tail_size(),
sz = r.get_uninterpreted_tail_size() ; i < sz; ++i) {
++tail_idx;
new_tail[tail_idx] = r.get_tail(i);
new_tail_neg[tail_idx] = true;
}
for (unsigned i = r.get_uninterpreted_tail_size(),
sz = r.get_tail_size(); i < sz; ++i) {
++tail_idx;
new_tail[tail_idx] = r.get_tail(i);
new_tail_neg[tail_idx] = r.is_neg_tail(i);
}
}
app_ref mk_synchronize::product_application(ptr_vector<app> const &apps) {
unsigned args_num = 0;
string_buffer<> buffer;
// AG: factor out into mk_name
for (auto *app : apps) {
buffer << app->get_decl()->get_name() << "!!";
args_num += app->get_num_args();
}
symbol name = symbol(buffer.c_str());
SASSERT(m_cache.contains(name));
func_decl * pred = m_cache[name];
ptr_vector<expr> args;
args.resize(args_num);
unsigned idx = 0;
for (auto *a : apps) {
for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i, ++idx)
args[idx] = a->get_arg(i);
}
return app_ref(m.mk_app(pred, args_num, args.c_ptr()), m);
}
rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) {
unsigned n = rules.size();
string_buffer<> buffer;
bool first_rule = true;
for (auto it = rules.begin(); it != rules.end(); ++it, first_rule = false) {
if (!first_rule) {
buffer << "+";
}
buffer << (*it)->name();
}
ptr_vector<app> heads;
heads.resize(n);
for (unsigned i = 0; i < n; ++i) {
heads[i] = rules[i]->get_head();
}
app_ref product_head = product_application(heads);
unsigned product_tail_length = 0;
bool has_recursion = false;
vector< ptr_vector<app> > recursive_calls;
recursive_calls.resize(n);
for (unsigned i = 0; i < n; ++i) {
rule& rule = *rules[i];
product_tail_length += rule.get_tail_size();
for (unsigned j = 0; j < rule.get_positive_tail_size(); ++j) {
app* tail = rule.get_tail(j);
if (is_recursive(rule, *tail)) {
has_recursion = true;
recursive_calls[i].push_back(tail);
}
}
if (recursive_calls[i].empty()) {
recursive_calls[i].push_back(rule.get_head());
}
}
app_ref_vector new_tail(m);
svector<bool> new_tail_neg;
new_tail.resize(product_tail_length);
new_tail_neg.resize(product_tail_length);
unsigned tail_idx = -1;
if (has_recursion) {
add_rec_tail(recursive_calls, new_tail, new_tail_neg, tail_idx);
}
for (rule_vector::const_iterator it = rules.begin(); it != rules.end(); ++it) {
rule& rule = **it;
add_non_rec_tail(rule, new_tail, new_tail_neg, tail_idx);
}
rule_ref new_rule(rm);
new_rule = rm.mk(product_head, tail_idx + 1,
new_tail.c_ptr(), new_tail_neg.c_ptr(), symbol(buffer.c_str()), false);
rm.fix_unbound_vars(new_rule, false);
return new_rule;
}
void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf,
vector<rule_ref_vector> const & merged_rules,
rule_set & all_rules) {
if (idx >= merged_rules.size()) {
rule_ref product = product_rule(buf);
all_rules.add_rule(product.get());
return;
}
for (auto *r : merged_rules[idx]) {
buf[idx] = r;
merge_rules(idx + 1, buf, merged_rules, all_rules);
}
}
void mk_synchronize::merge_applications(rule & r, rule_set & rules) {
ptr_vector<app> non_recursive_preds;
obj_hashtable<app> apps;
for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
app* t = r.get_tail(i);
if (!is_recursive(r, *t) && has_recursive_premise(t)) {
apps.insert(t);
}
}
if (apps.size() < 2) return;
for (auto *a : apps) non_recursive_preds.push_back(a);
item_set_vector merged_decls = add_merged_decls(non_recursive_preds);
unsigned n = non_recursive_preds.size();
ptr_vector<func_decl> decls_buf;
decls_buf.resize(n);
bool was_added = false;
add_new_rel_symbols(0, merged_decls, decls_buf, was_added);
if (was_added){
rule_ref_vector rules_buf(rm);
rules_buf.resize(n);
vector<rule_ref_vector> renamed_rules = rename_bound_vars(merged_decls, rules);
merge_rules(0, rules_buf, renamed_rules, rules);
}
replace_applications(r, rules, non_recursive_preds);
m_deps->populate(rules);
m_stratifier = alloc(rule_stratifier, *m_deps);
}
rule_set * mk_synchronize::operator()(rule_set const & source) {
rule_set* rules = alloc(rule_set, m_ctx);
rules->inherit_predicates(source);
for (auto *r : source) { rules->add_rule(r); }
m_deps = alloc(rule_dependencies, m_ctx);
m_deps->populate(*rules);
m_stratifier = alloc(rule_stratifier, *m_deps);
unsigned current_rule = 0;
while (current_rule < rules->get_num_rules()) {
rule *r = rules->get_rule(current_rule);
merge_applications(*r, *rules);
++current_rule;
}
return rules;
}
};

134
src/muz/transforms/dl_mk_synchronize.h Normal file
View file

@ -0,0 +1,134 @@
/*++
Copyright (c) 2017-2018 Saint-Petersburg State University
Module Name:
dl_mk_synchronize.h
Abstract:
Rule transformer that attempts to merge recursive iterations
relaxing the shape of the inductive invariant.
Example:
Q(z) :- A(x), B(y), phi1(x,y,z).
A(x) :- A(x'), phi2(x,x').
A(x) :- phi3(x).
B(y) :- C(y'), phi4(y,y').
C(y) :- B(y'), phi5(y,y').
B(y) :- phi6(y).
Transformed clauses:
Q(z) :- AB(x,y), phi1(x,y,z).
AB(x,y) :- AC(x',y'), phi2(x,x'), phi4(y,y').
AC(x,y) :- AB(x',y'), phi2(x,x'), phi5(y,y').
AB(x,y) :- AC(x, y'), phi3(x), phi4(y,y').
AC(x,y) :- AB(x, y'), phi3(x), phi5(y,y').
AB(x,y) :- AB(x',y), phi2(x,x'), phi6(y).
AB(x,y) :- phi3(x), phi6(y).
Author:
Dmitry Mordvinov (dvvrd) 2017-05-24
Lidiia Chernigovskaia (LChernigovskaya) 2017-10-20
Revision History:
--*/
#ifndef DL_MK_SYNCHRONIZE_H_
#define DL_MK_SYNCHRONIZE_H_
#include"muz/base/dl_context.h"
#include"muz/base/dl_rule_set.h"
#include"util/uint_set.h"
#include"muz/base/dl_rule_transformer.h"
#include"muz/transforms/dl_mk_rule_inliner.h"
namespace datalog {
/**
\brief Implements a synchronous product transformation.
*/
class mk_synchronize : public rule_transformer::plugin {
public:
typedef ptr_vector<rule_stratifier::item_set> item_set_vector;
private:
context& m_ctx;
ast_manager& m;
rule_manager& rm;
scoped_ptr<rule_dependencies> m_deps;
scoped_ptr<rule_stratifier> m_stratifier;
// symbol table that maps new predicate names to corresponding
// func_decl
map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> m_cache;
/// returns true if decl is recursive in the given rule
/// requires that decl appears in the tail of r
bool is_recursive(rule &r, func_decl &decl) const;
bool is_recursive(rule &r, expr &e) const {
SASSERT(is_app(&e));
return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl());
}
/// returns true if the top-level predicate of app is recursive
bool has_recursive_premise(app * app) const;
item_set_vector add_merged_decls(ptr_vector<app> & apps);
/**
Compute Cartesian product of decls and create a new
predicate for each element. For example, if decls is
( (a, b), (c, d) ) )
create new predicates: a!!c, a!!d, b!!c, and b!!d
*/
void add_new_rel_symbols(unsigned idx, item_set_vector const & decls,
ptr_vector<func_decl> & buf, bool & was_added);
/**
Convert vector of predicate apps into a single app. For example,
(Foo a) (Bar b) becomes (Foo!!Bar a b)
*/
app_ref product_application(ptr_vector<app> const & apps);
/**
Replace a given rule by a rule in which conjunction of
predicates is replaced by a single product predicate
*/
void replace_applications(rule & r, rule_set & rules,
ptr_vector<app> & apps);
rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx);
vector<rule_ref_vector> rename_bound_vars(item_set_vector const & heads,
rule_set & rules);
void add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
app_ref_vector & new_tail,
svector<bool> & new_tail_neg, unsigned & tail_idx);
void add_non_rec_tail(rule & r, app_ref_vector & new_tail,
svector<bool> & new_tail_neg,
unsigned & tail_idx);
rule_ref product_rule(rule_ref_vector const & rules);
void merge_rules(unsigned idx, rule_ref_vector & buf,
vector<rule_ref_vector> const & merged_rules, rule_set & all_rules);
void merge_applications(rule & r, rule_set & rules);
public:
/**
\brief Create synchronous product transformer.
*/
mk_synchronize(context & ctx, unsigned priority = 22500);
rule_set * operator()(rule_set const & source);
};
};
#endif /* DL_MK_SYNCHRONIZE_H_ */