From 533e9c5837f927359291e48c6684e1c6bf3836c8 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 1 Aug 2018 11:11:18 +0200 Subject: [PATCH 1/9] Expand equality literals when eq_prop is disabled When equality propagation is disabled for arithmetic, equality atoms are expanded into inequality for potentially better generalization with interpolation --- src/muz/spacer/spacer_context.cpp | 8 ++++++++ src/muz/spacer/spacer_context.h | 9 +++++---- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index f0e86f1a5..c4e606b77 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1344,6 +1344,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) { diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 48c27f96d..976259b6d 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -1027,11 +1027,12 @@ 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 use_eq_prop() {return m_use_eq_prop;} + 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_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;} From 0035d9b8cb1afa61aa031bf11e2fe213c0f82d92 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 13 Aug 2018 15:01:16 -0400 Subject: [PATCH 2/9] Background external invariants Background external invariants are constraints that are assumed to be true of the system. This commit introduces a mode in which background invariants are used only duing inductive generalization and lemma pushing, but not during predecessor computation. It is believed that this will be more efficient used of background external invariants since they will not be able to disturb how predecessors are generalized and computed. Based on a patch by Jorge Navas --- src/muz/base/fp_params.pyg | 1 + src/muz/spacer/spacer_context.cpp | 116 +++++++++++++++++++++--------- src/muz/spacer/spacer_context.h | 73 ++++++++++++------- 3 files changed, 132 insertions(+), 58 deletions(-) diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index 8cee99540..18eb85662 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -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'), )) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index c4e606b77..617266779 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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 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 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 @@ -1480,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); @@ -1490,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); @@ -1502,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(); @@ -1535,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, @@ -1949,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()) { @@ -2303,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 @@ -2431,36 +2481,36 @@ 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) { 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; @@ -2491,7 +2541,7 @@ bool context::validate() model_ref model; vector 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); @@ -2632,13 +2682,13 @@ void context::init_lemma_generalizers() } void context::get_level_property(unsigned lvl, expr_ref_vector& res, - vector& rs) const { + vector& 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 sig(r->head()->get_arity(), r->sig()); @@ -2670,7 +2720,7 @@ lbool context::solve(unsigned from_lvl) IF_VERBOSE(1, { expr_ref_vector refs(m); vector 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(); @@ -2852,7 +2902,7 @@ model_ref context::get_model() model_ref model; expr_ref_vector refs(m); vector 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(m_mc), rs); ex.to_model (model); return model; @@ -2885,7 +2935,7 @@ expr_ref context::mk_unsat_answer() const { expr_ref_vector refs(m); vector 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(m_mc), rs); return ex.to_expr(); } diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 976259b6d..0d8b2daf6 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -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 & rs) const; + vector & rs, + bool with_bg = false) const; // Initialization @@ -1027,19 +1049,20 @@ public: const fp_params &get_params() const { return m_params; } - bool use_eq_prop() {return m_use_eq_prop;} - 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;} @@ -1082,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(); From 3a01fd791b0b06ccf2439eaab8bce828dbbd7dbc Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 12 Jul 2018 22:38:29 +0300 Subject: [PATCH 3/9] Replace rule API --- src/muz/base/dl_rule_set.cpp | 59 +++++++++++++++++++++++------------- src/muz/base/dl_rule_set.h | 13 +++++--- 2 files changed, 46 insertions(+), 26 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index 5114fdca4..80af80266 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -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*)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"; } - + } }; diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index 736dd8888..e870e369c 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -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_ */ - From 84001225966ab74178c111e31fb9fb1be453b1dc Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 12 Jul 2018 22:38:46 +0300 Subject: [PATCH 4/9] mk_synchronize rule transformation --- src/muz/transforms/CMakeLists.txt | 1 + src/muz/transforms/dl_mk_synchronize.cpp | 378 +++++++++++++++++++++++ src/muz/transforms/dl_mk_synchronize.h | 98 ++++++ 3 files changed, 477 insertions(+) create mode 100644 src/muz/transforms/dl_mk_synchronize.cpp create mode 100644 src/muz/transforms/dl_mk_synchronize.h diff --git a/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt index e92aa1c2f..62272450c 100644 --- a/src/muz/transforms/CMakeLists.txt +++ b/src/muz/transforms/CMakeLists.txt @@ -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 diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp new file mode 100644 index 000000000..f691b69d8 --- /dev/null +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -0,0 +1,378 @@ +/*++ +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" + +namespace datalog { + + 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_app(rule & r, app * app) const { + func_decl* head_decl = r.get_head()->get_decl(); + func_decl* app_decl = app->get_decl(); + if (head_decl == app_decl) { + return true; + } + rule_stratifier::comp_vector const & strata = m_stratifier->get_strats(); + unsigned num_of_stratum = m_stratifier->get_predicate_strat(head_decl); + return strata[num_of_stratum]->contains(app_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; + } + + ptr_vector mk_synchronize::add_merged_decls(ptr_vector & apps) { + unsigned n = apps.size(); + ptr_vector merged_decls; + merged_decls.resize(n); + ptr_vector app_decls; + app_decls.resize(n); + for (unsigned j = 0; j < n; ++j) { + app_decls[j] = apps[j]->get_decl(); + } + rule_stratifier::comp_vector const & strata = m_stratifier->get_strats(); + for (unsigned j = 0; j < n; ++j) { + unsigned num_of_stratum = m_stratifier->get_predicate_strat(app_decls[j]); + merged_decls[j] = strata[num_of_stratum]; + } + return merged_decls; + } + + void mk_synchronize::add_new_rel_symbols(unsigned idx, ptr_vector const & decls, + ptr_vector & decls_buf, bool & was_added) { + if (idx >= decls.size()) { + string_buffer<> buffer; + ptr_vector domain; + ptr_vector::const_iterator it = decls_buf.begin(), end = decls_buf.end(); + for (; it != end; ++it) { + buffer << (*it)->get_name(); + buffer << "!!"; + domain.append((*it)->get_arity(), (*it)->get_domain()); + } + + symbol new_name = symbol(buffer.c_str()); + + if (!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); + cache.insert(new_name, product_pred); + } + return; + } + + rule_stratifier::item_set const & pred_decls = *decls[idx]; + for (rule_stratifier::item_set::iterator it = pred_decls.begin(); it != pred_decls.end(); ++it) { + decls_buf[idx] = *it; + add_new_rel_symbols(idx + 1, decls, decls_buf, was_added); + } + } + + void mk_synchronize::replace_applications(rule & r, rule_set & rules, ptr_vector & apps) { + app* replacing = product_application(apps); + + ptr_vector new_tail; + svector 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) { + ptr_vector 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 mk_synchronize::rename_bound_vars(ptr_vector const & heads, + rule_set & rules) { + vector result; + unsigned var_idx = 0; + for (unsigned i = 0; i < heads.size(); ++i) { + rule_ref_vector dst_vector(rm); + for (rule_stratifier::item_set::iterator it = heads[i]->begin(); it != heads[i]->end(); ++it) { + func_decl * head = *it; + rule_vector const & src_rules = rules.get_predicate_rules(head); + for (unsigned j = 0; j < src_rules.size(); ++j) { + rule_ref new_rule = rename_bound_vars_in_rule(src_rules[j], 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 > & recursive_calls, ptr_vector & new_tail, + svector & new_tail_neg, unsigned & tail_idx) { + int max_size = recursive_calls[0].size(); + unsigned n = recursive_calls.size(); + for (unsigned i = 0; i < n; ++i) { + if (recursive_calls[i].size() > max_size) { + max_size = recursive_calls[i].size(); + } + } + for (unsigned j = 0; j < max_size; ++j) { + ptr_vector merged_recursive_calls; + merged_recursive_calls.resize(n); + for (unsigned i = 0; i < n; ++i) { + unsigned cur_size = recursive_calls[i].size(); + j < cur_size ? merged_recursive_calls[i] = recursive_calls[i][j]: + merged_recursive_calls[i] = recursive_calls[i][cur_size - 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, ptr_vector & new_tail, svector & new_tail_neg, + unsigned & tail_idx) { + for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { + app* tail = r.get_tail(i); + if (!is_recursive_app(r, 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] = r.is_neg_tail(i); + } + } + + app* mk_synchronize::product_application(ptr_vector const &apps) { + ptr_vector::const_iterator it = apps.begin(), end = apps.end(); + unsigned args_num = 0; + string_buffer<> buffer; + + for (; it != end; ++it) { + buffer << (*it)->get_decl()->get_name(); + buffer << "!!"; + args_num += (*it)->get_num_args(); + } + + symbol name = symbol(buffer.c_str()); + SASSERT(cache.contains(name)); + func_decl * pred = cache[name]; + + ptr_vector args; + args.resize(args_num); + it = apps.begin(); + for (unsigned args_idx = 0; it != end; ++it) { + app* a = *it; + for (unsigned i = 0; i < a->get_num_args(); ++i, ++args_idx) { + args[args_idx] = a->get_arg(i); + } + } + + return m.mk_app(pred, args_num, args.c_ptr()); + } + + rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) { + unsigned n = rules.size(); + + string_buffer<> buffer; + bool first_rule = true; + for (rule_ref_vector::iterator it = rules.begin(); it != rules.end(); ++it, first_rule = false) { + if (!first_rule) { + buffer << "+"; + } + buffer << (*it)->name(); + } + + ptr_vector heads; + heads.resize(n); + for (unsigned i = 0; i < n; ++i) { + heads[i] = rules[i]->get_head(); + } + app* product_head = product_application(heads); + unsigned product_tail_length = 0; + bool has_recursion = false; + vector< ptr_vector > 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_app(rule, tail)) { + has_recursion = true; + recursive_calls[i].push_back(tail); + } + } + if (recursive_calls[i].empty()) { + recursive_calls[i].push_back(rule.get_head()); + } + } + + ptr_vector new_tail; + svector 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 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; + } + + rule_ref_vector const & pred_rules = merged_rules[idx]; + for (rule_ref_vector::iterator it = pred_rules.begin(); it != pred_rules.end(); ++it) { + buf[idx] = *it; + merge_rules(idx + 1, buf, merged_rules, all_rules); + } + } + + void mk_synchronize::merge_applications(rule & r, rule_set & rules) { + ptr_vector non_recursive_applications; + obj_hashtable apps; + for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { + app* application = r.get_tail(i); + if (!is_recursive_app(r, application) && has_recursive_premise(application)) { + apps.insert(application); + } + } + if (apps.size() < 2) { + return; + } + + for (obj_hashtable::iterator it = apps.begin(); it != apps.end(); it++) { + non_recursive_applications.push_back(*it); + } + + ptr_vector merged_decls = add_merged_decls(non_recursive_applications); + + unsigned n = non_recursive_applications.size(); + ptr_vector 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 renamed_rules = rename_bound_vars(merged_decls, rules); + merge_rules(0, rules_buf, renamed_rules, rules); + } + + replace_applications(r, rules, non_recursive_applications); + 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); + + rule_set::iterator it = source.begin(), end = source.end(); + for (; it != end; ++it) { + rules->add_rule(*it); + } + + 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; + } + +}; diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h new file mode 100644 index 000000000..e4ce7cad1 --- /dev/null +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -0,0 +1,98 @@ +/*++ +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 { + context& m_ctx; + ast_manager& m; + rule_manager& rm; + + scoped_ptr m_deps; + scoped_ptr m_stratifier; + map cache; + + bool is_recursive_app(rule & r, app * app) const; + bool has_recursive_premise(app * app) const; + + ptr_vector add_merged_decls(ptr_vector & apps); + void add_new_rel_symbols(unsigned idx, ptr_vector const & decls, + ptr_vector & buf, bool & was_added); + + void replace_applications(rule & r, rule_set & rules, ptr_vector & apps); + + rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx); + vector rename_bound_vars(ptr_vector const & heads, rule_set & rules); + + void add_rec_tail(vector< ptr_vector > & recursive_calls, ptr_vector & new_tail, + svector & new_tail_neg, unsigned & tail_idx); + void add_non_rec_tail(rule & r, ptr_vector & new_tail, svector & new_tail_neg, + unsigned & tail_idx); + + app* product_application(ptr_vector const & apps); + rule_ref product_rule(rule_ref_vector const & rules); + + void merge_rules(unsigned idx, rule_ref_vector & buf, + 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_ */ From 0516e6f21f9a99931f4cea789e4cf031e49656b5 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 24 Jul 2018 11:45:40 -0400 Subject: [PATCH 5/9] Integrating synchronize pass --- src/muz/transforms/dl_mk_synchronize.cpp | 174 +++++++++++------------ src/muz/transforms/dl_mk_synchronize.h | 30 ++-- 2 files changed, 105 insertions(+), 99 deletions(-) diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index f691b69d8..268c994d1 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -22,6 +22,8 @@ Revision History: 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), @@ -29,15 +31,16 @@ namespace datalog { rm(ctx.get_rule_manager()) {} - bool mk_synchronize::is_recursive_app(rule & r, app * app) const { - func_decl* head_decl = r.get_head()->get_decl(); - func_decl* app_decl = app->get_decl(); - if (head_decl == app_decl) { - return true; - } - rule_stratifier::comp_vector const & strata = m_stratifier->get_strats(); - unsigned num_of_stratum = m_stratifier->get_predicate_strat(head_decl); - return strata[num_of_stratum]->contains(app_decl); + 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::is_recursive(rule &r, expr &e) const { + return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl()); } bool mk_synchronize::has_recursive_premise(app * app) const { @@ -50,33 +53,29 @@ namespace datalog { return strata[num_of_stratum]->size() > 1; } - ptr_vector mk_synchronize::add_merged_decls(ptr_vector & apps) { - unsigned n = apps.size(); - ptr_vector merged_decls; - merged_decls.resize(n); - ptr_vector app_decls; - app_decls.resize(n); - for (unsigned j = 0; j < n; ++j) { - app_decls[j] = apps[j]->get_decl(); - } - rule_stratifier::comp_vector const & strata = m_stratifier->get_strats(); - for (unsigned j = 0; j < n; ++j) { - unsigned num_of_stratum = m_stratifier->get_predicate_strat(app_decls[j]); - merged_decls[j] = strata[num_of_stratum]; + item_set_vector mk_synchronize::add_merged_decls(ptr_vector & 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, ptr_vector const & decls, - ptr_vector & decls_buf, bool & was_added) { + void mk_synchronize::add_new_rel_symbols(unsigned idx, + item_set_vector const & decls, + ptr_vector & decls_buf, + bool & was_added) { if (idx >= decls.size()) { string_buffer<> buffer; ptr_vector domain; - ptr_vector::const_iterator it = decls_buf.begin(), end = decls_buf.end(); - for (; it != end; ++it) { - buffer << (*it)->get_name(); - buffer << "!!"; - domain.append((*it)->get_arity(), (*it)->get_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()); @@ -84,6 +83,7 @@ namespace datalog { if (!cache.contains(new_name)) { was_added = true; func_decl* orig = decls_buf[0]; + // AG : is this ref counted func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name, symbol::null, domain.size(), domain.c_ptr(), orig); cache.insert(new_name, product_pred); @@ -91,15 +91,16 @@ namespace datalog { return; } - rule_stratifier::item_set const & pred_decls = *decls[idx]; - for (rule_stratifier::item_set::iterator it = pred_decls.begin(); it != pred_decls.end(); ++it) { - decls_buf[idx] = *it; + // AG: why recursive? + 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 & apps) { - app* replacing = product_application(apps); + void mk_synchronize::replace_applications(rule & r, rule_set & rules, + ptr_vector & apps) { + app_ref replacing = product_application(apps); ptr_vector new_tail; svector new_tail_neg; @@ -135,7 +136,10 @@ namespace datalog { rules.replace_rule(&r, new_rule.get()); } - rule_ref mk_synchronize::rename_bound_vars_in_rule(rule * r, unsigned & var_idx) { + 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 sorts; r->get_vars(m, sorts); expr_ref_vector revsub(m); @@ -152,17 +156,18 @@ namespace datalog { return new_rule; } - vector mk_synchronize::rename_bound_vars(ptr_vector const & heads, - rule_set & rules) { + 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 result; unsigned var_idx = 0; - for (unsigned i = 0; i < heads.size(); ++i) { + for (auto item : heads) { rule_ref_vector dst_vector(rm); - for (rule_stratifier::item_set::iterator it = heads[i]->begin(); it != heads[i]->end(); ++it) { - func_decl * head = *it; - rule_vector const & src_rules = rules.get_predicate_rules(head); - for (unsigned j = 0; j < src_rules.size(); ++j) { - rule_ref new_rule = rename_bound_vars_in_rule(src_rules[j], var_idx); + 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()); } } @@ -171,9 +176,11 @@ namespace datalog { return result; } - void mk_synchronize::add_rec_tail(vector< ptr_vector > & recursive_calls, ptr_vector & new_tail, - svector & new_tail_neg, unsigned & tail_idx) { - int max_size = recursive_calls[0].size(); + void mk_synchronize::add_rec_tail(vector< ptr_vector > & recursive_calls, + app_ref_vector & new_tail, + svector & new_tail_neg, + unsigned & tail_idx) { + int max_size = 0; unsigned n = recursive_calls.size(); for (unsigned i = 0; i < n; ++i) { if (recursive_calls[i].size() > max_size) { @@ -194,11 +201,12 @@ namespace datalog { } } - void mk_synchronize::add_non_rec_tail(rule & r, ptr_vector & new_tail, svector & new_tail_neg, - unsigned & tail_idx) { + void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail, + svector & new_tail_neg, + unsigned & tail_idx) { for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { app* tail = r.get_tail(i); - if (!is_recursive_app(r, tail)) { + if (!is_recursive(r, *tail)) { ++tail_idx; new_tail[tail_idx] = tail; new_tail_neg[tail_idx] = false; @@ -216,15 +224,14 @@ namespace datalog { } } - app* mk_synchronize::product_application(ptr_vector const &apps) { - ptr_vector::const_iterator it = apps.begin(), end = apps.end(); + app_ref mk_synchronize::product_application(ptr_vector const &apps) { unsigned args_num = 0; string_buffer<> buffer; - for (; it != end; ++it) { - buffer << (*it)->get_decl()->get_name(); - buffer << "!!"; - args_num += (*it)->get_num_args(); + // 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()); @@ -233,15 +240,13 @@ namespace datalog { ptr_vector args; args.resize(args_num); - it = apps.begin(); - for (unsigned args_idx = 0; it != end; ++it) { - app* a = *it; - for (unsigned i = 0; i < a->get_num_args(); ++i, ++args_idx) { - args[args_idx] = a->get_arg(i); - } + 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 m.mk_app(pred, args_num, args.c_ptr()); + return app_ref(m.mk_app(pred, args_num, args.c_ptr()), m); } rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) { @@ -261,7 +266,7 @@ namespace datalog { for (unsigned i = 0; i < n; ++i) { heads[i] = rules[i]->get_head(); } - app* product_head = product_application(heads); + app_ref product_head = product_application(heads); unsigned product_tail_length = 0; bool has_recursion = false; vector< ptr_vector > recursive_calls; @@ -271,7 +276,7 @@ namespace datalog { 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_app(rule, tail)) { + if (is_recursive(rule, *tail)) { has_recursion = true; recursive_calls[i].push_back(tail); } @@ -281,7 +286,7 @@ namespace datalog { } } - ptr_vector new_tail; + app_ref_vector new_tail(m); svector new_tail_neg; new_tail.resize(product_tail_length); new_tail_neg.resize(product_tail_length); @@ -302,41 +307,36 @@ namespace datalog { return new_rule; } - void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf, vector const & merged_rules, - rule_set & all_rules) { + void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf, + 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; } - rule_ref_vector const & pred_rules = merged_rules[idx]; - for (rule_ref_vector::iterator it = pred_rules.begin(); it != pred_rules.end(); ++it) { - buf[idx] = *it; + 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 non_recursive_applications; + ptr_vector non_recursive_preds; obj_hashtable apps; for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { - app* application = r.get_tail(i); - if (!is_recursive_app(r, application) && has_recursive_premise(application)) { - apps.insert(application); + app* t = r.get_tail(i); + if (!is_recursive(r, *t) && has_recursive_premise(t)) { + apps.insert(t); } } - if (apps.size() < 2) { - return; - } + if (apps.size() < 2) return; + for (auto *a : apps) non_recursive_preds.push_back(a); - for (obj_hashtable::iterator it = apps.begin(); it != apps.end(); it++) { - non_recursive_applications.push_back(*it); - } + item_set_vector merged_decls = add_merged_decls(non_recursive_preds); - ptr_vector merged_decls = add_merged_decls(non_recursive_applications); - - unsigned n = non_recursive_applications.size(); + unsigned n = non_recursive_preds.size(); ptr_vector decls_buf; decls_buf.resize(n); bool was_added = false; @@ -348,7 +348,7 @@ namespace datalog { merge_rules(0, rules_buf, renamed_rules, rules); } - replace_applications(r, rules, non_recursive_applications); + replace_applications(r, rules, non_recursive_preds); m_deps->populate(rules); m_stratifier = alloc(rule_stratifier, *m_deps); } @@ -357,10 +357,7 @@ namespace datalog { rule_set* rules = alloc(rule_set, m_ctx); rules->inherit_predicates(source); - rule_set::iterator it = source.begin(), end = source.end(); - for (; it != end; ++it) { - rules->add_rule(*it); - } + for (auto *r : source) { rules->add_rule(r); } m_deps = alloc(rule_dependencies, m_ctx); m_deps->populate(*rules); @@ -372,6 +369,7 @@ namespace datalog { merge_applications(*r, *rules); ++current_rule; } + return rules; } diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index e4ce7cad1..767f09f6e 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -52,6 +52,9 @@ namespace datalog { \brief Implements a synchronous product transformation. */ class mk_synchronize : public rule_transformer::plugin { + public: + typedef ptr_vector item_set_vector; + private: context& m_ctx; ast_manager& m; rule_manager& rm; @@ -59,25 +62,30 @@ namespace datalog { scoped_ptr m_deps; scoped_ptr m_stratifier; map cache; + bool is_recursive(rule &r, func_decl &decl) const; + bool is_recursive(rule &r, expr &e) const; - bool is_recursive_app(rule & r, app * app) const; bool has_recursive_premise(app * app) const; - ptr_vector add_merged_decls(ptr_vector & apps); - void add_new_rel_symbols(unsigned idx, ptr_vector const & decls, - ptr_vector & buf, bool & was_added); + item_set_vector add_merged_decls(ptr_vector & apps); + void add_new_rel_symbols(unsigned idx, item_set_vector const & decls, + ptr_vector & buf, bool & was_added); - void replace_applications(rule & r, rule_set & rules, ptr_vector & apps); + void replace_applications(rule & r, rule_set & rules, + ptr_vector & apps); rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx); - vector rename_bound_vars(ptr_vector const & heads, rule_set & rules); + vector rename_bound_vars(item_set_vector const & heads, + rule_set & rules); - void add_rec_tail(vector< ptr_vector > & recursive_calls, ptr_vector & new_tail, - svector & new_tail_neg, unsigned & tail_idx); - void add_non_rec_tail(rule & r, ptr_vector & new_tail, svector & new_tail_neg, - unsigned & tail_idx); + void add_rec_tail(vector< ptr_vector > & recursive_calls, + app_ref_vector & new_tail, + svector & new_tail_neg, unsigned & tail_idx); + void add_non_rec_tail(rule & r, app_ref_vector & new_tail, + svector & new_tail_neg, + unsigned & tail_idx); - app* product_application(ptr_vector const & apps); + app_ref product_application(ptr_vector const & apps); rule_ref product_rule(rule_ref_vector const & rules); void merge_rules(unsigned idx, rule_ref_vector & buf, From 24044429a792008622ee49b505f0edd4a635f882 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 20 Aug 2018 15:24:11 -0400 Subject: [PATCH 6/9] Rename cache to m_cache --- src/muz/transforms/dl_mk_synchronize.cpp | 8 ++++---- src/muz/transforms/dl_mk_synchronize.h | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index 268c994d1..af2a6f8d3 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -80,13 +80,13 @@ namespace datalog { symbol new_name = symbol(buffer.c_str()); - if (!cache.contains(new_name)) { + if (!m_cache.contains(new_name)) { was_added = true; func_decl* orig = decls_buf[0]; // AG : is this ref counted func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name, symbol::null, domain.size(), domain.c_ptr(), orig); - cache.insert(new_name, product_pred); + m_cache.insert(new_name, product_pred); } return; } @@ -235,8 +235,8 @@ namespace datalog { } symbol name = symbol(buffer.c_str()); - SASSERT(cache.contains(name)); - func_decl * pred = cache[name]; + SASSERT(m_cache.contains(name)); + func_decl * pred = m_cache[name]; ptr_vector args; args.resize(args_num); diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 767f09f6e..50d748bfa 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -61,7 +61,7 @@ namespace datalog { scoped_ptr m_deps; scoped_ptr m_stratifier; - map cache; + map m_cache; bool is_recursive(rule &r, func_decl &decl) const; bool is_recursive(rule &r, expr &e) const; From 7bff74dec08a4ce700672c0fd3b03f3edc5a47ab Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 20 Aug 2018 16:11:19 -0400 Subject: [PATCH 7/9] Minor pass on synchronize transform --- src/muz/transforms/dl_mk_synchronize.cpp | 40 ++++++++++++------------ src/muz/transforms/dl_mk_synchronize.h | 36 ++++++++++++++++++--- 2 files changed, 52 insertions(+), 24 deletions(-) diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index af2a6f8d3..348c9b5de 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -19,6 +19,7 @@ Revision History: --*/ #include "muz/transforms/dl_mk_synchronize.h" +#include namespace datalog { @@ -39,9 +40,6 @@ namespace datalog { unsigned num_of_stratum = m_stratifier->get_predicate_strat(hdecl); return strata[num_of_stratum]->contains(&decl); } - bool mk_synchronize::is_recursive(rule &r, expr &e) const { - return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl()); - } bool mk_synchronize::has_recursive_premise(app * app) const { func_decl* app_decl = app->get_decl(); @@ -83,7 +81,6 @@ namespace datalog { if (!m_cache.contains(new_name)) { was_added = true; func_decl* orig = decls_buf[0]; - // AG : is this ref counted 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); @@ -91,7 +88,8 @@ namespace datalog { return; } - // AG: why recursive? + // -- 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); @@ -180,20 +178,20 @@ namespace datalog { app_ref_vector & new_tail, svector & new_tail_neg, unsigned & tail_idx) { - int max_size = 0; + unsigned max_sz = 0; + for (auto &rc : recursive_calls) + max_sz= std::max(rc.size(), max_sz); + unsigned n = recursive_calls.size(); - for (unsigned i = 0; i < n; ++i) { - if (recursive_calls[i].size() > max_size) { - max_size = recursive_calls[i].size(); - } - } - for (unsigned j = 0; j < max_size; ++j) { - ptr_vector merged_recursive_calls; + ptr_vector 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 cur_size = recursive_calls[i].size(); - j < cur_size ? merged_recursive_calls[i] = recursive_calls[i][j]: - merged_recursive_calls[i] = recursive_calls[i][cur_size - 1]; + 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); @@ -204,7 +202,7 @@ namespace datalog { void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail, svector & new_tail_neg, unsigned & tail_idx) { - for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { + 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; @@ -212,12 +210,14 @@ namespace datalog { new_tail_neg[tail_idx] = false; } } - for (unsigned i = r.get_positive_tail_size(); i < r.get_uninterpreted_tail_size(); ++i) { + 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(); i < r.get_tail_size(); ++i) { + 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); @@ -254,7 +254,7 @@ namespace datalog { string_buffer<> buffer; bool first_rule = true; - for (rule_ref_vector::iterator it = rules.begin(); it != rules.end(); ++it, first_rule = false) { + for (auto it = rules.begin(); it != rules.end(); ++it, first_rule = false) { if (!first_rule) { buffer << "+"; } diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 50d748bfa..6f4b3ca40 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -61,16 +61,45 @@ namespace datalog { scoped_ptr m_deps; scoped_ptr m_stratifier; - map m_cache; - bool is_recursive(rule &r, func_decl &decl) const; - bool is_recursive(rule &r, expr &e) const; + // symbol table that maps new predicate names to corresponding + // func_decl + map 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 & 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 & 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 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 & apps); @@ -85,7 +114,6 @@ namespace datalog { svector & new_tail_neg, unsigned & tail_idx); - app_ref product_application(ptr_vector const & apps); rule_ref product_rule(rule_ref_vector const & rules); void merge_rules(unsigned idx, rule_ref_vector & buf, From 5d2f682f7a0730e87b631d2b97e102f5b82e9ff2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 4 Sep 2018 15:29:14 -0400 Subject: [PATCH 8/9] Enable proof mode in add_cover --- src/muz/spacer/spacer_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 617266779..dd6656954 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2489,6 +2489,8 @@ expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p) 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); From f67346d16e6abe41d5a0e2b664103914a1be1d74 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 4 Sep 2018 21:48:07 -0400 Subject: [PATCH 9/9] Fix is_infty_level to treat 2^16-1 as infinity --- src/muz/spacer/spacer_prop_solver.cpp | 1 + src/muz/spacer/spacer_util.h | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 004ea6754..4899ad692 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -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(); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index 8da574d0e..0328d8640 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -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) {