From 8670e0926906805491c0ef84814f7c0c5af56b99 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 27 Jun 2019 15:07:43 -0700
Subject: [PATCH] starting the horner heuristic

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp | 14 ++++++++++++--
 src/math/lp/horner.h   |  5 ++++-
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 0bb6d7400..9dd0011d1 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -25,7 +25,17 @@ namespace nla {
 
 horner::horner(core * c) : common(c) {}
 
-void horner::lemma_on_row(const lp::row_strip<rational>&) {}
+template <typename T>
+bool horner::row_is_interesting(const T&) const {
+    return true;
+}
+
+template <typename T> 
+void horner::lemma_on_row(const T& row) {
+    if (!row_is_interesting(row))
+        return;
+    SASSERT(false);
+}
 
 void horner::horner_lemmas() {
     if (!c().m_settings.run_horner()) {
@@ -37,7 +47,7 @@ void horner::horner_lemmas() {
     unsigned r = random();
     unsigned s = m.row_count();
     for (unsigned i = 0; i < s && !done(); i++) {
-        lemma_on_row(m.m_rows[(i%s)]);
+        lemma_on_row(m.m_rows[((i + r) %s)]);
     }
     
     SASSERT(false);
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index 16b51a9e0..ff6d67dbe 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -29,7 +29,10 @@ class horner : common {
 public:
     horner(core *core);
     void horner_lemmas();
-    void lemma_on_row(const lp::row_strip<rational>&);
+    template <typename T> // T has an iterator of (coeff(), var())
+    void lemma_on_row(const T&);
+    template <typename T>
+    bool row_is_interesting(const T&) const;
 private:    
 }; // end of horner
 }