add hilbert basis utility for extracting auxiliary invariants

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/test/ast.cpp

@@ -62,7 +62,7 @@ static void tst1() {
 //     SASSERT(foo_foo_x2 == foo_foo_x);
 }
 
-void tst2() {
+static void tst2() {
 //     ast_manager m;
 //     ast_vector<ast> m_nodes(m);
 

src/test/main.cpp

@@ -207,6 +207,7 @@ int main(int argc, char ** argv) {
     TST(horn_subsume_model_converter);
     TST(model2expr);
     TST(rcf);
+    TST(hilbert_basis);
 }
 
 void initialize_mam() {}

src/util/heap.h

@@ -238,6 +238,24 @@ public:
         m_values.swap(other.m_values);
         m_value2indices.swap(other.m_value2indices);
     }
+
+    /**
+       \brief return set of values in heap that are less or equal to val.
+     */
+    void find_le(int val, int_vector& result) {
+        int_vector todo;
+        todo.push_back(1);
+        while (!todo.empty()) {
+            int index = todo.back();
+            todo.pop_back();
+            if (index < static_cast<int>(m_values.size()) &&
+                !less_than(val, m_values[index])) {
+                result.push_back(m_values[index]);
+                todo.push_back(left(index));
+                todo.push_back(right(index));
+            }
+        }
+    }
   
 };
 

src/util/vector.h

@@ -179,6 +179,9 @@ public:
     }
 
     vector & operator=(vector const & source) {
+        if (this == &source) {
+            return *this;
+        }
         destroy();
         if (source.m_data) {
             copy_core(source);