mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

rebase with Z3Prover

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-26 10:09:36 -08:00
parent f8deb4ed5f
commit 610a2837ea
3 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_pdd.h
View file

@ -378,8 +378,6 @@ namespace dd {
inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); } inline pdd operator-(rational const& r, pdd const& b) { return b.rev_sub(r); }
inline pdd operator-(int x, pdd const& b) { return rational(x) - b; } inline pdd operator-(int x, pdd const& b) { return rational(x) - b; }
inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); } inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; } inline pdd& operator&=(pdd & p, pdd const& q) { p = p & q; return p; }
inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; } inline pdd& operator^=(pdd & p, pdd const& q) { p = p ^ q; return p; }

1
src/math/grobner/pdd_grobner.cpp
View file

@ -698,7 +698,6 @@ namespace dd {
} }
} }
if (eq) { if (eq) {
pop_equation(eq); pop_equation(eq);
m_watch[eq->poly().var()].erase(eq); m_watch[eq->poly().var()].erase(eq);
return eq; return eq;

1
src/math/grobner/pdd_solver.h
View file

@ -130,7 +130,6 @@ public:
private: private:
bool step(); bool step();
equation* pick_next(); equation* pick_next();
equation* pick_linear();
bool canceled(); bool canceled();
bool done(); bool done();
void superpose(equation const& eq1, equation const& eq2); void superpose(equation const& eq1, equation const& eq2);