mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

debug emons

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-18 17:34:10 -07:00
parent e28e83a25e
commit 884a2628de
4 changed files with 22 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/util/lp/emonomials.cpp
View file

@ -161,6 +161,9 @@ namespace nla {
void emonomials::remove_cg(lpvar v) {
cell* c = m_use_lists[v].m_head;
if (c == nullptr) {
return;
}
cell* first = c;
inc_visited();
do {
@ -206,6 +209,10 @@ namespace nla {
*/
void emonomials::insert_cg(lpvar v) {
cell* c = m_use_lists[v].m_head;
if (c == nullptr) {
return;
}
cell* first = c;
inc_visited();
do {

7
src/util/lp/emonomials.h
View file

@ -210,7 +210,12 @@ namespace nla {
/**
\brief obtain the representative canonized monomial up to sign.
*/
signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
//signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
signed_vars const& rep(signed_vars const& sv) const {
unsigned j = -1;
m_cg_table.find(sv.var(), j);
return m_canonized[m_var2index[j]];
}
/**
\brief the original sign is defined as a sign of the equivalence class representative.

8
src/util/lp/lar_solver.cpp
View file

@ -46,10 +46,16 @@ bool lar_solver::get_track_pivoted_rows() const {
lar_solver::~lar_solver(){
for (auto c : m_constraints)
TRACE("lar_solver", tout << "~enter\n";);
for (auto c : m_constraints) {
TRACE("lar_solver", tout << c << "\n";);
delete c;
}
for (auto t : m_terms)
delete t;
TRACE("lar_solver", tout << "~exit\n";);
}
bool lar_solver::is_term(var_index j) const {

4
src/util/lp/nla_core.h
View file

@ -77,14 +77,14 @@ public:
class core {
public:
var_eqs m_evars;
emonomials m_emons;
lp::lar_solver m_lar_solver;
lp::lar_solver& m_lar_solver;
vector<lemma> * m_lemma_vec;
svector<lpvar> m_to_refine;
tangents m_tangents;
basics m_basics;
order m_order;
monotone m_monotone;
emonomials m_emons;
core(lp::lar_solver& s);