Changes between Version 58 and Version 59 of IR2

Timestamp:

05/01/21 10:53:52 (5 years ago)

Author:

siegel

Comment:

--

IR2

@@ -34 +34 @@
   * For now, you can't.  [Note to self: consider creating a type like `$byte` for this purpose?]
 1. **How do you iterate over a domain?**
+  * Coming soon.
+1. ** Bitvectors? **
   * Coming soon.
 
@@ -242 +244 @@
 === `civlc.cvh` ===
 
+* `round(e,t)`: returns value in numerical type `t` that is "closest" to the given value `e`
+ * add argument for rounding mode?
+ * exception if out of range?
+* `floor(e)` : given a real or floating number, returns the greatest `Integer` less than or equal to it.
+* `ceil(e)` : given a real or floating number, returns the least `Integer` greater than or equal to it.
+* `abs(e)`: given any numeric expression e, returns the absolute value; result is same type as `e`.
+* `pow(e,n)`: power operator
+ * given any numeric expression e and expression `n` of any integral type, returns e to the n-th power.
+ * `n` must evaluate to a nonnegative integer.
+* `herbrand(e)`: "Herbrandize" a numeric value.
+ * given a numeric value of type `T`, returns the value as type `Herbrand[T]`, a trivial symbolic expression consisting of a single node.
+* `eval(e)` : evaluate a Herbrand expression
+ * given a value of type `Herbrand[T]`, returns the value of type `T` obtained by evaluating all the delayed operations
+ * exceptions may be thrown if evaluating any of the delayed operations results in an exception
+
+
+
 {{{
 
@@ -248 +267 @@
 === `mem.cvh` ===
 
+* `mem_reach(ptr)`, where `ptr` is an expression with a pointer type.
+ * This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.
+* `mem_union(mem1,mem2)`, where `mem1` and `mem2` are expressions of type `Mem`.
+ * This is the union of the two memory sets.
+* `mem_isect(mem1,mem1)` : set intersection
+* `mem_comp(mem1)` : set complement (everything not in `mem1`)
+* `mem_slice(a,dom)`
+ * where `a` is an expression of array type and `dom` is an expression of `Domain` type.
+ * The dimension of the array must match the dimension of the domain.   This represents all memory units which are the cells in the array indexed by a tuple in `dom`.
+
 === `seq.cvh` ===
 
+Should these be language primitives or library functions (or does it matter)?
+
+* need concrete sequence
+* `seq_add(a,e)` : array obtained by adding element e to the end of the array.  Original array a is not modified.
+* `seq_append(a1,a2)` : array obtained by concatenating two arrays.  Original array not modified.
+* `seq_remove(a,i)` : array obtained by removing element at position i from a.  Original array a not modified.
+* `seq_insert(a,i,x)` : array obtained by inserting an element x at position i in a.
+* `seq_length(a)` : returns length of array a (an `Integer`)
+
 === `set.cvh` ===
+
+* concrete set
+* add an element to a set
+* test if an element is in a set
+* union
+* intersection
+* difference
+
 
 === `map.cvh` ===