port Grobner, add fixed var dependency to Horner's scheme

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

src/math/lp/cross_nested.h

@@ -24,7 +24,7 @@
 
 namespace nla {
 class cross_nested {
-
+    
     // fields
     nex *                                             m_e;
     std::function<bool (const nex*)>                  m_call_on_result;

src/math/lp/horner.cpp

@@ -69,7 +69,6 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
     return cn.done();
 }
 
-
 bool horner::check_cross_nested_expr(const nex* n) {
     TRACE("nla_horner", tout << "cross-nested n = " << *n << ", n->type() == " << n->type() << "\n";);
     c().lp_settings().stats().m_cross_nested_forms++;
@@ -80,9 +79,9 @@ bool horner::check_cross_nested_expr(const nex* n) {
         m_intervals.reset();
         return false;
     }
-    auto id = interval_of_expr_with_deps(n, 1);
-    TRACE("nla_horner", tout << "conflict: id = "; m_intervals.display(tout, id ) << *n << "\n";);
-    m_intervals.check_interval_for_conflict_on_zero(id);
+    auto interv_wd = interval_of_expr_with_deps(n, 1);
+    TRACE("nla_horner", tout << "conflict: interv_wd = "; m_intervals.display(tout, interv_wd ) << *n << "\n";);
+    m_intervals.check_interval_for_conflict_on_zero(interv_wd, m_fixed_var_deps);
     m_intervals.reset(); // clean the memory allocated by the interval bound dependencies
     return true;
 }
@@ -95,7 +94,7 @@ bool horner::lemmas_on_row(const T& row) {
         [this]() { return c().random(); }, m_nex_creator);
 
     SASSERT (row_is_interesting(row));
-    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum);
+    create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, m_fixed_var_deps);    
     nex* e =  m_nex_creator.simplify(&m_row_sum);
     if (!e->is_sum())
         return false;
@@ -109,6 +108,7 @@ void horner::horner_lemmas() {
         return;
     }
     c().lp_settings().stats().m_horner_calls++;
+    set_active_vars_weights();
     const auto& matrix = c().m_lar_solver.A_r();
     // choose only rows that depend on m_to_refine variables
     std::set<unsigned> rows_to_check; // we need it to be determenistic: cannot work with the unordered_set

src/math/lp/horner.h

@@ -32,6 +32,7 @@ class core;
 class horner : common {
     intervals             m_intervals;
     nex_sum               m_row_sum;
+    ci_dependency*        m_fixed_var_deps;
 public:
     typedef intervals::interval interv;
     horner(core *core);

src/math/lp/nex.h

@@ -269,6 +269,8 @@ public:
         return get_degree() < 2; // todo: make it more efficient
     }
 
+     bool all_factors_are_elementary() const;
+
 // #ifdef Z3DEBUG
 //     virtual void sort() {
 //         for (nex * c : m_children) {
@@ -418,6 +420,7 @@ inline std::ostream& operator<<(std::ostream& out, const nex& e ) {
 //     return less_than_nex(a, b, lt);
 // }
 
+
 inline std::unordered_set<lpvar> get_vars_of_expr(const nex *e ) {
         std::unordered_set<lpvar> r;
         switch (e->type()) {

src/math/lp/nex_creator.cpp

@@ -561,17 +561,18 @@ void nex_creator::simplify_children_of_sum(ptr_vector<nex> & children) {
     sort_join_sum(children);
 }
 
-bool all_factors_are_elementary(const nex_mul* a) {
+
+bool have_no_scalars(const nex_mul* a) {
     for (auto & p : *a)
-        if (!p.e()->is_elementary())
+        if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
             return false;
 
     return true;
 }
 
-bool have_no_scalars(const nex_mul* a) {
-    for (auto & p : *a)
-        if (p.e()->is_scalar() && !to_scalar(p.e())->value().is_one())
+bool nex_mul::all_factors_are_elementary() const {
+    for (auto & p : *this)
+        if (!p.e()->is_elementary())
             return false;
 
     return true;
@@ -587,7 +588,7 @@ nex * nex_creator::mk_div_sum_by_mul(const nex_sum* m, const nex_mul* b) {
 }
 
 nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
-    SASSERT(all_factors_are_elementary(a) && all_factors_are_elementary(b));
+    SASSERT(a->all_factors_are_elementary() && b->all_factors_are_elementary());
     b->get_powers_from_mul(m_powers);
     nex_mul* ret = new nex_mul();
     for (auto& p_from_a : *a) {

src/math/lp/nla_common.cpp

@@ -155,8 +155,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn) {
 }
 
 
-template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum) {
+template <typename T> void common::create_sum_from_row(const T& row, nex_creator& cn, nex_sum& sum, ci_dependency*& fixed_var_deps) {
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
+
+    fixed_var_deps = nullptr;
     
     SASSERT(row.size() > 1);
     sum.children().clear();
@@ -204,5 +206,5 @@ var_weight common::get_var_weight(lpvar j) const {
 
 
 }
-template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&);
+template void nla::common::create_sum_from_row<old_vector<lp::row_cell<rational>, true, unsigned int> >(old_vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_sum&, ci_dependency*&);
 

src/math/lp/nla_common.h

@@ -120,7 +120,7 @@ struct common {
     nex* nexvar(lpvar j, nex_creator& );
     nex* nexvar(const rational& coeff, lpvar j, nex_creator&);
     template <typename T>
-    void create_sum_from_row(const T&, nex_creator&, nex_sum&);
+    void create_sum_from_row(const T&, nex_creator&, nex_sum&, ci_dependency*&);
     void set_active_vars_weights();
     var_weight get_var_weight(lpvar) const;
 };

src/math/lp/nla_grobner.cpp

@@ -176,9 +176,9 @@ void nla_grobner::add_row(unsigned i) {
     const auto& row = c().m_lar_solver.A_r().m_rows[i];    
     TRACE("nla_grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout););
     nex_sum * ns = m_nex_creator.mk_sum();
-    create_sum_from_row(row, m_nex_creator, *ns);
+    ci_dependency * dep;
+    create_sum_from_row(row, m_nex_creator, *ns, dep);
     TRACE("nla_grobner", tout << "ns = " << *ns << "\n";);
-    ci_dependency * dep = nullptr;
     m_tmp_var_set.clear();
     assert_eq_0(ns, dep);
 }
@@ -195,7 +195,6 @@ void nla_grobner::init() {
     for (unsigned i : m_rows) {
         add_row(i);
     }
-    set_active_vars_weights();
     simplify_equations_to_process();
 }
 
@@ -266,17 +265,35 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) {
 
 }
 
+const nex_mul* nla_grobner::get_highest_monomial(const nex* e) const {
+    switch (e->type()) {
+    case expr_type::MUL:
+        return to_mul(e);
+    case expr_type::SUM:
+        return to_mul((*to_sum(e))[0]);
+    default:
+        return nullptr;
+    }    
+}
 // source 3f + k = 0, so f = -k/3
 // target 2fg + e = 0  
 // target is replaced by 2(-k/3)g + e = -2/3kg + e
-unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) {
-    TRACE("nla_grobner", tout << "source = " << *source->exp() << " , target = " << *target->exp() << "\n";);
+bool nla_grobner::simplify_target_monomials(equation const * source, equation * target) {
+    const nex_mul * high_mon = get_highest_monomial(source->exp());
+    if (high_mon == nullptr)
+        return false;
+    SASSERT(high_mon->all_factors_are_elementary());
+    TRACE("nla_grobner", tout << "source = "; display_equation(tout, *source) << " , target = "; display_equation(tout, *target) << " , high_mon = " << *high_mon << "\n";);
+
+    NOT_IMPLEMENTED_YET();
+    
+    /*
     unsigned i          = 0;
     unsigned new_target_sz = 0;
     unsigned sz         = target->exp()->size();
     //if (source->exp()->is_sum() && target->exp()->is_su
     NOT_IMPLEMENTED_YET();
-    /*
+    
     monomial const * LT = source->get_monomial(0); 
     ptr_vector<monomial> & new_monomials = m_tmp_monomials;
     new_monomials.reset();
@@ -305,7 +322,7 @@ unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source,
             target->m_monomials[n_sz++] = curr;
         }
         }*/
-    return 1;
+    return false;
 }
 
 
@@ -316,23 +333,18 @@ nla_grobner::equation * nla_grobner::simplify_source_target(equation const * sou
     m_stats.m_simplify++;
     bool result = false;
     do {
-        unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result);
-        if (target_new_size < target->exp()->size()) {
-            NOT_IMPLEMENTED_YET();
-            /*
-              target->m_monomials.shrink(target_new_size);
-            target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
-            simplify_eq(target);
-            */
+        if (simplify_target_monomials(source, target)) {
+            result = true;
         } else {
-            NOT_IMPLEMENTED_YET();
             break;
         }
+    } while (!canceled());
+    TRACE("grobner", tout << "result: " << result << "\n"; if (result) display_equation(tout, *target););
+    if (result) {
+        target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
+        return target;
     }
-    while (!canceled());
-    TRACE("grobner", tout << "result: "; display_equation(tout, *target););
-    return result ? target : nullptr;
-}
+    return nullptr;}
  
 void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
     if (new_target != target) {
@@ -549,6 +561,7 @@ void nla_grobner:: del_equations(unsigned old_size) {
 }
 
 void nla_grobner::display_equations(std::ostream & out, equation_set const & v, char const * header) const {
+    out << header << "\n";
     NOT_IMPLEMENTED_YET();
 }
 

src/math/lp/nla_grobner.h

@@ -116,7 +116,7 @@ private:
     bool compute_basis_step();
     equation * simplify_source_target(equation const * source, equation * target);
     equation* simplify_using_processed(equation*);
-    unsigned simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result);
+    bool simplify_target_monomials(equation const * source, equation * target);
     void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);
 bool simplify_processed_with_eq(equation*);
     void simplify_to_process(equation*);
@@ -164,5 +164,6 @@ bool simplify_processed_with_eq(equation*);
     std::ostream& display_dependency(std::ostream& out, ci_dependency*);
     void insert_to_process(equation *eq) { m_to_process.insert(eq); }
     void simplify_equations_to_process();
+    const nex_mul * get_highest_monomial(const nex * e) const;
 }; // end of grobner
 }

src/math/lp/nla_intervals.cpp

@@ -103,27 +103,33 @@ bool intervals::separated_from_zero_on_upper(const interval& i) const {
 }
 
 
-bool intervals::check_interval_for_conflict_on_zero(const interval & i) {
-    return check_interval_for_conflict_on_zero_lower(i) || check_interval_for_conflict_on_zero_upper(i);
+bool intervals::check_interval_for_conflict_on_zero(const interval & i, ci_dependency * fixed_var_deps) {
+    return check_interval_for_conflict_on_zero_lower(i, fixed_var_deps) || check_interval_for_conflict_on_zero_upper(i, fixed_var_deps);
 }
 
-bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i) {
+bool intervals::check_interval_for_conflict_on_zero_upper(const interval & i, ci_dependency* fixed_var_deps) {
     if (!separated_from_zero_on_upper(i))
         return false;
         
      add_empty_lemma();
      svector<lp::constraint_index> expl;
+     if (fixed_var_deps)
+         m_dep_manager.linearize(fixed_var_deps, expl); 
+         
      m_dep_manager.linearize(i.m_upper_dep, expl); 
      _().current_expl().add_expl(expl);
      TRACE("nla_solver", print_lemma(tout););
      return true;
 }
 
-bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i) {
+bool intervals::check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency* fixed_var_deps) {
     if (!separated_from_zero_on_lower(i))
         return false;
      add_empty_lemma();
      svector<lp::constraint_index> expl;
+     if (fixed_var_deps)
+         m_dep_manager.linearize(fixed_var_deps, expl); 
+
      m_dep_manager.linearize(i.m_lower_dep, expl); 
      _().current_expl().add_expl(expl);
      TRACE("nla_solver", print_lemma(tout););

src/math/lp/nla_intervals.h

@@ -425,9 +425,9 @@ public:
         return separated_from_zero_on_upper(i) ||
             separated_from_zero_on_lower(i);            
         }
-    bool check_interval_for_conflict_on_zero(const interval & i);
-    bool check_interval_for_conflict_on_zero_lower(const interval & i);
-    bool check_interval_for_conflict_on_zero_upper(const interval & i);
+    bool check_interval_for_conflict_on_zero(const interval & i, ci_dependency*);
+    bool check_interval_for_conflict_on_zero_lower(const interval & i, ci_dependency*);
+    bool check_interval_for_conflict_on_zero_upper(const interval & i, ci_dependency*);
     mpq const & lower(interval const & a) const { return m_config.lower(a); }
     mpq const & upper(interval const & a) const { return m_config.upper(a); }
     inline