From 4b2196f114b4db60fbd48fb3f389e324c1e5667f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Jun 2018 16:28:07 -0700 Subject: [PATCH] nits Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_unsat_core_learner.cpp | 3 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 82 +++++++---------- src/muz/spacer/spacer_unsat_core_plugin.h | 96 ++++++++------------ 3 files changed, 73 insertions(+), 108 deletions(-) diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index 5b3420800..da0d6ec34 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -44,8 +44,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) { if (m.get_num_parents(currentNode) > 0) { bool need_to_mark_closed = true; - for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) { - proof* premise = m.get_parent(currentNode, i); + for (proof* premise : m.get_parents(currentNode)) { need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise)); } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index 25b12cf25..eff05762b 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -37,8 +37,6 @@ namespace spacer { unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner): m(learner.m), m_learner(learner) {}; - - void unsat_core_plugin_lemma::compute_partial_core(proof* step) { SASSERT(m_learner.m_pr.is_a_marked(step)); SASSERT(m_learner.m_pr.is_b_marked(step)); @@ -103,12 +101,10 @@ namespace spacer { func_decl* d = step->get_decl(); symbol sym; if (!m_learner.is_closed(step) && // if step is not already interpolated - step->get_decl_kind() == PR_TH_LEMMA && // and step is a Farkas lemma - d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step - d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas", - d->get_parameter(1).is_symbol(sym) && sym == "farkas" && - d->get_num_parameters() >= m.get_num_parents(step) + 2) { // the following parameters are the Farkas coefficients + is_farkas_lemma(m, step)) { + // weaker check: d->get_num_parameters() >= m.get_num_parents(step) + 2 + SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); SASSERT(m.has_fact(step)); coeff_lits_t coeff_lits; @@ -142,12 +138,10 @@ namespace spacer { STRACE("spacer.farkas", verbose_stream() << "Farkas input: "<< "\n"; for (unsigned i = 0; i < m.get_num_parents(step); ++i) { - proof * prem = m.get_parent(step, i); - - rational coef = params[i].get_rational(); - + proof * prem = m.get_parent(step, i); + rational coef = params[i].get_rational(); bool b_pure = m_learner.m_pr.is_b_pure (prem); - verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n"; + verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; } ); @@ -197,11 +191,11 @@ namespace spacer { } SASSERT(m.get_num_parents(step) + 2 + num_args == d->get_num_parameters()); - bool_rewriter brw(m_learner.m); + bool_rewriter brw(m); for (unsigned i = 0; i < num_args; ++i) { expr* premise = args[i]; - expr_ref negatedPremise(m_learner.m); + expr_ref negatedPremise(m); brw.mk_not(premise, negatedPremise); pinned.push_back(negatedPremise); rational coefficient = params[i].get_rational(); @@ -235,8 +229,7 @@ namespace spacer { return util.get(); } else { - expr_ref negated_linear_combination = util.get(); - return expr_ref(mk_not(m, negated_linear_combination), m); + return expr_ref(mk_not(m, util.get()), m); } } @@ -248,15 +241,11 @@ namespace spacer { func_decl* d = step->get_decl(); symbol sym; if(!m_learner.is_closed(step) && // if step is not already interpolated - step->get_decl_kind() == PR_TH_LEMMA && // and step is a Farkas lemma - d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step - d->get_parameter(0).is_symbol(sym) && sym == "arith" && // the first two parameters are "arith", "farkas", - d->get_parameter(1).is_symbol(sym) && sym == "farkas" && - d->get_num_parameters() >= m.get_num_parents(step) + 2) // the following parameters are the Farkas coefficients - { + is_farkas_lemma(m, step)) { + SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); SASSERT(m.has_fact(step)); - vector > linear_combination; // collects all summands of the linear combination + coeff_lits_t linear_combination; // collects all summands of the linear combination parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient @@ -264,9 +253,7 @@ namespace spacer { verbose_stream() << "Farkas input: "<< "\n"; for (unsigned i = 0; i < m.get_num_parents(step); ++i) { proof * prem = m.get_parent(step, i); - - rational coef = params[i].get_rational(); - + rational coef = params[i].get_rational(); bool b_pure = m_learner.m_pr.is_b_pure (prem); verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n"; } @@ -284,8 +271,7 @@ namespace spacer { { rational coefficient = params[i].get_rational(); linear_combination.push_back - (std::make_pair(to_app(m.get_fact(premise)), - abs(coefficient))); + (std::make_pair(abs(coefficient), to_app(m.get_fact(premise)))); } else { @@ -308,15 +294,15 @@ namespace spacer { struct farkas_optimized_less_than_pairs { - inline bool operator() (const std::pair& pair1, const std::pair& pair2) const + inline bool operator() (const std::pair& pair1, const std::pair& pair2) const { - return (pair1.first->get_id() < pair2.first->get_id()); + return (pair1.second->get_id() < pair2.second->get_id()); } }; void unsat_core_plugin_farkas_lemma_optimized::finalize() { - if(m_linear_combinations.empty()) + if (m_linear_combinations.empty()) { return; } @@ -331,9 +317,9 @@ namespace spacer { unsigned counter = 0; for (const auto& linear_combination : m_linear_combinations) { for (const auto& pair : linear_combination) { - if (!map.contains(pair.first)) { - ordered_basis.push_back(pair.first); - map.insert(pair.first, counter++); + if (!map.contains(pair.second)) { + ordered_basis.push_back(pair.second); + map.insert(pair.second, counter++); } } } @@ -344,7 +330,7 @@ namespace spacer { for (unsigned i = 0; i < m_linear_combinations.size(); ++i) { auto linear_combination = m_linear_combinations[i]; for (const auto& pair : linear_combination) { - matrix.set(i, map[pair.first], pair.second); + matrix.set(i, map[pair.second], pair.first); } } @@ -368,9 +354,7 @@ namespace spacer { } - expr_ref unsat_core_plugin_farkas_lemma_optimized::compute_linear_combination(const coeff_lits_t& coeff_lits) - { - + expr_ref unsat_core_plugin_farkas_lemma_optimized::compute_linear_combination(const coeff_lits_t& coeff_lits) { smt::farkas_util util(m); for (auto const & p : coeff_lits) { util.add(p.first, p.second); @@ -387,7 +371,7 @@ namespace spacer { } DEBUG_CODE( for (auto& linear_combination : m_linear_combinations) { - SASSERT(linear_combination.size() > 0); + SASSERT(!linear_combination.empty()); }); // 1. construct ordered basis @@ -396,9 +380,9 @@ namespace spacer { unsigned counter = 0; for (const auto& linear_combination : m_linear_combinations) { for (const auto& pair : linear_combination) { - if (!map.contains(pair.first)) { - ordered_basis.push_back(pair.first); - map.insert(pair.first, counter++); + if (!map.contains(pair.second)) { + ordered_basis.push_back(pair.second); + map.insert(pair.second, counter++); } } } @@ -409,7 +393,7 @@ namespace spacer { for (unsigned i=0; i < m_linear_combinations.size(); ++i) { auto linear_combination = m_linear_combinations[i]; for (const auto& pair : linear_combination) { - matrix.set(i, map[pair.first], pair.second); + matrix.set(i, map[pair.second], pair.first); } } matrix.print_matrix(); @@ -695,14 +679,12 @@ namespace spacer { * computes min-cut on the graph constructed by compute_partial_core-method * and adds the corresponding lemmas to the core */ -void unsat_core_plugin_min_cut::finalize() -{ + void unsat_core_plugin_min_cut::finalize() { unsigned_vector cut_nodes; m_min_cut.compute_min_cut(cut_nodes); - - for (unsigned cut_node : cut_nodes) - { + + for (unsigned cut_node : cut_nodes) { m_learner.add_lemma_to_core(m_node_to_formula[cut_node]); - } - } + } + } } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.h b/src/muz/spacer/spacer_unsat_core_plugin.h index 44a3678b6..c05bcc5b9 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.h +++ b/src/muz/spacer/spacer_unsat_core_plugin.h @@ -23,66 +23,55 @@ Revision History: namespace spacer { -class unsat_core_learner; + class unsat_core_learner; -class unsat_core_plugin { -protected: - typedef vector> coeff_lits_t; - ast_manager& m; -public: - unsat_core_plugin(unsat_core_learner& learner); - virtual ~unsat_core_plugin() {}; - virtual void compute_partial_core(proof* step) = 0; - virtual void finalize(){}; + class unsat_core_plugin { + protected: + typedef vector> coeff_lits_t; + ast_manager& m; + public: + unsat_core_plugin(unsat_core_learner& learner); + virtual ~unsat_core_plugin() {}; + virtual void compute_partial_core(proof* step) = 0; + virtual void finalize(){}; + + unsat_core_learner& m_learner; + }; - unsat_core_learner& m_learner; -}; - - -class unsat_core_plugin_lemma : public unsat_core_plugin { - -public: - unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; - - void compute_partial_core(proof* step) override; - -private: - void add_lowest_split_to_core(proof* step) const; -}; - - -class unsat_core_plugin_farkas_lemma : public unsat_core_plugin { - -public: - unsat_core_plugin_farkas_lemma(unsat_core_learner& learner, - bool split_literals, - bool use_constant_from_a=true) : - unsat_core_plugin(learner), - m_split_literals(split_literals), - m_use_constant_from_a(use_constant_from_a) {}; - - void compute_partial_core(proof* step) override; - -private: - bool m_split_literals; - bool m_use_constant_from_a; - /* - * compute linear combination of literals 'literals' having coefficients 'coefficients' and save result in res - */ - expr_ref compute_linear_combination(const coeff_lits_t& coeff_lits); -}; - - class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin { + class unsat_core_plugin_lemma : public unsat_core_plugin { + public: + unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; + void compute_partial_core(proof* step) override; + private: + void add_lowest_split_to_core(proof* step) const; + }; + class unsat_core_plugin_farkas_lemma : public unsat_core_plugin { + public: + unsat_core_plugin_farkas_lemma(unsat_core_learner& learner, + bool split_literals, + bool use_constant_from_a=true) : + unsat_core_plugin(learner), + m_split_literals(split_literals), + m_use_constant_from_a(use_constant_from_a) {}; + void compute_partial_core(proof* step) override; + private: + bool m_split_literals; + bool m_use_constant_from_a; + /* + * compute linear combination of literals 'literals' having coefficients 'coefficients' and save result in res + */ + expr_ref compute_linear_combination(const coeff_lits_t& coeff_lits); + }; + + class unsat_core_plugin_farkas_lemma_optimized : public unsat_core_plugin { public: unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {}; - void compute_partial_core(proof* step) override; void finalize() override; - protected: - vector > > m_linear_combinations; + vector m_linear_combinations; /* * compute linear combination of literals 'literals' having coefficients 'coefficients' and save result in res */ @@ -90,22 +79,17 @@ private: }; class unsat_core_plugin_farkas_lemma_bounded : public unsat_core_plugin_farkas_lemma_optimized { - public: unsat_core_plugin_farkas_lemma_bounded(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin_farkas_lemma_optimized(learner, m) {}; - void finalize() override; }; class unsat_core_plugin_min_cut : public unsat_core_plugin { - public: unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m); - void compute_partial_core(proof* step) override; void finalize() override; private: - ast_mark m_visited; // saves for each node i whether the subproof with root i has already been added to the min-cut-problem obj_map m_proof_to_node_minus; // maps proof-steps to the corresponding minus-nodes (the ones which are closer to source) obj_map m_proof_to_node_plus; // maps proof-steps to the corresponding plus-nodes (the ones which are closer to sink)