starting the horner heuristic

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

src/math/lp/CMakeLists.txt

@@ -10,6 +10,7 @@ z3_add_component(lp
     factorization.cpp
     factorization_factory_imp.cpp
     gomory.cpp
+    horner.cpp
     indexed_vector.cpp
     int_solver.cpp
     lar_solver.cpp

src/math/lp/horner.cpp

@@ -0,0 +1,46 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+
+#include "math/lp/horner.h"
+#include "math/lp/nla_core.h"
+
+namespace nla {
+
+horner::horner(core * c) : common(c) {}
+
+void horner::lemma_on_row(const lp::row_strip<rational>&) {}
+
+void horner::horner_lemmas() {
+    if (!c().m_settings.run_horner()) {
+        TRACE("nla_solver", tout << "not generating horner lemmas\n";);
+        return;
+    }
+
+    const auto& m = c().m_lar_solver.A_r();
+    unsigned r = random();
+    unsigned s = m.row_count();
+    for (unsigned i = 0; i < s && !done(); i++) {
+        lemma_on_row(m.m_rows[(i%s)]);
+    }
+    
+    SASSERT(false);
+}
+
+}

src/math/lp/horner.h

@@ -0,0 +1,35 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Module Name:
+
+  <name>
+
+  Abstract:
+
+  <abstract>
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  Revision History:
+
+
+  --*/
+#pragma once
+
+#include "math/lp/nla_common.h"
+
+namespace nla {
+class core;
+
+
+class horner : common {   
+public:
+    horner(core *core);
+    void horner_lemmas();
+    void lemma_on_row(const lp::row_strip<rational>&);
+private:    
+}; // end of horner
+}

src/math/lp/nla_core.cpp

@@ -29,8 +29,8 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_basics(this),
     m_order(this),
     m_monotone(this),
-    m_emons(m_evars) {
-}
+    m_horner(this),
+    m_emons(m_evars) {}
     
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
     switch(cmp) {
@@ -182,7 +182,7 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
     bool first = true;
     for (lpvar v : m) {
         if (!first) out << "*"; else first = false;
-        if (settings().m_print_external_var_name)
+        if (lp_settings().m_print_external_var_name)
             out << "(" << m_lar_solver.get_variable_name(v) << "=" << val(v) << ")";
         else
             out << "(v" << v << " =" << val(v) << ")";
@@ -229,7 +229,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
 }
 
 std::ostream& core::print_monomial(const monomial& m, std::ostream& out) const {
-    if (settings().m_print_external_var_name)
+    if (lp_settings().m_print_external_var_name)
         out << "([" << m.var() << "] = " << m_lar_solver.get_variable_name(m.var()) << " = " << val(m.var()) << " = ";
     else 
         out << "(v" << m.var() << " = " << val(m.var()) << " = ";
@@ -805,14 +805,14 @@ bool core:: mon_has_zero(const T& product) const {
 template bool core::mon_has_zero<unsigned_vector>(const unsigned_vector& product) const;
 
 
-lp::lp_settings& core::settings() {
+lp::lp_settings& core::lp_settings() {
     return m_lar_solver.settings();
 }
-const lp::lp_settings& core::settings() const {
+const lp::lp_settings& core::lp_settings() const {
     return m_lar_solver.settings();
 }
     
-unsigned core::random() { return settings().random_next(); }
+unsigned core::random() { return lp_settings().random_next(); }
     
 
 // we look for octagon constraints here, with a left part  +-x +- y 
@@ -1268,6 +1268,12 @@ bool core:: done() const {
 }
         
 lbool core:: inner_check(bool derived) {
+    if (derived &&  (lp_settings().st().m_nla_calls % m_settings.horner_frequency() == 0))
+        m_horner.horner_lemmas();
+    if (done()) {
+        return l_false;
+    }
+       
     TRACE("nla_cn", print_terms(tout););
     for (int search_level = 0; search_level < 3 && !done(); search_level++) {
         TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";);
@@ -1318,8 +1324,8 @@ bool core::elists_are_consistent(bool check_in_model) const {
 }
 
 lbool core::check(vector<lemma>& l_vec) {
-    settings().st().m_nla_calls++;
-    TRACE("nla_solver", tout << "calls = " << settings().st().m_nla_calls << "\n";);
+    lp_settings().st().m_nla_calls++;
+    TRACE("nla_solver", tout << "calls = " << lp_settings().st().m_nla_calls << "\n";);
     m_lemma_vec =  &l_vec;
     if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) {
         TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";);

src/math/lp/nla_core.h

@@ -28,6 +28,7 @@
 #include "math/lp/emonomials.h"
 #include "math/lp/nla_settings.h"
 #include "math/lp/nla_expr.h"
+#include "math/lp/horner.h"
 namespace nla {
 
 template <typename A, typename B>
@@ -86,8 +87,11 @@ public:
     basics                   m_basics;
     order                    m_order;
     monotone                 m_monotone;
+    horner                   m_horner;
+    nla_settings             m_settings;
+private:
     emonomials               m_emons;
-    svector<lpvar>            m_add_buffer;
+    svector<lpvar>           m_add_buffer;
 public:
     emonomials& emons() { return m_emons; }
     const emonomials& emons() const { return m_emons; }
@@ -277,8 +281,8 @@ public:
 
     template <typename T>
     bool mon_has_zero(const T& product) const;
-    lp::lp_settings& settings();
-    const lp::lp_settings& settings() const;
+    lp::lp_settings& lp_settings();
+    const lp::lp_settings& lp_settings() const;
     unsigned random();
     void map_monomial_vars_to_monomial_indices(unsigned i);
 

src/math/lp/nla_settings.h

@@ -23,12 +23,25 @@ namespace nla {
 class nla_settings {
     bool m_run_order;
     bool m_run_tangents;
+    bool m_run_horner;
+    // how often to call the horner heuristic
+    unsigned m_horner_frequency;
 public:
-    nla_settings() : m_run_order(true), m_run_tangents(true) {}
+    nla_settings() : m_run_order(true),
+                     m_run_tangents(true),
+                     m_run_horner(true),
+                     m_horner_frequency(4) {}
+    
     bool run_order() const { return m_run_order; }
     bool& run_order() { return m_run_order; }
 
     bool run_tangents() const { return m_run_tangents; }
     bool& run_tangents() { return m_run_tangents; }    
+
+    bool run_horner() const { return m_run_horner; }
+    bool& run_horner() { return m_run_horner; }    
+
+    unsigned horner_frequency() const { return m_horner_frequency; }
+    unsigned& horner_frequency() { return m_horner_frequency; }    
 };
 }