Skip to content

Commit

Permalink
fix build break (debug assertion) and isolate gomory functionality
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jul 14, 2022
1 parent b253db2 commit 894fb83
Show file tree
Hide file tree
Showing 5 changed files with 208 additions and 139 deletions.
2 changes: 1 addition & 1 deletion src/cmd_context/cmd_context.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -619,7 +619,7 @@ void cmd_context::set_produce_unsat_cores(bool f) {
}

void cmd_context::set_produce_proofs(bool f) {
SASSERT(!has_assertions());
SASSERT(!has_assertions() || m_params.m_proof == f);
if (has_manager())
m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
m_params.m_proof = f;
Expand Down
56 changes: 11 additions & 45 deletions src/math/lp/nla_core.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_intervals(this, lim),
m_monomial_bounds(this),
m_horner(this),
m_pdd_manager(s.number_of_vars()),
m_pdd_grobner(lim, m_pdd_manager),
m_grobner(this),
m_emons(m_evars),
m_reslim(lim),
m_use_nra_model(false),
Expand Down Expand Up @@ -1506,7 +1505,7 @@ lbool core::check(vector<lemma>& l_vec) {
m_horner.horner_lemmas();

if (l_vec.empty() && !done() && need_run_grobner())
run_grobner();
m_grobner();

if (l_vec.empty() && !done())
m_basics.basic_lemma(true);
Expand Down Expand Up @@ -1661,51 +1660,15 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
}


void core::set_active_vars_weights(nex_creator& nc) {
nc.set_number_of_vars(m_lar_solver.column_count());
for (lpvar j : active_var_set())
nc.set_var_weight(j, get_var_weight(j));
bool core::is_nl_var(lpvar j) const {
return is_monic_var(j) || m_emons.is_used_in_monic(j);
}

void core::set_level2var_for_grobner() {
unsigned n = m_lar_solver.column_count();
unsigned_vector sorted_vars(n), weighted_vars(n);
for (unsigned j = 0; j < n; j++) {
sorted_vars[j] = j;
weighted_vars[j] = get_var_weight(j);
}
#if 1
// potential update to weights
for (unsigned j = 0; j < n; j++) {
if (is_monic_var(j) && m_to_refine.contains(j)) {
for (lpvar k : m_emons[j].vars()) {
weighted_vars[k] += 6;
}
}
}
#endif

std::sort(sorted_vars.begin(), sorted_vars.end(), [&](unsigned a, unsigned b) {
unsigned wa = weighted_vars[a];
unsigned wb = weighted_vars[b];
return wa < wb || (wa == wb && a < b); });

unsigned_vector l2v(n);
for (unsigned j = 0; j < n; j++)
l2v[j] = sorted_vars[j];

m_pdd_manager.reset(l2v);

TRACE("grobner",
for (auto v : sorted_vars)
tout << "j" << v << " w:" << weighted_vars[v] << " ";
tout << "\n");
}

unsigned core::get_var_weight(lpvar j) const {
unsigned k;
switch (m_lar_solver.get_column_type(j)) {

case lp::column_type::fixed:
k = 0;
break;
Expand All @@ -1725,14 +1688,17 @@ unsigned core::get_var_weight(lpvar j) const {
}
if (is_monic_var(j)) {
k++;
if (m_to_refine.contains(j))
if (m_to_refine.contains(j))
k++;
}
return k;
}

bool core::is_nl_var(lpvar j) const {
return is_monic_var(j) || m_emons.is_used_in_monic(j);

void core::set_active_vars_weights(nex_creator& nc) {
nc.set_number_of_vars(m_lar_solver.column_count());
for (lpvar j : active_var_set())
nc.set_var_weight(j, get_var_weight(j));
}

bool core::influences_nl_var(lpvar j) const {
Expand Down
46 changes: 18 additions & 28 deletions src/math/lp/nla_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,13 @@
#include "math/lp/nla_basics_lemmas.h"
#include "math/lp/nla_order_lemmas.h"
#include "math/lp/nla_monotone_lemmas.h"
#include "math/lp/nla_grobner.h"
#include "math/lp/emonics.h"
#include "math/lp/nla_settings.h"
#include "math/lp/nex.h"
#include "math/lp/horner.h"
#include "math/lp/monomial_bounds.h"
#include "math/lp/nla_intervals.h"
#include "math/grobner/pdd_solver.h"
#include "nlsat/nlsat_solver.h"


Expand Down Expand Up @@ -139,6 +139,9 @@ struct pp_factorization {
};

class core {
friend class new_lemma;
friend class grobner;

struct stats {
unsigned m_nla_explanations;
unsigned m_nla_lemmas;
Expand All @@ -148,11 +151,11 @@ class core {
memset(this, 0, sizeof(*this));
}
};
stats m_stats;
friend class new_lemma;

unsigned m_nlsat_delay { 50 };
unsigned m_nlsat_fails { 0 };
stats m_stats;
unsigned m_nlsat_delay = 50;
unsigned m_nlsat_fails = 0;

bool should_run_bounded_nlsat();
lbool bounded_nlsat();
public:
Expand All @@ -168,13 +171,12 @@ class core {
monomial_bounds m_monomial_bounds;
horner m_horner;
nla_settings m_nla_settings;
dd::pdd_manager m_pdd_manager;
dd::solver m_pdd_grobner;
grobner m_grobner;
private:
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable lp::u_set m_active_var_set;
lp::u_set m_rows;

reslimit m_nra_lim;
public:
reslimit& m_reslim;
Expand Down Expand Up @@ -205,6 +207,8 @@ class core {
m_active_var_set.resize(m_lar_solver.number_of_vars());
}

unsigned get_var_weight(lpvar) const;

reslimit& reslim() { return m_reslim; }
emonics& emons() { return m_emons; }
const emonics& emons() const { return m_emons; }
Expand Down Expand Up @@ -249,6 +253,9 @@ class core {
bool need_run_grobner() const {
return m_nla_settings.run_grobner && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0;
}

void set_active_vars_weights(nex_creator&);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);

void incremental_linearization(bool);

Expand Down Expand Up @@ -450,33 +457,16 @@ class core {
lpvar map_to_root(lpvar) const;
std::ostream& print_terms(std::ostream&) const;
std::ostream& print_term(const lp::lar_term&, std::ostream&) const;

template <typename T>
std::ostream& print_row(const T & row , std::ostream& out) const {
std::ostream& print_row(const T& row, std::ostream& out) const {
vector<std::pair<rational, lpvar>> v;
for (auto p : row) {
v.push_back(std::make_pair(p.coeff(), p.var()));
}
return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out);
return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out);
}


void run_grobner();
void find_nl_cluster();
void prepare_rows_and_active_vars();
void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);
std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
void display_matrix_of_m_rows(std::ostream & out) const;
void set_active_vars_weights(nex_creator&);
unsigned get_var_weight(lpvar) const;
void add_row_to_grobner(const vector<lp::row_cell<rational>> & row);
void add_fixed_monic_to_grobner(unsigned j);
bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
void add_eq_to_grobner(dd::pdd& p, u_dependency* dep);
bool check_pdd_eq(const dd::solver::equation*);
const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
void set_level2var_for_grobner();
void configure_grobner();
bool influences_nl_var(lpvar) const;
bool is_nl_var(lpvar) const;

Expand Down
Loading

0 comments on commit 894fb83

Please sign in to comment.