mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

nits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-06 16:28:07 -07:00 • committed by Arie Gurfinkel
parent 6adaed718f
commit 4b2196f114
3 changed files with 73 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -44,8 +44,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
if (m.get_num_parents(currentNode) > 0) { if (m.get_num_parents(currentNode) > 0) {
bool need_to_mark_closed = true; bool need_to_mark_closed = true;
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) { for (proof* premise : m.get_parents(currentNode)) {
proof* premise = m.get_parent(currentNode, i);
need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise)); need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
} }

70
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -37,8 +37,6 @@ namespace spacer {
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner): unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner):
m(learner.m), m_learner(learner) {}; m(learner.m), m_learner(learner) {};
void unsat_core_plugin_lemma::compute_partial_core(proof* step) { 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_a_marked(step));
SASSERT(m_learner.m_pr.is_b_marked(step)); SASSERT(m_learner.m_pr.is_b_marked(step));
@ -103,12 +101,10 @@ namespace spacer {
func_decl* d = step->get_decl(); func_decl* d = step->get_decl();
symbol sym; symbol sym;
if (!m_learner.is_closed(step) && // if step is not already interpolated 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 is_farkas_lemma(m, step)) {
d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step // weaker check: d->get_num_parameters() >= m.get_num_parents(step) + 2
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
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
SASSERT(m.has_fact(step)); SASSERT(m.has_fact(step));
coeff_lits_t coeff_lits; coeff_lits_t coeff_lits;
@ -143,11 +139,9 @@ namespace spacer {
verbose_stream() << "Farkas input: "<< "\n"; verbose_stream() << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) { for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(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); 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()); 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) { for (unsigned i = 0; i < num_args; ++i) {
expr* premise = args[i]; expr* premise = args[i];
expr_ref negatedPremise(m_learner.m); expr_ref negatedPremise(m);
brw.mk_not(premise, negatedPremise); brw.mk_not(premise, negatedPremise);
pinned.push_back(negatedPremise); pinned.push_back(negatedPremise);
rational coefficient = params[i].get_rational(); rational coefficient = params[i].get_rational();
@ -235,8 +229,7 @@ namespace spacer {
return util.get(); return util.get();
} }
else { else {
expr_ref negated_linear_combination = util.get(); return expr_ref(mk_not(m, util.get()), m);
return expr_ref(mk_not(m, negated_linear_combination), m);
} }
} }
@ -248,15 +241,11 @@ namespace spacer {
func_decl* d = step->get_decl(); func_decl* d = step->get_decl();
symbol sym; symbol sym;
if(!m_learner.is_closed(step) && // if step is not already interpolated 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 is_farkas_lemma(m, step)) {
d->get_num_parameters() >= 2 && // the Farkas coefficients are saved in the parameters of step SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
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
{
SASSERT(m.has_fact(step)); SASSERT(m.has_fact(step));
vector<std::pair<app*,rational> > 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 parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
@ -264,9 +253,7 @@ namespace spacer {
verbose_stream() << "Farkas input: "<< "\n"; verbose_stream() << "Farkas input: "<< "\n";
for (unsigned i = 0; i < m.get_num_parents(step); ++i) { for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
proof * prem = m.get_parent(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); 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_learner.m) << "\n";
} }
@ -284,8 +271,7 @@ namespace spacer {
{ {
rational coefficient = params[i].get_rational(); rational coefficient = params[i].get_rational();
linear_combination.push_back linear_combination.push_back
(std::make_pair(to_app(m.get_fact(premise)), (std::make_pair(abs(coefficient), to_app(m.get_fact(premise))));
abs(coefficient)));
} }
else else
{ {
@ -308,15 +294,15 @@ namespace spacer {
struct farkas_optimized_less_than_pairs struct farkas_optimized_less_than_pairs
{ {
inline bool operator() (const std::pair<app*,rational>& pair1, const std::pair<app*,rational>& pair2) const inline bool operator() (const std::pair<rational, app*>& pair1, const std::pair<rational, app*>& 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() void unsat_core_plugin_farkas_lemma_optimized::finalize()
{ {
if(m_linear_combinations.empty()) if (m_linear_combinations.empty())
{ {
return; return;
} }
@ -331,9 +317,9 @@ namespace spacer {
unsigned counter = 0; unsigned counter = 0;
for (const auto& linear_combination : m_linear_combinations) { for (const auto& linear_combination : m_linear_combinations) {
for (const auto& pair : linear_combination) { for (const auto& pair : linear_combination) {
if (!map.contains(pair.first)) { if (!map.contains(pair.second)) {
ordered_basis.push_back(pair.first); ordered_basis.push_back(pair.second);
map.insert(pair.first, counter++); map.insert(pair.second, counter++);
} }
} }
} }
@ -344,7 +330,7 @@ namespace spacer {
for (unsigned i = 0; i < m_linear_combinations.size(); ++i) { for (unsigned i = 0; i < m_linear_combinations.size(); ++i) {
auto linear_combination = m_linear_combinations[i]; auto linear_combination = m_linear_combinations[i];
for (const auto& pair : linear_combination) { 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); smt::farkas_util util(m);
for (auto const & p : coeff_lits) { for (auto const & p : coeff_lits) {
util.add(p.first, p.second); util.add(p.first, p.second);
@ -387,7 +371,7 @@ namespace spacer {
} }
DEBUG_CODE( DEBUG_CODE(
for (auto& linear_combination : m_linear_combinations) { for (auto& linear_combination : m_linear_combinations) {
SASSERT(linear_combination.size() > 0); SASSERT(!linear_combination.empty());
}); });
// 1. construct ordered basis // 1. construct ordered basis
@ -396,9 +380,9 @@ namespace spacer {
unsigned counter = 0; unsigned counter = 0;
for (const auto& linear_combination : m_linear_combinations) { for (const auto& linear_combination : m_linear_combinations) {
for (const auto& pair : linear_combination) { for (const auto& pair : linear_combination) {
if (!map.contains(pair.first)) { if (!map.contains(pair.second)) {
ordered_basis.push_back(pair.first); ordered_basis.push_back(pair.second);
map.insert(pair.first, counter++); map.insert(pair.second, counter++);
} }
} }
} }
@ -409,7 +393,7 @@ namespace spacer {
for (unsigned i=0; i < m_linear_combinations.size(); ++i) { for (unsigned i=0; i < m_linear_combinations.size(); ++i) {
auto linear_combination = m_linear_combinations[i]; auto linear_combination = m_linear_combinations[i];
for (const auto& pair : linear_combination) { 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(); matrix.print_matrix();
@ -695,13 +679,11 @@ namespace spacer {
* computes min-cut on the graph constructed by compute_partial_core-method * computes min-cut on the graph constructed by compute_partial_core-method
* and adds the corresponding lemmas to the core * 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; unsigned_vector cut_nodes;
m_min_cut.compute_min_cut(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]); m_learner.add_lemma_to_core(m_node_to_formula[cut_node]);
} }
} }

44
src/muz/spacer/spacer_unsat_core_plugin.h
View file

@ -23,66 +23,55 @@ Revision History:
namespace spacer { namespace spacer {
class unsat_core_learner; class unsat_core_learner;
class unsat_core_plugin { class unsat_core_plugin {
protected: protected:
typedef vector<std::pair<rational, app*>> coeff_lits_t; typedef vector<std::pair<rational, app*>> coeff_lits_t;
ast_manager& m; ast_manager& m;
public: public:
unsat_core_plugin(unsat_core_learner& learner); unsat_core_plugin(unsat_core_learner& learner);
virtual ~unsat_core_plugin() {}; virtual ~unsat_core_plugin() {};
virtual void compute_partial_core(proof* step) = 0; virtual void compute_partial_core(proof* step) = 0;
virtual void finalize(){}; virtual void finalize(){};
unsat_core_learner& m_learner; unsat_core_learner& m_learner;
}; };
class unsat_core_plugin_lemma : public unsat_core_plugin {
class unsat_core_plugin_lemma : public unsat_core_plugin { public:
public:
unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){}; unsat_core_plugin_lemma(unsat_core_learner& learner) : unsat_core_plugin(learner){};
void compute_partial_core(proof* step) override; void compute_partial_core(proof* step) override;
private:
private:
void add_lowest_split_to_core(proof* step) const; void add_lowest_split_to_core(proof* step) const;
}; };
class unsat_core_plugin_farkas_lemma : public unsat_core_plugin {
class unsat_core_plugin_farkas_lemma : public unsat_core_plugin { public:
public:
unsat_core_plugin_farkas_lemma(unsat_core_learner& learner, unsat_core_plugin_farkas_lemma(unsat_core_learner& learner,
bool split_literals, bool split_literals,
bool use_constant_from_a=true) : bool use_constant_from_a=true) :
unsat_core_plugin(learner), unsat_core_plugin(learner),
m_split_literals(split_literals), m_split_literals(split_literals),
m_use_constant_from_a(use_constant_from_a) {}; m_use_constant_from_a(use_constant_from_a) {};
void compute_partial_core(proof* step) override; void compute_partial_core(proof* step) override;
private:
private:
bool m_split_literals; bool m_split_literals;
bool m_use_constant_from_a; bool m_use_constant_from_a;
/* /*
* compute linear combination of literals 'literals' having coefficients 'coefficients' and save result in res * 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); 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_farkas_lemma_optimized : public unsat_core_plugin {
public: public:
unsat_core_plugin_farkas_lemma_optimized(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {}; 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 compute_partial_core(proof* step) override;
void finalize() override; void finalize() override;
protected: protected:
vector<vector<std::pair<app*, rational> > > m_linear_combinations; vector<coeff_lits_t> m_linear_combinations;
/* /*
* compute linear combination of literals 'literals' having coefficients 'coefficients' and save result in res * 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 { class unsat_core_plugin_farkas_lemma_bounded : public unsat_core_plugin_farkas_lemma_optimized {
public: public:
unsat_core_plugin_farkas_lemma_bounded(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin_farkas_lemma_optimized(learner, m) {}; unsat_core_plugin_farkas_lemma_bounded(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin_farkas_lemma_optimized(learner, m) {};
void finalize() override; void finalize() override;
}; };
class unsat_core_plugin_min_cut : public unsat_core_plugin { class unsat_core_plugin_min_cut : public unsat_core_plugin {
public: public:
unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m); unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m);
void compute_partial_core(proof* step) override; void compute_partial_core(proof* step) override;
void finalize() override; void finalize() override;
private: 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 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<proof, unsigned> m_proof_to_node_minus; // maps proof-steps to the corresponding minus-nodes (the ones which are closer to source) obj_map<proof, unsigned> m_proof_to_node_minus; // maps proof-steps to the corresponding minus-nodes (the ones which are closer to source)
obj_map<proof, unsigned> m_proof_to_node_plus; // maps proof-steps to the corresponding plus-nodes (the ones which are closer to sink) obj_map<proof, unsigned> m_proof_to_node_plus; // maps proof-steps to the corresponding plus-nodes (the ones which are closer to sink)