Merge pull request #1 from Z3Prover/master

src/ast/static_features.cpp

@@ -111,16 +111,6 @@ void static_features::flush_cache() {
     m_expr2formula_depth.reset();
 }
 
-#if 0
-bool static_features::is_non_linear(expr * e) const {
-    if (!is_arith_expr(e))
-        return false;
-    if (is_numeral(e))
-        return true;
-    if (m_autil.is_add(e))
-        return true; // the non
-} 
-#endif
 
 bool static_features::is_diff_term(expr const * e, rational & r) const {
     // lhs can be 'x' or '(+ k x)'
@@ -301,10 +291,12 @@ void static_features::update_core(expr * e) {
                 m_num_interpreted_constants++;
         }
         if (fid == m_afid) {
+            // std::cout << mk_pp(e, m_manager) << "\n";
             switch (to_app(e)->get_decl_kind()) {
             case OP_MUL:
-                if (!is_numeral(to_app(e)->get_arg(0)))
+                if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) {
                     m_num_non_linear++;
+                }
                 break;
             case OP_DIV:
             case OP_IDIV:

src/smt/smt_setup.cpp

@@ -978,7 +978,7 @@ namespace smt {
         if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) {
             if (!st.m_has_real)
                 setup_QF_UFLIA(st);
-            else if (!st.m_has_int)
+            else if (!st.m_has_int && st.m_num_non_linear == 0)
                 setup_QF_UFLRA();
             else
                 setup_unknown();

src/util/obj_ref_hashtable.h

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    obj_ref_hashtable.h
+
+Abstract:
+
+    corresponding obj_map with reference count managment.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2017-12-8
+
+Revision History:
+
+--*/
+#ifndef OBJ_REF_HASHTABLE_H_
+#define OBJ_REF_HASHTABLE_H_
+
+#include "util/obj_hashtable.h"
+
+template<typename M, typename Key, typename Value>
+class obj_ref_map {
+    M&                  m;
+    obj_map<Key, Value> m_table;
+public:
+    obj_ref_map(M& m):m(m) {}
+    
+    ~obj_ref_map() { reset();  }
+
+    void reset() {
+        for (auto& kv : m_table) {
+            m.dec_ref(kv.m_key);
+        }
+        m_table.reset();
+    }
+
+    void finalize() {
+        reset();
+        m_table.finalize();
+    }
+
+    bool empty() const { return m_table.empty(); }
+
+    unsigned size() const { return m_table.size();  }
+    
+    unsigned capacity() const { return m_table.capacity();  }
+    
+    iterator begin() const { return m_table.begin(); }
+    
+    iterator end() const { return m_table.end();  }
+    
+    void insert(Key * const k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        m_table.insert(k, v);
+    }
+
+    void insert(Key * const k, Value && v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        m_table.insert(k, v);
+    }
+    
+    key_data const & insert_if_not_there(Key * k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        return m_table.insert_if_not_there(k, v);
+    }
+
+    obj_map_entry * insert_if_not_there2(Key * k, Value const & v) {
+        if (!m_table.contains(k)) m.inc_ref(k);
+        return m_table.insert_if_not_there2(k, v);
+    }
+    
+    obj_map_entry * find_core(Key * k) const { return m_table.find_core(k); }
+
+    bool find(Key * const k, Value & v) const { return m_table.find(k, v); }
+
+    value const & find(key * k) const { return m_table.find(k); }
+
+    value & find(key * k)  { return m_table.find(k); }
+
+    value const & operator[](key * k) const { return find(k); }
+
+    value & operator[](key * k) { return find(k); }
+    
+    iterator find_iterator(Key * k) const { return m_table.find_iterator(k); }
+
+    bool contains(Key * k) const { return m_table.contains(k); }
+
+    void remove(Key * k) { 
+        if (m_table.contains(k)) {
+            m_table.remove(k);
+            m.dec_ref(k);
+        }
+    }
+    
+    void erase(Key * k) { remove(k); }
+
+    unsigned long long get_num_collision() const { return m_table.get_num_collision(); }
+
+    void swap(obj_ref_map & other) {
+        m_table.swap(other.m_table);
+    }
+
+    
+};
+
+
+#endif /* OBJ_REF_HASHTABLE_H_ */
+