Sync with master

include/crab/cfg/cfg.hpp

@@ -48,7 +48,7 @@
 #include <boost/unordered_map.hpp>
 
 #include <crab/common/types.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 #include <crab/domains/linear_constraints.hpp>
 #include <crab/domains/interval.hpp>
 #include <crab/domains/discrete_domains.hpp>

include/crab/domains/array_expansion.hpp

@@ -1266,43 +1266,41 @@ namespace domains {
 	CRAB_ERROR("array expansion domain expects constant array element sizes");		
       }
 
-      bool ignore_array_store = false;
       interval_t lb_i = to_interval(lb_idx);
       auto lb = lb_i.singleton();
       if (!lb) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "lower bound is not constant");
-	ignore_array_store = true;
+	return;
       }
 
       interval_t ub_i = to_interval(ub_idx);
       auto ub = ub_i.singleton();
       if (!ub) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "upper bound is not constant");
-	ignore_array_store = true;	
+	return;
       }
 
-
       if ((*ub - *lb) % *n != 0) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "the number of elements must be divisible by ", *n);
-	ignore_array_store = true;		
+	return;
       }
 
+      // TODO: this should be an user parameter.
       const number_t max_num_elems = 512;
+
       if (*ub - *lb > max_num_elems) {
 	CRAB_WARN("array expansion store range ignored because ",
 		  "the number of elements is larger than default limit of ",
 		  max_num_elems);
-	ignore_array_store = true;			
+	return;
       }
 
-      if (!ignore_array_store) {
-	for(number_t i = *lb, e = *ub; i < e; ) {
-	  array_store(a, elem_size, i, val, false);
-	  i = i + *n;
-	}
+      for(number_t i = *lb, e = *ub; i < e; ) {
+	array_store(a, elem_size, i, val, false);
+	i = i + *n;
       }
     }
 

include/crab/domains/graphs/graph_config.hpp

@@ -0,0 +1,166 @@
+#pragma once
+
+#include <type_traits>
+
+#include <crab/numbers/safeint.hpp>
+#include <crab/domains/graphs/adapt_sgraph.hpp>
+#include <crab/domains/graphs/sparse_graph.hpp>
+#include <crab/domains/graphs/ht_graph.hpp>
+#include <crab/domains/graphs/pt_graph.hpp>
+
+namespace crab {
+namespace domains {
+namespace DBM_impl {
+
+// All of these representations are implementations of a
+// sparse weighted graph. They differ on the datastructures
+// used to store successors and predecessors
+enum GraphRep { 
+  // sparse-map and sparse-sets
+  ss = 1,        
+  // adaptive sparse-map and sparse-sets
+  adapt_ss = 2,  
+  // patricia tree-maps and patricia tree-sets
+  pt = 3,           
+  // hash table and hash sets
+  ht = 4
+};          
+
+/** DBM weights (Wt) can be represented using one of the following
+ * types:
+ * 
+ * 1) basic integer type: e.g., long
+ * 2) safei64
+ * 3) z_number
+ * 
+ * 1) is the fastest but things can go wrong if some DBM
+ * operation overflows. 2) is slower than 1) but it checks for
+ * overflow before any DBM operation. 3) is the slowest and it
+ * represents weights using unbounded mathematical integers so
+ * overflow is not a concern but it might not be what you need
+ * when reasoning about programs with wraparound semantics.
+ **/
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class DefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 
+
+  typedef long Wt;
+
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+// We don't use GraphRep::adapt_ss because having problems
+// realloc'ed Number objects.
+template<typename Number, GraphRep Graph = GraphRep::ss>
+class BigNumDefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 	 
+
+  // Use Number as graph weights
+  typedef Number Wt;
+
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class SafeInt64DefaultParams {
+public:
+  enum { chrome_dijkstra = 1 };
+  enum { widen_restabilize = 1 };
+  enum { special_assign = 1 };
+  enum { close_bounds_inline = 0 };	 
+
+  typedef safe_i64 Wt;
+
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+
+template<typename Number, GraphRep Graph = GraphRep::adapt_ss>
+class SimpleParams {
+public:
+  enum { chrome_dijkstra = 0 };
+  enum { widen_restabilize = 0 };
+  enum { special_assign = 0 };
+  enum { close_bounds_inline = 1 };	 	 
+
+  typedef long Wt;
+
+  typedef typename std::conditional< 
+    (Graph == ss), 
+    SparseWtGraph<Wt>,
+    typename std::conditional< 
+      (Graph == adapt_ss), 
+      AdaptGraph<Wt>,
+      typename std::conditional< 
+	(Graph == pt), 
+	PtGraph<Wt>, 
+	HtGraph<Wt> 
+	>::type 
+      >::type 
+    >::type graph_t;
+};
+
+
+/**
+ * Helper to translate from Number (e.g., ikos::z_number) to DBM
+ * weight.  Number is the template parameter of the DBM-based abstract
+ * domain to represent a number. Note that Number might not fit into
+ * Wt type. If this is the case then a runtime error will be triggered
+ * when Number is casted to Wt
+ **/
+template<typename Number, typename Wt>
+class NtoW {
+public:
+static Wt convert(const Number& n) { 
+  return (Wt) n;
+}
+};
+
+}
+}
+}

include/crab/domains/graphs/graph_ops.hpp

@@ -1202,10 +1202,10 @@ namespace crab {
     */
     template<class G, class P>
     static bool repair_potential(G& g, P& p, vert_id ii, vert_id jj)
-    { 
+    {
       // Ensure there's enough scratch space. 
       unsigned int sz = g.size();
-//      assert(src < (int) sz && dest < (int) sz);
+      // assert(src < (int) sz && dest < (int) sz);
       grow_scratch(sz);
 
       for(vert_id vi : g.verts())
@@ -1249,7 +1249,7 @@ namespace crab {
           }
         }
       }
-      if(dists[ii] < 0)
+      if(dists[ii] < Wt(0))
         return false;
 
       for(vert_id v : g.verts())

include/crab/domains/interval.hpp

@@ -10,7 +10,7 @@
 #include <boost/optional.hpp>
 #include <crab/common/types.hpp>
 #include <crab/common/stats.hpp>
-#include <crab/common/bignums.hpp>
+#include <crab/numbers/bignums.hpp>
 
 namespace ikos {
 

include/crab/domains/linear_interval_solver.hpp

@@ -52,8 +52,8 @@
 #include <crab/common/types.hpp>
 #include <crab/common/debug.hpp>
 #include <crab/common/stats.hpp>
-#include <crab/common/bignums.hpp>
-#include <crab/common/wrapint.hpp>
+#include <crab/numbers/bignums.hpp>
+#include <crab/numbers/wrapint.hpp>
 #include <crab/domains/linear_constraints.hpp>
 
 namespace ikos {