mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
merge changes from Z3Prover
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
aafdab65bd
commit
5e19a52772
|
@ -723,7 +723,6 @@ namespace dd {
|
|||
bool do_gc = m_free_nodes.empty();
|
||||
if (do_gc && !m_disable_gc) {
|
||||
gc();
|
||||
SASSERT(n.m_hi == 0 || (!m_free_nodes.contains(n.m_hi) && !m_free_nodes.contains(n.m_lo)));
|
||||
e = m_node_table.insert_if_not_there2(n);
|
||||
e->get_data().m_refcount = 0;
|
||||
}
|
||||
|
|
|
@ -378,6 +378,8 @@ namespace dd {
|
|||
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-(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; }
|
||||
|
|
|
@ -698,6 +698,7 @@ namespace dd {
|
|||
}
|
||||
}
|
||||
if (eq) {
|
||||
|
||||
pop_equation(eq);
|
||||
m_watch[eq->poly().var()].erase(eq);
|
||||
return eq;
|
||||
|
|
|
@ -130,6 +130,7 @@ public:
|
|||
private:
|
||||
bool step();
|
||||
equation* pick_next();
|
||||
equation* pick_linear();
|
||||
bool canceled();
|
||||
bool done();
|
||||
void superpose(equation const& eq1, equation const& eq2);
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include "math/lp/nla_core.h"
|
||||
#include "math/lp/factorization_factory_imp.h"
|
||||
#include "math/lp/nex.h"
|
||||
#include "math/grobner/pdd_grobner.h"
|
||||
namespace nla {
|
||||
|
||||
core::core(lp::lar_solver& s, reslimit & lim) :
|
||||
|
|
|
@ -82,7 +82,7 @@ static void test3() {
|
|||
e = e * e;
|
||||
}
|
||||
e = e * b;
|
||||
std::cout << e << "\n";
|
||||
// std::cout << e << "\n";
|
||||
}
|
||||
|
||||
static void test_reset() {
|
||||
|
@ -103,7 +103,44 @@ static void test_reset() {
|
|||
c = m.mk_var(2);
|
||||
d = m.mk_var(3);
|
||||
std::cout << (a + b)*(c + d) << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
static void test5() {
|
||||
std::cout << "\ntest5\n";
|
||||
pdd_manager m(2);
|
||||
pdd a = m.mk_var(0);
|
||||
pdd b = m.mk_var(1);
|
||||
|
||||
pdd e = (a - b) * ( a + b);
|
||||
pdd f = a * a - b * b;
|
||||
SASSERT(e == f);
|
||||
|
||||
e = (a - b)* (a - b);
|
||||
f = a * a - 2 * a * b + b * b;
|
||||
SASSERT(e == f);
|
||||
e = a - 3;
|
||||
e = e * e;
|
||||
f = a * a - 6 * a + 9;
|
||||
SASSERT(e == f);
|
||||
e = 2 * a - 3;
|
||||
e = e * e;
|
||||
f = 4 * a * a - 12 * a + 9;
|
||||
SASSERT(e == f);
|
||||
}
|
||||
|
||||
static void test6() {
|
||||
std::cout << "\ntest6\n";
|
||||
pdd_manager m(5);
|
||||
pdd a = m.mk_var(0);
|
||||
pdd b = m.mk_var(1);
|
||||
pdd c = m.mk_var(2);
|
||||
pdd d = m.mk_var(3);
|
||||
pdd e = a * b * b * d + 2*a*b*c + (b*c*d) + (b*c) + (c*d) + 3;
|
||||
pdd f = a * d * c + a + d;
|
||||
pdd l = m.zero();
|
||||
VERIFY(m.try_spoly(e, f, l));
|
||||
std::cout << "superpose\n" << e << "\nand\n" << f << "\nresult\n" << l << "\n";
|
||||
}
|
||||
|
||||
void test_iterator() {
|
||||
std::cout << "test iterator\n";
|
||||
|
|
Loading…
Reference in a new issue