work on order lemma

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

src/util/lp/column_namer.h

@@ -33,31 +33,6 @@ public:
         print_linear_combination_of_column_indices(coeff, out);
     }
     
-
-    
-    template <typename T>
-    void print_linear_combination_of_column_indices_std(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) const {
-        bool first = true;
-        for (const auto & it : coeffs) {
-            auto val = it.first;
-            if (first) {
-                first = false;
-            } else {
-                if (numeric_traits<T>::is_pos(val)) {
-                    out << " + ";
-                } else {
-                    out << " - ";
-                    val = -val;
-                }
-            }
-            if (val == -numeric_traits<T>::one())
-                out << " - ";
-            else if (val != numeric_traits<T>::one())
-                out << val;
-        
-            out << get_variable_name(it.second);
-        }
-    }
     template <typename T>
     void print_linear_combination_of_column_indices(const vector<std::pair<T, unsigned>> & coeffs, std::ostream & out) const {
         bool first = true;

src/util/lp/factorization.cpp

@@ -8,9 +8,9 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
     k_vars.push_back(m_ff->m_cmon.vars().back()); 
     for (unsigned j = 0; j < m_mask.size(); j++) {
         if (m_mask[j]) {
-            k_vars.push_back(m_ff->m_cmon[j]);
+            k_vars.push_back(m_ff->m_cmon.vars()[j]);
         } else {
-            j_vars.push_back(m_ff->m_cmon[j]);
+            j_vars.push_back(m_ff->m_cmon.vars()[j]);
         }
     }
 }

src/util/lp/lar_solver.cpp

@@ -1282,6 +1282,9 @@ void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_in
     }
 }
 
+void lar_solver::set_variable_name(var_index vi, std::string name) {
+    m_var_register.set_name(vi, name);
+}
 
 std::string lar_solver::get_variable_name(var_index j) const {
     if (j >= m_terms_start_index) 
@@ -1289,6 +1292,11 @@ std::string lar_solver::get_variable_name(var_index j) const {
     if (j >= m_var_register.size())
         return std::string("_s") + T_to_string(j);
 
+    std::string s = m_var_register.get_name(j);
+    if (!s.empty()) {
+        return s;
+    }
+    
     return std::string("v") + T_to_string(m_var_register.local_to_external(j));
 }
 
@@ -1598,6 +1606,11 @@ bool lar_solver::strategy_is_undecided() const {
     return m_settings.simplex_strategy() == simplex_strategy_enum::undecided;
 }
 
+var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, std::string name) {
+    var_index j = add_var(ext_j,is_int);
+    m_var_register.set_name(j, name);
+    return j;
+}
 var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
     TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;);
     var_index local_j;

src/util/lp/lar_solver.h

@@ -161,6 +161,8 @@ public:
 
     var_index add_var(unsigned ext_j, bool is_integer);
 
+    var_index add_named_var(unsigned ext_j, bool is_integer, std::string);
+
     void register_new_ext_var_index(unsigned ext_v, bool is_int);
 
     bool external_is_used(unsigned) const;
@@ -489,6 +491,8 @@ public:
 
     std::string get_variable_name(var_index vi) const;
 
+    void set_variable_name(var_index vi, std::string);
+
     // ********** print region start
     std::ostream& print_constraint(constraint_index ci, std::ostream & out) const;
 

src/util/lp/lp_utils.h

@@ -58,6 +58,21 @@ bool contains(const std::unordered_map<A, B> & map, const A& key) {
 
 namespace lp {
 
+template <typename K> 
+bool is_non_decreasing(const K& v) {
+    auto a = v.begin();
+    if (a == v.end())
+        return true; // v is empty
+    auto b = v.begin();
+    b++;
+    for (; b != v.end(); a++, b++) {
+        if (*a > *b)
+            return false;
+    }
+    return true; 
+}
+
+
 template <typename T>
 void print_linear_combination_of_column_indices_only(const T & coeffs, std::ostream & out) {
     bool first = true;

src/util/lp/monomial.h

@@ -49,17 +49,14 @@ namespace nla {
      *  represents definition m_v = coeff* v1*v2*...*vn, 
      *  where m_vs = [v1, v2, .., vn]
      */
-    class monomial_coeff : public monomial {
+    class monomial_coeff  {
+        svector<lp::var_index> m_vs;
         rational m_coeff;
     public:
-        monomial_coeff(monomial const& eq, rational const& coeff):
-            monomial(eq), m_coeff(coeff) {}
-
-        monomial_coeff(lp::var_index v, const svector<lp::var_index> &vs, rational const& coeff):
-            monomial(v, vs),
-            m_coeff(coeff) {}
+        monomial_coeff(const svector<lp::var_index>& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {}
 
         rational const& coeff() const { return m_coeff; }
+        const svector<lp::var_index> & vars() const { return m_vs; } 
     };
 
 }

src/util/lp/nla_solver.cpp

@@ -33,23 +33,34 @@ struct solver::imp {
    
 
     //fields    
-    vars_equivalence                                       m_vars_equivalence;
-    vector<monomial>                                       m_monomials;
+    vars_equivalence                                                 m_vars_equivalence;
+    vector<monomial>                                                 m_monomials;
     // maps the vector of the rooted monomial vars to the list of the indices of monomials having the same rooted monomial
     std::unordered_map<svector<lpvar>,
                        vector<index_with_sign>,
                        hash_svector>
-                                                           m_rooted_monomials;
+                                                                     m_rooted_monomials_map;
+    vector<svector<lpvar>>                                           m_vector_of_rooted_monomials;
 
     // this field is used for the push/pop operations
-    unsigned_vector                                        m_monomials_counts;
-    lp::lar_solver&                                        m_lar_solver;
-    std::unordered_map<lpvar, unsigned_vector>             m_monomials_containing_var;
+    unsigned_vector                                                  m_monomials_counts;
+    lp::lar_solver&                                                  m_lar_solver;
+    std::unordered_map<lpvar, svector<lpvar>>                        m_monomials_containing_var;
+    // for every k 
+    // for each i in m_rooted_monomials_containing_var[k]
+    // m_vector_of_rooted_monomials[i] contains k
+    std::unordered_map<lpvar, std::unordered_set<unsigned>>          m_rooted_monomials_containing_var;
+
+    // A map from m_vector_of_rooted_monomials to a set
+    // of sets of m_vector_of_rooted_monomials,
+    // such that for every i and every h in m_vector_of_rooted_monomials[i]
+    // m_vector_of_rooted_monomials[i] is a proper factor of m_vector_of_rooted_monomials[h]
+    std::unordered_map<unsigned, std::unordered_set<unsigned>>       m_rooted_factor_to_product;
     
-    // monomial.var()  -> monomial index
-    u_map<unsigned>                                        m_var_to_its_monomial;
-    lp::explanation *                                      m_expl;
-    lemma *                                                m_lemma;
+    // u_map[m_monomials[i].var()] = i
+    u_map<unsigned>                                                  m_var_to_its_monomial;
+    lp::explanation *                                                m_expl;
+    lemma *                                                          m_lemma;
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
         :
         m_vars_equivalence([this](unsigned h){return vvr(h);}),
@@ -128,6 +139,8 @@ struct solver::imp {
         add_explanation_of_reducing_to_rooted_monomial(m_monomials[index], exp);
     }
 
+
+    
     std::ostream& print_monomial(const monomial& m, std::ostream& out) const {
         out << m_lar_solver.get_variable_name(m.var()) << " = ";
         for (unsigned k = 0; k < m.size(); k++) {
@@ -145,8 +158,8 @@ struct solver::imp {
         return print_monomial_with_vars(m_monomials[i], tout);
     }
 
-    std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const {
-        out << m_lar_solver.get_variable_name(m.var()) << " = ";
+    template <typename T>
+    std::ostream& print_product_with_vars(const T& m, std::ostream& out) const {
         for (unsigned k = 0; k < m.size(); k++) {
             out << m_lar_solver.get_variable_name(m.vars()[k]);
             if (k + 1 < m.size()) out << "*";
@@ -155,7 +168,12 @@ struct solver::imp {
         for (unsigned k = 0; k < m.size(); k++) {
             print_var(m.vars()[k], out);
         }
-       return out;
+        return out;
+        
+    }
+    std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const {
+        out << m_lar_solver.get_variable_name(m.var()) << " = ";
+        return print_product_with_vars(m, out);
     }
 
     
@@ -258,7 +276,7 @@ struct solver::imp {
     monomial_coeff canonize_monomial(monomial const& m) const {
         rational sign = rational(1);
         svector<lpvar> vars = reduce_monomial_to_rooted(m.vars(), sign);
-        return monomial_coeff(m.var(), vars, sign);
+        return monomial_coeff(vars, sign);
     }
 
     bool list_contains_one_to_refine(const std::unordered_set<unsigned> & to_refine_set,
@@ -410,8 +428,8 @@ struct solver::imp {
     
     // returns true if found
     bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const {
-        auto it = m_rooted_monomials.find(vars);
-        if (it == m_rooted_monomials.end()) {
+        auto it = m_rooted_monomials_map.find(vars);
+        if (it == m_rooted_monomials_map.end()) {
             return false;
         }
 
@@ -441,8 +459,8 @@ struct solver::imp {
                 m_imp(s) { }
         
          bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const {
-            auto it = m_imp.m_rooted_monomials.find(vars);
-            if (it == m_imp.m_rooted_monomials.end()) {
+            auto it = m_imp.m_rooted_monomials_map.find(vars);
+            if (it == m_imp.m_rooted_monomials_map.end()) {
                 return false;
             }
 
@@ -697,7 +715,7 @@ struct solver::imp {
         }
     }
 
-    void map_vars_to_monomials_and_constraints() {
+    void map_vars_to_monomials() {
         for (unsigned i = 0; i < m_monomials.size(); i++)
             map_monomial_vars_to_monomial_indices(i);
     }
@@ -755,12 +773,12 @@ struct solver::imp {
 
     void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i) {
         index_with_sign ms(i, mc.coeff());
-        auto it = m_rooted_monomials.find(mc.vars());
-        if (it == m_rooted_monomials.end()) {
+        auto it = m_rooted_monomials_map.find(mc.vars());
+        if (it == m_rooted_monomials_map.end()) {
             vector<index_with_sign> v;
             v.push_back(ms);
             // v is a vector containing a single index_with_sign
-            m_rooted_monomials.emplace(mc.vars(), v);
+            m_rooted_monomials_map.emplace(mc.vars(), v);
         } 
         else {
             it->second.push_back(ms);
@@ -773,94 +791,206 @@ struct solver::imp {
         register_key_mono_in_rooted_monomials(mc, i);        
     }
 
+    void fill_vector_of_rooted_monomials() {
+        SASSERT(m_vector_of_rooted_monomials.empty());
+        for (const auto& p : m_rooted_monomials_map) {
+            m_vector_of_rooted_monomials.push_back(p.first);
+        }
+    }
+
+    void register_rooted_monomial(unsigned i) {
+        for (unsigned j : m_vector_of_rooted_monomials[i]) {
+            auto it = m_rooted_monomials_containing_var.find(j);
+            if (it == m_rooted_monomials_containing_var.end()) {
+                std::unordered_set<unsigned> s;
+                s.insert(i);
+                m_rooted_monomials_containing_var[j] = s;
+            } else {
+                it->second.insert(i);
+            }
+        }
+    }
+    
+    void create_rooted_tables() {
+        fill_vector_of_rooted_monomials();
+        for (unsigned i = 0; i < m_vector_of_rooted_monomials.size(); i++) {
+            register_rooted_monomial(i);
+        }
+    }
+
+    void intersect_set(std::unordered_set<unsigned>& p, const std::unordered_set<unsigned>& w) {
+        for (auto it = p.begin(); it != p.end(); ) {
+            auto iit = it;
+            iit ++;
+            if (w.find(*it) == w.end())
+                p.erase(it);
+            it = iit;
+        }
+    }
+
+    
+    // returns true if a is a factar of b
+    bool is_factor(const svector<lpvar> & a, const svector<lpvar> & b) {
+        SASSERT(lp::is_non_decreasing(a) && lp::is_non_decreasing(b));
+        auto i = a.begin();
+        auto j = b.begin();
+
+        while (true) {
+            if (i == a.end()) {
+                return true;
+            }
+            if (j == b.end()) {
+                return false;
+            }
+
+            j = std::lower_bound(j, b.end(), *i);
+
+            if (j == b.end() || *i != *j) {
+                return false;
+            }
+            i++; j++;
+        }
+        
+    }
+
+    void reduce_set_by_checking_actual_containment(std::unordered_set<unsigned>& p,
+                                                   const svector<lpvar> & rm ) {
+        for (auto it = p.begin(); it != p.end();) {
+            if (is_factor(rm, m_vector_of_rooted_monomials[*it])) {
+                it++;
+                continue;
+            }
+            auto iit = it;
+            iit ++;
+            p.erase(it);
+            it = iit;
+        }
+    }
+    
+    // here i is the index of a monomial in m_vector_of_rooted_monomials
+    void find_containing_rooted_monomials(unsigned i) {
+        const svector<lpvar> & rm = m_vector_of_rooted_monomials[i];
+        std::unordered_set<unsigned> p = m_rooted_monomials_containing_var[rm[0]];
+        for (unsigned k = 1; k < rm.size(); k++) {
+            intersect_set(p, m_rooted_monomials_containing_var[rm[k]]);
+        }
+        reduce_set_by_checking_actual_containment(p, rm);
+        m_rooted_factor_to_product[i] = p;
+    }
+    
+    void fill_rooted_factor_to_product() {
+        for (unsigned i = 0; i < m_vector_of_rooted_monomials.size(); i++) {
+            find_containing_rooted_monomials(i);
+        }
+    }
+
     void register_monomials_in_tables() {
         m_vars_equivalence.clear_monomials_by_abs_vals();
         for (unsigned i = 0; i < m_monomials.size(); i++) 
             register_monomial_in_tables(i);
+
+        create_rooted_tables();
+        fill_rooted_factor_to_product();
     }
     
     void init_search() {
-        map_vars_to_monomials_and_constraints();
+        map_vars_to_monomials();
         init_vars_equivalence();
         register_monomials_in_tables();
         m_expl->clear();
         m_lemma->clear();
     }
 
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    // ac[k] plays the role of c
+    // d = +-c
+
     bool order_lemma_on_factor_equiv_and_other_mon_factor(unsigned i_f,
-                                                   unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
+                                                   unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k) {
+        TRACE("nla_solver", tout << "i_f = "; print_monomial_with_vars(i_f, tout); );
+        NOT_IMPLEMENTED_YET();
         return false;
     }    
-    
-    bool order_lemma_on_factor_equiv_and_other_mon(unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
-        if (o_i_mon == i_mon) return false;
-        const monomial & o_m = m_monomials[o_i_mon];
-        svector<lpvar> o_key;
-        for (unsigned j : o_m) {
-            if (j != e_j) {
-                o_key.push_back(j);
-            }
-        }
 
-        rational o_sign(1);
-        o_key = reduce_monomial_to_rooted(o_key, o_sign);
-        auto it = m_rooted_monomials.find(o_key);
-        if (it == m_rooted_monomials.end())
+    
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    // ac[k] plays the role of c
+    // d = +-c
+    bool order_lemma_on_factor_equiv_and_other_mon(unsigned i_bd, unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
+        if (i_bd == i_ac) {
+            return false;
+        }
+        TRACE("nla_solver", );
+        const monomial & m_bd = m_monomials[i_bd];
+        monomial_coeff m_bd_rooted = canonize_monomial(m_bd);
+        TRACE("nla_solver", tout << "i_bd monomial = "; print_monomial(m_bd, tout); );
+        TRACE("nla_solver", );
+        auto it = m_rooted_monomials_map.find(m_bd_rooted.vars());
+        if (it == m_rooted_monomials_map.end())
             return false;
         for (const index_with_sign& i_s : it->second) {
-            if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), o_i_mon, e_j, i_mon, f, k, sign * o_sign * i_s.sign()))
+            if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), i_bd, d, i_ac, ac, k))
                 return true;
         }
         return false;
     }
 
-    // f is a factorization of m_monomials[i_mon]
-    // here e_j is equivalent to f[k],
-    bool order_lemma_on_factor_and_equiv(unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) {
-        lpvar j = f[k];
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    // ac[k] plays the role of c
+    // d = +-c
+    bool order_lemma_on_factor_and_equiv(unsigned d, unsigned i_mon, const factorization& ac, unsigned k) {
+        TRACE("nla_solver", tout << "d = " << d << ", k = " << k << ", ac[k] = " << ac[k] << std::endl; );
+        SASSERT(abs(vvr(d)) == abs(vvr(ac[k])));
+        lpvar j = ac[k];
         for (unsigned i : m_monomials_containing_var[j]) {
-            if (order_lemma_on_factor_equiv_and_other_mon(i, e_j, i_mon, f, k, sign)) {
+            if (order_lemma_on_factor_equiv_and_other_mon(i, d, i_mon, ac, k)) {
                 return true;
             }
         }
         return false;
     }
 
-    
-    bool order_lemma_on_factor(unsigned i_mon, const factorization& f, unsigned k, int sign) {
-        lpvar j = f[k];
-        TRACE("nla_solver", tout << "k = " << k << ", j = " << j; );
-        for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j)) {
-            TRACE("nla_solver", tout << "p.var() = " << p.var() << ", p.sign() = " << p.sign(); );
-            if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) {
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    // ac[k] plays the role of c   
+    bool order_lemma_on_factor(unsigned i_mon, const factorization& ac, unsigned k) {
+        lpvar c = ac[k];
+        TRACE("nla_solver", tout << "k = " << k << ", c = " << c; );
+        for (const index_with_sign& d : m_vars_equivalence.get_equivalent_vars(c)) {
+            TRACE("nla_solver", tout << "d.var() = " << d.var() << ", d.sign() = " << d.sign(); );
+            if (order_lemma_on_factor_and_equiv(d.m_i, i_mon, ac, k)) {
                 return true;
             }
         }
         return false;
     }
 
-    bool order_lemma_on_factorization(unsigned i_mon, const factorization& f) {
-        TRACE("nla_solver", print_factorization(f, tout););
-        for (unsigned k = 0; k < f.size(); k++) {
-            const rational & v = vvr(f[k]);
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    bool order_lemma_on_factorization(unsigned i_mon, const factorization& ac) {
+        TRACE("nla_solver", tout << "factorization = "; print_factorization(ac, tout););
+        for (unsigned k = 0; k < ac.size(); k++) {
+            const rational & v = vvr(ac[k]);
             if (v.is_zero())
                 continue;
 
-            int sign = (v.is_pos() == f.sign().is_pos())? 1 : -1;
-            
-            if (order_lemma_on_factor(i_mon, f, k, sign)) { 
+            if (order_lemma_on_factor(i_mon, ac, k)) { 
                 return true;
             }
         }
         return false;
     }
 
+     // a > b && c == d => ac > bd
     bool order_lemma_on_monomial(unsigned i_mon) {
         TRACE("nla_solver", print_monomial_with_vars(i_mon, tout););
-        for (auto factorization : factorization_factory_imp(i_mon, *this)) {
-            if (factorization.is_empty())
+        for (auto ac : factorization_factory_imp(i_mon, *this)) {
+            if (ac.is_empty())
                 continue;
-            if (order_lemma_on_factorization(i_mon, factorization))
+            if (order_lemma_on_factorization(i_mon, ac))
                 return true;
         }
         return false;
@@ -1525,20 +1655,20 @@ void solver::test_order_lemma() {
         i = 8, j = 9,
         ab = 10, cd = 11, ef = 12, abef = 13, cdij = 16, ij = 17;
     
-    lpvar lp_a = s.add_var(a, true);
-    lpvar lp_b = s.add_var(b, true);
-    lpvar lp_c = s.add_var(c, true);
-    lpvar lp_d = s.add_var(d, true);
-    lpvar lp_e = s.add_var(e, true);
-    lpvar lp_f = s.add_var(f, true);
-    lpvar lp_i = s.add_var(i, true);
-    lpvar lp_j = s.add_var(j, true);
-    lpvar lp_ab = s.add_var(ab, true);
-    lpvar lp_cd = s.add_var(cd, true);
-    lpvar lp_ef = s.add_var(ef, true);
-    lpvar lp_ij = s.add_var(ij, true);
-    lpvar lp_abef = s.add_var(abef, true);
-    lpvar lp_cdij = s.add_var(cdij, true);
+    lpvar lp_a = s.add_named_var(a, true, "a");
+    lpvar lp_b = s.add_named_var(b, true, "b");
+    lpvar lp_c = s.add_named_var(c, true, "c");
+    lpvar lp_d = s.add_named_var(d, true, "d");
+    lpvar lp_e = s.add_named_var(e, true, "e");
+    lpvar lp_f = s.add_named_var(f, true, "f");
+    lpvar lp_i = s.add_named_var(i, true, "i");
+    lpvar lp_j = s.add_named_var(j, true, "j");
+    lpvar lp_ab = s.add_named_var(ab, true, "ab");
+    lpvar lp_cd = s.add_named_var(cd, true, "cd");
+    lpvar lp_ef = s.add_named_var(ef, true, "ef");
+    lpvar lp_ij = s.add_named_var(ij, true, "ij");
+    lpvar lp_abef = s.add_named_var(abef, true, "abef");
+    lpvar lp_cdij = s.add_named_var(cdij, true, "cdij");
 
     for (unsigned j = 0; j < s.number_of_vars(); j++) {
         s.set_column_value(j, rational(3));

src/util/lp/var_register.h

@@ -21,21 +21,38 @@ namespace lp  {
 class ext_var_info {
     unsigned m_external_j; // the internal index
     bool m_is_integer;
+    std::string m_name;
 public:
     ext_var_info() {}
     ext_var_info(unsigned j): ext_var_info(j, true) {}
     ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {}
+    ext_var_info(unsigned j , bool is_int, std::string name) : m_external_j(j), m_is_integer(is_int), m_name(name) {}
+    
     unsigned external_j() const { return m_external_j;}
     bool is_integer() const {return m_is_integer;}
+    void set_name(std::string name) { m_name = name; }
+    std::string get_name() const { return m_name; }
 };
 
 class var_register {
     svector<ext_var_info> m_local_to_external;
     std::unordered_map<unsigned, unsigned> m_external_to_local;
 public:
+
+    
+    
     unsigned add_var(unsigned user_var) {
         return add_var(user_var, true);
     }    
+
+    void set_name(unsigned j, std::string name) {
+        m_local_to_external[j].set_name(name);
+    }
+
+    std::string get_name(unsigned j) const {
+        return m_local_to_external[j].get_name();
+    }
+
     unsigned add_var(unsigned user_var, bool is_int) {
         auto t = m_external_to_local.find(user_var);
         if (t != m_external_to_local.end()) {