change the representatition of nex_mul to use nex_pow

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/CMakeLists.txt

@@ -26,6 +26,7 @@ z3_add_component(lp
     lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
+    nex.cpp
     nla_basics_lemmas.cpp
     nla_common.cpp
     nla_core.cpp

src/math/lp/cross_nested.h

@@ -125,10 +125,10 @@ public:
         
         nex* c_over_f = m_nex_creator.mk_div(*c, f);
         to_sum(c_over_f)->simplify(&c_over_f);
-        *c = m_nex_creator.mk_mul(f, c_over_f);
+        nex_mul* cm; 
+        *c = cm = m_nex_creator.mk_mul(f, c_over_f);
         TRACE("nla_cn", tout << "common factor=" << *f << ", c=" << **c << "\ne = " << *m_e << "\n";);
-        
+        explore_expr_on_front_elem(cm->children()[1].ee(),  front);
-        explore_expr_on_front_elem(&(*((*c)->children_ptr()))[1],  front);
         return true;
     }
 
@@ -405,7 +405,7 @@ public:
         TRACE("nla_cn_details", tout << "b = " << *b << "\n";);
         e = m_nex_creator.mk_sum(m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a), b); // e = j*a + b
         if (!a->is_linear()) {
-            nex **ptr_to_a = &(to_mul(to_sum(e)->children()[0]))->children()[1];
+            nex **ptr_to_a = (to_mul(to_sum(e)->children()[0]))->children()[1].ee();
             push_to_front(front, ptr_to_a);
         }
         
@@ -419,7 +419,7 @@ public:
         if (b == nullptr) {
             e = m_nex_creator.mk_mul(m_nex_creator.mk_var(j), a);
             if (!to_sum(a)->is_linear())
-                push_to_front(front, &(to_mul(e)->children()[1]));
+                push_to_front(front, to_mul(e)->children()[1].ee());
         } else {
             update_front_with_split_with_non_empty_b(e, j, front, a, b);
         }
@@ -458,8 +458,8 @@ public:
             }
         case expr_type::MUL:
             {
-                for (auto c: to_mul(e)->children())
+                for (auto &c: to_mul(e)->children())
-                    for ( lpvar j : get_vars_of_expr(c))
+                    for ( lpvar j : get_vars_of_expr(c.e()))
                         r.insert(j);
             }
             return r;
@@ -479,7 +479,7 @@ public:
 
     bool done() const { return m_done; }
 #if Z3DEBUG
-    nex *clone (nex * a) {
+    nex *clone (const nex * a) {
         switch (a->type()) {
         case expr_type::VAR: {
             auto v = to_var(a);
@@ -493,8 +493,8 @@ public:
         case expr_type::MUL: {
             auto m = to_mul(a);
             auto r = m_nex_creator.mk_mul();
-            for (nex * e : m->children()) {
+            for (const auto& p : m->children()) {
-                r->add_child(clone(e));
+                r->add_child_in_power(clone(p.e()), p.pow());
             }
             return r;
         }
@@ -524,6 +524,9 @@ public:
 
     nex * normalize_mul(nex_mul* a) {
         TRACE("nla_cn", tout << *a << "\n";);
+        NOT_IMPLEMENTED_YET();
+        return nullptr;
+        /*
         int sum_j = -1;
         for (unsigned j = 0; j < a->size(); j ++) {
             a->children()[j] = normalize(a->children()[j]);
@@ -554,7 +557,7 @@ public:
         nex *rs = normalize_sum(r);
         SASSERT(rs->is_simplified());
         return rs;
-
+        */
     }
 
     

src/math/lp/horner.cpp

@@ -193,11 +193,11 @@ interv horner::interval_of_mul_with_deps(const nex_mul* e) {
         
     SASSERT(e->is_mul());
     auto & es = to_mul(e)->children();
-    interv a = interval_of_expr_with_deps(es[0]);
+    interv a = interval_of_expr_with_deps(es[0].e());
-    TRACE("nla_horner_details", tout << "es[0]= "<< *es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
+    TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
     for (unsigned k = 1; k < es.size(); k++) {
-        interv b = interval_of_expr_with_deps(es[k]);
+        interv b = interval_of_expr_with_deps(es[k].e());
-        TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); );
+        TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
         interv c;
         interval_deps_combine_rule comb_rule;
         m_intervals.mul(a, b, c, comb_rule);
@@ -224,11 +224,11 @@ interv horner::interval_of_mul(const nex_mul* e) {
         
     SASSERT(e->is_mul());
     auto & es = to_mul(e)->children();
-    interv a = interval_of_expr(es[0]);
+    interv a = interval_of_expr(es[0].e());
-    TRACE("nla_horner_details", tout << "es[0]= "<< *es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
+    TRACE("nla_horner_details", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); );
     for (unsigned k = 1; k < es.size(); k++) {
-        interv b = interval_of_expr(es[k]);
+        interv b = interval_of_expr(es[k].e());
-        TRACE("nla_horner_details", tout << "es[" << k << "] "<< *es[k] << ", "; m_intervals.display(tout, b); );
+        TRACE("nla_horner_details", tout << "es[" << k << "] "<< es[k] << ", "; m_intervals.display(tout, b); );
         interv c;
         interval_deps_combine_rule comb_rule;
         m_intervals.mul(a, b, c, comb_rule);
@@ -249,12 +249,13 @@ void horner::add_mul_to_vector(const nex_mul* e, vector<std::pair<rational, lpva
     TRACE("nla_horner_details", tout << *e << "\n";);
     SASSERT(e->size() > 0);
     if (e->size() == 1) {
-        add_linear_to_vector(*(e->children().begin()), v);
+        add_linear_to_vector(e->children().begin()->e(), v);
         return;
     }
     rational r;
     lpvar j = -1;
-    for (const nex * c : e->children()) {
+    for (const auto & p: e->children()) {
+        const nex * c = p.e();
         switch (c->type()) {
         case expr_type::SCALAR:
             r = to_scalar(c)->value();
@@ -331,7 +332,8 @@ lp::lar_term horner::expression_to_normalized_term(const nex_sum* e, rational& a
 
 bool horner::mul_has_inf_interval(const nex_mul* e) const {
     bool has_inf = false;
-    for (const nex *c : e->children()) {
+    for (const auto & p  : e->children()) {
+        const nex *c = p.e();
         if (!c->is_elementary())
             return false; 
         if (has_zero_interval(c))
@@ -364,7 +366,8 @@ bool horner::has_zero_interval(const nex* e) const {
 }
 
 const nex* horner::get_zero_interval_child(const nex_mul* e) const {
-    for (auto * c : e->children()) {
+    for (const auto & p : e->children()) {
+        const nex * c = p.e();
         if (has_zero_interval(c))
             return c;        
     }

src/math/lp/nex.h

@@ -43,7 +43,7 @@ inline std::ostream & operator<<(std::ostream& out, expr_type t) {
 }
 
 
-// This class is needed in horner calculation with intervals
+// This is the class of non-linear expressions 
 class nex {
 public:
     virtual expr_type type() const = 0;
@@ -72,14 +72,6 @@ public:
     virtual bool is_simplified() const {
         return true;
     }
-    virtual const ptr_vector<nex> * children_ptr() const {
-        UNREACHABLE();
-        return nullptr;
-    }
-    virtual ptr_vector<nex> * children_ptr() {
-        UNREACHABLE();
-        return nullptr;
-    }
     #ifdef Z3DEBUG
     virtual void sort() {};
     #endif
@@ -132,7 +124,8 @@ public:
 };
 
 const nex_scalar * to_scalar(const nex* a);
-
+class nex_sum;
+const nex_sum* to_sum(const nex*a);
 static bool ignored_child(nex* e, expr_type t) {
     switch(t) {
     case expr_type::MUL:
@@ -144,77 +137,60 @@ static bool ignored_child(nex* e, expr_type t) {
     return false;
 }
 
-static void promote_children_by_type(ptr_vector<nex> * children, expr_type t) {
+void promote_children_of_sum(ptr_vector<nex> & children);
-    ptr_vector<nex> to_promote;
+class nex_pow;
-    int skipped = 0;
+void promote_children_of_mul(vector<nex_pow> & children);
-    for(unsigned j = 0; j < children->size(); j++) {
+
-        nex** e = &(*children)[j];
+class nex_pow {
-        (*e)->simplify(e);
+    nex* m_e;
-        if ((*e)->type() == t) {
+    int  m_power;
-            to_promote.push_back(*e);
+public:
-        } else if (ignored_child(*e, t)) {
+    explicit nex_pow(nex* e): m_e(e), m_power(1) {}
-            skipped ++;
+    explicit nex_pow(nex* e, int p): m_e(e), m_power(p) {}
-            continue;
+    const nex * e() const { return m_e; }
-        } else {
+    nex * e() { return m_e; }
-            unsigned offset = to_promote.size() + skipped;
+    nex ** ee() { return & m_e; }
-            if (offset) {
+    int pow() const { return m_power; }
-                (*children)[j - offset] = *e;
+    int& pow() { return m_power; }
-            }
+    std::string to_string() const { std::stringstream s; s << "(" << *e() << ", " << pow() << ")";
-        }
+        return s.str(); }
-    }
+    friend std::ostream& operator<<(std::ostream& out, const nex_pow & p) { out << p.to_string(); return out; }
-    
+};
-    children->shrink(children->size() - to_promote.size() - skipped);
-    
-    for (nex *e : to_promote) {
-        for (nex *ee : *(e->children_ptr())) {
-            if (!ignored_child(ee, t))
-                children->push_back(ee);            
-        }
-    }    
-}
 
 class nex_mul : public nex {
-    ptr_vector<nex> m_children;
+    vector<nex_pow> m_children;
 public:
     nex_mul()  {}
     unsigned size() const { return m_children.size(); }
     expr_type type() const { return expr_type::MUL; }
-    ptr_vector<nex>& children() { return m_children;}
+    vector<nex_pow>& children() { return m_children;}
-    const ptr_vector<nex>& children() const { return m_children;}
+    const vector<nex_pow>& children() const { return m_children;}
-    const ptr_vector<nex>* children_ptr() const { return &m_children;}
-    ptr_vector<nex>* children_ptr() { return &m_children;}
     // A monomial is 'pure' if does not have a numeric coefficient.
-    bool is_pure_monomial() const { return size() == 0 || (!m_children[0]->is_scalar()); }    
+    bool is_pure_monomial() const { return size() == 0 || (!m_children[0].e()->is_scalar()); }    
     std::ostream & print(std::ostream& out) const {
+        
         bool first = true;
-        for (const nex* v : m_children) {            
+        for (const nex_pow& v : m_children) {            
-            std::string s = v->str();
+            std::string s = v.to_string();
             if (first) {
                 first = false;
-                if (v->is_elementary())
+                out << s;
-                    out << s;
-                else 
-                    out << "(" << s << ")";                            
             } else {
-                if (v->is_elementary()) {
+                out << "*" << s;                        
-                    if (s[0] == '-') {
-                        out << "*(" << s << ")";
-                    } else {
-                        out << "*" << s;
-                    }
-                } else {
-                    out << "*(" << s << ")";
-                }
             }
         }
         return out;
     }
 
-    void add_child(nex* e) { m_children.push_back(e); }
+    void add_child(nex* e) {
+        add_child_in_power(e, 1);
+    }
+    
+    void add_child_in_power(nex* e, int power) { m_children.push_back(nex_pow(e, power)); }
 
     bool contains(lpvar j) const {
-        for (const nex* c : children()) {
+        for (const nex_pow& c : children()) {
-            if (c->contains(j))
+            if (c.e()->contains(j))
                 return true;
         }
         return false;
@@ -228,34 +204,32 @@ public:
     void get_powers_from_mul(std::unordered_map<lpvar, unsigned> & r) const {
         r.clear();
         for (const auto & c : children()) {
-            if (!c->is_var()) {
+            if (!c.e()->is_var()) {
                 continue;
             }
-            lpvar j = to_var(c)->var();
+            lpvar j = to_var(c.e())->var();
-            auto it = r.find(j);
+            SASSERT(r.find(j) == r.end());
-            if (it == r.end()) {
+            r[j] = c.pow();
-                r[j] = 1;
-            } else {
-                it->second++;
-            }
         }
         TRACE("nla_cn_details", tout << "powers of " << *this << "\n"; print_vector(r, tout)<< "\n";);
     }
 
     int get_degree() const {
         int degree = 0;       
-        for (auto  e : children()) {
+        for (const auto& p : children()) {
-            degree +=  e->get_degree();
+            degree +=  p.e()->get_degree() * p.pow();
         }
         return degree;
     }
     
     void simplify(nex **e) {
+        TRACE("nla_cn_details", tout << *this << "\n";);
+        TRACE("nla_cn_details", tout << "**e = " << **e << "\n";);
         *e = this;
         TRACE("nla_cn_details", tout << *this << "\n";);
-        promote_children_by_type(&m_children, expr_type::MUL);
+        promote_children_of_mul(m_children);
-        if (size() == 1) 
+        if (size() == 1 && m_children[0].pow() == 1) 
-            *e = m_children[0];
+            *e = m_children[0].e();
         TRACE("nla_cn_details", tout << *this << "\n";);
         SASSERT((*e)->is_simplified());
     }
@@ -263,7 +237,8 @@ public:
     virtual bool is_simplified() const {
         if (size() < 2)
             return false;
-        for (nex * e : children()) {
+        for (const auto &p : children()) {
+            const nex* e = p.e();
             if (e->is_mul()) 
                 return false;
             if (e->is_scalar() && to_scalar(e)->value().is_one())
@@ -274,25 +249,17 @@ public:
 
     bool is_linear() const {
         SASSERT(is_simplified());
-        if (children().size() > 2)
+        return get_degree() < 2; // todo: make it more efficient
-            return false;
-
-        SASSERT(children().size() == 2);
-        for (auto e : children()) {
-            if (e->is_scalar())
-                return true;
-        }
-        return false;
     }
 
-#ifdef Z3DEBUG
+// #ifdef Z3DEBUG
-    virtual void sort() {
+//     virtual void sort() {
-        for (nex * c : m_children) {
+//         for (nex * c : m_children) {
-            c->sort();
+//             c->sort();
-        }
+//         }
-        std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; });
+//         std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; });
-    }
+//     }
-    #endif
+//     #endif
 
 };
 
@@ -361,7 +328,7 @@ public:
 
     void simplify(nex **e) {
         *e = this;
-        promote_children_by_type(&m_children, expr_type::SUM);
+        promote_children_of_sum(m_children);
         if (size() == 1)
             *e = m_children[0];
     }
@@ -387,12 +354,15 @@ public:
     void add_child(nex* e) { m_children.push_back(e); }
 #ifdef Z3DEBUG
     virtual void sort() {
+        NOT_IMPLEMENTED_YET();
+        /*
         for (nex * c : m_children) {
             c->sort();
         }
         
 
         std::sort(m_children.begin(), m_children.end(), [](const nex* a, const nex* b) { return *a < *b; });
+        */
     }
 #endif
 };
@@ -449,30 +419,6 @@ inline bool operator<(const ptr_vector<nex>&a , const ptr_vector<nex>& b) {
     return false;
 }
 
-inline bool operator<(const nex& a , const nex& b) {
-    int r = (int)(a.type()) - (int)(b.type());
-    ptr_vector<nex> ch;
-    if (r) {
-        return r < 0;
-    }
-    switch (a.type()) {
-    case expr_type::VAR: {
-        return to_var(&a)->var() < to_var(&b)->var();
-    }
-    case expr_type::SCALAR: {
-        return to_scalar(&a)->value() < to_scalar(&b)->value();
-    }        
-    case expr_type::MUL: {
-        return to_mul(&a)->children() < to_mul(&b)->children();
-    }
-    case expr_type::SUM: {
-        return to_sum(&a)->children() < to_sum(&b)->children();
-    }
-    default:
-        SASSERT(false);
-        return false;
-    }
-}
 #endif
 }
     

src/math/lp/nex_creator.h

@@ -84,7 +84,7 @@ public:
         return r;
     }
 
-    nex_mul* mk_mul(const ptr_vector<nex>& v) {
+    nex_mul* mk_mul(const vector<nex_pow>& v) {
         auto r = new nex_mul();
         add_to_allocated(r);
         r->children() = v;
@@ -129,10 +129,13 @@ public:
 
     nex * mk_div(const nex* a, lpvar j) {
         TRACE("nla_cn_details", tout << "a=" << *a << ", v" << j << "\n";);
+        NOT_IMPLEMENTED_YET();
+        return nullptr;
+        /*
         SASSERT((a->is_mul() && a->contains(j)) || (a->is_var() && to_var(a)->var() == j));
         if (a->is_var())
             return mk_scalar(rational(1));
-        ptr_vector<nex> bv;
+        ptr_vector<nex> bv; 
         bool seenj = false;
         for (nex* c : to_mul(a)->children()) {
             if (!seenj) {
@@ -153,11 +156,11 @@ public:
         }
 
         SASSERT(bv.size() == 0);
-        return mk_scalar(rational(1));
+        return mk_scalar(rational(1));*/
     }
 
     nex * mk_div(const nex* a, const nex* b) {
-        TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
+        TRACE("nla_cn_details", tout <<"("  << *a << ") / (" << *b << ")\n";);
         if (b->is_var()) {
             return mk_div(a, to_var(b)->var());
         }
@@ -176,15 +179,18 @@ public:
             return mk_scalar(rational(1));
         }
         SASSERT(a->is_mul());
+        
         const nex_mul* am = to_mul(a);
         bm->get_powers_from_mul(m_powers);
+        TRACE("nla_cn_details", print_vector(m_powers, tout););
         nex_mul* ret = new nex_mul();
-        for (auto e : am->children()) {
+        for (const nex_pow& p : am->children()) {
+            const nex *e = p.e();
             TRACE("nla_cn_details", tout << "e=" << *e << "\n";);
             
             if (!e->is_var()) {
                 SASSERT(e->is_scalar());
-                ret->add_child(e);
+                ret->add_child(mk_scalar(to_scalar(e)->value()));
                 TRACE("nla_cn_details", tout << "continue\n";);
                 continue;
             }
@@ -192,7 +198,7 @@ public:
             lpvar j = to_var(e)->var();
             auto it = m_powers.find(j);
             if (it == m_powers.end()) {
-                 ret->add_child(e);
+                ret->add_child(mk_var(j));
             } else {
                 it->second --;
                 if (it->second == 0)

src/math/lp/nla_grobner.h

@@ -151,7 +151,7 @@ private:
 
     nex* mk_monomial_in_row(rational, lpvar, ci_dependency*&);
     rational get_monomial_coeff(const nex_mul* m) {        
-        const nex* a = m->children()[0];
+        const nex* a = m->children()[0].e();
         if (a->is_scalar())
             return static_cast<const nex_scalar*>(a)->value();
         return rational(1);

src/test/lp/lp.cpp

@@ -73,6 +73,22 @@ void test_cn_on_expr(nex_sum *t, cross_nested& cn) {
     cn.run(t);
 }
 
+void test_simplify(cross_nested& cn, nex_var* a, nex_var* b, nex_var* c) {
+    auto & r = cn.get_nex_creator();
+    auto m = r.mk_mul(); m->add_child_in_power(c, 2);
+    TRACE("nla_cn", tout << "m = " << *m << "\n";); 
+    auto n = r.mk_mul(a);
+    n->add_child_in_power(b, 7);
+    TRACE("nla_cn", tout << "n = " << *n << "\n";); 
+    m->add_child_in_power(n, 3);
+    TRACE("nla_cn", tout << "m = " << *m << "\n";); 
+    
+    nex * e = r.mk_sum(a, r.mk_sum(b, m));
+    TRACE("nla_cn", tout << "e = " << *e << "\n";);
+    e->simplify(&e);
+    TRACE("nla_cn", tout << "simplified e = " << *e << "\n";);
+}
+
 void test_cn() {
     cross_nested cn(
         [](const nex* n) {
@@ -91,6 +107,7 @@ void test_cn() {
     nex_var* e = cn.get_nex_creator().mk_var(4);
     nex_var* g = cn.get_nex_creator().mk_var(6);
     nex* min_1 = cn.get_nex_creator().mk_scalar(rational(-1));
+    test_simplify(cn, a, b, c);
     // test_cn_on_expr(min_1*c*e + min_1*b*d + min_1*a*b + a*c);
     nex* bcd = cn.get_nex_creator().mk_mul(b, c, d);
     nex_mul* bcg = cn.get_nex_creator().mk_mul(b, c, g);